1	import Base
2	import ../kernel_weights.bend as Weights
3	import ../kernel_tile.bend as Tile
4	import ../traversal_array.bend as Traversal
5	import ../storage_allocation.bend as Allocation
6	import ../tensor.bend as Tensors
7	import ./kernel_weights_witness.bend as WeightsWitness
8	import ./traversal_witness.bend as TraversalWitness
9	import ./storage_witness.bend as Witness
10	import ./storage_certificate.bend as Certificate
11	import ./storage_allocation_refinement.bend as AllocationLaws
12	import ./storage_tree_model.bend as Tree
13	
14	def family(-input: Array<F32>) -> Data:
15	  Witness.ArrayWitness<F32,input>
16	
17	def block(+depth: Nat,+block: U32,+layout: Weights.Layout,-input: Array<F32>,-owners: Array<F32> & Array<Tile.Tile8>,
18	  input_evidence: Witness.ArrayWitness<F32,input>,evidence: TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,owners>) ->
19	  TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,Weights.copy_block(block,layout,owners)>:
20	  Weights.Layout{+rows,+inner} = layout
21	  TraversalWitness.ResultEvidence{output,equation,output_evidence} = evidence
22	  %Equal.sym(Array<F32> & Array<Tile.Tile8>,owners,(input,output),equation) :
23	    TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,Weights.copy_block(block,Weights.Layout{rows,inner},_)>
24	  +context = {Weights.Context{rows,inner,(block * 8 : U32),(block * inner : U32)} : Weights.Context}
25	  -state = {Traversal.State{input,output,0,context} : Traversal.State<&1,&1,Array<F32>,Array<Tile.Tile8>,Weights.Context>}
26	  TraversalWitness.finish(~Array<F32>,~Tile.Tile8,~Weights.Context,input,depth,
27	    Traversal.run(~Array<F32>,~Tile.Tile8,~Weights.Context,~Weights.read,~Weights.destination,U32.to_nat(inner),state),
28	    TraversalWitness.run(~Array<F32>,~Tile.Tile8,~Weights.Context,~family,~Weights.read,~Weights.destination,~WeightsWitness.read,
29	      depth,U32.to_nat(inner),input,state,input_evidence,TraversalWitness.StateEvidence{output,0,context,{==},output_evidence}))
30	
31	def traverse(+depth: Nat,count: Nat,+index: U32,+layout: Weights.Layout,-input: Array<F32>,-owners: Array<F32> & Array<Tile.Tile8>,
32	  +input_evidence: Witness.ArrayWitness<F32,input>,evidence: TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,owners>) ->
33	  TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,
34	    Traversal.indexed_fold(~(Array<F32> & Array<Tile.Tile8>),~Weights.Layout,~Weights.copy_block,count,index,layout,owners)>:
35	  match count:
36	    case 0n: evidence
37	    case 1n+rest:
38	      traverse(depth,rest,(index + 1 : U32),layout,input,Weights.copy_block(index,layout,owners),input_evidence,
39	        block(depth,index,layout,input,owners,input_evidence,evidence))
40	
41	def finish(-depth: Nat,-input: Array<F32>,-owners: Array<F32> & Array<Tile.Tile8>,
42	  evidence: TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,owners>) -> Witness.Witness(Tile.Tile8,depth,Weights.reordered(owners)):
43	  TraversalWitness.ResultEvidence{output,equation,output_evidence} = evidence
44	  %Equal.sym(Array<F32> & Array<Tile.Tile8>,owners,(input,output),equation) : Witness.Witness(Tile.Tile8,depth,Weights.reordered(_))
45	  output_evidence
46	
47	def allocated(+depth: Nat) -> Witness.Witness(Tile.Tile8,depth,Allocation.array(~Tile.Tile8,depth,Tile.filled(0.0))):
48	  %Equal.sym(Array<Tile.Tile8>,Allocation.array(~Tile.Tile8,depth,Tile.filled(0.0)),Array.new(Tile.Tile8,depth,Tile.filled(0.0)),
49	    AllocationLaws.array_same(Tile.Tile8,depth,Tile.filled(0.0))) : Witness.Witness(Tile.Tile8,depth,_)
50	  Witness.fresh(Tile.Tile8,depth,Tile.filled(0.0))
51	
52	def run(+rows: U32,+inner: U32,-input: Array<F32>,evidence: Witness.ArrayWitness<F32,input>) ->
53	  Witness.Witness(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.run(rows,inner,input)):
54	  +blocks = ((rows + 7) / 8 : U32)
55	  +depth = Tensors.depth_for((blocks * inner : U32))
56	  +layout = {Weights.Layout{rows,inner} : Weights.Layout}
57	  -output = Allocation.array(~Tile.Tile8,depth,Tile.filled(0.0))
58	  finish(depth,input,Traversal.indexed_fold(~(Array<F32> & Array<Tile.Tile8>),~Weights.Layout,~Weights.copy_block,U32.to_nat(blocks),0,layout,(input,output)),
59	    traverse(depth,U32.to_nat(blocks),0,layout,input,(input,output),evidence,TraversalWitness.ResultEvidence{output,{==},allocated(depth)}))
60	
61	def equation(+rows: U32,+inner: U32,-input: Array<F32>,certificate: Certificate.Certificate<F32,input>) ->
62	  {Weights.run(rows,inner,input) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),
63	    Tree.reflect(Tile.Tile8,Weights.run(rows,inner,input)))) : Array<Tile.Tile8>}:
64	  %Certificate.restored(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.run(rows,inner,input),
65	    run(rows,inner,input,Certificate.witness(F32,input,certificate))) :
66	    {_ == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),
67	      Tree.reflect(Tile.Tile8,Weights.run(rows,inner,input)))) : Array<Tile.Tile8>}
68	  {==}
69	
70	def certificate(+rows: U32,+inner: U32,-input: Array<F32>,certificate: Certificate.Certificate<F32,input>) ->
71	  Certificate.Certificate<Tile.Tile8,Weights.run(rows,inner,input)>:
72	  Certificate.Certificate{Tensors.depth_for((((rows + 7) / 8) * inner : U32)),equation(rows,inner,input,certificate)}