nx_bck_iv_gate.nx source
↩ module page · 261 lines · 16598 B
1// nx_bck_iv_gate.nx -- THE ELISION PROOF GATE for LN7b (bck_elide_induction) and for the compiler's
2// data-driven MODES (--mode=<name>, knowledge/lang_modes.conf). Sibling of nx_bck_elide_gate and
3// built from the same parts (nx_ccbuild_lib, gv_*): sources assembled at RUNTIME under /tmp, compiled
4// two ways by the compiler named in argv[1] (there is NO default compiler -- a gate that forks whatever
5// is installed reports on a binary nobody chose), the emitted ASSEMBLY as the oracle for "fired" /
6// "did not fire", and out-of-bounds witnesses whose only remaining protection is the check the pass
7// was asked to keep.
8//
9// WHAT MUST FIRE: the receipt loop's own shape -- a counter initialised to a constant, incremented by a
10// constant inside a `while k < N` whose N is the array's length, indexing that array. WHAT MUST NOT:
11// F2 the guard is WIDER than the array (`while k < 2048` over [1024]i64) -- and it traps 71 under
12// both builds, so the refusal is measured on a program that really does go out of range;
13// F3 the counter is incremented by a value that is not a constant -- its range is unknowable here;
14// F4 a constant reset (`k = 4000`) sits on the path between the guard and the access -- the guard's
15// fact is dead by the time the access runs, and the program traps 71 under both builds;
16// F5 the counter's address ESCAPES (`let p: *i64 = &k`) -- a store through p is invisible to the
17// pass, and the program traps 71 under both builds.
18// gv_bite ties the two halves: the detector must change F1 and leave F2 byte-identical.
19// MODES: `--mode=f1` must produce assembly byte-identical to `--bckelide` (the bundle is exactly its
20// flags, no more), and `--mode=nonesuch` must REFUSE the build (a silent default is a mode wearing
21// the wrong name).
22// Products land in _build/ because NAS /tmp is mounted noexec (the sibling gate's measured lesson).
23// license_tier: ORIGINAL No hw writes (Rule 26).
24import "nx_gate_verdict.nx"
25import "nx_ccbuild_lib.nx"
26
27const IVG_TRAP_BOUNDS: i64 = 71
28const IVG_F1_EXIT: i64 = 88 // sum_{i<1024}(3i+1) = 1572352; 1572352 mod 251 = 88, a closed form the fixture returns
29const IVG_MODE_644: i64 = 420
30const IVG_MODE_755: i64 = 493
31const IVG_WAIT_SIGMASK: i64 = 128
32const IVG_WAIT_CODESHIFT: i64 = 256
33const IVG_SCRATCH: i64 = 64
34const IVG_N_SOURCES: i64 = 5
35
36func ivg_resolve_cc(argc: i64, argv: *i64, out: *i64) -> i64 {
37 out[0] = 0
38 if argc < 2 { return 0 }
39 let p: *u8 = argv[1] as *u8
40 if p[0] == (0 as u8) { return 0 }
41 out[0] = p as i64
42 return 1
43}
44func ivg_exit_code(st: i64) -> i64 {
45 if (st % IVG_WAIT_SIGMASK) != 0 { return 0 - 1 }
46 return (st / IVG_WAIT_CODESHIFT) % 256
47}
48func ivg_write_src(path: *u8, body: *u8) -> i64 {
49 let fd: i64 = sys_openat_wr(path, IVG_MODE_644)
50 if fd < 0 { return 0 }
51 var n: i64 = 0
52 while body[n] != (0 as u8) { n = n + 1 }
53 let w: i64 = sys_write(fd, body, n)
54 sys_close(fd)
55 if w != n { return 0 }
56 return 1
57}
58func ivg_run0(elf: *u8, out_path: *u8, envp: *i64, errfd: i64) -> i64 {
59 let ofd: i64 = sys_openat_wr(out_path, IVG_MODE_644)
60 let a: *i64 = sys_mmap(IVG_SCRATCH) as *i64
61 a[0] = elf as i64
62 a[1] = 0
63 let st: i64 = cb_run(elf, a, envp, ofd, errfd)
64 sys_close(ofd)
65 return st
66}
67// How many bounds-check TRAP SITES an assembly file carries: every emitted check ends in
68// `movabsq $71, %rdi` before exit_group, one per site, so the count is the number of checks that
69// survived -- the ruler that lets a fixture with TWO loops say WHICH loop kept its check.
70func ivg_count_trap(path: *u8) -> i64 {
71 let ln: *i64 = sys_mmap(16) as *i64
72 let b: *u8 = sys_read_file(path, ln)
73 if (b as i64) == 0 { return 0 - 1 }
74 let n: i64 = ln[0]
75 let pat: *u8 = "movabsq $71, %rdi" as *u8
76 var pl: i64 = 0
77 while pat[pl] != (0 as u8) { pl = pl + 1 }
78 var cnt: i64 = 0
79 var i: i64 = 0
80 while i + pl <= n {
81 var j: i64 = 0
82 while j < pl { if b[i + j] != pat[j] { break } j = j + 1 }
83 if j == pl { cnt = cnt + 1; i = i + pl } else { i = i + 1 }
84 }
85 return cnt
86}
87func ivg_kv(label: *u8, v: i64) -> i64 {
88 gv_puts(" " as *u8); gv_puts(label); gv_puts("=" as *u8); gv_num(v); gv_puts("\n" as *u8)
89 return 0
90}
91
92func main(argc: i64, argv: *i64) -> i64 {
93 let ctr: *i64 = gv_ctr()
94 gv_head("nx_bck_iv_gate -- LN7b: a loop guard proves the single check inside its loop, and every shape the proof does not cover keeps its check and still traps" as *u8)
95
96 let ccbuf: *i64 = sys_mmap(IVG_SCRATCH) as *i64
97 let neg_absent: i64 = ivg_resolve_cc(1, argv, ccbuf)
98 let pos_present: i64 = ivg_resolve_cc(argc, argv, ccbuf)
99 gv_bite("neg-control-refuses-a-silent-default-compiler-and-accepts-an-explicit-one" as *u8, 1 - neg_absent, 1 - pos_present, ctr)
100 if gv_need("compiler-under-test named in argv[1]" as *u8, pos_present, ctr) == 0 {
101 gv_puts(" usage: nx_bck_iv_gate <path-to-compiler-elf>\n" as *u8)
102 sys_exit(gv_verdict("BCK-IV-GATE" as *u8, ctr, "no compiler named" as *u8))
103 }
104 let cc: *u8 = ccbuf[0] as *u8
105 let anchored: i64 = cb_anchor_root()
106 if gv_need("buildroot tree reachable from the working directory" as *u8, anchored, ctr) == 0 {
107 sys_exit(gv_verdict("BCK-IV-GATE" as *u8, ctr, "tree not found" as *u8))
108 }
109 let dir: *u8 = "/tmp/nx_bck_iv_gate\x00"
110 sys_mkdir(dir, IVG_MODE_755)
111
112 // ---- fixtures, assembled at runtime ----
113 let src1: *u8 = "/tmp/nx_bck_iv_gate/f1_loop.nx\x00"
114 let body1: *u8 = "func main() -> i64 {\n var a: [1024]i64\n var i: i64 = 0\n while i < 1024 { a[i] = i * 3 + 1; i = i + 1 }\n var acc: i64 = 0\n var k: i64 = 0\n while k < 1024 { acc = acc + a[k]; k = k + 1 }\n return acc % 251\n}\n"
115 let src2: *u8 = "/tmp/nx_bck_iv_gate/f2_wideguard.nx\x00"
116 let body2: *u8 = "func main() -> i64 {\n var a: [1024]i64\n var acc: i64 = 0\n var k: i64 = 0\n while k < 2048 { acc = acc + a[k]; k = k + 1 }\n return acc % 251\n}\n"
117 let src3: *u8 = "/tmp/nx_bck_iv_gate/f3_varstep.nx\x00"
118 let body3: *u8 = "func main() -> i64 {\n var a: [1024]i64\n var acc: i64 = 0\n var step: i64 = 1\n var k: i64 = 0\n while k < 1024 { acc = acc + a[k]; k = k + step; step = step + 1 }\n return acc % 251\n}\n"
119 let src4: *u8 = "/tmp/nx_bck_iv_gate/f4_resetonpath.nx\x00"
120 let body4: *u8 = "func main() -> i64 {\n var a: [1024]i64\n var i: i64 = 0\n while i < 1024 { a[i] = i * 3 + 1; i = i + 1 }\n var acc: i64 = 0\n var k: i64 = 0\n while k < 1024 {\n if acc > 500000 { k = 4000 }\n acc = acc + a[k]\n k = k + 1\n }\n return acc % 251\n}\n"
121 let src5: *u8 = "/tmp/nx_bck_iv_gate/f5_escape.nx\x00"
122 let body5: *u8 = "func main() -> i64 {\n var a: [1024]i64\n var i: i64 = 0\n while i < 1024 { a[i] = i * 3 + 1; i = i + 1 }\n var acc: i64 = 0\n var k: i64 = 0\n let p: *i64 = &k\n while k < 1024 {\n if acc > 500000 { *p = 4000 }\n acc = acc + a[k]\n *p = *p + 1\n }\n return acc % 251\n}\n"
123 var nsrc: i64 = 0
124 if ivg_write_src(src1, body1) == 1 { nsrc = nsrc + 1 }
125 if ivg_write_src(src2, body2) == 1 { nsrc = nsrc + 1 }
126 if ivg_write_src(src3, body3) == 1 { nsrc = nsrc + 1 }
127 if ivg_write_src(src4, body4) == 1 { nsrc = nsrc + 1 }
128 if ivg_write_src(src5, body5) == 1 { nsrc = nsrc + 1 }
129 if gv_subjects("fixture sources written" as *u8, nsrc, ctr) == 0 {
130 sys_exit(gv_verdict("BCK-IV-GATE" as *u8, ctr, "no fixtures" as *u8))
131 }
132 gv_check("all-five-fixtures-written" as *u8, (nsrc == IVG_N_SOURCES) as i64, ctr)
133
134 let envp: *i64 = sys_mmap(IVG_SCRATCH) as *i64
135 envp[0] = 0
136 let cclog: i64 = sys_openat_wr("/tmp/nx_bck_iv_gate/cc.log\x00" as *u8, IVG_MODE_644)
137 let asmlog: *u8 = "/tmp/nx_bck_iv_gate/asm.log\x00"
138 let asmtmp: *u8 = "_build/ivg_asm.tmp\x00"
139 let flag: *u8 = "--bckelide\x00"
140 let s1p: *u8 = "/tmp/nx_bck_iv_gate/f1_plain.s\x00"
141 let s1f: *u8 = "/tmp/nx_bck_iv_gate/f1_flag.s\x00"
142 let s2p: *u8 = "/tmp/nx_bck_iv_gate/f2_plain.s\x00"
143 let s2f: *u8 = "/tmp/nx_bck_iv_gate/f2_flag.s\x00"
144 let s3p: *u8 = "/tmp/nx_bck_iv_gate/f3_plain.s\x00"
145 let s3f: *u8 = "/tmp/nx_bck_iv_gate/f3_flag.s\x00"
146 let s4p: *u8 = "/tmp/nx_bck_iv_gate/f4_plain.s\x00"
147 let s4f: *u8 = "/tmp/nx_bck_iv_gate/f4_flag.s\x00"
148 let s5p: *u8 = "/tmp/nx_bck_iv_gate/f5_plain.s\x00"
149 let s5f: *u8 = "/tmp/nx_bck_iv_gate/f5_flag.s\x00"
150 let e1p: *u8 = "_build/ivg_f1_plain.elf\x00"
151 let e1f: *u8 = "_build/ivg_f1_flag.elf\x00"
152 let e2p: *u8 = "_build/ivg_f2_plain.elf\x00"
153 let e2f: *u8 = "_build/ivg_f2_flag.elf\x00"
154 let e3p: *u8 = "_build/ivg_f3_plain.elf\x00"
155 let e3f: *u8 = "_build/ivg_f3_flag.elf\x00"
156 let e4p: *u8 = "_build/ivg_f4_plain.elf\x00"
157 let e4f: *u8 = "_build/ivg_f4_flag.elf\x00"
158 let e5p: *u8 = "_build/ivg_f5_plain.elf\x00"
159 let e5f: *u8 = "_build/ivg_f5_flag.elf\x00"
160
161 let r1p: i64 = cb_build_flag(cc, src1, s1p, e1p, envp, cclog, asmtmp, asmlog, 0 as *u8)
162 let r1f: i64 = cb_build_flag(cc, src1, s1f, e1f, envp, cclog, asmtmp, asmlog, flag)
163 let r2p: i64 = cb_build_flag(cc, src2, s2p, e2p, envp, cclog, asmtmp, asmlog, 0 as *u8)
164 let r2f: i64 = cb_build_flag(cc, src2, s2f, e2f, envp, cclog, asmtmp, asmlog, flag)
165 let r3p: i64 = cb_build_flag(cc, src3, s3p, e3p, envp, cclog, asmtmp, asmlog, 0 as *u8)
166 let r3f: i64 = cb_build_flag(cc, src3, s3f, e3f, envp, cclog, asmtmp, asmlog, flag)
167 let r4p: i64 = cb_build_flag(cc, src4, s4p, e4p, envp, cclog, asmtmp, asmlog, 0 as *u8)
168 let r4f: i64 = cb_build_flag(cc, src4, s4f, e4f, envp, cclog, asmtmp, asmlog, flag)
169 let r5p: i64 = cb_build_flag(cc, src5, s5p, e5p, envp, cclog, asmtmp, asmlog, 0 as *u8)
170 let r5f: i64 = cb_build_flag(cc, src5, s5f, e5f, envp, cclog, asmtmp, asmlog, flag)
171 ivg_kv("build_rc_f1_plain" as *u8, r1p); ivg_kv("build_rc_f1_flag" as *u8, r1f)
172 ivg_kv("build_rc_f2_plain" as *u8, r2p); ivg_kv("build_rc_f2_flag" as *u8, r2f)
173 ivg_kv("build_rc_f3_plain" as *u8, r3p); ivg_kv("build_rc_f3_flag" as *u8, r3f)
174 ivg_kv("build_rc_f4_plain" as *u8, r4p); ivg_kv("build_rc_f4_flag" as *u8, r4f)
175 ivg_kv("build_rc_f5_plain" as *u8, r5p); ivg_kv("build_rc_f5_flag" as *u8, r5f)
176 var builds_ok: i64 = 0
177 if r1p == 0 { if r1f == 0 { if r2p == 0 { if r2f == 0 { if r3p == 0 { if r3f == 0 { if r4p == 0 { if r4f == 0 { if r5p == 0 { if r5f == 0 { builds_ok = 1 } } } } } } } } } }
178 if gv_need("all ten fixture builds succeeded under the compiler named in argv[1]" as *u8, builds_ok, ctr) == 0 {
179 gv_puts(" the named compiler did not build every fixture -- diagnostics in /tmp/nx_bck_iv_gate/cc.log; NOTHING below was run\n" as *u8)
180 sys_close(cclog)
181 sys_exit(gv_verdict("BCK-IV-GATE" as *u8, ctr, "fixtures unbuildable" as *u8))
182 }
183 let out_tmp: *u8 = "/tmp/nx_bck_iv_gate/run.out\x00"
184
185 // ---- F1: the receipt loop's shape MUST be elided, and the elided program computes the closed form ----
186 let same1: i64 = cb_files_equal(s1p, s1f)
187 let sz1p: i64 = cb_fsize(s1p)
188 let sz1f: i64 = cb_fsize(s1f)
189 ivg_kv("f1_asm_bytes_plain" as *u8, sz1p); ivg_kv("f1_asm_bytes_flag" as *u8, sz1f)
190 gv_check("F1-loop-guarded-check-IS-elided-assembly-changes-under-the-flag" as *u8, (same1 == 0) as i64, ctr)
191 var shrank: i64 = 0
192 if sz1f > 0 { if sz1f < sz1p { shrank = 1 } }
193 let t1p: i64 = ivg_count_trap(s1p)
194 let t1f: i64 = ivg_count_trap(s1f)
195 ivg_kv("f1_trap_sites_plain" as *u8, t1p); ivg_kv("f1_trap_sites_flag" as *u8, t1f)
196 // the appended crash guard carries its own (unelided) sites on both sides, so the ruler is the DELTA
197 gv_check("F1-both-loop-checks-are-elided-the-flag-removes-exactly-2-trap-sites" as *u8, ((t1p - t1f) == 2) as i64, ctr)
198 gv_check("F1-the-elision-removes-work-the-assembly-is-strictly-smaller" as *u8, shrank, ctr)
199 let c1f: i64 = ivg_exit_code(ivg_run0(e1f, out_tmp, envp, cclog))
200 let c1p: i64 = ivg_exit_code(ivg_run0(e1p, out_tmp, envp, cclog))
201 ivg_kv("f1_exit_flag" as *u8, c1f); ivg_kv("f1_exit_plain" as *u8, c1p)
202 gv_check("F1-elided-program-computes-the-closed-form-88-under-the-flag" as *u8, (c1f == IVG_F1_EXIT) as i64, ctr)
203 gv_check("F1-same-program-computes-88-without-the-flag" as *u8, (c1p == IVG_F1_EXIT) as i64, ctr)
204
205 // ---- F2: guard wider than the array -- refused, and the check it kept traps ----
206 let same2: i64 = cb_files_equal(s2p, s2f)
207 gv_check("F2-REFUSAL-a-guard-wider-than-the-array-is-KEPT-assembly-byte-identical" as *u8, same2, ctr)
208 let c2f: i64 = ivg_exit_code(ivg_run0(e2f, out_tmp, envp, cclog))
209 let c2p: i64 = ivg_exit_code(ivg_run0(e2p, out_tmp, envp, cclog))
210 ivg_kv("f2_exit_flag" as *u8, c2f); ivg_kv("f2_exit_plain" as *u8, c2p)
211 gv_check("F2-out-of-range-index-still-traps-71-under-the-flag" as *u8, (c2f == IVG_TRAP_BOUNDS) as i64, ctr)
212 gv_check("F2-fixture-reached-the-condition-it-traps-71-without-the-flag-too" as *u8, (c2p == IVG_TRAP_BOUNDS) as i64, ctr)
213 gv_bite("bite-fires-on-the-guarded-loop-and-stays-silent-on-the-wide-guard" as *u8, 1 - same1, 1 - same2, ctr)
214
215 // ---- F3: non-constant increment -- refused ----
216 let same3: i64 = cb_files_equal(s3p, s3f)
217 gv_check("F3-REFUSAL-a-counter-incremented-by-a-non-constant-is-KEPT-assembly-byte-identical" as *u8, same3, ctr)
218
219 // ---- F4: a reset on the path between guard and access -- refused, and it traps ----
220 let t4p: i64 = ivg_count_trap(s4p)
221 let t4f: i64 = ivg_count_trap(s4f)
222 ivg_kv("f4_trap_sites_plain" as *u8, t4p); ivg_kv("f4_trap_sites_flag" as *u8, t4f)
223 // the fixture carries TWO loops on purpose: the fill loop is a sound elision and MUST go, the reset loop
224 // MUST stay -- a whole-file byte compare could not tell those apart (it read "assembly changed" as
225 // "the reset was elided", which is the wrong subject)
226 gv_check("F4-REFUSAL-the-reset-loop-KEEPS-its-check-while-only-the-fill-loop-loses-its-exactly-1-site-removed" as *u8, ((t4p - t4f) == 1) as i64, ctr)
227 let c4f: i64 = ivg_exit_code(ivg_run0(e4f, out_tmp, envp, cclog))
228 let c4p: i64 = ivg_exit_code(ivg_run0(e4p, out_tmp, envp, cclog))
229 ivg_kv("f4_exit_flag" as *u8, c4f); ivg_kv("f4_exit_plain" as *u8, c4p)
230 gv_check("F4-the-reset-index-still-traps-71-under-the-flag" as *u8, (c4f == IVG_TRAP_BOUNDS) as i64, ctr)
231 gv_check("F4-fixture-reached-the-condition-it-traps-71-without-the-flag-too" as *u8, (c4p == IVG_TRAP_BOUNDS) as i64, ctr)
232
233 // ---- F5: the counter escapes through a pointer -- refused, and it traps ----
234 let t5p: i64 = ivg_count_trap(s5p)
235 let t5f: i64 = ivg_count_trap(s5f)
236 ivg_kv("f5_trap_sites_plain" as *u8, t5p); ivg_kv("f5_trap_sites_flag" as *u8, t5f)
237 gv_check("F5-REFUSAL-the-escaped-counter-loop-KEEPS-its-check-exactly-1-site-removed" as *u8, ((t5p - t5f) == 1) as i64, ctr)
238 let c5f: i64 = ivg_exit_code(ivg_run0(e5f, out_tmp, envp, cclog))
239 let c5p: i64 = ivg_exit_code(ivg_run0(e5p, out_tmp, envp, cclog))
240 ivg_kv("f5_exit_flag" as *u8, c5f); ivg_kv("f5_exit_plain" as *u8, c5p)
241 gv_check("F5-the-pointer-written-index-still-traps-71-under-the-flag" as *u8, (c5f == IVG_TRAP_BOUNDS) as i64, ctr)
242 gv_check("F5-fixture-reached-the-condition-it-traps-71-without-the-flag-too" as *u8, (c5p == IVG_TRAP_BOUNDS) as i64, ctr)
243
244 // ---- MODES: --mode=f1 is exactly its bundle, and an undeclared mode refuses ----
245 let s1m: *u8 = "/tmp/nx_bck_iv_gate/f1_modef1.s\x00"
246 let e1m: *u8 = "_build/ivg_f1_modef1.elf\x00"
247 let r1m: i64 = cb_build_flag(cc, src1, s1m, e1m, envp, cclog, asmtmp, asmlog, "--mode=f1\x00" as *u8)
248 ivg_kv("build_rc_f1_mode_f1" as *u8, r1m)
249 var mode_same: i64 = 0
250 if r1m == 0 { mode_same = cb_files_equal(s1f, s1m) }
251 gv_check("MODE-f1-expands-to-exactly-its-declared-bundle-assembly-byte-identical-to---bckelide" as *u8, mode_same, ctr)
252 let s1x: *u8 = "/tmp/nx_bck_iv_gate/f1_modebad.s\x00"
253 let e1x: *u8 = "_build/ivg_f1_modebad.elf\x00"
254 let r1x: i64 = cb_build_flag(cc, src1, s1x, e1x, envp, cclog, asmtmp, asmlog, "--mode=nonesuch\x00" as *u8)
255 ivg_kv("build_rc_f1_mode_nonesuch" as *u8, r1x)
256 gv_bite("neg-control-an-undeclared-mode-REFUSES-the-build-and-a-declared-one-builds" as *u8, (r1x != 0) as i64, (r1m != 0) as i64, ctr)
257
258 sys_close(cclog)
259 sys_exit(gv_verdict("BCK-IV-GATE" as *u8, ctr, "the loop guard proves the loop's check, every uncovered shape keeps it and traps, and a mode is exactly its bundle" as *u8))
260 return 0
261}