src/tensor/read_contract.bend
bendtorch-core@0.1.0.0 · 239 lines · 28 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/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/read_write_records.bend as Laws
15
16def count_exact(+shape: Shape.Shape) -> {U32.to_nat(Shape.count(shape)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}:
17 Equal.trans(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Conversion.shape_count_exact(shape), Shape.elements_exact(shape))
18
19def word_inside(+shape: Shape.Shape, +index: U32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
20 {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool}:
21 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), count_exact(shape)) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
22 inside
23
24def word_outside(+shape: Shape.Shape, +index: U32, outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) ->
25 {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == False{} : Bool}:
26 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), count_exact(shape)) : {Nat.is_lt(U32.to_nat(index), _) == False{} : Bool}
27 outside
28
29def created_size(+shape: Shape.Shape, +fill: F32) -> {StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)) == U32.to_nat(Shape.count(shape)) : Nat}:
30 StorageLaws.replay_size(Shape.count(shape), fill, [], Conversion.shape_count_within(shape))
31
32def size_is_length(storage: Storage.Storage) -> {StorageLaws.size(storage) == Lifecycle.logical_length(storage) : Nat}:
33 match storage:
34 case Storage.Empty{}:
35 {==}
36 case Storage.Owned{depth, length, array, balanced, valid}:
37 {==}
38
39def created_exact(+shape: Shape.Shape, +fill: F32) -> {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}:
40 Equal.trans(Nat, Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
41 Equal.sym(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), size_is_length(StorageLaws.created(Shape.count(shape), fill))),
42 Equal.trans(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), created_size(shape, fill), count_exact(shape)))
43
44def size_outside(+shape: Shape.Shape, +fill: F32, +index: U32, outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) ->
45 {Nat.is_lt(U32.to_nat(index), StorageLaws.size(StorageLaws.created(Shape.count(shape), fill))) == False{} : Bool}:
46 %Equal.sym(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), U32.to_nat(Shape.count(shape)), created_size(shape, fill)) : {Nat.is_lt(U32.to_nat(index), _) == False{} : Bool}
47 word_outside(shape, index, outside)
48
49def attached(+shape: Shape.Shape, -storage: Storage.Storage, +n: Nat, -exact: {Lifecycle.logical_length(storage) == n : Nat},
50 decision: Shape.BoolCase<Nat.is_eq(n, Shape.elements(shape))>, counted: {n == Shape.elements(shape) : Nat},
51 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type,
52 h: @-valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> P(Done{Core.TTensor{storage, valid}})) ->
53 P(Core.attach_decided(shape, storage, n, exact, decision)):
54 match decision:
55 case Shape.BFalse{no}:
56 Empty.absurd(P(Core.attach_decided(shape, storage, n, exact, Shape.BFalse{no})),
57 Nats.contradiction(Nat.is_eq(n, Shape.elements(shape)), AllocationProof.natural_equal_true(n, Shape.elements(shape), counted), no))
58 case Shape.BTrue{yes}:
59 h(Equal.trans(Nat, Lifecycle.logical_length(storage), n, Shape.logical_numel(Shape.dimensions(shape)), exact,
60 Equal.trans(Nat, n, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Lifecycle.natural_equal(n, Shape.elements(shape), yes), Shape.elements_exact(shape))))
61
62def attach_lift(+shape: Shape.Shape, storage: Storage.Storage, counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat},
63 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type,
64 h: @-valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> P(Done{Core.TTensor{storage, valid}})) ->
65 P(Core.attach(shape, storage)):
66 match storage:
67 case Storage.Empty{}:
68 attached(shape, Storage.Empty{}, 0n, {==}, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), counted, P, h)
69 case Storage.Owned{+depth, +length, array, balanced, valid}:
70 attached(shape, Storage.Owned{depth, length, array, balanced, valid}, length, {==},
71 Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))), counted, P, h)
72
73def result_lift(+shape: Shape.Shape, result: Result<&2, &1, Storage.Error, Storage.Storage>,
74 counted: {Allocation.storage_length(result) == Some{Shape.elements(shape)} : Maybe<&2, Nat>},
75 -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type,
76 h: @-valid: {Lifecycle.logical_length(StorageLaws.created.of(result)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
77 P(Done{Core.TTensor{StorageLaws.created.of(result), valid}})) ->
78 P(Core.new_result(shape, result)):
79 match result:
80 case Fail{error}:
81 Empty.absurd(P(Core.new_result(shape, Fail{error})),
82 Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.elements(shape)}, counted)))
83 case Done{storage}:
84 attach_lift(shape, storage,
85 Equal.cong(Maybe<&2, Nat>, Nat, value => Maybe.default(&2, Nat, value, 0n),
86 Some{Lifecycle.logical_length(storage)}, Some{Shape.elements(shape)}, counted), P, h)
87
88def new_lift(+shape: Shape.Shape, +fill: F32, -P: Result<&2, &1, Core.Error, Core.Tensor<shape>> -> Type,
89 h: @-valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> P(Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}})) -> P(Core.new(shape, fill)):
90 result_lift(shape, Storage.new(Shape.count(shape), fill),
91 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)},
92 AllocationProof.storage_new(Shape.count(shape), fill, Conversion.shape_count_within(shape)),
93 Equal.cong(Nat, Maybe<&2, Nat>, value => Some{value}, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape))),
94 P, h)
95
96def storage_value(result: Result<&2, &2, Storage.Error, F32>) -> Maybe<&2, F32>:
97 match result:
98 case Fail{error}:
99 None{}
100 case Done{value}:
101 Some{value}
102
103def storage_pair_value(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>) ->
104 {Lifecycle.read_value(pair) == storage_value(StorageLaws.outcome(Result<&2, &2, Storage.Error, F32>, pair)) : Maybe<&2, F32>}:
105 (storage, result) = pair
106 match result:
107 case Fail{error}:
108 {==}
109 case Done{value}:
110 {==}
111
112def stored_value(storage: Storage.Storage, +other: U32, -expected: F32,
113 read: {StorageLaws.read(storage, other) == Done{expected} : Result<&2, &2, Storage.Error, F32>}) ->
114 {Lifecycle.read_value(Storage.get(storage, other)) == Some{expected} : Maybe<&2, F32>}:
115 Equal.trans(Maybe<&2, F32>, Lifecycle.read_value(Storage.get(storage, other)), storage_value(StorageLaws.read(storage, other)), Some{expected},
116 storage_pair_value(Storage.get(storage, other)),
117 Equal.cong(Result<&2, &2, Storage.Error, F32>, Maybe<&2, F32>, storage_value, StorageLaws.read(storage, other), Done{expected}, read))
118
119def read_code_projection(-shape: Shape.Shape, -original: Storage.Storage,
120 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
121 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
122 {Observation.read_code_pair(shape, Core.read_result(shape, original, valid, index, pair, same)) ==
123 Observation.read_status(Core.storage_read_error(StorageLaws.outcome(Result<&2, &2, Storage.Error, F32>, pair))) : U32}:
124 (storage, result) = pair
125 {==}
126
127def read_code_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, -expected: Result<&2, &2, Storage.Error, F32>,
128 read: {StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index) == expected : Result<&2, &2, Storage.Error, F32>}) ->
129 {Observation.read_code(shape, index, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Observation.read_status(Core.storage_read_error(expected))} : Maybe<&2, U32>}:
130 Equal.cong(U32, Maybe<&2, U32>, code => Some{code},
131 Observation.read_code_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})),
132 Observation.read_status(Core.storage_read_error(expected)),
133 Equal.trans(U32, Observation.read_code_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})),
134 Observation.read_status(Core.storage_read_error(StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index))), Observation.read_status(Core.storage_read_error(expected)),
135 read_code_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}),
136 Equal.cong(Result<&2, &2, Storage.Error, F32>, U32, result => Observation.read_status(Core.storage_read_error(result)), StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index), expected, read)))
137
138def read_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
139 {Observation.after_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
140 (tensor, result) = pair
141 {==}
142
143def read_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
144 {Observation.after_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
145 (tensor, result) = pair
146 {==}
147
148def read_length_projection(-shape: Shape.Shape, -original: Storage.Storage,
149 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
150 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
151 {Observation.after_length_pair(shape, Core.read_result(shape, original, valid, index, pair, same)) == Lifecycle.retained_read(pair) : Nat}:
152 (storage, result) = pair
153 {==}
154
155def read_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32) ->
156 {Observation.after_length(shape, index, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
157 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
158 Observation.after_length_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})), Shape.logical_numel(Shape.dimensions(shape)),
159 Equal.trans(Nat, Observation.after_length_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})),
160 Lifecycle.retained_read(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)), Shape.logical_numel(Shape.dimensions(shape)),
161 read_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}),
162 Equal.trans(Nat, Lifecycle.retained_read(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
163 Lifecycle.get_length(StorageLaws.created(Shape.count(shape), fill), index), created_exact(shape, fill))))
164
165def read_value_projection(-shape: Shape.Shape, -original: Storage.Storage,
166 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +other: U32,
167 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
168 {Observation.after_value_pair(shape, other, Core.read_result(shape, original, valid, index, pair, same)) ==
169 Lifecycle.read_value(Storage.get(StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, pair), other)) : Maybe<&2, F32>}:
170 (storage, result) = pair
171 Core.read_result_value(shape, storage,
172 Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
173 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, (storage, result), Storage.get(original, index), same) :
174 {Lifecycle.retained_read(_) == Lifecycle.logical_length(original) : Nat}
175 Lifecycle.get_length(original, index), valid),
176 other, Storage.get(storage, other), {==})
177
178def read_after_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
179 {Observation.after_value(shape, index, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
180 Equal.trans(Maybe<&2, F32>,
181 Observation.after_value_pair(shape, other, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})),
182 Lifecycle.read_value(Storage.get(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other)), Some{fill},
183 read_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, other, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}),
184 stored_value(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other, fill,
185 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Read{index}], other, Conversion.shape_count_within(shape), word_inside(shape, other, inside))))
186
187def read_point_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
188 {Observation.point(shape, index, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
189 Equal.trans(Maybe<&2, F32>,
190 Core.read_value(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})),
191 Lifecycle.read_value(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)), Some{fill},
192 Core.read_result_value(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}),
193 stored_value(StorageLaws.created(Shape.count(shape), fill), index, fill,
194 StorageLaws.replay_get(Shape.count(shape), fill, [], index, Conversion.shape_count_within(shape), word_inside(shape, index, inside))))
195
196def read_contract(+shape: Shape.Shape, +fill: F32, +index: U32, -expected: Result<&2, &2, Storage.Error, F32>,
197 read: {StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index) == expected : Result<&2, &2, Storage.Error, F32>}) ->
198 Laws.ReadContract<shape, fill, index, Observation.read_status(Core.storage_read_error(expected))>:
199 Laws.ReadContract{
200 new_lift(shape, fill, result => {Observation.read_code(shape, index, result) == Some{Observation.read_status(Core.storage_read_error(expected))} : Maybe<&2, U32>},
201 valid => read_code_done(shape, fill, valid, index, expected, read)),
202 new_lift(shape, fill, result => {Observation.after_dimensions(shape, index, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
203 valid => read_dimensions_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))),
204 new_lift(shape, fill, result => {Observation.after_length(shape, index, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
205 valid => read_length_done(shape, fill, valid, index)),
206 new_lift(shape, fill, result => {Observation.after_count(shape, index, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
207 valid => read_count_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))),
208 other => inside => new_lift(shape, fill, result => {Observation.after_value(shape, index, other, result) == Some{fill} : Maybe<&2, F32>},
209 valid => read_after_done(shape, fill, valid, index, other, inside))}
210
211def dynamic_point_result(+shape: Shape.Shape, +index: U32, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
212 {Observation.dynamic_point(shape, index, result) == Observation.point(shape, index, result) : Maybe<&2, F32>}:
213 match result:
214 case Fail{error}:
215 {==}
216 case Done{tensor}:
217 Core.dynamic_result_value(shape, Core.read_flat(shape, tensor, index))
218
219def read_inside(+shape: Shape.Shape, +fill: F32, +index: U32,
220 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.ReadInside<shape, fill, index>:
221 +inside = inside
222 Laws.ReadInside{
223 read_contract(shape, fill, index, Done{fill},
224 StorageLaws.replay_get(Shape.count(shape), fill, [], index, Conversion.shape_count_within(shape), word_inside(shape, index, inside))),
225 new_lift(shape, fill, result => {Observation.point(shape, index, result) == Some{fill} : Maybe<&2, F32>},
226 valid => read_point_done(shape, fill, valid, index, inside))}
227
228def read_outside(+shape: Shape.Shape, +fill: F32, +index: U32,
229 outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) -> Laws.ReadContract<shape, fill, index, 8>:
230 read_contract(shape, fill, index, Fail{Storage.OutOfBounds{}},
231 StorageLaws.get_outside(StorageLaws.created(Shape.count(shape), fill), index, size_outside(shape, fill, index, outside)))
232
233def dynamic_read_inside(+shape: Shape.Shape, +fill: F32, +index: U32,
234 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
235 {Observation.dynamic_point(shape, index, Core.new(shape, fill)) == Some{fill} : Maybe<&2, F32>}:
236 Equal.trans(Maybe<&2, F32>, Observation.dynamic_point(shape, index, Core.new(shape, fill)), Observation.point(shape, index, Core.new(shape, fill)), Some{fill},
237 dynamic_point_result(shape, index, Core.new(shape, fill)),
238 new_lift(shape, fill, result => {Observation.point(shape, index, result) == Some{fill} : Maybe<&2, F32>},
239 valid => read_point_done(shape, fill, valid, index, inside)))