proofs/kernel_weights_certificate.bend
stelliferous@0.0.2.0 · 72 lines · 8 definitions
1import Base
2import stelliferous@0.0.2.0/kernel_weights.bend as Weights
3import stelliferous@0.0.2.0/kernel_tile.bend as Tile
4import stelliferous@0.0.2.0/traversal_array.bend as Traversal
5import stelliferous@0.0.2.0/storage_allocation.bend as Allocation
6import stelliferous@0.0.2.0/tensor.bend as Tensors
7import stelliferous@0.0.2.0/proofs/kernel_weights_witness.bend as WeightsWitness
8import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
9import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
10import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
11import stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend as AllocationLaws
12import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
13
14def family(-input: Array<F32>) -> Data:
15 Witness.ArrayWitness<F32,input>
16
17def 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
31def 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
41def 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
47def 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
52def 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
61def 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
70def 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)}