code wiki / _hdl_build / nx_schemadrift_gate.nx
nx_schemadrift_gate.nx source
↩ module page · 153 lines · 8331 B
1// nx_schemadrift_gate.nx -- proves the safety-flag ruler DISCRIMINATES (2026-08-25).
2//
3// The defect under test is a deriver that fails PERMISSIVE: it publishes readOnly=1 for an organ that
4// reaches a write syscall through an imported helper. A gate for that ruler must therefore prove BOTH
5// directions on EVERY axis it claims, because a scanner that answers "writer" to everything passes every
6// permissive test while destroying all the information, and a scanner that answers "read-only" to
7// everything passes every conservative test while destroying all the safety.
8//
9// THE LOAD-BEARING TOOTH IS T6. It runs the ruler at two depths over ONE REAL SUBJECT that ships in this
10// estate -- nx_divprobe, which writes nothing itself and imports nx_gate_verdict.nx, whose gv_journal
11// appends to knowledge/status/harness.jrnl. Depth 0 must say read-only and the transitive closure must
12// say writer. A single-file scanner CANNOT pass it, which is the whole point: an anti-vacuity tooth the
13// trivially wrong implementation fails by construction.
14//
15// T7 is the negative control that stops the opposite cheat. nx_syscalls.nx is imported by essentially
16// every organ in the estate and it DEFINES every write syscall there is; if the ruler counted those
17// definitions the entire estate would read as writers and the derivation would buy nothing. Its two
18// occurrences of the mkdir marker are one COMMENT and one DEFINITION, so the shim alone must measure
19// clean. Get this wrong and T6 still passes -- which is exactly why both are here.
20// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
21import "nx_toolsafety_lib.nx"
22import "nx_gate_verdict.nx"
23import "nx_syscalls.nx"
24
25const GS_FIX: i64 = 2048
26const GS_PATH: i64 = 512
27// The nx_divprobe closure is exactly three files and they are NAMED, not counted from a run: the subject
28// itself, nx_syscalls.nx and nx_gate_verdict.nx (its two imports; nx_gate_verdict re-imports the shim,
29// which must dedup to one visit). Pinned because the first build of this ruler silently visited TWO --
30// a visited-set that compared HASHES ONLY dropped the shim on a collision, and every symptom of that bug
31// pointed toward read-only, i.e. the flattering direction. A count-of-files tooth is the cheapest thing
32// that can see a dropped closure file at all.
33const GS_DIVPROBE_CLOSURE: i64 = 3
34
35func gs_cp(s: *u8, out: *u8) -> i64 {
36 var i: i64 = 0
37 while s[i] != (0 as u8) { out[i] = s[i]; i = i + 1 }
38 out[i] = 0 as u8
39 return i
40}
41
42// strip `src` then ask whether `needle` survives as a CALL. This is the exact composition the deriver
43// uses, so the teeth test the shipping path and not a paraphrase of it.
44func gs_probe(src: *u8, needle: *u8) -> i64 {
45 let raw: *u8 = sys_mmap(GS_FIX)
46 let n: i64 = gs_cp(src, raw)
47 let st: *u8 = sys_mmap(GS_FIX)
48 let sn: i64 = ts_strip(raw, n, st)
49 let r: i64 = ts_has(st, sn, needle)
50 sys_munmap(raw, GS_FIX)
51 sys_munmap(st, GS_FIX)
52 return r
53}
54
55func main() -> i64 {
56 gv_head("nx_schemadrift_gate -- does the import-closure safety ruler discriminate?" as *u8)
57 let ctr: *i64 = gv_ctr()
58
59 // ---- T1/T2: the marker table is DATA and it actually loaded -----------------------------------
60 let loaded: i64 = ts_load_markers()
61 gv_check("marker-table-loads-from-conf" as *u8, loaded, ctr)
62 var allcls: i64 = 1
63 if ts_marker_count(TS_CW) < 1 { allcls = 0 }
64 if ts_marker_count(TS_CD) < 1 { allcls = 0 }
65 if ts_marker_count(TS_CN) < 1 { allcls = 0 }
66 if ts_marker_count(TS_CX) < 1 { allcls = 0 }
67 gv_check("every-marker-class-non-empty-fail-closed" as *u8, allcls, ctr)
68 gv_subjects("write-markers-declared" as *u8, ts_marker_count(TS_CW), ctr)
69
70 // ---- T3: a marker inside a STRING LITERAL is not a reach --------------------------------------
71 let b3: i64 = gs_probe("let fd: i64 = sys_openat_wr(p, m)" as *u8, "sys_openat_wr" as *u8)
72 let g3: i64 = gs_probe("gw(\"sys_openat_wr\" as *u8)" as *u8, "sys_openat_wr" as *u8)
73 gv_bite("string-literal-marker-is-not-a-call" as *u8, b3, g3, ctr)
74
75 // ---- T4: a DEFINITION is not a call ----------------------------------------------------------
76 let b4: i64 = gs_probe("r = sys_unlink(path)" as *u8, "sys_unlink" as *u8)
77 let g4: i64 = gs_probe("func sys_unlink(path: *u8) -> i64 { return 0 }" as *u8, "sys_unlink" as *u8)
78 gv_bite("definition-is-not-a-call" as *u8, b4, g4, ctr)
79
80 // ---- T5: a marker inside a COMMENT is not a reach ---------------------------------------------
81 let b5: i64 = gs_probe("sys_mkdir(d, m)" as *u8, "sys_mkdir" as *u8)
82 let g5: i64 = gs_probe("// sys_mkdir(d, m) is what we would call here" as *u8, "sys_mkdir" as *u8)
83 gv_bite("comment-marker-is-not-a-call" as *u8, b5, g5, ctr)
84
85 // ---- T6: THE ANTI-VACUITY TOOTH, on a real shipping subject -----------------------------------
86 // nx_divprobe writes nothing in its own source and imports nx_gate_verdict.nx, whose gv_journal
87 // appends to a journal. Depth 0 must read clean; the transitive closure must find the writer.
88 // A single-file deriver -- the one this whole lane exists to correct -- cannot pass this.
89 let sp: *u8 = sys_mmap(GS_PATH)
90 let subj: i64 = ts_resolve("nx_divprobe.nx" as *u8, sp)
91 gv_need("subject-nx_divprobe-source-present" as *u8, subj, ctr)
92 var t6bad: i64 = 0
93 var t6good: i64 = 0
94 var walked: i64 = 0
95 var d0files: i64 = 0
96 if subj == 1 {
97 let d0: *i64 = sys_mmap(64) as *i64
98 let dn: *i64 = sys_mmap(64) as *i64
99 ts_reach(sp, 0, d0)
100 ts_reach(sp, TS_DEPTH_ALL, dn)
101 t6good = d0[TS_CW]
102 t6bad = dn[TS_CW]
103 d0files = d0[4]
104 walked = dn[4]
105 }
106 // ASSERT THE FIXTURE REACHED THE CONDITION BEFORE ASSERTING THE OUTCOME: a depth-0 run that visited
107 // more than its one subject, or a transitive run that never descended, would make T6 meaningless
108 // while still printing a verdict.
109 var reached: i64 = 0
110 if d0files == 1 { if walked > 1 { reached = 1 } }
111 gv_check("fixture-reached-the-condition-depth0-is-one-file-and-transitive-descended" as *u8, reached, ctr)
112 gv_bite("closure-finds-a-write-that-a-single-file-scan-cannot" as *u8, t6bad, t6good, ctr)
113 var everyimport: i64 = 0
114 if walked == GS_DIVPROBE_CLOSURE { everyimport = 1 }
115 gv_check("closure-visits-every-import-no-dedup-collision-drops-a-file" as *u8, everyimport, ctr)
116
117 // ---- T7: NEGATIVE CONTROL -- the syscall shim alone is NOT a writer ---------------------------
118 // Every organ imports it and it DEFINES every write syscall. If definitions or comments counted,
119 // this would read as a writer and the whole estate would collapse to the cautious constant the
120 // derivation exists to replace. T6 passes either way, so this control is not redundant with it.
121 let shim: *u8 = sys_mmap(GS_PATH)
122 let sh: i64 = ts_resolve("nx_syscalls.nx" as *u8, shim)
123 gv_need("neg-control-shim-source-present" as *u8, sh, ctr)
124 var shimclean: i64 = 0
125 var shimfiles: i64 = 0
126 if sh == 1 {
127 let sb: *i64 = sys_mmap(64) as *i64
128 ts_reach(shim, TS_DEPTH_ALL, sb)
129 shimfiles = sb[4]
130 if sb[TS_CW] == 0 { shimclean = 1 }
131 }
132 gv_subjects("neg-control-shim-closure-files" as *u8, shimfiles, ctr)
133 gv_check("neg-control-syscall-shim-alone-is-not-a-writer" as *u8, shimclean, ctr)
134
135 // ---- T8: the ruler is not stuck on one answer -------------------------------------------------
136 // Two real subjects, opposite verdicts, from the SAME call. A scanner wired to a constant fails.
137 var discriminates: i64 = 0
138 if t6bad == 1 { if shimclean == 1 { discriminates = 1 } }
139 gv_check("ruler-returns-both-answers-on-real-subjects" as *u8, discriminates, ctr)
140
141 gv_puts("\n diag: divprobe depth0_write=" as *u8); gv_num(t6good)
142 gv_puts(" transitive_write=" as *u8); gv_num(t6bad)
143 gv_puts(" depth0_files=" as *u8); gv_num(d0files)
144 gv_puts(" transitive_files=" as *u8); gv_num(walked)
145 gv_puts(" shim_files=" as *u8); gv_num(shimfiles)
146 gv_puts(" shim_write=" as *u8)
147 if shimclean == 1 { gv_puts("0" as *u8) } else { gv_puts("1" as *u8) }
148 gv_puts("\n" as *u8)
149
150 let rc: i64 = gv_verdict("SCHEMADRIFT-GATE" as *u8, ctr, "import-closure safety ruler" as *u8)
151 sys_exit(rc)
152 return rc
153}