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}