nx_mcu_q4_gate.nx source
↩ module page · 147 lines · 6727 B
1// nx_mcu_q4_gate.nx -- pins the int4 x int8 MCU kernel to EXACT integer answers.
2//
3// Every expectation below is hand-computable, so this gate asserts EQUALITY, not closeness. That matters:
4// the two classic ways to get this kernel wrong -- swapping the low/high nibble order, and reading int8
5// activations as unsigned -- both still produce plausible, well-scaled numbers. A tolerance-based check
6// would wave them through. So each control is chosen so that the WRONG implementation yields a DIFFERENT
7// NUMBER, and the gate names that number:
8// T2 a swapped packer would emit 0x0F where we require 0xF0.
9// T5b an unsigned read of byte 255 yields 255, not -1.
10// T7b an unsigned-activation dot yields -2011, not 37 -- and the gate asserts it is NOT -2011.
11// T12 is the composition property real inference depends on: summing per-group dots must equal the whole
12// row dot, or every grouped matvec silently drifts from the reference.
13// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
14import "nx_syscalls.nx"
15import "nx_gate_verdict.nx"
16import "nx_mcu_q4.nx"
17
18func main() -> i64 {
19 let ctr: *i64 = gv_ctr()
20 gv_head("nx_mcu_q4_gate -- int4 weight x int8 activation group dot, pinned to exact integers" as *u8)
21
22 let vals: *i64 = sys_mmap(64 * 8) as *i64
23 let row: *u8 = sys_mmap(64)
24 let xq: *u8 = sys_mmap(64)
25
26 // ---- T1 code/value mapping over the full int4 range, via a real pack+unpack round trip
27 var j: i64 = 0
28 while j < 16 { vals[j] = j - 8; j = j + 1 }
29 q4_pack(row, vals, 16)
30 var t1: i64 = 1
31 j = 0
32 while j < 16 { if q4_val_at(row, j) != (j - 8) { t1 = 0 } j = j + 1 }
33 gv_check("T1 pack/unpack round-trips every int4 code exactly across -8..+7" as *u8, t1, ctr)
34
35 // ---- T2 DIRECTION PIN: column 0 goes in the LOW nibble. pack([-8,+7]) MUST be 0xF0 (240).
36 // A swapped packer emits 0x0F (15) and is caught here, not three layers downstream.
37 vals[0] = 0 - 8
38 vals[1] = 7
39 q4_pack(row, vals, 2)
40 var t2: i64 = 0
41 if (row[0] as i64) == 240 { t2 = 1 }
42 gv_check("T2 DIRECTION: even column -> LOW nibble; pack([-8,+7])==0xF0 (a swapped packer gives 0x0F)" as *u8, t2, ctr)
43
44 // ---- T3 and the unpack side agrees with that direction
45 var t3: i64 = 0
46 if q4_val_at(row, 0) == (0 - 8) { if q4_val_at(row, 1) == 7 { t3 = 1 } }
47 gv_check("T3 unpack agrees with pack on direction: val[0]==-8, val[1]==+7" as *u8, t3, ctr)
48
49 // ---- T4 ragged row sizing: rows are byte-aligned, odd cols leave a dead high nibble
50 var t4: i64 = 1
51 if q4_row_bytes(0) != 0 { t4 = 0 }
52 if q4_row_bytes(1) != 1 { t4 = 0 }
53 if q4_row_bytes(2) != 1 { t4 = 0 }
54 if q4_row_bytes(3) != 2 { t4 = 0 }
55 if q4_row_bytes(4) != 2 { t4 = 0 }
56 if q4_row_bytes(5) != 3 { t4 = 0 }
57 gv_check("T4 row_bytes=ceil(cols/2) for cols 0..5 (ragged, byte-aligned, never padded)" as *u8, t4, ctr)
58
59 // ---- T5 int8 sign extension
60 var t5: i64 = 1
61 if q4_i8(0) != 0 { t5 = 0 }
62 if q4_i8(127) != 127 { t5 = 0 }
63 if q4_i8(128) != (0 - 128) { t5 = 0 }
64 if q4_i8(255) != (0 - 1) { t5 = 0 }
65 gv_check("T5 int8 sign extension: 0->0, 127->127, 128->-128, 255->-1" as *u8, t5, ctr)
66
67 // ---- T5b NEG-CONTROL on T5: an unsigned read returns 255. Prove we are not doing that.
68 var t5b: i64 = 0
69 if q4_i8(255) != 255 { t5b = 1 }
70 gv_check("T5b NEG-CONTROL: byte 255 is NOT read as 255 (sign extension actually happens)" as *u8, t5b, ctr)
71
72 // ---- T6 exact dot with positive activations: row=[-8,+7], xq=[2,3] -> -16+21 = 5
73 xq[0] = 2 as u8
74 xq[1] = 3 as u8
75 var t6: i64 = 0
76 if q4_group_dot(row, xq, 0, 2) == 5 { t6 = 1 }
77 gv_check("T6 exact dot: (-8*2)+(7*3) == 5" as *u8, t6, ctr)
78
79 // ---- T7 exact dot with a NEGATIVE activation: xq=[254(-2),3] -> 16+21 = 37
80 xq[0] = 254 as u8
81 xq[1] = 3 as u8
82 let d7: i64 = q4_group_dot(row, xq, 0, 2)
83 var t7: i64 = 0
84 if d7 == 37 { t7 = 1 }
85 gv_check("T7 exact dot with a negative activation: (-8*-2)+(7*3) == 37" as *u8, t7, ctr)
86
87 // ---- T7b NEG-CONTROL: reading that activation unsigned gives (-8*254)+(7*3) = -2011.
88 // This is the tooth that makes T7 mean something at the RESULT level, not just in the helper.
89 var t7b: i64 = 0
90 if d7 != (0 - 2011) { t7b = 1 }
91 gv_check("T7b NEG-CONTROL: the dot is NOT -2011 (unsigned activations would give exactly that)" as *u8, t7b, ctr)
92
93 // ---- T8 empty range contributes nothing
94 var t8: i64 = 0
95 if q4_group_dot(row, xq, 1, 1) == 0 { t8 = 1 }
96 gv_check("T8 an empty column range dots to 0" as *u8, t8, ctr)
97
98 // ---- T9 MISALIGNED START: a group beginning on an ODD column reads the HIGH nibble first.
99 // row=[-8,+7], begin=1 -> 7 * xq[1](3) = 21. This is the branch most ports get wrong.
100 var t9: i64 = 0
101 if q4_group_dot(row, xq, 1, 2) == 21 { t9 = 1 }
102 gv_check("T9 group starting on an ODD column reads the high nibble first: 7*3 == 21" as *u8, t9, ctr)
103
104 // ---- T10 RAGGED TAIL: odd cols=3, last value sits in the LOW nibble of the final byte
105 vals[0] = 0 - 8
106 vals[1] = 7
107 vals[2] = 0 - 1
108 q4_pack(row, vals, 3)
109 xq[0] = 1 as u8
110 xq[1] = 1 as u8
111 xq[2] = 1 as u8
112 var t10: i64 = 0
113 if q4_row_bytes(3) == 2 { if q4_val_at(row, 2) == (0 - 1) { if q4_row_dot(row, xq, 3) == (0 - 2) { t10 = 1 } } }
114 gv_check("T10 ragged tail: odd cols=3 -> 2 bytes, val[2]==-1, row dot == -2" as *u8, t10, ctr)
115
116 // ---- T11 group geometry, including the CLAMP on the short final group
117 var t11: i64 = 1
118 if q4_n_groups(5, 2) != 3 { t11 = 0 }
119 if q4_group_end(5, 2, 0) != 2 { t11 = 0 }
120 if q4_group_end(5, 2, 1) != 4 { t11 = 0 }
121 if q4_group_end(5, 2, 2) != 5 { t11 = 0 }
122 gv_check("T11 groups over cols=5 width=2 -> 3 groups, final group CLAMPED to 5 not 6" as *u8, t11, ctr)
123
124 // ---- T12 COMPOSITION: sum of per-group dots MUST equal the whole-row dot, or every grouped
125 // matvec drifts from the reference. cols=5 across 3 ragged groups.
126 j = 0
127 while j < 5 { vals[j] = j - 2; j = j + 1 }
128 q4_pack(row, vals, 5)
129 xq[0] = 1 as u8
130 xq[1] = 254 as u8
131 xq[2] = 3 as u8
132 xq[3] = 127 as u8
133 xq[4] = 200 as u8
134 let whole: i64 = q4_row_dot(row, xq, 5)
135 var parts: i64 = 0
136 var gi: i64 = 0
137 while gi < q4_n_groups(5, 2) {
138 parts = parts + q4_group_dot(row, xq, gi * 2, q4_group_end(5, 2, gi))
139 gi = gi + 1
140 }
141 var t12: i64 = 0
142 if whole == parts { t12 = 1 }
143 gv_check("T12 COMPOSITION: sum of ragged per-group dots equals the whole-row dot" as *u8, t12, ctr)
144
145 let rc: i64 = gv_verdict("MCU-Q4" as *u8, ctr, "int4xint8 group dot is exact: direction, sign, ragged tail, clamp and composition all pinned" as *u8)
146 return rc
147}