code wiki / _hdl_build / nx_recycler_intguard_gate.nx
nx_recycler_intguard_gate.nx source
↩ module page · 58 lines · 3216 B
1import "nx_gate_gn.nx"
2// nx_recycler_intguard_gate.nx -- proves the integer-overflow-recycled checked-arithmetic primitive catches real
3// i64 overflow and passes safe arithmetic. Large operands are BUILT by shifting (1<<62) to avoid the large-literal
4// miscompile landmine. Grounding: the source artifact recyc_intoverflow.raw exists. expect_exit: 0
5import "nx_syscalls.nx"
6import "nx_recycler_intguard.nx"
7import "nx_gate_verdict.nx"
8
9func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
10func have_file(p: *u8) -> i64 { let fd: i64=sys_openat_rd(p); if fd<0 { return 0 } sys_close(fd); return 1 }
11
12func main() -> i64 {
13 gp("=== nx_recycler_intguard_gate: integer-overflow recycled into checked i64 arithmetic ===\n" as *u8)
14 var pass: i64=0; var fail: i64=0
15 let ok: *i64 = sys_mmap(16) as *i64
16 let big: i64 = 1 << 62 // 4.6e18, positive, < MAX (built, not a huge literal)
17
18 // KAT1 safe add -> ok, correct result
19 let r1: i64 = ig_add_checked(5, 3, ok)
20 if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-safe-add-flagged\n" as *u8) }
21 if r1==8 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-wrong-sum\n" as *u8) }
22
23 // KAT2 ADD OVERFLOW: big + big wraps positive -> negative
24 ig_add_checked(big, big, ok)
25 if ok[0]==0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat2-add-overflow-missed\n" as *u8) }
26
27 // KAT3 add with opposite signs never overflows
28 ig_add_checked(big, 0-big, ok)
29 if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat3-false-overflow-opposite-signs\n" as *u8) }
30
31 // KAT4 safe mul -> ok, correct result
32 let r4: i64 = ig_mul_checked(6, 7, ok)
33 if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat4-safe-mul-flagged\n" as *u8) }
34 if r4==42 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat4-wrong-product\n" as *u8) }
35
36 // KAT5 MUL OVERFLOW: big * 4 = 1<<64 wraps
37 ig_mul_checked(big, 4, ok)
38 if ok[0]==0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat5-mul-overflow-missed\n" as *u8) }
39
40 // KAT6 mul no-overflow: (1<<30)*(1<<30) = 1<<60, fits
41 let m: i64 = 1 << 30
42 ig_mul_checked(m, m, ok)
43 if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat6-false-mul-overflow\n" as *u8) }
44
45 // KAT7 grounding: the integer-overflow intake artifact exists
46 if have_file("knowledge/fetched/recyc_intoverflow.raw" as *u8)==1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat7-ungrounded\n" as *u8) }
47
48 gp("RECYCLER-INTGUARD-GATE pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail)
49 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
50 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
51 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
52 let ctr__dry: *i64 = gv_ctr()
53 ctr__dry[0] = pass
54 ctr__dry[1] = pass + fail
55 let rc__dry: i64 = gv_verdict("RECYCLER-INTGUARD-GATE" as *u8, ctr__dry, "i64 add/mul overflow CAUGHT, safe arithmetic passes -- the integer-overflow CVE recycled into a checked primitive)" as *u8)
56 sys_exit(rc__dry)
57 return rc__dry
58}