nx_chkarith_jo_gate.nx source
↩ module page · 215 lines · 13368 B
1// nx_chkarith_jo_gate.nx -- THE PROOF GATE for LN18 (x86ctx_ovf_fuse): checked integer arithmetic at
2// add+jo cost. Sibling of nx_bck_iv_gate, built from the same parts (nx_ccbuild_lib, gv_*): sources
3// assembled at RUNTIME under /tmp, compiled by the compiler named in argv[1] (there is NO default
4// compiler), the emitted ASSEMBLY as the oracle for "the long form is gone", and overflow WITNESSES
5// whose only protection is the trap the fuse was asked to keep.
6//
7// WHAT THE FUSE MUST DO (measured on the /compare/lang receipt 2026-09-01: the daily mode cost 2.4x the
8// default build because every checked add was six instructions with spills): under --chkarith the LN1
9// shape r = a + b; x1 = a ^ r; x2 = b ^ r; a1 = x1 & x2; c = a1 < 0; br_cond c becomes `addq` + `jo`.
10// F1 a checked accumulate loop (sum 1..1000 = 500500, mod 251 = 6): the --chkarith assembly carries
11// jo/jno branches, the plain assembly carries none, and the checked build adds NO xorq to the plain
12// one (every checked add and sub site fused -- a single surviving long form would show as +2 xorq);
13// exit 6 under plain, --chkarith AND --mode=daily (the fuse composes with the full daily bundle).
14// F2 an add that overflows i64 at run time (MAX + argc): traps 72 under --chkarith, wraps to 91 plain.
15// F3 a sub that overflows (MIN - argc): traps 72 under --chkarith, wraps to 159 plain.
16// F4 __wrap_add(MAX, argc): the declared wrap-around intent stays exempt, exit 91 under --chkarith.
17// gv_bite ties the halves: the trap fires on F2 and stays silent on F1 under the same flag.
18// The overflow fixtures take their second operand from argc so no constant folds (the parser REFUSES a
19// constant overflow at parse time, which would test the wrong rung).
20// Products land in _build/ because NAS /tmp is mounted noexec (the sibling gate's measured lesson).
21// license_tier: ORIGINAL No hw writes (Rule 26).
22import "nx_gate_verdict.nx"
23import "nx_ccbuild_lib.nx"
24
25const CJG_TRAP_OVERFLOW: i64 = 72
26const CJG_F1_EXIT: i64 = 6 // 500500 mod 251
27const CJG_WRAP_ADD_EXIT: i64 = 91 // (-2^63 mod 251 + 251) mod 251, the wrapped MAX+1 reduced
28const CJG_WRAP_SUB_EXIT: i64 = 159 // (2^63-1) mod 251, the wrapped MIN-1 reduced
29const CJG_MODE_644: i64 = 420
30const CJG_MODE_755: i64 = 493
31const CJG_WAIT_SIGMASK: i64 = 128
32const CJG_WAIT_CODESHIFT: i64 = 256
33const CJG_SCRATCH: i64 = 64
34const CJG_N_SOURCES: i64 = 4
35const CJG_MIN_FUSED: i64 = 2 // the F1 loop has two checked adds (the accumulate and the counter)
36
37func cjg_resolve_cc(argc: i64, argv: *i64, out: *i64) -> i64 {
38 out[0] = 0
39 if argc < 2 { return 0 }
40 let p: *u8 = argv[1] as *u8
41 if p[0] == (0 as u8) { return 0 }
42 out[0] = p as i64
43 return 1
44}
45func cjg_exit_code(st: i64) -> i64 {
46 if (st % CJG_WAIT_SIGMASK) != 0 { return 0 - 1 }
47 return (st / CJG_WAIT_CODESHIFT) % 256
48}
49func cjg_write_src(path: *u8, body: *u8) -> i64 {
50 let fd: i64 = sys_openat_wr(path, CJG_MODE_644)
51 if fd < 0 { return 0 }
52 var n: i64 = 0
53 while body[n] != (0 as u8) { n = n + 1 }
54 let w: i64 = sys_write(fd, body, n)
55 sys_close(fd)
56 if w != n { return 0 }
57 return 1
58}
59func cjg_run0(elf: *u8, out_path: *u8, envp: *i64, errfd: i64) -> i64 {
60 let ofd: i64 = sys_openat_wr(out_path, CJG_MODE_644)
61 let a: *i64 = sys_mmap(CJG_SCRATCH) as *i64
62 a[0] = elf as i64
63 a[1] = 0
64 let st: i64 = cb_run(elf, a, envp, ofd, errfd)
65 sys_close(ofd)
66 return st
67}
68// Occurrences of a pattern in a file -- the assembly ruler. -1 when the file cannot be read, so an
69// unreadable product never reads as "zero long forms".
70func cjg_count(path: *u8, pat: *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 var pl: i64 = 0
76 while pat[pl] != (0 as u8) { pl = pl + 1 }
77 var cnt: i64 = 0
78 var i: i64 = 0
79 while i + pl <= n {
80 var j: i64 = 0
81 while j < pl { if b[i + j] != pat[j] { break } j = j + 1 }
82 if j == pl { cnt = cnt + 1; i = i + pl } else { i = i + 1 }
83 }
84 return cnt
85}
86func cjg_kv(label: *u8, v: i64) -> i64 {
87 gv_puts(" " as *u8); gv_puts(label); gv_puts("=" as *u8); gv_num(v); gv_puts("\n" as *u8)
88 return 0
89}
90
91func main(argc: i64, argv: *i64) -> i64 {
92 let ctr: *i64 = gv_ctr()
93 gv_puts("nx_chkarith_jo_gate -- LN18: a checked add or sub is `add` then `jo` on the live flags, and every overflow still traps 72\n\n" as *u8)
94 let ccbuf: *i64 = sys_mmap(CJG_SCRATCH) as *i64
95 let neg_absent: i64 = cjg_resolve_cc(1, argv, ccbuf)
96 let pos_present: i64 = cjg_resolve_cc(argc, argv, ccbuf)
97 gv_bite("neg-control-refuses-a-silent-default-compiler-and-accepts-an-explicit-one" as *u8, 1 - neg_absent, 1 - pos_present, ctr)
98 if gv_need("compiler-under-test named in argv[1]" as *u8, pos_present, ctr) == 0 {
99 gv_puts(" usage: nx_chkarith_jo_gate <path-to-compiler-elf>\n" as *u8)
100 sys_exit(gv_verdict("CHKARITH-JO-GATE" as *u8, ctr, "no compiler named" as *u8))
101 }
102 let cc: *u8 = ccbuf[0] as *u8
103 let anchored: i64 = cb_anchor_root()
104 if gv_need("buildroot tree reachable from the working directory" as *u8, anchored, ctr) == 0 {
105 sys_exit(gv_verdict("CHKARITH-JO-GATE" as *u8, ctr, "tree not found" as *u8))
106 }
107 let dir: *u8 = "/tmp/nx_chkarith_jo_gate\x00"
108 sys_mkdir(dir, CJG_MODE_755)
109
110 let src1: *u8 = "/tmp/nx_chkarith_jo_gate/f1_loop.nx\x00"
111 let body1: *u8 = "func main() -> i64 {\n var acc: i64 = 0\n var k: i64 = 1\n while k <= 1000 { acc = acc + k; k = k + 1 }\n return acc % 251\n}\n"
112 let src2: *u8 = "/tmp/nx_chkarith_jo_gate/f2_addovf.nx\x00"
113 let body2: *u8 = "func main(argc: i64, argv: *i64) -> i64 {\n var x: i64 = 9223372036854775807\n var y: i64 = argc\n x = x + y\n return ((x % 251) + 251) % 251\n}\n"
114 let src3: *u8 = "/tmp/nx_chkarith_jo_gate/f3_subovf.nx\x00"
115 let body3: *u8 = "func main(argc: i64, argv: *i64) -> i64 {\n var m: i64 = 0 - 9223372036854775807\n var y: i64 = argc\n m = m - y\n m = m - y\n return ((m % 251) + 251) % 251\n}\n"
116 let src4: *u8 = "/tmp/nx_chkarith_jo_gate/f4_wrap.nx\x00"
117 let body4: *u8 = "func main(argc: i64, argv: *i64) -> i64 {\n var x: i64 = 9223372036854775807\n var y: i64 = argc\n x = __wrap_add(x, y)\n return ((x % 251) + 251) % 251\n}\n"
118 var nsrc: i64 = 0
119 if cjg_write_src(src1, body1) == 1 { nsrc = nsrc + 1 }
120 if cjg_write_src(src2, body2) == 1 { nsrc = nsrc + 1 }
121 if cjg_write_src(src3, body3) == 1 { nsrc = nsrc + 1 }
122 if cjg_write_src(src4, body4) == 1 { nsrc = nsrc + 1 }
123 if gv_subjects("fixture sources written" as *u8, nsrc, ctr) == 0 {
124 sys_exit(gv_verdict("CHKARITH-JO-GATE" as *u8, ctr, "no fixtures" as *u8))
125 }
126 gv_check("all-four-fixtures-written" as *u8, (nsrc == CJG_N_SOURCES) as i64, ctr)
127
128 let envp: *i64 = sys_mmap(CJG_SCRATCH) as *i64
129 envp[0] = 0
130 let cclog: i64 = sys_openat_wr("/tmp/nx_chkarith_jo_gate/cc.log\x00" as *u8, CJG_MODE_644)
131 let asmlog: *u8 = "/tmp/nx_chkarith_jo_gate/asm.log\x00"
132 let asmtmp: *u8 = "_build/cjg_asm.tmp\x00"
133 let flag: *u8 = "--chkarith\x00"
134 let s1p: *u8 = "/tmp/nx_chkarith_jo_gate/f1_plain.s\x00"
135 let s1c: *u8 = "/tmp/nx_chkarith_jo_gate/f1_chk.s\x00"
136 let s1d: *u8 = "/tmp/nx_chkarith_jo_gate/f1_daily.s\x00"
137 let s2p: *u8 = "/tmp/nx_chkarith_jo_gate/f2_plain.s\x00"
138 let s2c: *u8 = "/tmp/nx_chkarith_jo_gate/f2_chk.s\x00"
139 let s3p: *u8 = "/tmp/nx_chkarith_jo_gate/f3_plain.s\x00"
140 let s3c: *u8 = "/tmp/nx_chkarith_jo_gate/f3_chk.s\x00"
141 let s4c: *u8 = "/tmp/nx_chkarith_jo_gate/f4_chk.s\x00"
142 let e1p: *u8 = "_build/cjg_f1_plain.elf\x00"
143 let e1c: *u8 = "_build/cjg_f1_chk.elf\x00"
144 let e1d: *u8 = "_build/cjg_f1_daily.elf\x00"
145 let e2p: *u8 = "_build/cjg_f2_plain.elf\x00"
146 let e2c: *u8 = "_build/cjg_f2_chk.elf\x00"
147 let e3p: *u8 = "_build/cjg_f3_plain.elf\x00"
148 let e3c: *u8 = "_build/cjg_f3_chk.elf\x00"
149 let e4c: *u8 = "_build/cjg_f4_chk.elf\x00"
150 let r1p: i64 = cb_build_flag(cc, src1, s1p, e1p, envp, cclog, asmtmp, asmlog, 0 as *u8)
151 let r1c: i64 = cb_build_flag(cc, src1, s1c, e1c, envp, cclog, asmtmp, asmlog, flag)
152 let r1d: i64 = cb_build_flag(cc, src1, s1d, e1d, envp, cclog, asmtmp, asmlog, "--mode=daily\x00" as *u8)
153 let r2p: i64 = cb_build_flag(cc, src2, s2p, e2p, envp, cclog, asmtmp, asmlog, 0 as *u8)
154 let r2c: i64 = cb_build_flag(cc, src2, s2c, e2c, envp, cclog, asmtmp, asmlog, flag)
155 let r3p: i64 = cb_build_flag(cc, src3, s3p, e3p, envp, cclog, asmtmp, asmlog, 0 as *u8)
156 let r3c: i64 = cb_build_flag(cc, src3, s3c, e3c, envp, cclog, asmtmp, asmlog, flag)
157 let r4c: i64 = cb_build_flag(cc, src4, s4c, e4c, envp, cclog, asmtmp, asmlog, flag)
158 cjg_kv("build_rc_f1_plain" as *u8, r1p); cjg_kv("build_rc_f1_chk" as *u8, r1c); cjg_kv("build_rc_f1_daily" as *u8, r1d)
159 cjg_kv("build_rc_f2_plain" as *u8, r2p); cjg_kv("build_rc_f2_chk" as *u8, r2c)
160 cjg_kv("build_rc_f3_plain" as *u8, r3p); cjg_kv("build_rc_f3_chk" as *u8, r3c)
161 cjg_kv("build_rc_f4_chk" as *u8, r4c)
162 var builds_ok: i64 = 0
163 if r1p == 0 { if r1c == 0 { if r1d == 0 { if r2p == 0 { if r2c == 0 { if r3p == 0 { if r3c == 0 { if r4c == 0 { builds_ok = 1 } } } } } } } }
164 if gv_need("all eight fixture builds succeeded under the compiler named in argv[1] (the assembler must know jo/jno)" as *u8, builds_ok, ctr) == 0 {
165 gv_puts(" the named compiler did not build every fixture -- diagnostics in /tmp/nx_chkarith_jo_gate/cc.log and asm.log; NOTHING below was run\n" as *u8)
166 sys_close(cclog)
167 sys_exit(gv_verdict("CHKARITH-JO-GATE" as *u8, ctr, "builds failed" as *u8))
168 }
169 let out_tmp: *u8 = "/tmp/nx_chkarith_jo_gate/run.out\x00"
170
171 // ---- F1: the assembly says the long form is gone and the fused branch is there ----
172 let jo_p: i64 = cjg_count(s1p, " jo ." as *u8) + cjg_count(s1p, " jno ." as *u8)
173 let jo_c: i64 = cjg_count(s1c, " jo ." as *u8) + cjg_count(s1c, " jno ." as *u8)
174 let xor_p: i64 = cjg_count(s1p, "xorq" as *u8)
175 let xor_c: i64 = cjg_count(s1c, "xorq" as *u8)
176 cjg_kv("f1_jo_plain" as *u8, jo_p); cjg_kv("f1_jo_chk" as *u8, jo_c)
177 cjg_kv("f1_xorq_plain" as *u8, xor_p); cjg_kv("f1_xorq_chk" as *u8, xor_c)
178 gv_check("F1-checked-build-carries-fused-overflow-branches-jo-or-jno-at-least-two" as *u8, (jo_c >= CJG_MIN_FUSED) as i64, ctr)
179 gv_check("F1-plain-build-carries-no-overflow-branch" as *u8, (jo_p == 0) as i64, ctr)
180 gv_check("F1-no-checked-site-survives-in-the-long-form-the-checked-build-adds-zero-xorq-to-plain" as *u8, ((xor_p >= 0) as i64) * ((xor_c == xor_p) as i64), ctr)
181 let c1p: i64 = cjg_exit_code(cjg_run0(e1p, out_tmp, envp, cclog))
182 let c1c: i64 = cjg_exit_code(cjg_run0(e1c, out_tmp, envp, cclog))
183 let c1d: i64 = cjg_exit_code(cjg_run0(e1d, out_tmp, envp, cclog))
184 cjg_kv("f1_exit_plain" as *u8, c1p); cjg_kv("f1_exit_chk" as *u8, c1c); cjg_kv("f1_exit_daily" as *u8, c1d)
185 gv_check("F1-plain-loop-computes-500500-mod-251-is-6" as *u8, (c1p == CJG_F1_EXIT) as i64, ctr)
186 gv_check("F1-checked-loop-computes-6-through-the-fused-branches" as *u8, (c1c == CJG_F1_EXIT) as i64, ctr)
187 gv_check("F1-daily-mode-loop-computes-6-the-fuse-composes-with-the-whole-bundle" as *u8, (c1d == CJG_F1_EXIT) as i64, ctr)
188
189 // ---- F2: the overflowing add still traps ----
190 let c2p: i64 = cjg_exit_code(cjg_run0(e2p, out_tmp, envp, cclog))
191 let c2c: i64 = cjg_exit_code(cjg_run0(e2c, out_tmp, envp, cclog))
192 cjg_kv("f2_exit_plain" as *u8, c2p); cjg_kv("f2_exit_chk" as *u8, c2c)
193 gv_check("F2-fixture-reached-the-condition-plain-build-wraps-MAX-plus-1-to-91" as *u8, (c2p == CJG_WRAP_ADD_EXIT) as i64, ctr)
194 gv_check("F2-overflowing-add-traps-72-under-chkarith-through-jo" as *u8, (c2c == CJG_TRAP_OVERFLOW) as i64, ctr)
195 gv_bite("bite-the-trap-fires-on-the-overflowing-add-and-stays-silent-on-the-in-range-loop" as *u8, (c2c == CJG_TRAP_OVERFLOW) as i64, (c1c == CJG_TRAP_OVERFLOW) as i64, ctr)
196
197 // ---- F3: the overflowing sub still traps ----
198 let c3p: i64 = cjg_exit_code(cjg_run0(e3p, out_tmp, envp, cclog))
199 let c3c: i64 = cjg_exit_code(cjg_run0(e3c, out_tmp, envp, cclog))
200 cjg_kv("f3_exit_plain" as *u8, c3p); cjg_kv("f3_exit_chk" as *u8, c3c)
201 gv_check("F3-fixture-reached-the-condition-plain-build-wraps-MIN-minus-1-to-159" as *u8, (c3p == CJG_WRAP_SUB_EXIT) as i64, ctr)
202 gv_check("F3-overflowing-sub-traps-72-under-chkarith-through-jo" as *u8, (c3c == CJG_TRAP_OVERFLOW) as i64, ctr)
203 let jo_3: i64 = cjg_count(s3c, " jo ." as *u8) + cjg_count(s3c, " jno ." as *u8)
204 cjg_kv("f3_jo_chk" as *u8, jo_3)
205 gv_check("F3-the-sub-shape-is-fused-too-its-checked-assembly-carries-an-overflow-branch" as *u8, (jo_3 >= 1) as i64, ctr)
206
207 // ---- F4: wrap-around by intent stays exempt ----
208 let c4c: i64 = cjg_exit_code(cjg_run0(e4c, out_tmp, envp, cclog))
209 cjg_kv("f4_exit_chk" as *u8, c4c)
210 gv_check("F4-declared-wrap-add-is-exempt-under-chkarith-and-wraps-to-91" as *u8, (c4c == CJG_WRAP_ADD_EXIT) as i64, ctr)
211
212 sys_close(cclog)
213 sys_exit(gv_verdict("CHKARITH-JO-GATE" as *u8, ctr, "every checked add and sub is add-then-jo on the live flags, and every overflow still traps 72" as *u8))
214 return 0
215}