def store_tail

stelliferous@0.0.2.0 · proofs/kernel_gemm_certificate.bend:21

import Base
import stelliferous@0.0.2.0/kernel_gemm.bend as Gemm
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

21def store_tail(+count: U32,+depth: Nat,-output: Array<F32>,+offset: U32,-bias: F32,-accumulator: Tile.Tile8,
22  evidence: Witness.Witness(F32,depth,output)) ->
23  Witness.Witness(F32,depth,Gemm.store_tail(count,output,offset,bias,accumulator)):
24  -a = (Tile.lane0(accumulator) + bias : F32)
25  -b = (Tile.lane1(accumulator) + bias : F32)
26  -c = (Tile.lane2(accumulator) + bias : F32)
27  -d = (Tile.lane3(accumulator) + bias : F32)
28  -e = (Tile.lane4(accumulator) + bias : F32)
29  -f = (Tile.lane5(accumulator) + bias : F32)
30  -g = (Tile.lane6(accumulator) + bias : F32)
31  -h = (Tile.lane7(accumulator) + bias : F32)
32  -o1 = Gemm.store_lane(U32.is_lt(0,count),output,offset,a)
33  -o2 = Gemm.store_lane(U32.is_lt(1,count),o1,(offset + 1 : U32),b)
34  -o3 = Gemm.store_lane(U32.is_lt(2,count),o2,(offset + 2 : U32),c)
35  -o4 = Gemm.store_lane(U32.is_lt(3,count),o3,(offset + 3 : U32),d)
36  -o5 = Gemm.store_lane(U32.is_lt(4,count),o4,(offset + 4 : U32),e)
37  -o6 = Gemm.store_lane(U32.is_lt(5,count),o5,(offset + 5 : U32),f)
38  -o7 = Gemm.store_lane(U32.is_lt(6,count),o6,(offset + 6 : U32),g)
39  evidence = store_lane(depth,U32.is_lt(0,count),output,offset,a,evidence)
40  evidence = store_lane(depth,U32.is_lt(1,count),o1,(offset + 1 : U32),b,evidence)
41  evidence = store_lane(depth,U32.is_lt(2,count),o2,(offset + 2 : U32),c,evidence)
42  evidence = store_lane(depth,U32.is_lt(3,count),o3,(offset + 3 : U32),d,evidence)
43  evidence = store_lane(depth,U32.is_lt(4,count),o4,(offset + 4 : U32),e,evidence)
44  evidence = store_lane(depth,U32.is_lt(5,count),o5,(offset + 5 : U32),f,evidence)
45  evidence = store_lane(depth,U32.is_lt(6,count),o6,(offset + 6 : U32),g,evidence)
46  store_lane(depth,U32.is_lt(7,count),o7,(offset + 7 : U32),h,evidence)