law batched_build_cells

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_LAWS.bend:128

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

128# For two balanced input arrays A and B and every split, every cell of the
129# parallel build holds the fold its layout names, so no word depends on the
130# split or the thread count, and both arrays are only read. The forward
131# product and both gradients of the tape's BatchedMatmul are such builds
132# (`Batched.forward_layout`, `left_layout`, `right_layout`).
133law batched_build_cells:
134  for +depth: Nat
135  for +splits: Nat
136  for +dl: Nat
137  for +dr: Nat
138  for -A: Array<F32>
139  for -B: Array<F32>
140  for +lo: Matrix.Order
141  for +ro: Matrix.Order
142  for +inner: Nat
143  for +rows: Nat
144  for +columns: Nat
145  for +l1: Nat
146  for +l2: Nat
147  for +r1: Nat
148  for +r2: Nat
149  for +o2: Nat
150  for +count: Nat
151  for +base: Nat
152  for la: Array<F32>
153  for ra: Array<F32>
154  for el: {la == A : Array<F32>}
155  for er: {ra == B : Array<F32>}
156  for left_valid: Model.Balanced(F32, dl, A)
157  for right_valid: Model.Balanced(F32, dr, B)
158  Holds<Cells(depth, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, o2, count, base,
159    Batched.build(depth, splits, layout_of(lo, ro, inner, rows, columns, l1, l2, r1, r2, o2), count, base, la, ra))>