code wiki / _hdl_build / nx_eqsat_bw_witness.nx
nx_eqsat_bw_witness.nx source
↩ module page · 43 lines · 1537 B
1// Throwaway witness: confirm mod-2^W truncation semantics for the bounded proof.
2// For W bits, mask = 2^W - 1. CLAIM: ((x * (1<<k)) & mask) == ((x << k) & mask)
3// for ALL x in [0,2^W) and ALL k in [0,W). This is the mul_pow2 identity mod 2^W.
4// Known answer (FAIL LOUD): "<total> <total> ".
5
6import "nx_syscalls.nx"
7
8func _emit_num(v: i64) -> i64 {
9 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n }
10 let t2: *u8 = sys_mmap(28); var t: i64 = 0
11 if n == 0 { t2[0] = 48; t = 1 }
12 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
13 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
14 b[t] = 32; sys_write(1, b, t + 1); return 0
15}
16func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
17
18func main() -> i64 {
19 let W: i64 = 16
20 let N: i64 = 1
21 var ws: i64 = 0
22 var nn: i64 = 1
23 while ws < W { nn = nn * 2; ws = ws + 1 } // nn = 2^W
24 let mask: i64 = nn - 1
25 var total: i64 = 0
26 var agree: i64 = 0
27 var x: i64 = 0
28 while x < nn {
29 var k: i64 = 0
30 while k < W {
31 let pw: i64 = (1 << k)
32 let lhs: i64 = (x * pw) & mask // mul x 2^k (truncated)
33 let rhs: i64 = (x << k) & mask // shl x k (truncated)
34 total = total + 1
35 if lhs == rhs { agree = agree + 1 }
36 k = k + 1
37 }
38 x = x + 1
39 }
40 _emit_num(agree); _emit_num(total); _nl()
41 if agree != total { sys_exit(1); return 1 }
42 sys_exit(0); return 0
43}