1	import Base
2	import ../shape/core.bend as Shape
3	import ../shape/nat_proofs.bend as Nats
4	import ../storage/main.bend as Storage
5	import ../storage/LAWS.bend as StorageLaws
6	import ../storage/api.bend as StorageApi
7	import ../storage/arith.bend as Arith
8	import ./core.bend as Core
9	import ./lifecycle.bend as Lifecycle
10	import ./allocation_spec.bend as Allocation
11	import ./allocation_PROOF.bend as AllocationProof
12	import ./word_conversion.bend as Conversion
13	import ./observation.bend as Observation
14	import ./construction_metadata.bend as Metadata
15	import ./construction_contract_LAWS.bend as Laws
16	
17	def 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	
24	def 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	
33	def 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	
38	def 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	
45	def 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	
58	def 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	
79	def 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	
91	def 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	
106	def 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	
117	def 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	
124	def 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	
129	def 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	
143	def 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	
162	def 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	
176	def 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	
184	def 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	
203	def 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	
214	def 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	
228	def 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	
237	def 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	
266	def 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	
277	def 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	
290	def 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	
298	def 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	
303	def 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	
308	def 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	
317	def 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	
326	def Laws.new_metadata(shape, fill):
327	  Metadata.construction(shape, fill)
328	
329	def 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)}