1	import Base
2	import ../shape/core.bend as Shape
3	import ../shape/LAWS.bend as ShapeLaws
4	import ../shape/plan_proofs.bend as PlanProof
5	import ../shape/nat_proofs.bend as Nats
6	import ../storage/arith.bend as Arith
7	import ../tensor/core.bend as Core
8	import ../tensor/layout.bend as Layout
9	import ../tensor/elementwise.bend as Elementwise
10	import ../tensor/elementwise_totality.bend as Totality
11	import ../tensor/elementwise_PROOF.bend as ElementwiseProof
12	import ../tensor/elementwise_parallel_proof.bend as ParallelProof
13	import ../tensor/core_PROOF.bend as CoreProof
14	import ../tensor/transform_PROOF.bend as TransformProof
15	import ../tensor/projection_LAWS.bend as Projection
16	import ../tensor/projection_PROOF.bend as ProjectionProof
17	import ../tensor/allocation_spec.bend as Allocation
18	import ../tensor/allocation_PROOF.bend as AllocationProof
19	import ./broadcast.bend as Broadcast
20	import ./broadcast_LAWS.bend as Laws
21	
22	type Holds<-P: Type> is Data:
23	  Holds{-proof: P}
24	
25	def Laws.keep_left_scalar(left, right):
26	  {==}
27	
28	def finish_retains(-input: Core.Dynamic, -right: Core.Dynamic,
29	  pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
30	  -retention: Totality.Retention<input, right, pair>) -> Laws.Retained<input, Broadcast.finish(pair)>:
31	  ((left, other), result) = pair
32	  match result:
33	    case Fail{error}:
34	      Laws.Retained{{\{Totality.Retention: l => r => l} : Totality.Retention<input, right, ((left, other), Fail{error})> -> Totality.SameSource(input, left)}(retention)}
35	    case Done{output}:
36	      Laws.Retained{{\{Totality.Retention: l => r => l} : Totality.Retention<input, right, ((left, other), Done{output})> -> Totality.SameSource(input, left)}(retention)}
37	
38	def zeroed_retains(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
39	  result: Result<&2, &1, Core.Error, Core.Tensor<target>>) -> Laws.Retained<input, Broadcast.zeroed(input, target, plan, result)>:
40	  match result:
41	    case Fail{error}:
42	      Laws.Retained{property => {==}}
43	    case Done{zeros}:
44	      finish_retains(input, Core.Packed{target, zeros}, Elementwise.parallel_allocated(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0)),
45	        ElementwiseProof.parallel_allocated_retains(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0)))
46	
47	def fitted_retains(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool) ->
48	  Laws.Retained<input, Broadcast.fitted(input, target, plan, same)>:
49	  match same:
50	    case False{}:
51	      Laws.Retained{property => {==}}
52	    case True{}:
53	      zeroed_retains(input, target, plan, Core.new(target, 0.0))
54	
55	def planned_retains(input: Core.Dynamic, +target: Shape.Shape, result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>) ->
56	  Laws.Retained<input, Broadcast.planned(input, target, result)>:
57	  match result:
58	    case Fail{error}:
59	      Laws.Retained{property => {==}}
60	    case Done{+plan}:
61	      fitted_retains(input, target, plan, Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)))
62	
63	def Laws.broadcast_retains_input(input, target):
64	  Core.Packed{+shape, tensor} = input
65	  planned_retains(Core.Packed{shape, tensor}, target, Shape.broadcast_checked(shape, target))
66	
67	type WithModel<-input: Core.Dynamic, -target: Shape.Shape, -plan: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
68	  -pair: Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>> is Data:
69	  WithModel{-mapping: Laws.MappingWith(input, target, plan, pair)}
70	
71	def keep_left_expected(-right: Core.Dynamic, -right_index: U32, +left: Maybe<&2, F32>, -value: F32,
72	  -present: {Some{value} == Core.checked_observe_dynamic(right, right_index) : Maybe<&2, F32>}) ->
73	  Holds<{Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, left) == left : Maybe<&2, F32>}>:
74	  match left:
75	    case None{}:
76	      Holds{{==}}
77	    case Some{+found}:
78	      Holds{
79	        %present : {Elementwise.expected_right(Elementwise.KeepLeft{}, found, _) == Some{found} : Maybe<&2, F32>}
80	        {==}}
81	
82	def keep_left_source(+plan: Shape.BroadcastPlan, +index: U32, -input: Core.Dynamic, -right: Core.Dynamic,
83	  -left_index: U32, -right_index: U32, -value: F32,
84	  -exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
85	  -present: {Some{value} == Core.checked_observe_dynamic(right, right_index) : Maybe<&2, F32>}) ->
86	  Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, right, index) ==
87	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}>:
88	  Holds{Equal.trans(Maybe<&2, F32>, Elementwise.expected(Elementwise.KeepLeft{}, plan, input, right, index),
89	    Projection.specified_expected(Elementwise.KeepLeft{}, input, right, Projection.offset_spec(plan, U32.to_nat(index))),
90	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))),
91	    Projection.expected_projection_refines(Elementwise.KeepLeft{}, plan, input, right, index),
92	    %Equal.trans(Maybe<&1, U32 & U32>, Some{(left_index, right_index)}, Projection.indices_result(Elementwise.input_indices(plan, index)),
93	      Projection.offset_spec(plan, U32.to_nat(index)),
94	      Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Maybe<&1, U32 & U32>, Projection.indices_result,
95	        Done{(left_index, right_index)}, Elementwise.input_indices(plan, index), exact),
96	      Projection.input_indices_refines(plan, index)) :
97	      {Projection.specified_expected(Elementwise.KeepLeft{}, input, right, _) == Laws.source_value(input, _) : Maybe<&2, F32>}
98	    {\{Holds: proof => proof} : Holds<{Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, Core.checked_observe_dynamic(input, left_index)) ==
99	      Core.checked_observe_dynamic(input, left_index) : Maybe<&2, F32>}> ->
100	      {Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, Core.checked_observe_dynamic(input, left_index)) ==
101	        Core.checked_observe_dynamic(input, left_index) : Maybe<&2, F32>}}(
102	      keep_left_expected(right, right_index, Core.checked_observe_dynamic(input, left_index), value, present)))}
103	
104	def mapped_value(+plan: Shape.BroadcastPlan, +index: U32, -input: Core.Dynamic, +target: Shape.Shape, -zeros: Core.Tensor<target>,
105	  -right_dims: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
106	  -indices: ElementwiseProof.IndicesDone<plan, Elementwise.input_indices(plan, index)>) ->
107	  Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
108	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}>:
109	  Holds{{\{ElementwiseProof.IndicesDone: li => ri => exact => lb => rb =>
110	    {\{TransformProof.PresentObservation: value => equal =>
111	      {\{Holds: proof => proof} : Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
112	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}> -> {Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
113	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}}(
114	        keep_left_source(plan, index, input, Core.Packed{target, zeros}, li, ri, value, exact,
115	          Equal.sym(Maybe<&2, F32>, Core.checked_observe(target, zeros, ri), Some{value}, equal)))} :
116	      TransformProof.PresentObservation<target, zeros, ri> -> {Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
117	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}}(
118	      TransformProof.present_observation(target, zeros, ri,
119	        %right_dims : {Nat.is_lt(U32.to_nat(ri), Shape.logical_numel(_)) == True{} : Bool}
120	        rb))} :
121	    ElementwiseProof.IndicesDone<plan, Elementwise.input_indices(plan, index)> -> {Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
122	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}}(indices)}
123	
124	def output_inside(+plan: Shape.BroadcastPlan, +target: Shape.Shape, +index: U32,
125	  -same_dims: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
126	  -inside: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target)))) ->
127	  Holds<{Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}>:
128	  Holds{
129	    %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.numel(Shape.extents(Shape.output_shape(plan))), Shape.elements_exact(Shape.output_shape(plan))) :
130	      {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
131	    %Equal.sym(List<&2, U32>, Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target), same_dims) :
132	      {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
133	    Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))),
134	      Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target)), inside))}
135	
136	def finish_mapping(-input: Core.Dynamic, +target: Shape.Shape, -zeros: Core.Tensor<target>, +plan: Shape.BroadcastPlan,
137	  pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
138	  -dims: Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), pair>,
139	  -mapping: Elementwise.MappingModel<Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, pair>,
140	  -same_dims: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
141	  -right_dims: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(target) : List<&2, U32>}) ->
142	  WithModel<input, target, Done{plan}, Broadcast.finish(pair)>:
143	  ((left, right), result) = pair
144	  match result:
145	    case Fail{error}:
146	      WithModel{Unit{}}
147	    case Done{output}:
148	      WithModel{(
149	        Equal.trans(List<&2, U32>, Totality.dimensions(output), Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target),
150	          {\{Totality.DimensionsModel: exact => exact} : Totality.DimensionsModel<Shape.dimensions(Shape.output_shape(plan)), ((left, right), Done{output})> ->
151	            {Totality.dimensions(output) == Shape.dimensions(Shape.output_shape(plan)) : List<&2, U32>}}(dims),
152	          same_dims),
153	        index => inside => Equal.trans(Maybe<&2, F32>, Core.observe_dynamic(output, index),
154	          Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index),
155	          Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))),
156	          {\{Elementwise.MappingModel: prefix => prefix} :
157	            Elementwise.MappingModel<Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, ((left, right), Done{output})> ->
158	            Elementwise.PrefixMapping(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros},
159	              Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), output)}(mapping)(index)(
160	            %Equal.sym(List<&2, U32>, Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target), same_dims) :
161	              Shape.LT(U32.to_nat(index), Shape.logical_numel(_))
162	            inside),
163	          {\{Holds: proof => proof} : Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
164	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}> -> {Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
165	    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}}(
166	            mapped_value(plan, index, input, target, zeros, right_dims,
167	              ElementwiseProof.indices_success(plan, index,
168	                {\{Holds: proof => proof} : Holds<{Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}> ->
169	                  {Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}}(
170	                  output_inside(plan, target, index, same_dims, inside))))))
171	      )}
172	
173	def zeroed_mapping(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
174	  result: Result<&2, &1, Core.Error, Core.Tensor<target>>,
175	  -same_dims: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
176	  +left_dims: {Totality.dimensions(input) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
177	  +right_dims: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(target) : List<&2, U32>}) ->
178	  WithModel<input, target, Done{plan}, Broadcast.zeroed(input, target, plan, result)>:
179	  match result:
180	    case Fail{error}:
181	      WithModel{Unit{}}
182	    case Done{zeros}:
183	      finish_mapping(input, target, zeros, plan, Elementwise.parallel_allocated(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0)),
184	        ElementwiseProof.parallel_allocated_dimensions(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0)),
185	        ParallelProof.allocated_mapping(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0),
186	          left_dims, Equal.sym(List<&2, U32>, Shape.dimensions(Shape.right_shape(plan)), Shape.dimensions(target), right_dims)),
187	        same_dims, right_dims)
188	
189	def fitted_mapping(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool,
190	  -decided: {same == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)) : Bool},
191	  +left_dims: {Totality.dimensions(input) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
192	  +right_dims: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(target) : List<&2, U32>}) ->
193	  WithModel<input, target, Done{plan}, Broadcast.fitted(input, target, plan, same)>:
194	  match same:
195	    case False{}:
196	      WithModel{Unit{}}
197	    case True{}:
198	      zeroed_mapping(input, target, plan, Core.new(target, 0.0),
199	        TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target), decided), left_dims, right_dims)
200	
201	def planned_mapping(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
202	  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
203	  +sources: {ShapeLaws.planned_dimensions(shape, target, result) == (Shape.dimensions(shape), Shape.dimensions(target)) : List<&2, U32> & List<&2, U32>}) ->
204	  WithModel<Core.Packed{shape, tensor}, target, result, Broadcast.planned(Core.Packed{shape, tensor}, target, result)>:
205	  match result:
206	    case Fail{error}:
207	      WithModel{Unit{}}
208	    case Done{+plan}:
209	      fitted_mapping(Core.Packed{shape, tensor}, target, plan,
210	        Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)), {==},
211	        Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(shape),
212	          Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>),
213	            (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(shape), Shape.dimensions(target)), sources)),
214	        Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>),
215	          (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(shape), Shape.dimensions(target)), sources))
216	
217	def Laws.broadcast_mapping(input, target):
218	  Core.Packed{+shape, tensor} = input
219	  Laws.MappingModel{
220	    {\{WithModel: mapping => mapping} :
221	      WithModel<Core.Packed{shape, tensor}, target, Shape.broadcast_checked(shape, target), Broadcast.broadcast_to(Core.Packed{shape, tensor}, target)> ->
222	        Laws.Mapping(Core.Packed{shape, tensor}, target, Broadcast.broadcast_to(Core.Packed{shape, tensor}, target))}(
223	          planned_mapping(shape, tensor, target, Shape.broadcast_checked(shape, target), PlanProof.broadcast_checked_plan(shape, target)))}
224	
225	def finish_success(pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
226	  -success: Totality.Success<pair>) -> Laws.Success<Broadcast.finish(pair)>:
227	  ((input, zeros), result) = pair
228	  match result:
229	    case Fail{error}:
230	      Laws.Success{Empty.absurd({False{} == True{} : Bool}, Arith.clash(
231	        {\{Totality.Success: successful => successful} : Totality.Success<((input, zeros), Fail{error})> -> {False{} == True{} : Bool}}(success)))}
232	    case Done{output}:
233	      Laws.Success{{==}}
234	
235	def zeroed_success(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
236	  result: Result<&2, &1, Core.Error, Core.Tensor<target>>, -done: Allocation.TensorDone<target, result>,
237	  -left_dims: {Totality.dimensions(input) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
238	  -right_dims: {Shape.dimensions(target) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}) ->
239	  Laws.Success<Broadcast.zeroed(input, target, plan, result)>:
240	  match result:
241	    case Fail{error}:
242	      Laws.Success{Empty.absurd({False{} == True{} : Bool},
243	        {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<target>>, Bool,
244	          found => Result.is_done(&2, &1, Core.Error, Core.Tensor<target>, found), Fail{error}, Done{tensor},
245	          Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{tensor}, Fail{error}, same)))} :
246	          Allocation.TensorDone<target, Fail{error}> -> Empty}(done))}
247	    case Done{zeros}:
248	      finish_success(Elementwise.parallel_allocated(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0)),
249	        ElementwiseProof.parallel_allocated_success(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, Core.new(Shape.output_shape(plan), 0.0),
250	          AllocationProof.core_new_done(Shape.output_shape(plan), 0.0)))
251	
252	def fitted_success(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, same: Bool,
253	  -decided: {same == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)) : Bool},
254	  -truth: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
255	  -left_dims: {Totality.dimensions(input) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>},
256	  -right_dims: {Shape.dimensions(target) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}) ->
257	  Laws.Success<Broadcast.fitted(input, target, plan, same)>:
258	  match same:
259	    case False{}:
260	      Laws.Success{Empty.absurd({False{} == True{} : Bool},
261	        Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)), True{}, decided,
262	          %truth : {Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), _) == True{} : Bool}
263	          TransformProof.words_same_refl(Shape.dimensions(Shape.output_shape(plan))))))}
264	    case True{}:
265	      zeroed_success(input, target, plan, Core.new(target, 0.0), AllocationProof.core_new_done(target, 0.0), left_dims, right_dims)
266	
267	def planned_success(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +target: Shape.Shape,
268	  result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>,
269	  -sources: {ShapeLaws.planned_dimensions(shape, target, result) == (Shape.dimensions(shape), Shape.dimensions(target)) : List<&2, U32> & List<&2, U32>},
270	  -built: {ShapeLaws.broadcast_built(result) == True{} : Bool},
271	  -alignment: Shape.Broadcast<Shape.extents(shape), Shape.extents(target), Shape.extents(target)>) ->
272	  Laws.Success<Broadcast.planned(Core.Packed{shape, tensor}, target, result)>:
273	  match result:
274	    case Fail{error}:
275	      Laws.Success{Empty.absurd({False{} == True{} : Bool}, Arith.clash(built))}
276	    case Done{+plan}:
277	      fitted_success(Core.Packed{shape, tensor}, target, plan,
278	        Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)), {==},
279	        ElementwiseProof.planned_output_dimensions(shape, target, plan, Shape.dimensions(target), alignment, sources),
280	        Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(shape),
281	          Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>),
282	            (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(shape), Shape.dimensions(target)), sources)),
283	        Equal.sym(List<&2, U32>, Shape.dimensions(Shape.right_shape(plan)), Shape.dimensions(target),
284	          Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>),
285	            (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(shape), Shape.dimensions(target)), sources)))
286	
287	def rank_of(+shape: Shape.Shape) -> Shape.LE(Shape.rank_dimensions(Shape.dimensions(shape)), 4n):
288	  match shape:
289	    case Shape.SShape{dims, size, exact, rank_bound, capacity_bound}:
290	      rank_bound
291	
292	def capacity_of(+shape: Shape.Shape) -> Shape.LE(Shape.logical_numel(Shape.dimensions(shape)), 1048576n):
293	  match shape:
294	    case Shape.SShape{dims, size, exact, rank_bound, capacity_bound}:
295	      capacity_bound
296	
297	def Laws.broadcast_valid_success(input, target, alignment):
298	  Core.Packed{+shape, tensor} = input
299	  planned_success(shape, tensor, target, Shape.broadcast_checked(shape, target), PlanProof.broadcast_checked_plan(shape, target),
300	    PlanProof.broadcast_checked_complete(shape, target, Shape.dimensions(target), alignment, rank_of(target), capacity_of(target)), alignment)
301	
302	def Laws.broadcast_shape_error(input, target, error, rejected):
303	  Core.Packed{+shape, tensor} = input
304	  %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(shape, target), Fail{error}, rejected) :
305	    {Broadcast.planned(Core.Packed{shape, tensor}, target, _) == (Core.Packed{shape, tensor}, Fail{Broadcast.TensorError{Core.ShapeError{error}}}) :
306	      Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>}
307	  {==}
308	
309	def fitted_not_target(input: Core.Dynamic, +target: Shape.Shape, +plan: Shape.BroadcastPlan, flag: Bool,
310	  decided: {flag == Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)) : Bool},
311	  differ: {Shape.dimensions(Shape.output_shape(plan)) != Shape.dimensions(target) : List<&2, U32>}) ->
312	  {Broadcast.fitted(input, target, plan, flag) == (input, Fail{Broadcast.NotBroadcastable{}}) :
313	    Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>}:
314	  match flag:
315	    case False{}:
316	      {==}
317	    case True{}:
318	      Empty.absurd({Broadcast.fitted(input, target, plan, True{}) == (input, Fail{Broadcast.NotBroadcastable{}}) :
319	        Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>},
320	        differ(TransformProof.words_equal(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target), decided)))
321	
322	def Laws.broadcast_not_target(input, target, plan, planned, differ):
323	  Core.Packed{+shape, tensor} = input
324	  %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(shape, target), Done{plan}, planned) :
325	    {Broadcast.planned(Core.Packed{shape, tensor}, target, _) == (Core.Packed{shape, tensor}, Fail{Broadcast.NotBroadcastable{}}) :
326	      Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic>}
327	  fitted_not_target(Core.Packed{shape, tensor}, target, plan,
328	    Layout.words_same(Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target)), {==}, differ)