src/tensor/construction_contract_PROOF.bend
bendtorch-core@0.1.0.0 · 339 lines · 27 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
4import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
5import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
6import bendtorch-core@0.1.0.0/src/storage/api.bend as StorageApi
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/allocation_spec.bend as Allocation
11import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
12import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
13import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
14import bendtorch-core@0.1.0.0/src/tensor/construction_metadata.bend as Metadata
15import bendtorch-core@0.1.0.0/src/tensor/construction_contract_LAWS.bend as Laws
16
17def storage_value(result: Result<&2, &2, Storage.Error, F32>) -> Maybe<&2, F32>:
18 match result:
19 case Fail{error}:
20 None{}
21 case Done{value}:
22 Some{value}
23
24def storage_pair_value(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>) ->
25 {Lifecycle.read_value(pair) == storage_value(StorageLaws.outcome(Result<&2, &2, Storage.Error, F32>, pair)) : Maybe<&2, F32>}:
26 (storage, result) = pair
27 match result:
28 case Fail{error}:
29 {==}
30 case Done{value}:
31 {==}
32
33def count_exact(+shape: Shape.Shape) ->
34 {U32.to_nat(Shape.count(shape)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}:
35 Equal.trans(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
36 Conversion.shape_count_exact(shape), Shape.elements_exact(shape))
37
38def word_inside(+shape: Shape.Shape, +index: U32,
39 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
40 {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool}:
41 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), count_exact(shape)) :
42 {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
43 inside
44
45def storage_new_value(+shape: Shape.Shape, +fill: F32, +index: U32,
46 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
47 {Lifecycle.read_value(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)) == Some{fill} : Maybe<&2, F32>}:
48 +within = Conversion.shape_count_within(shape)
49 Equal.trans(Maybe<&2, F32>, Lifecycle.read_value(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)),
50 storage_value(StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index)), Some{fill},
51 storage_pair_value(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)),
52 Equal.cong(Result<&2, &2, Storage.Error, F32>, Maybe<&2, F32>, storage_value,
53 StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index), Done{fill},
54 StorageApi.new_read(U32.to_nat(Shape.count(shape)), fill, U32.is_le(Shape.count(shape), 1048576), [], index,
55 Equal.sym(Bool, U32.is_le(Shape.count(shape), 1048576), True{}, within),
56 StorageApi.cap_from(Shape.count(shape), within), word_inside(shape, index, inside))))
57
58def attached_point(+shape: Shape.Shape, +fill: F32, +index: U32, +length: Nat,
59 decision: Shape.BoolCase<Nat.is_eq(length, Shape.elements(shape))>, storage: Storage.Storage,
60 -exact: {Lifecycle.logical_length(storage) == length : Nat},
61 counted: {length == Shape.elements(shape) : Nat},
62 value: {Lifecycle.read_value(Storage.get(storage, index)) == Some{fill} : Maybe<&2, F32>}) ->
63 {Observation.point(shape, index, Core.attach_decided(shape, storage, length, exact, decision)) == Some{fill} : Maybe<&2, F32>}:
64 match decision:
65 case Shape.BFalse{no}:
66 Empty.absurd({None{} == Some{fill} : Maybe<&2, F32>},
67 Nats.contradiction(Nat.is_eq(length, Shape.elements(shape)),
68 AllocationProof.natural_equal_true(length, Shape.elements(shape), counted), no))
69 case Shape.BTrue{yes}:
70 Equal.trans(Maybe<&2, F32>,
71 Observation.point(shape, index, Core.attach_decided(shape, storage, length, exact, Shape.BTrue{yes})),
72 Lifecycle.read_value(Storage.get(storage, index)), Some{fill},
73 Core.read_result_value(shape, storage,
74 Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
75 Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
76 Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape))),
77 index, Storage.get(storage, index), {==}), value)
78
79def attach_point(+shape: Shape.Shape, +fill: F32, +index: U32, storage: Storage.Storage,
80 counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat},
81 value: {Lifecycle.read_value(Storage.get(storage, index)) == Some{fill} : Maybe<&2, F32>}) ->
82 {Observation.point(shape, index, Core.attach(shape, storage)) == Some{fill} : Maybe<&2, F32>}:
83 match storage:
84 case Storage.Empty{}:
85 attached_point(shape, fill, index, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))),
86 Storage.Empty{}, {==}, counted, value)
87 case Storage.Owned{+depth, +length, array, balanced, valid}:
88 attached_point(shape, fill, index, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))),
89 Storage.Owned{depth, length, array, balanced, valid}, {==}, counted, value)
90
91def result_point(+shape: Shape.Shape, +fill: F32, +index: U32,
92 result: Result<&2, &1, Storage.Error, Storage.Storage>,
93 counted: {Allocation.storage_length(result) == Some{Shape.elements(shape)} : Maybe<&2, Nat>},
94 value: {Lifecycle.read_value(Storage.get(StorageLaws.created.of(result), index)) == Some{fill} : Maybe<&2, F32>}) ->
95 {Observation.point(shape, index, Core.new_result(shape, result)) == Some{fill} : Maybe<&2, F32>}:
96 match result:
97 case Fail{error}:
98 Empty.absurd({None{} == Some{fill} : Maybe<&2, F32>},
99 Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value),
100 None{}, Some{Shape.elements(shape)}, counted)))
101 case Done{storage}:
102 attach_point(shape, fill, index, storage,
103 Equal.cong(Maybe<&2, Nat>, Nat, value => Maybe.default(&2, Nat, value, 0n),
104 Some{Lifecycle.logical_length(storage)}, Some{Shape.elements(shape)}, counted), value)
105
106def point_value(+shape: Shape.Shape, +fill: F32, +index: U32,
107 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
108 {Observation.point(shape, index, Core.new(shape, fill)) == Some{fill} : Maybe<&2, F32>}:
109 result_point(shape, fill, index, Storage.new(Shape.count(shape), fill),
110 Equal.trans(Maybe<&2, Nat>, Allocation.storage_length(Storage.new(Shape.count(shape), fill)),
111 Some{U32.to_nat(Shape.count(shape))}, Some{Shape.elements(shape)},
112 AllocationProof.storage_new(Shape.count(shape), fill, Conversion.shape_count_within(shape)),
113 Equal.cong(Nat, Maybe<&2, Nat>, value => Some{value}, U32.to_nat(Shape.count(shape)), Shape.elements(shape),
114 Conversion.shape_count_exact(shape))),
115 storage_new_value(shape, fill, index, inside))
116
117def size_is_length(storage: Storage.Storage) -> {StorageLaws.size(storage) == Lifecycle.logical_length(storage) : Nat}:
118 match storage:
119 case Storage.Empty{}:
120 {==}
121 case Storage.Owned{depth, length, array, balanced, valid}:
122 {==}
123
124def retained_is_kept(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>) ->
125 {Lifecycle.retained_read(pair) == Lifecycle.logical_length(StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, pair)) : Nat}:
126 (storage, result) = pair
127 {==}
128
129def stored_after_value(+shape: Shape.Shape, +fill: F32, +index: U32, +other: U32,
130 inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
131 {Lifecycle.read_value(Storage.get(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other)) == Some{fill} : Maybe<&2, F32>}:
132 +within = Conversion.shape_count_within(shape)
133 Equal.trans(Maybe<&2, F32>,
134 Lifecycle.read_value(Storage.get(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other)),
135 storage_value(StorageLaws.read(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other)), Some{fill},
136 storage_pair_value(Storage.get(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other)),
137 Equal.cong(Result<&2, &2, Storage.Error, F32>, Maybe<&2, F32>, storage_value,
138 StorageLaws.read(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other), Done{fill},
139 StorageApi.new_read(U32.to_nat(Shape.count(shape)), fill, U32.is_le(Shape.count(shape), 1048576), [StorageLaws.Read{index}], other,
140 Equal.sym(Bool, U32.is_le(Shape.count(shape), 1048576), True{}, within), StorageApi.cap_from(Shape.count(shape), within),
141 word_inside(shape, other, inside))))
142
143def stored_after_length(+shape: Shape.Shape, +fill: F32, +index: U32) ->
144 {Lifecycle.retained_read(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)) ==
145 Shape.logical_numel(Shape.dimensions(shape)) : Nat}:
146 +within = Conversion.shape_count_within(shape)
147 Equal.trans(Nat, Lifecycle.retained_read(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)),
148 StorageLaws.size(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index)), Shape.logical_numel(Shape.dimensions(shape)),
149 Equal.trans(Nat, Lifecycle.retained_read(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)),
150 Lifecycle.logical_length(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index)),
151 StorageLaws.size(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index)),
152 retained_is_kept(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)),
153 Equal.sym(Nat, StorageLaws.size(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index)),
154 Lifecycle.logical_length(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index)),
155 size_is_length(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index)))),
156 Equal.trans(Nat, StorageLaws.size(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index)),
157 U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)),
158 StorageApi.new_size(U32.to_nat(Shape.count(shape)), fill, U32.is_le(Shape.count(shape), 1048576), [StorageLaws.Read{index}],
159 Equal.sym(Bool, U32.is_le(Shape.count(shape), 1048576), True{}, within), StorageApi.cap_from(Shape.count(shape), within)),
160 count_exact(shape)))
161
162def next_projection(-shape: Shape.Shape, -original: Storage.Storage,
163 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +other: U32,
164 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>,
165 -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
166 {Observation.after_value_pair(shape, other, Core.read_result(shape, original, valid, index, pair, same)) ==
167 Lifecycle.read_value(Storage.get(StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, pair), other)) : Maybe<&2, F32>}:
168 (storage, result) = pair
169 Core.read_result_value(shape, storage,
170 Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
171 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, (storage, result), Storage.get(original, index), same) :
172 {Lifecycle.retained_read(_) == Lifecycle.logical_length(original) : Nat}
173 Lifecycle.get_length(original, index), valid),
174 other, Storage.get(storage, other), {==})
175
176def length_projection(-shape: Shape.Shape, -original: Storage.Storage,
177 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
178 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>,
179 -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
180 {Observation.after_length_pair(shape, Core.read_result(shape, original, valid, index, pair, same)) == Lifecycle.retained_read(pair) : Nat}:
181 (storage, result) = pair
182 {==}
183
184def attached_value(+shape: Shape.Shape, +fill: F32, +index: U32, +other: U32, +length: Nat,
185 decision: Shape.BoolCase<Nat.is_eq(length, Shape.elements(shape))>, storage: Storage.Storage,
186 -exact: {Lifecycle.logical_length(storage) == length : Nat}, counted: {length == Shape.elements(shape) : Nat},
187 kept: {Lifecycle.read_value(Storage.get(StorageLaws.kept(storage, index), other)) == Some{fill} : Maybe<&2, F32>}) ->
188 {Observation.after_value(shape, index, other, Core.attach_decided(shape, storage, length, exact, decision)) == Some{fill} : Maybe<&2, F32>}:
189 match decision:
190 case Shape.BFalse{no}:
191 Empty.absurd({None{} == Some{fill} : Maybe<&2, F32>}, Nats.contradiction(Nat.is_eq(length, Shape.elements(shape)),
192 AllocationProof.natural_equal_true(length, Shape.elements(shape), counted), no))
193 case Shape.BTrue{yes}:
194 Equal.trans(Maybe<&2, F32>,
195 Observation.after_value(shape, index, other, Core.attach_decided(shape, storage, length, exact, Shape.BTrue{yes})),
196 Lifecycle.read_value(Storage.get(StorageLaws.kept(storage, index), other)), Some{fill},
197 next_projection(shape, storage,
198 Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
199 Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
200 Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape))),
201 index, other, Storage.get(storage, index), {==}), kept)
202
203def attach_value(+shape: Shape.Shape, +fill: F32, +index: U32, +other: U32, storage: Storage.Storage,
204 counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat},
205 kept: {Lifecycle.read_value(Storage.get(StorageLaws.kept(storage, index), other)) == Some{fill} : Maybe<&2, F32>}) ->
206 {Observation.after_value(shape, index, other, Core.attach(shape, storage)) == Some{fill} : Maybe<&2, F32>}:
207 match storage:
208 case Storage.Empty{}:
209 attached_value(shape, fill, index, other, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), Storage.Empty{}, {==}, counted, kept)
210 case Storage.Owned{+depth, +length, array, balanced, valid}:
211 attached_value(shape, fill, index, other, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))),
212 Storage.Owned{depth, length, array, balanced, valid}, {==}, counted, kept)
213
214def retained_result_value(+shape: Shape.Shape, +fill: F32, +index: U32, +other: U32,
215 result: Result<&2, &1, Storage.Error, Storage.Storage>,
216 counted: {Allocation.storage_length(result) == Some{Shape.elements(shape)} : Maybe<&2, Nat>},
217 kept: {Lifecycle.read_value(Storage.get(StorageLaws.kept(StorageLaws.created.of(result), index), other)) == Some{fill} : Maybe<&2, F32>}) ->
218 {Observation.after_value(shape, index, other, Core.new_result(shape, result)) == Some{fill} : Maybe<&2, F32>}:
219 match result:
220 case Fail{error}:
221 Empty.absurd({None{} == Some{fill} : Maybe<&2, F32>}, Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool,
222 value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.elements(shape)}, counted)))
223 case Done{storage}:
224 attach_value(shape, fill, index, other, storage,
225 Equal.cong(Maybe<&2, Nat>, Nat, value => Maybe.default(&2, Nat, value, 0n),
226 Some{Lifecycle.logical_length(storage)}, Some{Shape.elements(shape)}, counted), kept)
227
228def retained_value(+shape: Shape.Shape, +fill: F32, +index: U32, +other: U32,
229 inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
230 {Observation.after_value(shape, index, other, Core.new(shape, fill)) == Some{fill} : Maybe<&2, F32>}:
231 retained_result_value(shape, fill, index, other, Storage.new(Shape.count(shape), fill),
232 Equal.trans(Maybe<&2, Nat>, Allocation.storage_length(Storage.new(Shape.count(shape), fill)), Some{U32.to_nat(Shape.count(shape))}, Some{Shape.elements(shape)},
233 AllocationProof.storage_new(Shape.count(shape), fill, Conversion.shape_count_within(shape)),
234 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape))),
235 stored_after_value(shape, fill, index, other, inside))
236
237def attached_length(+shape: Shape.Shape, +index: U32, +length: Nat,
238 decision: Shape.BoolCase<Nat.is_eq(length, Shape.elements(shape))>, storage: Storage.Storage,
239 -exact: {Lifecycle.logical_length(storage) == length : Nat}, counted: {length == Shape.elements(shape) : Nat},
240 kept: {Lifecycle.retained_read(Storage.get(storage, index)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
241 {Observation.after_length(shape, index, Core.attach_decided(shape, storage, length, exact, decision)) ==
242 Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
243 match decision:
244 case Shape.BFalse{no}:
245 Empty.absurd({None{} == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
246 Nats.contradiction(Nat.is_eq(length, Shape.elements(shape)), AllocationProof.natural_equal_true(length, Shape.elements(shape), counted), no))
247 case Shape.BTrue{yes}:
248 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
249 Observation.after_length_pair(shape, Core.read_flat(shape,
250 Core.TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
251 Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
252 Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape)))}, index)),
253 Shape.logical_numel(Shape.dimensions(shape)),
254 Equal.trans(Nat,
255 Observation.after_length_pair(shape, Core.read_flat(shape,
256 Core.TTensor{storage, Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
257 Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
258 Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape)))}, index)),
259 Lifecycle.retained_read(Storage.get(storage, index)), Shape.logical_numel(Shape.dimensions(shape)),
260 length_projection(shape, storage,
261 Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
262 Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
263 Lifecycle.natural_equal(length, Shape.elements(shape), yes), Shape.elements_exact(shape))),
264 index, Storage.get(storage, index), {==}), kept))
265
266def attach_length(+shape: Shape.Shape, +index: U32, storage: Storage.Storage,
267 counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat},
268 kept: {Lifecycle.retained_read(Storage.get(storage, index)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
269 {Observation.after_length(shape, index, Core.attach(shape, storage)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
270 match storage:
271 case Storage.Empty{}:
272 attached_length(shape, index, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), Storage.Empty{}, {==}, counted, kept)
273 case Storage.Owned{+depth, +length, array, balanced, valid}:
274 attached_length(shape, index, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))),
275 Storage.Owned{depth, length, array, balanced, valid}, {==}, counted, kept)
276
277def result_length(+shape: Shape.Shape, +index: U32, result: Result<&2, &1, Storage.Error, Storage.Storage>,
278 counted: {Allocation.storage_length(result) == Some{Shape.elements(shape)} : Maybe<&2, Nat>},
279 kept: {Lifecycle.retained_read(Storage.get(StorageLaws.created.of(result), index)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
280 {Observation.after_length(shape, index, Core.new_result(shape, result)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
281 match result:
282 case Fail{error}:
283 Empty.absurd({None{} == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}, Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool,
284 value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.elements(shape)}, counted)))
285 case Done{storage}:
286 attach_length(shape, index, storage,
287 Equal.cong(Maybe<&2, Nat>, Nat, value => Maybe.default(&2, Nat, value, 0n),
288 Some{Lifecycle.logical_length(storage)}, Some{Shape.elements(shape)}, counted), kept)
289
290def retained_length(+shape: Shape.Shape, +fill: F32, +index: U32) ->
291 {Observation.after_length(shape, index, Core.new(shape, fill)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
292 result_length(shape, index, Storage.new(Shape.count(shape), fill),
293 Equal.trans(Maybe<&2, Nat>, Allocation.storage_length(Storage.new(Shape.count(shape), fill)), Some{U32.to_nat(Shape.count(shape))}, Some{Shape.elements(shape)},
294 AllocationProof.storage_new(Shape.count(shape), fill, Conversion.shape_count_within(shape)),
295 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape))),
296 stored_after_length(shape, fill, index))
297
298def retained_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
299 {Observation.after_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
300 (tensor, result) = pair
301 {==}
302
303def retained_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
304 {Observation.after_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
305 (tensor, result) = pair
306 {==}
307
308def dimensions_result(+shape: Shape.Shape, +index: U32, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
309 successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}) ->
310 {Observation.after_dimensions(shape, index, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
311 match result:
312 case Fail{error}:
313 Empty.absurd({None{} == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}, Arith.clash(successful))
314 case Done{tensor}:
315 retained_dimensions_pair(shape, Core.read_flat(shape, tensor, index))
316
317def count_result(+shape: Shape.Shape, +index: U32, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
318 successful: {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}) ->
319 {Observation.after_count(shape, index, result) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
320 match result:
321 case Fail{error}:
322 Empty.absurd({None{} == Some{Shape.count(shape)} : Maybe<&2, U32>}, Arith.clash(successful))
323 case Done{tensor}:
324 retained_count_pair(shape, Core.read_flat(shape, tensor, index))
325
326def Laws.new_metadata(shape, fill):
327 Metadata.construction(shape, fill)
328
329def Laws.new_reads(shape, fill, index, inside):
330 +successful = Metadata.generic_status_consumer(shape, fill)
331 Laws.NewReads{successful,
332 Metadata.completed_dimensions(shape, Core.new(shape, fill), successful),
333 AllocationProof.core_new(shape, fill),
334 Metadata.completed_count(shape, Core.new(shape, fill), successful),
335 point_value(shape, fill, index, inside),
336 dimensions_result(shape, index, Core.new(shape, fill), successful),
337 retained_length(shape, fill, index),
338 count_result(shape, index, Core.new(shape, fill), successful),
339 other => inside => retained_value(shape, fill, index, other, inside)}