src/tensor/from_values_contract.bend
bendtorch-core@0.1.0.0 · 377 lines · 31 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/PROOF.bend as StorageProof
7import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
8import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
9import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
10import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
11import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
12import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
13import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
14import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
15import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
16import bendtorch-core@0.1.0.0/src/tensor/from_values_records.bend as Laws
17
18def writes(values: List<&2, F32>, +cursor: Nat) -> List<&2, StorageLaws.Op>:
19 match values:
20 case Nil{}:
21 Nil{}
22 case value <> rest:
23 StorageLaws.Write{U32.from_nat(cursor), value} <> writes(rest, 1n+cursor)
24
25def base(+shape: Shape.Shape, +prefix: List<&2, StorageLaws.Op>) -> Storage.Storage:
26 StorageLaws.replay(prefix, StorageLaws.created(Shape.count(shape), 0.0))
27
28def Filled(+shape: Shape.Shape, +values: List<&2, F32>, +cursor: Nat, +prefix: List<&2, StorageLaws.Op>,
29 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type) -> Type:
30 @-fits: {Lifecycle.logical_length(StorageLaws.replay(writes(values, cursor), base(shape, prefix))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
31 P(Done{Core.TTensor{StorageLaws.replay(writes(values, cursor), base(shape, prefix)), fits}})
32
33def storage_of(-shape: Shape.Shape, tensor: Core.Tensor<shape>) -> Storage.Storage:
34 Core.TTensor{storage, valid} = tensor
35 storage
36
37def written_storage(-shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) -> Storage.Storage:
38 (tensor, result) = pair
39 storage_of(shape, tensor)
40
41def room_next(+cursor: Nat, +remaining: Nat, +bound: Nat,
42 room: {Nat.is_le(Nat.add(cursor, 1n+remaining), bound) == True{} : Bool}) ->
43 {Nat.is_le(Nat.add(1n+cursor, remaining), bound) == True{} : Bool}:
44 %Arith.add_succ(cursor, remaining) : {Nat.is_le(_, bound) == True{} : Bool}
45 room
46
47def cursor_le(+cursor: Nat, +remaining: Nat, +bound: Nat,
48 room: {Nat.is_le(Nat.add(cursor, 1n+remaining), bound) == True{} : Bool}) ->
49 {Nat.is_le(cursor, bound) == True{} : Bool}:
50 Conversion.le_trans(cursor, Nat.add(cursor, 1n+remaining), bound, Api.le_add_right(cursor, 1n+remaining), room)
51
52def cursor_lt(+cursor: Nat, +remaining: Nat, +bound: Nat,
53 room: {Nat.is_le(Nat.add(cursor, 1n+remaining), bound) == True{} : Bool}) ->
54 {Nat.is_lt(cursor, bound) == True{} : Bool}:
55 Arith.lt_le_trans(cursor, 1n+cursor, bound, Arith.lt_succ(cursor, cursor, Api.le_refl(cursor)),
56 Conversion.le_trans(1n+cursor, Nat.add(1n+cursor, remaining), bound, Api.le_add_right(1n+cursor, remaining),
57 room_next(cursor, remaining, bound, room)))
58
59def cursor_exact(+cursor: Nat, +remaining: Nat, +limit: U32,
60 room: {Nat.is_le(Nat.add(cursor, 1n+remaining), U32.to_nat(limit)) == True{} : Bool}) ->
61 {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
62 Conversion.natural_word_exact(cursor, limit, cursor_le(cursor, remaining, U32.to_nat(limit), room))
63
64def cursor_inside(+cursor: Nat, +remaining: Nat, +limit: U32,
65 room: {Nat.is_le(Nat.add(cursor, 1n+remaining), U32.to_nat(limit)) == True{} : Bool}) ->
66 {Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), U32.to_nat(limit)) == True{} : Bool}:
67 +room = room
68 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_exact(cursor, remaining, limit, room)) :
69 {Nat.is_lt(_, U32.to_nat(limit)) == True{} : Bool}
70 cursor_lt(cursor, remaining, U32.to_nat(limit), room)
71
72def lt_different(+small: Nat, +big: Nat, earlier: {Nat.is_lt(small, big) == True{} : Bool}) ->
73 {Nat.is_eq(big, small) == False{} : Bool}:
74 match small big:
75 case 0n 0n:
76 Empty.absurd({True{} == False{} : Bool}, Arith.clash(earlier))
77 case 0n 1n+q:
78 {==}
79 case 1n+p 0n:
80 {==}
81 case 1n+p 1n+q:
82 lt_different(p, q, earlier)
83
84def missed(+cursor: Nat, +remaining: Nat, +limit: U32, +index: U32, +value: F32, +base: F32,
85 room: {Nat.is_le(Nat.add(cursor, 1n+remaining), U32.to_nat(limit)) == True{} : Bool},
86 earlier: {Nat.is_lt(U32.to_nat(index), cursor) == True{} : Bool}) ->
87 {StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base) == base : F32}:
88 +room = room
89 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_exact(cursor, remaining, limit, room)) :
90 {Bool.pick(F32, Bool.and(Nat.is_lt(_, U32.to_nat(limit)), Nat.is_eq(_, U32.to_nat(index))), value, base) == base : F32}
91 %Equal.sym(Bool, Nat.is_lt(cursor, U32.to_nat(limit)), True{}, cursor_lt(cursor, remaining, U32.to_nat(limit), room)) :
92 {Bool.pick(F32, Bool.and(_, Nat.is_eq(cursor, U32.to_nat(index))), value, base) == base : F32}
93 %Equal.sym(Bool, Nat.is_eq(cursor, U32.to_nat(index)), False{}, lt_different(U32.to_nat(index), cursor, earlier)) :
94 {Bool.pick(F32, _, value, base) == base : F32}
95 {==}
96
97def later_writes(+values: List<&2, F32>, +cursor: Nat, +limit: U32, +index: U32, +base: F32,
98 room: {Nat.is_le(Nat.add(cursor, List.length(&2, F32, values)), U32.to_nat(limit)) == True{} : Bool},
99 earlier: {Nat.is_lt(U32.to_nat(index), cursor) == True{} : Bool}) ->
100 {StorageLaws.expected(writes(values, cursor), U32.to_nat(limit), index, base) == base : F32}:
101 match values:
102 case Nil{}:
103 {==}
104 case +value <> +rest:
105 +room = room
106 +earlier = earlier
107 Equal.trans(F32,
108 StorageLaws.expected(writes(rest, 1n+cursor), U32.to_nat(limit), index,
109 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base)),
110 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base), base,
111 later_writes(rest, 1n+cursor, limit, index,
112 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base),
113 room_next(cursor, List.length(&2, F32, rest), U32.to_nat(limit), room),
114 Arith.lt_le_trans(U32.to_nat(index), cursor, 1n+cursor, earlier, Arith.le_succ(cursor, cursor, Api.le_refl(cursor)))),
115 missed(cursor, List.length(&2, F32, rest), limit, index, value, base, room, earlier))
116
117def hit(+cursor: Nat, +remaining: Nat, +limit: U32, +index: U32, +value: F32, +base: F32,
118 room: {Nat.is_le(Nat.add(cursor, 1n+remaining), U32.to_nat(limit)) == True{} : Bool},
119 at: {U32.to_nat(index) == cursor : Nat}) ->
120 {StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base) == value : F32}:
121 +room = room
122 %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_exact(cursor, remaining, limit, room)) :
123 {Bool.pick(F32, Bool.and(Nat.is_lt(_, U32.to_nat(limit)), Nat.is_eq(_, U32.to_nat(index))), value, base) == value : F32}
124 %Equal.sym(Nat, U32.to_nat(index), cursor, at) :
125 {Bool.pick(F32, Bool.and(Nat.is_lt(cursor, U32.to_nat(limit)), Nat.is_eq(cursor, _)), value, base) == value : F32}
126 %Equal.sym(Bool, Nat.is_lt(cursor, U32.to_nat(limit)), True{}, cursor_lt(cursor, remaining, U32.to_nat(limit), room)) :
127 {Bool.pick(F32, Bool.and(_, Nat.is_eq(cursor, cursor)), value, base) == value : F32}
128 %Equal.sym(Bool, Nat.is_eq(cursor, cursor), True{}, Arith.eq_refl(cursor)) :
129 {Bool.pick(F32, _, value, base) == value : F32}
130 {==}
131
132def written_at(+values: List<&2, F32>, +cursor: Nat, +limit: U32, +index: U32, +base: F32, +offset: Nat,
133 +room: {Nat.is_le(Nat.add(cursor, List.length(&2, F32, values)), U32.to_nat(limit)) == True{} : Bool},
134 at: {U32.to_nat(index) == Nat.add(cursor, offset) : Nat},
135 below: {Nat.is_lt(offset, List.length(&2, F32, values)) == True{} : Bool}) ->
136 {Some{StorageLaws.expected(writes(values, cursor), U32.to_nat(limit), index, base)} == List.get(&2, F32, values, offset) : Maybe<&2, F32>}:
137 match values offset:
138 case Nil{} _:
139 Empty.absurd({Some{base} == None{} : Maybe<&2, F32>}, Arith.lt_zero(offset, below))
140 case +value <> +rest 0n:
141 +exact = Equal.trans(Nat, U32.to_nat(index), Nat.add(cursor, 0n), cursor, at, Conversion.add_zero(cursor))
142 Equal.cong(F32, Maybe<&2, F32>, found => Some{found},
143 StorageLaws.expected(writes(rest, 1n+cursor), U32.to_nat(limit), index,
144 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base)), value,
145 Equal.trans(F32,
146 StorageLaws.expected(writes(rest, 1n+cursor), U32.to_nat(limit), index,
147 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base)),
148 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base), value,
149 later_writes(rest, 1n+cursor, limit, index,
150 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base),
151 room_next(cursor, List.length(&2, F32, rest), U32.to_nat(limit), room),
152 %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, 1n+cursor) == True{} : Bool}
153 Arith.lt_succ(cursor, cursor, Api.le_refl(cursor))),
154 hit(cursor, List.length(&2, F32, rest), limit, index, value, base, room, exact)))
155 case +value <> +rest 1n+next:
156 written_at(rest, 1n+cursor, limit, index,
157 StorageLaws.latest(U32.to_nat(limit), StorageLaws.Write{U32.from_nat(cursor), value}, index, base), next,
158 room_next(cursor, List.length(&2, F32, rest), U32.to_nat(limit), room),
159 Equal.trans(Nat, U32.to_nat(index), Nat.add(cursor, 1n+next), 1n+Nat.add(cursor, next), at, Arith.add_succ(cursor, next)),
160 below)
161
162def replay_snoc(+ops: List<&2, StorageLaws.Op>, +op: StorageLaws.Op, -storage: Storage.Storage) ->
163 {StorageLaws.replay(List.append(&2, StorageLaws.Op, ops, [op]), storage) == StorageLaws.step(StorageLaws.replay(ops, storage), op) : Storage.Storage}:
164 match ops:
165 case Nil{}:
166 {==}
167 case +first <> +rest:
168 replay_snoc(rest, op, StorageLaws.step(storage, first))
169
170def moved_projection(-shape: Shape.Shape, -original: Storage.Storage,
171 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
172 pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
173 -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
174 {written_storage(shape, Core.write_result(shape, original, valid, index, value, pair, same)) ==
175 StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, pair) : Storage.Storage}:
176 (storage, result) = pair
177 {==}
178
179def done_projection(-shape: Shape.Shape, -original: Storage.Storage,
180 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
181 pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
182 -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
183 {Observation.write_done_pair(shape, Core.write_result(shape, original, valid, index, value, pair, same)) ==
184 Result.is_done(&2, &2, Storage.Error, Unit, StorageLaws.outcome(Result<&2, &2, Storage.Error, Unit>, pair)) : Bool}:
185 (storage, result) = pair
186 match result:
187 case Fail{error}:
188 {==}
189 case Done{unit}:
190 {==}
191
192def write_moved(+shape: Shape.Shape, +prefix: List<&2, StorageLaws.Op>,
193 -valid: {Lifecycle.logical_length(base(shape, prefix)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32) ->
194 {written_storage(shape, Core.write_flat(shape, Core.TTensor{base(shape, prefix), valid}, index, value)) ==
195 StorageLaws.written(base(shape, prefix), index, value) : Storage.Storage}:
196 moved_projection(shape, base(shape, prefix), valid, index, value, Storage.set(base(shape, prefix), index, value), {==})
197
198def write_done(+shape: Shape.Shape, +prefix: List<&2, StorageLaws.Op>,
199 -valid: {Lifecycle.logical_length(base(shape, prefix)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
200 inside: {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool}) ->
201 {Observation.write_done_pair(shape, Core.write_flat(shape, Core.TTensor{base(shape, prefix), valid}, index, value)) == True{} : Bool}:
202 Equal.trans(Bool, Observation.write_done_pair(shape, Core.write_flat(shape, Core.TTensor{base(shape, prefix), valid}, index, value)),
203 Result.is_done(&2, &2, Storage.Error, Unit, StorageLaws.status(base(shape, prefix), index, value)), True{},
204 done_projection(shape, base(shape, prefix), valid, index, value, Storage.set(base(shape, prefix), index, value), {==}),
205 Equal.cong(Result<&2, &2, Storage.Error, Unit>, Bool, Result.is_done(&2, &2, Storage.Error, Unit),
206 StorageLaws.status(base(shape, prefix), index, value), Done{Unit{}},
207 StorageLaws.replay_set(Shape.count(shape), 0.0, prefix, index, value, Conversion.shape_count_within(shape), inside)))
208
209def moved_lift(+shape: Shape.Shape, -rest: List<&2, F32>, +cursor: Nat, -source: Storage.Storage, -target: Storage.Storage,
210 moved: {source == target : Storage.Storage}, -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type,
211 next: @-valid: {Lifecycle.logical_length(source) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
212 P(Core.fill_values(rest, shape, Core.TTensor{source, valid}, 1n+cursor))) ->
213 @-valid: {Lifecycle.logical_length(target) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
214 P(Core.fill_values(rest, shape, Core.TTensor{target, valid}, 1n+cursor)):
215 %moved : (@-valid: {Lifecycle.logical_length(_) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
216 P(Core.fill_values(rest, shape, Core.TTensor{_, valid}, 1n+cursor)))
217 next
218
219def written_step(+shape: Shape.Shape, +value: F32, -rest: List<&2, F32>, +cursor: Nat, +prefix: List<&2, StorageLaws.Op>, +index: U32,
220 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
221 done: {Observation.write_done_pair(shape, pair) == True{} : Bool},
222 moved: {written_storage(shape, pair) == StorageLaws.written(base(shape, prefix), index, value) : Storage.Storage},
223 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type,
224 next: @-valid: {Lifecycle.logical_length(base(shape, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{index, value}]))) ==
225 Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
226 P(Core.fill_values(rest, shape, Core.TTensor{base(shape, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{index, value}])), valid}, 1n+cursor))) ->
227 P(Core.fill_values_step(shape, tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), pair)):
228 match pair:
229 case (Core.TTensor{storage, valid}, Fail{error}):
230 Empty.absurd(P(Fail{error}), Arith.clash(done))
231 case (Core.TTensor{storage, valid}, Done{unit}):
232 moved_lift(shape, rest, cursor, base(shape, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{index, value}])), storage,
233 Equal.trans(Storage.Storage, base(shape, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{index, value}])),
234 StorageLaws.written(base(shape, prefix), index, value), storage,
235 replay_snoc(prefix, StorageLaws.Write{index, value}, StorageLaws.created(Shape.count(shape), 0.0)),
236 Equal.sym(Storage.Storage, storage, StorageLaws.written(base(shape, prefix), index, value), moved)),
237 P, next)(valid)
238
239def decided_step(+shape: Shape.Shape, +value: F32, -rest: List<&2, F32>, +cursor: Nat, +prefix: List<&2, StorageLaws.Op>, +index: U32,
240 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
241 converted: {U32.to_nat(index) == cursor : Nat},
242 inside: {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool},
243 -valid: {Lifecycle.logical_length(base(shape, prefix)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
244 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type,
245 next: @-valid: {Lifecycle.logical_length(base(shape, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{index, value}]))) ==
246 Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
247 P(Core.fill_values(rest, shape, Core.TTensor{base(shape, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{index, value}])), valid}, 1n+cursor))) ->
248 P(Core.fill_values_decided(shape, cursor, index, value, Core.TTensor{base(shape, prefix), valid},
249 tensor => Core.fill_values(rest, shape, tensor, 1n+cursor), decision)):
250 match decision:
251 case Shape.BFalse{equal}:
252 Empty.absurd(P(Fail{Core.StorageError{Storage.InvalidIndex{}}}),
253 Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor),
254 AllocationProof.natural_equal_true(U32.to_nat(index), cursor, converted), equal))
255 case Shape.BTrue{equal}:
256 written_step(shape, value, rest, cursor, prefix, index,
257 Core.write_flat(shape, Core.TTensor{base(shape, prefix), valid}, index, value),
258 write_done(shape, prefix, valid, index, value, inside), write_moved(shape, prefix, valid, index, value), P, next)
259
260def filled_next(+shape: Shape.Shape, +value: F32, +rest: List<&2, F32>, +cursor: Nat, +prefix: List<&2, StorageLaws.Op>,
261 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type, h: Filled(shape, value <> rest, cursor, prefix, P)) ->
262 Filled(shape, rest, 1n+cursor, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{U32.from_nat(cursor), value}]), P):
263 %Equal.sym(Storage.Storage, base(shape, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{U32.from_nat(cursor), value}])),
264 StorageLaws.written(base(shape, prefix), U32.from_nat(cursor), value),
265 replay_snoc(prefix, StorageLaws.Write{U32.from_nat(cursor), value}, StorageLaws.created(Shape.count(shape), 0.0))) :
266 (@-fits: {Lifecycle.logical_length(StorageLaws.replay(writes(rest, 1n+cursor), _)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
267 P(Done{Core.TTensor{StorageLaws.replay(writes(rest, 1n+cursor), _), fits}}))
268 h
269
270def fill_lift(+values: List<&2, F32>, +shape: Shape.Shape, +cursor: Nat, +prefix: List<&2, StorageLaws.Op>,
271 room: {Nat.is_le(Nat.add(cursor, List.length(&2, F32, values)), U32.to_nat(Shape.count(shape))) == True{} : Bool},
272 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type, h: Filled(shape, values, cursor, prefix, P)) ->
273 @-valid: {Lifecycle.logical_length(base(shape, prefix)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
274 P(Core.fill_values(values, shape, Core.TTensor{base(shape, prefix), valid}, cursor)):
275 match values:
276 case Nil{}:
277 h
278 case +value <> +rest:
279 +room = room
280 valid => decided_step(shape, value, rest, cursor, prefix, U32.from_nat(cursor),
281 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)),
282 cursor_exact(cursor, List.length(&2, F32, rest), Shape.count(shape), room),
283 cursor_inside(cursor, List.length(&2, F32, rest), Shape.count(shape), room), valid, P,
284 fill_lift(rest, shape, 1n+cursor, List.append(&2, StorageLaws.Op, prefix, [StorageLaws.Write{U32.from_nat(cursor), value}]),
285 room_next(cursor, List.length(&2, F32, rest), U32.to_nat(Shape.count(shape)), room), P,
286 filled_next(shape, value, rest, cursor, prefix, P, h)))
287
288def start_room(+shape: Shape.Shape, +values: List<&2, F32>,
289 +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
290 {Nat.is_le(Nat.add(0n, List.length(&2, F32, values)), U32.to_nat(Shape.count(shape))) == True{} : Bool}:
291 %Equal.sym(Nat, List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), counted) :
292 {Nat.is_le(_, U32.to_nat(Shape.count(shape))) == True{} : Bool}
293 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), Reads.count_exact(shape)) :
294 {Nat.is_le(Shape.logical_numel(Shape.dimensions(shape)), _) == True{} : Bool}
295 Api.le_refl(Shape.logical_numel(Shape.dimensions(shape)))
296
297def counted_lift(+shape: Shape.Shape, +values: List<&2, F32>,
298 decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>,
299 +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
300 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type, h: Filled(shape, values, 0n, Nil{}, P)) ->
301 P(Core.from_values_counted(shape, values, decision)):
302 match decision:
303 case Shape.BFalse{equal}:
304 Empty.absurd(P(Fail{Core.ValueCountMismatch{}}),
305 Nats.contradiction(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape)),
306 AllocationProof.natural_equal_true(List.length(&2, F32, values), Shape.elements(shape),
307 Equal.trans(Nat, List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape), counted,
308 Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape)))),
309 equal))
310 case Shape.BTrue{equal}:
311 Reads.new_lift(shape, 0.0, result => P(Core.from_values_new(shape, values, result)),
312 fill_lift(values, shape, 0n, Nil{}, start_room(shape, values, counted), P, h))
313
314def from_values_lift(+shape: Shape.Shape, +values: List<&2, F32>,
315 +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
316 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type, h: Filled(shape, values, 0n, Nil{}, P)) ->
317 P(Core.from_values(shape, values)):
318 counted_lift(shape, values, Shape.bool_case(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))), counted, P, h)
319
320def filled_length(+shape: Shape.Shape, +values: List<&2, F32>) ->
321 {Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}:
322 Equal.trans(Nat, Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))),
323 StorageLaws.size(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))), Shape.logical_numel(Shape.dimensions(shape)),
324 Equal.sym(Nat, StorageLaws.size(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))),
325 Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))),
326 Reads.size_is_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})))),
327 Equal.trans(Nat, StorageLaws.size(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))),
328 U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)),
329 StorageLaws.replay_size(Shape.count(shape), 0.0, writes(values, 0n), Conversion.shape_count_within(shape)),
330 Reads.count_exact(shape)))
331
332def filled_value(+shape: Shape.Shape, +values: List<&2, F32>,
333 +counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
334 +index: U32, +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
335 -fits: {Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
336 {Observation.point(shape, index, Done{Core.TTensor{StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits}}) ==
337 List.get(&2, F32, values, U32.to_nat(index)) : Maybe<&2, F32>}:
338 Equal.trans(Maybe<&2, F32>,
339 Observation.point(shape, index, Done{Core.TTensor{StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits}}),
340 Lifecycle.read_value(Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index)),
341 List.get(&2, F32, values, U32.to_nat(index)),
342 Core.read_result_value(shape, StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), fits, index,
343 Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index), {==}),
344 Equal.trans(Maybe<&2, F32>,
345 Lifecycle.read_value(Storage.get(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index)),
346 Some{StorageLaws.expected(writes(values, 0n), U32.to_nat(Shape.count(shape)), index, 0.0)},
347 List.get(&2, F32, values, U32.to_nat(index)),
348 Reads.stored_value(StorageLaws.replay(writes(values, 0n), base(shape, Nil{})), index,
349 StorageLaws.expected(writes(values, 0n), U32.to_nat(Shape.count(shape)), index, 0.0),
350 StorageLaws.replay_get(Shape.count(shape), 0.0, writes(values, 0n), index, Conversion.shape_count_within(shape),
351 Reads.word_inside(shape, index, inside))),
352 written_at(values, 0n, Shape.count(shape), index, 0.0, U32.to_nat(index), start_room(shape, values, counted), {==},
353 %Equal.sym(Nat, List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), counted) :
354 {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
355 inside)))
356
357def from_values_contract(+shape: Shape.Shape, +values: List<&2, F32>,
358 counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
359 Laws.FromValuesContract<shape, values>:
360 +counted = counted
361 Laws.FromValuesContract{
362 from_values_lift(shape, values, counted,
363 result => {Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, result) == True{} : Bool}, fits => {==}),
364 from_values_lift(shape, values, counted,
365 result => {Observation.dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}, fits => {==}),
366 from_values_lift(shape, values, counted,
367 result => {Allocation.tensor_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
368 fits => Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
369 Lifecycle.logical_length(StorageLaws.replay(writes(values, 0n), base(shape, Nil{}))), Shape.logical_numel(Shape.dimensions(shape)),
370 filled_length(shape, values))),
371 from_values_lift(shape, values, counted,
372 result => {Observation.count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>}, fits => {==}),
373 index => inside =>
374 +inside = inside
375 from_values_lift(shape, values, counted,
376 result => {Observation.point(shape, index, result) == List.get(&2, F32, values, U32.to_nat(index)) : Maybe<&2, F32>},
377 fits => filled_value(shape, values, counted, index, inside, fits))}