1	import Base
2	import ../storage/model.bend as Model
3	import ./parallel.bend as Parallel
4	import ./parallel_proofs.bend as Proof
5	import ./parallel_LAWS.bend as Laws
6	
7	def 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	
10	def 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	
16	def 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)))}