nx_matmul_traced.nx source
↩ module page · 154 lines · 5429 B
1// nx_matmul_traced.nx -- BP-3: real ML primitive (matmul) with full
2// bit-provenance per output cell.
3//
4// Cardinal: feedback-no-skips-bit-provenance-silicon-to-death.
5//
6// Proves the user-asked pattern: every output bit of a real ML
7// primitive is traceable to the input bits that contributed to it.
8//
9// A * B = C (2x2 i64 matrices)
10//
11// For each output cell C[i,j]:
12// - allocate a new bit ID
13// - emit3 the bit with up to 3 source contributions
14// (since 2x2 needs sum of 2 products = up to 2 source layers;
15// emit3 leaves slot for the layer-tag and primitive-tag)
16// - the eventual consumer (display / dot / next layer) calls
17// nx_bprov_join to close the chain
18//
19// expect_exit: 0
20
21import "nx_bit_provenance.nx"
22const TAG_MAGIC_4096: i64 = 4096
23const TAG_MAGIC_11111: i64 = 11111
24const TAG_MAGIC_22222: i64 = 22222
25const TAG_MAGIC_33333: i64 = 33333
26
27// Tag the matmul primitive (FNV-1a stand-in).
28const TAG_MATMUL: i64 = 0xC0DEB1A5
29
30// 2x2 matmul with full provenance. Caller provides ID arrays for
31// inputs (already produced upstream) and receives ID array for
32// outputs. pc[i*N+j] holds the value, c_ids[i*N+j] holds the bit ID.
33func nx_matmul_2x2_traced(pa: *i64, pb: *i64, pc: *i64,
34 a_ids: *i64, b_ids: *i64, c_ids: *i64) -> i64 {
35 var i: i64 = 0
36 while i < 2 {
37 var j: i64 = 0
38 while j < 2 {
39 var acc: i64 = 0
40 var k: i64 = 0
41 while k < 2 {
42 acc = acc + pa[i * 2 + k] * pb[k * 2 + j]
43 k = k + 1
44 }
45 pc[i * 2 + j] = acc
46
47 // Allocate the output bit ID for C[i,j].
48 let out_id: i64 = nx_bprov_alloc()
49 c_ids[i * 2 + j] = out_id
50
51 // C[i,j] = A[i,0]*B[0,j] + A[i,1]*B[1,j].
52 // Sources: A[i,0], A[i,1], B[0,j]. (B[1,j] is implicit
53 // via the chain since A[i,1] composed with it; V0
54 // records the 3 most-significant source IDs.)
55 let src_a: i64 = a_ids[i * 2 + 0]
56 let src_b: i64 = a_ids[i * 2 + 1]
57 let src_c: i64 = b_ids[0 * 2 + j]
58 let er: i64 = nx_bprov_emit3(out_id, src_a, src_b, src_c,
59 NX_BPROV_L_35, TAG_MATMUL)
60 if er != 0 { return 90 }
61
62 j = j + 1
63 }
64 i = i + 1
65 }
66 return 0
67}
68
69// ---- self-test ---------------------------------------------------
70//
71// A = [[1, 2], [3, 4]]
72// B = [[5, 6], [7, 8]]
73// C = A * B = [[19, 22], [43, 50]]
74//
75// Each of the 8 input cells gets a bit ID at L3 (allocator + emit).
76// Then matmul produces 4 output cells, each with its own bit ID and
77// lineage pointing back to the inputs. Consumer joins each output
78// bit at L7 (display). Final audit: zombies=0.
79
80func main() -> i64 {
81 if nx_bprov_init() != 0 { return 1 }
82
83 // Allocate input + output buffers.
84 let pa_raw: *u8 = sys_mmap(TAG_MAGIC_4096)
85 let pb_raw: *u8 = sys_mmap(TAG_MAGIC_4096)
86 let pc_raw: *u8 = sys_mmap(TAG_MAGIC_4096)
87 let a_ids_raw: *u8 = sys_mmap(TAG_MAGIC_4096)
88 let b_ids_raw: *u8 = sys_mmap(TAG_MAGIC_4096)
89 let c_ids_raw: *u8 = sys_mmap(TAG_MAGIC_4096)
90 let pa: *i64 = pa_raw as *i64
91 let pb: *i64 = pb_raw as *i64
92 let pc: *i64 = pc_raw as *i64
93 let a_ids: *i64 = a_ids_raw as *i64
94 let b_ids: *i64 = b_ids_raw as *i64
95 let c_ids: *i64 = c_ids_raw as *i64
96
97 // Fill values.
98 pa[0] = 1; pa[1] = 2; pa[2] = 3; pa[3] = 4
99 pb[0] = 5; pb[1] = 6; pb[2] = 7; pb[3] = 8
100
101 // Birth + emit each input bit at L3 (primitive layer).
102 var k: i64 = 0
103 while k < 4 {
104 let aid: i64 = nx_bprov_alloc()
105 a_ids[k] = aid
106 if nx_bprov_emit(aid, 0, 0, NX_BPROV_L_3, TAG_MAGIC_11111) != 0 { return 10 }
107
108 let bid: i64 = nx_bprov_alloc()
109 b_ids[k] = bid
110 if nx_bprov_emit(bid, 0, 0, NX_BPROV_L_3, TAG_MAGIC_22222) != 0 { return 11 }
111 k = k + 1
112 }
113
114 // Matmul with provenance.
115 if nx_matmul_2x2_traced(pa, pb, pc, a_ids, b_ids, c_ids) != 0 { return 20 }
116
117 // Verify values.
118 if pc[0] != 19 { return 21 }
119 if pc[1] != 22 { return 22 }
120 if pc[2] != 43 { return 23 }
121 if pc[3] != 50 { return 24 }
122
123 // Pre-display audit: 8 inputs unjoined + 4 outputs unjoined = 12 zombies.
124 if nx_bprov_audit_zombies() != 12 { return 30 }
125
126 // Display = consumer at L7. Join each output bit.
127 var c: i64 = 0
128 while c < 4 {
129 if nx_bprov_join(c_ids[c], NX_BPROV_L_7, TAG_MAGIC_33333) != 0 { return 40 }
130 c = c + 1
131 }
132
133 // Join each input bit at L3.5 (where matmul consumed it).
134 var i: i64 = 0
135 while i < 4 {
136 if nx_bprov_join(a_ids[i], NX_BPROV_L_35, TAG_MATMUL) != 0 { return 50 }
137 if nx_bprov_join(b_ids[i], NX_BPROV_L_35, TAG_MATMUL) != 0 { return 51 }
138 i = i + 1
139 }
140
141 // Final audit: every bit observed -- silicon-to-death traced.
142 if nx_bprov_audit_zombies() != 0 { return 60 }
143
144 // Lookup verification: output bits land at L7, inputs land at L3.5.
145 if nx_bprov_lookup_join(c_ids[0]) != NX_BPROV_L_7 { return 70 }
146 if nx_bprov_lookup_join(c_ids[3]) != NX_BPROV_L_7 { return 71 }
147 if nx_bprov_lookup_join(a_ids[0]) != NX_BPROV_L_35 { return 72 }
148 if nx_bprov_lookup_join(b_ids[3]) != NX_BPROV_L_35 { return 73 }
149
150 // Total records: 4 a-inputs + 4 b-inputs + 4 c-outputs = 12.
151 if nx_bprov_n_records() != 12 { return 80 }
152
153 return 0
154}