nx_g17_probe.nx source
↩ module page · 12 lines · 554 B
1// nx_g17_probe.nx -- emits ONE provable div (masked -> nonneg) and ONE
2// sign-unknown div, so the asm shows G17 fired (bare shrq) on the first and
3// kept the bias dance (sarq $63) on the second. Not a bench; an asm witness.
4// license_tier: ORIGINAL No hw writes (Rule 26).
5import "nx_syscalls_x86_64.nx"
6func g17_provable(x: i64) -> i64 { let m: i64 = x & 1023 return m / 8 }
7func g17_unknown(x: i64) -> i64 { return x / 8 }
8func main() -> i64 {
9 let a: i64 = g17_provable(1000)
10 let b: i64 = g17_unknown(0 - 1001)
11 return (a + b) & 255
12}