_probe_mulpow2_soundness.nx source
↩ module page · 79 lines · 3147 B
1// Adversarial probe #2: is the LIVE rule's union actually SOUND for every k it
2// admits? The live rule computes k by halving a positive const and fires if
3// is_pow2 && k<64. We verify: for EVERY k the live guard admits (i.e. every
4// positive power-of-two const), does (x * 2^k) == (x << k) hold in REAL 64-bit
5// 2's-complement arithmetic (native i64, which IS mod-2^64)? And we confirm the
6// k>=W path is genuinely unreachable from a positive const.
7
8import "nx_syscalls.nx"
9
10const NX_EQSAT_W: i64 = 64
11
12func _emit_num(v: i64) -> i64 {
13 let b: *u8 = sys_mmap(40); var n: i64 = v; if n < 0 { n = 0 - n }
14 let t2: *u8 = sys_mmap(40); var t: i64 = 0
15 if v < 0 { sys_write(1, "-", 1) }
16 if n == 0 { t2[0] = 48; t = 1 }
17 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
18 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
19 b[t] = 32; sys_write(1, b, t + 1); return 0
20}
21func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
22
23// log2-by-halving exactly as the live rule does it (positive cval path).
24func live_k(cval: i64) -> i64 {
25 var k: i64 = 0
26 var t: i64 = cval
27 while t > 1 { t = t / 2; k = k + 1 }
28 return k
29}
30
31func main() -> i64 {
32 // For every positive power-of-two const 2^k (k = 1..62; 2^63 is negative as
33 // i64 so the live rule's cval>1 rejects it), verify mul==shl in native i64.
34 // Also confirm the live_k matches k and stays < 64.
35 var k: i64 = 1
36 var max_k_seen: i64 = 0
37 var all_sound: i64 = 1
38 var any_k_ge_W: i64 = 0
39 // sample x values including sign-bit and high-bit cases
40 let xs: *i64 = sys_mmap(8 * 8) as *i64
41 xs[0] = 1
42 xs[1] = 3
43 xs[2] = 0 - 1 // all ones
44 xs[3] = 0 - 9223372036854775807 - 1 // i64 MIN (sign bit)
45 xs[4] = 12345678901234567
46 xs[5] = 1 << 40
47 let nxs: i64 = 6
48 while k < 63 {
49 let cval: i64 = 1 << k // 2^k, positive for k in 1..62
50 if cval > 1 {
51 let lk: i64 = live_k(cval)
52 if lk != k { all_sound = 0 }
53 if lk >= NX_EQSAT_W { any_k_ge_W = 1 }
54 if lk > max_k_seen { max_k_seen = lk }
55 // soundness: x*2^k == x<<k in native i64 (== mod 2^64) for all sample x
56 var xi: i64 = 0
57 while xi < nxs {
58 let x: i64 = xs[xi]
59 let viamul: i64 = x * cval
60 let viashl: i64 = x << k
61 if viamul != viashl { all_sound = 0 }
62 xi = xi + 1
63 }
64 }
65 k = k + 1
66 }
67 // RESULT LINE: all_sound (1=every admitted k gives mul==shl), max_k_seen,
68 // any_k_ge_W (1=guard's k>=W path was reachable from pos const).
69 _emit_num(all_sound); _emit_num(max_k_seen); _emit_num(any_k_ge_W); _nl()
70
71 // SECOND CHECK: the cval=2^63 case. As an i64 literal 1<<63 is negative; the
72 // live rule's `if cval > 1` is FALSE so it never fires. Confirm by value.
73 let c63: i64 = 1 << 63
74 var c63_rejected: i64 = 0
75 if c63 > 1 { c63_rejected = 0 } else { c63_rejected = 1 }
76 _emit_num(c63); _emit_num(c63_rejected); _nl()
77
78 sys_exit(0); return 0
79}