src/autograd/broadcast_PROOF.bend
bendtorch-core@0.1.0.0 · 328 lines · 21 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
4import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
5import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
6import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
7import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
8import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
9import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
10import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
11import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
12import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ParallelProof
13import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof
14import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
15import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
16import bendtorch-core@0.1.0.0/src/tensor/projection_PROOF.bend as ProjectionProof
17import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
18import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
19import bendtorch-core@0.1.0.0/src/autograd/broadcast.bend as Broadcast
20import bendtorch-core@0.1.0.0/src/autograd/broadcast_LAWS.bend as Laws
21
22type Holds<-P: Type> is Data:
23 Holds{-proof: P}
24
25def Laws.keep_left_scalar(left, right):
26 {==}
27
28def 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
38def 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
47def 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
55def 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
63def 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
67type 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
71def 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
82def 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
104def 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
124def 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
136def 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
173def 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
189def 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
201def 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
217def 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
225def 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
235def 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
252def 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
267def 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
287def 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
292def 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
297def 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
302def 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
309def 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
322def 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)