src/tensor/elementwise_parallel_proof.bend

bendtorch-core@0.1.0.0 · 567 lines · 45 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/flat.bend as Flat
4import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
5import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
6import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
7import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
8# Proves the shape laws that importing ShapeLaws would otherwise leave open.
9import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
10import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
11import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
12import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
13import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
14import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
15import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
16import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
17import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
18import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
19import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
20import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
21import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
22import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic
23import bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend as WalkProof
24
25# Proofs that the parallel elementwise build writes, at every output index,
26# the value `Elementwise.expected` names there.
27
28type Fact<-P: Type> is Data:
29  Fact{-proof: P}
30
31# The value a cell gets from the two observed input cells.
32def pick(operation: Elementwise.Operation, left: Maybe<&2, F32>, right: Maybe<&2, F32>) -> Maybe<&2, F32>:
33  match left:
34    case None{}:
35      None{}
36    case Some{value}:
37      Elementwise.expected_right(operation, value, right)
38
39def want(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, A: Array<F32>, B: Array<F32>, +position: Nat) ->
40  Maybe<&2, F32>:
41  pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(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)))), Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(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)))))
42
43def transport_balanced(-d: Nat, -a: Array<F32>, -b: Array<F32>, -same: {a == b : Array<F32>}, -valid: Model.Balanced(F32, d, b)) ->
44  Fact<Model.Balanced(F32, d, a)>:
45  Fact{
46    %Equal.sym(Array<F32>, a, b, same) : Model.Balanced(F32, d, _)
47    valid}
48
49# A read keeps the array and returns the observed cell.
50def read_keeps(-d: Nat, -original: Array<F32>, -target: Array<F32>, -i: U32, -pair: Array<F32> & F32,
51  -exact: {pair == Array.get(F32, original, i) : Array<F32> & F32}, -same: {original == target : Array<F32>},
52  -valid: Model.Balanced(F32, d, target)) -> Fact<{Refinement.first(F32, pair) == target : Array<F32>}>:
53  Fact{Equal.trans(Array<F32>, Refinement.first(F32, pair), Refinement.first(F32, Array.get(F32, original, i)), target,
54    Equal.cong(Array<F32> & F32, Array<F32>, p => Refinement.first(F32, p), pair, Array.get(F32, original, i), exact),
55    Equal.trans(Array<F32>, Refinement.first(F32, Array.get(F32, original, i)), original, target,
56      Refinement.law_get_retains(F32, d, original, i, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid))),
57      same))}
58
59def read_value(-d: Nat, -original: Array<F32>, -target: Array<F32>, -i: U32, -pair: Array<F32> & F32,
60  -exact: {pair == Array.get(F32, original, i) : Array<F32> & F32}, -same: {original == target : Array<F32>},
61  -valid: Model.Balanced(F32, d, target)) ->
62  Fact<{Some{Refinement.second(F32, pair)} == Model.observe(F32, d, target, Refinement.route(d, i)) : Maybe<&2, F32>}>:
63  Fact{Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, pair)}, Some{Refinement.second(F32, Array.get(F32, original, i))},
64    Model.observe(F32, d, target, Refinement.route(d, i)),
65    Equal.cong(Array<F32> & F32, Maybe<&2, F32>, p => Some{Refinement.second(F32, p)}, pair, Array.get(F32, original, i), exact),
66    Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, original, i))},
67      Model.observe(F32, d, original, Refinement.route(d, i)), Model.observe(F32, d, target, Refinement.route(d, i)),
68      Refinement.law_get_refines(F32, d, original, i, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid))),
69      Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, d, a, Refinement.route(d, i)), original, target, same)))}
70
71def pick_value(+operation: Elementwise.Operation, -x: F32, -y: F32, -lm: Maybe<&2, F32>, -rm: Maybe<&2, F32>,
72  -ex: {Some{x} == lm : Maybe<&2, F32>}, -ey: {Some{y} == rm : Maybe<&2, F32>}) ->
73  Fact<{Some{Elementwise.scalar(operation, x, y)} == pick(operation, lm, rm) : Maybe<&2, F32>}>:
74  Fact{
75    %ex : {Some{Elementwise.scalar(operation, x, y)} == pick(operation, _, rm) : Maybe<&2, F32>}
76    %ey : {Some{Elementwise.scalar(operation, x, y)} == Elementwise.expected_right(operation, x, _) : Maybe<&2, F32>}
77    {==}}
78
79def clone_first(-d: Nat, -original: Array<F32>, -target: Array<F32>, -pair: Array<F32> & Array<F32>,
80  -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>}, -same: {original == target : Array<F32>},
81  -valid: Model.Balanced(F32, d, target)) -> Fact<{Pair.fst(Array<F32>, Array<F32>, pair) == target : Array<F32>}>:
82  Fact{Equal.trans(Array<F32>, Pair.fst(Array<F32>, Array<F32>, pair), Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, original)), target,
83    Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.fst(Array<F32>, Array<F32>, p), pair, Array.clone(F32, original), exact),
84    Equal.trans(Array<F32>, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, original)), original, target,
85      Clone.first_equal(F32, d, original, Clone.certify(F32, d, original, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid)))),
86      same))}
87
88def clone_second(-d: Nat, -original: Array<F32>, -target: Array<F32>, -pair: Array<F32> & Array<F32>,
89  -exact: {pair == Array.clone(F32, original) : Array<F32> & Array<F32>}, -same: {original == target : Array<F32>},
90  -valid: Model.Balanced(F32, d, target)) -> Fact<{Pair.snd(Array<F32>, Array<F32>, pair) == target : Array<F32>}>:
91  Fact{Equal.trans(Array<F32>, Pair.snd(Array<F32>, Array<F32>, pair), Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, original)), target,
92    Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.snd(Array<F32>, Array<F32>, p), pair, Array.clone(F32, original), exact),
93    Equal.trans(Array<F32>, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, original)), original, target,
94      Clone.second_equal(F32, d, original, Clone.certify(F32, d, original, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid)))),
95      same))}
96
97# The input cells a build reads for output cell `position`.
98def left_at(+plan: Shape.BroadcastPlan, +position: Nat) -> U32:
99  U32.from_nat(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))
100
101def right_at(+plan: Shape.BroadcastPlan, +position: Nat) -> U32:
102  U32.from_nat(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))
103
104def pair_equal(-a: Array<F32>, -b: Array<F32>, -A: Array<F32>, -B: Array<F32>, ea: {a == A : Array<F32>}, eb: {b == B : Array<F32>}) ->
105  {(a, b) == (A, B) : Array<F32> & Array<F32>}:
106  Equal.trans(Array<F32> & Array<F32>, (a, b), (A, b), (A, B),
107    Equal.cong(Array<F32>, Array<F32> & Array<F32>, x => (x, b), a, A, ea),
108    Equal.cong(Array<F32>, Array<F32> & Array<F32>, y => (A, y), b, B, eb))
109
110# What an inside cell of the build gives: both arrays back, and the F32
111# `want` names.
112def CellOut(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +position: Nat,
113  -result: F32 & (Array<F32> & Array<F32>)) -> Type:
114  {Pair.snd(F32, Array<F32> & Array<F32>, result) == (A, B) : Array<F32> & Array<F32>} &
115    {Some{Pair.fst(F32, Array<F32> & Array<F32>, result)} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>}
116
117def right_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +position: Nat,
118  -x: F32, -la: Array<F32>, pair: Array<F32> & F32, -exact: {pair == Array.get(F32, B, right_at(plan, position)) : Array<F32> & F32},
119  -ex: {Some{x} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>},
120  -el: {la == A : Array<F32>}, -valid: Model.Balanced(F32, dr, B)) ->
121  Fact<CellOut(operation, plan, dl, dr, A, B, position, Elementwise.cell_right(operation, x, la, pair))>:
122  (kept, y) = pair
123  Fact{(pair_equal(la, kept, A, B, el,
124      {\{Fact: q => q} : Fact<({Refinement.first(F32, (kept, y)) == B : Array<F32>})> -> {Refinement.first(F32, (kept, y)) == B : Array<F32>}}(
125        read_keeps(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid))),
126    {\{Fact: q => q} : Fact<({Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>})> ->
127      {Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>}}(
128      pick_value(operation, x, y, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))), ex,
129        {\{Fact: q => q} : Fact<({Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>})> ->
130          {Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>}}(
131          read_value(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid)))))}
132
133def left_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, B: Array<F32>, +position: Nat,
134  pair: Array<F32> & F32, -exact: {pair == Array.get(F32, A, left_at(plan, position)) : Array<F32> & F32},
135  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
136  Fact<CellOut(operation, plan, dl, dr, A, B, position, Elementwise.cell_left(operation, B, right_at(plan, position), pair))>:
137  (kept, x) = pair
138  right_out(operation, plan, dl, dr, A, B, position, x, kept, Array.get(F32, B, right_at(plan, position)), {==},
139    {\{Fact: q => q} : Fact<({Some{Refinement.second(F32, (kept, x))} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>})> ->
140      {Some{Refinement.second(F32, (kept, x))} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>}}(
141      read_value(dl, A, A, left_at(plan, position), (kept, x), exact, {==}, left_valid)),
142    {\{Fact: q => q} : Fact<({Refinement.first(F32, (kept, x)) == A : Array<F32>})> -> {Refinement.first(F32, (kept, x)) == A : Array<F32>}}(
143      read_keeps(dl, A, A, left_at(plan, position), (kept, x), exact, {==}, left_valid)),
144    right_valid)
145
146# The elementwise cell function of `Parallel.build`, from the input arrays.
147def cell_of(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +position: Nat, A: Array<F32>, B: Array<F32>, inside: Bool) ->
148  F32 & (Array<F32> & Array<F32>):
149  Elementwise.cell_at(Elementwise.walk(Elementwise.Request{operation, plan}), position, (A, B), inside)
150
151def cell_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, A: Array<F32>, B: Array<F32>, +position: Nat,
152  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
153  Fact<CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))>:
154  %Equal.sym(F32 & (Array<F32> & Array<F32>), cell_of(operation, plan, position, A, B, True{}),
155    Elementwise.cell(operation, Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)),
156      Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position, A, B, True{}),
157    WalkProof.cell_at_walk(operation, plan, position, A, B, True{})) :
158    Fact<CellOut(operation, plan, dl, dr, A, B, position, _)>
159  left_out(operation, plan, dl, dr, A, B, position, Array.get(F32, A, left_at(plan, position)), {==}, left_valid, right_valid)
160
161# Every cell hands both input arrays back.
162def cell_keeps(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +position: Nat,
163  inside: Bool, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
164  Fact<{Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, inside)) == (A, B) : Array<F32> & Array<F32>}>:
165  match inside:
166    case False{}:
167      Fact{
168        %Equal.sym(F32 & (Array<F32> & Array<F32>), cell_of(operation, plan, position, A, B, False{}),
169          Elementwise.cell(operation, Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)),
170            Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position, A, B, False{}),
171          WalkProof.cell_at_walk(operation, plan, position, A, B, False{})) :
172          {Pair.snd(F32, Array<F32> & Array<F32>, _) == (A, B) : Array<F32> & Array<F32>}
173        {==}}
174    case True{}:
175      Fact{Pair.fst({Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array<F32> & Array<F32>},
176        {Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{}))} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>},
177        {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> ->
178          CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}(
179          cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid)))}
180
181# A split hands each half both input arrays.
182def halves_equal(+dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, lp: Array<F32> & Array<F32>, rp: Array<F32> & Array<F32>,
183  -le: {lp == Array.clone(F32, A) : Array<F32> & Array<F32>}, -re: {rp == Array.clone(F32, B) : Array<F32> & Array<F32>},
184  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
185  Fact<({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.halves(lp, rp)) == (A, B) : Array<F32> & Array<F32>} &
186    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.halves(lp, rp)) == (A, B) : Array<F32> & Array<F32>})>:
187  (l1, l2) = lp
188  (r1, r2) = rp
189  Fact{(pair_equal(l1, r1, A, B,
190      {\{Fact: q => q} : Fact<({Pair.fst(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>})> -> {Pair.fst(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>}}(
191        clone_first(dl, A, A, (l1, l2), le, {==}, left_valid)),
192      {\{Fact: q => q} : Fact<({Pair.fst(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>})> -> {Pair.fst(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>}}(
193        clone_first(dr, B, B, (r1, r2), re, {==}, right_valid))),
194    pair_equal(l2, r2, A, B,
195      {\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>})> -> {Pair.snd(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>}}(
196        clone_second(dl, A, A, (l1, l2), le, {==}, left_valid)),
197      {\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>})> -> {Pair.snd(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>}}(
198        clone_second(dr, B, B, (r1, r2), re, {==}, right_valid))))}
199
200def split_equal(+dl: Nat, +dr: Nat, A: Array<F32>, B: Array<F32>, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
201  Fact<({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>} &
202    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>})>:
203  halves_equal(dl, dr, A, B, Array.clone(F32, A), Array.clone(F32, B), {==}, {==}, left_valid, right_valid)
204
205# An inside cell of the parallel build holds what `want` names there: the
206# generic law of `Parallel.build`, with the elementwise cell.
207def build_cell(+depth: Nat, +splits: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +count: Nat, +base: Nat,
208  +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +path: Model.Path(depth),
209  -inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool},
210  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
211  Fact<{Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) ==
212    want(operation, plan, dl, dr, A, B, Nat.add(Model.offset(depth, path), base)) : Maybe<&2, F32>}>:
213  +position = Nat.add(Model.offset(depth, path), base)
214  -split = {\{Fact: q => q} : Fact<({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>} &
215    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>})> ->
216    {Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>} &
217    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>}}(
218    split_equal(dl, dr, A, B, left_valid, right_valid))
219  Fact{Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path),
220    Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{}))},
221    want(operation, plan, dl, dr, A, B, position),
222    %inside : {Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) ==
223      Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, _))} : Maybe<&2, F32>}
224    {\{Generic.Fact: q => q} :
225      Generic.Fact<Generic.Cells(~Elementwise.Walk, ~Array<F32>, ~Array<F32>, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base,
226        Elementwise.build(depth, splits, operation, plan, count, base, A, B))> ->
227      Generic.Cells(~Elementwise.Walk, ~Array<F32>, ~Array<F32>, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base,
228        Elementwise.build(depth, splits, operation, plan, count, base, A, B))}(
229      Generic.build_cells(~Elementwise.Request, ~Elementwise.Walk, ~Array<F32>, ~Array<F32>, ~Elementwise.walk, ~Elementwise.split, ~Elementwise.cell_at,
230        Elementwise.Request{operation, plan}, (A, B), depth, splits, count, base, (A, B), {==},
231        at => inside => {\{Fact: q => q} : Fact<({Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array<F32> & Array<F32>})> ->
232          {Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array<F32> & Array<F32>}}(
233          cell_keeps(operation, plan, dl, dr, A, B, at, inside, left_valid, right_valid)),
234        Pair.fst({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>},
235          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>}, split),
236        Pair.snd({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>},
237          {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.split((A, B))) == (A, B) : Array<F32> & Array<F32>}, split)))(path),
238    Pair.snd({Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array<F32> & Array<F32>},
239      {Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{}))} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>},
240      {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> ->
241        CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}(
242        cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid))))}
243
244# What `take` hands back for one input: the copy for the build is balanced at
245# some depth and, below the input's element count, holds what the checked
246# observation of the input sees; the kept tensor observes like the input.
247def SourceReads(-input: Core.Dynamic, -depth: Nat, -copy: Array<F32>) -> Type:
248  @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Totality.dimensions(input))) == True{} : Bool} ->
249    {Model.observe(F32, depth, copy, Refinement.route(depth, index)) == Core.checked_observe_dynamic(input, index) : Maybe<&2, F32>}
250
251type Taken<-input: Core.Dynamic, -pair: Core.Dynamic & Array<F32>> is Data:
252  Taken{-depth: Nat, -balanced: Model.Balanced(F32, depth, Pair.snd(Core.Dynamic, Array<F32>, pair)),
253    -reads: SourceReads(input, depth, Pair.snd(Core.Dynamic, Array<F32>, pair)),
254    -retained: Totality.SameSource(input, Pair.fst(Core.Dynamic, Array<F32>, pair))}
255
256def owned_inspect(+shape: Shape.Shape, +depth: Nat, +length: Nat, property: Totality.Property, array: Array<F32>) -> Totality.Inspection:
257  match property:
258    case Totality.Dimensions{}:
259      Totality.Dims{Shape.dimensions(shape)}
260    case Totality.Checked{+index}:
261      Totality.Value{Lifecycle.checked_observe_array(depth, length, array, index)}
262    case Totality.Raw{+index}:
263      Totality.Value{Model.observe(F32, depth, array, Refinement.route(depth, index))}
264
265def owned_view(+shape: Shape.Shape, +depth: Nat, +length: Nat, property: Totality.Property, -array: Array<F32>,
266  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
267  -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
268  {Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}) ==
269    owned_inspect(shape, depth, length, property, array) : Totality.Inspection}:
270  match property:
271    case Totality.Dimensions{}:
272      {==}
273    case Totality.Checked{+index}:
274      {==}
275    case Totality.Raw{+index}:
276      {==}
277
278def observe_allowed_equal(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool,
279  accepted: {allowed == True{} : Bool}, matched: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
280  {Lifecycle.observe_allowed(depth, length, array, index, allowed) ==
281    Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}:
282  match allowed:
283    case False{}:
284      Empty.absurd({None{} == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}, Arith.clash(accepted))
285    case True{}:
286      %Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, matched) :
287        {Lifecycle.observe_index(depth, length, array, index, _) == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}
288      {==}
289
290def taken_owned(+shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, pair: Array<F32> & Array<F32>,
291  -same: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>}, -balanced: Model.Balanced(F32, depth, array),
292  -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
293  Taken<Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}},
294    Elementwise.take_owned(shape, depth, length, array, pair, same, balanced, valid, exact)>:
295  (kept, copy) = pair
296  -kept_same = {\{Fact: p => p} : Fact<({Pair.fst(Array<F32>, Array<F32>, (kept, copy)) == array : Array<F32>})> -> {kept == array : Array<F32>}}(
297    clone_first(depth, array, array, (kept, copy), same, {==}, balanced))
298  -copy_same = {\{Fact: p => p} : Fact<({Pair.snd(Array<F32>, Array<F32>, (kept, copy)) == array : Array<F32>})> -> {copy == array : Array<F32>}}(
299    clone_second(depth, array, array, (kept, copy), same, {==}, balanced))
300  Taken{depth,
301    {\{Fact: p => p} : Fact<(Model.Balanced(F32, depth, copy))> -> Model.Balanced(F32, depth, copy)}(transport_balanced(depth, copy, array, copy_same, balanced)),
302    index => inside => Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, copy, Refinement.route(depth, index)),
303      Model.observe(F32, depth, array, Refinement.route(depth, index)),
304      Lifecycle.observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length)),
305      Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)), copy, array, copy_same),
306      Equal.sym(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length)),
307        Model.observe(F32, depth, array, Refinement.route(depth, index)),
308        observe_allowed_equal(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length),
309          %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
310          inside,
311          Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index),
312            Route.index_complete(depth, length, index, valid,
313              %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
314              inside))))),
315    property => Equal.trans(Totality.Inspection,
316      Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, kept,
317        Certificates.clone_first(F32, depth, array, (kept, copy), same, balanced), valid}, exact}}),
318      owned_inspect(shape, depth, length, property, kept),
319      Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}),
320      owned_view(shape, depth, length, property, kept, Certificates.clone_first(F32, depth, array, (kept, copy), same, balanced), valid, exact),
321      Equal.trans(Totality.Inspection, owned_inspect(shape, depth, length, property, kept), owned_inspect(shape, depth, length, property, array),
322        Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}),
323        Equal.cong(Array<F32>, Totality.Inspection, a => owned_inspect(shape, depth, length, property, a), kept, array, kept_same),
324        Equal.sym(Totality.Inspection, Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}),
325          owned_inspect(shape, depth, length, property, array), owned_view(shape, depth, length, property, array, balanced, valid, exact))))}
326
327def taken(dynamic: Core.Dynamic) -> Taken<dynamic, Elementwise.take(dynamic)>:
328  Core.Packed{+shape, Core.TTensor{storage, exact}} = dynamic
329  match storage:
330    case Storage.Empty{}:
331      Taken{0n, Unit{},
332        index => inside => Empty.absurd({Model.observe(F32, 0n, Array.new(F32, 0n, 0.0), Refinement.route(0n, index)) ==
333          Core.checked_observe_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index) : Maybe<&2, F32>},
334          Arith.lt_zero(U32.to_nat(index),
335            %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
336            inside)),
337        property => {==}}
338    case Storage.Owned{+depth, +length, array, balanced, valid}:
339      taken_owned(shape, depth, length, array, Array.clone(F32, array), {==}, balanced, valid, exact)
340
341def walk_pair(+plan: Shape.BroadcastPlan,
342  +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>,
343  +value: Nat, +bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) ->
344  {(Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, map, Shape.FIndex{value, bound})),
345    Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, map, Shape.FIndex{value, bound}))) ==
346    (U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value)),
347      U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value))) : U32 & U32}:
348  match map:
349    case Shape.Indexed{rows, exact}:
350      {==}
351    case Shape.Unindexed{zero}:
352      Empty.absurd({(Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, Shape.Unindexed{zero}, Shape.FIndex{value, bound})),
353        Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, Shape.Unindexed{zero}, Shape.FIndex{value, bound}))) == (U32.from_nat(0n), U32.from_nat(0n)) : U32 & U32},
354        Flat.hollow(Shape.output_shape(plan), value, zero, bound))
355
356def left_walk_bound(+plan: Shape.BroadcastPlan,
357  +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>,
358  +value: Nat, +bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) ->
359  {True{} == Nat.is_lt(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value),
360    Shape.elements(Shape.left_shape(plan))) : Bool}:
361  match map:
362    case Shape.Indexed{rows, exact}:
363      Flat.left_bound(plan, rows, exact, value, bound)
364    case Shape.Unindexed{zero}:
365      Empty.absurd({True{} == Nat.is_lt(0n, Shape.elements(Shape.left_shape(plan))) : Bool}, Flat.hollow(Shape.output_shape(plan), value, zero, bound))
366
367def right_walk_bound(+plan: Shape.BroadcastPlan,
368  +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>,
369  +value: Nat, +bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) ->
370  {True{} == Nat.is_lt(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value),
371    Shape.elements(Shape.right_shape(plan))) : Bool}:
372  match map:
373    case Shape.Indexed{rows, exact}:
374      Flat.right_bound(plan, rows, exact, value, bound)
375    case Shape.Unindexed{zero}:
376      Empty.absurd({True{} == Nat.is_lt(0n, Shape.elements(Shape.right_shape(plan))) : Bool}, Flat.hollow(Shape.output_shape(plan), value, zero, bound))
377
378# Below the output's element count, `expected` reads the inputs at the cells
379# the build's index walks name.
380def decided_walks(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic, +position: Nat,
381  decision: Shape.BoolCase<Nat.is_lt(position, Shape.elements(Shape.output_shape(plan)))>,
382  +bound: {True{} == Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))) : Bool}) ->
383  {Elementwise.expected_indices(operation, left, right, Elementwise.flat_input_indices(plan, Shape.flat_checked.finish(Shape.output_shape(plan), position, decision))) ==
384    Elementwise.expected_left(operation, right,
385      U32.from_nat(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)),
386      Core.checked_observe_dynamic(left,
387        U32.from_nat(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)))) : Maybe<&2, F32>}:
388  match decision:
389    case Shape.BFalse{equal}:
390      Empty.absurd({None{} ==
391        Elementwise.expected_left(operation, right,
392          U32.from_nat(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)),
393          Core.checked_observe_dynamic(left,
394            U32.from_nat(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)))) : Maybe<&2, F32>},
395        Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))), True{}, equal,
396          Equal.sym(Bool, True{}, Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))), bound))))
397    case Shape.BTrue{equal}:
398      Equal.cong(U32 & U32, Maybe<&2, F32>, indices => Elementwise.expected_indices(operation, left, right, Done{indices}),
399        (Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, Shape.index_map(plan), Shape.FIndex{position, equal})),
400          Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, Shape.index_map(plan), Shape.FIndex{position, equal}))),
401        (U32.from_nat(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)),
402          U32.from_nat(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))),
403        walk_pair(plan, Shape.index_map(plan), position, equal))
404
405def pick_expected(+operation: Elementwise.Operation, value: Maybe<&2, F32>, -right: Core.Dynamic, -right_index: U32, -other: Maybe<&2, F32>,
406  same: {other == Core.checked_observe_dynamic(right, right_index) : Maybe<&2, F32>}) ->
407  {pick(operation, value, other) == Elementwise.expected_left(operation, right, right_index, value) : Maybe<&2, F32>}:
408  match value:
409    case None{}:
410      {==}
411    case Some{value}:
412      %same : {Elementwise.expected_right(operation, value, other) == Elementwise.expected_right(operation, value, _) : Maybe<&2, F32>}
413      {==}
414
415def add_zero_right(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
416  match number:
417    case 0n:
418      {==}
419    case 1n+p:
420      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero_right(p))
421
422def output_offset(+depth: Nat, +length: Nat, +index: U32, +valid: {Storage.bounds(depth, length) == True{} : Bool},
423  +inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) ->
424  {U32.to_nat(index) == Model.offset(depth, Refinement.route(depth, index)) : Nat}:
425  +rest = Arith.and_right(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid)
426  Route.route_offset(depth, index,
427    Arith.and_left(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid),
428    Arith.lt_le_trans(U32.to_nat(index), length, Model.capacity(depth), inside,
429      Arith.and_right(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth)), rest)))
430
431def word_exact(+shape: Shape.Shape, +cursor: Nat, within: {Nat.is_le(cursor, Shape.elements(shape)) == True{} : Bool}) ->
432  {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
433  WordConversion.natural_word_exact(cursor, Shape.count(shape),
434    %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) :
435      {Nat.is_le(cursor, _) == True{} : Bool}
436    within)
437
438# A cell an index walk names lies inside the input it reads.
439def side_inside(-input: Core.Dynamic, +side: Shape.Shape, +walk: Nat,
440  fits: {Totality.dimensions(input) == Shape.dimensions(side) : List<&2, U32>},
441  +bound: {True{} == Nat.is_lt(walk, Shape.elements(side)) : Bool}) ->
442  {Nat.is_lt(U32.to_nat(U32.from_nat(walk)), Shape.logical_numel(Totality.dimensions(input))) == True{} : Bool}:
443  %Equal.sym(Nat, U32.to_nat(U32.from_nat(walk)), walk,
444    word_exact(side, walk, WordConversion.lt_le(walk, Shape.elements(side), Equal.sym(Bool, True{}, Nat.is_lt(walk, Shape.elements(side)), bound)))) :
445    {Nat.is_lt(_, Shape.logical_numel(Totality.dimensions(input))) == True{} : Bool}
446  %Equal.sym(List<&2, U32>, Totality.dimensions(input), Shape.dimensions(side), fits) :
447    {Nat.is_lt(walk, Shape.logical_numel(_)) == True{} : Bool}
448  %Shape.elements_exact(side) : {Nat.is_lt(walk, _) == True{} : Bool}
449  Equal.sym(Bool, True{}, Nat.is_lt(walk, Shape.elements(side)), bound)
450
451def output_inside(+plan: Shape.BroadcastPlan, +length: Nat, +index: U32,
452  +exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat},
453  +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) -> {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}:
454  %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
455  Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound))
456
457def output_bound(+plan: Shape.BroadcastPlan, +index: U32, +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) ->
458  {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) : Bool}:
459  %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.numel(Shape.extents(Shape.output_shape(plan))), Shape.elements_exact(Shape.output_shape(plan))) :
460    {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
461  Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound)
462
463def output_position(+depth: Nat, +length: Nat, +index: U32, +valid: {Storage.bounds(depth, length) == True{} : Bool},
464  +inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) ->
465  {Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n) == U32.to_nat(index) : Nat}:
466  Equal.trans(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index), add_zero_right(Model.offset(depth, Refinement.route(depth, index))),
467    Equal.sym(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)), output_offset(depth, length, index, valid, inside)))
468
469# At an index below the output's element count, the parallel build holds the
470# value `expected` names there.
471def output_cell(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
472  +valid: {Storage.bounds(depth, length) == True{} : Bool}, +exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat},
473  -left: Core.Dynamic, -right: Core.Dynamic, la: Array<F32>, ra: Array<F32>, +dl: Nat, +dr: Nat,
474  -left_valid: Model.Balanced(F32, dl, la), -right_valid: Model.Balanced(F32, dr, ra),
475  -left_reads: SourceReads(left, dl, la), -right_reads: SourceReads(right, dr, ra),
476  +left_fits: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
477  +right_fits: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>},
478  +index: U32, +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) ->
479  Fact<{Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}>:
480  +inside = output_inside(plan, length, index, exact, bound)
481  +within = output_bound(plan, index, bound)
482  +position = output_position(depth, length, index, valid, inside)
483  Fact{Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)), want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)), Elementwise.expected(operation, plan, left, right, index),
484    {\{Fact: q => q} : Fact<({Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)) : Maybe<&2, F32>})> ->
485      {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)) : Maybe<&2, F32>}}(
486      build_cell(depth, Elementwise.splits(depth), operation, plan, length, 0n, dl, dr, la, ra, Refinement.route(depth, index),
487        %Equal.sym(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), U32.to_nat(index), position) : {Nat.is_lt(_, length) == True{} : Bool}
488        inside, left_valid, right_valid)),
489    Equal.trans(Maybe<&2, F32>, want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)), want(operation, plan, dl, dr, la, ra, U32.to_nat(index)), Elementwise.expected(operation, plan, left, right, index),
490      Equal.cong(Nat, Maybe<&2, F32>, at => want(operation, plan, dl, dr, la, ra, at), Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), U32.to_nat(index), position),
491      Equal.trans(Maybe<&2, F32>, want(operation, plan, dl, dr, la, ra, U32.to_nat(index)), Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index)))))), Elementwise.expected(operation, plan, left, right, index),
492        pick_expected(operation, Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index))))), right, U32.from_nat(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), U32.to_nat(index))), Model.observe(F32, dr, ra, Refinement.route(dr, U32.from_nat(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), U32.to_nat(index))))),
493          right_reads(U32.from_nat(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), U32.to_nat(index))))(side_inside(right, Shape.right_shape(plan), 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), U32.to_nat(index)), right_fits,
494            right_walk_bound(plan, Shape.index_map(plan), U32.to_nat(index), within)))),
495        Equal.trans(Maybe<&2, F32>, Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index)))))), Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Core.checked_observe_dynamic(left, U32.from_nat(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), U32.to_nat(index))))), Elementwise.expected(operation, plan, left, right, index),
496          Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, value => Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), value), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index))))), Core.checked_observe_dynamic(left, U32.from_nat(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), U32.to_nat(index)))),
497            left_reads(U32.from_nat(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), U32.to_nat(index))))(side_inside(left, Shape.left_shape(plan), 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), U32.to_nat(index)), left_fits,
498              left_walk_bound(plan, Shape.index_map(plan), U32.to_nat(index), within)))),
499          Equal.sym(Maybe<&2, F32>, Elementwise.expected(operation, plan, left, right, index), Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Core.checked_observe_dynamic(left, U32.from_nat(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), U32.to_nat(index))))),
500            decided_walks(operation, plan, left, right, U32.to_nat(index), Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan)))), within))))))}
501
502def output_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
503  -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat},
504  -left: Core.Dynamic, -right: Core.Dynamic, taken_left: Core.Dynamic & Array<F32>, taken_right: Core.Dynamic & Array<F32>,
505  -left_taken: Taken<left, taken_left>, -right_taken: Taken<right, taken_right>,
506  +left_fits: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
507  +right_fits: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}) ->
508  Elementwise.MappingModel<operation, plan, left, right, Elementwise.parallel_output(operation, plan, depth, length, valid, exact, taken_left, taken_right)>:
509  (kept_left, la) = taken_left
510  (kept_right, ra) = taken_right
511  Elementwise.MappingModel{index => bound =>
512    {\{Taken: dl => left_valid => left_reads => left_same =>
513      {\{Taken: dr => right_valid => right_reads => right_same =>
514        {\{Fact: equal => equal} : Fact<({Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>})> -> {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}(
515          output_cell(operation, plan, depth, length, valid, exact, left, right, la, ra, dl, dr, left_valid, right_valid, left_reads, right_reads,
516            left_fits, right_fits, index, bound))} : Taken<right, (kept_right, ra)> -> {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}(right_taken)} : Taken<left, (kept_left, la)> -> {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}(left_taken)}
517
518def allocated_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic,
519  result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>,
520  +left_fits: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
521  +right_fits: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}) ->
522  Elementwise.MappingModel<operation, plan, left, right, Elementwise.parallel_allocated(operation, plan, left, right, result)>:
523  match result:
524    case Fail{error}:
525      Elementwise.MappingModel{Unit{}}
526    case Done{Core.TTensor{storage, exact}}:
527      match storage:
528        case Storage.Empty{}:
529          Elementwise.MappingModel{index => bound => Empty.absurd(
530            {Core.observe_dynamic(Core.Packed{Shape.output_shape(plan), Core.TTensor{Storage.Empty{}, exact}}, index) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>},
531            Arith.lt_zero(U32.to_nat(index),
532              %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
533              Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound))))}
534        case Storage.Owned{+depth, +length, array, balanced, valid}:
535          output_mapping(operation, plan, depth, length, valid, exact, left, right, Elementwise.take(left), Elementwise.take(right),
536            taken(left), taken(right), left_fits, right_fits)
537
538def planned_mapping(+operation: Elementwise.Operation, +left_shape: Shape.Shape, +right_shape: Shape.Shape,
539  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, left: Core.Tensor<left_shape>, right: Core.Tensor<right_shape>,
540  -same: {result == Elementwise.plan_for(Core.Packed{left_shape, left}, Core.Packed{right_shape, right}) : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>},
541  +sources: {ShapeLaws.planned_dimensions(left_shape, right_shape, result) == (Shape.dimensions(left_shape), Shape.dimensions(right_shape)) : List<&2, U32> & List<&2, U32>}) ->
542  Elementwise.BinaryModel<operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_planned(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, result)>:
543  match result:
544    case Fail{error}:
545      Elementwise.BinaryModel{
546        %same : Elementwise.PlannedMeaning(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_planned(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Fail{error}), _)
547        Unit{}}
548    case Done{+plan}:
549      Elementwise.BinaryModel{
550        %same : Elementwise.PlannedMeaning(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_planned(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Done{plan}), _)
551        {\{Elementwise.MappingModel: mapping => mapping} :
552          Elementwise.MappingModel<operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_allocated(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0))> -> Elementwise.SuccessfulMapping(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_allocated(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0)))}(
553            allocated_mapping(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0),
554              Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(left_shape),
555                Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>),
556                  (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left_shape), Shape.dimensions(right_shape)), sources)),
557              Equal.sym(List<&2, U32>, Shape.dimensions(Shape.right_shape(plan)), Shape.dimensions(right_shape),
558                Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>),
559                  (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left_shape), Shape.dimensions(right_shape)), sources))))}
560
561# The parallel `binary` meets the same `BinaryModel` as the sequential loop.
562def binary_mapping(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic) ->
563  Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
564  Core.Packed{+left_shape, left_tensor} = left
565  Core.Packed{+right_shape, right_tensor} = right
566  planned_mapping(operation, left_shape, right_shape, Shape.broadcast_checked(left_shape, right_shape), left_tensor, right_tensor, {==},
567    PlanProof.broadcast_checked_plan(left_shape, right_shape))