proofs/kernel_weights_witness.bend
stelliferous@0.0.3.0 · 95 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/storage_buffer.bend as Storage
5import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
6import stelliferous@0.0.3.0/proofs/traversal_witness.bend as TraversalWitness
7
8# Missing rows are zero-filled without changing the source owner.
9def conditional(-input: Array<F32>,valid: Bool,+index: U32,evidence: Witness.ArrayWitness<F32,input>) ->
10 TraversalWitness.Sample<Array<F32>,F32,input,Storage.read_when(~F32,0.0,valid,input,index)>:
11 match valid:
12 case False{}: TraversalWitness.Sample{0.0,{==}}
13 case True{}: TraversalWitness.array_sample(~F32,input,Array.get(F32,input,index),Witness.observed(F32,input,index,evidence))
14
15def eighth(-input: Array<F32>,-a: F32,-b: F32,-c: F32,-d: F32,-e: F32,-f: F32,-g: F32,-result: Array<F32> & F32,
16 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>) ->
17 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.eighth(a,b,c,d,e,f,g,result)>:
18 TraversalWitness.Sample{h,equation} = observed
19 %Equal.sym(Array<F32> & F32,result,(input,h),equation) :
20 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.eighth(a,b,c,d,e,f,g,_)>
21 TraversalWitness.Sample{Tile.Tile{a,b,c,d,e,f,g,h},{==}}
22
23def seventh_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array<F32>,-a: F32,-b: F32,-c: F32,-d: F32,-e: F32,-f: F32,-result: Array<F32> & F32,
24 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>,evidence: Witness.ArrayWitness<F32,input>) ->
25 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.seventh_rows(rows,row,index,bases,a,b,c,d,e,f,result)>:
26 TraversalWitness.Sample{g,equation} = observed
27 %Equal.sym(Array<F32> & F32,result,(input,g),equation) :
28 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.seventh_rows(rows,row,index,bases,a,b,c,d,e,f,_)>
29 eighth(input,a,b,c,d,e,f,g,Storage.read_when(~F32,0.0,U32.is_lt((row + 7 : U32),rows),input,(Weights.base7(bases) + index : U32)),
30 conditional(input,U32.is_lt((row + 7 : U32),rows),(Weights.base7(bases) + index : U32),evidence))
31
32def sixth_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array<F32>,-a: F32,-b: F32,-c: F32,-d: F32,-e: F32,-result: Array<F32> & F32,
33 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>,+evidence: Witness.ArrayWitness<F32,input>) ->
34 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.sixth_rows(rows,row,index,bases,a,b,c,d,e,result)>:
35 TraversalWitness.Sample{f,equation} = observed
36 %Equal.sym(Array<F32> & F32,result,(input,f),equation) :
37 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.sixth_rows(rows,row,index,bases,a,b,c,d,e,_)>
38 seventh_rows(rows,row,index,bases,input,a,b,c,d,e,f,Storage.read_when(~F32,0.0,U32.is_lt((row + 6 : U32),rows),input,(Weights.base6(bases) + index : U32)),
39 conditional(input,U32.is_lt((row + 6 : U32),rows),(Weights.base6(bases) + index : U32),evidence),evidence)
40
41def fifth_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array<F32>,-a: F32,-b: F32,-c: F32,-d: F32,-result: Array<F32> & F32,
42 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>,+evidence: Witness.ArrayWitness<F32,input>) ->
43 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.fifth_rows(rows,row,index,bases,a,b,c,d,result)>:
44 TraversalWitness.Sample{e,equation} = observed
45 %Equal.sym(Array<F32> & F32,result,(input,e),equation) :
46 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.fifth_rows(rows,row,index,bases,a,b,c,d,_)>
47 sixth_rows(rows,row,index,bases,input,a,b,c,d,e,Storage.read_when(~F32,0.0,U32.is_lt((row + 5 : U32),rows),input,(Weights.base5(bases) + index : U32)),
48 conditional(input,U32.is_lt((row + 5 : U32),rows),(Weights.base5(bases) + index : U32),evidence),evidence)
49
50def fourth_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array<F32>,-a: F32,-b: F32,-c: F32,-result: Array<F32> & F32,
51 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>,+evidence: Witness.ArrayWitness<F32,input>) ->
52 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.fourth_rows(rows,row,index,bases,a,b,c,result)>:
53 TraversalWitness.Sample{d,equation} = observed
54 %Equal.sym(Array<F32> & F32,result,(input,d),equation) :
55 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.fourth_rows(rows,row,index,bases,a,b,c,_)>
56 fifth_rows(rows,row,index,bases,input,a,b,c,d,Storage.read_when(~F32,0.0,U32.is_lt((row + 4 : U32),rows),input,(Weights.base4(bases) + index : U32)),
57 conditional(input,U32.is_lt((row + 4 : U32),rows),(Weights.base4(bases) + index : U32),evidence),evidence)
58
59def third_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array<F32>,-a: F32,-b: F32,-result: Array<F32> & F32,
60 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>,+evidence: Witness.ArrayWitness<F32,input>) ->
61 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.third_rows(rows,row,index,bases,a,b,result)>:
62 TraversalWitness.Sample{c,equation} = observed
63 %Equal.sym(Array<F32> & F32,result,(input,c),equation) :
64 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.third_rows(rows,row,index,bases,a,b,_)>
65 fourth_rows(rows,row,index,bases,input,a,b,c,Storage.read_when(~F32,0.0,U32.is_lt((row + 3 : U32),rows),input,(Weights.base3(bases) + index : U32)),
66 conditional(input,U32.is_lt((row + 3 : U32),rows),(Weights.base3(bases) + index : U32),evidence),evidence)
67
68def second_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array<F32>,-a: F32,-result: Array<F32> & F32,
69 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>,+evidence: Witness.ArrayWitness<F32,input>) ->
70 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.second_rows(rows,row,index,bases,a,result)>:
71 TraversalWitness.Sample{b,equation} = observed
72 %Equal.sym(Array<F32> & F32,result,(input,b),equation) :
73 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.second_rows(rows,row,index,bases,a,_)>
74 third_rows(rows,row,index,bases,input,a,b,Storage.read_when(~F32,0.0,U32.is_lt((row + 2 : U32),rows),input,(Weights.base2(bases) + index : U32)),
75 conditional(input,U32.is_lt((row + 2 : U32),rows),(Weights.base2(bases) + index : U32),evidence),evidence)
76
77def first_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array<F32>,-result: Array<F32> & F32,
78 observed: TraversalWitness.Sample<Array<F32>,F32,input,result>,+evidence: Witness.ArrayWitness<F32,input>) ->
79 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.first_rows(rows,row,index,bases,result)>:
80 TraversalWitness.Sample{a,equation} = observed
81 %Equal.sym(Array<F32> & F32,result,(input,a),equation) :
82 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.first_rows(rows,row,index,bases,_)>
83 second_rows(rows,row,index,bases,input,a,Storage.read_when(~F32,0.0,U32.is_lt((row + 1 : U32),rows),input,(Weights.base1(bases) + index : U32)),
84 conditional(input,U32.is_lt((row + 1 : U32),rows),(Weights.base1(bases) + index : U32),evidence),evidence)
85
86def read_rows(-input: Array<F32>,+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,+evidence: Witness.ArrayWitness<F32,input>) ->
87 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.read_rows(input,rows,row,index,bases)>:
88 first_rows(rows,row,index,bases,input,Storage.read_when(~F32,0.0,U32.is_lt(row,rows),input,(Weights.base0(bases) + index : U32)),
89 conditional(input,U32.is_lt(row,rows),(Weights.base0(bases) + index : U32),evidence),evidence)
90
91def read_mapped_rows(~Context: Data,~offset: Context -> U32 -> U32,-input: Array<F32>,context: Weights.MappedRows<Context>,index: U32,
92 evidence: Witness.ArrayWitness<F32,input>) ->
93 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.read_mapped_rows(~Context,~offset,input,context,index)>:
94 Weights.MappedRows{rows,row,destination,context,bases} = context
95 read_rows(input,rows,row,offset(context,index),bases,evidence)