proofs/kernel_gemm_certificate.bend
stelliferous@0.0.3.0 · 237 lines · 0 definitions
1# Shape evidence follows the real readers and writers. Only the final flat
2# certificate is live; witness traversals occur beneath erased rewrites.
3import Base
4import stelliferous@0.0.3.0/kernel_gemm.bend as Gemm
5import stelliferous@0.0.3.0/kernel_rows.bend as Rows
6import stelliferous@0.0.3.0/kernel_tile.bend as Tile
7import stelliferous@0.0.3.0/traversal_array.bend as Traversal
8import stelliferous@0.0.3.0/traversal_loop.bend as Loop
9import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
10import stelliferous@0.0.3.0/proofs/storage_certificate.bend as Certificate
11import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
12import stelliferous@0.0.3.0/proofs/loop_projection.bend as Projection
13import stelliferous@0.0.3.0/proofs/kernel_read_witness.bend as ReadWitness
14
15def store_lane(+depth: Nat,inside: Bool,-output: Array<F32>,+offset: U32,-value: F32,evidence: Witness.Witness(F32,depth,output)) ->
16 Witness.Witness(F32,depth,Gemm.store_lane(inside,output,offset,value)):
17 match inside:
18 case True{}: Witness.write(F32,depth,output,offset,value,evidence)
19 case False{}: evidence
20
21def store_tail(+count: U32,+depth: Nat,-output: Array<F32>,+offset: U32,-bias: F32,-accumulator: Tile.Tile8,
22 evidence: Witness.Witness(F32,depth,output)) ->
23 Witness.Witness(F32,depth,Gemm.store_tail(True{},count,output,offset,bias,accumulator)):
24 -a = (Tile.lane0(accumulator) + bias : F32)
25 -b = (Tile.lane1(accumulator) + bias : F32)
26 -c = (Tile.lane2(accumulator) + bias : F32)
27 -d = (Tile.lane3(accumulator) + bias : F32)
28 -e = (Tile.lane4(accumulator) + bias : F32)
29 -f = (Tile.lane5(accumulator) + bias : F32)
30 -g = (Tile.lane6(accumulator) + bias : F32)
31 -h = (Tile.lane7(accumulator) + bias : F32)
32 -o1 = Gemm.store_lane(U32.is_lt(0,count),output,offset,a)
33 -o2 = Gemm.store_lane(U32.is_lt(1,count),o1,(offset + 1 : U32),b)
34 -o3 = Gemm.store_lane(U32.is_lt(2,count),o2,(offset + 2 : U32),c)
35 -o4 = Gemm.store_lane(U32.is_lt(3,count),o3,(offset + 3 : U32),d)
36 -o5 = Gemm.store_lane(U32.is_lt(4,count),o4,(offset + 4 : U32),e)
37 -o6 = Gemm.store_lane(U32.is_lt(5,count),o5,(offset + 5 : U32),f)
38 -o7 = Gemm.store_lane(U32.is_lt(6,count),o6,(offset + 6 : U32),g)
39 evidence = store_lane(depth,U32.is_lt(0,count),output,offset,a,evidence)
40 evidence = store_lane(depth,U32.is_lt(1,count),o1,(offset + 1 : U32),b,evidence)
41 evidence = store_lane(depth,U32.is_lt(2,count),o2,(offset + 2 : U32),c,evidence)
42 evidence = store_lane(depth,U32.is_lt(3,count),o3,(offset + 3 : U32),d,evidence)
43 evidence = store_lane(depth,U32.is_lt(4,count),o4,(offset + 4 : U32),e,evidence)
44 evidence = store_lane(depth,U32.is_lt(5,count),o5,(offset + 5 : U32),f,evidence)
45 evidence = store_lane(depth,U32.is_lt(6,count),o6,(offset + 6 : U32),g,evidence)
46 store_lane(depth,U32.is_lt(7,count),o7,(offset + 7 : U32),h,evidence)
47
48type Written<-bias: Array<F32>,-depth: Nat,-result: Array<F32> & Array<F32>> is Data:
49 Written{-output: Array<F32>,equation: {result == (bias,output) : Array<F32> & Array<F32>},balanced: Witness.Witness(F32,depth,output)}
50
51def write_bias(+depth: Nat,-bias: Array<F32>,-output: Array<F32>,+offset: U32,+row: U32,-accumulator: Tile.Tile8,+count: U32,
52 read: Witness.Read<F32,bias,Array.get(F32,bias,row)>,evidence: Witness.Witness(F32,depth,output)) ->
53 Written<bias,depth,Gemm.write_bias(output,offset,accumulator,count,Array.get(F32,bias,row))>:
54 Witness.Read{value,equation} = read
55 Written{Gemm.store_tail(True{},count,output,offset,value,accumulator),
56 %Equal.sym(Array<F32> & F32,Array.get(F32,bias,row),(bias,value),equation) :
57 {Gemm.write_bias(output,offset,accumulator,count,_) == (bias,Gemm.store_tail(True{},count,output,offset,value,accumulator)) : Array<F32> & Array<F32>}
58 {==},store_tail(count,depth,output,offset,value,accumulator,evidence)}
59
60def write_row(+depth: Nat,valid: Bool,+row: U32,+position: U32,+columns: U32,-accumulator: Tile.Tile8,
61 -bias: Array<F32>,-output: Array<F32>,bias_evidence: Witness.ArrayWitness<F32,bias>,evidence: Witness.Witness(F32,depth,output)) ->
62 Written<bias,depth,Gemm.write_row(True{},valid,row,position,columns,accumulator,(bias,output))>:
63 match valid:
64 case False{}: Written{output,{==},evidence}
65 case True{}:
66 write_bias(depth,bias,output,(row * columns + position : U32),row,accumulator,U32.min(8,(columns - position : U32)),Witness.observed(F32,bias,row,bias_evidence),evidence)
67
68def next(+depth: Nat,valid: Bool,row: U32,position: U32,columns: U32,-accumulator: Tile.Tile8,
69 -bias: Array<F32>,-owners: Array<F32> & Array<F32>,bias_evidence: Witness.ArrayWitness<F32,bias>,evidence: Written<bias,depth,owners>) ->
70 Written<bias,depth,Gemm.write_row(True{},valid,row,position,columns,accumulator,owners)>:
71 Written{output,equation,balanced} = evidence
72 %Equal.sym(Array<F32> & Array<F32>,owners,(bias,output),equation) :
73 Written<bias,depth,Gemm.write_row(True{},valid,row,position,columns,accumulator,_)>
74 write_row(depth,valid,row,position,columns,accumulator,bias,output,bias_evidence,balanced)
75
76def write(+depth: Nat,context: Gemm.Context,-accumulators: Rows.Rows<Tile.Tile8>,
77 -bias: Array<F32>,-output: Array<F32>,+bias_evidence: Witness.ArrayWitness<F32,bias>,balanced: Witness.Witness(F32,depth,output)) ->
78 Written<bias,depth,Gemm.write(True{},context,accumulators,bias,output)>:
79 Gemm.Context{+row,+position,+rows,+columns,input_base,weight_base} = context
80 -a = Rows.first(~Tile.Tile8,accumulators)
81 -b = Rows.second(~Tile.Tile8,accumulators)
82 -c = Rows.third(~Tile.Tile8,accumulators)
83 -d = Rows.fourth(~Tile.Tile8,accumulators)
84 evidence = write_row(depth,U32.is_lt(row,rows),row,position,columns,a,bias,output,bias_evidence,balanced)
85 -owners = Gemm.write_row(True{},U32.is_lt(row,rows),row,position,columns,a,(bias,output))
86 evidence = next(depth,U32.is_lt((row + 1 : U32),rows),(row + 1 : U32),position,columns,b,bias,owners,bias_evidence,evidence)
87 -owners = Gemm.write_row(True{},U32.is_lt((row + 1 : U32),rows),(row + 1 : U32),position,columns,b,owners)
88 evidence = next(depth,U32.is_lt((row + 2 : U32),rows),(row + 2 : U32),position,columns,c,bias,owners,bias_evidence,evidence)
89 -owners = Gemm.write_row(True{},U32.is_lt((row + 2 : U32),rows),(row + 2 : U32),position,columns,c,owners)
90 next(depth,U32.is_lt((row + 3 : U32),rows),(row + 3 : U32),position,columns,d,bias,owners,bias_evidence,evidence)
91
92type Evidence<-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-depth: Nat,-state: Gemm.Buffers> is Data:
93 Evidence{-output: Array<F32>,equation: {state == Gemm.Buffers{input,weights,bias,output} : Gemm.Buffers},balanced: Witness.Witness(F32,depth,output)}
94
95def after_write(-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-depth: Nat,-written: Array<F32> & Array<F32>,
96 evidence: Written<bias,depth,written>) -> Evidence<input,weights,bias,depth,Gemm.after_write(input,weights,written)>:
97 Written{output,equation,balanced} = evidence
98 Evidence{output,
99 %Equal.sym(Array<F32> & Array<F32>,written,(bias,output),equation) :
100 {Gemm.after_write(input,weights,_) == Gemm.Buffers{input,weights,bias,output} : Gemm.Buffers}
101 {==},balanced}
102
103# The final step stores into the owners the loop returned unchanged.
104def finished(+depth: Nat,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,-state: Gemm.Loop,
105 +bias_evidence: Witness.ArrayWitness<F32,bias>,balanced: Witness.Witness(F32,depth,output),
106 evidence: ReadWitness.Looped<input,weights,bias,output,state>) -> Evidence<input,weights,bias,depth,Gemm.finish(~True{},state)>:
107 ReadWitness.Looped{index,context,accumulators,equation} = evidence
108 %Equal.sym(Gemm.Loop,state,Gemm.Loop{input,weights,bias,output,index,context,accumulators},equation) :
109 Evidence<input,weights,bias,depth,Gemm.finish(~True{},_)>
110 after_write(input,weights,bias,depth,Gemm.write(True{},context,accumulators,bias,output),
111 write(depth,context,accumulators,bias,output,bias_evidence,balanced))
112
113def reduced(~upper: Bool,+depth: Nat,+count: Nat,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,-state: Gemm.Loop,
114 +input_evidence: Witness.ArrayWitness<Tile.Tile8,input>,+weight_evidence: Witness.ArrayWitness<Tile.Tile8,weights>,
115 +bias_evidence: Witness.ArrayWitness<F32,bias>,balanced: Witness.Witness(F32,depth,output),evidence: ReadWitness.Looped<input,weights,bias,output,state>) ->
116 Evidence<input,weights,bias,depth,Loop.run_then(~Gemm.Loop,~Gemm.Buffers,~Gemm.step(~upper),~Gemm.finish(~True{}),count,state)>:
117 %Equal.sym(Gemm.Buffers,Loop.run_then(~Gemm.Loop,~Gemm.Buffers,~Gemm.step(~upper),~Gemm.finish(~True{}),count,state),
118 Gemm.finish(~True{},Loop.run(~Gemm.Loop,~Gemm.step(~upper),count,state)),
119 Projection.run_then_finishes(~Gemm.Loop,~Gemm.Buffers,~Gemm.step(~upper),~Gemm.finish(~True{}),count,state)) :
120 Evidence<input,weights,bias,depth,_>
121 finished(depth,input,weights,bias,output,Loop.run(~Gemm.Loop,~Gemm.step(~upper),count,state),bias_evidence,balanced,
122 ReadWitness.run(~upper,count,input,weights,bias,output,state,input_evidence,weight_evidence,evidence))
123
124def reduce(upper: Bool,+depth: Nat,+count: Nat,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,+context: Gemm.Context,
125 +input_evidence: Witness.ArrayWitness<Tile.Tile8,input>,+weight_evidence: Witness.ArrayWitness<Tile.Tile8,weights>,
126 +bias_evidence: Witness.ArrayWitness<F32,bias>,balanced: Witness.Witness(F32,depth,output)) ->
127 Evidence<input,weights,bias,depth,Gemm.reduce(~True{},upper,count,Gemm.Loop{input,weights,bias,output,0,context,Rows.filled(~Tile.Tile8,Tile.filled(0.0))})>:
128 match upper:
129 case False{}:
130 reduced(~False{},depth,count,input,weights,bias,output,Gemm.Loop{input,weights,bias,output,0,context,Rows.filled(~Tile.Tile8,Tile.filled(0.0))},
131 input_evidence,weight_evidence,bias_evidence,balanced,ReadWitness.Looped{0,context,Rows.filled(~Tile.Tile8,Tile.filled(0.0)),{==}})
132 case True{}:
133 reduced(~True{},depth,count,input,weights,bias,output,Gemm.Loop{input,weights,bias,output,0,context,Rows.filled(~Tile.Tile8,Tile.filled(0.0))},
134 input_evidence,weight_evidence,bias_evidence,balanced,ReadWitness.Looped{0,context,Rows.filled(~Tile.Tile8,Tile.filled(0.0)),{==}})
135
136def execute(+depth: Nat,job: Gemm.Job,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-state: Gemm.Buffers,
137 +input_evidence: Witness.ArrayWitness<Tile.Tile8,input>,+weight_evidence: Witness.ArrayWitness<Tile.Tile8,weights>,+bias_evidence: Witness.ArrayWitness<F32,bias>,
138 evidence: Evidence<input,weights,bias,depth,state>) -> Evidence<input,weights,bias,depth,Gemm.execute(~True{},job,state)>:
139 Gemm.Job{+context,+upper,+count} = job
140 Evidence{output,equation,balanced} = evidence
141 %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,output},equation) :
142 Evidence<input,weights,bias,depth,Gemm.execute(~True{},Gemm.Job{context,upper,count},_)>
143 reduce(upper,depth,count,input,weights,bias,output,context,input_evidence,weight_evidence,bias_evidence,balanced)
144
145def traverse(+depth: Nat,count: Nat,+index: U32,+layout: Gemm.Layout,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-state: Gemm.Buffers,
146 +input_evidence: Witness.ArrayWitness<Tile.Tile8,input>,+weight_evidence: Witness.ArrayWitness<Tile.Tile8,weights>,+bias_evidence: Witness.ArrayWitness<F32,bias>,
147 evidence: Evidence<input,weights,bias,depth,state>) ->
148 Evidence<input,weights,bias,depth,Traversal.indexed_fold(~Gemm.Buffers,~Gemm.Layout,~Gemm.step_job(~True{}),count,index,layout,state)>:
149 match count:
150 case 0n: evidence
151 case 1n+rest:
152 traverse(depth,rest,(index + 1 : U32),layout,input,weights,bias,Gemm.step_job(~True{},index,layout,state),input_evidence,weight_evidence,bias_evidence,
153 execute(depth,Gemm.job(layout,index),input,weights,bias,state,input_evidence,weight_evidence,bias_evidence,evidence))
154
155def finish(-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-depth: Nat,-state: Gemm.Buffers,
156 evidence: Evidence<input,weights,bias,depth,state>) -> Witness.Witness(F32,depth,Gemm.result(state)):
157 Evidence{output,equation,balanced} = evidence
158 %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,output},equation) : Witness.Witness(F32,depth,Gemm.result(_))
159 balanced
160
161def run(+depth: Nat,+rows: U32,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,+columns: U32,+inner: U32,+start: U32,+output_columns: U32,
162 input_evidence: Witness.ArrayWitness<Tile.Tile8,input>,weight_evidence: Witness.ArrayWitness<Tile.Tile8,weights>,bias_evidence: Witness.ArrayWitness<F32,bias>,
163 balanced: Witness.Witness(F32,depth,output)) -> Witness.Witness(F32,depth,Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)):
164 +count = U32.to_nat(Gemm.job_count(rows,columns))
165 +layout = {Gemm.Layout{rows,columns,inner,start,output_columns} : Gemm.Layout}
166 -state = {Gemm.Buffers{input,weights,bias,output} : Gemm.Buffers}
167 finish(input,weights,bias,depth,Traversal.indexed_fold(~Gemm.Buffers,~Gemm.Layout,~Gemm.step_job(~True{}),count,0,layout,state),
168 traverse(depth,count,0,layout,input,weights,bias,state,input_evidence,weight_evidence,bias_evidence,Evidence{output,{==},balanced}))
169
170def equation(+depth: Nat,+rows: U32,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,+columns: U32,+inner: U32,+start: U32,+output_columns: U32,
171 input_certificate: Certificate.Certificate<Tile.Tile8,input>,weight_certificate: Certificate.Certificate<Tile.Tile8,weights>,bias_certificate: Certificate.Certificate<F32,bias>,
172 balanced: {output == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,output))) : Array<F32>}) ->
173 {Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns) ==
174 Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)))) : Array<F32>}:
175 %Certificate.restored(F32,depth,Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns),
176 run(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,Certificate.witness(Tile.Tile8,input,input_certificate),
177 Certificate.witness(Tile.Tile8,weights,weight_certificate),Certificate.witness(F32,bias,bias_certificate),Certificate.witness_at(F32,depth,output,balanced))) :
178 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)))) : Array<F32>}
179 {==}
180
181def certificate(rows: U32,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,columns: U32,inner: U32,start: U32,output_columns: U32,
182 input_certificate: Certificate.Certificate<Tile.Tile8,input>,weight_certificate: Certificate.Certificate<Tile.Tile8,weights>,bias_certificate: Certificate.Certificate<F32,bias>,
183 output_certificate: Certificate.Certificate<F32,output>) -> Certificate.Certificate<F32,Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)>:
184 Certificate.Certificate{+depth,balanced} = output_certificate
185 Certificate.Certificate{depth,equation(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,input_certificate,weight_certificate,bias_certificate,balanced)}
186
187# The fold gives back the three buffers it only reads, next to the output of run.
188def kept_state(-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-depth: Nat,-state: Gemm.Buffers,
189 evidence: Evidence<input,weights,bias,depth,state>) -> {state == Gemm.Buffers{input,weights,bias,Gemm.result(state)} : Gemm.Buffers}:
190 Evidence{output,equation,balanced} = evidence
191 %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,output},equation) :
192 {_ == Gemm.Buffers{input,weights,bias,Gemm.result(_)} : Gemm.Buffers}
193 {==}
194
195def kept_equation(+depth: Nat,+rows: U32,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,+columns: U32,+inner: U32,+start: U32,+output_columns: U32,
196 input_evidence: Witness.ArrayWitness<Tile.Tile8,input>,weight_evidence: Witness.ArrayWitness<Tile.Tile8,weights>,bias_evidence: Witness.ArrayWitness<F32,bias>,
197 balanced: Witness.Witness(F32,depth,output)) ->
198 {Gemm.run_keeping(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns) ==
199 Gemm.Buffers{input,weights,bias,Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)} : Gemm.Buffers}:
200 +count = U32.to_nat(Gemm.job_count(rows,columns))
201 +layout = {Gemm.Layout{rows,columns,inner,start,output_columns} : Gemm.Layout}
202 -state = {Gemm.Buffers{input,weights,bias,output} : Gemm.Buffers}
203 kept_state(input,weights,bias,depth,Traversal.indexed_fold(~Gemm.Buffers,~Gemm.Layout,~Gemm.step_job(~True{}),count,0,layout,state),
204 traverse(depth,count,0,layout,input,weights,bias,state,input_evidence,weight_evidence,bias_evidence,Evidence{output,{==},balanced}))
205
206type Kept<-state: Gemm.Buffers> is Data:
207 Kept{input: Certificate.Certificate<Tile.Tile8,Gemm.kept_input(state)>,weights: Certificate.Certificate<Tile.Tile8,Gemm.kept_weights(state)>,
208 bias: Certificate.Certificate<F32,Gemm.kept_bias(state)>,output: Certificate.Certificate<F32,Gemm.result(state)>}
209
210# The certificates of the read-only buffers are the ones that came in.
211def kept(+rows: U32,-input: Array<Tile.Tile8>,-weights: Array<Tile.Tile8>,-bias: Array<F32>,-output: Array<F32>,+columns: U32,+inner: U32,+start: U32,+output_columns: U32,
212 input_certificate: Certificate.Certificate<Tile.Tile8,input>,weight_certificate: Certificate.Certificate<Tile.Tile8,weights>,bias_certificate: Certificate.Certificate<F32,bias>,
213 output_certificate: Certificate.Certificate<F32,output>) -> Kept<Gemm.run_keeping(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)>:
214 Certificate.Certificate{+input_depth,+input_equation} = input_certificate
215 Certificate.Certificate{+weight_depth,+weight_equation} = weight_certificate
216 Certificate.Certificate{+bias_depth,+bias_equation} = bias_certificate
217 Certificate.Certificate{+depth,+balanced} = output_certificate
218 -state = Gemm.run_keeping(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)
219 -result = Gemm.run_at(~True{},rows,input,weights,bias,output,columns,inner,start,output_columns)
220 +owners = kept_equation(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,
221 Certificate.witness(Tile.Tile8,input,Certificate.Certificate{input_depth,input_equation}),Certificate.witness(Tile.Tile8,weights,Certificate.Certificate{weight_depth,weight_equation}),
222 Certificate.witness(F32,bias,Certificate.Certificate{bias_depth,bias_equation}),Certificate.witness_at(F32,depth,output,balanced))
223 Kept{
224 Certificate.Certificate{input_depth,
225 %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
226 {Gemm.kept_input(_) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,input_depth,Tree.reflect(Tile.Tile8,Gemm.kept_input(_)))) : Array<Tile.Tile8>}
227 input_equation},
228 Certificate.Certificate{weight_depth,
229 %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
230 {Gemm.kept_weights(_) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,weight_depth,Tree.reflect(Tile.Tile8,Gemm.kept_weights(_)))) : Array<Tile.Tile8>}
231 weight_equation},
232 Certificate.Certificate{bias_depth,
233 %Equal.sym(Gemm.Buffers,state,Gemm.Buffers{input,weights,bias,result},owners) :
234 {Gemm.kept_bias(_) == Tree.pack(F32,Certificate.normalized(F32,bias_depth,Tree.reflect(F32,Gemm.kept_bias(_)))) : Array<F32>}
235 bias_equation},
236 Certificate.Certificate{depth,equation(depth,rows,input,weights,bias,output,columns,inner,start,output_columns,Certificate.Certificate{input_depth,input_equation},
237 Certificate.Certificate{weight_depth,weight_equation},Certificate.Certificate{bias_depth,bias_equation},balanced)}}