_nx_bits_clz64_oracle.nx source
↩ module page · 71 lines · 2418 B
1// _nx_bits_clz64_oracle.nx
2//
3// Paired correctness oracle for nx_bits_clz64 / nx_bits_ctz64
4// (composed from two 32-bit intrinsics). Each must match a portable
5// reference implementation (the legacy Knuth linear-scan) on the
6// curated input set.
7
8import "syscalls.nx"
9import "nx_bits.nx"
10import "nx_loop.nx"
11
12// Reference (Knuth TAOCP 4A linear scan, structured via V2 loop API).
13// Same algorithm; bound = 64 declared at the call site; verdict is
14// pattern-matched. Lighthouse migration for the post-cardinal loop
15// discipline (see [[feedback-loop-discipline-cardinal-2026-05-21]]).
16func _ref_clz64(x: i64) -> i64 {
17 if x == 0 { return 64 }
18 var v: i64 = x
19 var n: i64 = 0
20 var mask: i64 = 0x8000000000000000
21 let lp: *NxLoopFrame = nx_loop_begin(64)
22 while nx_loop_step(lp) == 1 {
23 if (v & mask) != 0 {
24 nx_loop_break(lp)
25 } else {
26 n = n + 1
27 mask = mask >> 1
28 if mask == 0 { nx_loop_break(lp) }
29 }
30 }
31 return n
32}
33
34func _ref_ctz64(x: i64) -> i64 {
35 if x == 0 { return 64 }
36 var v: i64 = x
37 var n: i64 = 0
38 let lp: *NxLoopFrame = nx_loop_begin(64)
39 while nx_loop_step(lp) == 1 {
40 if (v & 1) != 0 {
41 nx_loop_break(lp)
42 } else {
43 n = n + 1
44 v = v >> 1
45 if n >= 64 { nx_loop_break(lp) }
46 }
47 }
48 return n
49}
50
51func main() -> i64 {
52 // clz64 oracles
53 if nx_bits_clz64(0) != _ref_clz64(0) { return 1 }
54 if nx_bits_clz64(1) != _ref_clz64(1) { return 2 }
55 if nx_bits_clz64(-1) != _ref_clz64(-1) { return 3 }
56 if nx_bits_clz64(0x100000000) != _ref_clz64(0x100000000) { return 4 }
57 if nx_bits_clz64(0xFFFFFFFF) != _ref_clz64(0xFFFFFFFF) { return 5 }
58 if nx_bits_clz64(0x4000000000000000) != _ref_clz64(0x4000000000000000) { return 6 }
59 if nx_bits_clz64(0x0000800000000000) != _ref_clz64(0x0000800000000000) { return 7 }
60
61 // ctz64 oracles
62 if nx_bits_ctz64(0) != _ref_ctz64(0) { return 8 }
63 if nx_bits_ctz64(1) != _ref_ctz64(1) { return 9 }
64 if nx_bits_ctz64(-1) != _ref_ctz64(-1) { return 10 }
65 if nx_bits_ctz64(0x100000000) != _ref_ctz64(0x100000000) { return 11 }
66 if nx_bits_ctz64(0x80000000) != _ref_ctz64(0x80000000) { return 12 }
67 if nx_bits_ctz64(0x10) != _ref_ctz64(0x10) { return 13 }
68 if nx_bits_ctz64(0x4000000000000000) != _ref_ctz64(0x4000000000000000) { return 14 }
69
70 return 0
71}