src/tensor/construction_PROOF.bend
bendtorch-core@0.1.0.0 · 708 lines · 52 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/clone.bend as Clone
7import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
8import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
9import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
10import bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend as Laws
11import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof
12import bendtorch-core@0.1.0.0/src/tensor/word_injective.bend as Injective
13import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
14import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
15import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
16import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
17import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
18import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
19import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
20import bendtorch-core@0.1.0.0/src/tensor/transform_LAWS.bend as TransformLaws
21import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
22import bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend as Totality
23
24def clone_first_checked_view(-shape: Shape.Shape, -original: Storage.Storage,
25 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
26 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
27 {Laws.clone_first_checked(shape, Core.clone_result(shape, original, valid, pair, same), index) ==
28 Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, pair), index) : Maybe<&2, F32>}:
29 (first, second) = pair
30 {==}
31
32def clone_second_checked_view(-shape: Shape.Shape, -original: Storage.Storage,
33 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
34 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
35 {Laws.clone_second_checked(shape, Core.clone_result(shape, original, valid, pair, same), index) ==
36 Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, pair), index) : Maybe<&2, F32>}:
37 (first, second) = pair
38 {==}
39
40def clone_first_model_view(-shape: Shape.Shape, -original: Storage.Storage,
41 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
42 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
43 {Laws.clone_first_model(shape, Core.clone_result(shape, original, valid, pair, same), index) ==
44 Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, pair), index) : Maybe<&2, F32>}:
45 (first, second) = pair
46 {==}
47
48def clone_second_model_view(-shape: Shape.Shape, -original: Storage.Storage,
49 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
50 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
51 {Laws.clone_second_model(shape, Core.clone_result(shape, original, valid, pair, same), index) ==
52 Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, pair), index) : Maybe<&2, F32>}:
53 (first, second) = pair
54 {==}
55
56def storage_clone_first_checked_view(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
57 pair: Array<F32> & Array<F32>, -exact: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>},
58 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
59 {Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.finish_clone(depth, length, array, pair, exact, balanced, valid)), index) ==
60 Lifecycle.checked_observe_array(depth, length, Pair.fst(Array<F32>, Array<F32>, pair), index) : Maybe<&2, F32>}:
61 (first, second) = pair
62 {==}
63
64def storage_clone_second_checked_view(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
65 pair: Array<F32> & Array<F32>, -exact: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>},
66 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
67 {Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.finish_clone(depth, length, array, pair, exact, balanced, valid)), index) ==
68 Lifecycle.checked_observe_array(depth, length, Pair.snd(Array<F32>, Array<F32>, pair), index) : Maybe<&2, F32>}:
69 (first, second) = pair
70 {==}
71
72def storage_clone_first_model_view(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
73 pair: Array<F32> & Array<F32>, -exact: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>},
74 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
75 {Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.finish_clone(depth, length, array, pair, exact, balanced, valid)), index) ==
76 Model.observe(F32, depth, Pair.fst(Array<F32>, Array<F32>, pair), Refinement.route(depth, index)) : Maybe<&2, F32>}:
77 (first, second) = pair
78 {==}
79
80def storage_clone_second_model_view(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32,
81 pair: Array<F32> & Array<F32>, -exact: {pair == Array.clone(F32, array) : Array<F32> & Array<F32>},
82 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}) ->
83 {Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.finish_clone(depth, length, array, pair, exact, balanced, valid)), index) ==
84 Model.observe(F32, depth, Pair.snd(Array<F32>, Array<F32>, pair), Refinement.route(depth, index)) : Maybe<&2, F32>}:
85 (first, second) = pair
86 {==}
87
88def clone_owned_meaning(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>,
89 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
90 -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
91 Laws.CloneMeaning<shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}>:
92 Laws.CloneMeaning{
93 index => Equal.trans(Maybe<&2, F32>,
94 Laws.clone_first_checked(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
95 Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
96 Lifecycle.checked_observe_array(depth, length, array, index),
97 clone_first_checked_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
98 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
99 Equal.trans(Maybe<&2, F32>,
100 Lifecycle.checked_observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
101 Lifecycle.checked_observe_array(depth, length, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), index),
102 Lifecycle.checked_observe_array(depth, length, array, index),
103 storage_clone_first_checked_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
104 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Lifecycle.checked_observe_array(depth, length, a, index),
105 Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))),
106 index => Equal.trans(Maybe<&2, F32>,
107 Laws.clone_second_checked(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
108 Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
109 Lifecycle.checked_observe_array(depth, length, array, index),
110 clone_second_checked_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
111 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
112 Equal.trans(Maybe<&2, F32>,
113 Lifecycle.checked_observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
114 Lifecycle.checked_observe_array(depth, length, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), index),
115 Lifecycle.checked_observe_array(depth, length, array, index),
116 storage_clone_second_checked_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
117 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Lifecycle.checked_observe_array(depth, length, a, index),
118 Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))),
119 index => Equal.trans(Maybe<&2, F32>,
120 Laws.clone_first_model(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
121 Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
122 Model.observe(F32, depth, array, Refinement.route(depth, index)),
123 clone_first_model_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
124 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
125 Equal.trans(Maybe<&2, F32>,
126 Lifecycle.observe(Pair.fst(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
127 Model.observe(F32, depth, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), Refinement.route(depth, index)),
128 Model.observe(F32, depth, array, Refinement.route(depth, index)),
129 storage_clone_first_model_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
130 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)),
131 Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced))))),
132 index => Equal.trans(Maybe<&2, F32>,
133 Laws.clone_second_model(shape, Core.clone(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}), index),
134 Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
135 Model.observe(F32, depth, array, Refinement.route(depth, index)),
136 clone_second_model_view(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index,
137 Storage.clone(Storage.Owned{depth, length, array, balanced, valid}), {==}),
138 Equal.trans(Maybe<&2, F32>,
139 Lifecycle.observe(Pair.snd(Storage.Storage, Storage.Storage, Storage.clone(Storage.Owned{depth, length, array, balanced, valid})), index),
140 Model.observe(F32, depth, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), Refinement.route(depth, index)),
141 Model.observe(F32, depth, array, Refinement.route(depth, index)),
142 storage_clone_second_model_view(depth, length, array, index, Array.clone(F32, array), {==}, balanced, valid),
143 Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)),
144 Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), array, Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced)))))}
145
146def clone_meaning(-shape: Shape.Shape, original: Core.Tensor<shape>) -> Laws.CloneMeaning<shape, original>:
147 Core.TTensor{storage, length_exact} = original
148 match storage:
149 case Storage.Empty{}:
150 Laws.CloneMeaning{index => {==}, index => {==}, index => {==}, index => {==}}
151 case Storage.Owned{+depth, +length, array, balanced, valid}:
152 clone_owned_meaning(shape, depth, length, array, balanced, valid, length_exact)
153
154def Laws.public_clone_elements(shape, original):
155 clone_meaning(shape, original)
156
157def FillElements(-shape: Shape.Shape, +values: List<&2, F32>, +cursor: Nat, -tensor: Core.Tensor<shape>) -> Type:
158 @+index: U32 -> @+offset: Nat -> @at: {U32.to_nat(index) == Nat.add(cursor, offset) : Nat} ->
159 @inside: Shape.LT(offset, List.length(&2, F32, values)) ->
160 Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
161 {Core.checked_observe(shape, tensor, index) == Laws.list_element(values, offset) : Maybe<&2, F32>}
162
163def FillFrame(-shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, -tensor: Core.Tensor<shape>) -> Type:
164 @+index: U32 -> @earlier: Shape.LT(U32.to_nat(index), cursor) ->
165 @checked: Core.ObservationChecked(Core.Packed{shape, original}, index) ->
166 Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
167 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}
168
169def FillMeaning(-shape: Shape.Shape, -original: Core.Tensor<shape>, +values: List<&2, F32>, +cursor: Nat,
170 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) -> Type:
171 match result:
172 case Fail{error}:
173 Unit
174 case Done{tensor}:
175 FillElements(shape, values, cursor, tensor) & FillFrame(shape, original, cursor, tensor)
176
177type FillOutcome<-shape: Shape.Shape, -original: Core.Tensor<shape>, -values: List<&2, F32>, -cursor: Nat,
178 -result: Result<&2, &1, Core.Error, Core.Tensor<shape>>> is Data:
179 FillOutcome{-meaning: FillMeaning(shape, original, values, cursor, result)}
180
181type Written<-shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, -cursor: Nat, -value: F32> is Data:
182 Written{-point: @+index: U32 -> @at: {U32.to_nat(index) == cursor : Nat} ->
183 Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
184 {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>},
185 -frame: FillFrame(shape, original, cursor, tensor)}
186
187def lt_zero(+number: Nat, proof: Shape.LT(number, 0n)) -> Empty:
188 match number:
189 case 0n:
190 proof
191 case 1n+p:
192 proof
193
194def lt_self_successor(number: Nat) -> Shape.LT(number, 1n+number):
195 match number:
196 case 0n:
197 Unit{}
198 case 1n+p:
199 lt_self_successor(p)
200
201def lt_extend(+number: Nat, +bound: Nat, proof: Shape.LT(number, bound)) -> Shape.LT(number, 1n+bound):
202 match number bound:
203 case 0n 0n:
204 match proof:
205 case 0n 1n+p:
206 Unit{}
207 case 1n+p 0n:
208 match proof:
209 case 1n+p 1n+q:
210 lt_extend(p, q, proof)
211
212def add_zero_right(number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
213 match number:
214 case 0n:
215 {==}
216 case 1n+p:
217 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero_right(p))
218
219def fill_head(-shape: Shape.Shape, -written: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat, +value: F32,
220 point: @+index: U32 -> @at: {U32.to_nat(index) == cursor : Nat} ->
221 Core.ObservationChecked(Core.Packed{shape, written}, index) &
222 {Core.checked_observe(shape, written, index) == Some{value} : Maybe<&2, F32>},
223 frame: FillFrame(shape, written, 1n+cursor, tensor), +index: U32, +at: {U32.to_nat(index) == cursor : Nat}) ->
224 Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
225 {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>}:
226 {\{Tuple: checked => observed =>
227 {\{Tuple: after_checked => retained =>
228 (after_checked, Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, index), Core.checked_observe(shape, written, index),
229 Some{value}, retained, observed))} :
230 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
231 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, written, index) : Maybe<&2, F32>}) ->
232 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
233 {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>})}(frame(index)(
234 %Equal.sym(Nat, U32.to_nat(index), cursor, at) : Shape.LT(_, 1n+cursor)
235 lt_self_successor(cursor))(checked))
236 } :
237 (Core.ObservationChecked(Core.Packed{shape, written}, index) &
238 {Core.checked_observe(shape, written, index) == Some{value} : Maybe<&2, F32>}) ->
239 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
240 {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>})}(point(index)(at))
241
242def fill_elements_advance(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat,
243 -written: Core.Tensor<shape>, -tensor: Core.Tensor<shape>,
244 point: @+index: U32 -> @at: {U32.to_nat(index) == cursor : Nat} ->
245 Core.ObservationChecked(Core.Packed{shape, written}, index) &
246 {Core.checked_observe(shape, written, index) == Some{value} : Maybe<&2, F32>},
247 mapping: FillElements(shape, rest, 1n+cursor, tensor), frame: FillFrame(shape, written, 1n+cursor, tensor),
248 +index: U32, +offset: Nat, at: {U32.to_nat(index) == Nat.add(cursor, offset) : Nat},
249 inside: Shape.LT(offset, List.length(&2, F32, value <> rest))) ->
250 Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
251 {Core.checked_observe(shape, tensor, index) == Laws.list_element(value <> rest, offset) : Maybe<&2, F32>}:
252 match offset:
253 case 0n:
254 fill_head(shape, written, tensor, cursor, value, point, frame, index,
255 Equal.trans(Nat, U32.to_nat(index), Nat.add(cursor, 0n), cursor, at, add_zero_right(cursor)))
256 case 1n+p:
257 mapping(index)(p)(Equal.trans(Nat, U32.to_nat(index), Nat.add(cursor, 1n+p), Nat.add(1n+cursor, p), at, Arith.add_succ(cursor, p)))(inside)
258
259def fill_frame_advance(-shape: Shape.Shape, -original: Core.Tensor<shape>, -written: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
260 before: FillFrame(shape, original, cursor, written), after: FillFrame(shape, written, 1n+cursor, tensor),
261 +index: U32, +earlier: Shape.LT(U32.to_nat(index), cursor), checked: Core.ObservationChecked(Core.Packed{shape, original}, index)) ->
262 Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
263 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}:
264 {\{Tuple: middle_checked => middle_equal =>
265 {\{Tuple: after_checked => after_equal =>
266 (after_checked, Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, index), Core.checked_observe(shape, written, index),
267 Core.checked_observe(shape, original, index), after_equal, middle_equal))} :
268 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
269 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, written, index) : Maybe<&2, F32>}) ->
270 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
271 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(after(index)(lt_extend(U32.to_nat(index), cursor, earlier))(middle_checked))
272 } :
273 (Core.ObservationChecked(Core.Packed{shape, written}, index) &
274 {Core.checked_observe(shape, written, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}) ->
275 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
276 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(before(index)(earlier)(checked))
277
278def fill_advance(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat,
279 -original: Core.Tensor<shape>, -written: Core.Tensor<shape>,
280 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, -point: Written<shape, original, written, cursor, value>,
281 -next: FillMeaning(shape, written, rest, 1n+cursor, result)) -> FillOutcome<shape, original, value <> rest, cursor, result>:
282 match result:
283 case Fail{error}:
284 FillOutcome{Unit{}}
285 case Done{tensor}:
286 FillOutcome{
287 (index => offset => at => inside =>
288 {\{Written: observed => before =>
289 {\{Tuple: mapping => after => fill_elements_advance(shape, value, rest, cursor, written, tensor,
290 observed, mapping, after, index, offset, at, inside)} :
291 (FillElements(shape, rest, 1n+cursor, tensor) & FillFrame(shape, written, 1n+cursor, tensor)) ->
292 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
293 {Core.checked_observe(shape, tensor, index) == Laws.list_element(value <> rest, offset) : Maybe<&2, F32>})}(next)
294 } : Written<shape, original, written, cursor, value> ->
295 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
296 {Core.checked_observe(shape, tensor, index) == Laws.list_element(value <> rest, offset) : Maybe<&2, F32>})}(point),
297 index => earlier => checked =>
298 {\{Written: observed => before =>
299 {\{Tuple: mapping => after => fill_frame_advance(shape, original, written, tensor, cursor, before, after, index, earlier, checked)} :
300 (FillElements(shape, rest, 1n+cursor, tensor) & FillFrame(shape, written, 1n+cursor, tensor)) ->
301 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
302 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(next)
303 } : Written<shape, original, written, cursor, value> ->
304 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
305 {Core.checked_observe(shape, tensor, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>})}(point))}
306
307type ElementPoint<-shape: Shape.Shape, -values: List<&2, F32>, -tensor: Core.Tensor<shape>, -index: U32> is Data:
308 ElementPoint{-meaning: Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
309 ({Core.checked_observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>} &
310 {Core.observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>})}
311
312def element_point(-shape: Shape.Shape, +values: List<&2, F32>, -tensor: Core.Tensor<shape>, +index: U32,
313 -checked: Core.ObservationChecked(Core.Packed{shape, tensor}, index),
314 -observed: {Core.checked_observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>}) ->
315 ElementPoint<shape, values, tensor, index>:
316 ElementPoint{(checked, (observed,
317 {\{Core.ObservationModel: same =>
318 Equal.trans(Maybe<&2, F32>, Core.observe(shape, tensor, index), Core.checked_observe(shape, tensor, index), Laws.list_element(values, U32.to_nat(index)),
319 Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, tensor, index), Core.observe(shape, tensor, index), same), observed)
320 } : Core.ObservationModel<shape, tensor, index, checked> ->
321 {Core.observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>}}(Core.observation_model(shape, tensor, index, checked))))}
322
323type ElementsOutcome<-shape: Shape.Shape, -values: List<&2, F32>, -result: Result<&2, &1, Core.Error, Core.Tensor<shape>>> is Data:
324 ElementsOutcome{-meaning: Laws.FromValuesMeaning(shape, values, result)}
325
326def complete_fill(-shape: Shape.Shape, +values: List<&2, F32>, -original: Core.Tensor<shape>,
327 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
328 -count: {Shape.logical_numel(Shape.dimensions(shape)) == List.length(&2, F32, values) : Nat},
329 -fill: FillMeaning(shape, original, values, 0n, result)) -> ElementsOutcome<shape, values, result>:
330 match result:
331 case Fail{error}:
332 ElementsOutcome{Unit{}}
333 case Done{tensor}:
334 ElementsOutcome{index => inside =>
335 {\{Tuple: mapping => frame =>
336 {\{Tuple: checked => observed =>
337 {\{ElementPoint: meaning => meaning} : ElementPoint<shape, values, tensor, index> ->
338 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
339 ({Core.checked_observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>} &
340 {Core.observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>}))}(element_point(shape, values, tensor, index, checked, observed))
341 } :
342 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
343 {Core.checked_observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>}) ->
344 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
345 ({Core.checked_observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>} &
346 {Core.observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>}))}(mapping(index)(U32.to_nat(index))({==})(
347 %count : Shape.LT(U32.to_nat(index), _)
348 inside))
349 } : (FillElements(shape, values, 0n, tensor) & FillFrame(shape, original, 0n, tensor)) ->
350 (Core.ObservationChecked(Core.Packed{shape, tensor}, index) &
351 ({Core.checked_observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>} &
352 {Core.observe(shape, tensor, index) == Laws.list_element(values, U32.to_nat(index)) : Maybe<&2, F32>}))}(fill)}
353
354type ConstructionOutcome<-values: List<&2, F32>, -result: Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
355 ConstructionOutcome{-meaning: Laws.ConstructionMeaning(values, result)}
356
357def construction_values_elements(+shape: Shape.Shape, +values: List<&2, F32>,
358 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, -meaning: Laws.FromValuesMeaning(shape, values, result)) ->
359 ConstructionOutcome<values, Core.construct_values(shape, result)>:
360 match result:
361 case Fail{error}:
362 ConstructionOutcome{Unit{}}
363 case Done{tensor}:
364 ConstructionOutcome{meaning}
365
366def construction_shape_elements(+dimensions: List<&2, U32>, +values: List<&2, F32>, result: Shape.ConstructResult<dimensions>) ->
367 ConstructionOutcome<values, Core.construct_shape(dimensions, values, result)>:
368 match result:
369 case Shape.SError{error}:
370 ConstructionOutcome{Unit{}}
371 case Shape.SBuilt{+shape, preserved}:
372 ConstructionOutcome{
373 {\{ConstructionOutcome: meaning => meaning} : ConstructionOutcome<values, Core.construct_values(shape, Core.from_values(shape, values))> ->
374 Laws.ConstructionMeaning(values, Core.construct_values(shape, Core.from_values(shape, values)))}(construction_values_elements(shape, values, Core.from_values(shape, values),
375 {\{Laws.FromValuesModel: meaning => meaning} : Laws.FromValuesModel<shape, values> ->
376 Laws.FromValuesMeaning(shape, values, Core.from_values(shape, values))}(Laws.public_from_values_elements(shape, values))))}
377
378def Laws.public_construction_elements(dimensions, values):
379 Laws.ConstructionModel{
380 {\{ConstructionOutcome: meaning => meaning} : ConstructionOutcome<values, Core.construct(dimensions, values)> ->
381 Laws.ConstructionMeaning(values, Core.construct(dimensions, values))}(construction_shape_elements(dimensions, values, Shape.construct(dimensions)))}
382
383def supplied_count(+shape: Shape.Shape, +values: List<&2, F32>,
384 decided: {True{} == Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape)) : Bool}) ->
385 {Shape.logical_numel(Shape.dimensions(shape)) == List.length(&2, F32, values) : Nat}:
386 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape), List.length(&2, F32, values),
387 Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape)),
388 Equal.sym(Nat, List.length(&2, F32, values), Shape.elements(shape),
389 Lifecycle.natural_equal(List.length(&2, F32, values), Shape.elements(shape), decided)))
390
391def written_point(-shape: Shape.Shape, -tensor: Core.Tensor<shape>, +cursor: Nat, +index: U32, +value: F32,
392 converted: {U32.to_nat(index) == cursor : Nat}, checked: Core.ObservationChecked(Core.Packed{shape, tensor}, index),
393 observed: {Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>}, +other: U32,
394 at: {U32.to_nat(other) == cursor : Nat}) ->
395 Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
396 {Core.checked_observe(shape, tensor, other) == Some{value} : Maybe<&2, F32>}:
397 %Injective.u32_natural_injective(index, other)(Equal.trans(Nat, U32.to_nat(index), cursor, U32.to_nat(other), converted,
398 Equal.sym(Nat, U32.to_nat(other), cursor, at))) :
399 Core.ObservationChecked(Core.Packed{shape, tensor}, _) &
400 {Core.checked_observe(shape, tensor, _) == Some{value} : Maybe<&2, F32>}
401 (checked, observed)
402
403def written_model(-shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
404 +index: U32, +value: F32, -unit: Unit, -converted: {U32.to_nat(index) == cursor : Nat},
405 -meaning: Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit}))) -> Written<shape, original, tensor, cursor, value>:
406 Written{
407 other => at =>
408 {\{Tuple: checked => rest =>
409 {\{Tuple: observed => frame => written_point(shape, tensor, cursor, index, value, converted, checked, observed, other, at)} :
410 ({Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
411 (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
412 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
413 Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
414 {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})) ->
415 (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
416 {Core.checked_observe(shape, tensor, other) == Some{value} : Maybe<&2, F32>})}(rest)
417 } : Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit})) ->
418 (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
419 {Core.checked_observe(shape, tensor, other) == Some{value} : Maybe<&2, F32>})}(meaning),
420 other => earlier => before_checked =>
421 {\{Tuple: checked => rest =>
422 {\{Tuple: observed => frame => frame(other)(before_checked)(
423 %Equal.sym(Nat, U32.to_nat(index), cursor, converted) : {Nat.is_eq(_, U32.to_nat(other)) == False{} : Bool}
424 CoreProof.lt_big_small_different(U32.to_nat(other), cursor, earlier))} :
425 ({Core.checked_observe(shape, tensor, index) == Some{value} : Maybe<&2, F32>} &
426 (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
427 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
428 Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
429 {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})) ->
430 (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
431 {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(rest)
432 } : Core.CheckedUpdateMeaning(shape, original, index, value, (tensor, Done{unit})) ->
433 (Core.ObservationChecked(Core.Packed{shape, tensor}, other) &
434 {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(meaning)}
435
436def fill_write_pair(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +index: U32,
437 -original: Core.Tensor<shape>, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
438 -same: {pair == Core.write_flat(shape, original, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
439 -converted: {U32.to_nat(index) == cursor : Nat}, -model: Core.CheckedUpdateModel<shape, original, index, value>,
440 -rec: @tensor: Core.Tensor<shape> -> FillOutcome<shape, tensor, rest, 1n+cursor, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
441 FillOutcome<shape, original, value <> rest, cursor,
442 Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), pair)>:
443 (tensor, result) = pair
444 match result:
445 case Fail{error}:
446 FillOutcome{Unit{}}
447 case Done{unit}:
448 FillOutcome{
449 {\{FillOutcome: meaning => meaning} : FillOutcome<shape, original, value <> rest, cursor, Core.fill_values(rest, shape, tensor, 1n+cursor)> ->
450 FillMeaning(shape, original, value <> rest, cursor, Core.fill_values(rest, shape, tensor, 1n+cursor))}(fill_advance(shape, value, rest, cursor,
451 original, tensor, Core.fill_values(rest, shape, tensor, 1n+cursor),
452 written_model(shape, original, tensor, cursor, index, value, unit, converted,
453 %Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (tensor, Done{unit}), Core.write_flat(shape, original, index, value), same) :
454 Core.CheckedUpdateMeaning(shape, original, index, value, _)
455 {\{Core.CheckedUpdateModel: meaning => meaning} : Core.CheckedUpdateModel<shape, original, index, value> ->
456 Core.CheckedUpdateMeaning(shape, original, index, value, Core.write_flat(shape, original, index, value))}(model)),
457 {\{FillOutcome: meaning => meaning} : FillOutcome<shape, tensor, rest, 1n+cursor, Core.fill_values(rest, shape, tensor, 1n+cursor)> ->
458 FillMeaning(shape, tensor, rest, 1n+cursor, Core.fill_values(rest, shape, tensor, 1n+cursor))}(rec(tensor))))}
459
460def fill_decision_model(-shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +index: U32,
461 -original: Core.Tensor<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
462 -rec: @tensor: Core.Tensor<shape> -> FillOutcome<shape, tensor, rest, 1n+cursor, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
463 FillOutcome<shape, original, value <> rest, cursor, Core.fill_values_decided(shape, cursor, index, value, original,
464 tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), decision)>:
465 match decision:
466 case Shape.BFalse{equal}:
467 FillOutcome{Unit{}}
468 case Shape.BTrue{equal}:
469 FillOutcome{
470 {\{FillOutcome: meaning => meaning} :
471 FillOutcome<shape, original, value <> rest, cursor,
472 Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Core.write_flat(shape, original, index, value))> ->
473 FillMeaning(shape, original, value <> rest, cursor,
474 Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Core.write_flat(shape, original, index, value)))}(fill_write_pair(shape, value, rest, cursor, index, original, Core.write_flat(shape, original, index, value), {==},
475 Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), CoreProof.checked_update_model(shape, original, index, value), rec))}
476
477def fill_model(+values: List<&2, F32>, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat) ->
478 FillOutcome<shape, original, values, cursor, Core.fill_values(values, shape, original, cursor)>:
479 match values:
480 case Nil{}:
481 FillOutcome{(index => offset => at => inside =>
482 Empty.absurd(Core.ObservationChecked(Core.Packed{shape, original}, index) &
483 {Core.checked_observe(shape, original, index) == Laws.list_element(Nil{}, offset) : Maybe<&2, F32>}, lt_zero(offset, inside)),
484 index => earlier => checked => (checked, {==}))}
485 case +value <> +rest:
486 FillOutcome{
487 {\{FillOutcome: meaning => meaning} :
488 FillOutcome<shape, original, value <> rest, cursor,
489 Core.fill_values_decided(shape, cursor, U32.from_nat(cursor), value, original,
490 tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)))> ->
491 FillMeaning(shape, original, value <> rest, cursor, Core.fill_values(value <> rest, shape, original, cursor))}(fill_decision_model(shape, value, rest,
492 cursor, U32.from_nat(cursor), original, Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)),
493 tensor => fill_model(rest, shape, tensor, 1n+cursor)))}
494
495def from_values_new_elements(-shape: Shape.Shape, +values: List<&2, F32>,
496 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
497 -count: {Shape.logical_numel(Shape.dimensions(shape)) == List.length(&2, F32, values) : Nat}) ->
498 ElementsOutcome<shape, values, Core.from_values_new(shape, values, result)>:
499 match result:
500 case Fail{error}:
501 ElementsOutcome{Unit{}}
502 case Done{tensor}:
503 ElementsOutcome{
504 {\{ElementsOutcome: meaning => meaning} : ElementsOutcome<shape, values, Core.fill_values(values, shape, tensor, 0n)> ->
505 Laws.FromValuesMeaning(shape, values, Core.fill_values(values, shape, tensor, 0n))}(complete_fill(shape, values, tensor,
506 Core.fill_values(values, shape, tensor, 0n), count,
507 {\{FillOutcome: meaning => meaning} : FillOutcome<shape, tensor, values, 0n, Core.fill_values(values, shape, tensor, 0n)> ->
508 FillMeaning(shape, tensor, values, 0n, Core.fill_values(values, shape, tensor, 0n))}(fill_model(values, shape, tensor, 0n))))}
509
510def from_values_counted_elements(+shape: Shape.Shape, +values: List<&2, F32>,
511 decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>) ->
512 ElementsOutcome<shape, values, Core.from_values_counted(shape, values, decision)>:
513 match decision:
514 case Shape.BFalse{equal}:
515 ElementsOutcome{Unit{}}
516 case Shape.BTrue{equal}:
517 ElementsOutcome{
518 {\{ElementsOutcome: meaning => meaning} : ElementsOutcome<shape, values, Core.from_values_new(shape, values, Core.new(shape, 0.0))> ->
519 Laws.FromValuesMeaning(shape, values, Core.from_values_new(shape, values, Core.new(shape, 0.0)))}(from_values_new_elements(shape, values, Core.new(shape, 0.0), supplied_count(shape, values, equal)))}
520
521def Laws.public_from_values_elements(shape, values):
522 Laws.FromValuesModel{
523 {\{ElementsOutcome: meaning => meaning} : ElementsOutcome<shape, values, Core.from_values(shape, values)> ->
524 Laws.FromValuesMeaning(shape, values, Core.from_values(shape, values))}(from_values_counted_elements(shape, values,
525 Shape.bool_case(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape)))))}
526
527def add_successor(+left: Nat, +right: Nat) -> {Nat.add(left, 1n+right) == Nat.add(1n+left, right) : Nat}:
528 match left:
529 case 0n:
530 {==}
531 case 1n+p:
532 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 1n+right), Nat.add(1n+p, right), add_successor(p, right))
533
534def cursor_below(+cursor: Nat, +remaining: Nat, +count: Nat,
535 room: Shape.LE(Nat.add(cursor, 1n+remaining), count)) -> Shape.LT(cursor, count):
536 match cursor count:
537 case 0n 0n:
538 match room:
539 case 0n 1n+q:
540 Unit{}
541 case 1n+p 0n:
542 match room:
543 case 1n+p 1n+q:
544 cursor_below(p, remaining, q, room)
545
546def cursor_exact(+shape: Shape.Shape, +cursor: Nat, room: Shape.LE(cursor, Shape.elements(shape))) ->
547 {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
548 WordConversion.natural_word_exact(cursor, Shape.count(shape),
549 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) :
550 {Nat.is_le(cursor, _) == True{} : Bool}
551 Equal.sym(Bool, True{}, Nat.is_le(cursor, Shape.elements(shape)), Nats.le_true(cursor, Shape.elements(shape), room)))
552
553def cursor_inside(+shape: Shape.Shape, +cursor: Nat, +index: U32,
554 converted: {U32.to_nat(index) == cursor : Nat}, below: Shape.LT(cursor, Shape.elements(shape))) ->
555 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
556 Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))),
557 Nat.is_lt(cursor, Shape.logical_numel(Shape.dimensions(shape))), True{},
558 Equal.cong(Nat, Bool, n => Nat.is_lt(n, Shape.logical_numel(Shape.dimensions(shape))), U32.to_nat(index), cursor, converted),
559 Equal.trans(Bool, Nat.is_lt(cursor, Shape.logical_numel(Shape.dimensions(shape))), Nat.is_lt(cursor, Shape.elements(shape)), True{},
560 Equal.cong(Nat, Bool, n => Nat.is_lt(cursor, n), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape),
561 Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape))),
562 Equal.sym(Bool, True{}, Nat.is_lt(cursor, Shape.elements(shape)), Nats.lt_true(cursor, Shape.elements(shape), below))))
563
564type FillSuccess<-shape: Shape.Shape, -result: Result<&2, &1, Core.Error, Core.Tensor<shape>>> is Data:
565 FillSuccess{-successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}}
566
567def fill_step_success(+shape: Shape.Shape, +rest: List<&2, F32>, +cursor: Nat,
568 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
569 successful: {TransformTotality.write_succeeded(shape, pair) == True{} : Bool},
570 -rec: @tensor: Core.Tensor<shape> -> FillSuccess<shape, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
571 FillSuccess<shape, Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), pair)>:
572 (tensor, result) = pair
573 match result:
574 case Fail{error}:
575 FillSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
576 case Done{unit}:
577 FillSuccess{{\{FillSuccess: successful => successful} : FillSuccess<shape, Core.fill_values(rest, shape, tensor, 1n+cursor)> ->
578 {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, Core.fill_values(rest, shape, tensor, 1n+cursor)) == True{} : Bool}}(rec(tensor))}
579
580def fill_decided_success(+shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +index: U32,
581 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, -original: Core.Tensor<shape>,
582 converted: {U32.to_nat(index) == cursor : Nat},
583 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
584 -rec: @tensor: Core.Tensor<shape> -> FillSuccess<shape, Core.fill_values(rest, shape, tensor, 1n+cursor)>) ->
585 FillSuccess<shape, Core.fill_values_decided(shape, cursor, index, value, original,
586 tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), decision)>:
587 match decision:
588 case Shape.BFalse{equal}:
589 FillSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor),
590 AllocationProof.natural_equal_true(U32.to_nat(index), cursor, converted), equal))}
591 case Shape.BTrue{equal}:
592 FillSuccess{{\{FillSuccess: successful => successful} :
593 FillSuccess<shape, Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor),
594 Core.write_flat(shape, original, index, value))> ->
595 {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>,
596 Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor),
597 Core.write_flat(shape, original, index, value))) == True{} : Bool}}(
598 fill_step_success(shape, rest, cursor, Core.write_flat(shape, original, index, value),
599 {\{TransformTotality.WriteSuccess: successful => successful} : TransformTotality.WriteSuccess<shape, original, index, value> ->
600 {TransformTotality.write_succeeded(shape, Core.write_flat(shape, original, index, value)) == True{} : Bool}}(
601 TransformLaws.tensor_write_valid_success(shape, original, index, value, inside)), rec))}
602
603def fill_success(+values: List<&2, F32>, +shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat,
604 +room: Shape.LE(Nat.add(cursor, List.length(&2, F32, values)), Shape.elements(shape))) ->
605 FillSuccess<shape, Core.fill_values(values, shape, original, cursor)>:
606 match values:
607 case Nil{}:
608 FillSuccess{{==}}
609 case +value <> +rest:
610 fill_decided_success(shape, value, rest, cursor, U32.from_nat(cursor),
611 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), original,
612 cursor_exact(shape, cursor, Nats.le_add_left(cursor, 1n+List.length(&2, F32, rest), Shape.elements(shape), room)),
613 cursor_inside(shape, cursor, U32.from_nat(cursor),
614 cursor_exact(shape, cursor, Nats.le_add_left(cursor, 1n+List.length(&2, F32, rest), Shape.elements(shape), room)),
615 cursor_below(cursor, List.length(&2, F32, rest), Shape.elements(shape), room)),
616 tensor => fill_success(rest, shape, tensor, 1n+cursor,
617 Nats.le_rewrite(Nat.add(1n+cursor, List.length(&2, F32, rest)), Nat.add(cursor, 1n+List.length(&2, F32, rest)),
618 Shape.elements(shape), add_successor(cursor, List.length(&2, F32, rest)), room)))
619
620def allocated_fill_success(+shape: Shape.Shape, +values: List<&2, F32>,
621 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, certificate: Allocation.TensorDone<shape, result>,
622 counted: {List.length(&2, F32, values) == Shape.elements(shape) : Nat}) ->
623 FillSuccess<shape, Core.from_values_new(shape, values, result)>:
624 match result:
625 case Fail{error}:
626 FillSuccess{Empty.absurd({False{} == True{} : Bool},
627 {\{Allocation.TensorDone: tensor => same => Arith.clash(Equal.sym(Bool, True{}, False{},
628 Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Bool,
629 Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>), Done{tensor}, Fail{error}, same)))} :
630 Allocation.TensorDone<shape, Fail{error}> -> Empty}(certificate))}
631 case Done{tensor}:
632 fill_success(values, shape, tensor, 0n,
633 %Equal.sym(Nat, List.length(&2, F32, values), Shape.elements(shape), counted) : Shape.LE(_, Shape.elements(shape))
634 Shape.LE.from(Shape.elements(shape), Shape.elements(shape),
635 Equal.sym(Bool, Nat.is_le(Shape.elements(shape), Shape.elements(shape)), True{}, WordConversion.le_reflexive(Shape.elements(shape)))))
636
637def counted_from_values_success(+shape: Shape.Shape, +values: List<&2, F32>,
638 decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>,
639 counted: {List.length(&2, F32, values) == Shape.elements(shape) : Nat}) ->
640 FillSuccess<shape, Core.from_values_counted(shape, values, decision)>:
641 match decision:
642 case Shape.BFalse{equal}:
643 FillSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape)),
644 AllocationProof.natural_equal_true(List.length(&2, F32, values), Shape.elements(shape), counted), equal))}
645 case Shape.BTrue{equal}:
646 allocated_fill_success(shape, values, Core.new(shape, 0.0), AllocationProof.core_new_done(shape, 0.0), counted)
647
648def completed_tensor(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
649 -successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}) -> Totality.TensorDone<shape, result>:
650 match result:
651 case Fail{error}:
652 Totality.TensorDone{Empty.absurd(Allocation.TensorDone<shape, Fail{error}>, Arith.clash(successful)), successful, Unit{}}
653 case Done{tensor}:
654 Totality.TensorDone{Allocation.TensorDone{tensor, {==}}, {==}, index => inside =>
655 TransformProof.read_success_status(shape, tensor, index, TransformProof.read_success(shape, tensor, index, inside))}
656
657def from_values_complete(+shape: Shape.Shape, +values: List<&2, F32>,
658 counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
659 Totality.TensorDone<shape, Core.from_values(shape, values)>:
660 completed_tensor(shape, Core.from_values(shape, values),
661 {\{FillSuccess: successful => successful} : FillSuccess<shape, Core.from_values(shape, values)> ->
662 {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, Core.from_values(shape, values)) == True{} : Bool}}(
663 counted_from_values_success(shape, values, Shape.bool_case(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))),
664 Equal.trans(Nat, List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape), counted,
665 Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape))))))
666
667def Laws.public_from_values_complete(shape, values, counted):
668 from_values_complete(shape, values, counted)
669
670def construction_values_complete(+dimensions: List<&2, U32>, +shape: Shape.Shape,
671 +preserved: {Shape.dimensions(shape) == dimensions : List<&2, U32>},
672 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>, certificate: Totality.TensorDone<shape, result>) ->
673 Totality.ConstructionDone<dimensions, Core.construct_values(shape, result)>:
674 match result:
675 case Fail{error}:
676 Totality.ConstructionDone{
677 Empty.absurd(Totality.ConstructionWitness<dimensions, Fail{error}>,
678 {\{Totality.TensorDone: witness => successful => readable => Arith.clash(successful)} :
679 Totality.TensorDone<shape, Fail{error}> -> Empty}(certificate)),
680 {\{Totality.TensorDone: witness => successful => readable => successful} :
681 Totality.TensorDone<shape, Fail{error}> -> {False{} == True{} : Bool}}(certificate), Unit{}}
682 case Done{tensor}:
683 Totality.ConstructionDone{Totality.ConstructionWitness{shape, tensor, {==}, preserved}, {==}, index => inside =>
684 TransformProof.read_success_status(shape, tensor, index, TransformProof.read_success(shape, tensor, index,
685 %Equal.sym(List<&2, U32>, Shape.dimensions(shape), dimensions, preserved) :
686 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
687 inside))}
688
689def construction_shape_complete(+dimensions: List<&2, U32>, +values: List<&2, F32>, result: Shape.ConstructResult<dimensions>,
690 built: {ShapeLaws.built(dimensions, result) == Some{dimensions} : Maybe<&2, List<&2, U32>>},
691 +counted: {List.length(&2, F32, values) == Shape.logical_numel(dimensions) : Nat}) ->
692 Totality.ConstructionDone<dimensions, Core.construct_shape(dimensions, values, result)>:
693 match result:
694 case Shape.SError{error}:
695 Totality.ConstructionDone{
696 Empty.absurd(Totality.ConstructionWitness<dimensions, Fail{Core.ShapeError{error}}>,
697 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Maybe.is_some(&2, List<&2, U32>), None{}, Some{dimensions}, built))),
698 Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Maybe.is_some(&2, List<&2, U32>), None{}, Some{dimensions}, built), Unit{}}
699 case Shape.SBuilt{+shape, +preserved}:
700 construction_values_complete(dimensions, shape, preserved, Core.from_values(shape, values),
701 from_values_complete(shape, values,
702 %Equal.sym(List<&2, U32>, Shape.dimensions(shape), dimensions, preserved) :
703 {List.length(&2, F32, values) == Shape.logical_numel(_) : Nat}
704 counted))
705
706def Laws.public_construction_complete(dimensions, values, rank_bound, capacity_bound, counted):
707 construction_shape_complete(dimensions, values, Shape.construct(dimensions),
708 ShapeLaws.construction_complete(dimensions, rank_bound, capacity_bound), counted)