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: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,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 32 def sixth(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,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 41 def fifth(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,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 50 def fourth(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,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 59 def third(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,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 68 def second(+rows: U32,+inner: U32,+row: U32,+index: U32,-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,inner,row,index,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,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 77 def first(+rows: U32,+inner: U32,+row: U32,+index: U32,-input: Array,-result: Array & F32, 78 observed: TraversalWitness.Sample,F32,input,result>,+evidence: Witness.ArrayWitness) -> 79 TraversalWitness.Sample,Tile.Tile8,input,Weights.first(rows,inner,row,index,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,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 86 def read(-input: Array,context: Weights.Context,index: U32,evidence: Witness.ArrayWitness) -> 87 TraversalWitness.Sample,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)