law parallel_build_sequential

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

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

57# Under the same two facts, the parallel build and the one-thread build
58# (no split) hold the same F32 in every slot, so no output word depends on
59# the split or on the thread count.
60law parallel_build_sequential:
61  for ~Q: Data
62  for ~P: Data
63  for ~A: Type
64  for ~B: Type
65  for ~prepare: @+q: Q -> P
66  for ~split: A & B -> (A & B) & (A & B)
67  for ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B)
68  for +q: Q
69  for +depth: Nat
70  for +splits: Nat
71  for +count: Nat
72  for +base: Nat
73  for state: (A & B)
74  for keeps: @+position: Nat -> @inside: Bool -> {Pair.snd(F32, (A & B), cell(prepare(q), position, state, inside)) == state : (A & B)}
75  for first: {Pair.fst((A & B), (A & B), split(state)) == state : (A & B)}
76  for second: {Pair.snd((A & B), (A & B), split(state)) == state : (A & B)}
77  Holds<@+path: Model.Path(depth) ->
78    {Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state), path) ==
79      Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, 0n, count, base, state), path) : Maybe<&2, F32>}>