src/tensor/contracts/binary_storage_proof.bend
bendtorch-core@0.1.0.0 · 287 lines · 12 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
4import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
5import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
6import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
7import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
8import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
9import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
10import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as Build
11
12
13
14
15
16
17
18def pair_eq(-A: Type, -B: Type, -a: A, -b: A, -c: B, -e: B, x: {a == b : A}, y: {c == e : B}) -> {(a, c) == (b, e) : A & B}:
19 %x : {(a, c) == (_, e) : A & B}
20 %y : {(a, c) == (a, _) : A & B}
21 {==}
22
23def balanced_unique(+d: Nat, array: Array<F32>, p: Model.Balanced(F32, d, array), q: Model.Balanced(F32, d, array)) ->
24 {p == q : Model.Balanced(F32, d, array)}:
25 match d array:
26 case 0n ALeaf{x}:
27 match p q:
28 case Unit{} Unit{}:
29 {==}
30 case 0n ANode{xs, ys}:
31 match p:
32 case 1n+k ALeaf{x}:
33 match p:
34 case 1n+k ANode{xs, ys}:
35 (p1, p2) = p
36 (q1, q2) = q
37 pair_eq(Model.Balanced(F32, k, xs), Model.Balanced(F32, k, ys), p1, q1, p2, q2,
38 balanced_unique(k, xs, p1, q1), balanced_unique(k, ys, p2, q2))
39
40def owned_eq(+d: Nat, +n: Nat, array: Array<F32>, -other: Array<F32>, e: {array == other : Array<F32>},
41 p: Model.Balanced(F32, d, array), -f: {Storage.bounds(d, n) == True{} : Bool}) ->
42 @q: Model.Balanced(F32, d, other) -> {Storage.Owned{d, n, array, p, f} == Storage.Owned{d, n, other, q, f} : Storage.Storage}:
43 %e : (@q: Model.Balanced(F32, d, _) -> {Storage.Owned{d, n, array, p, f} == Storage.Owned{d, n, _, q, f} : Storage.Storage})
44 q => Equal.cong(Model.Balanced(F32, d, array), Storage.Storage, r => Storage.Owned{d, n, array, r, f}, p, q, balanced_unique(d, array, p, q))
45
46
47
48
49def norm(+n: Nat, +ops: List<&2, StorageLaws.Op>, +history: List<&2, Api.Effect>) -> List<&2, Api.Effect>:
50 match ops:
51 case Nil{}:
52 history
53 case +op <> +later:
54 match op:
55 case StorageLaws.Write{+i, +w}:
56 Bool.pick(List<&2, Api.Effect>, Nat.is_lt(U32.to_nat(i), n), norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history))
57 case StorageLaws.Read{+i}:
58 Bool.pick(List<&2, Api.Effect>, Nat.is_lt(U32.to_nat(i), n), norm(n, later, Api.Kept{i} <> history), norm(n, later, history))
59 case StorageLaws.First{}:
60 norm(n, later, Api.Left{} <> history)
61 case StorageLaws.Second{}:
62 norm(n, later, Api.Right{} <> history)
63 case StorageLaws.Length{}:
64 norm(n, later, history)
65
66def norm_current(+n: Nat, +ops: List<&2, StorageLaws.Op>, +history: List<&2, Api.Effect>, +j: U32, +fill: F32,
67 hit: Bool, +dhit: {hit == Api.hit_of(n, ops) : Bool}) ->
68 {Api.current(norm(n, ops, history), j, fill) == StorageLaws.expected(ops, n, j, Api.current(history, j, fill)) : F32}:
69 match ops:
70 case Nil{}:
71 {==}
72 case +op <> +later:
73 match op:
74 case StorageLaws.Write{+i, +w}:
75 match hit:
76 case True{}:
77 %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), j, fill) ==
78 StorageLaws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, Api.current(history, j, fill))) : F32}
79 norm_current(n, later, Api.Wrote{i, w} <> history, j, fill, Api.hit_of(n, later), {==})
80 case False{}:
81 %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), j, fill) ==
82 StorageLaws.expected(later, n, j, Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), w, Api.current(history, j, fill))) : F32}
83 norm_current(n, later, history, j, fill, Api.hit_of(n, later), {==})
84 case StorageLaws.Read{+i}:
85 match hit:
86 case True{}:
87 %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), j, fill) ==
88 StorageLaws.expected(later, n, j, Api.current(history, j, fill)) : F32}
89 norm_current(n, later, Api.Kept{i} <> history, j, fill, Api.hit_of(n, later), {==})
90 case False{}:
91 %dhit : {Api.current(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), j, fill) ==
92 StorageLaws.expected(later, n, j, Api.current(history, j, fill)) : F32}
93 norm_current(n, later, history, j, fill, Api.hit_of(n, later), {==})
94 case StorageLaws.First{}:
95 norm_current(n, later, Api.Left{} <> history, j, fill, Api.hit_of(n, later), {==})
96 case StorageLaws.Second{}:
97 norm_current(n, later, Api.Right{} <> history, j, fill, Api.hit_of(n, later), {==})
98 case StorageLaws.Length{}:
99 norm_current(n, later, history, j, fill, Api.hit_of(n, later), {==})
100
101def norm_written(+n: Nat, +ops: List<&2, StorageLaws.Op>, +history: List<&2, Api.Effect>, hit: Bool, +dhit: {hit == Api.hit_of(n, ops) : Bool},
102 +all: {Build.written(n, history) == True{} : Bool}) -> {Build.written(n, norm(n, ops, history)) == True{} : Bool}:
103 match ops:
104 case Nil{}:
105 all
106 case +op <> +later:
107 match op:
108 case StorageLaws.Write{+i, +w}:
109 match hit:
110 case True{}:
111 %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history))) == True{} : Bool}
112 norm_written(n, later, Api.Wrote{i, w} <> history, Api.hit_of(n, later), {==},
113 %dhit : {Bool.and(_, Build.written(n, history)) == True{} : Bool}
114 all)
115 case False{}:
116 %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history))) == True{} : Bool}
117 norm_written(n, later, history, Api.hit_of(n, later), {==}, all)
118 case StorageLaws.Read{+i}:
119 match hit:
120 case True{}:
121 %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history))) == True{} : Bool}
122 norm_written(n, later, Api.Kept{i} <> history, Api.hit_of(n, later), {==}, all)
123 case False{}:
124 %dhit : {Build.written(n, Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history))) == True{} : Bool}
125 norm_written(n, later, history, Api.hit_of(n, later), {==}, all)
126 case StorageLaws.First{}:
127 norm_written(n, later, Api.Left{} <> history, Api.hit_of(n, later), {==}, all)
128 case StorageLaws.Second{}:
129 norm_written(n, later, Api.Right{} <> history, Api.hit_of(n, later), {==}, all)
130 case StorageLaws.Length{}:
131 norm_written(n, later, history, Api.hit_of(n, later), {==}, all)
132
133
134
135def replay_lift(+rest: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, +fill: F32, +history: List<&2, Api.Effect>,
136 hit: Bool, +dhit: {hit == Api.hit_of(n, rest) : Bool},
137 -b: Model.Balanced(F32, d, Api.arr(history, d, fill)), -f: {Storage.bounds(d, n) == True{} : Bool},
138 +fits: {Storage.bounds(d, n) == True{} : Bool}, -Q: Storage.Storage -> Type,
139 h: @-c: Model.Balanced(F32, d, Api.arr(norm(n, rest, history), d, fill)) ->
140 Q(Storage.Owned{d, n, Api.arr(norm(n, rest, history), d, fill), c, f})) ->
141 Q(StorageLaws.replay(rest, Storage.Owned{d, n, Api.arr(history, d, fill), b, f})):
142 match rest:
143 case Nil{}:
144 h(b)
145 case +op <> +later:
146 match op:
147 case StorageLaws.Write{+i, +w}:
148 match hit:
149 case True{}:
150 +inside = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
151 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
152 Storage.set_checked(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
153 (Storage.Owned{d, n, Array.set(F32, Api.arr(history, d, fill), i, w),
154 Certificates.set_result(F32, d, Api.arr(history, d, fill), i, w, Array.set(F32, Api.arr(history, d, fill), i, w), {==}, b), f}, Done{Unit{}}),
155 Api.set_checked_hit(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside)) :
156 Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _)))
157 replay_lift(later, d, n, fill, Api.Wrote{i, w} <> history, Api.hit_of(n, later), {==},
158 Certificates.set_result(F32, d, Api.arr(history, d, fill), i, w, Array.set(F32, Api.arr(history, d, fill), i, w), {==}, b), f, fits, Q,
159 %Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
160 (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill)) ->
161 Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill), c, f}))
162 h)
163 case False{}:
164 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
165 Storage.set_checked(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
166 (Storage.Owned{d, n, Api.arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}),
167 Api.set_checked_miss(d, n, Api.arr(history, d, fill), i, w, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
168 Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _)))
169 replay_lift(later, d, n, fill, history, Api.hit_of(n, later), {==}, b, f, fits, Q,
170 %Equal.sym(Bool, False{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
171 (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill)) ->
172 Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Wrote{i, w} <> history), norm(n, later, history)), d, fill), c, f}))
173 h)
174 case StorageLaws.Read{+i}:
175 match hit:
176 case True{}:
177 +inside = Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit)
178 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>,
179 Storage.get_checked(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
180 (Storage.Owned{d, n, Refinement.first(F32, Array.get(F32, Api.arr(history, d, fill), i)),
181 Certificates.get_result(F32, d, Api.arr(history, d, fill), i, Array.get(F32, Api.arr(history, d, fill), i), {==}, b), f},
182 Done{Refinement.second(F32, Array.get(F32, Api.arr(history, d, fill), i))}),
183 Api.get_checked_keep(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit, fits, inside)) :
184 Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, _)))
185 replay_lift(later, d, n, fill, Api.Kept{i} <> history, Api.hit_of(n, later), {==},
186 Certificates.get_result(F32, d, Api.arr(history, d, fill), i, Array.get(F32, Api.arr(history, d, fill), i), {==}, b), f, fits, Q,
187 %Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
188 (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill)) ->
189 Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill), c, f}))
190 h)
191 case False{}:
192 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>,
193 Storage.get_checked(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f),
194 (Storage.Owned{d, n, Api.arr(history, d, fill), b, f}, Fail{Storage.OutOfBounds{}}),
195 Api.get_checked_stay(d, n, Api.arr(history, d, fill), i, Nat.is_lt(U32.to_nat(i), n), {==}, b, f, dhit)) :
196 Q(StorageLaws.replay(later, StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, _)))
197 replay_lift(later, d, n, fill, history, Api.hit_of(n, later), {==}, b, f, fits, Q,
198 %Equal.sym(Bool, False{}, Nat.is_lt(U32.to_nat(i), n), dhit) :
199 (@-c: Model.Balanced(F32, d, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill)) ->
200 Q(Storage.Owned{d, n, Api.arr(Bool.pick(List<&2, Api.Effect>, _, norm(n, later, Api.Kept{i} <> history), norm(n, later, history)), d, fill), c, f}))
201 h)
202 case StorageLaws.First{}:
203 %Equal.sym(Storage.Storage & Storage.Storage,
204 Storage.finish_clone(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f),
205 (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
206 Certificates.clone_first(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f},
207 Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
208 Certificates.clone_second(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f}),
209 Api.finish_pair(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f)) :
210 Q(StorageLaws.replay(later, StorageLaws.owner(Storage.Storage, _)))
211 replay_lift(later, d, n, fill, Api.Left{} <> history, Api.hit_of(n, later), {==},
212 Certificates.clone_first(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f, fits, Q, h)
213 case StorageLaws.Second{}:
214 %Equal.sym(Storage.Storage & Storage.Storage,
215 Storage.finish_clone(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f),
216 (Storage.Owned{d, n, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
217 Certificates.clone_first(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f},
218 Storage.Owned{d, n, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(history, d, fill))),
219 Certificates.clone_second(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f}),
220 Api.finish_pair(d, n, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b, f)) :
221 Q(StorageLaws.replay(later, StorageLaws.outcome(Storage.Storage, _)))
222 replay_lift(later, d, n, fill, Api.Right{} <> history, Api.hit_of(n, later), {==},
223 Certificates.clone_second(F32, d, Api.arr(history, d, fill), Array.clone(F32, Api.arr(history, d, fill)), {==}, b), f, fits, Q, h)
224 case StorageLaws.Length{}:
225 replay_lift(later, d, n, fill, history, Api.hit_of(n, later), {==}, b, f, fits, Q, h)
226
227def replay_empty(+ops: List<&2, StorageLaws.Op>) -> {StorageLaws.replay(ops, Storage.Empty{}) == Storage.Empty{} : Storage.Storage}:
228 match ops:
229 case Nil{}:
230 {==}
231 case +op <> +later:
232 match op:
233 case StorageLaws.Write{+i, +w}:
234 replay_empty(later)
235 case StorageLaws.Read{+i}:
236 replay_empty(later)
237 case StorageLaws.First{}:
238 replay_empty(later)
239 case StorageLaws.Second{}:
240 replay_empty(later)
241 case StorageLaws.Length{}:
242 replay_empty(later)
243
244def created_alloc(+d: Nat, +n: Nat, +fill: F32, valid: Bool, -decision: {valid == Storage.bounds(d, n) : Bool},
245 +yes: {True{} == valid : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, -Q: Storage.Storage -> Type,
246 owned: @+d: Nat -> @+fits: {Storage.bounds(d, n) == True{} : Bool} -> @-f: {Storage.bounds(d, n) == True{} : Bool} ->
247 Q(Storage.Owned{d, n, Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
248 Q(StorageLaws.created.of(Storage.allocate(d, n, fill, valid, decision))):
249 match valid:
250 case True{}:
251 owned(d, fits, Equal.sym(Bool, True{}, Storage.bounds(d, n), decision))
252 case False{}:
253 Empty.absurd(Q(StorageLaws.created.of(Storage.allocate(d, n, fill, False{}, decision))), Arith.clash_true(yes))
254
255def created_meta(+n: Nat, +fill: F32, metadata: Nat & Nat,
256 +fits: {Storage.bounds(Pair.fst(Nat, Nat, metadata), n) == True{} : Bool}, -Q: Storage.Storage -> Type,
257 owned: @+d: Nat -> @+fits: {Storage.bounds(d, n) == True{} : Bool} -> @-f: {Storage.bounds(d, n) == True{} : Bool} ->
258 Q(Storage.Owned{d, n, Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
259 Q(StorageLaws.created.of(Storage.allocate_at(n, fill, metadata))):
260 (+d, +capacity) = metadata
261 created_alloc(d, n, fill, Storage.bounds(d, n), {==}, Equal.sym(Bool, Storage.bounds(d, n), True{}, fits), fits, Q, owned)
262
263def created_checked(+n: Nat, +fill: F32, allowed: Bool, +yes: {True{} == allowed : Bool},
264 +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, -Q: Storage.Storage -> Type,
265 empty: @zero: {n == 0n : Nat} -> Q(Storage.Empty{}),
266 owned: @+d: Nat -> @+fits: {Storage.bounds(d, n) == True{} : Bool} -> @-f: {Storage.bounds(d, n) == True{} : Bool} ->
267 Q(Storage.Owned{d, n, Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
268 Q(StorageLaws.created.of(Storage.new_checked(n, fill, allowed))):
269 match n:
270 case 0n:
271 empty({==})
272 case 1n+p:
273 match allowed:
274 case True{}:
275 created_meta(1n+p, fill, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), Api.seek(1n+p, limit, {==}), Q, owned)
276 case False{}:
277 Empty.absurd(Q(StorageLaws.created.of(Storage.new_checked(1n+p, fill, False{}))), Arith.clash_true(yes))
278
279
280
281def created_lift(+c: U32, +fill: F32, +within: {U32.is_le(c, 1048576) == True{} : Bool}, -Q: Storage.Storage -> Type,
282 empty: @zero: {U32.to_nat(c) == 0n : Nat} -> Q(Storage.Empty{}),
283 owned: @+d: Nat -> @+fits: {Storage.bounds(d, U32.to_nat(c)) == True{} : Bool} -> @-f: {Storage.bounds(d, U32.to_nat(c)) == True{} : Bool} ->
284 Q(Storage.Owned{d, U32.to_nat(c), Array.new(F32, d, fill), ArrayCore.new_balanced(F32, d, fill), f})) ->
285 Q(StorageLaws.created(c, fill)):
286 created_checked(U32.to_nat(c), fill, U32.is_le(c, 1048576), Equal.sym(Bool, U32.is_le(c, 1048576), True{}, within),
287 Api.cap_from(c, within), Q, empty, owned)