src/tensor/parallel_PROOF.bend

bendtorch-core@0.1.0.0 · 31 lines · 0 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel
4import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Proof
5import bendtorch-core@0.1.0.0/src/tensor/parallel_LAWS.bend as Laws
6
7def Laws.parallel_build_balanced(Q, P, A, B, prepare, split, cell, q, depth, splits, count, base, state):
8  Parallel.balanced(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state)
9
10def Laws.parallel_build_cells(Q, P, A, B, prepare, split, cell, q, depth, splits, count, base, state, keeps, first, second):
11  Laws.Holds{{\{Proof.Fact: q => q} :
12    Proof.Fact<Proof.Cells(~P, ~A, ~B, ~cell, prepare(q), state, depth, count, base, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state))> ->
13    Proof.Cells(~P, ~A, ~B, ~cell, prepare(q), state, depth, count, base, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state))}(
14    Proof.build_cells(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, state, depth, splits, count, base, state, {==}, keeps, first, second))}
15
16def Laws.parallel_build_sequential(Q, P, A, B, prepare, split, cell, q, depth, splits, count, base, state, keeps, first, second):
17  Laws.Holds{path => Equal.trans(Maybe<&2, F32>,
18    Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state), path),
19    Some{Pair.fst(F32, (A & B), cell(prepare(q), Nat.add(Model.offset(depth, path), base), state, Nat.is_lt(Nat.add(Model.offset(depth, path), base), count)))},
20    Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, 0n, count, base, state), path),
21    {\{Proof.Fact: q => q} :
22      Proof.Fact<Proof.Cells(~P, ~A, ~B, ~cell, prepare(q), state, depth, count, base, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state))> ->
23      Proof.Cells(~P, ~A, ~B, ~cell, prepare(q), state, depth, count, base, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state))}(
24      Proof.build_cells(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, state, depth, splits, count, base, state, {==}, keeps, first, second))(path),
25    Equal.sym(Maybe<&2, F32>,
26      Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, 0n, count, base, state), path),
27      Some{Pair.fst(F32, (A & B), cell(prepare(q), Nat.add(Model.offset(depth, path), base), state, Nat.is_lt(Nat.add(Model.offset(depth, path), base), count)))},
28      {\{Proof.Fact: q => q} :
29        Proof.Fact<Proof.Cells(~P, ~A, ~B, ~cell, prepare(q), state, depth, count, base, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, 0n, count, base, state))> ->
30        Proof.Cells(~P, ~A, ~B, ~cell, prepare(q), state, depth, count, base, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, 0n, count, base, state))}(
31        Proof.build_cells(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, state, depth, 0n, count, base, state, {==}, keeps, first, second))(path)))}