nx_zeroprint_gate.nx source
↩ module page · 123 lines · 7435 B
1// nx_zeroprint_gate.nx -- teeth for nx_zeroprint (the zero-prints-as-NUL detector/repairer).
2//
3// The subject's whole job is to tell four look-alike shapes apart, so the fixture carries ALL FOUR
4// and the gate asserts each bucket by name. Three of them MUST come back SAFE; a detector that
5// flagged them would be a false-positive generator, and the estate's own first census of this defect
6// (written in Python) did exactly that -- it could not see the else-form and over-counted by six.
7//
8// EVERY FIXTURE IS ASSEMBLED AT RUNTIME under /tmp/nx_zeroprint_gate/, never shared with a beat and
9// never committed as a file: a detector that scans source WILL find its own test fixture, and a
10// fixture written into the tree would make this gate flag itself forever.
11//
12// T1 is the anti-vacuity tooth: if the planted defect is NOT detected, nothing below proves anything.
13// license_tier: ORIGINAL
14// expect_exit: 0
15import "nx_syscalls.nx"
16import "nx_tool_run.nx"
17import "nx_gate_verdict.nx"
18
19const ZG_DIR: *u8 = "/tmp/nx_zeroprint_gate" as *u8
20const ZG_ELF: *u8 = "./nx_zeroprint.elf" as *u8
21const ZG_CAP: i64 = 65536
22
23func zg_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
24func zg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
25func zg_has(h: *u8, n: i64, needle: *u8) -> i64 {
26 let m: i64 = zg_slen(needle)
27 if m == 0 { return 0 }
28 var i: i64 = 0
29 while i + m <= n {
30 var k: i64 = 0
31 var ok: i64 = 1
32 while k < m { if (h[i+k] & 0xff) != (needle[k] & 0xff) { ok = 0; k = m } else { k = k + 1 } }
33 if ok == 1 { return 1 }
34 i = i + 1
35 }
36 return 0
37}
38func zg_put(path: *u8, body: *u8) -> i64 {
39 let fd: i64 = sys_openat_wr(path, MODE_0644)
40 if fd < 0 { return 0 - 1 }
41 sys_write(fd, body, zg_slen(body))
42 sys_close(fd)
43 return 0
44}
45func zg_run(verb: *u8, out: *u8, olen: *i64) -> i64 {
46 let av: *i64 = sys_mmap(64) as *i64
47 av[0] = ZG_ELF as i64
48 av[1] = verb as i64
49 av[2] = ZG_DIR as i64
50 av[3] = 0
51 return tr_run_capture(ZG_ELF, av, out, ZG_CAP, olen)
52}
53
54func main() -> i64 {
55 zg_puts("=== nx_zeroprint_gate -- four look-alike printer shapes, one must be flagged ===\n" as *u8)
56 let ctr: *i64 = gv_ctr()
57
58 // ---- SETUP: assemble the fixture. sys_mkdir at SETUP, not teardown -- a teardown does not run
59 // when a run crashes, and the next run would then measure the previous run's leftovers.
60 sys_mkdir(ZG_DIR, 0x1ff)
61 let pa: *u8 = "/tmp/nx_zeroprint_gate/a_defect.nx" as *u8
62 let pb: *u8 = "/tmp/nx_zeroprint_gate/b_else.nx" as *u8
63 let pc: *u8 = "/tmp/nx_zeroprint_gate/c_same.nx" as *u8
64 let pd: *u8 = "/tmp/nx_zeroprint_gate/d_early.nx" as *u8
65 zg_put(pa, "func p(v: i64) -> i64 {\n let b: *u8 = sys_mmap(24)\n var m: i64 = v\n var k: i64 = 0\n if m == 0 { b[0] = 48 as u8; k = 1 }\n let t: *u8 = sys_mmap(24)\n while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }\n var i: i64 = 0\n while i < k { b[i] = t[k-1-i]; i = i + 1 }\n return 0\n}\n" as *u8)
66 zg_put(pb, "func q(v: i64) -> i64 {\n let buf: *u8 = sys_mmap(24)\n var m: i64 = v\n var o: i64 = 0\n if m == 0 { buf[0] = 48 as u8; o = 1 } else { let t: *u8 = sys_mmap(24); var k: i64 = 0; while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } while o < k { buf[o] = t[k-1-o]; o = o + 1 } }\n return 0\n}\n" as *u8)
67 zg_put(pc, "func r(v: i64) -> i64 {\n let b: *u8 = sys_mmap(24)\n let o: *u8 = sys_mmap(24)\n var m: i64 = v\n var k: i64 = 0\n if m == 0 { b[0] = 48 as u8; k = 1 }\n while m > 0 { b[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }\n var i: i64 = 0\n while i < k { o[i] = b[k-1-i]; i = i + 1 }\n return 0\n}\n" as *u8)
68 zg_put(pd, "func s(v: i64) -> i64 {\n let b: *u8 = sys_mmap(24)\n var m: i64 = v\n var k: i64 = 0\n if m == 0 { b[0] = 48 as u8; sys_write(1, b, 1); return 0 }\n let t: *u8 = sys_mmap(24)\n while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }\n return 0\n}\n" as *u8)
69
70 let bl: *i64 = sys_mmap(8) as *i64
71 let bbefore: *u8 = sys_read_file(pb, bl)
72 let nb: i64 = bl[0]
73
74 let out: *u8 = sys_mmap(ZG_CAP + 1)
75 let ol: *i64 = sys_mmap(8) as *i64
76 let rc1: i64 = zg_run("scan" as *u8, out, ol)
77 // "I could not run the subject" is NOT a failure of the rule -- abstain instead of acquitting.
78 // gv_need returns 1 when the precondition IS present and 0 when it is MISSING -- the inverse of
79 // the "non-zero means trouble" reflex. Reading it the other way made this gate abstain precisely
80 // BECAUSE its subject was runnable, and report passed 0/0 with no missing-precondition line.
81 if gv_need("subject-nx_zeroprint-is-runnable" as *u8, ol[0] > 0, ctr) == 0 {
82 return gv_verdict("ZEROPRINT" as *u8, ctr, "subject absent or unrunnable -- UNOBSERVABLE, not GREEN" as *u8)
83 }
84 sys_write(1, out, ol[0])
85
86 gv_check("T1-anti-vacuity-planted-defect-IS-detected" as *u8, zg_has(out, ol[0], "DEFECTIVE = 1" as *u8), ctr)
87 gv_check("T2-early-return-shape-classified-safe" as *u8, zg_has(out, ol[0], "early_return = 1" as *u8), ctr)
88 gv_check("T3-neg-control-else-form-NOT-flagged" as *u8, zg_has(out, ol[0], "else_form = 1" as *u8), ctr)
89 gv_check("T4-neg-control-same-buffer-NOT-flagged" as *u8, zg_has(out, ol[0], "same_buffer = 1" as *u8), ctr)
90 gv_check("T5-partition-sums-to-the-site-count" as *u8, zg_has(out, ol[0], "RECONCILES" as *u8), ctr)
91 gv_check("T6-scan-exit-carries-found" as *u8, rc1 == 1, ctr)
92
93 let rc2: i64 = zg_run("apply" as *u8, out, ol)
94 gv_check("T7-apply-repairs-exactly-the-one-defect" as *u8, zg_has(out, ol[0], "repaired = 1" as *u8), ctr)
95 gv_check("T8-apply-exit-clean" as *u8, rc2 == 0, ctr)
96
97 let rc3: i64 = zg_run("scan" as *u8, out, ol)
98 gv_check("T9-rescan-defect-count-is-zero" as *u8, zg_has(out, ol[0], "DEFECTIVE = 0" as *u8), ctr)
99 gv_check("T10-repaired-file-moved-into-same-buffer-bucket" as *u8, zg_has(out, ol[0], "same_buffer = 2" as *u8), ctr)
100 gv_check("T11-rescan-exit-clean" as *u8, rc3 == 0, ctr)
101
102 // The repair must be the exact statement reorder: declaration first, zero branch retargeted at it.
103 let al: *i64 = sys_mmap(8) as *i64
104 let after: *u8 = sys_read_file(pa, al)
105 gv_check("T12-decl-moved-above-and-zero-branch-retargeted" as *u8,
106 zg_has(after, al[0], "let t: *u8 = sys_mmap(24)\n if m == 0 { t[0] = 48 as u8; k = 1 }" as *u8), ctr)
107 gv_check("T13-repair-did-not-eat-the-opening-brace" as *u8,
108 zg_has(after, al[0], "if m == 0 { t[0]" as *u8), ctr)
109
110 // A repairer that rewrites files it was not asked to touch is worse than one that does nothing.
111 let bl2: *i64 = sys_mmap(8) as *i64
112 let bafter: *u8 = sys_read_file(pb, bl2)
113 var same: i64 = 0
114 if bl2[0] == nb {
115 var j: i64 = 0
116 var eq: i64 = 1
117 while j < nb { if (bbefore[j] & 0xff) != (bafter[j] & 0xff) { eq = 0 } j = j + 1 }
118 same = eq
119 }
120 gv_check("T14-neg-control-safe-file-is-BYTE-identical-after-apply" as *u8, same, ctr)
121
122 return gv_verdict("ZEROPRINT" as *u8, ctr, "a zero that prints as an invisible NUL is found, repaired, and the three safe shapes are left alone" as *u8)
123}