KernelGemmCertificate.store_tail: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend as KernelGemmCertificate
Lines 21-46 of stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend&start_line=21&end_line=46

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

def store_tail(+count: U32,+depth: Nat,-output: Array<F32>,+offset: U32,-bias: F32,-accumulator: Tile.Tile8,
  evidence: Witness.Witness(F32,depth,output)) ->
  Witness.Witness(F32,depth,Gemm.store_tail(count,output,offset,bias,accumulator)):
  -a = (Tile.lane0(accumulator) + bias : F32)
  -b = (Tile.lane1(accumulator) + bias : F32)
  -c = (Tile.lane2(accumulator) + bias : F32)
  -d = (Tile.lane3(accumulator) + bias : F32)
  -e = (Tile.lane4(accumulator) + bias : F32)
  -f = (Tile.lane5(accumulator) + bias : F32)
  -g = (Tile.lane6(accumulator) + bias : F32)
  -h = (Tile.lane7(accumulator) + bias : F32)
  -o1 = Gemm.store_lane(U32.is_lt(0,count),output,offset,a)
  -o2 = Gemm.store_lane(U32.is_lt(1,count),o1,(offset + 1 : U32),b)
  -o3 = Gemm.store_lane(U32.is_lt(2,count),o2,(offset + 2 : U32),c)
  -o4 = Gemm.store_lane(U32.is_lt(3,count),o3,(offset + 3 : U32),d)
  -o5 = Gemm.store_lane(U32.is_lt(4,count),o4,(offset + 4 : U32),e)
  -o6 = Gemm.store_lane(U32.is_lt(5,count),o5,(offset + 5 : U32),f)
  -o7 = Gemm.store_lane(U32.is_lt(6,count),o6,(offset + 6 : U32),g)
  evidence = store_lane(depth,U32.is_lt(0,count),output,offset,a,evidence)
  evidence = store_lane(depth,U32.is_lt(1,count),o1,(offset + 1 : U32),b,evidence)
  evidence = store_lane(depth,U32.is_lt(2,count),o2,(offset + 2 : U32),c,evidence)
  evidence = store_lane(depth,U32.is_lt(3,count),o3,(offset + 3 : U32),d,evidence)
  evidence = store_lane(depth,U32.is_lt(4,count),o4,(offset + 4 : U32),e,evidence)
  evidence = store_lane(depth,U32.is_lt(5,count),o5,(offset + 5 : U32),f,evidence)
  evidence = store_lane(depth,U32.is_lt(6,count),o6,(offset + 6 : U32),g,evidence)
  store_lane(depth,U32.is_lt(7,count),o7,(offset + 7 : U32),h,evidence)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=store_lane
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_gemm.bend&name=store_tail
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane0
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane1
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane2
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane3
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane4
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane5
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane6
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=lane7
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend&name=store_lane
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness