src/tensor/core_PROOF.bend
bendtorch-core@0.1.0.0 · 1,146 lines · 86 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
4import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
5import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
6import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
7import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
8import bendtorch-core@0.1.0.0/src/storage/PROOF.bend as StorageProof
9import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
10import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
11import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
12import bendtorch-core@0.1.0.0/src/tensor/word_injective.bend as Injective
13import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
14import bendtorch-core@0.1.0.0/src/tensor/core_LAWS.bend as Laws
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/elementwise_parallel_proof.bend as Parallel
18
19def Laws.scalar_add(left, right):
20 {==}
21
22def Laws.scalar_sub(left, right):
23 {==}
24
25def Laws.scalar_mul(left, right):
26 {==}
27
28def Laws.indexed_length(shape, tensor):
29 Core.TTensor{storage, exact} = tensor
30 Core.LengthValid{exact}
31
32def construction_values_dimensions(+dimensions: List<&2, U32>, +shape: Shape.Shape,
33 preserved: {Shape.dimensions(shape) == dimensions : List<&2, U32>},
34 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
35 Core.ConstructionDimensions(dimensions, Core.construct_values(shape, result)):
36 match result:
37 case Fail{error}:
38 Unit{}
39 case Done{tensor}:
40 preserved
41
42def construction_shape_dimensions(+dimensions: List<&2, U32>, values: List<&2, F32>, result: Shape.ConstructResult<dimensions>) ->
43 Core.ConstructionDimensions(dimensions, Core.construct_shape(dimensions, values, result)):
44 match result:
45 case Shape.SError{error}:
46 Unit{}
47 case Shape.SBuilt{+shape, preserved}:
48 construction_values_dimensions(dimensions, shape, preserved, Core.from_values(shape, values))
49
50def Laws.successful_construction_dimensions(dimensions, values):
51 construction_shape_dimensions(dimensions, values, Shape.construct(dimensions))
52
53def count_outcome(+shape: Shape.Shape, +values: List<&2, F32>,
54 equal: {Shape.logical_numel(Shape.dimensions(shape)) == List.length(&2, F32, values) : Nat},
55 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) -> Core.ValuesCount(shape, values, result):
56 match result:
57 case Fail{error}:
58 Unit{}
59 case Done{tensor}:
60 equal
61
62def count_decision(+shape: Shape.Shape, +values: List<&2, F32>,
63 decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>) ->
64 Core.ValuesCount(shape, values, Core.from_values_counted(shape, values, decision)):
65 match decision:
66 case Shape.BFalse{equal}:
67 Unit{}
68 case Shape.BTrue{equal}:
69 count_outcome(shape, values,
70 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape), List.length(&2, F32, values),
71 Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape)),
72 Equal.sym(Nat, List.length(&2, F32, values), Shape.elements(shape),
73 Lifecycle.natural_equal(List.length(&2, F32, values), Shape.elements(shape), equal))),
74 Core.from_values_new(shape, values, Core.new(shape, 0.0)))
75
76def Laws.successful_value_count(shape, values):
77 count_decision(shape, values, Shape.bool_case(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))))
78
79def Laws.checked_reader_pair(shape, original, index):
80 Core.read_certificate(shape, original, index)
81
82def Laws.reader_certificate_value(shape, original, index, certificate):
83 Core.Read{tensor, result, exact} = certificate
84 %exact : {Core.read_value(shape, _) == Core.result_value(result) : Maybe<&2, F32>}
85 {==}
86
87def Laws.checked_reader_source(shape, original, index):
88 Core.source_read_model(shape, original, index)
89
90def Laws.checked_dynamic_reader_source(original, index):
91 Core.dynamic_source_read_model(original, index)
92
93def Laws.checked_reader_retains_source(shape, original, index):
94 Core.source_read_keeps(shape, original, index)
95
96def Laws.checked_dynamic_reader_retains_source(original, index):
97 Core.dynamic_source_read_keeps(original, index)
98
99def Laws.primitive_read_retains_elements(depth, array, index, other, balanced):
100 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, other)),
101 Refinement.first(F32, Array.get(F32, array, index)), array,
102 Refinement.law_get_retains(F32, depth, array, index, balanced))
103
104def Laws.storage_read_retains_length(storage, index):
105 Lifecycle.get_length(storage, index)
106
107def Laws.storage_write_retains_length(storage, index, value):
108 Lifecycle.set_length(storage, index, value)
109
110def Laws.storage_clone_first_length(storage):
111 Lifecycle.clone_first_length(storage)
112
113def Laws.storage_clone_second_length(storage):
114 Lifecycle.clone_second_length(storage)
115
116def Laws.primitive_clone_first_elements(depth, array, path, balanced):
117 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, path),
118 Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), array,
119 Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced)))
120
121def Laws.primitive_clone_second_elements(depth, array, path, balanced):
122 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, path),
123 Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), array,
124 Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced)))
125
126def write_checked_mapping(-shape: Shape.Shape, +d: Nat, +n: Nat, array: Array<F32>, +i: U32, +value: F32,
127 balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
128 -exact: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, allowed: Bool,
129 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
130 -same: {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
131 Storage.set(Storage.Owned{d, n, array, balanced, valid}, i, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
132 accepted: {allowed == True{} : Bool}) ->
133 {Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
134 Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid), same), i) == Some{value} : Maybe<&2, F32>}:
135 match allowed:
136 case False{}:
137 Empty.absurd({Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
138 Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid), same), i) == Some{value} : Maybe<&2, F32>},
139 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
140 case True{}:
141 StorageLaws.primitive_write_read(F32, d, array, i, value, balanced)
142
143def Laws.tensor_write_mapping(shape, depth, length, array, index, value, balanced, valid, exact, allowed, matched):
144 write_checked_mapping(shape, depth, length, array, index, value, balanced, valid, exact,
145 Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed)
146
147def step_checked_mapping(-shape: Shape.Shape, +d: Nat, +n: Nat, array: Array<F32>, +i: U32, +value: F32,
148 -left: Core.Dynamic, -right: Core.Dynamic,
149 balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
150 -exact: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, allowed: Bool,
151 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
152 -same: {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
153 Storage.set(Storage.Owned{d, n, array, balanced, valid}, i, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
154 accepted: {allowed == True{} : Bool}) ->
155 {Elementwise.step_observe(shape, Elementwise.step_write(shape, left, right,
156 Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
157 Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid), same)), i) == Some{value} : Maybe<&2, F32>}:
158 match allowed:
159 case False{}:
160 Empty.absurd({Elementwise.step_observe(shape, Elementwise.step_write(shape, left, right,
161 Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
162 Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid), same)), i) == Some{value} : Maybe<&2, F32>},
163 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
164 case True{}:
165 StorageLaws.primitive_write_read(F32, d, array, i, value, balanced)
166
167def Laws.broadcast_step_mapping(operation, shape, depth, length, array, index, left, right,
168 left_value, right_value, balanced, valid, exact, allowed, matched):
169 step_checked_mapping(shape, depth, length, array, index, Elementwise.scalar(operation, left_value, right_value),
170 left, right, balanced, valid, exact, Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed)
171
172def and_true_left(+left: Bool, +right: Bool, equal: {Bool.and(left, right) == True{} : Bool}) -> {left == True{} : Bool}:
173 match left:
174 case False{}:
175 Empty.absurd({False{} == True{} : Bool}, Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
176 case True{}:
177 {==}
178
179def same_path_offset(+depth: Nat, +left: Model.Path(depth), +right: Model.Path(depth),
180 equal: {Model.same(depth, left, right) == True{} : Bool}) -> {Model.offset(depth, left) == Model.offset(depth, right) : Nat}:
181 match depth:
182 case 0n:
183 {==}
184 case 1n++p:
185 Model.Step{+lb, +lt} = left
186 match lb:
187 case False{}:
188 Model.Step{+rb, +rt} = right
189 match rb:
190 case False{}:
191 same_path_offset(p, lt, rt, equal)
192 case True{}:
193 Empty.absurd({Model.offset(p, lt) == Nat.add(Model.capacity(p), Model.offset(p, rt)) : Nat},
194 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
195 case True{}:
196 Model.Step{+rb, +rt} = right
197 match rb:
198 case False{}:
199 Empty.absurd({Nat.add(Model.capacity(p), Model.offset(p, lt)) == Model.offset(p, rt) : Nat},
200 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
201 case True{}:
202 Equal.cong(Nat, Nat, n => Nat.add(Model.capacity(p), n), Model.offset(p, lt), Model.offset(p, rt),
203 same_path_offset(p, lt, rt, equal))
204
205def checked_offset(+depth: Nat, +length: Nat, +index: U32,
206 checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
207 {Model.offset(depth, Refinement.route(depth, index)) == U32.to_nat(index) : Nat}:
208 Lifecycle.natural_equal(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
209 Equal.sym(Bool, Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)), True{},
210 and_true_left(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
211 Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked)))
212
213def nat_equal_self(+n: Nat) -> {Nat.is_eq(n, n) == True{} : Bool}:
214 match n:
215 case 0n:
216 {==}
217 case 1n+p:
218 nat_equal_self(p)
219
220def natural_clash(+left: Nat, +right: Nat, equal: {left == right : Nat},
221 different: {Nat.is_eq(left, right) == False{} : Bool}) -> Empty:
222 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_eq(left, right), False{},
223 Equal.sym(Bool, Nat.is_eq(left, right), True{},
224 %equal : {Nat.is_eq(left, _) == True{} : Bool}
225 nat_equal_self(left)), different))
226
227def route_separation_decided(+depth: Nat, +length: Nat, +index: U32, +other: U32,
228 index_checked: {Storage.index_matches(depth, length, index) == True{} : Bool},
229 other_checked: {Storage.index_matches(depth, length, other) == True{} : Bool},
230 different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}, same: Bool,
231 decision: {same == Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)) : Bool}) -> {same == False{} : Bool}:
232 match same:
233 case False{}:
234 {==}
235 case True{}:
236 Empty.absurd({True{} == False{} : Bool}, natural_clash(U32.to_nat(index), U32.to_nat(other),
237 Equal.trans(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(other),
238 Equal.sym(Nat, Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index), checked_offset(depth, length, index, index_checked)),
239 Equal.trans(Nat, Model.offset(depth, Refinement.route(depth, index)), Model.offset(depth, Refinement.route(depth, other)), U32.to_nat(other),
240 same_path_offset(depth, Refinement.route(depth, index), Refinement.route(depth, other),
241 Equal.sym(Bool, True{}, Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), decision)),
242 checked_offset(depth, length, other, other_checked))), different))
243
244def Laws.checked_route_separation(depth, length, index, other, index_checked, other_checked, different):
245 route_separation_decided(depth, length, index, other, index_checked, other_checked, different,
246 Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), {==})
247
248def frame_checked_mapping(-shape: Shape.Shape, +d: Nat, +n: Nat, array: Array<F32>, +i: U32, +other: U32, +value: F32,
249 balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
250 -exact: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, allowed: Bool,
251 -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
252 -same: {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
253 Storage.set(Storage.Owned{d, n, array, balanced, valid}, i, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
254 accepted: {allowed == True{} : Bool},
255 index_checked: {Storage.index_matches(d, n, i) == True{} : Bool},
256 other_checked: {Storage.index_matches(d, n, other) == True{} : Bool},
257 different: {Nat.is_eq(U32.to_nat(i), U32.to_nat(other)) == False{} : Bool}) ->
258 {Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
259 Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid), same), other) ==
260 Model.observe(F32, d, array, Refinement.route(d, other)) : Maybe<&2, F32>}:
261 match allowed:
262 case False{}:
263 Empty.absurd({Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
264 Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid), same), other) ==
265 Model.observe(F32, d, array, Refinement.route(d, other)) : Maybe<&2, F32>},
266 Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
267 case True{}:
268 %Laws.checked_route_separation(d, n, i, other, index_checked, other_checked, different) :
269 {Model.observe(F32, d, Array.set(F32, array, i, value), Refinement.route(d, other)) ==
270 Model.select(F32, _, value, Model.observe(F32, d, array, Refinement.route(d, other))) : Maybe<&2, F32>}
271 StorageLaws.primitive_update_frame(F32, d, array, i, Refinement.route(d, other), value, balanced)
272
273def Laws.tensor_write_frame(shape, depth, length, array, index, other, value, balanced, valid, exact,
274 allowed, index_checked, other_checked, different):
275 frame_checked_mapping(shape, depth, length, array, index, other, value, balanced, valid, exact,
276 Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed, index_checked, other_checked, different)
277
278def Laws.checked_conversion_value(cursor, index, verdict):
279 Lifecycle.natural_equal(U32.to_nat(index), cursor, verdict)
280
281def cursor_validity(-shape: Shape.Shape, +cursor: Nat, result: Elementwise.NaturalStep<shape, cursor>) ->
282 Elementwise.CursorValidity(shape, cursor, result):
283 match result:
284 case Elementwise.NaturalStop{left, right, error}:
285 Unit{}
286 case Elementwise.NaturalContinue{state, index, exact}:
287 Elementwise.CursorWitness{exact}
288
289def Laws.natural_cursor_step(operation, plan, cursor, state):
290 cursor_validity(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))
291
292def Laws.u32_natural_injective(left, right, equal):
293 Injective.u32_natural_injective(left, right)(equal)
294
295type UpdateCheckedModel<-shape: Shape.Shape, -depth: Nat, -length: Nat, -array: Array<F32>, -index: U32, -value: F32,
296 -allowed: Bool, -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
297 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
298 -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
299 -same: {Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid) ==
300 Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}> is Data:
301 UpdateCheckedModel{-meaning: Core.UpdateMeaning(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}, index, value,
302 Core.write_result(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index, value,
303 Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid), same))}
304
305def update_checked_model(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, +value: F32,
306 allowed: Bool, -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
307 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
308 -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
309 -same: {Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid) ==
310 Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
311 UpdateCheckedModel<shape, depth, length, array, index, value, allowed, decision, balanced, valid, length_exact, same>:
312 match allowed:
313 case False{}:
314 UpdateCheckedModel{Unit{}}
315 case True{}:
316 UpdateCheckedModel{(Route.index_matched(depth, length, index, valid, Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), length), decision)),
317 (StorageLaws.primitive_write_read(F32, depth, array, index, value, balanced),
318 other => checked => different => (checked,
319 %Laws.checked_route_separation(depth, length, index, other,
320 Route.index_matched(depth, length, index, valid, Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), length), decision)),
321 checked, different) :
322 {Model.observe(F32, depth, Array.set(F32, array, index, value), Refinement.route(depth, other)) ==
323 Model.select(F32, _, value, Model.observe(F32, depth, array, Refinement.route(depth, other))) : Maybe<&2, F32>}
324 StorageLaws.primitive_update_frame(F32, depth, array, index, Refinement.route(depth, other), value, balanced))))}
325
326def update_checked_tensor(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, +value: F32,
327 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
328 -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
329 certificate: UpdateCheckedModel<shape, depth, length, array, index, value, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid, length_exact, {==}>) ->
330 Core.UpdateModel<shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}, index, value>:
331 UpdateCheckedModel{meaning} = certificate
332 Core.UpdateModel{meaning}
333
334def update_model(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32) -> Core.UpdateModel<shape, original, index, value>:
335 Core.TTensor{storage, length_exact} = original
336 match storage:
337 case Storage.Empty{}:
338 Core.UpdateModel{Unit{}}
339 case Storage.Owned{+depth, +length, array, balanced, valid}:
340 update_checked_tensor(shape, depth, length, array, index, value, balanced, valid, length_exact,
341 update_checked_model(shape, depth, length, array, index, value, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid, length_exact, {==}))
342
343type WriteInfo<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32, -value: F32> is Type:
344 WriteInfo{owner: Core.Tensor<shape>, same: {owner == original : Core.Tensor<shape>}, model: Core.UpdateModel<shape, original, index, value>}
345
346def write_info(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32) -> WriteInfo<shape, original, index, value>:
347 Core.TTensor{storage, length_exact} = original
348 match storage:
349 case Storage.Empty{}:
350 WriteInfo{Core.TTensor{Storage.Empty{}, length_exact}, {==}, Core.UpdateModel{Unit{}}}
351 case Storage.Owned{+depth, +length, array, balanced, valid}:
352 WriteInfo{Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}, {==},
353 update_checked_tensor(shape, depth, length, array, index, value, balanced, valid, length_exact,
354 update_checked_model(shape, depth, length, array, index, value, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid, length_exact, {==}))}
355
356def read_original(-original: Core.Dynamic, -owner: Core.Dynamic, +index: U32, same: {owner == original : Core.Dynamic},
357 certificate: Core.DynamicRead<owner, index>) -> Core.DynamicRead<original, index>:
358 Core.DynamicRead{dynamic, result, exact} = certificate
359 Core.DynamicRead{dynamic, result, Equal.trans(Core.Dynamic & Result<&2, &2, Core.Error, F32>, (dynamic, result),
360 Core.read_dynamic(owner, index), Core.read_dynamic(original, index), exact,
361 Equal.cong(Core.Dynamic, Core.Dynamic & Result<&2, &2, Core.Error, F32>, input => Core.read_dynamic(input, index), owner, original, same))}
362
363def write_original(-shape: Shape.Shape, -original: Core.Tensor<shape>, -owner: Core.Tensor<shape>, +index: U32, +value: F32,
364 same: {owner == original : Core.Tensor<shape>}, certificate: Core.Write<shape, owner, index, value>) -> Core.Write<shape, original, index, value>:
365 Core.Write{tensor, result, exact} = certificate
366 Core.Write{tensor, result, Equal.trans(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (tensor, result),
367 Core.write_flat(shape, owner, index, value), Core.write_flat(shape, original, index, value), exact,
368 Equal.cong(Core.Tensor<shape>, Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, input => Core.write_flat(shape, input, index, value), owner, original, same))}
369
370type ReadValueModel<-original: Core.Dynamic, -index: U32, -value: F32> is Data:
371 ReadValueModel{-equal: {Core.checked_observe_dynamic(original, index) == Some{value} : Maybe<&2, F32>}}
372
373def read_value_model(-original: Core.Dynamic, -retained: Core.Dynamic, +index: U32, +value: F32,
374 -exact: {(retained, Done{value}) == Core.read_dynamic(original, index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
375 certificate: Core.DynamicSourceRead<original, index>) -> ReadValueModel<original, index, value>:
376 Core.DynamicSourceRead{meaning} = certificate
377 ReadValueModel{Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(original, index),
378 Core.dynamic_read_value(Core.read_dynamic(original, index)), Some{value},
379 Equal.sym(Maybe<&2, F32>, Core.dynamic_read_value(Core.read_dynamic(original, index)), Core.checked_observe_dynamic(original, index), meaning),
380 Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.dynamic_read_value(pair),
381 Core.read_dynamic(original, index), (retained, Done{value}),
382 Equal.sym(Core.Dynamic & Result<&2, &2, Core.Error, F32>, (retained, Done{value}), Core.read_dynamic(original, index), exact)))}
383
384type RetainedSourceModel<-original: Core.Dynamic, -retained: Core.Dynamic> is Data:
385 RetainedSourceModel{-kept: Elementwise.SameSource(original, retained)}
386
387def retained_source_model(-original: Core.Dynamic, -retained: Core.Dynamic, +index: U32, -value: F32,
388 -exact: {(retained, Done{value}) == Core.read_dynamic(original, index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
389 certificate: Core.DynamicSourceReadKeeps<original, index>) -> RetainedSourceModel<original, retained>:
390 Core.DynamicSourceReadKeeps{kept} = certificate
391 RetainedSourceModel{other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(retained, other),
392 Core.retained_dynamic_observe(Core.read_dynamic(original, index), other), Core.checked_observe_dynamic(original, other),
393 Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_dynamic_observe(pair, other),
394 (retained, Done{value}), Core.read_dynamic(original, index), exact), kept(other))}
395
396type ExpectedValue<-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
397 -left: Core.Dynamic, -right: Core.Dynamic, -left_value: F32, -right_value: F32> is Data:
398 ExpectedValue{-equal: {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}
399
400def expected_value(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32, -left: Core.Dynamic, -right: Core.Dynamic,
401 +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32,
402 -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
403 left_model: ReadValueModel<left, left_index, left_value>, right_model: ReadValueModel<right, right_index, right_value>) ->
404 ExpectedValue<operation, plan, index, left, right, left_value, right_value>:
405 ReadValueModel{left_equal} = left_model
406 ReadValueModel{right_equal} = right_model
407 ExpectedValue{
408 %indices_exact : {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_indices(operation, left, right, _) : Maybe<&2, F32>}
409 %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(left, left_index), Some{left_value}, left_equal) :
410 {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_left(operation, right, right_index, _) : Maybe<&2, F32>}
411 %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(right, right_index), Some{right_value}, right_equal) :
412 {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_right(operation, left_value, _) : Maybe<&2, F32>}
413 {==}}
414
415type KnownUpdate<-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit> is Data:
416 KnownUpdate{-meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))}
417
418def known_update(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, +index: U32, +value: F32, -unit: Unit,
419 -exact: {(output, Done{unit}) == Core.write_flat(shape, original, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
420 certificate: Core.UpdateModel<shape, original, index, value>) -> KnownUpdate<shape, original, output, index, value, unit>:
421 Core.UpdateModel{meaning} = certificate
422 KnownUpdate{
423 %Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (output, Done{unit}), Core.write_flat(shape, original, index, value), exact) :
424 Core.UpdateMeaning(shape, original, index, value, _)
425 meaning}
426
427def update_route(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
428 meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))) -> Core.ObservationChecked(Core.Packed{shape, output}, index):
429 (checked, rest) = meaning
430 checked
431
432def update_value(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
433 meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))) -> {Core.observe(shape, output, index) == Some{value} : Maybe<&2, F32>}:
434 (checked, rest) = meaning
435 (observed, frame) = rest
436 observed
437
438def update_frame(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
439 meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
440 @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
441 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
442 Core.ObservationChecked(Core.Packed{shape, output}, other) &
443 {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}:
444 (checked, rest) = meaning
445 (observed, frame) = rest
446 frame
447
448type CheckedFrame<-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -other: U32> is Data:
449 CheckedFrame{-equal: {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}
450
451def checked_frame(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, +other: U32,
452 -before: Core.ObservationChecked(Core.Packed{shape, original}, other),
453 -after: Core.ObservationChecked(Core.Packed{shape, output}, other),
454 -physical: {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}) -> CheckedFrame<shape, original, output, other>:
455 CheckedFrame{
456 {\{Core.ObservationModel: after_equal =>
457 {\{Core.ObservationModel: before_equal =>
458 Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, output, other), Core.observe(shape, output, other), Core.checked_observe(shape, original, other),
459 after_equal, Equal.trans(Maybe<&2, F32>, Core.observe(shape, output, other), Core.observe(shape, original, other), Core.checked_observe(shape, original, other),
460 physical, Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, original, other), Core.observe(shape, original, other), before_equal)))
461 } : Core.ObservationModel<shape, original, other, before> -> {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(Core.observation_model(shape, original, other, before))
462 } : Core.ObservationModel<shape, output, other, after> -> {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(Core.observation_model(shape, output, other, after))}
463
464type CheckedUpdatePair<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32, -value: F32,
465 -pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>> is Data:
466 CheckedUpdatePair{-meaning: Core.CheckedUpdateMeaning(shape, original, index, value, pair)}
467
468def checked_update_pair(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32, +value: F32,
469 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, -meaning: Core.UpdateMeaning(shape, original, index, value, pair)) ->
470 CheckedUpdatePair<shape, original, index, value, pair>:
471 (output, result) = pair
472 match result:
473 case Fail{error}:
474 CheckedUpdatePair{Unit{}}
475 case Done{unit}:
476 CheckedUpdatePair{(update_route(shape, original, output, index, value, unit, meaning),
477 (Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, output, index), Core.observe(shape, output, index), Some{value},
478 {\{Core.ObservationModel: equal => equal} :
479 Core.ObservationModel<shape, output, index, update_route(shape, original, output, index, value, unit, meaning)> ->
480 {Core.checked_observe(shape, output, index) == Core.observe(shape, output, index) : Maybe<&2, F32>}}(Core.observation_model(shape, output, index, update_route(shape, original, output, index, value, unit, meaning))),
481 update_value(shape, original, output, index, value, unit, meaning)),
482 other => checked => different =>
483 {\{Tuple: after => physical => (after,
484 {\{CheckedFrame: equal => equal} : CheckedFrame<shape, original, output, other> ->
485 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(checked_frame(shape, original, output, other, checked, after, physical)))
486 } :
487 (Core.ObservationChecked(Core.Packed{shape, output}, other) &
488 {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}) ->
489 (Core.ObservationChecked(Core.Packed{shape, output}, other) &
490 {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(update_frame(shape, original, output, index, value, unit, meaning)(other)(checked)(different))))}
491
492def checked_update_model(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32) -> Core.CheckedUpdateModel<shape, original, index, value>:
493 Core.CheckedUpdateModel{
494 {\{Core.UpdateModel: meaning =>
495 {\{CheckedUpdatePair: checked_meaning => checked_meaning} :
496 CheckedUpdatePair<shape, original, index, value, Core.write_flat(shape, original, index, value)> ->
497 Core.CheckedUpdateMeaning(shape, original, index, value, Core.write_flat(shape, original, index, value))}(checked_update_pair(shape, original, index, value, Core.write_flat(shape, original, index, value), meaning))
498 } : Core.UpdateModel<shape, original, index, value> ->
499 Core.CheckedUpdateMeaning(shape, original, index, value, Core.write_flat(shape, original, index, value))}(update_model(shape, original, index, value))}
500
501def step_write_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
502 -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original_output: Core.Tensor<Shape.output_shape(plan)>,
503 +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32,
504 -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
505 certificate: Core.Write<Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)>,
506 left: Core.Dynamic, right: Core.Dynamic,
507 -left_exact: {(left, Done{left_value}) == Core.read_dynamic(original_left, left_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
508 -right_exact: {(right, Done{right_value}) == Core.read_dynamic(original_right, right_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
509 lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
510 {result == Elementwise.step_write(Shape.output_shape(plan), left, right,
511 Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))) : Elementwise.Step<Shape.output_shape(plan)>} ->
512 {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>}) ->
513 Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
514 Core.Write{output, result, exact} = certificate
515 match result:
516 case Fail{error}:
517 Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
518 lift(Elementwise.Stop{left, right, error},
519 Equal.cong(Core.Tensor<Shape.output_shape(plan)> & Result<&2, &2, Core.Error, Unit>, Elementwise.Step<Shape.output_shape(plan)>,
520 pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair),
521 (output, Fail{error}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)), Unit{}}
522 case Done{unit}:
523 Elementwise.StepCertificate{Elementwise.Continue{Elementwise.State{left, right, output}},
524 lift(Elementwise.Continue{Elementwise.State{left, right, output}},
525 Equal.cong(Core.Tensor<Shape.output_shape(plan)> & Result<&2, &2, Core.Error, Unit>, Elementwise.Step<Shape.output_shape(plan)>,
526 pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair),
527 (output, Done{unit}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)),
528 ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel<original_left, left> -> Elementwise.SameSource(original_left, left)}(retained_source_model(original_left, left, left_index, left_value, left_exact, Core.dynamic_source_read_keeps(original_left, left_index))),
529 ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel<original_right, right> -> Elementwise.SameSource(original_right, right)}(retained_source_model(original_right, right, right_index, right_value, right_exact, Core.dynamic_source_read_keeps(original_right, right_index))),
530 {\{KnownUpdate: meaning =>
531 (update_route(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning),
532 (Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), output, index), Some{Elementwise.scalar(operation, left_value, right_value)},
533 Elementwise.expected(operation, plan, original_left, original_right, index),
534 update_value(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning),
535 {\{ExpectedValue: equal => equal} : ExpectedValue<operation, plan, index, original_left, original_right, left_value, right_value> ->
536 {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}(expected_value(operation, plan, index, original_left, original_right, left_index, right_index, left_value, right_value, indices_exact,
537 read_value_model(original_left, left, left_index, left_value, left_exact, Core.dynamic_source_read_model(original_left, left_index)),
538 read_value_model(original_right, right, right_index, right_value, right_exact, Core.dynamic_source_read_model(original_right, right_index))))),
539 update_frame(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning)))
540 } : KnownUpdate<Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit> ->
541 (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, index) &
542 ({Core.observe(Shape.output_shape(plan), output, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>} &
543 (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), original_output}, other) ->
544 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
545 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) &
546 {Core.observe(Shape.output_shape(plan), output, other) == Core.observe(Shape.output_shape(plan), original_output, other) : Maybe<&2, F32>})))}(known_update(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, exact,
547 update_model(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))))))}
548
549def step_right_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
550 -original_left: Core.Dynamic, -original_right: Core.Dynamic,
551 +left_index: U32, +right_index: U32, +left_value: F32,
552 -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
553 certificate: Core.DynamicRead<original_right, right_index>,
554 original_output: Core.Tensor<Shape.output_shape(plan)>,
555 left: Core.Dynamic,
556 -left_exact: {(left, Done{left_value}) == Core.read_dynamic(original_left, left_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
557 lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
558 {result == Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value,
559 Core.read_dynamic(original_right, right_index)) : Elementwise.Step<Shape.output_shape(plan)>} ->
560 {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>}) ->
561 Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
562 Core.DynamicRead{right, result, exact} = certificate
563 match result:
564 case Fail{error}:
565 Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
566 lift(Elementwise.Stop{left, right, error}, Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
567 pair => Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, pair),
568 (right, Fail{error}), Core.read_dynamic(original_right, right_index), exact)), Unit{}}
569 case Done{+right_value}:
570 step_write_certificate(operation, plan, index, original_left, original_right, original_output,
571 left_index, right_index, left_value, right_value, indices_exact,
572 Core.write_certificate(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), left, right, left_exact, exact,
573 result => equality => lift(result,
574 Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
575 Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, (right, Done{right_value})),
576 Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, Core.read_dynamic(original_right, right_index)), equality,
577 Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
578 pair => Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, pair),
579 (right, Done{right_value}), Core.read_dynamic(original_right, right_index), exact))))
580
581def step_left_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
582 -original_left: Core.Dynamic, original_right: Core.Dynamic, original_output: Core.Tensor<Shape.output_shape(plan)>,
583 +left_index: U32, +right_index: U32,
584 -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
585 lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
586 {result == Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index,
587 Core.read_dynamic(original_left, left_index)) : Elementwise.Step<Shape.output_shape(plan)>} ->
588 {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>},
589 certificate: Core.DynamicRead<original_left, left_index>) ->
590 Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
591 Core.DynamicRead{left, result, exact} = certificate
592 match result:
593 case Fail{error}:
594 Elementwise.StepCertificate{Elementwise.Stop{left, original_right, error},
595 lift(Elementwise.Stop{left, original_right, error}, Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
596 pair => Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, pair),
597 (left, Fail{error}), Core.read_dynamic(original_left, left_index), exact)), Unit{}}
598 case Done{+left_value}:
599 step_right_certificate(operation, plan, index, original_left, original_right,
600 left_index, right_index, left_value, indices_exact, Core.dynamic_read_certificate(original_right, right_index), original_output, left, exact,
601 result => equality => lift(result,
602 Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
603 Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, (left, Done{left_value})),
604 Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, Core.read_dynamic(original_left, left_index)), equality,
605 Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
606 pair => Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, pair),
607 (left, Done{left_value}), Core.read_dynamic(original_left, left_index), exact))))
608
609def step_indices_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
610 state: Elementwise.State<Shape.output_shape(plan)>, result: Result<&2, &1, Core.Error, U32 & U32>,
611 exact: {result == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>}) -> Elementwise.StepCertificate<operation, plan, index, state>:
612 Elementwise.State{left, right, output} = state
613 match result:
614 case Fail{error}:
615 Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
616 Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Elementwise.Step<Shape.output_shape(plan)>,
617 input => Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, input),
618 Fail{error}, Elementwise.input_indices(plan, index), exact), Unit{}}
619 case Done{indices}:
620 (+left_index, +right_index) = indices
621 step_left_certificate(operation, plan, index, left, right, output, left_index, right_index, exact,
622 result => equality => Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
623 Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, Done{(left_index, right_index)}),
624 Elementwise.step(operation, plan, index, Elementwise.State{left, right, output}), equality,
625 Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Elementwise.Step<Shape.output_shape(plan)>,
626 input => Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, input),
627 Done{(left_index, right_index)}, Elementwise.input_indices(plan, index), exact)),
628 Core.dynamic_read_certificate(left, left_index))
629
630def step_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
631 state: Elementwise.State<Shape.output_shape(plan)>) -> Elementwise.StepCertificate<operation, plan, index, state>:
632 step_indices_certificate(operation, plan, index, state, Elementwise.input_indices(plan, index), {==})
633
634def converted_step_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
635 +equal: {True{} == Nat.is_eq(U32.to_nat(index), cursor) : Bool}, -original: Elementwise.State<Shape.output_shape(plan)>,
636 certificate: Elementwise.StepCertificate<operation, plan, index, original>) ->
637 Elementwise.ConvertedCertificate<operation, plan, cursor, index, Shape.BTrue{equal}, original>:
638 Elementwise.StepCertificate{result, exact, meaning} = certificate
639 match result:
640 case Elementwise.Stop{left, right, error}:
641 Elementwise.ConvertedCertificate{Elementwise.NaturalStop{left, right, error},
642 Equal.cong(Elementwise.Step<Shape.output_shape(plan)>, Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
643 step => Elementwise.natural_step_result(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), step),
644 Elementwise.Stop{left, right, error}, Elementwise.step(operation, plan, index, original), exact), Unit{}}
645 case Elementwise.Continue{state}:
646 Elementwise.ConvertedCertificate{Elementwise.NaturalContinue{state, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal)},
647 Equal.cong(Elementwise.Step<Shape.output_shape(plan)>, Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
648 step => Elementwise.natural_step_result(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), step),
649 Elementwise.Continue{state}, Elementwise.step(operation, plan, index, original), exact), meaning}
650
651def natural_decision_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
652 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>) ->
653 Elementwise.ConvertedCertificate<operation, plan, cursor, index, decision, state>:
654 match decision:
655 case Shape.BFalse{equal}:
656 Elementwise.State{left, right, output} = state
657 Elementwise.ConvertedCertificate{Elementwise.NaturalStop{left, right, Core.StorageError{Storage.InvalidIndex{}}}, {==}, Unit{}}
658 case Shape.BTrue{+equal}:
659 converted_step_certificate(operation, plan, cursor, index, equal, state, step_certificate(operation, plan, index, state))
660
661def natural_converted_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
662 -original: Elementwise.State<Shape.output_shape(plan)>,
663 certificate: Elementwise.ConvertedCertificate<operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), original>) ->
664 Elementwise.NaturalCertificate<operation, plan, cursor, original>:
665 Elementwise.ConvertedCertificate{result, exact, meaning} = certificate
666 Elementwise.NaturalCertificate{result, exact, meaning}
667
668def natural_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
669 state: Elementwise.State<Shape.output_shape(plan)>) -> Elementwise.NaturalCertificate<operation, plan, cursor, state>:
670 natural_converted_certificate(operation, plan, cursor, state,
671 natural_decision_certificate(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state))
672
673def lt_zero(+number: Nat, proof: Shape.LT(number, 0n)) -> Empty:
674 match number:
675 case 0n:
676 match proof:
677 case 1n+p:
678 match proof:
679
680def lt_previous_or_equal(+number: Nat, +cursor: Nat, proof: Shape.LT(number, 1n+cursor)) ->
681 Either<Shape.LT(number, cursor), {number == cursor : Nat}>:
682 match number cursor:
683 case 0n 0n:
684 Inr{{==}}
685 case 0n 1n+p:
686 Inl{Unit{}}
687 case 1n+p 0n:
688 Empty.absurd(Either<Shape.LT(1n+p, 0n), {1n+p == 0n : Nat}>, lt_zero(p, proof))
689 case 1n+p 1n+q:
690 {\{Inl: earlier => Inl{earlier}; Inr: equal => Inr{Equal.cong(Nat, Nat, n => 1n+n, p, q, equal)}} :
691 Either<Shape.LT(p, q), {p == q : Nat}> -> Either<Shape.LT(1n+p, 1n+q), {1n+p == 1n+q : Nat}>}(lt_previous_or_equal(p, q, proof))
692
693def lt_big_small_different(+small: Nat, +big: Nat, proof: Shape.LT(small, big)) -> {Nat.is_eq(big, small) == False{} : Bool}:
694 match small big:
695 case 0n 0n:
696 match proof:
697 case 0n 1n+p:
698 {==}
699 case 1n+p 0n:
700 match proof:
701 case 1n+p 1n+q:
702 lt_big_small_different(p, q, proof)
703
704def add_successor_right(+left: Nat, -right: Nat) -> {Nat.add(left, 1n+right) == 1n+Nat.add(left, right) : Nat}:
705 match left:
706 case 0n:
707 {==}
708 case 1n+p:
709 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 1n+right), 1n+Nat.add(p, right), add_successor_right(p, right))
710
711def expected_left_same(+operation: Elementwise.Operation, -current: Core.Dynamic, -original: Core.Dynamic, +index: U32,
712 left: Maybe<&2, F32>, equal: {Core.checked_observe_dynamic(current, index) == Core.checked_observe_dynamic(original, index) : Maybe<&2, F32>}) ->
713 {Elementwise.expected_left(operation, current, index, left) == Elementwise.expected_left(operation, original, index, left) : Maybe<&2, F32>}:
714 match left:
715 case None{}:
716 {==}
717 case Some{+value}:
718 Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, right => Elementwise.expected_right(operation, value, right),
719 Core.checked_observe_dynamic(current, index), Core.checked_observe_dynamic(original, index), equal)
720
721type ExpectedSame<-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
722 -original_left: Core.Dynamic, -original_right: Core.Dynamic, -left: Core.Dynamic, -right: Core.Dynamic> is Data:
723 ExpectedSame{-equal: {Elementwise.expected(operation, plan, left, right, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}
724
725def expected_same_indices(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
726 -original_left: Core.Dynamic, -original_right: Core.Dynamic, -left: Core.Dynamic, -right: Core.Dynamic,
727 -left_same: Elementwise.SameSource(original_left, left), -right_same: Elementwise.SameSource(original_right, right),
728 result: Result<&2, &1, Core.Error, U32 & U32>,
729 -exact: {result == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>}) ->
730 ExpectedSame<operation, plan, index, original_left, original_right, left, right>:
731 match result:
732 case Fail{error}:
733 ExpectedSame{
734 %exact : {Elementwise.expected_indices(operation, left, right, _) == Elementwise.expected_indices(operation, original_left, original_right, _) : Maybe<&2, F32>}
735 {==}}
736 case Done{indices}:
737 (+left_index, +right_index) = indices
738 ExpectedSame{
739 %exact : {Elementwise.expected_indices(operation, left, right, _) == Elementwise.expected_indices(operation, original_left, original_right, _) : Maybe<&2, F32>}
740 Equal.trans(Maybe<&2, F32>, Elementwise.expected_left(operation, right, right_index, Core.checked_observe_dynamic(left, left_index)),
741 Elementwise.expected_left(operation, right, right_index, Core.checked_observe_dynamic(original_left, left_index)),
742 Elementwise.expected_left(operation, original_right, right_index, Core.checked_observe_dynamic(original_left, left_index)),
743 Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, value => Elementwise.expected_left(operation, right, right_index, value),
744 Core.checked_observe_dynamic(left, left_index), Core.checked_observe_dynamic(original_left, left_index), left_same(left_index)),
745 expected_left_same(operation, right, original_right, right_index, Core.checked_observe_dynamic(original_left, left_index), right_same(right_index)))}
746
747def expected_same(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
748 -original_left: Core.Dynamic, -original_right: Core.Dynamic, -left: Core.Dynamic, -right: Core.Dynamic,
749 -left_same: Elementwise.SameSource(original_left, left), -right_same: Elementwise.SameSource(original_right, right)) ->
750 ExpectedSame<operation, plan, index, original_left, original_right, left, right>:
751 expected_same_indices(operation, plan, index, original_left, original_right, left, right, left_same, right_same, Elementwise.input_indices(plan, index), {==})
752
753type PrefixModel<-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
754 -cursor: Nat, -output: Core.Tensor<Shape.output_shape(plan)>> is Data:
755 PrefixModel{-prefix: Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), output})}
756
757def prefix_previous(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
758 -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
759 -before: Core.Tensor<Shape.output_shape(plan)>, -after: Core.Tensor<Shape.output_shape(plan)>,
760 converted: {U32.to_nat(index) == cursor : Nat},
761 prefix: Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), before}),
762 frame: @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), before}, other) ->
763 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
764 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
765 {Core.observe(Shape.output_shape(plan), after, other) == Core.observe(Shape.output_shape(plan), before, other) : Maybe<&2, F32>},
766 +other: U32, +earlier: Shape.LT(U32.to_nat(other), cursor)) ->
767 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
768 {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}:
769 {\{Tuple: before_checked => before_equal =>
770 {\{Tuple: after_checked => after_equal => (after_checked,
771 Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), after, other), Core.observe(Shape.output_shape(plan), before, other),
772 Elementwise.expected(operation, plan, original_left, original_right, other), after_equal, before_equal))} :
773 (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
774 {Core.observe(Shape.output_shape(plan), after, other) == Core.observe(Shape.output_shape(plan), before, other) : Maybe<&2, F32>}) ->
775 (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
776 {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>})}(frame(other)(before_checked)(
777 %Equal.sym(Nat, U32.to_nat(index), cursor, converted) : {Nat.is_eq(_, U32.to_nat(other)) == False{} : Bool}
778 lt_big_small_different(U32.to_nat(other), cursor, earlier)))
779 } :
780 (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), before}, other) &
781 {Core.observe(Shape.output_shape(plan), before, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}) ->
782 (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
783 {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>})}(prefix(other)(earlier))
784
785def prefix_equal(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
786 -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
787 -after: Core.Tensor<Shape.output_shape(plan)>, converted: {U32.to_nat(index) == cursor : Nat},
788 checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, index),
789 observed: {Core.observe(Shape.output_shape(plan), after, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>},
790 +other: U32, equal: {U32.to_nat(other) == cursor : Nat}) ->
791 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
792 {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}:
793 %Injective.u32_natural_injective(index, other)(Equal.trans(Nat, U32.to_nat(index), cursor, U32.to_nat(other), converted,
794 Equal.sym(Nat, U32.to_nat(other), cursor, equal))) :
795 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, _) &
796 {Core.observe(Shape.output_shape(plan), after, _) == Elementwise.expected(operation, plan, original_left, original_right, _) : Maybe<&2, F32>}
797 (checked, observed)
798
799def prefix_extend(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
800 -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
801 -before: Core.Tensor<Shape.output_shape(plan)>, -after: Core.Tensor<Shape.output_shape(plan)>,
802 -converted: {U32.to_nat(index) == cursor : Nat},
803 -prefix: Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), before}),
804 -checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, index),
805 -observed: {Core.observe(Shape.output_shape(plan), after, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>},
806 -frame: @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), before}, other) ->
807 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
808 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
809 {Core.observe(Shape.output_shape(plan), after, other) == Core.observe(Shape.output_shape(plan), before, other) : Maybe<&2, F32>}) ->
810 PrefixModel<operation, plan, original_left, original_right, 1n+cursor, after>:
811 PrefixModel{other => bound =>
812 {\{Inl: earlier => prefix_previous(operation, plan, original_left, original_right, cursor, index, before, after, converted, prefix, frame, other, earlier);
813 Inr: equal => prefix_equal(operation, plan, original_left, original_right, cursor, index, after, converted, checked, observed, other, equal)} :
814 Either<Shape.LT(U32.to_nat(other), cursor), {U32.to_nat(other) == cursor : Nat}> ->
815 (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
816 {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>})}(lt_previous_or_equal(U32.to_nat(other), cursor, bound))}
817
818def invariant_left(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
819 -cursor: Nat, -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
820 invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, Elementwise.State{left, right, output})) ->
821 Elementwise.SameSource(original_left, left):
822 (same, rest) = invariant
823 same
824
825def invariant_right(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
826 -cursor: Nat, -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
827 invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, Elementwise.State{left, right, output})) ->
828 Elementwise.SameSource(original_right, right):
829 (same, rest) = invariant
830 (right_same, prefix) = rest
831 right_same
832
833def invariant_prefix(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
834 -cursor: Nat, -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
835 invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, Elementwise.State{left, right, output})) ->
836 Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), output}):
837 (same, rest) = invariant
838 (right_same, prefix) = rest
839 prefix
840
841def step_same_left(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
842 -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
843 -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
844 meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
845 Elementwise.SameSource(left, after_left):
846 (same, rest) = meaning
847 same
848
849def step_same_right(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
850 -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
851 -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
852 meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
853 Elementwise.SameSource(right, after_right):
854 (same, rest) = meaning
855 (right_same, result) = rest
856 right_same
857
858def step_checked(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
859 -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
860 -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
861 meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
862 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after_output}, index):
863 (same, rest) = meaning
864 (right_same, result) = rest
865 (checked, values) = result
866 checked
867
868def step_observed(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
869 -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
870 -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
871 meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
872 {Core.observe(Shape.output_shape(plan), after_output, index) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}:
873 (same, rest) = meaning
874 (right_same, result) = rest
875 (checked, values) = result
876 (observed, frame) = values
877 observed
878
879def step_frame(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
880 -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
881 -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
882 meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
883 @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) ->
884 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
885 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after_output}, other) &
886 {Core.observe(Shape.output_shape(plan), after_output, other) == Core.observe(Shape.output_shape(plan), output, other) : Maybe<&2, F32>}:
887 (same, rest) = meaning
888 (right_same, result) = rest
889 (checked, values) = result
890 (observed, frame) = values
891 frame
892
893def invariant_advance(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
894 +cursor: Nat, +index: U32, -converted: {U32.to_nat(index) == cursor : Nat},
895 before: Elementwise.State<Shape.output_shape(plan)>, after: Elementwise.State<Shape.output_shape(plan)>,
896 -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, before),
897 -meaning: Elementwise.StepMeaning(operation, plan, index, before, Elementwise.Continue{after})) ->
898 Elementwise.InvariantModel<operation, plan, original_left, original_right, 1n+cursor, after>:
899 Elementwise.State{left, right, output} = before
900 Elementwise.State{after_left, after_right, after_output} = after
901 Elementwise.InvariantModel{(other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_left, other), Core.checked_observe_dynamic(left, other), Core.checked_observe_dynamic(original_left, other),
902 step_same_left(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other),
903 invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)),
904 (other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_right, other), Core.checked_observe_dynamic(right, other), Core.checked_observe_dynamic(original_right, other),
905 step_same_right(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other),
906 invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)),
907 {\{PrefixModel: prefix => prefix} : PrefixModel<operation, plan, original_left, original_right, 1n+cursor, after_output> ->
908 Elementwise.PrefixInvariant(operation, plan, original_left, original_right, 1n+cursor, Core.Packed{Shape.output_shape(plan), after_output})}(prefix_extend(operation, plan, original_left, original_right, cursor, index, output, after_output, converted,
909 invariant_prefix(operation, plan, original_left, original_right, cursor, left, right, output, invariant),
910 step_checked(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning),
911 Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), after_output, index), Elementwise.expected(operation, plan, left, right, index),
912 Elementwise.expected(operation, plan, original_left, original_right, index),
913 step_observed(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning),
914 {\{ExpectedSame: equal => equal} : ExpectedSame<operation, plan, index, original_left, original_right, left, right> ->
915 {Elementwise.expected(operation, plan, left, right, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}(expected_same(operation, plan, index, original_left, original_right, left, right,
916 invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant),
917 invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)))),
918 step_frame(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)))))}
919
920def initial_invariant(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
921 -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>) ->
922 Elementwise.InvariantModel<operation, plan, left, right, 0n, Elementwise.State{left, right, output}>:
923 Elementwise.InvariantModel{(other => {==}, (other => {==}, other => bound =>
924 Empty.absurd(Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) &
925 {Core.observe(Shape.output_shape(plan), output, other) == Elementwise.expected(operation, plan, left, right, other) : Maybe<&2, F32>}, lt_zero(U32.to_nat(other), bound))))}
926
927def add_zero_right(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
928 match number:
929 case 0n:
930 {==}
931 case 1n+p:
932 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero_right(p))
933
934def loop_continue_certificate(+remaining: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
935 -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original: Elementwise.State<Shape.output_shape(plan)>,
936 -after: Elementwise.State<Shape.output_shape(plan)>, -index: U32, -converted: {U32.to_nat(index) == cursor : Nat},
937 natural_exact: {Elementwise.NaturalContinue{after, index, converted} == Elementwise.natural_step(operation, plan, cursor, original) : Elementwise.NaturalStep<Shape.output_shape(plan), cursor>},
938 certificate: Elementwise.LoopCertificate<remaining, operation, plan, 1n+cursor, original_left, original_right, after>) ->
939 Elementwise.LoopCertificate<1n+remaining, operation, plan, cursor, original_left, original_right, original>:
940 Elementwise.LoopCertificate{result, exact, meaning} = certificate
941 Elementwise.LoopCertificate{result,
942 Equal.trans((Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>, result,
943 Elementwise.loop(remaining, operation, plan, 1n+cursor, after), Elementwise.loop(1n+remaining, operation, plan, cursor, original), exact,
944 Equal.cong(Elementwise.NaturalStep<Shape.output_shape(plan), cursor>, (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
945 step => Elementwise.finish_step(Shape.output_shape(plan), cursor, state => Elementwise.loop(remaining, operation, plan, 1n+cursor, state), step),
946 Elementwise.NaturalContinue{after, index, converted}, Elementwise.natural_step(operation, plan, cursor, original), natural_exact)),
947 %Equal.sym(Nat, Nat.add(cursor, 1n+remaining), Nat.add(1n+cursor, remaining), add_successor_right(cursor, remaining)) :
948 Elementwise.LoopMeaning(operation, plan, original_left, original_right, _, result)
949 meaning}
950
951def loop_after_certificate(+remaining: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
952 -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original: Elementwise.State<Shape.output_shape(plan)>,
953 -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, original),
954 certificate: Elementwise.NaturalCertificate<operation, plan, cursor, original>,
955 rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
956 @-invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state) ->
957 Elementwise.LoopCertificate<remaining, operation, plan, 1n+cursor, original_left, original_right, state>) ->
958 Elementwise.LoopCertificate<1n+remaining, operation, plan, cursor, original_left, original_right, original>:
959 Elementwise.NaturalCertificate{result, exact, meaning} = certificate
960 match result:
961 case Elementwise.NaturalStop{left, right, error}:
962 Elementwise.LoopCertificate{((left, right), Fail{error}),
963 Equal.cong(Elementwise.NaturalStep<Shape.output_shape(plan), cursor>, (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
964 step => Elementwise.finish_step(Shape.output_shape(plan), cursor, state => Elementwise.loop(remaining, operation, plan, 1n+cursor, state), step),
965 Elementwise.NaturalStop{left, right, error}, Elementwise.natural_step(operation, plan, cursor, original), exact), Unit{}}
966 case Elementwise.NaturalContinue{state, index, converted}:
967 loop_continue_certificate(remaining, operation, plan, cursor, original_left, original_right, original, state, index, converted, exact,
968 rec(state,
969 {\{Elementwise.InvariantModel: invariant => invariant} :
970 Elementwise.InvariantModel<operation, plan, original_left, original_right, 1n+cursor, state> ->
971 Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state)}(invariant_advance(operation, plan, original_left, original_right, cursor, index, converted,
972 original, state, invariant, meaning))))
973
974def loop_certificate(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
975 -original_left: Core.Dynamic, -original_right: Core.Dynamic, state: Elementwise.State<Shape.output_shape(plan)>,
976 -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, state)) ->
977 Elementwise.LoopCertificate<fuel, operation, plan, cursor, original_left, original_right, state>:
978 match fuel:
979 case 0n:
980 Elementwise.State{left, right, output} = state
981 Elementwise.LoopCertificate{((left, right), Done{Core.Packed{Shape.output_shape(plan), output}}), {==},
982 %Equal.sym(Nat, Nat.add(cursor, 0n), cursor, add_zero_right(cursor)) :
983 Elementwise.PrefixInvariant(operation, plan, original_left, original_right, _, Core.Packed{Shape.output_shape(plan), output})
984 invariant_prefix(operation, plan, original_left, original_right, cursor, left, right, output, invariant)}
985 case 1n++remaining:
986 loop_after_certificate(remaining, operation, plan, cursor, original_left, original_right, state, invariant,
987 natural_certificate(operation, plan, cursor, state),
988 state => invariant => loop_certificate(remaining, operation, plan, 1n+cursor, original_left, original_right, state, invariant))
989
990def successful_pair_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
991 result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
992 -meaning: Elementwise.LoopMeaning(operation, plan, left, right, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), result)) ->
993 Elementwise.MappingModel<operation, plan, left, right, result>:
994 (inputs, outcome) = result
995 match outcome:
996 case Fail{error}:
997 Elementwise.MappingModel{Unit{}}
998 case Done{output}:
999 Elementwise.MappingModel{index => bound => Pair.snd(Core.ObservationChecked(output, index),
1000 {Core.observe_dynamic(output, index) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}, meaning(index)(bound))}
1001
1002def successful_loop_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1003 -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
1004 certificate: Elementwise.LoopCertificate<Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, left, right, Elementwise.State{left, right, output}>) ->
1005 Elementwise.MappingModel<operation, plan, left, right,
1006 Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output})>:
1007 Elementwise.LoopCertificate{result, exact, meaning} = certificate
1008 Elementwise.MappingModel{
1009 %exact : Elementwise.SuccessfulMapping(operation, plan, left, right, _)
1010 {\{Elementwise.MappingModel: mapping => mapping} : Elementwise.MappingModel<operation, plan, left, right, result> ->
1011 Elementwise.SuccessfulMapping(operation, plan, left, right, result)}(successful_pair_mapping(operation, plan, left, right, result, meaning))}
1012
1013def successful_loop_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1014 left: Core.Dynamic, right: Core.Dynamic, output: Core.Tensor<Shape.output_shape(plan)>) ->
1015 Elementwise.MappingModel<operation, plan, left, right,
1016 Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output})>:
1017 successful_loop_certificate(operation, plan, left, right, output,
1018 loop_certificate(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, left, right, Elementwise.State{left, right, output},
1019 {\{Elementwise.InvariantModel: invariant => invariant} : Elementwise.InvariantModel<operation, plan, left, right, 0n, Elementwise.State{left, right, output}> ->
1020 Elementwise.StateInvariant(operation, plan, left, right, 0n, Elementwise.State{left, right, output})}(initial_invariant(operation, plan, left, right, output))))
1021
1022def Laws.checked_writer_pair(shape, original, index, value):
1023 Core.write_certificate(shape, original, index, value)
1024
1025def Laws.checked_writer_source(shape, original, index, value):
1026 checked_update_model(shape, original, index, value)
1027
1028def Laws.actual_elementwise_step(operation, plan, index, original):
1029 step_certificate(operation, plan, index, original)
1030
1031def Laws.successful_elementwise_loop(operation, plan, left, right, output):
1032 successful_loop_mapping(operation, plan, left, right, output)
1033
1034def successful_cached_loop_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1035 left: Core.Dynamic, right: Core.Dynamic, output: Core.Tensor<Shape.output_shape(plan)>) ->
1036 Elementwise.MappingModel<operation, plan, left, right,
1037 Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})>:
1038 Elementwise.MappingModel{
1039 %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Shape.elements_exact(Shape.output_shape(plan))) :
1040 Elementwise.SuccessfulMapping(operation, plan, left, right, Elementwise.loop(_, operation, plan, 0n, Elementwise.State{left, right, output}))
1041 {\{Elementwise.MappingModel: mapping => mapping} :
1042 Elementwise.MappingModel<operation, plan, left, right,
1043 Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output})> ->
1044 Elementwise.SuccessfulMapping(operation, plan, left, right,
1045 Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output}))}(successful_loop_mapping(operation, plan, left, right, output))}
1046
1047def allocated_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1048 result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>, left: Core.Dynamic, right: Core.Dynamic) ->
1049 Elementwise.MappingModel<operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, result)>:
1050 match result:
1051 case Fail{error}:
1052 Elementwise.MappingModel{Unit{}}
1053 case Done{output}:
1054 successful_cached_loop_mapping(operation, plan, left, right, output)
1055
1056def successful_allocated_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic) ->
1057 Elementwise.MappingModel<operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0))>:
1058 Elementwise.MappingModel{
1059 {\{Elementwise.MappingModel: mapping => mapping} :
1060 Elementwise.MappingModel<operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0))> ->
1061 Elementwise.SuccessfulMapping(operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0)))}(allocated_mapping(operation, plan, Core.new(Shape.output_shape(plan), 0.0), left, right))}
1062
1063def successful_binary_mapping(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic) ->
1064 Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
1065 Parallel.binary_mapping(operation, left, right)
1066
1067def Laws.successful_elementwise_cached_loop(operation, plan, left, right, output):
1068 successful_cached_loop_mapping(operation, plan, left, right, output)
1069
1070def Laws.successful_elementwise_allocated(operation, plan, left, right):
1071 successful_allocated_mapping(operation, plan, left, right)
1072
1073def Laws.successful_elementwise_binary(operation, left, right):
1074 successful_binary_mapping(operation, left, right)
1075
1076def independent_pair_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
1077 result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
1078 -shared: Elementwise.SuccessfulMapping(operation, plan, left, right, result)) -> Laws.IndependentModel<operation, plan, left, right, result>:
1079 (inputs, outcome) = result
1080 match outcome:
1081 case Fail{error}:
1082 Laws.IndependentModel{Unit{}}
1083 case Done{output}:
1084 Laws.IndependentModel{index => inside => Equal.trans(Maybe<&2, F32>, Core.observe_dynamic(output, index), Elementwise.expected(operation, plan, left, right, index),
1085 Projection.specified_expected(operation, left, right, Projection.offset_spec(plan, U32.to_nat(index))), shared(index)(inside),
1086 Projection.expected_projection_refines(operation, plan, left, right, index))}
1087
1088def independent_loop_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1089 left: Core.Dynamic, right: Core.Dynamic, output: Core.Tensor<Shape.output_shape(plan)>) ->
1090 Laws.IndependentModel<operation, plan, left, right,
1091 Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})>:
1092 Laws.IndependentModel{
1093 {\{Elementwise.MappingModel: mapping =>
1094 {\{Laws.IndependentModel: independent => independent} :
1095 Laws.IndependentModel<operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})> ->
1096 Laws.IndependentMapping(operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output}))}(independent_pair_mapping(operation, plan, left, right,
1097 Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output}), mapping))
1098 } : Elementwise.MappingModel<operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})> ->
1099 Laws.IndependentMapping(operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output}))}(successful_cached_loop_mapping(operation, plan, left, right, output))}
1100
1101type IndependentPlannedModel<-operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic,
1102 -result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
1103 -plan: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>> is Data:
1104 IndependentPlannedModel{-mapping: Laws.IndependentPlanned(operation, left, right, result, plan)}
1105
1106def independent_planned_pair(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic,
1107 result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
1108 plan: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, -shared: Elementwise.PlannedMeaning(operation, left, right, result, plan)) ->
1109 IndependentPlannedModel<operation, left, right, result, plan>:
1110 match plan:
1111 case Fail{error}:
1112 IndependentPlannedModel{Unit{}}
1113 case Done{+plan}:
1114 IndependentPlannedModel{{\{Laws.IndependentModel: independent => independent} : Laws.IndependentModel<operation, plan, left, right, result> -> Laws.IndependentMapping(operation, plan, left, right, result)}(independent_pair_mapping(operation, plan, left, right, result, shared))}
1115
1116def independent_binary_reasoning(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic) ->
1117 Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
1118 Laws.IndependentBinaryModel{
1119 {\{Elementwise.BinaryModel: mapping =>
1120 {\{IndependentPlannedModel: independent => independent} :
1121 IndependentPlannedModel<operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right)> ->
1122 Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(independent_planned_pair(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right), mapping))
1123 } : Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)> ->
1124 Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(successful_binary_mapping(operation, left, right))}
1125
1126def independent_binary_mapping(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic) ->
1127 Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
1128 Laws.IndependentBinaryModel{
1129 {\{Laws.IndependentBinaryModel: mapping => mapping} :
1130 Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)> ->
1131 Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(independent_binary_reasoning(operation, left, right))}
1132
1133def Laws.independent_elementwise_loop(operation, plan, left, right, output):
1134 independent_loop_mapping(operation, plan, left, right, output)
1135
1136def Laws.independent_elementwise_binary(operation, left, right):
1137 independent_binary_mapping(operation, left, right)
1138
1139def Laws.public_add_dispatch(left, right):
1140 {==}
1141
1142def Laws.public_sub_dispatch(left, right):
1143 {==}
1144
1145def Laws.public_mul_dispatch(left, right):
1146 {==}