src/tensor/reduction_PROOF.bend
bendtorch-core@0.1.0.0 · 854 lines · 51 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
5import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
6import bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend as Laws
7import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
8import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
9import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
10import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
11import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
12import bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend as TransformLaws
13import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
14import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
15import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
16import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
17import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
18import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
19import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
20
21def SomeMatches(-value: F32, result: Maybe<&2, F32>) -> Data:
22 match result:
23 case None{}:
24 Empty
25 case Some{other}:
26 {value == other : F32}
27
28def some_injective(+left: F32, +right: F32, equal: {Some{left} == Some{right} : Maybe<&2, F32>}) -> {left == right : F32}:
29 %equal : SomeMatches(left, _)
30 {==}
31
32def no_value(+value: F32, equal: {None{} == Some{value} : Maybe<&2, F32>}) -> Empty:
33 %Equal.sym(Maybe<&2, F32>, None{}, Some{value}, equal) : SomeMatches(value, _)
34 {==}
35
36def natural_reflexive(+value: Nat) -> {Nat.is_eq(value, value) == True{} : Bool}:
37 match value:
38 case 0n:
39 {==}
40 case 1n+tail:
41 natural_reflexive(tail)
42
43def conversion_clash(+a: Nat, +b: Nat, exact: {a == b : Nat}, rejected: {False{} == Nat.is_eq(a, b) : Bool}) -> Empty:
44 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_eq(a, a), False{},
45 Equal.sym(Bool, Nat.is_eq(a, a), True{}, natural_reflexive(a)),
46 Equal.trans(Bool, Nat.is_eq(a, a), Nat.is_eq(a, b), False{},
47 Equal.cong(Nat, Bool, n => Nat.is_eq(a, n), a, b, exact), Equal.sym(Bool, False{}, Nat.is_eq(a, b), rejected))))
48
49def logical_keeps(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
50 values: List<&2, F32>, logical: Laws.LogicalValues(fuel, shape, original, cursor, values),
51 -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
52 Laws.LogicalValues(fuel, shape, tensor, cursor, values):
53 match fuel values:
54 case 0n Nil{}:
55 Unit{}
56 case 1n+tail +value <> rest:
57 Laws.LogicalStep{exact, observed, remaining} = logical
58 Laws.LogicalStep{exact, Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, U32.from_nat(cursor)),
59 Core.checked_observe(shape, original, U32.from_nat(cursor)), Some{value}, kept(U32.from_nat(cursor)), observed),
60 logical_keeps(tail, shape, original, tensor, 1n+cursor, rest, remaining, kept)}
61 case 0n value <> rest:
62 Empty.absurd(Laws.LogicalValues(0n, shape, tensor, cursor, value <> rest), logical)
63 case 1n+tail Nil{}:
64 Empty.absurd(Laws.LogicalValues(1n+tail, shape, tensor, cursor, Nil{}), logical)
65
66def read_interpretation(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
67 +head: F32, +values: List<&2, F32>, tensor: Core.Tensor<shape>, result: Result<&2, &2, Core.Error, F32>,
68 rec: @tensor: Core.Tensor<shape> -> @logical: Laws.LogicalValues(fuel, shape, tensor, 1n+cursor, values) ->
69 {Laws.loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head))) ==
70 Some{Reduction.sequential_sum(values, F32.add(accumulator, head))} : Maybe<&2, F32>},
71 remaining: Laws.LogicalValues(fuel, shape, original, 1n+cursor, values),
72 meaning: {Core.result_value(result) == Some{head} : Maybe<&2, F32>},
73 -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
74 {Laws.loop_value(shape, Reduction.read_step(shape,
75 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))) ==
76 Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>}:
77 match result:
78 case Fail{error}:
79 Empty.absurd({None{} == Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>}, no_value(head, meaning))
80 case Done{+value}:
81 %Equal.sym(F32, value, head, some_injective(value, head, meaning)) :
82 {Laws.loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, _))) ==
83 Some{Reduction.sequential_sum(values, F32.add(accumulator, head))} : Maybe<&2, F32>}
84 %rec(tensor, logical_keeps(fuel, shape, original, tensor, 1n+cursor, values, remaining, kept)) :
85 {Laws.loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head))) == _ : Maybe<&2, F32>}
86 {==}
87
88def read_certificate_interpretation(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat,
89 +accumulator: F32, +head: F32, +values: List<&2, F32>,
90 rec: @tensor: Core.Tensor<shape> -> @logical: Laws.LogicalValues(fuel, shape, tensor, 1n+cursor, values) ->
91 {Laws.loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head))) ==
92 Some{Reduction.sequential_sum(values, F32.add(accumulator, head))} : Maybe<&2, F32>},
93 observed: {Core.checked_observe(shape, original, U32.from_nat(cursor)) == Some{head} : Maybe<&2, F32>},
94 remaining: Laws.LogicalValues(fuel, shape, original, 1n+cursor, values), certificate: Core.Read<shape, original, U32.from_nat(cursor)>,
95 meaning: {Core.read_value(shape, Core.read_flat(shape, original, U32.from_nat(cursor))) == Core.checked_observe(shape, original, U32.from_nat(cursor)) : Maybe<&2, F32>},
96 -kept: @+other: U32 -> {Core.retained_read_observe(shape, Core.read_flat(shape, original, U32.from_nat(cursor)), other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
97 {Laws.loop_value(shape, Reduction.read_step(shape,
98 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))) ==
99 Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>}:
100 Core.Read{tensor, +result, +exact} = certificate
101 %exact :
102 {Laws.loop_value(shape, Reduction.read_step(shape,
103 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, _)) ==
104 Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>}
105 read_interpretation(fuel, shape, original, cursor, accumulator, head, values, tensor, result, rec, remaining,
106 Equal.trans(Maybe<&2, F32>, Core.result_value(result), Core.checked_observe(shape, original, U32.from_nat(cursor)), Some{head},
107 Equal.trans(Maybe<&2, F32>, Core.result_value(result), Core.read_value(shape, Core.read_flat(shape, original, U32.from_nat(cursor))),
108 Core.checked_observe(shape, original, U32.from_nat(cursor)),
109 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
110 (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact),
111 meaning), observed),
112 other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other),
113 Core.retained_read_observe(shape, Core.read_flat(shape, original, U32.from_nat(cursor)), other), Core.checked_observe(shape, original, other),
114 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other),
115 (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), kept(other)))
116
117def decision_interpretation(+fuel: Nat, -shape: Shape.Shape, tensor: Core.Tensor<shape>, +cursor: Nat,
118 +accumulator: F32, +head: F32, +values: List<&2, F32>,
119 -rec: @tensor: Core.Tensor<shape> -> @logical: Laws.LogicalValues(fuel, shape, tensor, 1n+cursor, values) ->
120 {Laws.loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head))) ==
121 Some{Reduction.sequential_sum(values, F32.add(accumulator, head))} : Maybe<&2, F32>},
122 logical: Laws.LogicalStep<fuel, shape, tensor, cursor, head, values>,
123 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>) ->
124 Laws.Interpretation<Laws.loop_value(shape, Reduction.sum_decided(shape,
125 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), tensor, cursor, U32.from_nat(cursor), accumulator, decision)),
126 Some{Reduction.sequential_sum(head <> values, accumulator)}>:
127 Laws.LogicalStep{exact, observed, remaining} = logical
128 match decision:
129 case Shape.BFalse{equal}:
130 Laws.Interpretation{unit => Empty.absurd({None{} == Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>},
131 conversion_clash(U32.to_nat(U32.from_nat(cursor)), cursor, exact, equal))}
132 case Shape.BTrue{equal}:
133 Laws.Interpretation{unit =>
134 prove : @certificates: Core.SourceRead<shape, tensor, U32.from_nat(cursor)> & Core.SourceReadKeeps<shape, tensor, U32.from_nat(cursor)> ->
135 {Laws.loop_value(shape, Reduction.read_step(shape,
136 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, tensor, U32.from_nat(cursor)))) ==
137 Some{Reduction.sequential_sum(head <> values, accumulator)} : Maybe<&2, F32>} =
138 \{Tuple: \{Core.SourceRead: meaning => \{Core.SourceReadKeeps: kept =>
139 read_certificate_interpretation(fuel, shape, tensor, cursor, accumulator, head, values, rec, observed, remaining,
140 Core.read_certificate(shape, tensor, U32.from_nat(cursor)), meaning, kept)}}}
141 prove((Core.source_read_model(shape, tensor, U32.from_nat(cursor)), Core.source_read_keeps(shape, tensor, U32.from_nat(cursor))))}
142
143def Laws.ordered_loop_interpretation(fuel, shape, tensor, cursor, accumulator, values, logical):
144 match fuel values:
145 case 0n Nil{}:
146 Laws.Interpretation{unit => {==}}
147 case 1n+tail +head <> +rest:
148 decision_interpretation(tail, shape, tensor, cursor, accumulator, head, rest,
149 tensor => logical =>
150 claim : @certificate: Laws.Interpretation<Laws.loop_value(shape, Reduction.natural_sum_loop(tail, shape, tensor, 1n+cursor, F32.add(accumulator, head))),
151 Some{Reduction.sequential_sum(rest, F32.add(accumulator, head))}> ->
152 {Laws.loop_value(shape, Reduction.natural_sum_loop(tail, shape, tensor, 1n+cursor, F32.add(accumulator, head))) ==
153 Some{Reduction.sequential_sum(rest, F32.add(accumulator, head))} : Maybe<&2, F32>} =
154 \{Laws.Interpretation: proof => proof(Unit{})}
155 claim(Laws.ordered_loop_interpretation(tail, shape, tensor, 1n+cursor, F32.add(accumulator, head), rest, logical)),
156 logical, Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)))
157 case 0n head <> rest:
158 Laws.Interpretation{unit => Empty.absurd({Laws.loop_value(shape, Reduction.natural_sum_loop(0n, shape, tensor, cursor, accumulator)) ==
159 Some{Reduction.sequential_sum(head <> rest, accumulator)} : Maybe<&2, F32>}, logical)}
160 case 1n+tail Nil{}:
161 Laws.Interpretation{unit => Empty.absurd({Laws.loop_value(shape, Reduction.natural_sum_loop(1n+tail, shape, tensor, cursor, accumulator)) ==
162 Some{Reduction.sequential_sum(Nil{}, accumulator)} : Maybe<&2, F32>}, logical)}
163
164def success_keeps(-shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>,
165 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>, +other: U32,
166 kept: {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
167 {Laws.successful_observe(shape, tensor, result, other) == Laws.successful_observe(shape, original, result, other) : Maybe<&2, F32>}:
168 match result:
169 case Fail{error}:
170 {==}
171 case Done{pair}:
172 kept
173
174def preserved_read(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
175 tensor: Core.Tensor<shape>, result: Result<&2, &2, Core.Error, F32>,
176 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.Preserved<shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
177 -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
178 Laws.Preserved<shape, original, Reduction.read_step(shape,
179 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))>:
180 match result:
181 case Fail{error}:
182 Laws.Preserved{other => {==}}
183 case Done{+value}:
184 Laws.Preserved{other =>
185 claim : @certificate: Laws.Preserved<shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value))> ->
186 {Laws.retained_observe(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)), other) ==
187 Laws.successful_observe(shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)), other) : Maybe<&2, F32>} =
188 \{Laws.Preserved: kept => kept(other)}
189 Equal.trans(Maybe<&2, F32>,
190 Laws.retained_observe(shape, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)), other),
191 Laws.successful_observe(shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)), other),
192 Laws.successful_observe(shape, original, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)), other),
193 claim(rec(tensor, F32.add(accumulator, value))), success_keeps(shape, original, tensor,
194 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)), other, kept(other)))}
195
196def preserved_certificate(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
197 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.Preserved<shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
198 certificate: Core.Read<shape, original, U32.from_nat(cursor)>, -retention: Core.SourceReadKeeps<shape, original, U32.from_nat(cursor)>) ->
199 Laws.Preserved<shape, original, Reduction.read_step(shape,
200 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))>:
201 Core.Read{tensor, +result, +exact} = certificate
202 Laws.Preserved{other =>
203 claim : @certificate: Laws.Preserved<shape, original, Reduction.read_step(shape,
204 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))> ->
205 {Laws.retained_observe(shape, Reduction.read_step(shape,
206 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result)), other) ==
207 Laws.successful_observe(shape, original, Reduction.read_step(shape,
208 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result)), other) : Maybe<&2, F32>} =
209 \{Laws.Preserved: kept => kept(other)}
210 prove : @retention: Core.SourceReadKeeps<shape, original, U32.from_nat(cursor)> ->
211 {Laws.retained_observe(shape, Reduction.read_step(shape,
212 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor))), other) ==
213 Laws.successful_observe(shape, original, Reduction.read_step(shape,
214 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor))), other) : Maybe<&2, F32>} =
215 \{Core.SourceReadKeeps: kept =>
216 %exact :
217 {Laws.retained_observe(shape, Reduction.read_step(shape,
218 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, _), other) ==
219 Laws.successful_observe(shape, original, Reduction.read_step(shape,
220 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, _), other) : Maybe<&2, F32>}
221 claim(preserved_read(fuel, shape, original, cursor, accumulator, tensor, result, rec,
222 other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other),
223 Core.retained_read_observe(shape, Core.read_flat(shape, original, U32.from_nat(cursor)), other), Core.checked_observe(shape, original, other),
224 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other),
225 (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), kept(other))))}
226 prove(retention)}
227
228def preserved_decision(+fuel: Nat, -shape: Shape.Shape, tensor: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
229 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.Preserved<shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
230 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>) ->
231 Laws.Preserved<shape, tensor, Reduction.sum_decided(shape,
232 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), tensor, cursor, U32.from_nat(cursor), accumulator, decision)>:
233 match decision:
234 case Shape.BFalse{equal}:
235 Laws.Preserved{other => {==}}
236 case Shape.BTrue{equal}:
237 preserved_certificate(fuel, shape, tensor, cursor, accumulator, rec,
238 Core.read_certificate(shape, tensor, U32.from_nat(cursor)), Core.source_read_keeps(shape, tensor, U32.from_nat(cursor)))
239
240def Laws.ordered_loop_preservation(fuel, shape, tensor, cursor, accumulator):
241 match fuel:
242 case 0n:
243 Laws.Preserved{other => {==}}
244 case 1n+tail:
245 preserved_decision(tail, shape, tensor, cursor, accumulator,
246 tensor => value => Laws.ordered_loop_preservation(tail, shape, tensor, 1n+cursor, value),
247 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)))
248
249def sum_result_value(-shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>) ->
250 {Reduction.sum_observation(shape, Reduction.sum_result(shape, result)) == Laws.loop_value(shape, result) : Maybe<&2, F32>}:
251 match result:
252 case Fail{error}:
253 {==}
254 case Done{pair}:
255 (tensor, value) = pair
256 {==}
257
258
259
260
261
262
263type Fact<-P: Type> is Data:
264 Fact{-proof: P}
265
266def allowed_true(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool, +value: F32,
267 observed: {Lifecycle.observe_allowed(depth, length, array, index, allowed) == Some{value} : Maybe<&2, F32>}) ->
268 {allowed == True{} : Bool}:
269 match allowed:
270 case False{}:
271 Empty.absurd({False{} == True{} : Bool}, no_value(value, observed))
272 case True{}:
273 {==}
274
275def allowed_observe(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool,
276 accepted: {allowed == True{} : Bool}, matched: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
277 {Lifecycle.observe_allowed(depth, length, array, index, allowed) ==
278 Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}:
279 match allowed:
280 case False{}:
281 Empty.absurd({None{} == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}, Arith.clash(accepted))
282 case True{}:
283 %Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, matched) :
284 {Lifecycle.observe_index(depth, length, array, index, _) == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}
285 {==}
286
287
288
289def read_word(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original),
290 -valid: {Storage.bounds(depth, length) == True{} : Bool},
291 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, -array: Array<F32>, +index: U32,
292 -pair: Array<F32> & F32, -read: {pair == Array.get(F32, array, index) : Array<F32> & F32},
293 -same: {array == original : Array<F32>}, +value: F32,
294 -observed: {Core.checked_observe(shape, Core.TTensor{Storage.Owned{depth, length, original, balanced, valid}, exact}, index) ==
295 Some{value} : Maybe<&2, F32>}) -> Fact<{Refinement.second(F32, pair) == value : F32}>:
296 Fact{some_injective(Refinement.second(F32, pair), value,
297 Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, pair)}, Some{Refinement.second(F32, Array.get(F32, array, index))}, Some{value},
298 Equal.cong(Array<F32> & F32, Maybe<&2, F32>, p => Some{Refinement.second(F32, p)}, pair, Array.get(F32, array, index), read),
299 Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, array, index))},
300 Model.observe(F32, depth, array, Refinement.route(depth, index)), Some{value},
301 Refinement.law_get_refines(F32, depth, array, index,
302 {\{Reduction.Fact: p => p} : Reduction.Fact<(Model.Balanced(F32, depth, array))> -> Model.Balanced(F32, depth, array)}(
303 Reduction.kept_balanced(depth, original, balanced, array, same))),
304 Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, array, Refinement.route(depth, index)),
305 Model.observe(F32, depth, original, Refinement.route(depth, index)), Some{value},
306 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)), array, original, same),
307 Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, original, Refinement.route(depth, index)),
308 Lifecycle.observe_allowed(depth, length, original, index, Nat.is_lt(U32.to_nat(index), length)), Some{value},
309 Equal.sym(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, original, index, Nat.is_lt(U32.to_nat(index), length)),
310 Model.observe(F32, depth, original, Refinement.route(depth, index)),
311 allowed_observe(depth, length, original, index, Nat.is_lt(U32.to_nat(index), length),
312 allowed_true(depth, length, original, index, Nat.is_lt(U32.to_nat(index), length), value, observed),
313 Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index),
314 Route.index_complete(depth, length, index, valid,
315 allowed_true(depth, length, original, index, Nat.is_lt(U32.to_nat(index), length), value, observed))))),
316 observed)))))}
317
318
319
320def run_value(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original),
321 -valid: {Storage.bounds(depth, length) == True{} : Bool},
322 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, fuel: Nat, +cursor: Nat, +accumulator: F32,
323 -array: Array<F32>, pair: Array<F32> & F32, -read: {pair == Array.get(F32, array, U32.from_nat(cursor)) : Array<F32> & F32},
324 -same: {array == original : Array<F32>}, values: List<&2, F32>,
325 logical: Laws.LogicalValues(1n+fuel, shape, Core.TTensor{Storage.Owned{depth, length, original, balanced, valid}, exact}, cursor, values)) ->
326 Fact<{Pair.fst(F32, Array<F32>, Reduction.array_run(fuel, cursor, accumulator, pair)) == Reduction.sequential_sum(values, accumulator) : F32}>:
327 match fuel pair values:
328 case 0n Tuple{kept, word} +value <> Nil{}:
329 Laws.LogicalStep{index_exact, observed, remaining} = logical
330 Fact{Equal.cong(F32, F32, w => F32.add(accumulator, w), word, value,
331 {\{Fact: p => p} : Fact<({Refinement.second(F32, (kept, word)) == value : F32})> -> {word == value : F32}}(
332 read_word(shape, depth, length, original, balanced, valid, exact, array, U32.from_nat(cursor), (kept, word), read, same, value, observed)))}
333 case 0n Tuple{kept, word} value <> later <> others:
334 Laws.LogicalStep{index_exact, observed, remaining} = logical
335 Fact{Empty.absurd({Pair.fst(F32, Array<F32>, Reduction.array_run(0n, cursor, accumulator, (kept, word))) ==
336 Reduction.sequential_sum(value <> later <> others, accumulator) : F32}, remaining)}
337 case 1n+next Tuple{kept, word} +value <> rest:
338 Laws.LogicalStep{index_exact, observed, remaining} = logical
339 -word_same = {\{Fact: p => p} : Fact<({Refinement.second(F32, (kept, word)) == value : F32})> -> {word == value : F32}}(
340 read_word(shape, depth, length, original, balanced, valid, exact, array, U32.from_nat(cursor), (kept, word), read, same, value, observed))
341 Fact{
342 %word_same : {Pair.fst(F32, Array<F32>, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word),
343 Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, _)) : F32}
344 {\{Fact: p => p} : Fact<({Pair.fst(F32, Array<F32>, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word),
345 Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, word)) : F32})> ->
346 {Pair.fst(F32, Array<F32>, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word),
347 Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, word)) : F32}}(
348 run_value(shape, depth, length, original, balanced, valid, exact, next, 1n+cursor, F32.add(accumulator, word), kept,
349 Array.get(F32, kept, U32.from_nat(1n+cursor)), {==},
350 {\{Reduction.Fact: p => p} : Reduction.Fact<({Reduction.array_from((kept, word)) == original : Array<F32>})> -> {kept == original : Array<F32>}}(
351 Reduction.read_keeps(depth, original, balanced, array, U32.from_nat(cursor), (kept, word), read, same)),
352 rest, remaining))}
353 case fuel pair Nil{}:
354 Empty.absurd(Fact<{Pair.fst(F32, Array<F32>, Reduction.array_run(fuel, cursor, accumulator, pair)) == Reduction.sequential_sum(Nil{}, accumulator) : F32}>, logical)
355
356
357def fold_value(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original),
358 -valid: {Storage.bounds(depth, length) == True{} : Bool},
359 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +fuel: Nat, +accumulator: F32,
360 +values: List<&2, F32>,
361 logical: Laws.LogicalValues(fuel, shape, Core.TTensor{Storage.Owned{depth, length, original, balanced, valid}, exact}, 0n, values)) ->
362 Fact<{Pair.fst(F32, Array<F32>, Reduction.array_sum(fuel, 0n, accumulator, original)) == Reduction.sequential_sum(values, accumulator) : F32}>:
363 match fuel values:
364 case 0n Nil{}:
365 Fact{{==}}
366 case 1n+rest values:
367 Fact{{\{Fact: p => p} : Fact<({Pair.fst(F32, Array<F32>, Reduction.array_sum(1n+rest, 0n, accumulator, original)) == Reduction.sequential_sum(values, accumulator) : F32})> ->
368 {Pair.fst(F32, Array<F32>, Reduction.array_sum(1n+rest, 0n, accumulator, original)) == Reduction.sequential_sum(values, accumulator) : F32}}(
369 run_value(shape, depth, length, original, balanced, valid, exact, rest, 0n, accumulator, original,
370 Array.get(F32, original, U32.from_nat(0n)), {==}, {==}, values, logical))}
371 case 0n value <> others:
372 Empty.absurd(Fact<{Pair.fst(F32, Array<F32>, Reduction.array_sum(0n, 0n, accumulator, original)) ==
373 Reduction.sequential_sum(value <> others, accumulator) : F32}>, logical)
374
375
376def empty_values(-shape: Shape.Shape, -exact: {0n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, fuel: Nat, +cursor: Nat,
377 values: List<&2, F32>,
378 logical: Laws.LogicalValues(fuel, shape, Core.TTensor{Storage.Empty{}, exact}, cursor, values)) ->
379 Fact<{0.0 == Reduction.sequential_sum(values, 0.0) : F32}>:
380 match fuel values:
381 case 0n Nil{}:
382 Fact{{==}}
383 case 1n+rest +value <> others:
384 Laws.LogicalStep{index_exact, observed, remaining} = logical
385 Fact{Empty.absurd({0.0 == Reduction.sequential_sum(value <> others, 0.0) : F32}, no_value(value, observed))}
386 case 0n value <> others:
387 Empty.absurd(Fact<{0.0 == Reduction.sequential_sum(value <> others, 0.0) : F32}>, logical)
388 case 1n+rest Nil{}:
389 Empty.absurd(Fact<{0.0 == Reduction.sequential_sum(Nil{}, 0.0) : F32}>, logical)
390
391def owned_value(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original),
392 -valid: {Storage.bounds(depth, length) == True{} : Bool},
393 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +fuel: Nat, +values: List<&2, F32>,
394 logical: Laws.LogicalValues(fuel, shape, Core.TTensor{Storage.Owned{depth, length, original, balanced, valid}, exact}, 0n, values),
395 pair: F32 & Array<F32>, -kept: Reduction.Fact<{Pair.snd(F32, Array<F32>, pair) == original : Array<F32>}>,
396 -folded: {pair == Reduction.array_sum(fuel, 0n, 0.0, original) : F32 & Array<F32>}) ->
397 Fact<{Laws.loop_value(shape, Reduction.owned_sum(shape, depth, length, original, balanced, valid, exact, pair, kept)) ==
398 Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}>:
399 (value, retained) = pair
400 Fact{Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, value, Reduction.sequential_sum(values, 0.0),
401 Equal.trans(F32, value, Pair.fst(F32, Array<F32>, Reduction.array_sum(fuel, 0n, 0.0, original)), Reduction.sequential_sum(values, 0.0),
402 Equal.cong(F32 & Array<F32>, F32, p => Pair.fst(F32, Array<F32>, p), (value, retained), Reduction.array_sum(fuel, 0n, 0.0, original), folded),
403 {\{Fact: p => p} : Fact<({Pair.fst(F32, Array<F32>, Reduction.array_sum(fuel, 0n, 0.0, original)) == Reduction.sequential_sum(values, 0.0) : F32})> ->
404 {Pair.fst(F32, Array<F32>, Reduction.array_sum(fuel, 0n, 0.0, original)) == Reduction.sequential_sum(values, 0.0) : F32}}(
405 fold_value(shape, depth, length, original, balanced, valid, exact, fuel, 0.0, values, logical))))}
406
407
408
409def tensor_value(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
410 logical: Laws.LogicalValues(fuel, shape, tensor, 0n, values)) ->
411 Fact<{Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}>:
412 Core.TTensor{storage, exact} = tensor
413 match storage:
414 case Storage.Empty{}:
415 Fact{Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, 0.0, Reduction.sequential_sum(values, 0.0),
416 {\{Fact: p => p} : Fact<({0.0 == Reduction.sequential_sum(values, 0.0) : F32})> -> {0.0 == Reduction.sequential_sum(values, 0.0) : F32}}(
417 empty_values(shape, exact, fuel, 0n, values, logical)))}
418 case Storage.Owned{+depth, +length, array, balanced, valid}:
419 owned_value(shape, depth, length, array, balanced, valid, exact, fuel, values, logical, Reduction.array_sum(fuel, 0n, 0.0, array),
420 Reduction.array_sum_keeps(depth, array, balanced, fuel, 0n, 0.0, array, {==}), {==})
421
422
423
424type Words<-fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>> is Data:
425 Words{values: List<&2, F32>, -logical: Laws.LogicalValues(fuel, shape, tensor, 0n, values)}
426
427def words_of(-fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
428 meaning: Laws.LoopMeaning(fuel, shape, tensor, 0n, 0.0, result),
429 status: Totality.Status<Core.Error, Core.Tensor<shape> & F32, result>) -> Fact<Words<fuel, shape, tensor>>:
430 match result:
431 case Fail{error}:
432 Fact{{\{Totality.Status: successful => Empty.absurd(Words<fuel, shape, tensor>, Arith.clash(successful))} :
433 Totality.Status<Core.Error, Core.Tensor<shape> & F32, Fail{error}> -> Words<fuel, shape, tensor>}(status)}
434 case Done{pair}:
435 (retained, value) = pair
436 Laws.SumMeaning{values, logical, fold} = meaning
437 Fact{Words{values, logical}}
438
439def meaning_from(-shape: Shape.Shape, -fuel: Nat, -tensor: Core.Tensor<shape>, values: List<&2, F32>,
440 logical: Laws.LogicalValues(fuel, shape, tensor, 0n, values), result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
441 value: {Laws.loop_value(shape, result) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}) ->
442 Laws.LoopMeaning(fuel, shape, tensor, 0n, 0.0, result):
443 match result:
444 case Fail{error}:
445 Unit{}
446 case Done{pair}:
447 (retained, +sum) = pair
448 Laws.SumMeaning{values, logical, some_injective(sum, Reduction.sequential_sum(values, 0.0), value)}
449
450def tensor_source(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>, words: Words<fuel, shape, tensor>) ->
451 Fact<Laws.SourceSum<fuel, shape, tensor, 0n, 0.0, Reduction.tensor_sum(shape, fuel, tensor)>>:
452 Words{values, logical} = words
453 Fact{Laws.SourceSum{unit => meaning_from(shape, fuel, tensor, values, logical, Reduction.tensor_sum(shape, fuel, tensor),
454 {\{Fact: p => p} : Fact<({Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>})> ->
455 {Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}}(
456 tensor_value(shape, fuel, tensor, values, logical)))}}
457
458def owned_preserved(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original),
459 -valid: {Storage.bounds(depth, length) == True{} : Bool},
460 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
461 pair: F32 & Array<F32>, -kept: Reduction.Fact<{Pair.snd(F32, Array<F32>, pair) == original : Array<F32>}>) ->
462 Fact<Laws.Preserved<shape, Core.TTensor{Storage.Owned{depth, length, original, balanced, valid}, exact},
463 Reduction.owned_sum(shape, depth, length, original, balanced, valid, exact, pair, kept)>>:
464 (value, retained) = pair
465 Fact{Laws.Preserved{other => Equal.cong(Array<F32>, Maybe<&2, F32>,
466 a => Lifecycle.observe_allowed(depth, length, a, other, Nat.is_lt(U32.to_nat(other), length)), retained, original,
467 {\{Reduction.Fact: p => p} : Reduction.Fact<({Pair.snd(F32, Array<F32>, (value, retained)) == original : Array<F32>})> -> {retained == original : Array<F32>}}(kept))}}
468
469
470def tensor_preserved(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>) ->
471 Fact<Laws.Preserved<shape, tensor, Reduction.tensor_sum(shape, fuel, tensor)>>:
472 Core.TTensor{storage, exact} = tensor
473 match storage:
474 case Storage.Empty{}:
475 Fact{Laws.Preserved{other => {==}}}
476 case Storage.Owned{+depth, +length, array, balanced, valid}:
477 owned_preserved(shape, depth, length, array, balanced, valid, exact, Reduction.array_sum(fuel, 0n, 0.0, array),
478 Reduction.array_sum_keeps(depth, array, balanced, fuel, 0n, 0.0, array, {==}))
479
480def owned_status(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original),
481 -valid: {Storage.bounds(depth, length) == True{} : Bool},
482 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
483 pair: F32 & Array<F32>, -kept: Reduction.Fact<{Pair.snd(F32, Array<F32>, pair) == original : Array<F32>}>) ->
484 Totality.Status<Core.Error, Core.Tensor<shape> & F32, Reduction.owned_sum(shape, depth, length, original, balanced, valid, exact, pair, kept)>:
485 (value, retained) = pair
486 Totality.Status{{==}}
487
488
489def tensor_status(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>) ->
490 Totality.Status<Core.Error, Core.Tensor<shape> & F32, Reduction.tensor_sum(shape, fuel, tensor)>:
491 Core.TTensor{storage, exact} = tensor
492 match storage:
493 case Storage.Empty{}:
494 Totality.Status{{==}}
495 case Storage.Owned{+depth, +length, array, balanced, valid}:
496 owned_status(shape, depth, length, array, balanced, valid, exact, Reduction.array_sum(fuel, 0n, 0.0, array),
497 Reduction.array_sum_keeps(depth, array, balanced, fuel, 0n, 0.0, array, {==}))
498
499def Laws.ordered_sum_interpretation(shape, tensor, values, logical):
500 Laws.Interpretation{unit =>
501 Equal.trans(Maybe<&2, F32>, Reduction.sum_observation(shape, Reduction.sum(shape, tensor)),
502 Laws.loop_value(shape, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)),
503 Some{Reduction.sequential_sum(values, 0.0)},
504 sum_result_value(shape, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)),
505 {\{Fact: p => p} : Fact<({Laws.loop_value(shape, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>})> ->
506 {Laws.loop_value(shape, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}}(
507 tensor_value(shape, Shape.elements(shape), tensor, values,
508 %Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape)) :
509 Laws.LogicalValues(_, shape, tensor, 0n, values)
510 logical)))}
511
512def logical_original(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
513 values: List<&2, F32>, logical: Laws.LogicalValues(fuel, shape, tensor, cursor, values),
514 -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
515 Laws.LogicalValues(fuel, shape, original, cursor, values):
516 logical_keeps(fuel, shape, tensor, original, cursor, values, logical,
517 other => Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other), Core.checked_observe(shape, original, other), kept(other)))
518
519def source_extend(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
520 +accumulator: F32, +head: F32, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
521 next: Laws.LoopMeaning(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head), result),
522 -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
523 -observed: {Core.checked_observe(shape, original, U32.from_nat(cursor)) == Some{head} : Maybe<&2, F32>},
524 -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
525 Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, result):
526 match result:
527 case Fail{error}:
528 Unit{}
529 case Done{pair}:
530 (retained, value) = pair
531 Laws.SumMeaning{values, logical, fold} = next
532 Laws.SumMeaning{head <> values,
533 Laws.LogicalStep{exact, observed, logical_original(fuel, shape, original, tensor, 1n+cursor, values, logical, kept)}, fold}
534
535def source_read(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
536 tensor: Core.Tensor<shape>, result: Result<&2, &2, Core.Error, F32>,
537 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.SourceSum<fuel, shape, tensor, 1n+cursor, value,
538 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
539 -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
540 -meaning: {Core.result_value(result) == Core.checked_observe(shape, original, U32.from_nat(cursor)) : Maybe<&2, F32>},
541 -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
542 Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
543 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))>:
544 match result:
545 case Fail{error}:
546 Laws.SourceSum{unit => Unit{}}
547 case Done{+value}:
548 Laws.SourceSum{unit =>
549 claim : @certificate: Laws.SourceSum<fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value),
550 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value))> ->
551 Laws.LoopMeaning(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value),
552 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value))) =
553 \{Laws.SourceSum: proof => proof(Unit{})}
554 source_extend(fuel, shape, original, tensor, cursor, accumulator, value,
555 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)),
556 claim(rec(tensor, F32.add(accumulator, value))), exact,
557 Equal.sym(Maybe<&2, F32>, Some{value}, Core.checked_observe(shape, original, U32.from_nat(cursor)), meaning), kept)}
558
559def source_pair(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
560 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.SourceSum<fuel, shape, tensor, 1n+cursor, value,
561 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
562 -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
563 certificate: Core.Read<shape, original, U32.from_nat(cursor)>,
564 -source: Core.SourceRead<shape, original, U32.from_nat(cursor)>, -retention: Core.SourceReadKeeps<shape, original, U32.from_nat(cursor)>) ->
565 Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
566 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))>:
567 Core.Read{tensor, +result, +exact} = certificate
568 Laws.SourceSum{unit =>
569 claim : @certificate: Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
570 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))> ->
571 Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
572 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))) =
573 \{Laws.SourceSum: proof => proof(Unit{})}
574 prove : @certificates: Core.SourceRead<shape, original, U32.from_nat(cursor)> & Core.SourceReadKeeps<shape, original, U32.from_nat(cursor)> ->
575 Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
576 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))) =
577 \{Tuple: \{Core.SourceRead: meaning => \{Core.SourceReadKeeps: kept =>
578 %exact : Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
579 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, _))
580 claim(source_read(fuel, shape, original, cursor, accumulator, tensor, result, rec, exact_cursor,
581 Equal.trans(Maybe<&2, F32>, Core.result_value(result), Core.read_value(shape, Core.read_flat(shape, original, U32.from_nat(cursor))),
582 Core.checked_observe(shape, original, U32.from_nat(cursor)),
583 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
584 (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), meaning),
585 other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other),
586 Core.retained_read_observe(shape, Core.read_flat(shape, original, U32.from_nat(cursor)), other), Core.checked_observe(shape, original, other),
587 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other),
588 (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), kept(other))))}}}
589 prove((source, retention))}
590
591def source_decision(+fuel: Nat, -shape: Shape.Shape, tensor: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
592 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.SourceSum<fuel, shape, tensor, 1n+cursor, value,
593 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
594 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>) ->
595 Laws.SourceSum<1n+fuel, shape, tensor, cursor, accumulator, Reduction.sum_decided(shape,
596 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), tensor, cursor, U32.from_nat(cursor), accumulator, decision)>:
597 match decision:
598 case Shape.BFalse{equal}:
599 Laws.SourceSum{unit => Unit{}}
600 case Shape.BTrue{equal}:
601 source_pair(fuel, shape, tensor, cursor, accumulator, rec,
602 Lifecycle.natural_equal(U32.to_nat(U32.from_nat(cursor)), cursor, equal),
603 Core.read_certificate(shape, tensor, U32.from_nat(cursor)), Core.source_read_model(shape, tensor, U32.from_nat(cursor)),
604 Core.source_read_keeps(shape, tensor, U32.from_nat(cursor)))
605
606def Laws.successful_loop_interpretation(fuel, shape, tensor, cursor, accumulator):
607 match fuel:
608 case 0n:
609 Laws.SourceSum{unit => Laws.SumMeaning{Nil{}, Unit{}, {==}}}
610 case 1n+tail:
611 source_decision(tail, shape, tensor, cursor, accumulator,
612 tensor => value => Laws.successful_loop_interpretation(tail, shape, tensor, 1n+cursor, value),
613 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)))
614
615def sum_source_result(+shape: Shape.Shape, -original: Core.Tensor<shape>,
616 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
617 -source: Laws.SourceSum<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0, result>,
618 -preservation: Laws.Preserved<shape, original, result>) -> Laws.SourceSumResult<shape, original, Reduction.sum_result(shape, result)>:
619 match result:
620 case Fail{error}:
621 Laws.SourceSumResult{unit => Unit{}}
622 case Done{pair}:
623 (retained, +value) = pair
624 Laws.SourceSumResult{unit =>
625 prove : @certificates: Laws.SourceSum<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0,
626 (Done{(retained, value)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>)> &
627 Laws.Preserved<shape, original, (Done{(retained, value)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>)> ->
628 Laws.SumResultMeaning(shape, original, Reduction.sum_result(shape, Done{(retained, value)})) =
629 \{Tuple: \{Laws.SourceSum: meaning => \{Laws.Preserved: kept =>
630 build : @meaning: Laws.SumMeaning<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0, value> ->
631 Laws.SumResultMeaning(shape, original, Reduction.sum_result(shape, Done{(retained, value)})) =
632 \{Laws.SumMeaning: values => logical => fold =>
633 Laws.SumResult{values, logical,
634 Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, value, Reduction.sequential_sum(values, 0.0), fold), kept}}
635 build(meaning(Unit{}))}}}
636 prove((source, preservation))}
637
638
639
640def tensor_words(+shape: Shape.Shape, tensor: Core.Tensor<shape>) -> Fact<Words<Shape.elements(shape), shape, tensor>>:
641 Fact{{\{Fact: p => p} : Fact<(Words<Shape.elements(shape), shape, tensor>)> -> Words<Shape.elements(shape), shape, tensor>}(words_of(Shape.elements(shape), shape, tensor, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0),
642 {\{Laws.SourceSum: meaning => meaning(Unit{})} :
643 Laws.SourceSum<Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0)> ->
644 Laws.LoopMeaning(Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0))}(
645 Laws.successful_loop_interpretation(Shape.elements(shape), shape, tensor, 0n, 0.0)),
646 sum_loop_status(Shape.elements(shape), shape, tensor, 0n, 0.0,
647 %Equal.sym(Nat, Nat.add(Shape.elements(shape), 0n), Shape.elements(shape), add_zero(Shape.elements(shape))) : Shape.LE(_, Shape.elements(shape))
648 Shape.LE.from(Shape.elements(shape), Shape.elements(shape), Equal.sym(Bool, Nat.is_le(Shape.elements(shape), Shape.elements(shape)), True{}, Conversion.le_reflexive(Shape.elements(shape)))))))}
649
650def Laws.successful_sum_interpretation(shape, tensor):
651 Laws.SourceSumResult{unit =>
652 claim : @certificate: Laws.SourceSumResult<shape, tensor, Reduction.sum(shape, tensor)> ->
653 Laws.SumResultMeaning(shape, tensor, Reduction.sum(shape, tensor)) =
654 \{Laws.SourceSumResult: meaning => meaning(Unit{})}
655 claim(sum_source_result(shape, tensor, Reduction.tensor_sum(shape, Shape.elements(shape), tensor),
656 %Shape.elements_exact(shape) : Laws.SourceSum<_, shape, tensor, 0n, 0.0, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)>
657 {\{Fact: p => p} : Fact<(Laws.SourceSum<Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)>)> ->
658 Laws.SourceSum<Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)>}(
659 tensor_source(shape, Shape.elements(shape), tensor,
660 {\{Fact: p => p} : Fact<(Words<Shape.elements(shape), shape, tensor>)> -> Words<Shape.elements(shape), shape, tensor>}(tensor_words(shape, tensor)))),
661 {\{Fact: p => p} : Fact<(Laws.Preserved<shape, tensor, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)>)> ->
662 Laws.Preserved<shape, tensor, Reduction.tensor_sum(shape, Shape.elements(shape), tensor)>}(
663 tensor_preserved(shape, Shape.elements(shape), tensor))))}
664
665def dynamic_sum_result(+shape: Shape.Shape, -original: Core.Tensor<shape>,
666 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>,
667 -source: Laws.SourceSumResult<shape, original, result>) -> Laws.SourceDynamicSum<Core.Packed{shape, original}, Reduction.pack_result(shape, result)>:
668 match result:
669 case Fail{error}:
670 Laws.SourceDynamicSum{unit => Unit{}}
671 case Done{pair}:
672 (owner, scalar) = pair
673 Laws.SourceDynamicSum{unit =>
674 claim : @source: Laws.SourceSumResult<shape, original,
675 (Done{(owner, scalar)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>)> ->
676 Laws.SumResult<shape, original, owner, scalar> = \{Laws.SourceSumResult: meaning => meaning(Unit{})}
677 Laws.DynamicSumSuccess{shape, original, owner, scalar, {==}, {==}, {==}, claim(source)}}
678
679def Laws.successful_dynamic_sum_interpretation(tensor):
680 Core.Packed{+shape, owner} = tensor
681 dynamic_sum_result(shape, owner, Reduction.sum(shape, owner), Laws.successful_sum_interpretation(shape, owner))
682
683def Laws.empty_accumulation(shape, tensor, index, accumulator):
684 {==}
685
686def empty_tensor_sum(+shape: Shape.Shape, tensor: Core.Tensor<shape>) ->
687 {Reduction.sum_observation(shape, Reduction.sum_result(shape, Reduction.tensor_sum(shape, 0n, tensor))) == Some{0.0} : Maybe<&2, F32>}:
688 Core.TTensor{storage, exact} = tensor
689 match storage:
690 case Storage.Empty{}:
691 {==}
692 case Storage.Owned{+depth, +length, array, balanced, valid}:
693 {==}
694
695def Laws.empty_sum_identity(shape, tensor, empty):
696 match shape:
697 case Shape.SShape{+dimensions, +size, +exact, +rank_bound, +capacity_bound}:
698 %Equal.sym(Nat, size, 0n, Equal.trans(Nat, size, Shape.logical_numel(dimensions), 0n, exact, empty)) :
699 {Reduction.sum_observation(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound},
700 Reduction.sum_result(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound},
701 Reduction.tensor_sum(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound}, _, tensor))) == Some{0.0} : Maybe<&2, F32>}
702 empty_tensor_sum(Shape.SShape{dimensions, size, exact, rank_bound, capacity_bound}, tensor)
703
704def success(-error: Data, -value: Type, result: Result<&2, &1, error, value>,
705 -status: Totality.Status<error, value, result>) -> Totality.Success<error, value, result>:
706 match result:
707 case Fail{failure}:
708 Totality.Success{
709 {\{Totality.Status: successful => Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))} :
710 Totality.Status<error, value, Fail{failure}> -> {False{} == True{} : Bool}}(status),
711 {\{Totality.Status: successful => Empty.absurd(Totality.DoneWitness<error, value, Fail{failure}>, Arith.clash(successful))} :
712 Totality.Status<error, value, Fail{failure}> -> Totality.DoneWitness<error, value, Fail{failure}>}(status)}
713 case Done{returned}:
714 Totality.Success{{==}, Totality.DoneWitness{returned, {==}}}
715
716def add_zero(+value: Nat) -> {Nat.add(value, 0n) == value : Nat}:
717 match value:
718 case 0n:
719 {==}
720 case 1n+p:
721 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero(p))
722
723def add_comm(+a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}:
724 match a:
725 case 0n:
726 Equal.sym(Nat, Nat.add(b, 0n), b, add_zero(b))
727 case 1n+p:
728 Equal.trans(Nat, 1n+Nat.add(p, b), 1n+Nat.add(b, p), Nat.add(b, 1n+p),
729 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, b), Nat.add(b, p), add_comm(p, b)),
730 Equal.sym(Nat, Nat.add(b, 1n+p), 1n+Nat.add(b, p), Arith.add_succ(b, p)))
731
732def cursor_bounds(+fuel: Nat, +cursor: Nat, +limit: Nat,
733 bound: Shape.LE(Nat.add(1n+fuel, cursor), limit)) -> {Nat.is_lt(cursor, limit) == True{} : Bool}:
734 Conversion.le_successor_lt(cursor, limit,
735 Equal.sym(Bool, True{}, Nat.is_le(1n+cursor, limit),
736 Nats.le_true(1n+cursor, limit,
737 Nats.le_add_left(1n+cursor, fuel, limit,
738 %add_comm(fuel, cursor) : Shape.LE(1n+_, limit)
739 bound))))
740
741def cursor_exact(+fuel: Nat, +shape: Shape.Shape, +cursor: Nat,
742 bound: Shape.LE(Nat.add(1n+fuel, cursor), Shape.elements(shape))) -> {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
743 Conversion.natural_word_exact(cursor, Shape.count(shape),
744 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape)) : {Nat.is_le(cursor, _) == True{} : Bool}
745 Conversion.le_predecessor(cursor, Shape.elements(shape),
746 Equal.sym(Bool, True{}, Nat.is_le(1n+cursor, Shape.elements(shape)),
747 Nats.le_true(1n+cursor, Shape.elements(shape),
748 Nats.le_add_left(1n+cursor, fuel, Shape.elements(shape),
749 %add_comm(fuel, cursor) : Shape.LE(1n+_, Shape.elements(shape))
750 bound)))))
751
752def sum_read_status(+fuel: Nat, +shape: Shape.Shape, +cursor: Nat, +accumulator: F32,
753 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>,
754 -successful: {TransformTotality.read_succeeded(shape, pair) == True{} : Bool},
755 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Totality.Status<Core.Error, Core.Tensor<shape> & F32,
756 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>) ->
757 Totality.Status<Core.Error, Core.Tensor<shape> & F32, Reduction.read_step(shape,
758 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, pair)>:
759 (tensor, result) = pair
760 match result:
761 case Fail{error}:
762 Totality.Status{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
763 case Done{+value}:
764 Totality.Status{{\{Totality.Status: successful => successful} :
765 Totality.Status<Core.Error, Core.Tensor<shape> & F32,
766 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value))> ->
767 {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape> & F32,
768 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value))) == True{} : Bool}}(
769 rec(tensor, F32.add(accumulator, value)))}
770
771def sum_decision_status(+fuel: Nat, +shape: Shape.Shape, +cursor: Nat, +accumulator: F32,
772 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)>,
773 tensor: Core.Tensor<shape>,
774 -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
775 -inside: {Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
776 -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Totality.Status<Core.Error, Core.Tensor<shape> & F32,
777 Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>) ->
778 Totality.Status<Core.Error, Core.Tensor<shape> & F32, Reduction.sum_decided(shape,
779 tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), tensor, cursor, U32.from_nat(cursor), accumulator, decision)>:
780 match decision:
781 case Shape.BFalse{equal}:
782 Totality.Status{Empty.absurd({False{} == True{} : Bool}, conversion_clash(U32.to_nat(U32.from_nat(cursor)), cursor, exact, equal))}
783 case Shape.BTrue{equal}:
784 sum_read_status(fuel, shape, cursor, accumulator, Core.read_flat(shape, tensor, U32.from_nat(cursor)),
785 {\{TransformTotality.ReadSuccess: successful => successful} :
786 TransformTotality.ReadSuccess<shape, tensor, U32.from_nat(cursor)> ->
787 {TransformTotality.read_succeeded(shape, Core.read_flat(shape, tensor, U32.from_nat(cursor))) == True{} : Bool}}(
788 TransformLaws.tensor_read_valid_success(shape, tensor, U32.from_nat(cursor), inside)), rec)
789
790def sum_loop_status(fuel: Nat, +shape: Shape.Shape, tensor: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
791 -bound: Shape.LE(Nat.add(fuel, cursor), Shape.elements(shape))) ->
792 Totality.Status<Core.Error, Core.Tensor<shape> & F32, Reduction.natural_sum_loop(fuel, shape, tensor, cursor, accumulator)>:
793 match fuel:
794 case 0n:
795 Totality.Status{{==}}
796 case 1n+tail:
797 sum_decision_status(tail, shape, cursor, accumulator,
798 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)),
799 tensor,
800 cursor_exact(tail, shape, cursor, bound),
801 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_exact(tail, shape, cursor, bound)) : {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
802 %Shape.elements_exact(shape) : {Nat.is_lt(cursor, _) == True{} : Bool}
803 cursor_bounds(tail, cursor, Shape.elements(shape), bound),
804 tensor => value => sum_loop_status(tail, shape, tensor, 1n+cursor, value,
805 %Equal.sym(Nat, Nat.add(tail, 1n+cursor), 1n+Nat.add(tail, cursor), Arith.add_succ(tail, cursor)) : Shape.LE(_, Shape.elements(shape))
806 bound))
807
808def sum_allocated_status(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +value: F32) ->
809 Totality.Status<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Reduction.scalar_result(shape, tensor, Core.new(Reduction.scalar_shape(), value))>:
810 Totality.Status{
811 {\{Allocation.TensorDone: scalar => same =>
812 %same : {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Reduction.scalar_result(shape, tensor, _)) == True{} : Bool}
813 {==}} : Allocation.TensorDone<Reduction.scalar_shape(), Core.new(Reduction.scalar_shape(), value)> ->
814 {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Reduction.scalar_result(shape, tensor, Core.new(Reduction.scalar_shape(), value))) == True{} : Bool}}(
815 AllocationProof.core_new_done(Reduction.scalar_shape(), value))}
816
817def sum_result_status(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
818 -status: Totality.Status<Core.Error, Core.Tensor<shape> & F32, result>) ->
819 Totality.Status<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Reduction.sum_result(shape, result)>:
820 match result:
821 case Fail{error}:
822 Totality.Status{{\{Totality.Status: successful => Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))} :
823 Totality.Status<Core.Error, Core.Tensor<shape> & F32, Fail{error}> -> {False{} == True{} : Bool}}(status)}
824 case Done{pair}:
825 (tensor, +value) = pair
826 sum_allocated_status(shape, tensor, value)
827
828def Laws.sum_valid_success(shape, tensor):
829 success(Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Reduction.sum(shape, tensor),
830 sum_result_status(shape, Reduction.tensor_sum(shape, Shape.elements(shape), tensor),
831 tensor_status(shape, Shape.elements(shape), tensor)))
832
833def sum_packed_status(+shape: Shape.Shape,
834 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>,
835 -certificate: Totality.Success<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, result>) ->
836 Totality.Status<Core.Error, Core.Dynamic & Core.Dynamic, Reduction.pack_result(shape, result)>:
837 match result:
838 case Fail{error}:
839 Totality.Status{{\{Totality.Success: successful => witness => Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))} :
840 Totality.Success<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Fail{error}> -> {False{} == True{} : Bool}}(certificate)}
841 case Done{pair}:
842 (tensor, scalar) = pair
843 Totality.Status{{==}}
844
845def Laws.sum_dynamic_valid_success(tensor):
846 Core.Packed{+shape, owner} = tensor
847 success(Core.Error, Core.Dynamic & Core.Dynamic, Reduction.pack_result(shape, Reduction.sum(shape, owner)),
848 sum_packed_status(shape, Reduction.sum(shape, owner), Laws.sum_valid_success(shape, owner)))
849
850def Laws.sum_valid_result(shape, tensor):
851 Laws.TotalSum{Laws.sum_valid_success(shape, tensor), Laws.successful_sum_interpretation(shape, tensor)}
852
853def Laws.sum_dynamic_valid_result(tensor):
854 Laws.TotalDynamicSum{Laws.sum_dynamic_valid_success(tensor), Laws.successful_dynamic_sum_interpretation(tensor)}