code wiki / _hdl_build / nx_triangulate_test.nx
nx_triangulate_test.nx source
↩ module page · 146 lines · 6170 B
1// nx_triangulate_test.nx -- VALIDATES the reusable triangulation harness
2// (nx_triangulate.nx) itself: proves it PASSES three agreeing legs and CATCHES a
3// deliberately-wrong leg. A harness that only ever says "pass" is worthless; this
4// test proves the catch path fires, so the harness can be trusted to gate real
5// capabilities (Cardinal 7 test before ship; Cardinal 25 build intelligence).
6//
7// We exercise the harness on a REAL capability (integer division) using three
8// genuinely independent legs over a battery, exactly as the divider proof does:
9// LEG A -- Newton-Raphson reciprocal divide (the multiplicative frontier)
10// LEG B -- restoring shift-subtract divide (independent algorithm)
11// LEG C -- behavioral `/` (oracle is C; A,B are the legs judged against it)
12// Then we run two adversarial scenarios THROUGH the harness:
13// (1) all three legs correct -> harness must report PASS, all-agree.
14// (2) one leg deliberately corrupted (off-by-one) -> harness must report a
15// CAUGHT failure, naming the bad leg index + its wrong value.
16//
17// KNOWN ANSWER (FAIL LOUD), one line:
18// "<good_passed> <good_total> <caught> <bad_leg> <bad_got> <bad_exp> <argguard>"
19// good_passed == good_total (clean battery: every vector triangulates)
20// caught == 1 (the corrupted leg WAS detected, not swallowed)
21// bad_leg, bad_got, bad_exp (the 5W1H diagnostic the harness surfaced)
22// argguard == 1 (boundary guard rejects a malformed request)
23// Any deviation -> nonzero exit. Expected: "65536 65536 1 1 36 35 1 " run=0
24
25import "nx_triangulate.nx"
26
27const TW_W: i64 = 16
28const TW_F: i64 = 65536
29const TW_FF: i64 = 4294967296
30const TW_ITERS: i64 = 3
31
32func _emit_num(v: i64) -> i64 {
33 let b: *u8 = sys_mmap(28); var n: i64 = v; if n < 0 { n = 0 - n }
34 let t2: *u8 = sys_mmap(28); var t: i64 = 0
35 if n == 0 { t2[0] = 48; t = 1 }
36 while n > 0 { t2[t] = 48 + (n % 10); n = n / 10; t = t + 1 }
37 var i: i64 = 0; while i < t { b[i] = t2[t - 1 - i]; i = i + 1 }
38 b[t] = 32; sys_write(1, b, t + 1); return 0
39}
40func _nl() -> i64 { let z: *u8 = sys_mmap(2); z[0] = 10; sys_write(1, z, 1); return 0 }
41
42// MSB position p such that 2^p <= d < 2^(p+1) (d >= 1)
43func tw_msb_pos(d: i64) -> i64 {
44 var p: i64 = 0
45 while (1 << (p + 1)) <= d { p = p + 1 }
46 return p
47}
48
49// LEG A -- Newton reciprocal divide (the proven scalar at W=16).
50func tw_newton(N: i64, D: i64) -> i64 {
51 let p: i64 = tw_msb_pos(D)
52 let s: i64 = 15 - p
53 let dn: i64 = D << s
54 var x: i64 = (48 * TW_F - 32 * dn) / 17
55 var it: i64 = 0
56 while it < TW_ITERS {
57 let dx: i64 = dn * x
58 let t: i64 = 2 * TW_FF - dx
59 x = (x * t) >> 32
60 it = it + 1
61 }
62 var q: i64 = (N * x) >> (17 + p)
63 while (q + 1) * D <= N { q = q + 1 }
64 while q * D > N { q = q - 1 }
65 return q
66}
67
68// LEG B -- independent restoring (shift-subtract) divider, W=16.
69func tw_restoring(N: i64, D: i64) -> i64 {
70 var q: i64 = 0
71 var r: i64 = 0
72 var i: i64 = TW_W - 1
73 while i >= 0 {
74 r = (r << 1) | ((N >> i) & 1)
75 if r >= D { r = r - D; q = q | (1 << i) }
76 i = i - 1
77 }
78 return q
79}
80
81func main() -> i64 {
82 let legs: *i64 = sys_mmap(8 * 8) as *i64
83 let v: *NxTriVerdict = sys_mmap(64) as *NxTriVerdict
84 let t: *NxTriTally = sys_mmap(64) as *NxTriTally
85
86 // ---- SCENARIO 1: clean battery, all three legs correct, harness must PASS
87 // every vector. Dense exhaustive D in [1,128], N in [0,511] = 65536 vectors;
88 // each judged by nx_tri_pass_strict requiring >=3 independent legs all == oracle.
89 nx_tri_tally_init(t)
90 var vec: i64 = 0
91 var D: i64 = 1
92 while D <= 128 {
93 var N: i64 = 0
94 while N <= 511 {
95 legs[0] = tw_newton(N, D) // LEG A
96 legs[1] = tw_restoring(N, D) // LEG B
97 legs[2] = N / D // LEG C (here treated as a 3rd witness)
98 let oracle: i64 = N / D // ground truth
99 nx_tri_pass_strict(legs, 3, oracle, 3, v)
100 nx_tri_tally_add(t, v, vec)
101 vec = vec + 1
102 N = N + 1
103 }
104 D = D + 1
105 }
106 let good_passed: i64 = t.passed
107 let good_total: i64 = t.total
108
109 // ---- SCENARIO 2: inject a deliberately-WRONG leg, harness must CATCH it.
110 // N=35, D=1 -> oracle=35. Legs A,B correct (35); leg index 1 corrupted to 36
111 // (off-by-one). A harness that catches this reports pass=0, first_bad=1,
112 // bad_value=36, oracle=35. If the harness wrongly passed, caught stays 0 and
113 // we FAIL LOUD below.
114 legs[0] = 35 // correct
115 legs[1] = 35 + 1 // DELIBERATELY WRONG (off-by-one)
116 legs[2] = 35 // correct
117 let oracle2: i64 = 35
118 nx_tri_check(legs, 3, oracle2, 3, v)
119 var caught: i64 = 0
120 if v.pass == 0 { caught = 1 }
121 let bad_leg: i64 = v.first_bad
122 let bad_got: i64 = v.bad_value
123 let bad_exp: i64 = v.oracle
124
125 // ---- SCENARIO 3: boundary guard -- a malformed request (k_min > n_legs)
126 // must be REJECTED loud, not silently treated as a pass.
127 legs[0] = 7; legs[1] = 7; legs[2] = 7
128 let rc: i64 = nx_tri_check(legs, 3, 7, 9, v) // k_min=9 > n_legs=3 -> bad args
129 var argguard: i64 = 0
130 if rc == (0 - NX_TRI_BAD_ARGS) { if v.pass == (0 - 1) { argguard = 1 } }
131
132 _emit_num(good_passed); _emit_num(good_total)
133 _emit_num(caught); _emit_num(bad_leg); _emit_num(bad_got); _emit_num(bad_exp)
134 _emit_num(argguard)
135 _nl()
136
137 // FAIL LOUD known-answer assertions.
138 if good_passed != good_total { sys_exit(1); return 1 } // clean battery all-agree
139 if good_total != 65536 { sys_exit(2); return 2 } // 128 * 512 vectors swept
140 if caught != 1 { sys_exit(3); return 3 } // the wrong leg WAS caught
141 if bad_leg != 1 { sys_exit(4); return 4 } // named the right leg
142 if bad_got != 36 { sys_exit(5); return 5 } // surfaced its wrong value
143 if bad_exp != 35 { sys_exit(6); return 6 } // surfaced the oracle
144 if argguard != 1 { sys_exit(7); return 7 } // boundary guard fires
145 sys_exit(0); return 0
146}