law parallel_build_cells

bendtorch-core@0.1.0.0 · src/tensor/parallel_LAWS.bend:31

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel

31# If each cell hands its input state back and the split copies the state
32# into both halves, then for every split each slot of the build, cell
33# base + offset, holds the F32 the cell function computes for it from the
34# input state, the padding past `count` included.
35law parallel_build_cells:
36  for ~Q: Data
37  for ~P: Data
38  for ~A: Type
39  for ~B: Type
40  for ~prepare: @+q: Q -> P
41  for ~split: A & B -> (A & B) & (A & B)
42  for ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B)
43  for +q: Q
44  for +depth: Nat
45  for +splits: Nat
46  for +count: Nat
47  for +base: Nat
48  for state: (A & B)
49  for keeps: @+position: Nat -> @inside: Bool -> {Pair.snd(F32, (A & B), cell(prepare(q), position, state, inside)) == state : (A & B)}
50  for first: {Pair.fst((A & B), (A & B), split(state)) == state : (A & B)}
51  for second: {Pair.snd((A & B), (A & B), split(state)) == state : (A & B)}
52  Holds<@+path: Model.Path(depth) ->
53    {Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state), path) ==
54      Some{Pair.fst(F32, (A & B), cell(prepare(q), Nat.add(Model.offset(depth, path), base), state,
55        Nat.is_lt(Nat.add(Model.offset(depth, path), base), count)))} : Maybe<&2, F32>}>