_probe_mulpow2_guard.nx source
↩ module page · 76 lines · 3175 B
1// Adversarial probe: reproduce the EXACT log2-by-halving + k<W guard logic from
2// nx_eqsat_apply_rule_mul_pow2 (lines 447-471) on hostile constants, to test
3// whether the guard has a hole. We do NOT import nx_eqsat (that would drag the
4// gsim); we transcribe the guard arithmetic 1:1.
5
6import "nx_syscalls.nx"
7
8const NX_EQSAT_W: i64 = 64
9
10func _emit_num(v: i64) -> i64 {
11 let b: *u8 = sys_mmap(40); var n: i64 = v; if n < 0 { n = 0 - n }
12 let t2: *u8 = sys_mmap(40); var t: i64 = 0
13 if v < 0 { sys_write(1, "-", 1) }
14 if n == 0 { t2[0] = 48; t = 1 }
15 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
16 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
17 b[t] = 32; sys_write(1, b, t + 1); return 0
18}
19func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
20
21// Returns: would_fire (1=union would happen), k computed, is_pow2 flag.
22// Transcribes lines 453-471 EXACTLY. Returns k via out ptr; result = would_fire.
23func guard_decision(cval: i64, out_k: *i64, out_pow2: *i64) -> i64 {
24 out_k[0] = 0 - 7777
25 out_pow2[0] = 0 - 7777
26 var fired: i64 = 0
27 if cval > 1 { // line 453
28 var k: i64 = 0
29 var t: i64 = cval
30 var is_pow2: i64 = 1
31 while t > 1 { // lines 458-462
32 if (t % 2) != 0 { is_pow2 = 0 }
33 t = t / 2
34 k = k + 1
35 }
36 out_k[0] = k
37 out_pow2[0] = is_pow2
38 if is_pow2 == 1 { if k < NX_EQSAT_W { // line 464 GUARD
39 fired = 1
40 } }
41 }
42 return fired
43}
44
45func main() -> i64 {
46 let kp: *i64 = sys_mmap(8) as *i64
47 let pp: *i64 = sys_mmap(8) as *i64
48
49 // SCENARIO 1: cval = 2^63 (the i64 MIN as a positive-looking power of two is
50 // actually negative). 1<<63 = -9223372036854775808.
51 let two63: i64 = 1 << 63
52 let f1: i64 = guard_decision(two63, kp, pp)
53 _emit_num(two63); _emit_num(f1); _emit_num(kp[0]); _emit_num(pp[0]); _nl()
54
55 // SCENARIO 2: cval = -8 (a negative constant whose payload looks like a
56 // negative number). cval>1 is FALSE for -8, so the rule never fires. Confirm.
57 let negeight: i64 = 0 - 8
58 let f2: i64 = guard_decision(negeight, kp, pp)
59 _emit_num(negeight); _emit_num(f2); _emit_num(kp[0]); _emit_num(pp[0]); _nl()
60
61 // SCENARIO 3: cval = 2^62 (largest CLEAN positive power of two that fits in
62 // i64 as a positive value). k should be 62, < 64, so it FIRES. Is x*2^62
63 // == x<<62 sound in 64-bit? Yes mod 2^64. Confirm k=62 fires.
64 let two62: i64 = 1 << 62
65 let f3: i64 = guard_decision(two62, kp, pp)
66 _emit_num(two62); _emit_num(f3); _emit_num(kp[0]); _emit_num(pp[0]); _nl()
67
68 // SCENARIO 4: cval = 2^63 reached by *positive* doubling path won't happen
69 // (overflows to negative). But what about cval that is a NON-power-of-2 with a
70 // huge bit set, e.g. 0x6000...0 -- ensure is_pow2 catches it. Use 3<<61.
71 let huge_nonpow2: i64 = 3 << 61
72 let f4: i64 = guard_decision(huge_nonpow2, kp, pp)
73 _emit_num(huge_nonpow2); _emit_num(f4); _emit_num(kp[0]); _emit_num(pp[0]); _nl()
74
75 sys_exit(0); return 0
76}