code wiki / _hdl_build / nx_recycler_intguard_gate.nx
`nx_recycler_intguard_gate.nx` source

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"
7
8func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
9func have_file(p: *u8) -> i64 { let fd: i64=sys_openat_rd(p); if fd<0 { return 0 } sys_close(fd); return 1 }
10
11func main() -> i64 {
12    gp("=== nx_recycler_intguard_gate: integer-overflow recycled into checked i64 arithmetic ===\n" as *u8)
13    var pass: i64=0; var fail: i64=0
14    let ok: *i64 = sys_mmap(16) as *i64
15    let big: i64 = 1 << 62                       // 4.6e18, positive, < MAX (built, not a huge literal)
16
17    // KAT1 safe add -> ok, correct result
18    let r1: i64 = ig_add_checked(5, 3, ok)
19    if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat1-safe-add-flagged\n" as *u8) }
20    if r1==8 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat1-wrong-sum\n" as *u8) }
21
22    // KAT2 ADD OVERFLOW: big + big wraps positive -> negative
23    ig_add_checked(big, big, ok)
24    if ok[0]==0 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat2-add-overflow-missed\n" as *u8) }
25
26    // KAT3 add with opposite signs never overflows
27    ig_add_checked(big, 0-big, ok)
28    if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat3-false-overflow-opposite-signs\n" as *u8) }
29
30    // KAT4 safe mul -> ok, correct result
31    let r4: i64 = ig_mul_checked(6, 7, ok)
32    if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat4-safe-mul-flagged\n" as *u8) }
33    if r4==42 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat4-wrong-product\n" as *u8) }
34
35    // KAT5 MUL OVERFLOW: big * 4 = 1<<64 wraps
36    ig_mul_checked(big, 4, ok)
37    if ok[0]==0 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat5-mul-overflow-missed\n" as *u8) }
38
39    // KAT6 mul no-overflow: (1<<30)*(1<<30) = 1<<60, fits
40    let m: i64 = 1 << 30
41    ig_mul_checked(m, m, ok)
42    if ok[0]==1 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat6-false-mul-overflow\n" as *u8) }
43
44    // KAT7 grounding: the integer-overflow intake artifact exists
45    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) }
46
47    gp("RECYCLER-INTGUARD-GATE pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail)
48    if fail==0 { gp(" verdict=GREEN (i64 add/mul overflow CAUGHT, safe arithmetic passes -- the integer-overflow CVE recycled into a checked primitive)\n" as *u8); sys_exit(0); return 0 }
49    gp(" verdict=RED\n" as *u8); sys_exit(1); return 1
50}
nx_recycler_intguard_gate.nx source

`nx_recycler_intguard_gate.nx` source
