1	import Base
2	
3	import ../shape/core.bend as Shape
4	
5	import ../shape/LAWS.bend as ShapeLaws
6	
7	import ../shape/plan_proofs.bend as PlanProof
8	
9	import ../shape/nat_proofs.bend as Nats
10	
11	import ../storage/arith.bend as Arith
12	
13	import ../storage/main.bend as Storage
14	
15	import ../tensor/core.bend as Core
16	
17	import ../tensor/layout.bend as Layout
18	
19	import ../tensor/lifecycle.bend as Lifecycle
20	
21	import ../tensor/elementwise.bend as Elementwise
22	
23	import ../tensor/elementwise_totality.bend as Totality
24	
25	import ../tensor/elementwise_PROOF.bend as ElementwiseProof
26	
27	import ../tensor/core_PROOF.bend as CoreProof
28	
29	import ../tensor/transform_PROOF.bend as TransformProof
30	
31	import ../tensor/transform_totality.bend as TransformTotality
32	
33	import ../tensor/projection_LAWS.bend as Projection
34	
35	import ../tensor/projection_PROOF.bend as ProjectionProof
36	
37	import ../tensor/allocation_spec.bend as Allocation
38	
39	import ../tensor/allocation_PROOF.bend as AllocationProof
40	
41	import ../tensor/construction_contract_PROOF.bend as ConstructionProof
42	
43	import ../tensor/word_conversion.bend as Conversion
44	
45	import ../tensor/observation.bend as Observation
46	
47	import ./reduce.bend as Reduce
48	
49	import ./reduce_LAWS.bend as Laws
50	
51	import ../storage/model.bend as Model
52	
53	import ../storage/refinement.bend as Refinement
54	
55	import ../storage/route.bend as Route
56	
57	import ../tensor/matmul.bend as Matrix
58	
59	import ../tensor/matrix_index_proof.bend as MatrixIndex
60	
61	import ../tensor/elementwise_parallel_proof.bend as Parallel
62	
63	import ./reduce_parallel_proof.bend as ReduceParallel
64	
65	import ../tensor/matmul_PROOF.bend as MatmulProof
66	
67	type Holds<-P: Type> is Data:
68	  Holds{-proof: P}
69	
70	def inspection_value(value: Totality.Inspection) -> Maybe<&2, F32>:
71	  match value:
72	    case Totality.Dims{dimensions}:
73	      None{}
74	    case Totality.Value{value}:
75	      value
76	
77	def same_checked(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained), +index: U32) ->
78	  Holds<{Core.checked_observe_dynamic(retained, index) == Core.checked_observe_dynamic(original, index) : Maybe<&2, F32>}>:
79	  Holds{Equal.cong(Totality.Inspection, Maybe<&2, F32>, inspection_value,
80	    Totality.inspect(Totality.Checked{index}, retained), Totality.inspect(Totality.Checked{index}, original), same(Totality.Checked{index}))}
81	
82	def same_dimensions(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained)) ->
83	  Holds<{Totality.dimensions(retained) == Totality.dimensions(original) : List<&2, U32>}>:
84	  Holds{Equal.cong(Totality.Inspection, List<&2, U32>, ElementwiseProof.inspection_dimensions,
85	    Totality.inspect(Totality.Dimensions{}, retained), Totality.inspect(Totality.Dimensions{}, original), same(Totality.Dimensions{}))}
86	
87	def same_trans(-a: Core.Dynamic, -b: Core.Dynamic, -c: Core.Dynamic,
88	  -ab: Totality.SameSource(a, b), -bc: Totality.SameSource(b, c)) -> Holds<Totality.SameSource(a, c)>:
89	  Holds{property => Equal.trans(Totality.Inspection, Totality.inspect(property, c), Totality.inspect(property, b), Totality.inspect(property, a),
90	    bc(property), ab(property))}
91	
92	def Inv(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +target: Shape.Shape, +cursor: Nat, output: Core.Tensor<target>) -> Type:
93	  @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
94	    {Core.checked_observe(target, output, index) == Laws.fiber(plan, values, index, cursor) : Maybe<&2, F32>}
95	
96	def update_written(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
97	  meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
98	  {Core.checked_observe(shape, output, index) == Some{value} : Maybe<&2, F32>}:
99	  (checked, rest) = meaning
100	  (observed, frame) = rest
101	  observed
102	
103	def update_frame(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
104	  meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
105	  @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
106	    @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
107	      Core.ObservationChecked(Core.Packed{shape, output}, other) &
108	        {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}:
109	  (checked, rest) = meaning
110	  (observed, frame) = rest
111	  frame
112	
113	def frame_equal(-shape: Shape.Shape, -output: Core.Tensor<shape>, -original: Core.Tensor<shape>, -other: U32,
114	  pair: Core.ObservationChecked(Core.Packed{shape, output}, other) &
115	    {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
116	  {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}:
117	  (checked, equal) = pair
118	  equal
119	
120	def listed_kept(-original: Core.Dynamic, -retained: Core.Dynamic, +values: List<&2, F32>,
121	  -same: Totality.SameSource(original, retained), -listed: Laws.Listed(original, values)) -> Holds<Laws.Listed(retained, values)>:
122	  Holds{source => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(retained, source), Core.checked_observe_dynamic(original, source),
123	    Laws.word_at(values, U32.to_nat(source)),
124	    {\{Holds: proof => proof} : Holds<{Core.checked_observe_dynamic(retained, source) == Core.checked_observe_dynamic(original, source) : Maybe<&2, F32>}> ->
125	      {Core.checked_observe_dynamic(retained, source) == Core.checked_observe_dynamic(original, source) : Maybe<&2, F32>}}(
126	      same_checked(original, retained, same, source)),
127	    listed(source))}
128	
129	def zero_inv(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +target: Shape.Shape, output: Core.Tensor<target>,
130	  -same: {Done{output} == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>}) ->
131	  Holds<Inv(plan, values, target, 0n, output)>:
132	  Holds{index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe(target, output, index),
133	    Core.read_value(target, Core.read_flat(target, output, index)), Some{0.0},
134	    Equal.sym(Maybe<&2, F32>, Core.read_value(target, Core.read_flat(target, output, index)), Core.checked_observe(target, output, index),
135	      {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<target, output, index> ->
136	        {Core.read_value(target, Core.read_flat(target, output, index)) == Core.checked_observe(target, output, index) : Maybe<&2, F32>}}(
137	        Core.source_read_model(target, output, index))),
138	    %Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{output}, Core.new(target, 0.0), same) :
139	      {Observation.point(target, index, _) == Some{0.0} : Maybe<&2, F32>}
140	    ConstructionProof.point_value(target, 0.0, index, inside))}
141	
142	def mapping_values(-input: Core.Dynamic, -target: Shape.Shape, -plan: Shape.BroadcastPlan, -output: Core.Dynamic,
143	  model: {Totality.dimensions(output) == Shape.dimensions(target) : List<&2, U32>} &
144	    (@+values: List<&2, F32> -> @-listed: Laws.Listed(input, values) ->
145	      @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
146	        {Core.checked_observe_dynamic(output, index) == Laws.planned_fiber(values, index, Shape.logical_numel(Totality.dimensions(input)), Done{plan}) : Maybe<&2, F32>})) ->
147	  @+values: List<&2, F32> -> @-listed: Laws.Listed(input, values) ->
148	    @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
149	      {Core.checked_observe_dynamic(output, index) == Laws.planned_fiber(values, index, Shape.logical_numel(Totality.dimensions(input)), Done{plan}) : Maybe<&2, F32>}:
150	  (dimensions, mapped) = model
151	  mapped
152	
153	def output_count(+shape: Shape.Shape, +plan: Shape.BroadcastPlan,
154	  -equal: {True{} == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool}) ->
155	  Holds<{Shape.elements(Shape.output_shape(plan)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
156	  Holds{Equal.trans(Nat, Shape.elements(Shape.output_shape(plan)), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))),
157	    Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(Shape.output_shape(plan)),
158	    Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape),
159	      TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape), equal)))}
160	
161	def rank_of(+shape: Shape.Shape) -> Shape.LE(Shape.rank_dimensions(Shape.dimensions(shape)), 4n):
162	  match shape:
163	    case Shape.SShape{dims, size, exact, rank_bound, capacity_bound}:
164	      rank_bound
165	
166	def capacity_of(+shape: Shape.Shape) -> Shape.LE(Shape.logical_numel(Shape.dimensions(shape)), 1048576n):
167	  match shape:
168	    case Shape.SShape{dims, size, exact, rank_bound, capacity_bound}:
169	      capacity_bound
170	
171	# The parallel reduction keeps the contribution: it hands back the kept
172	# half of the contribution's clone, which observes like the contribution.
173	
174	def indexed_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
175	  +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
176	  -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
177	  map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>) ->
178	  Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map)>:
179	  match map:
180	    case Shape.Unindexed{zero}:
181	      Laws.Retained{property => {==}}
182	    case Shape.Indexed{rows, same}:
183	      MatmulProof.take_lift(shape, tensor,
184	        pair => Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows)>,
185	        kept => copy => taken => Laws.Retained{{\{Parallel.Taken: depth => balanced => reads => retained => retained} :
186	          Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, copy)> -> Totality.SameSource(Core.Packed{shape, tensor}, Core.Packed{shape, kept})}(taken)})
187	
188	def parallel_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
189	  result: Result<&2, &1, Core.Error, Core.Tensor<target>>) ->
190	  Laws.Retained<Core.Packed{shape, tensor}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, result)>:
191	  match result:
192	    case Fail{error}:
193	      Laws.Retained{property => {==}}
194	    case Done{Core.TTensor{storage, exact}}:
195	      match storage:
196	        case Storage.Empty{}:
197	          Laws.Retained{property => {==}}
198	        case Storage.Owned{+depth, +length, array, balanced, valid}:
199	          indexed_retains(shape, tensor, target, plan, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, depth, length,
200	            valid, exact, Shape.index_map(plan))
201	
202	def fitted_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool) ->
203	  Laws.Retained<Core.Packed{shape, tensor}, Reduce.fitted(Core.Packed{shape, tensor}, target, plan, same)>:
204	  match same:
205	    case False{}:
206	      Laws.Retained{property => {==}}
207	    case True{}:
208	      parallel_retains(shape, tensor, target, plan, Core.new(target, 0.0))
209	
210	def planned_retains(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
211	  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>) ->
212	  Laws.Retained<Core.Packed{shape, tensor}, Reduce.planned(shape, tensor, target, result)>:
213	  match result:
214	    case Fail{error}:
215	      Laws.Retained{property => {==}}
216	    case Done{+plan}:
217	      fitted_retains(shape, tensor, target, plan,
218	        Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)))
219	
220	def Laws.reduce_retains_input(input, target):
221	  Core.Packed{+shape, tensor} = input
222	  planned_retains(shape, tensor, target, Shape.broadcast_checked(target, shape))
223	
224	# The parallel reduction's mapping: every target cell of the parallel build
225	# holds the masked fiber sum over any list that lists the contribution.
226	
227	def parallel_build(+plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat, +rows: List<&2, Shape.Row>, array: Array<F32>) -> Array<F32>:
228	  Reduce.build(depth, Reduce.splits(plan, depth, length), rows, Shape.extents(Shape.output_shape(plan)), length, 0n, array)
229	
230	def rows_cell(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
231	  -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
232	  +rows: List<&2, Shape.Row>,
233	  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
234	  -array: Array<F32>, +d: Nat, -balanced: Model.Balanced(F32, d, array), -reads: Parallel.SourceReads(Core.Packed{shape, tensor}, d, array),
235	  +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
236	  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
237	  +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
238	  +values: List<&2, F32>, -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +index: U32,
239	  +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) ->
240	  Holds<{Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
241	    Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}>:
242	  +t = U32.to_nat(index)
243	  +extents = Shape.extents(Shape.output_shape(plan))
244	  +splits = Reduce.splits(plan, depth, length)
245	  -built = parallel_build(plan, depth, length, rows, array)
246	  -inside_length : {Nat.is_lt(t, length) == True{} : Bool} =
247	    %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(target)), exact) : {Nat.is_lt(t, _) == True{} : Bool}
248	    inside
249	  +path = Refinement.route(depth, index)
250	  Holds{{\{ReduceParallel.CellAt: word => observed => words => seen => total =>
251	    Equal.trans(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, built, index, Nat.is_lt(t, length)),
252	      Model.observe(F32, depth, built, path), Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))),
253	      Parallel.observe_allowed_equal(depth, length, built, index, Nat.is_lt(t, length), inside_length,
254	        Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index), Route.index_complete(depth, length, index, valid, inside_length))),
255	      %Equal.sym(Maybe<&2, F32>, Model.observe(F32, depth, built, path), Some{word}, observed) :
256	        {_ == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}
257	      %Equal.sym(F32, word, ReduceParallel.fsum(words, 0.0), total) :
258	        {Some{_} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}
259	      %count : {Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, _) : Maybe<&2, F32>}
260	      {\{Parallel.Fact: p => p} :
261	        Parallel.Fact<{Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}> ->
262	        {Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}}(
263	        ReduceParallel.cell_value(plan, rows, rows_exact, values, index, d, array, words, seen,
264	          %Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(target), left) :
265	            {Nat.is_lt(t, Shape.logical_numel(_)) == True{} : Bool}
266	          inside,
267	          position => below =>
268	            +shaped : {Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool} =
269	              %right : {Nat.is_lt(position, Shape.logical_numel(_)) == True{} : Bool}
270	              below
271	            +exact_word = MatrixIndex.word_exact(position, shape, shaped)
272	            Equal.trans(Maybe<&2, F32>, Model.observe(F32, d, array, Refinement.route(d, U32.from_nat(position))),
273	              Core.checked_observe_dynamic(Core.Packed{shape, tensor}, U32.from_nat(position)), Laws.word_at(values, position),
274	              reads(U32.from_nat(position))(
275	                %Equal.sym(Nat, U32.to_nat(U32.from_nat(position)), position, exact_word) :
276	                  {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
277	                shaped),
278	              %exact_word :
279	                {Core.checked_observe_dynamic(Core.Packed{shape, tensor}, U32.from_nat(position)) == Laws.word_at(values, _) : Maybe<&2, F32>}
280	              listed(U32.from_nat(position))))))} :
281	    ReduceParallel.CellAt<d, array, rows, extents, t, Model.observe(F32, depth, built, path)> ->
282	    {Lifecycle.observe_allowed(depth, length, built, index, Nat.is_lt(t, length)) ==
283	      Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(
284	    %inside_length : ReduceParallel.CellSpec(d, array, rows, extents, t, _, Model.observe(F32, depth, built, path))
285	    %Parallel.output_position(depth, length, index, valid, inside_length) :
286	      ReduceParallel.CellIs(d, array, rows, extents, length, _, Model.observe(F32, depth, built, path))
287	    {\{Parallel.Fact: p => p} :
288	      Parallel.Fact<ReduceParallel.Cells(depth, d, array, rows, extents, length, 0n, built)> -> ReduceParallel.Cells(depth, d, array, rows, extents, length, 0n, built)}(
289	      ReduceParallel.build_cells(depth, splits, d, array, rows, extents, length, 0n, array, {==}, balanced))(path))}
290	
291	def rows_mapping(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
292	  -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
293	  -kept: Core.Tensor<shape>, -array: Array<F32>, -taken: Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)>,
294	  +rows: List<&2, Shape.Row>,
295	  +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
296	  +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
297	  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
298	  +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
299	  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan},
300	    Reduce.parallel_rows(plan, target, depth, length, valid, exact, (Core.Packed{shape, kept}, array), rows))>:
301	  Holds{({==}, values => listed => index => inside =>
302	    {\{Parallel.Taken: d => balanced => reads => retained =>
303	      {\{Holds: proof => proof} :
304	        Holds<{Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
305	          Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}> ->
306	        {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
307	          Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(
308	        rows_cell(shape, tensor, target, plan, depth, length, valid, exact, rows, rows_exact, array, d, balanced, reads, left, right, count,
309	          values, listed, index, inside))} :
310	      Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)> ->
311	      {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
312	        Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(taken))}
313	
314	def indexed_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
315	  +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
316	  -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
317	  map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>,
318	  -same: {Done{output} == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>},
319	  +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
320	  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
321	  +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
322	  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan},
323	    Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map))>:
324	  match map:
325	    case Shape.Unindexed{zero}:
326	      Holds{({==}, values => listed => index => inside =>
327	        %Equal.trans(Nat, 0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Shape.logical_numel(Shape.dimensions(shape)), zero, count) :
328	          {Core.checked_observe(target, output, index) == Laws.fiber(plan, values, index, _) : Maybe<&2, F32>}
329	        {\{Holds: proof => proof} : Holds<Inv(plan, values, target, 0n, output)> -> Inv(plan, values, target, 0n, output)}(
330	          zero_inv(plan, values, target, output, same))(index)(inside))}
331	    case Shape.Indexed{rows, same_rows}:
332	      MatmulProof.take_lift(shape, tensor,
333	        pair => Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows))>,
334	        kept => copy => taken => rows_mapping(shape, tensor, target, plan, depth, length, valid, exact, kept, copy,
335	          taken, rows, same_rows, left, right, count))
336	
337	def parallel_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
338	  result: Result<&2, &1, Core.Error, Core.Tensor<target>>,
339	  -same: {result == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>},
340	  +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
341	  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
342	  +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
343	  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, result))>:
344	  match result:
345	    case Fail{error}:
346	      Holds{Unit{}}
347	    case Done{Core.TTensor{storage, exact}}:
348	      match storage:
349	        case Storage.Empty{}:
350	          Holds{({==}, values => listed => index => inside =>
351	            Empty.absurd({Core.checked_observe(target, Core.TTensor{Storage.Empty{}, exact}, index) ==
352	              Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>},
353	              Arith.lt_zero(U32.to_nat(index),
354	                %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(target)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
355	                inside)))}
356	        case Storage.Owned{+depth, +length, array, balanced, valid}:
357	          indexed_mapping(shape, tensor, target, plan, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, depth, length,
358	            valid, exact, Shape.index_map(plan), same, left, right, count)
359	
360	def output_numel(+shape: Shape.Shape, +plan: Shape.BroadcastPlan,
361	  -equal: {True{} == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool}) ->
362	  Holds<{Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
363	  Holds{Equal.cong(List<&2, U32>, Nat, Shape.logical_numel, Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape),
364	    TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape), equal))}
365	
366	def fitted_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool,
367	  -decided: {same == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool},
368	  -left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
369	  -right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}) ->
370	  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.fitted(Core.Packed{shape, tensor}, target, plan, same))>:
371	  match same:
372	    case False{}:
373	      Holds{Unit{}}
374	    case True{}:
375	      Holds{{\{Holds: proof => proof} :
376	        Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, Core.new(target, 0.0)))> ->
377	        Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, Core.new(target, 0.0)))}(
378	        parallel_mapping(shape, tensor, target, plan, Core.new(target, 0.0), {==}, left, right,
379	          {\{Holds: proof => proof} :
380	            Holds<{Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}> ->
381	            {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}}(
382	            output_numel(shape, plan, decided))))}
383	
384	def planned_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
385	  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
386	  -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>}) ->
387	  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, result, Reduce.planned(shape, tensor, target, result))>:
388	  match result:
389	    case Fail{error}:
390	      Holds{Unit{}}
391	    case Done{+plan}:
392	      fitted_mapping(shape, tensor, target, plan, Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), {==},
393	        Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>),
394	          (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(target), Shape.dimensions(shape)), sources),
395	        Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>),
396	          (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(target), Shape.dimensions(shape)), sources))
397	
398	def Laws.reduce_mapping(input, target):
399	  Core.Packed{+shape, tensor} = input
400	  Laws.MappingModel{
401	    {\{Holds: proof => proof} :
402	      Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Shape.broadcast_checked(target, shape),
403	        Reduce.planned(shape, tensor, target, Shape.broadcast_checked(target, shape)))> ->
404	      Laws.Mapping(Core.Packed{shape, tensor}, target, Reduce.reduce_to(Core.Packed{shape, tensor}, target))}(
405	      planned_mapping(shape, tensor, target, Shape.broadcast_checked(target, shape), PlanProof.broadcast_checked_plan(target, shape)))}
406	
407	# The parallel reduction succeeds once the target is allocated.
408	
409	def indexed_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, output: Core.Tensor<target>,
410	  +depth: Nat, +length: Nat, -valid: {Storage.bounds(depth, length) == True{} : Bool},
411	  -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
412	  map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>) ->
413	  Laws.Success<Reduce.parallel_indexed(Core.Packed{shape, tensor}, target, plan, output, depth, length, valid, exact, map)>:
414	  match map:
415	    case Shape.Unindexed{zero}:
416	      Laws.Success{{==}}
417	    case Shape.Indexed{rows, same}:
418	      MatmulProof.take_lift(shape, tensor, pair => Laws.Success<Reduce.parallel_rows(plan, target, depth, length, valid, exact, pair, rows)>,
419	        kept => copy => taken => Laws.Success{{==}})
420	
421	def parallel_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
422	  result: Result<&2, &1, Core.Error, Core.Tensor<target>>, -done: Allocation.TensorDone<target, result>) ->
423	  Laws.Success<Reduce.parallel_allocated(Core.Packed{shape, tensor}, target, plan, result)>:
424	  match result:
425	    case Fail{error}:
426	      Laws.Success{Empty.absurd({False{} == True{} : Bool},
427	        {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<target>>, Bool,
428	          found => Result.is_done(&2, &1, Core.Error, Core.Tensor<target>, found), Fail{error}, Done{tensor},
429	          Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{tensor}, Fail{error}, same)))} :
430	          Allocation.TensorDone<target, Fail{error}> -> Empty}(done))}
431	    case Done{Core.TTensor{storage, exact}}:
432	      match storage:
433	        case Storage.Empty{}:
434	          Laws.Success{{==}}
435	        case Storage.Owned{+depth, +length, array, balanced, valid}:
436	          indexed_success(shape, tensor, target, plan, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, depth, length,
437	            valid, exact, Shape.index_map(plan))
438	
439	def fitted_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool,
440	  -decided: {same == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)) : Bool},
441	  -truth: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}) ->
442	  Laws.Success<Reduce.fitted(Core.Packed{shape, tensor}, target, plan, same)>:
443	  match same:
444	    case False{}:
445	      Laws.Success{Empty.absurd({False{} == True{} : Bool},
446	        Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), True{}, decided,
447	          %truth : {Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), _) == True{} : Bool}
448	          TransformProof.words_same_refl(Shape.dimensions(Shape.output_shape(plan))))))}
449	    case True{}:
450	      parallel_success(shape, tensor, target, plan, Core.new(target, 0.0), AllocationProof.core_new_done(target, 0.0))
451	
452	def planned_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
453	  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
454	  -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>},
455	  -built: {ShapeLaws.broadcast_built(result) == True{} : Bool},
456	  -alignment: Shape.Broadcast<Shape.extents(target), Shape.extents(shape), Shape.extents(shape)>) ->
457	  Laws.Success<Reduce.planned(shape, tensor, target, result)>:
458	  match result:
459	    case Fail{error}:
460	      Laws.Success{Empty.absurd({False{} == True{} : Bool}, Arith.clash(built))}
461	    case Done{+plan}:
462	      fitted_success(shape, tensor, target, plan,
463	        Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), {==},
464	        ElementwiseProof.planned_output_dimensions(target, shape, plan, Shape.dimensions(shape), alignment, sources))
465	
466	def Laws.reduce_valid_success(input, target, alignment):
467	  Core.Packed{+shape, tensor} = input
468	  planned_success(shape, tensor, target, Shape.broadcast_checked(target, shape), PlanProof.broadcast_checked_plan(target, shape),
469	    PlanProof.broadcast_checked_complete(target, shape, Shape.dimensions(shape), alignment, rank_of(shape), capacity_of(shape)), alignment)
470	
471	def empty_fiber(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +index: U32, +count: Nat,
472	  -empty: {count == 0n : Nat}) -> Holds<{Laws.fiber(plan, values, index, count) == Some{0.0} : Maybe<&2, F32>}>:
473	  Holds{
474	    %Equal.sym(Nat, count, 0n, empty) : {Laws.fiber(plan, values, index, _) == Some{0.0} : Maybe<&2, F32>}
475	    {==}}
476	
477	def below_zero(+number: Nat) -> Holds<{Nat.is_lt(number, 0n) == False{} : Bool}>:
478	  match number:
479	    case 0n:
480	      Holds{{==}}
481	    case 1n+rest:
482	      Holds{{==}}
483	
484	def empty_unlisted(+depth: Nat, +length: Nat, -array: Array<F32>, +source: U32,
485	  -empty: {length == 0n : Nat}) -> Holds<{Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), length)) == None{} : Maybe<&2, F32>}>:
486	  Holds{
487	    %Equal.sym(Nat, length, 0n, empty) :
488	      {Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), _)) == None{} : Maybe<&2, F32>}
489	    %Equal.sym(Bool, Nat.is_lt(U32.to_nat(source), 0n), False{},
490	      {\{Holds: proof => proof} : Holds<{Nat.is_lt(U32.to_nat(source), 0n) == False{} : Bool}> -> {Nat.is_lt(U32.to_nat(source), 0n) == False{} : Bool}}(
491	        below_zero(U32.to_nat(source)))) :
492	      {Lifecycle.observe_allowed(depth, length, array, source, _) == None{} : Maybe<&2, F32>}
493	    {==}}
494	
495	def listed_empty(input: Core.Dynamic, -empty: {Shape.logical_numel(Totality.dimensions(input)) == 0n : Nat}) -> Holds<Laws.Listed(input, Nil{})>:
496	  Core.Packed{+shape, Core.TTensor{storage, exact}} = input
497	  match storage:
498	    case Storage.Empty{}:
499	      Holds{source => {==}}
500	    case Storage.Owned{+depth, +length, array, balanced, valid}:
501	      Holds{source => {\{Holds: proof => proof} :
502	        Holds<{Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), length)) == None{} : Maybe<&2, F32>}> ->
503	        {Lifecycle.observe_allowed(depth, length, array, source, Nat.is_lt(U32.to_nat(source), length)) == None{} : Maybe<&2, F32>}}(
504	        empty_unlisted(depth, length, array, source, Equal.trans(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), 0n, exact, empty)))}
505	
506	def below_self(+number: Nat) -> {Nat.is_lt(number, number) == False{} : Bool}:
507	  match number:
508	    case 0n:
509	      {==}
510	    case 1n+rest:
511	      below_self(rest)
512	
513	def neither_below(+left: Nat, +right: Nat, first: {Nat.is_lt(left, right) == False{} : Bool},
514	  second: {Nat.is_lt(right, left) == False{} : Bool}) -> {left == right : Nat}:
515	  match left right:
516	    case 0n 0n:
517	      {==}
518	    case 0n 1n+r:
519	      Empty.absurd({0n == 1n+r : Nat}, Arith.clash_true(first))
520	    case 1n+l 0n:
521	      Empty.absurd({1n+l == 0n : Nat}, Arith.clash_true(second))
522	    case 1n+l 1n+r:
523	      Equal.cong(Nat, Nat, n => 1n+n, l, r, neither_below(l, r, first, second))
524	
525	def word_presence(+values: List<&2, F32>, +position: Nat) ->
526	  {Nat.is_lt(position, List.length(&2, F32, values)) == TransformProof.maybe_present(Laws.word_at(values, position)) : Bool}:
527	  match values position:
528	    case Nil{} 0n:
529	      {==}
530	    case Nil{} 1n+next:
531	      {==}
532	    case value <> rest 0n:
533	      {==}
534	    case value <> rest 1n+next:
535	      word_presence(rest, next)
536	
537	def absent_observation(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +source: U32,
538	  -outside: {Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) ->
539	  Holds<{Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}>:
540	  Core.TTensor{storage, exact} = tensor
541	  match storage:
542	    case Storage.Empty{}:
543	      Holds{{==}}
544	    case Storage.Owned{+depth, +length, array, balanced, valid}:
545	      Holds{
546	        %Equal.sym(Bool, Nat.is_lt(U32.to_nat(source), length), False{},
547	          %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(source), _) == False{} : Bool}
548	          outside) : {Lifecycle.observe_allowed(depth, length, array, source, _) == None{} : Maybe<&2, F32>}
549	        {==}}
550	
551	def observed_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +source: U32, +inside: Bool,
552	  -decision: {inside == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}) ->
553	  Holds<{TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == inside : Bool}>:
554	  match inside:
555	    case False{}:
556	      Holds{Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Core.checked_observe(shape, tensor, source), None{},
557	        {\{Holds: proof => proof} : Holds<{Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}> -> {Core.checked_observe(shape, tensor, source) == None{} : Maybe<&2, F32>}}(
558	          absent_observation(shape, tensor, source, Equal.sym(Bool, False{}, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), decision))))}
559	    case True{}:
560	      Holds{{\{TransformProof.PresentObservation: value => equal =>
561	        Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Core.checked_observe(shape, tensor, source), Some{value}, equal)} :
562	        TransformProof.PresentObservation<shape, tensor, source> -> {TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == True{} : Bool}}(
563	        TransformProof.present_observation(shape, tensor, source, Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), decision)))}
564	
565	def same_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
566	  -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +source: U32) ->
567	  Holds<{Nat.is_lt(U32.to_nat(source), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}>:
568	  Holds{Equal.trans(Bool, Nat.is_lt(U32.to_nat(source), List.length(&2, F32, values)), TransformProof.maybe_present(Laws.word_at(values, U32.to_nat(source))),
569	    Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
570	    word_presence(values, U32.to_nat(source)),
571	    Equal.trans(Bool, TransformProof.maybe_present(Laws.word_at(values, U32.to_nat(source))),
572	      TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)), Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))),
573	      Equal.cong(Maybe<&2, F32>, Bool, TransformProof.maybe_present, Laws.word_at(values, U32.to_nat(source)),
574	        Core.checked_observe(shape, tensor, source),
575	        Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, tensor, source), Laws.word_at(values, U32.to_nat(source)), listed(source))),
576	      {\{Holds: proof => proof} : Holds<{TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {TransformProof.maybe_present(Core.checked_observe(shape, tensor, source)) == Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
577	        observed_presence(shape, tensor, source, Nat.is_lt(U32.to_nat(source), Shape.logical_numel(Shape.dimensions(shape))), {==}))))}
578	
579	def natural_presence(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
580	  -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +position: Nat, -within: Shape.LE(position, 1048576n)) ->
581	  Holds<{Nat.is_lt(position, List.length(&2, F32, values)) == Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(shape))) : Bool}>:
582	  Holds{
583	    %Conversion.capacity_natural_word_exact(position, within) : {Nat.is_lt(_, List.length(&2, F32, values)) == Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) : Bool}
584	    {\{Holds: proof => proof} : Holds<{Nat.is_lt(U32.to_nat(U32.from_nat(position)), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(U32.from_nat(position)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(U32.to_nat(U32.from_nat(position)), List.length(&2, F32, values)) == Nat.is_lt(U32.to_nat(U32.from_nat(position)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
585	      same_presence(shape, tensor, values, listed, U32.from_nat(position)))}
586	
587	def length_decided(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
588	  -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +below: Bool,
589	  -decision: {below == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}) -> Holds<{List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
590	  match below:
591	    case True{}:
592	      Holds{Empty.absurd({List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, Arith.clash(
593	        Equal.trans(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), True{},
594	          Equal.sym(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), False{}, below_self(List.length(&2, F32, values))),
595	          Equal.trans(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), True{},
596	            {\{Holds: proof => proof} : Holds<{Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
597	              natural_presence(shape, tensor, values, listed, List.length(&2, F32, values),
598	              Shape.LE.from(List.length(&2, F32, values), 1048576n, Equal.sym(Bool, Nat.is_le(List.length(&2, F32, values), 1048576n), True{},
599	                Conversion.le_trans(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), 1048576n,
600	                  Conversion.lt_le(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)),
601	                  Equal.sym(Bool, True{}, Nat.is_le(Shape.logical_numel(Shape.dimensions(shape)), 1048576n), Nats.le_true(Shape.logical_numel(Shape.dimensions(shape)), 1048576n, capacity_of(shape)))))))),
602	            Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)))))}
603	    case False{}:
604	      Holds{neither_below(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision),
605	        Equal.trans(Bool, Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)), Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))), False{},
606	          {\{Holds: proof => proof} : Holds<{Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
607	            natural_presence(shape, tensor, values, listed, Shape.logical_numel(Shape.dimensions(shape)), capacity_of(shape))),
608	          below_self(Shape.logical_numel(Shape.dimensions(shape)))))}
609	
610	def Laws.listed_length(input, values, listed):
611	  Core.Packed{+shape, tensor} = input
612	  Laws.Length{{\{Holds: proof => proof} : Holds<{List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}> -> {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}}(
613	    length_decided(shape, tensor, values, listed, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), {==}))}
614	
615	def zeros_from_mapping(-input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
616	  pair: Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>,
617	  -mapping: Laws.MappingWith(input, target, Done{plan}, pair),
618	  -listed: Laws.Listed(input, Nil{}),
619	  -empty: {Shape.logical_numel(Totality.dimensions(input)) == 0n : Nat}) -> Laws.Zeros<target, pair>:
620	  (owner, outcome) = pair
621	  match outcome:
622	    case Fail{error}:
623	      Laws.Zeros{Unit{}}
624	    case Done{output}:
625	      Laws.Zeros{index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(output, index),
626	        Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))), Some{0.0},
627	        mapping_values(input, target, plan, output, mapping)(Nil{})(listed)(index)(inside),
628	        {\{Holds: proof => proof} : Holds<{Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))) == Some{0.0} : Maybe<&2, F32>}> ->
629	          {Laws.fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input))) == Some{0.0} : Maybe<&2, F32>}}(
630	          empty_fiber(plan, Nil{}, index, Shape.logical_numel(Totality.dimensions(input)), empty)))}
631	
632	def planned_zeros(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
633	  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
634	  -sources: {ShapeLaws.planned_dimensions(target, shape, result) == (Shape.dimensions(target), Shape.dimensions(shape)) : List<&2, U32> & List<&2, U32>},
635	  -empty: {Shape.logical_numel(Shape.dimensions(shape)) == 0n : Nat}) ->
636	  Laws.Zeros<target, Reduce.planned(shape, tensor, target, result)>:
637	  match result:
638	    case Fail{error}:
639	      Laws.Zeros{Unit{}}
640	    case Done{+plan}:
641	      zeros_from_mapping(Core.Packed{shape, tensor}, target, plan, Reduce.planned(shape, tensor, target, Done{plan}),
642	        {\{Holds: proof => proof} :
643	          Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))> ->
644	          Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan}, Reduce.planned(shape, tensor, target, Done{plan}))}(
645	          planned_mapping(shape, tensor, target, Done{plan}, sources)),
646	        {\{Holds: proof => proof} : Holds<Laws.Listed(Core.Packed{shape, tensor}, Nil{})> -> Laws.Listed(Core.Packed{shape, tensor}, Nil{})}(
647	          listed_empty(Core.Packed{shape, tensor}, empty)),
648	        empty)
649	
650	def Laws.reduce_empty_zeros(input, target, empty):
651	  Core.Packed{+shape, tensor} = input
652	  planned_zeros(shape, tensor, target, Shape.broadcast_checked(target, shape), PlanProof.broadcast_checked_plan(target, shape), empty)
653	
654	def Laws.reduce_shape_error(input, target, error, rejected):
655	  Core.Packed{+shape, tensor} = input
656	  %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(target, shape), Fail{error}, rejected) :
657	    {Reduce.planned(shape, tensor, target, _) == (Core.Packed{shape, tensor}, Fail{Reduce.TensorError{Core.ShapeError{error}}}) :
658	      Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}
659	  {==}
660	
661	def fitted_not_reducible(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +dims: List<&2, U32>, flag: Bool,
662	  decided: {flag == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), dims) : Bool},
663	  differ: {Shape.dimensions(Shape.output_shape(plan)) != dims : List<&2, U32>}) ->
664	  {Reduce.fitted(input, target, plan, flag) == (input, Fail{Reduce.NotReducible{}}) :
665	    Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}:
666	  match flag:
667	    case False{}:
668	      {==}
669	    case True{}:
670	      Empty.absurd({Reduce.fitted(input, target, plan, True{}) == (input, Fail{Reduce.NotReducible{}}) :
671	        Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>},
672	        differ(TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), dims, decided)))
673	
674	def Laws.reduce_not_reducible(input, target, plan, planned, differ):
675	  Core.Packed{+shape, tensor} = input
676	  %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(target, shape), Done{plan}, planned) :
677	    {Reduce.planned(shape, tensor, target, _) == (Core.Packed{shape, tensor}, Fail{Reduce.NotReducible{}}) :
678	      Core.Dynamic & Result<&2, &1, Reduce.Error, Core.Dynamic>}
679	  fitted_not_reducible(Core.Packed{shape, tensor}, target, plan, Shape.dimensions(shape),
680	    Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(shape)), {==}, differ)