proofs/kernel_weights_witness.bend
stelliferous@0.0.2.0 · 92 lines · 10 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/storage_buffer.bend as Storage
5import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
6import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
7
8
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: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,inner,row,index,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,((row + 7) * inner + index : U32)),
30 conditional(input,U32.is_lt((row + 7 : U32),rows),((row + 7) * inner + index : U32),evidence))
31
32def sixth(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,inner,row,index,a,b,c,d,e,_)>
38 seventh(rows,inner,row,index,input,a,b,c,d,e,f,Storage.read_when(~F32,0.0,U32.is_lt((row + 6 : U32),rows),input,((row + 6) * inner + index : U32)),
39 conditional(input,U32.is_lt((row + 6 : U32),rows),((row + 6) * inner + index : U32),evidence),evidence)
40
41def fifth(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,inner,row,index,a,b,c,d,_)>
47 sixth(rows,inner,row,index,input,a,b,c,d,e,Storage.read_when(~F32,0.0,U32.is_lt((row + 5 : U32),rows),input,((row + 5) * inner + index : U32)),
48 conditional(input,U32.is_lt((row + 5 : U32),rows),((row + 5) * inner + index : U32),evidence),evidence)
49
50def fourth(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,inner,row,index,a,b,c,_)>
56 fifth(rows,inner,row,index,input,a,b,c,d,Storage.read_when(~F32,0.0,U32.is_lt((row + 4 : U32),rows),input,((row + 4) * inner + index : U32)),
57 conditional(input,U32.is_lt((row + 4 : U32),rows),((row + 4) * inner + index : U32),evidence),evidence)
58
59def third(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,inner,row,index,a,b,_)>
65 fourth(rows,inner,row,index,input,a,b,c,Storage.read_when(~F32,0.0,U32.is_lt((row + 3 : U32),rows),input,((row + 3) * inner + index : U32)),
66 conditional(input,U32.is_lt((row + 3 : U32),rows),((row + 3) * inner + index : U32),evidence),evidence)
67
68def second(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,inner,row,index,a,_)>
74 third(rows,inner,row,index,input,a,b,Storage.read_when(~F32,0.0,U32.is_lt((row + 2 : U32),rows),input,((row + 2) * inner + index : U32)),
75 conditional(input,U32.is_lt((row + 2 : U32),rows),((row + 2) * inner + index : U32),evidence),evidence)
76
77def first(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,inner,row,index,_)>
83 second(rows,inner,row,index,input,a,Storage.read_when(~F32,0.0,U32.is_lt((row + 1 : U32),rows),input,((row + 1) * inner + index : U32)),
84 conditional(input,U32.is_lt((row + 1 : U32),rows),((row + 1) * inner + index : U32),evidence),evidence)
85
86def read(-input: Array<F32>,context: Weights.Context,index: U32,evidence: Witness.ArrayWitness<F32,input>) ->
87 TraversalWitness.Sample<Array<F32>,Tile.Tile8,input,Weights.read(input,context,index)>:
88 Weights.Context{+rows,+inner,+row,destination} = context
89 +index = index
90 +evidence = evidence
91 first(rows,inner,row,index,input,Storage.read_when(~F32,0.0,U32.is_lt(row,rows),input,(row * inner + index : U32)),
92 conditional(input,U32.is_lt(row,rows),(row * inner + index : U32),evidence),evidence)