code wiki / (root) / nx_checked_arith_wrap.nx

nx_checked_arith_wrap.nx source

↩ module page · 43 lines · 1375 B

1// nx_checked_arith_wrap.nx -- LN1 wrap-by-intent witness (sibling of nx_checked_arith.nx). 2// __wrap_add / __wrap_sub / __wrap_mul reproduce the WRAPPED values under BOTH modes: under the 3// default they are exactly `+ - *`; under --chkarith they are exempt from the overflow check, 4// so a hash or ring counter written with them keeps running once the mode flips. Exit 0 iff all 5// three wrapped results are the expected ones. Separate file on purpose: a pre-LN1 compiler has 6// no such intrinsics, and the gate must be able to say WHICH tooth the old compiler fails. 7// license_tier: ORIGINAL No hw writes (Rule 26). 8import "nx_syscalls.nx" 9 10func cw_pow62() -> i64 { 11 var m: i64 = 1 12 m = m << 62 13 return m 14} 15func cw_max() -> i64 { 16 let p: i64 = cw_pow62() 17 return p - 1 + p 18} 19func cw_min() -> i64 { 20 var m: i64 = 1 21 m = m << 63 22 return m 23} 24func cw_pow32() -> i64 { 25 var m: i64 = 1 26 m = m << 32 27 return m 28} 29func cw_one() -> i64 { return 1 } 30func cw_zero() -> i64 { return 0 } 31 32func main() -> i64 { 33 let mx: i64 = cw_max() 34 let mn: i64 = cw_min() 35 let one: i64 = cw_one() 36 let p32: i64 = cw_pow32() 37 var bad: i64 = 0 38 if __wrap_add(mx, one) != mn { bad = bad + 1 } 39 if __wrap_sub(mn, one) != mx { bad = bad + 1 } 40 if __wrap_mul(p32, p32) != cw_zero() { bad = bad + 1 } 41 if bad != 0 { return 1 } 42 return 0 43}