src/tensor/write_contract.bend
bendtorch-core@0.1.0.0 · 230 lines · 23 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
15import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
16
17def write_value_projection(-shape: Shape.Shape, -original: Storage.Storage,
18 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32,
19 pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>, -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
20 {Observation.written_value_pair(shape, other, Core.write_result(shape, original, valid, index, value, pair, same)) ==
21 Lifecycle.read_value(Storage.get(StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, pair), other)) : Maybe<&2, F32>}:
22 (storage, result) = pair
23 Core.read_result_value(shape, storage,
24 Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
25 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, (storage, result), Storage.set(original, index, value), same) :
26 {Lifecycle.retained_write(_) == Lifecycle.logical_length(original) : Nat}
27 Lifecycle.set_length(original, index, value), valid),
28 other, Storage.get(storage, other), {==})
29
30def written_pick(+shape: Shape.Shape, +index: U32, +value: F32, +other: U32, +fill: F32) -> F32:
31 Bool.pick(F32, Bool.and(Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), Nat.is_eq(U32.to_nat(index), U32.to_nat(other))), value, fill)
32
33def write_value_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, +value: F32, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
34 {Observation.written_value(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{written_pick(shape, index, value, other, fill)} : Maybe<&2, F32>}:
35 Equal.trans(Maybe<&2, F32>,
36 Observation.written_value_pair(shape, other, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
37 Lifecycle.read_value(Storage.get(StorageLaws.written(StorageLaws.created(Shape.count(shape), fill), index, value), other)), Some{written_pick(shape, index, value, other, fill)},
38 write_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, other, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==}),
39 Reads.stored_value(StorageLaws.written(StorageLaws.created(Shape.count(shape), fill), index, value), other, written_pick(shape, index, value, other, fill),
40 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Write{index, value}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
41
42def write_code_projection(-shape: Shape.Shape, -original: Storage.Storage,
43 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
44 pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>, -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
45 {Observation.write_code_pair(shape, Core.write_result(shape, original, valid, index, value, pair, same)) ==
46 Observation.write_status(Core.storage_write_error(StorageLaws.outcome(Result<&2, &2, Storage.Error, Unit>, pair))) : U32}:
47 (storage, result) = pair
48 {==}
49
50def write_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, +value: F32, -expected: Result<&2, &2, Storage.Error, Unit>,
51 status: {StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value) == expected : Result<&2, &2, Storage.Error, Unit>}) ->
52 {Observation.write_code(shape, index, value, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Observation.write_status(Core.storage_write_error(expected))} : Maybe<&2, U32>}:
53 Equal.cong(U32, Maybe<&2, U32>, code => Some{code},
54 Observation.write_code_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
55 Observation.write_status(Core.storage_write_error(expected)),
56 Equal.trans(U32, Observation.write_code_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
57 Observation.write_status(Core.storage_write_error(StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value))), Observation.write_status(Core.storage_write_error(expected)),
58 write_code_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==}),
59 Equal.cong(Result<&2, &2, Storage.Error, Unit>, U32, result => Observation.write_status(Core.storage_write_error(result)), StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value), expected, status)))
60
61def written_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
62 {Observation.written_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
63 (tensor, result) = pair
64 {==}
65
66def written_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
67 {Observation.written_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
68 (tensor, result) = pair
69 {==}
70
71def write_length_projection(-shape: Shape.Shape, -original: Storage.Storage,
72 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
73 pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>, -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
74 {Observation.written_length_pair(shape, Core.write_result(shape, original, valid, index, value, pair, same)) == Lifecycle.retained_write(pair) : Nat}:
75 (storage, result) = pair
76 {==}
77
78def write_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, +value: F32) ->
79 {Observation.written_length(shape, index, value, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
80 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
81 Observation.written_length_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})), Shape.logical_numel(Shape.dimensions(shape)),
82 Equal.trans(Nat, Observation.written_length_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
83 Lifecycle.retained_write(Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value)), Shape.logical_numel(Shape.dimensions(shape)),
84 write_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==}),
85 Equal.trans(Nat, Lifecycle.retained_write(Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value)), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
86 Lifecycle.set_length(StorageLaws.created(Shape.count(shape), fill), index, value), Reads.created_exact(shape, fill))))
87
88def pick_hit(+shape: Shape.Shape, +index: U32, +value: F32, +fill: F32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
89 {written_pick(shape, index, value, index, fill) == value : F32}:
90 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), True{}, Reads.word_inside(shape, index, inside)) :
91 {Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(index), U32.to_nat(index))), value, fill) == value : F32}
92 %Equal.sym(Bool, Nat.is_eq(U32.to_nat(index), U32.to_nat(index)), True{}, Arith.eq_refl(U32.to_nat(index))) :
93 {Bool.pick(F32, _, value, fill) == value : F32}
94 {==}
95
96def pick_frame(+shape: Shape.Shape, +index: U32, +value: F32, +other: U32, +fill: F32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
97 different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}) ->
98 {written_pick(shape, index, value, other, fill) == fill : F32}:
99 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), True{}, Reads.word_inside(shape, index, inside)) :
100 {Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(index), U32.to_nat(other))), value, fill) == fill : F32}
101 %Equal.sym(Bool, Nat.is_eq(U32.to_nat(index), U32.to_nat(other)), False{}, different) :
102 {Bool.pick(F32, _, value, fill) == fill : F32}
103 {==}
104
105def pick_outside(+shape: Shape.Shape, +index: U32, +value: F32, +other: U32, +fill: F32, outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) ->
106 {written_pick(shape, index, value, other, fill) == fill : F32}:
107 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), False{}, Reads.word_outside(shape, index, outside)) :
108 {Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(index), U32.to_nat(other))), value, fill) == fill : F32}
109 {==}
110
111def written_value(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32, +other: U32, -expected: F32,
112 inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}, picked: {written_pick(shape, index, value, other, fill) == expected : F32}) ->
113 {Observation.written_value(shape, index, value, other, Core.new(shape, fill)) == Some{expected} : Maybe<&2, F32>}:
114 Reads.new_lift(shape, fill, result => {Observation.written_value(shape, index, value, other, result) == Some{expected} : Maybe<&2, F32>},
115 valid => Equal.trans(Maybe<&2, F32>, Observation.written_value(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}),
116 Some{written_pick(shape, index, value, other, fill)}, Some{expected},
117 write_value_done(shape, fill, valid, index, value, other, inside),
118 Equal.cong(F32, Maybe<&2, F32>, number => Some{number}, written_pick(shape, index, value, other, fill), expected, picked)))
119
120def write_contract(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32, -expected: Result<&2, &2, Storage.Error, Unit>,
121 status: {StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value) == expected : Result<&2, &2, Storage.Error, Unit>}) ->
122 Laws.WriteContract<shape, fill, index, value, Observation.write_status(Core.storage_write_error(expected))>:
123 Laws.WriteContract{
124 Reads.new_lift(shape, fill, result => {Observation.write_code(shape, index, value, result) == Some{Observation.write_status(Core.storage_write_error(expected))} : Maybe<&2, U32>},
125 valid => write_code_done(shape, fill, valid, index, value, expected, status)),
126 Reads.new_lift(shape, fill, result => {Observation.written_dimensions(shape, index, value, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
127 valid => written_dimensions_pair(shape, Core.write_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index, value))),
128 Reads.new_lift(shape, fill, result => {Observation.written_length(shape, index, value, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
129 valid => write_length_done(shape, fill, valid, index, value)),
130 Reads.new_lift(shape, fill, result => {Observation.written_count(shape, index, value, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
131 valid => written_count_pair(shape, Core.write_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index, value)))}
132
133def located_index(-shape: Shape.Shape, +index: Shape.FlatIndex<shape>, +expected: U32,
134 located: {Observation.coordinate_index(shape, Done{index}) == Some{expected} : Maybe<&2, U32>}) ->
135 {Shape.index_value(shape, index) == expected : U32}:
136 Equal.cong(Maybe<&2, U32>, U32, word => Maybe.default(&2, U32, word, 0), Some{Shape.index_value(shape, index)}, Some{expected}, located)
137
138def coordinate_read_flat(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
139 +index: U32, located: {Observation.coordinate_index(shape, result) == Some{index} : Maybe<&2, U32>}) ->
140 {Core.read_coordinate_result(shape, tensor, result) == Core.read_flat(shape, tensor, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>}:
141 match result:
142 case Fail{error}:
143 Empty.absurd({(tensor, Fail{Core.ShapeError{error}}) == Core.read_flat(shape, tensor, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>},
144 Arith.clash(Equal.cong(Maybe<&2, U32>, Bool, word => Maybe.is_some(&2, U32, word), None{}, Some{index}, located)))
145 case Done{+flat}:
146 Equal.cong(U32, Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, word => Core.read_flat(shape, tensor, word),
147 Shape.index_value(shape, flat), index, located_index(shape, flat, index, located))
148
149def coordinate_write_flat(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, -value: F32,
150 result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
151 +index: U32, located: {Observation.coordinate_index(shape, result) == Some{index} : Maybe<&2, U32>}) ->
152 {Core.write_coordinate_result(shape, tensor, value, result) == Core.write_flat(shape, tensor, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>}:
153 match result:
154 case Fail{error}:
155 Empty.absurd({(tensor, Fail{Core.ShapeError{error}}) == Core.write_flat(shape, tensor, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
156 Arith.clash(Equal.cong(Maybe<&2, U32>, Bool, word => Maybe.is_some(&2, U32, word), None{}, Some{index}, located)))
157 case Done{+flat}:
158 Equal.cong(U32, Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, word => Core.write_flat(shape, tensor, word, value),
159 Shape.index_value(shape, flat), index, located_index(shape, flat, index, located))
160
161def coordinate_value_pair(+shape: Shape.Shape, +coordinates: List<&2, U32>, +index: U32,
162 located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
163 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
164 {Observation.coordinate_value_pair(shape, coordinates, pair) == Observation.written_value_pair(shape, index, pair) : Maybe<&2, F32>}:
165 (tensor, result) = pair
166 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, read => Core.read_value(shape, read),
167 Core.read_coordinate(shape, tensor, coordinates), Core.read_flat(shape, tensor, index),
168 coordinate_read_flat(shape, tensor, Shape.flatten_checked(shape, coordinates), index, located))
169
170def coordinate_value_result(+shape: Shape.Shape, +coordinates: List<&2, U32>, +index: U32, +value: F32,
171 located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
172 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
173 {Observation.coordinate_value(shape, index, value, coordinates, result) == Observation.written_value(shape, index, value, index, result) : Maybe<&2, F32>}:
174 match result:
175 case Fail{error}:
176 {==}
177 case Done{tensor}:
178 coordinate_value_pair(shape, coordinates, index, located, Core.write_flat(shape, tensor, index, value))
179
180def coordinate_written_result(+shape: Shape.Shape, +coordinates: List<&2, U32>, +index: U32, +value: F32, +other: U32,
181 located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
182 result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
183 {Observation.coordinate_written(shape, coordinates, value, other, result) == Observation.written_value(shape, index, value, other, result) : Maybe<&2, F32>}:
184 match result:
185 case Fail{error}:
186 {==}
187 case Done{tensor}:
188 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, Maybe<&2, F32>, pair => Observation.written_value_pair(shape, other, pair),
189 Core.write_coordinate(shape, tensor, coordinates, value), Core.write_flat(shape, tensor, index, value),
190 coordinate_write_flat(shape, tensor, value, Shape.flatten_checked(shape, coordinates), index, located))
191
192def write_inside(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32,
193 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.WriteInside<shape, fill, index, value>:
194 +inside = inside
195 Laws.WriteInside{
196 write_contract(shape, fill, index, value, Done{Unit{}},
197 StorageLaws.replay_set(Shape.count(shape), fill, [], index, value, Conversion.shape_count_within(shape), Reads.word_inside(shape, index, inside))),
198 written_value(shape, fill, index, value, index, value, inside, pick_hit(shape, index, value, fill, inside)),
199 other => inside_other => different =>
200 written_value(shape, fill, index, value, other, fill, inside_other, pick_frame(shape, index, value, other, fill, inside, different))}
201
202def write_outside(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32,
203 outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) -> Laws.WriteOutside<shape, fill, index, value>:
204 +outside = outside
205 Laws.WriteOutside{
206 write_contract(shape, fill, index, value, Fail{Storage.OutOfBounds{}},
207 StorageLaws.set_outside(StorageLaws.created(Shape.count(shape), fill), index, value, Reads.size_outside(shape, fill, index, outside))),
208 other => inside =>
209 written_value(shape, fill, index, value, other, fill, inside, pick_outside(shape, index, value, other, fill, outside))}
210
211def coordinate_inside(+shape: Shape.Shape, +fill: F32, +coordinates: List<&2, U32>, +index: U32, +value: F32,
212 located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
213 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
214 Laws.CoordinateInside<shape, fill, coordinates, index, value>:
215 +located = located
216 +inside = inside
217 Laws.CoordinateInside{
218 Equal.trans(Maybe<&2, F32>, Observation.coordinate_value(shape, index, value, coordinates, Core.new(shape, fill)),
219 Observation.written_value(shape, index, value, index, Core.new(shape, fill)), Some{value},
220 coordinate_value_result(shape, coordinates, index, value, located, Core.new(shape, fill)),
221 written_value(shape, fill, index, value, index, value, inside, pick_hit(shape, index, value, fill, inside))),
222 Equal.trans(Maybe<&2, F32>, Observation.coordinate_written(shape, coordinates, value, index, Core.new(shape, fill)),
223 Observation.written_value(shape, index, value, index, Core.new(shape, fill)), Some{value},
224 coordinate_written_result(shape, coordinates, index, value, index, located, Core.new(shape, fill)),
225 written_value(shape, fill, index, value, index, value, inside, pick_hit(shape, index, value, fill, inside))),
226 other => inside_other => different =>
227 Equal.trans(Maybe<&2, F32>, Observation.coordinate_written(shape, coordinates, value, other, Core.new(shape, fill)),
228 Observation.written_value(shape, index, value, other, Core.new(shape, fill)), Some{fill},
229 coordinate_written_result(shape, coordinates, index, value, other, located, Core.new(shape, fill)),
230 written_value(shape, fill, index, value, other, fill, inside_other, pick_frame(shape, index, value, other, fill, inside, different)))}