BatchedMatmulLAWS.batched_build_cells: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as BatchedMatmulLAWS
Lines 128-159 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&start_line=128&end_line=159

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched

# For two balanced input arrays A and B and every split, every cell of the
# parallel build holds the fold its layout names, so no word depends on the
# split or the thread count, and both arrays are only read. The forward
# product and both gradients of the tape's BatchedMatmul are such builds
# (`Batched.forward_layout`, `left_layout`, `right_layout`).
law batched_build_cells:
  for +depth: Nat
  for +splits: Nat
  for +dl: Nat
  for +dr: Nat
  for -A: Array<F32>
  for -B: Array<F32>
  for +lo: Matrix.Order
  for +ro: Matrix.Order
  for +inner: Nat
  for +rows: Nat
  for +columns: Nat
  for +l1: Nat
  for +l2: Nat
  for +r1: Nat
  for +r2: Nat
  for +o2: Nat
  for +count: Nat
  for +base: Nat
  for la: Array<F32>
  for ra: Array<F32>
  for el: {la == A : Array<F32>}
  for er: {ra == B : Array<F32>}
  for left_valid: Model.Balanced(F32, dl, A)
  for right_valid: Model.Balanced(F32, dr, B)
  Holds<Cells(depth, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, o2, count, base,
    Batched.build(depth, splits, layout_of(lo, ro, inner, rows, columns, l1, l2, r1, r2, o2), count, base, la, ra))>

Uses (31):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=Layout
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=cell_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=layout
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=CellSpec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=Cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=layout_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=cell_keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=cell_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=cell_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=split
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=pair_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=split_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Order
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=build_cells