1 import Base 2 import ../kernel_weights.bend as Weights 3 import ../kernel_tile.bend as Tile 4 import ../storage_buffer.bend as Storage 5 import ./storage_witness.bend as Witness 6 import ./traversal_witness.bend as TraversalWitness 7 8 # Missing rows are zero-filled without changing the source owner. 9 def conditional(-input: Array,valid: Bool,+index: U32,evidence: Witness.ArrayWitness) -> 10 TraversalWitness.Sample,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 15 def eighth(-input: Array,-a: F32,-b: F32,-c: F32,-d: F32,-e: F32,-f: F32,-g: F32,-result: Array & F32, 16 observed: TraversalWitness.Sample,F32,input,result>) -> 17 TraversalWitness.Sample,Tile.Tile8,input,Weights.eighth(a,b,c,d,e,f,g,result)>: 18 TraversalWitness.Sample{h,equation} = observed 19 %Equal.sym(Array & F32,result,(input,h),equation) : 20 TraversalWitness.Sample,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 23 def seventh_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array,-a: F32,-b: F32,-c: F32,-d: F32,-e: F32,-f: F32,-result: Array & F32, 24 observed: TraversalWitness.Sample,F32,input,result>,evidence: Witness.ArrayWitness) -> 25 TraversalWitness.Sample,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,result,(input,g),equation) : 28 TraversalWitness.Sample,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 32 def sixth_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array,-a: F32,-b: F32,-c: F32,-d: F32,-e: F32,-result: Array & F32, 33 observed: TraversalWitness.Sample,F32,input,result>,+evidence: Witness.ArrayWitness) -> 34 TraversalWitness.Sample,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,result,(input,f),equation) : 37 TraversalWitness.Sample,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 41 def fifth_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array,-a: F32,-b: F32,-c: F32,-d: F32,-result: Array & F32, 42 observed: TraversalWitness.Sample,F32,input,result>,+evidence: Witness.ArrayWitness) -> 43 TraversalWitness.Sample,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,result,(input,e),equation) : 46 TraversalWitness.Sample,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 50 def fourth_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array,-a: F32,-b: F32,-c: F32,-result: Array & F32, 51 observed: TraversalWitness.Sample,F32,input,result>,+evidence: Witness.ArrayWitness) -> 52 TraversalWitness.Sample,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,result,(input,d),equation) : 55 TraversalWitness.Sample,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 59 def third_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array,-a: F32,-b: F32,-result: Array & F32, 60 observed: TraversalWitness.Sample,F32,input,result>,+evidence: Witness.ArrayWitness) -> 61 TraversalWitness.Sample,Tile.Tile8,input,Weights.third_rows(rows,row,index,bases,a,b,result)>: 62 TraversalWitness.Sample{c,equation} = observed 63 %Equal.sym(Array & F32,result,(input,c),equation) : 64 TraversalWitness.Sample,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 68 def second_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array,-a: F32,-result: Array & F32, 69 observed: TraversalWitness.Sample,F32,input,result>,+evidence: Witness.ArrayWitness) -> 70 TraversalWitness.Sample,Tile.Tile8,input,Weights.second_rows(rows,row,index,bases,a,result)>: 71 TraversalWitness.Sample{b,equation} = observed 72 %Equal.sym(Array & F32,result,(input,b),equation) : 73 TraversalWitness.Sample,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 77 def first_rows(+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,-input: Array,-result: Array & F32, 78 observed: TraversalWitness.Sample,F32,input,result>,+evidence: Witness.ArrayWitness) -> 79 TraversalWitness.Sample,Tile.Tile8,input,Weights.first_rows(rows,row,index,bases,result)>: 80 TraversalWitness.Sample{a,equation} = observed 81 %Equal.sym(Array & F32,result,(input,a),equation) : 82 TraversalWitness.Sample,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 86 def read_rows(-input: Array,+rows: U32,+row: U32,+index: U32,+bases: Weights.Bases,+evidence: Witness.ArrayWitness) -> 87 TraversalWitness.Sample,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 91 def read_mapped_rows(~Context: Data,~offset: Context -> U32 -> U32,-input: Array,context: Weights.MappedRows,index: U32, 92 evidence: Witness.ArrayWitness) -> 93 TraversalWitness.Sample,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)