proofs/kernel_weights_certificate.bend
stelliferous@0.0.3.0 · 124 lines · 0 definitions
1import Base
2import stelliferous@0.0.3.0/kernel_weights.bend as Weights
3import stelliferous@0.0.3.0/kernel_tile.bend as Tile
4import stelliferous@0.0.3.0/traversal_array.bend as Traversal
5import stelliferous@0.0.3.0/storage_allocation.bend as Allocation
6import stelliferous@0.0.3.0/tensor.bend as Tensors
7import stelliferous@0.0.3.0/proofs/kernel_weights_witness.bend as WeightsWitness
8import stelliferous@0.0.3.0/proofs/traversal_witness.bend as TraversalWitness
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_allocation_refinement.bend as AllocationLaws
12import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
13
14def family(-input: Array<F32>) -> Data:
15 Witness.ArrayWitness<F32,input>
16
17def block_mapped_with(~Context: Data,~offset: Context -> U32 -> U32,~row_bases: Context -> @+row_stride: U32 -> @+row: U32 -> Weights.Bases,+depth: Nat,+block: U32,+layout: Weights.MappedLayout<Context>,-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_mapped_with(~Context,~offset,~row_bases,block,layout,owners)>:
20 Weights.MappedLayout{+rows,+inner,+row_stride,+context} = 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_mapped_with(~Context,~offset,~row_bases,block,Weights.MappedLayout{rows,inner,row_stride,context},_)>
24 +mapped = {Weights.MappedRows{rows,(block * 8 : U32),(block * inner : U32),context,row_bases(context,row_stride,(block * 8 : U32))} : Weights.MappedRows<Context>}
25 -state = {Traversal.State{input,output,0,mapped} : Traversal.State<&1,&1,Array<F32>,Array<Tile.Tile8>,Weights.MappedRows<Context>>}
26 TraversalWitness.finish(~Array<F32>,~Tile.Tile8,~Weights.MappedRows<Context>,input,depth,
27 Traversal.run(~Array<F32>,~Tile.Tile8,~Weights.MappedRows<Context>,~Weights.read_mapped_rows(~Context,~offset),~Weights.destination_rows(~Context),U32.to_nat(inner),state),
28 TraversalWitness.run(~Array<F32>,~Tile.Tile8,~Weights.MappedRows<Context>,~family,~Weights.read_mapped_rows(~Context,~offset),~Weights.destination_rows(~Context),~WeightsWitness.read_mapped_rows(~Context,~offset),
29 depth,U32.to_nat(inner),input,state,input_evidence,TraversalWitness.StateEvidence{output,0,mapped,{==},output_evidence}))
30
31def traverse_mapped_with(~Context: Data,~offset: Context -> U32 -> U32,~row_bases: Context -> @+row_stride: U32 -> @+row: U32 -> Weights.Bases,+depth: Nat,count: Nat,+index: U32,+layout: Weights.MappedLayout<Context>,-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.MappedLayout<Context>,~Weights.copy_mapped_with(~Context,~offset,~row_bases),count,index,layout,owners)>:
35 match count:
36 case 0n: evidence
37 case 1n+rest:
38 traverse_mapped_with(~Context,~offset,~row_bases,depth,rest,(index + 1 : U32),layout,input,Weights.copy_mapped_with(~Context,~offset,~row_bases,index,layout,owners),input_evidence,
39 block_mapped_with(~Context,~offset,~row_bases,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_mapped_with(~Context: Data,~offset: Context -> U32 -> U32,~row_bases: Context -> @+row_stride: U32 -> @+row: U32 -> Weights.Bases,+rows: U32,+inner: U32,+row_stride: U32,+context: Context,-input: Array<F32>,evidence: Witness.ArrayWitness<F32,input>) ->
53 TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input)>:
54 +blocks = ((rows + 7) / 8 : U32)
55 +depth = Tensors.depth_for((blocks * inner : U32))
56 +layout = {Weights.MappedLayout{rows,inner,row_stride,context} : Weights.MappedLayout<Context>}
57 -output = Allocation.array(~Tile.Tile8,depth,Tile.filled(0.0))
58 traverse_mapped_with(~Context,~offset,~row_bases,depth,U32.to_nat(blocks),0,layout,input,(input,output),evidence,TraversalWitness.ResultEvidence{output,{==},allocated(depth)})
59
60def run_mapped(~Context: Data,~offset: Context -> U32 -> U32,+rows: U32,+inner: U32,+row_stride: U32,+context: Context,-input: Array<F32>,evidence: Witness.ArrayWitness<F32,input>) ->
61 TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.run_mapped(~Context,~offset,rows,inner,row_stride,context,input)>:
62 run_mapped_with(~Context,~offset,~Weights.linear_bases(~Context),rows,inner,row_stride,context,input,evidence)
63
64def run(+rows: U32,+inner: U32,-input: Array<F32>,evidence: Witness.ArrayWitness<F32,input>) ->
65 Witness.Witness(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.run(rows,inner,input)):
66 finish(Tensors.depth_for((((rows + 7) / 8) * inner : U32)),input,Weights.run_mapped(~Unit,~Weights.identity,rows,inner,inner,Unit{},input),
67 run_mapped(~Unit,~Weights.identity,rows,inner,inner,Unit{},input,evidence))
68
69def equation(+rows: U32,+inner: U32,-input: Array<F32>,certificate: Certificate.Certificate<F32,input>) ->
70 {Weights.run(rows,inner,input) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),
71 Tree.reflect(Tile.Tile8,Weights.run(rows,inner,input)))) : Array<Tile.Tile8>}:
72 %Certificate.restored(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.run(rows,inner,input),
73 run(rows,inner,input,Certificate.witness(F32,input,certificate))) :
74 {_ == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),
75 Tree.reflect(Tile.Tile8,Weights.run(rows,inner,input)))) : Array<Tile.Tile8>}
76 {==}
77
78def certificate(+rows: U32,+inner: U32,-input: Array<F32>,certificate: Certificate.Certificate<F32,input>) ->
79 Certificate.Certificate<Tile.Tile8,Weights.run(rows,inner,input)>:
80 Certificate.Certificate{Tensors.depth_for((((rows + 7) / 8) * inner : U32)),equation(rows,inner,input,certificate)}
81
82# The witness traversal occurs only beneath erased owner equations.
83def source_at(+depth: Nat,-input: Array<F32>,-result: Array<F32> & Array<Tile.Tile8>,evidence: TraversalWitness.ResultEvidence<Array<F32>,Tile.Tile8,input,depth,result>) ->
84 {Weights.source(result) == input : Array<F32>}:
85 TraversalWitness.ResultEvidence{output,equation,output_evidence} = evidence
86 Equal.cong(Array<F32> & Array<Tile.Tile8>,Array<F32>,pair => Weights.source(pair),result,(input,output),equation)
87
88def input_equation_with(~Context: Data,~offset: Context -> U32 -> U32,~row_bases: Context -> @+row_stride: U32 -> @+row: U32 -> Weights.Bases,+rows: U32,+inner: U32,+row_stride: U32,+context: Context,-input: Array<F32>,+depth: Nat,
89 equation: {input == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,input))) : Array<F32>}) ->
90 {input == Weights.source(Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input)) : Array<F32>}:
91 %Equal.sym(Array<F32>,Weights.source(Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input)),input,
92 source_at(Tensors.depth_for((((rows + 7) / 8) * inner : U32)),input,Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input),
93 run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input,Witness.ArrayWitness{depth,Certificate.witness_at(F32,depth,input,equation)}))) : {input == _ : Array<F32>}
94 {==}
95
96def retained(-input: Array<F32>,-output: Array<F32>,+depth: Nat,
97 equation: {input == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,input))) : Array<F32>},same: {input == output : Array<F32>}) -> Certificate.Certificate<F32,output>:
98 %same : Certificate.Certificate<F32,_>
99 Certificate.Certificate{depth,equation}
100
101def equation_mapped_with(~Context: Data,~offset: Context -> U32 -> U32,~row_bases: Context -> @+row_stride: U32 -> @+row: U32 -> Weights.Bases,+rows: U32,+inner: U32,+row_stride: U32,+context: Context,-input: Array<F32>,+depth: Nat,
102 equation: {input == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,input))) : Array<F32>}) ->
103 {Weights.reordered(Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input)) == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),
104 Tree.reflect(Tile.Tile8,Weights.reordered(Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input))))) : Array<Tile.Tile8>}:
105 %Certificate.restored(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),Weights.reordered(Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input)),
106 finish(Tensors.depth_for((((rows + 7) / 8) * inner : U32)),input,Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input),
107 run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input,Witness.ArrayWitness{depth,Certificate.witness_at(F32,depth,input,equation)}))) :
108 {_ == Tree.pack(Tile.Tile8,Certificate.normalized(Tile.Tile8,Tensors.depth_for((((rows + 7) / 8) * inner : U32)),
109 Tree.reflect(Tile.Tile8,Weights.reordered(Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input))))) : Array<Tile.Tile8>}
110 {==}
111
112type MappedCertificates<-result: Array<F32> & Array<Tile.Tile8>> is Data:
113 MappedCertificates{source: Certificate.Certificate<F32,Weights.source(result)>,output: Certificate.Certificate<Tile.Tile8,Weights.reordered(result)>}
114
115def certificates_mapped_with(~Context: Data,~offset: Context -> U32 -> U32,~row_bases: Context -> @+row_stride: U32 -> @+row: U32 -> Weights.Bases,+rows: U32,+inner: U32,+row_stride: U32,+context: Context,-input: Array<F32>,certificate: Certificate.Certificate<F32,input>) ->
116 MappedCertificates<Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input)>:
117 Certificate.Certificate{+depth,+equation} = certificate
118 MappedCertificates{retained(input,Weights.source(Weights.run_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input)),depth,equation,
119 input_equation_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input,depth,equation)),
120 Certificate.Certificate{Tensors.depth_for((((rows + 7) / 8) * inner : U32)),equation_mapped_with(~Context,~offset,~row_bases,rows,inner,row_stride,context,input,depth,equation)}}
121
122def certificates_mapped(~Context: Data,~offset: Context -> U32 -> U32,+rows: U32,+inner: U32,+row_stride: U32,+context: Context,-input: Array<F32>,certificate: Certificate.Certificate<F32,input>) ->
123 MappedCertificates<Weights.run_mapped(~Context,~offset,rows,inner,row_stride,context,input)>:
124 certificates_mapped_with(~Context,~offset,~Weights.linear_bases(~Context),rows,inner,row_stride,context,input,certificate)