src/tensor/contracts/binary_proofs.bend

bendtorch-core@0.1.0.0 · 465 lines · 31 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
4import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
5import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
6import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
7import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
8import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
9import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
10import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
11import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
12import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
13import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
14import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
15import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
16import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
17import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
18import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
19import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
20import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
21import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
22import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
23import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as Broadcast
24import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast_proof.bend as BroadcastProof
25import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts
26import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_LAWS.bend as Laws
27import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as Build
28import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
29import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts
30
31def cell(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +index: Nat) -> F32:
32  Pointwise.cell(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, index)
33
34def out_leaf(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +position: Nat, inside: Bool) -> F32:
35  match inside:
36    case False{}:
37      0.0
38    case True{}:
39      cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position)
40
41def out_spec(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Array<F32>:
42  match depth:
43    case 0n:
44      ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, count))}
45    case 1n+inner:
46      ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, base), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, Nat.add(Model.capacity(inner), base))}
47
48def out_balanced(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Model.Balanced(F32, depth, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, depth, base)):
49  match depth:
50    case 0n:
51      Unit{}
52    case 1n+inner:
53      (out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, base), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, Nat.add(Model.capacity(inner), base)))
54
55def new_spec(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +depth: Nat, +base: Nat) -> {Array.new(F32, depth, 0.0) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, depth, base) : Array<F32>}:
56  match depth:
57    case 0n:
58      %Equal.sym(Bool, Nat.is_lt(base, 0n), False{}, Facts.lt_zero_false(base)) :
59        {ALeaf{0.0} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array<F32>}
60      {==}
61    case 1n+inner:
62      %Equal.sym(Array<F32>, Array.new(F32, inner, 0.0), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, base), new_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, inner, base)) :
63        {ANode{_, Array.new(F32, inner, 0.0)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 1n+inner, base) : Array<F32>}
64      %Equal.sym(Array<F32>, Array.new(F32, inner, 0.0), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, Nat.add(Model.capacity(inner), base)),
65        new_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, inner, Nat.add(Model.capacity(inner), base))) :
66        {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 1n+inner, base) : Array<F32>}
67      {==}
68
69# A subtree whose positions all lie above k is the same for k and 1 + k.
70def above(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_lt(k, b) == True{} : Bool}) ->
71  {out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, b) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, b) : Array<F32>}:
72  match depth:
73    case 0n:
74      %Equal.sym(Bool, Nat.is_lt(b, k), False{}, Facts.lt_asym(k, b, h)) :
75        {ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, Nat.is_lt(b, 1n+k))} : Array<F32>}
76      %Equal.sym(Bool, Nat.is_lt(b, 1n+k), False{}, Facts.above_false(k, b, h)) :
77        {ALeaf{0.0} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} : Array<F32>}
78      {==}
79    case 1n+inner:
80      +high = Nat.add(Model.capacity(inner), b)
81      %Equal.sym(Array<F32>, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), above(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b, h)) :
82        {ANode{_, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
83      %Equal.sym(Array<F32>, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high),
84        above(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, Arith.lt_le_trans(k, b, high, h, Api.le_add_left(Model.capacity(inner), b)))) :
85        {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
86      {==}
87
88# A subtree whose positions all lie below k is the same for k and 1 + k.
89def below(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_le(Nat.add(Model.capacity(depth), b), k) == True{} : Bool}) ->
90  {out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, b) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, b) : Array<F32>}:
91  match depth:
92    case 0n:
93      +lower = Facts.below_true(b, k, h)
94      %Equal.sym(Bool, Nat.is_lt(b, k), True{}, lower) :
95        {ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, Nat.is_lt(b, 1n+k))} : Array<F32>}
96      %Equal.sym(Bool, Nat.is_lt(b, 1n+k), True{}, Facts.lt_succ_right(b, k, lower)) :
97        {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} : Array<F32>}
98      {==}
99    case 1n+inner:
100      +c = Model.capacity(inner)
101      +high = Nat.add(c, b)
102      +nested = Equal.trans(Bool, Nat.is_le(Nat.add(c, high), k), Nat.is_le(Nat.add(Nat.add(c, c), b), k), True{},
103        Equal.cong(Nat, Bool, x => Nat.is_le(x, k), Nat.add(c, high), Nat.add(Nat.add(c, c), b), Index.add_assoc(c, c, b)), h)
104      +low_h = Facts.le_trans(high, Nat.add(c, high), k, Facts.le_add_cong(c, b, high, Api.le_add_left(c, b)), nested)
105      %Equal.sym(Array<F32>, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), below(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b, low_h)) :
106        {ANode{_, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
107      %Equal.sym(Array<F32>, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), below(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, nested)) :
108        {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array<F32>}
109      {==}
110
111# Writing cell k at the path whose position is k turns the spec for k into
112# the spec for 1 + k.
113def write_spec(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +base: Nat, +path: Model.Path(depth),
114  +h: {Nat.add(Model.offset(depth, path), base) == k : Nat}) ->
115  {ArrayCore.write_path(F32, depth, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, base), path, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, base) : Array<F32>}:
116  match depth:
117    case 0n:
118      %h : {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, _)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, 1n+_))} : Array<F32>}
119      %Equal.sym(Bool, Nat.is_lt(base, 1n+base), True{}, Facts.lt_self_succ(base)) :
120        {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array<F32>}
121      {==}
122    case 1n+inner:
123      Model.Step{+bit, +rest} = path
124      match bit:
125        case False{}:
126          +c = Model.capacity(inner)
127          +high = Nat.add(c, base)
128          +inside = Equal.trans(Bool, Nat.is_lt(k, high), Nat.is_lt(Nat.add(Model.offset(inner, rest), base), high), True{},
129            Equal.cong(Nat, Bool, x => Nat.is_lt(x, high), k, Nat.add(Model.offset(inner, rest), base),
130              Equal.sym(Nat, Nat.add(Model.offset(inner, rest), base), k, h)),
131            Facts.lt_add_right(Model.offset(inner, rest), c, base, Api.offset_lt(inner, rest)))
132          %Equal.sym(Array<F32>, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)),
133            out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, rest, h)) :
134            {ANode{_, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
135          %Equal.sym(Array<F32>, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), above(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, inside)) :
136            {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
137          {==}
138        case True{}:
139          +c = Model.capacity(inner)
140          +high = Nat.add(c, base)
141          +off = Model.offset(inner, rest)
142          +lower = Equal.trans(Bool, Nat.is_le(high, k), Nat.is_le(high, Nat.add(c, Nat.add(off, base))), True{},
143            Equal.cong(Nat, Bool, x => Nat.is_le(high, x), k, Nat.add(c, Nat.add(off, base)),
144              Equal.trans(Nat, k, Nat.add(Nat.add(c, off), base), Nat.add(c, Nat.add(off, base)),
145                Equal.sym(Nat, Nat.add(Nat.add(c, off), base), k, h),
146                Equal.sym(Nat, Nat.add(c, Nat.add(off, base)), Nat.add(Nat.add(c, off), base), Index.add_assoc(c, off, base)))),
147            Facts.le_add_cong(c, base, Nat.add(off, base), Api.le_add_left(off, base)))
148          +shifted = Equal.trans(Nat, Nat.add(off, high), Nat.add(Nat.add(c, off), base), k, Facts.position_step(c, off, base), h)
149          %Equal.sym(Array<F32>, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), below(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, lower)) :
150            {ANode{_, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k))} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
151          %Equal.sym(Array<F32>, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)),
152            out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, rest, shifted)) :
153            {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array<F32>}
154          {==}
155
156# The family history, replayed on the owned storage that `created` makes,
157# is the owned storage that holds the output spec.
158def chain(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
159  +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool},
160  +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) ->
161  {StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, k, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), f} : Storage.Storage}:
162  match k:
163    case 0n:
164      Owned.owned_eq(d, n, Array.new(F32, d, 0.0), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n), new_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)(
165        out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n))
166    case 1n+j:
167      +index = U32.from_nat(j)
168      +value = cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j)
169      +below_n = Conversion.le_successor_lt(j, n, room)
170      +exact = Conversion.natural_word_exact(j, limit, Facts.le_trans(j, n, U32.to_nat(limit), Conversion.lt_le(j, n, below_n), n_limit))
171      +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{},
172        Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n)
173      +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j,
174        Facts.output_position(d, n, index, fits, inside), exact)
175      +written = Equal.trans(Array<F32>, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), Refinement.route(d, index), value),
176        out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)),
177        write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n, Refinement.route(d, index), offset))
178      Equal.trans(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, 1n+j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
179        StorageLaws.step(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}),
180        Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f},
181        FromValues.replay_snoc(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
182        %Equal.sym(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f},
183          chain(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) :
184          {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
185        %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
186          Storage.set_checked(d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f),
187          (Storage.Owned{d, n, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value),
188            Certificates.set_result(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f}, Done{Unit{}}),
189          Api.set_checked_hit(d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f,
190            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) :
191          {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
192        Owned.owned_eq(d, n, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), written,
193          Certificates.set_result(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f)(
194          out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n)))
195
196# The plan's input shapes have the inputs' dimensions.
197def left_dims(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
198  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
199  {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(left) : List<&2, U32>}:
200  Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, p => Pair.fst(List<&2, U32>, List<&2, U32>, p),
201    (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)),
202    %planned : {ShapeLaws.planned_dimensions(left, right, _) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}
203    PlanProof.broadcast_checked_plan(left, right))
204
205def right_dims(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
206  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
207  {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(right) : List<&2, U32>}:
208  Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, p => Pair.snd(List<&2, U32>, List<&2, U32>, p),
209    (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)),
210    %planned : {ShapeLaws.planned_dimensions(left, right, _) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>}
211    PlanProof.broadcast_checked_plan(left, right))
212
213def left_count(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
214  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
215  {U32.to_nat(Shape.count(left)) == Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))) : Nat}:
216  Equal.trans(Nat, U32.to_nat(Shape.count(left)), Shape.logical_numel(Shape.dimensions(left)), Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))), Reads.count_exact(left),
217    Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(left), Shape.dimensions(Shape.left_shape(plan)),
218      Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(left), left_dims(left, right, plan, planned))))
219
220def right_count(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
221  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) ->
222  {U32.to_nat(Shape.count(right)) == Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))) : Nat}:
223  Equal.trans(Nat, U32.to_nat(Shape.count(right)), Shape.logical_numel(Shape.dimensions(right)), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))), Reads.count_exact(right),
224    Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(right), Shape.dimensions(Shape.right_shape(plan)),
225      Equal.sym(List<&2, U32>, Shape.dimensions(Shape.right_shape(plan)), Shape.dimensions(right), right_dims(left, right, plan, planned))))
226
227def scalar_cong(+operation: Elementwise.Operation, -x: F32, -y: F32, -u: F32, -v: F32, ex: {x == y : F32}, eu: {u == v : F32}) ->
228  {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, y, v) : F32}:
229  %ex : {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, _, v) : F32}
230  %eu : {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, x, _) : F32}
231  {==}
232
233# The build's leaf reads the replayed words the family cell names.
234def leaf_same(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +dl: Nat, +dr: Nat, +position: Nat, inside: Bool) ->
235  {Build.leaf(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), position, inside) == out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position, inside) : F32}:
236  match inside:
237    case False{}:
238      {==}
239    case True{}:
240      +li = Build.left_index(plan, position)
241      +ri = Build.right_index(plan, position)
242      +bli = U32.from_nat(Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position))
243      +bri = U32.from_nat(Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position))
244      Equal.trans(F32, Build.word(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), position),
245        Elementwise.scalar(operation, StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill)),
246        cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position),
247        scalar_cong(operation, Api.current(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), li, left_fill), StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill),
248          Api.current(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), ri, right_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill),
249          Owned.norm_current(U32.to_nat(Shape.count(left)), left_ops, Nil{}, li, left_fill, Api.hit_of(U32.to_nat(Shape.count(left)), left_ops), {==}),
250          Owned.norm_current(U32.to_nat(Shape.count(right)), right_ops, Nil{}, ri, right_fill, Api.hit_of(U32.to_nat(Shape.count(right)), right_ops), {==})),
251        scalar_cong(operation, StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill), StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), bli, left_fill),
252          StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), bri, right_fill),
253          Equal.cong(Nat, F32, w => StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), U32.from_nat(w), left_fill),
254            Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Build.walk_left_same(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)),
255          Equal.cong(Nat, F32, w => StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), U32.from_nat(w), right_fill),
256            Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Build.walk_right_same(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position))))
257
258def spec_same(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +dl: Nat, +dr: Nat, +depth: Nat, +base: Nat) ->
259  {Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), depth, base) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), depth, base) : Array<F32>}:
260  match depth:
261    case 0n:
262      Equal.cong(F32, Array<F32>, x => ALeaf{x}, Build.leaf(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), base, Nat.is_lt(base, U32.to_nat(Shape.count(Shape.output_shape(plan))))), out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, U32.to_nat(Shape.count(Shape.output_shape(plan))))),
263        leaf_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, base, Nat.is_lt(base, U32.to_nat(Shape.count(Shape.output_shape(plan))))))
264    case 1n+inner:
265      +high = Nat.add(Model.capacity(inner), base)
266      %Equal.sym(Array<F32>, Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), inner, base), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), inner, base), spec_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, inner, base)) :
267        {ANode{_, Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), 1n+inner, base) : Array<F32>}
268      %Equal.sym(Array<F32>, Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), inner, high), spec_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, inner, high)) :
269        {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), 1n+inner, base) : Array<F32>}
270      {==}
271
272def cells_snoc(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +previous: Nat, +before: List<&2, F32>, +word: F32, +other: F32,
273  rest: {before == Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous) : List<&2, F32>}, last: {word == other : F32}) ->
274  {List.append(&2, F32, before, [word]) == List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [other]) : List<&2, F32>}:
275  Equal.trans(List<&2, F32>, List.append(&2, F32, before, [word]), List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [word]),
276    List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [other]),
277    Equal.cong(List<&2, F32>, List<&2, F32>, values => List.append(&2, F32, values, [word]), before, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), rest),
278    Equal.cong(F32, List<&2, F32>, value => List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [value]), word, other, last))
279
280# The words of the family history are `cells`.
281def words_cells(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) ->
282  {Contracts.words(Shape.output_shape(plan), 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), count) == Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count) : List<&2, F32>}:
283  match count:
284    case 0n:
285      {==}
286    case 1n+previous:
287      +output = Shape.output_shape(plan)
288      +total = Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))
289      +below = Conversion.le_successor_lt(previous, total, room)
290      +position = U32.from_nat(previous)
291      cells_snoc(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous, Contracts.words(output, 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), previous), Replayed.value(output, 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), position),
292        cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), words_cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous, Conversion.le_predecessor(previous, total, room)),
293        Equal.trans(F32, Replayed.value(output, 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), position), cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(position)), cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous),
294          PointwiseProof.writes_value(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, total, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, output, position,
295            PointwiseProof.word_inside(previous, output, below), Conversion.le_reflexive(total)),
296          Equal.cong(Nat, F32, number => cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, number), U32.to_nat(position), previous, PointwiseProof.word_exact(previous, output, below))))
297
298def half_keeps(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +index: U32) ->
299  {Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), index) == Replayed.value(shape, fill, ops, index) : F32}:
300  Replayed.expected_snoc(ops, StorageLaws.First{}, U32.to_nat(Shape.count(shape)), index, fill)
301
302def words_snoc(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +word: F32, +other: F32,
303  +before: List<&2, F32>, rest: {Contracts.words(shape, fill, ops, previous) == before : List<&2, F32>}, last: {word == other : F32}) ->
304  {List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]) == List.append(&2, F32, before, [other]) : List<&2, F32>}:
305  Equal.trans(List<&2, F32>, List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]),
306    List.append(&2, F32, before, [word]), List.append(&2, F32, before, [other]),
307    Equal.cong(List<&2, F32>, List<&2, F32>, values => List.append(&2, F32, values, [word]), Contracts.words(shape, fill, ops, previous), before, rest),
308    Equal.cong(F32, List<&2, F32>, value => List.append(&2, F32, before, [value]), word, other, last))
309
310# The First half of a clone lists the same words.
311def words_first(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
312  {Contracts.words(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), count) == Contracts.words(shape, fill, ops, count) : List<&2, F32>}:
313  match count:
314    case 0n:
315      {==}
316    case 1n+previous:
317      +position = U32.from_nat(previous)
318      words_snoc(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), previous,
319        Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), position), Replayed.value(shape, fill, ops, position),
320        Contracts.words(shape, fill, ops, previous), words_first(shape, fill, ops, previous), half_keeps(shape, fill, ops, position))
321
322# `take` of an owned tensor hands back the First half of its clone and the
323# Second half's array.
324def take_owned_lift(+shape: Shape.Shape, +d: Nat, +n: Nat, -array: Array<F32>, pair: Array<F32> & Array<F32>,
325  -same: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>}, -b: Model.Balanced(F32, d, array),
326  -f: {Storage.bounds(d, n) == True{} : Bool}, -fits: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
327  -Q: (Core.Dynamic & Array<F32>) -> Type,
328  h: @-kept: {Lifecycle.logical_length(StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f))) ==
329    Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
330    Q((Core.Packed{shape, Core.TTensor{StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f)), kept}},
331      Pair.snd(Array<F32>, Array<F32>, pair)))) ->
332  Q(Elementwise.take_owned(shape, d, n, array, pair, same, b, f, fits)):
333  (kept, copy) = pair
334  h(fits)
335
336def positive_of_lt(+w: Nat, +n: Nat, h: {Nat.is_lt(w, n) == True{} : Bool}) -> {Nat.is_lt(0n, n) == True{} : Bool}:
337  match n:
338    case 0n:
339      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, Arith.lt_zero(w, h))
340    case 1n+q:
341      {==}
342
343def output_positive(+plan: Shape.BroadcastPlan, +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) ->
344  {Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}:
345  Equal.trans(Bool, Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), Nat.is_lt(0n, U32.to_nat(Shape.count(Shape.output_shape(plan)))), True{},
346    Equal.cong(Nat, Bool, x => Nat.is_lt(0n, x), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), U32.to_nat(Shape.count(Shape.output_shape(plan))), Equal.sym(Nat, U32.to_nat(Shape.count(Shape.output_shape(plan))), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Reads.count_exact(Shape.output_shape(plan)))),
347    Arith.and_left(Nat.is_lt(0n, U32.to_nat(Shape.count(Shape.output_shape(plan)))), Nat.is_le(U32.to_nat(Shape.count(Shape.output_shape(plan))), Model.capacity(d)),
348      Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, U32.to_nat(Shape.count(Shape.output_shape(plan)))), Nat.is_le(U32.to_nat(Shape.count(Shape.output_shape(plan))), Model.capacity(d))), fits)))
349
350# An output with a cell reads a cell of each input, so neither input is empty.
351def left_positive(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
352  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>},
353  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> {Nat.is_lt(0n, U32.to_nat(Shape.count(left))) == True{} : Bool}:
354  +walk = Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), 0n)
355  positive_of_lt(walk, U32.to_nat(Shape.count(left)),
356    Equal.trans(Bool, Nat.is_lt(walk, U32.to_nat(Shape.count(left))), Nat.is_lt(walk, Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan)))), True{},
357      Equal.cong(Nat, Bool, x => Nat.is_lt(walk, x), U32.to_nat(Shape.count(left)), Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))), left_count(left, right, plan, planned)),
358      BroadcastProof.left_walk_bound(plan, Shape.index_map(plan), 0n, output_positive(plan, d, fits))))
359
360def right_positive(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
361  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>},
362  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> {Nat.is_lt(0n, U32.to_nat(Shape.count(right))) == True{} : Bool}:
363  +walk = Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), 0n)
364  positive_of_lt(walk, U32.to_nat(Shape.count(right)),
365    Equal.trans(Bool, Nat.is_lt(walk, U32.to_nat(Shape.count(right))), Nat.is_lt(walk, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))), True{},
366      Equal.cong(Nat, Bool, x => Nat.is_lt(walk, x), U32.to_nat(Shape.count(right)), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))), right_count(left, right, plan, planned)),
367      BroadcastProof.right_walk_bound(plan, Shape.index_map(plan), 0n, output_positive(plan, d, fits))))
368
369def output_eq(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, +dl: Nat, +fitsl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool},
370  +dr: Nat, +fitsr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool},
371  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> {StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f} : Storage.Storage}:
372  +spec = Equal.trans(Array<F32>, Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), d, 0n), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n),
373    Build.build_eq(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), fitsl, fitsr,
374      Owned.norm_written(U32.to_nat(Shape.count(left)), left_ops, Nil{}, Api.hit_of(U32.to_nat(Shape.count(left)), left_ops), {==}, {==}),
375      Owned.norm_written(U32.to_nat(Shape.count(right)), right_ops, Nil{}, Api.hit_of(U32.to_nat(Shape.count(right)), right_ops), {==}, {==}),
376      Reads.count_exact(Shape.output_shape(plan)), left_count(left, right, plan, planned), right_count(left, right, plan, planned),
377      d, Elementwise.splits(d), 0n),
378    spec_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, d, 0n))
379  Equal.trans(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, U32.to_nat(Shape.count(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
380    Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f},
381    Equal.cong(Nat, Storage.Storage, count => StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), U32.to_nat(Shape.count(Shape.output_shape(plan))),
382      Equal.sym(Nat, U32.to_nat(Shape.count(Shape.output_shape(plan))), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Reads.count_exact(Shape.output_shape(plan)))),
383    Equal.trans(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, U32.to_nat(Shape.count(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), f},
384      Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f},
385      chain(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fits, Shape.count(Shape.output_shape(plan)), Conversion.le_reflexive(U32.to_nat(Shape.count(Shape.output_shape(plan)))), U32.to_nat(Shape.count(Shape.output_shape(plan))), Conversion.le_reflexive(U32.to_nat(Shape.count(Shape.output_shape(plan))))),
386      Owned.owned_eq(d, U32.to_nat(Shape.count(Shape.output_shape(plan))), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Equal.sym(Array<F32>, Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), spec),
387        out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), f)(Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)))))
388
389def core(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, +dl: Nat, +fitsl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool}, -bl: Model.Balanced(F32, dl, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)),
390  -fl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool},
391  +dr: Nat, +fitsr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool}, -br: Model.Balanced(F32, dr, Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)),
392  -fr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool},
393  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool},
394  -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
395  hyp: @-kl: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-kr: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{}), kr}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))) ->
396  @-lfits: {Lifecycle.logical_length(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
397  @-fo: {U32.to_nat(Shape.count(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} ->
398  P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.Packed{left, Core.TTensor{Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, lfits}}),
399    Elementwise.take(Core.Packed{right, Core.TTensor{Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, rfits}}))):
400  lfits => rfits => fo =>
401    take_owned_lift(left, dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)), {==}, bl, fl, lfits,
402      t => P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, t, Elementwise.take(Core.Packed{right, Core.TTensor{Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, rfits}}))),
403      kl => take_owned_lift(right, dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), {==}, br, fr, rfits,
404        t => P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, (Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)))), t)),
405        kr => Facts.storage_shift(Shape.output_shape(plan), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f},
406          output_eq(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, dl, fitsl, dr, fitsr, d, fits, f),
407          st => k => P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{}), kr}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{st, k}}})), hyp(kl, kr))(fo)))
408
409# The output storage is owned: normalize the left input, then the right one,
410# and run `core`.
411def owned_case(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
412  -rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat},
413  -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
414  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) ->
415  (@+left_kept: List<&2, StorageLaws.Op> -> @left_words: {Contracts.words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) == Contracts.words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} -> @-left_kfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_kfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))) -> @-fo: {U32.to_nat(Shape.count(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} ->
416  P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits})), Elementwise.take(Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits})))):
417  ho => fo =>
418    Facts.input_lift(left, left_fill, left_ops, left_positive(left, right, plan, planned, d, fits),
419      sl => (@-lf: {Lifecycle.logical_length(sl) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> (@-kl: {Lifecycle.logical_length(StorageLaws.step(sl, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(sl, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))) ->
420        P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.Packed{left, Core.TTensor{sl, lf}}), Elementwise.take(Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}))))),
421      dl => fitsl => bl => fl => lf => hl =>
422        Facts.input_lift(right, right_fill, right_ops, right_positive(left, right, plan, planned, d, fits),
423          sr => (@-rf: {Lifecycle.logical_length(sr) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> (@-kl: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-kr: {Lifecycle.logical_length(StorageLaws.step(sr, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(sr, StorageLaws.First{}), kr}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))) ->
424            P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.Packed{left, Core.TTensor{Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, lf}}),
425              Elementwise.take(Core.Packed{right, Core.TTensor{sr, rf}})))),
426          dr => fitsr => br => fr => rf => hr => core(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, dl, fitsl, bl, fl, dr, fitsr, br, fr, d, fits, f, P, hr)(lf, rf, fo))(
427          rfits,
428          kl => Facts.storage_shift(right, Replayed.storage(right, right_fill, Replayed.snoc(right_ops, StorageLaws.First{})),
429            StorageLaws.step(Replayed.storage(right, right_fill, right_ops), StorageLaws.First{}), Replayed.replay_snoc(right_ops, StorageLaws.First{}, right, right_fill),
430            st => k => (@-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{st, k}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))),
431            rk => hl(kl, Replayed.snoc(right_ops, StorageLaws.First{}), words_first(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))), rk))))(
432      lfits,
433      Facts.storage_shift(left, Replayed.storage(left, left_fill, Replayed.snoc(left_ops, StorageLaws.First{})),
434        StorageLaws.step(Replayed.storage(left, left_fill, left_ops), StorageLaws.First{}), Replayed.replay_snoc(left_ops, StorageLaws.First{}, left, left_fill),
435        st => k => (@+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{st, k}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))),
436        lk => ho(Replayed.snoc(left_ops, StorageLaws.First{}), words_first(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))), lk)))
437
438# The parallel build on two replayed inputs into an output that `Core.new`
439# allocates: binary_replayed below the planner, which broadcast_to shares.
440def allocated_replayed(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
441  h: Laws.BinaryWith(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, P)) ->
442  @-lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
443  P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Core.new(Shape.output_shape(plan), 0.0))):
444  lfits => rfits =>
445    Replayed.new_lift(Shape.output_shape(plan), 0.0, result => P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), result)),
446      fo => Owned.created_lift(Shape.count(Shape.output_shape(plan)), 0.0, Conversion.shape_count_within(Shape.output_shape(plan)),
447        s => ((@+left_kept: List<&2, StorageLaws.Op> -> @left_words: {Contracts.words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) == Contracts.words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} -> @-left_kfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s)) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_kfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s), ko}}}))) -> @-fo: {Lifecycle.logical_length(s) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} ->
448          P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Done{Core.TTensor{s, fo}}))),
449        zero => ho => fo =>
450          Facts.storage_shift(Shape.output_shape(plan), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)),
451            st => k => P(((Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits})), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{st, k}}})),
452            ho(left_ops, {==}, lfits, right_ops, {==}, rfits))(fo),
453        d => fits => f => owned_case(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, lfits, rfits, P, d, fits, f))(
454        left_kept => left_words => left_kfits => right_kept => right_words => right_kfits => ko =>
455          h(left_kept, left_words, left_kfits, right_kept, right_words, right_kfits, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops),
456            words_cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Conversion.le_reflexive(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))), ko), fo))
457
458def binary_replayed(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
459  h: Laws.BinaryWith(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, P)) ->
460  @-lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
461  P(Elementwise.binary(operation, Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}})):
462  lfits => rfits =>
463    %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(left, right), Done{plan}, planned) :
464      P(Elementwise.parallel_planned(operation, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), _))
465    allocated_replayed(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, P, h)(lfits, rfits)