code wiki / (root) / nx_readcap_gate.nx

nx_readcap_gate.nx source

↩ module page · 108 lines · 6353 B

1// nx_readcap_gate.nx -- teeth for nx_readcap_lib: the ONE read-into-cap helper names every outcome the hand-rolled 2// loops could not. In-process (the lib is imported), fixtures built at SETUP under /tmp/nx_readcap/ (the gate-fixture 3// law), every tooth prints its values, and the negative controls are named so the census can see them. 4// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 5import "nx_syscalls.nx" 6import "nx_gate_verdict.nx" 7import "nx_readcap_lib.nx" 8 9const RG_DIR: *u8 = "/tmp/nx_readcap" as *u8 10const RG_SMALL: *u8 = "/tmp/nx_readcap/small.bin" as *u8 11const RG_BIG: *u8 = "/tmp/nx_readcap/big.bin" as *u8 12const RG_EXACT: *u8 = "/tmp/nx_readcap/exact.bin" as *u8 13const RG_ABSENT: *u8 = "/tmp/nx_readcap/absent.bin" as *u8 14const RG_CAP: i64 = 1000 15const RG_SMALL_N: i64 = 100 16const RG_BIG_N: i64 = 5000 17const RG_MODE_755: i64 = 493 18const RG_MODE_644: i64 = 420 19 20func rg_mkdir(path: *u8) -> i64 { 21 let nbox: *i64 = sys_mmap(16) as *i64 22 nbox[0] = 258 23 let rc: i64 = __syscall(nbox[0], 0 - 100, path as i64, RG_MODE_755, 0, 0, 0) 24 sys_munmap(nbox as *u8, 16) 25 return rc 26} 27// a fixture whose byte i is (i * 7 + 3) mod 251, so any window can be checked against its offset 28func rg_write_fixture(path: *u8, n: i64) -> i64 { 29 let b: *u8 = sys_mmap(n + 16) 30 var i: i64 = 0 31 while i < n { b[i] = ((i * 7 + 3) % 251) as u8; i = i + 1 } 32 let fd: i64 = sys_openat_wr(path, RG_MODE_644) 33 if fd < 0 { return fd } 34 sys_write(fd, b, n) 35 sys_close(fd) 36 return n 37} 38func rg_bytes_match(buf: *u8, n: i64) -> i64 { 39 var i: i64 = 0 40 while i < n { if buf[i] != (((i * 7 + 3) % 251) as u8) { return 0 } i = i + 1 } 41 return 1 42} 43 44func main(argc: i64, argv: *i64) -> i64 { 45 let ctr: *i64 = gv_ctr() 46 gv_head("nx_readcap_gate -- the ONE read-into-cap helper names EOF, CAPPED, TRUNCATED-more-remains, EXACT and ERR" as *u8) 47 // SETUP (idempotent): fixtures rewritten every run 48 rg_mkdir(RG_DIR) 49 sys_unlinkat(RG_ABSENT) 50 gv_check("fixture-small-written (100 B)" as *u8, rg_write_fixture(RG_SMALL, RG_SMALL_N) == RG_SMALL_N, ctr) 51 gv_check("fixture-big-written (5000 B)" as *u8, rg_write_fixture(RG_BIG, RG_BIG_N) == RG_BIG_N, ctr) 52 gv_check("fixture-exact-written (exactly the cap, 1000 B)" as *u8, rg_write_fixture(RG_EXACT, RG_CAP) == RG_CAP, ctr) 53 let buf: *u8 = sys_mmap(RG_CAP + 16) 54 let st: *i64 = sys_mmap(32) as *i64 55 56 // 1. a source smaller than the cap reads whole and says EOF 57 let n1: i64 = rc_read_file_into(RG_SMALL, buf, RG_CAP, st) 58 gv_check_eq("T1 small file: bytes read equal the file" as *u8, n1, RG_SMALL_N, ctr) 59 gv_check_eq("T1b small file: state is EOF" as *u8, st[0], RC_EOF, ctr) 60 gv_check("T1c small file: the bytes are the file's (offset-checked)" as *u8, rg_bytes_match(buf, n1) == 1, ctr) 61 gv_check_eq("T1d small file: rc_complete says COMPLETE" as *u8, rc_complete(st), 1, ctr) 62 63 // 2. a source bigger than the cap fills the cap and is NAMED truncated -- the state no hand-rolled loop had 64 let n2: i64 = rc_read_file_into(RG_BIG, buf, RG_CAP, st) 65 gv_check_eq("T2 big file: bytes read equal the cap (never past it)" as *u8, n2, RG_CAP, ctr) 66 gv_check_eq("T2b big file: state is TRUNCATED-more-remains (RC_FULL)" as *u8, st[0], RC_FULL, ctr) 67 gv_check_eq("T2c big file: the probe saw one more byte" as *u8, st[2], RC_PROBE_BYTES, ctr) 68 gv_check_eq("T2d big file: rc_complete says NOT complete" as *u8, rc_complete(st), 0, ctr) 69 gv_check("T2e big file: the cap window holds the file's first cap bytes" as *u8, rg_bytes_match(buf, n2) == 1, ctr) 70 71 // 3. a source exactly the cap is EXACT, not truncated -- the discrimination the naive loop cannot make 72 let n3: i64 = rc_read_file_into(RG_EXACT, buf, RG_CAP, st) 73 gv_check_eq("T3 exact file: bytes read equal the cap" as *u8, n3, RG_CAP, ctr) 74 gv_check_eq("T3b exact file: state is EXACT (the probe read 0 bytes)" as *u8, st[0], RC_EXACT, ctr) 75 gv_check_eq("T3c exact file: probe rc 0" as *u8, st[2], 0, ctr) 76 gv_check_eq("T3d exact file: rc_complete says COMPLETE" as *u8, rc_complete(st), 1, ctr) 77 78 // 4. neg-control: the socket-safe rc_fill does NOT probe -- the byte after the cap is still unread afterwards 79 let fd4: i64 = sys_openat_rd(RG_BIG) 80 let n4: i64 = rc_fill(fd4, buf, RG_CAP, st) 81 let after: *u8 = sys_mmap(16) 82 let a4: i64 = sys_read(fd4, after, 1) 83 sys_close(fd4) 84 gv_check_eq("neg-control-T4 rc_fill on a bigger source reads exactly the cap and reports CAPPED-unprobed" as *u8, st[0], RC_CAPPED, ctr) 85 gv_check("neg-control-T4b the byte after the cap is STILL THERE (rc_fill consumed nothing past the cap: safe on a socket)" as *u8, (a4 == 1) && (after[0] == (((RG_CAP * 7 + 3) % 251) as u8)), ctr) 86 gv_check_eq("T4c rc_fill bytes equal the cap" as *u8, n4, RG_CAP, ctr) 87 88 // 5. an absent file is ERR with the open rc, and zero bytes -- never a silent empty buffer 89 let n5: i64 = rc_read_file_into(RG_ABSENT, buf, RG_CAP, st) 90 gv_check_eq("neg-control-T5 absent file: zero bytes" as *u8, n5, 0, ctr) 91 gv_check_eq("neg-control-T5b absent file: state ERR" as *u8, st[0], RC_ERR, ctr) 92 gv_check("neg-control-T5c absent file: st[1] carries the open's negative rc" as *u8, st[1] < 0, ctr) 93 gv_check_eq("neg-control-T5d absent file: rc_complete says NOT complete" as *u8, rc_complete(st), 0, ctr) 94 95 // 6. a zero cap reads nothing and says CAPPED (a caller who passes 0 asked for nothing, and is told so) 96 let n6: i64 = rc_read_file_into(RG_SMALL, buf, 0, st) 97 gv_check_eq("T6 cap 0: zero bytes" as *u8, n6, 0, ctr) 98 gv_check_eq("T6b cap 0 on a non-empty file: TRUNCATED-more-remains (the file has bytes the caller did not ask for)" as *u8, st[0], RC_FULL, ctr) 99 100 // 7. the state names spell the census's own announce vocabulary 101 let tn7: *u8 = rc_state_name(RC_FULL) 102 gv_check("T7 the truncated state name starts with TRUNCATED (an adopter that prints it announces its envelope)" as *u8, tn7[0] == (84 as u8), ctr) 103 gv_kv("readcap_small_bytes" as *u8, n1) 104 gv_kv("readcap_big_bytes" as *u8, n2) 105 gv_kv("readcap_exact_bytes" as *u8, n3) 106 gv_kv("readcap_cap" as *u8, RG_CAP) 107 return gv_verdict("NX-READCAP" as *u8, ctr, "one read-into-cap loop for the estate, and every outcome the hand-rolled copies could not name is a state here" as *u8) 108}