proof_ops.bend

lawful-bytes@0.1.1.0 · 268 lines · 15 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-bytes@0.1.1.0/proof_seq.bend as Q
5import lawful-bytes@0.1.1.0/proof_core.bend as C
6import lawful-words@0.1.0.0/defs.bend as W
7import lawful-words@0.1.0.0/proof_nat.bend as N
8import lawful-arrays@0.1.0.0/defs.bend as A
9import lawful-arrays@0.1.0.0/proof_base.bend as AB
10import lawful-arrays@0.1.0.0/proof_tree.bend as P
11import lawful-arrays@0.1.0.0/proof_index.bend as I
12
13# The laws that do not loop, stated on the mirror C.BT(len, t): `name_t` is
14# law `name` with each Bytes b replaced by BT(len, t) (its parameters in the
15# same order, b giving len, t).
16
17# The bytes in use fit in the block.
18law ulen:
19  for +t: P.Tree<U32>
20  for +d: Nat
21  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
22  {List.length(&2, U32, D.unpack(C.WL(t))) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
23
24def ulen(t, d, hf):
25  %Equal.sym(Nat, List.length(&2, U32, D.unpack(C.WL(t))), Nat.mul(4n, List.length(&2, U32, C.WL(t))), Q.unpack_length(C.WL(t))) :
26    {_ == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
27  %Equal.sym(Nat, List.length(&2, U32, C.WL(t)), Nat.pow(2n, d), P.view_length(U32, d, t, hf)) :
28    {Nat.mul(4n, _) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
29  {==}
30
31# What a Bytes holds
32# ==================
33
34law view_size_t:
35  for +len: U32
36  for +t: P.Tree<U32>
37  for +d: Nat
38  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
39  {List.length(&2, U32, D.view(C.BT(len, t))) == D.size(C.BT(len, t)) : Nat}
40
41def view_size_t(len, t, d, h):
42  +U = D.unpack(C.WL(t))
43  Q.take_length(U, U32.to_nat(len),
44    AB.subst(Nat, x => {Nat.is_le(U32.to_nat(len), x) == True{} : Bool}, Nat.mul(4n, Nat.pow(2n, d)), List.length(&2, U32, U),
45      Equal.sym(Nat, List.length(&2, U32, U), Nat.mul(4n, Nat.pow(2n, d)), ulen(t, d, C.ok_full(len, t, d, h))),
46      C.ok_len(len, t, d, h)))
47
48law view_bytes_t:
49  for +len: U32
50  for +t: P.Tree<U32>
51  {D.all_bytes(D.view(C.BT(len, t))) == True{} : Bool}
52
53def view_bytes_t(len, t):
54  Q.all_bytes_take(D.unpack(C.WL(t)), U32.to_nat(len), Q.all_bytes_unpack(C.WL(t)))
55
56law cap_ok_t:
57  for +len: U32
58  for +t: P.Tree<U32>
59  for +d: Nat
60  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
61  {D.cap(C.BT(len, t)) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
62
63def cap_ok_t(len, t, d, h):
64  %Equal.sym(Nat, List.length(&2, U32, C.WL(t)), Nat.pow(2n, d), P.view_length(U32, d, t, C.ok_full(len, t, d, h))) :
65    {Nat.mul(4n, _) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
66  {==}
67
68# Writing
69# =======
70
71law set_eq_t:
72  for +len: U32
73  for +t: P.Tree<U32>
74  for +i: U32
75  for +v: U32
76  {B.set(C.BT(len, t), i, v) == C.BT(len, I.set_tree(U32, t, (i >> 2n : U32), W.put_byte(C.WD(t, (i >> 2n : U32)), U32.to_nat((i .&. 3 : U32)), v))) : D.Bytes}
77
78def set_eq_t(len, t, i, v):
79  +k = (i >> 2n : U32)
80  +pb = W.put_byte(C.WD(t, k), U32.to_nat((i .&. 3 : U32)), v)
81  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), k), (P.fromT(U32, t), C.WD(t, k)), P.get_pair_t(U32, t, k)) :
82    {B.set.fin(len, i, v, _) == C.BT(len, I.set_tree(U32, t, k, pb)) : D.Bytes}
83  %Equal.sym(Array<U32>, Array.set(U32, P.fromT(U32, t), k, pb), P.fromT(U32, I.set_tree(U32, t, k, pb)), I.set_tree_eq(U32, t, k, pb)) :
84    {D.Bytes{len, _} == C.BT(len, I.set_tree(U32, t, k, pb)) : D.Bytes}
85  {==}
86
87law set_view_t:
88  for +len: U32
89  for +t: P.Tree<U32>
90  for +d: Nat
91  for +i: U32
92  for +v: U32
93  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
94  for +hi: {Nat.is_lt(U32.to_nat(i), D.size(C.BT(len, t))) == True{} : Bool}
95  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
96  {D.view(B.set(C.BT(len, t), i, v)) == List.set(&2, U32, D.view(C.BT(len, t)), U32.to_nat(i), v) : List<&2, U32>}
97
98def set_view_t(len, t, d, i, v, h, hi, hv):
99  +k = (i >> 2n : U32)
100  +w = C.WD(t, k)
101  +pb = W.put_byte(w, U32.to_nat((i .&. 3 : U32)), v)
102  +hf = C.ok_full(len, t, d, h)
103  +hd = C.ok_d(len, t, d, h)
104  +hk = C.word_lt(i, d, N.lt_le_trans(U32.to_nat(i), U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), hi, C.ok_len(len, t, d, h)))
105  +RHS = List.set(&2, U32, D.view(C.BT(len, t)), U32.to_nat(i), v)
106  %Equal.sym(D.Bytes, B.set(C.BT(len, t), i, v), C.BT(len, I.set_tree(U32, t, k, pb)), set_eq_t(len, t, i, v)) :
107    {D.view(_) == RHS : List<&2, U32>}
108  %Equal.sym(List<&2, U32>, C.WL(I.set_tree(U32, t, k, pb)), List.set(&2, U32, C.WL(t), U32.to_nat(k), pb), C.wl_set(t, d, k, pb, hf, hd, hk)) :
109    {List.take(&2, U32, D.unpack(_), U32.to_nat(len)) == RHS : List<&2, U32>}
110  %Equal.sym(List<&2, U32>, D.unpack(List.set(&2, U32, C.WL(t), U32.to_nat(k), pb)), List.set(&2, U32, D.unpack(C.WL(t)), U32.to_nat(i), v),
111    C.unpack_set_i(C.WL(t), i, w, v, hv, C.wd_get(t, d, k, hf, hd, hk))) :
112    {List.take(&2, U32, _, U32.to_nat(len)) == RHS : List<&2, U32>}
113  Q.take_set(D.unpack(C.WL(t)), U32.to_nat(len), U32.to_nat(i), v)
114
115law set_ok_t:
116  for +len: U32
117  for +t: P.Tree<U32>
118  for +d: Nat
119  for +i: U32
120  for +v: U32
121  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
122  {D.ok(B.set(C.BT(len, t), i, v), d) == True{} : Bool}
123
124def set_ok_t(len, t, d, i, v, h):
125  +k = (i >> 2n : U32)
126  +pb = W.put_byte(C.WD(t, k), U32.to_nat((i .&. 3 : U32)), v)
127  %Equal.sym(D.Bytes, B.set(C.BT(len, t), i, v), C.BT(len, I.set_tree(U32, t, k, pb)), set_eq_t(len, t, i, v)) :
128    {D.ok(_, d) == True{} : Bool}
129  C.ok_mk(len, I.set_tree(U32, t, k, pb), d, C.full_set(t, d, k, pb, C.ok_full(len, t, d, h)), C.ok_d(len, t, d, h), C.ok_len(len, t, d, h))
130
131law push_eq_t:
132  for +len: U32
133  for +t: P.Tree<U32>
134  for +v: U32
135  {B.push(C.BT(len, t), v) == C.BT((len + 1 : U32), I.set_tree(U32, t, (len >> 2n : U32), W.put_byte(C.WD(t, (len >> 2n : U32)), U32.to_nat((len .&. 3 : U32)), v))) : D.Bytes}
136
137def push_eq_t(len, t, v):
138  +k = (len >> 2n : U32)
139  +pb = W.put_byte(C.WD(t, k), U32.to_nat((len .&. 3 : U32)), v)
140  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), k), (P.fromT(U32, t), C.WD(t, k)), P.get_pair_t(U32, t, k)) :
141    {B.push.fin(len, v, _) == C.BT((len + 1 : U32), I.set_tree(U32, t, k, pb)) : D.Bytes}
142  %Equal.sym(Array<U32>, Array.set(U32, P.fromT(U32, t), k, pb), P.fromT(U32, I.set_tree(U32, t, k, pb)), I.set_tree_eq(U32, t, k, pb)) :
143    {D.Bytes{(len + 1 : U32), _} == C.BT((len + 1 : U32), I.set_tree(U32, t, k, pb)) : D.Bytes}
144  {==}
145
146# The room test of push, as numbers.
147law push_room:
148  for +len: U32
149  for +t: P.Tree<U32>
150  for +d: Nat
151  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
152  for +hc: {Nat.is_lt(D.size(C.BT(len, t)), D.cap(C.BT(len, t))) == True{} : Bool}
153  {Nat.is_lt(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
154
155def push_room(len, t, d, h, hc):
156  AB.subst(Nat, x => {Nat.is_lt(U32.to_nat(len), x) == True{} : Bool}, D.cap(C.BT(len, t)), Nat.mul(4n, Nat.pow(2n, d)),
157    cap_ok_t(len, t, d, h), hc)
158
159law push_view_t:
160  for +len: U32
161  for +t: P.Tree<U32>
162  for +d: Nat
163  for +v: U32
164  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
165  for +hc: {Nat.is_lt(D.size(C.BT(len, t)), D.cap(C.BT(len, t))) == True{} : Bool}
166  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
167  {D.view(B.push(C.BT(len, t), v)) == List.append(&2, U32, D.view(C.BT(len, t)), [v]) : List<&2, U32>}
168
169def push_view_t(len, t, d, v, h, hc, hv):
170  +k = (len >> 2n : U32)
171  +w = C.WD(t, k)
172  +pb = W.put_byte(w, U32.to_nat((len .&. 3 : U32)), v)
173  +hf = C.ok_full(len, t, d, h)
174  +hd = C.ok_d(len, t, d, h)
175  +hr = push_room(len, t, d, h, hc)
176  +hk = C.word_lt(len, d, hr)
177  +U = D.unpack(C.WL(t))
178  +RHS = List.append(&2, U32, D.view(C.BT(len, t)), [v])
179  %Equal.sym(D.Bytes, B.push(C.BT(len, t), v), C.BT((len + 1 : U32), I.set_tree(U32, t, k, pb)), push_eq_t(len, t, v)) :
180    {D.view(_) == RHS : List<&2, U32>}
181  %Equal.sym(List<&2, U32>, C.WL(I.set_tree(U32, t, k, pb)), List.set(&2, U32, C.WL(t), U32.to_nat(k), pb), C.wl_set(t, d, k, pb, hf, hd, hk)) :
182    {List.take(&2, U32, D.unpack(_), U32.to_nat((len + 1 : U32))) == RHS : List<&2, U32>}
183  %Equal.sym(List<&2, U32>, D.unpack(List.set(&2, U32, C.WL(t), U32.to_nat(k), pb)), List.set(&2, U32, U, U32.to_nat(len), v),
184    C.unpack_set_i(C.WL(t), len, w, v, hv, C.wd_get(t, d, k, hf, hd, hk))) :
185    {List.take(&2, U32, _, U32.to_nat((len + 1 : U32))) == RHS : List<&2, U32>}
186  %Equal.sym(Nat, U32.to_nat((len + 1 : U32)), Nat.add(U32.to_nat(len), 1n), C.inc_fits(len, d, hd, hr)) :
187    {List.take(&2, U32, List.set(&2, U32, U, U32.to_nat(len), v), _) == RHS : List<&2, U32>}
188  Q.take_set_succ(U, U32.to_nat(len), v,
189    AB.subst(Nat, x => {Nat.is_lt(U32.to_nat(len), x) == True{} : Bool}, Nat.mul(4n, Nat.pow(2n, d)), List.length(&2, U32, U),
190      Equal.sym(Nat, List.length(&2, U32, U), Nat.mul(4n, Nat.pow(2n, d)), ulen(t, d, hf)), hr))
191
192law push_ok_t:
193  for +len: U32
194  for +t: P.Tree<U32>
195  for +d: Nat
196  for +v: U32
197  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
198  for +hc: {Nat.is_lt(D.size(C.BT(len, t)), D.cap(C.BT(len, t))) == True{} : Bool}
199  {D.ok(B.push(C.BT(len, t), v), d) == True{} : Bool}
200
201def push_ok_t(len, t, d, v, h, hc):
202  +k = (len >> 2n : U32)
203  +pb = W.put_byte(C.WD(t, k), U32.to_nat((len .&. 3 : U32)), v)
204  +hd = C.ok_d(len, t, d, h)
205  +hr = push_room(len, t, d, h, hc)
206  +M = Nat.mul(4n, Nat.pow(2n, d))
207  %Equal.sym(D.Bytes, B.push(C.BT(len, t), v), C.BT((len + 1 : U32), I.set_tree(U32, t, k, pb)), push_eq_t(len, t, v)) :
208    {D.ok(_, d) == True{} : Bool}
209  C.ok_mk((len + 1 : U32), I.set_tree(U32, t, k, pb), d, C.full_set(t, d, k, pb, C.ok_full(len, t, d, h)), hd,
210    AB.subst(Nat, x => {Nat.is_le(x, M) == True{} : Bool}, Nat.add(U32.to_nat(len), 1n), U32.to_nat((len + 1 : U32)),
211      Equal.sym(Nat, U32.to_nat((len + 1 : U32)), Nat.add(U32.to_nat(len), 1n), C.inc_fits(len, d, hd, hr)),
212      C.succ_le(U32.to_nat(len), M, hr)))
213
214# Length, capacity, trimming
215# ==========================
216
217law capacity_pair_t:
218  for +len: U32
219  for +t: P.Tree<U32>
220  {B.capacity(C.BT(len, t)) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.capacity(C.BT(len, t)))) : D.Bytes & U32}
221
222def capacity_pair_t(len, t):
223  %Equal.sym(Array<U32> & U32, Array.size(U32, P.fromT(U32, t)), (P.fromT(U32, t), Pair.snd(Array<U32>, U32, Array.size(U32, P.fromT(U32, t)))), P.size_eta(U32, P.fromT(U32, t))) :
224    {B.capacity.fin(len, _) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.capacity.fin(len, _))) : D.Bytes & U32}
225  {==}
226
227law capacity_view_t:
228  for +len: U32
229  for +t: P.Tree<U32>
230  for +d: Nat
231  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
232  {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity(C.BT(len, t)))) == D.cap(C.BT(len, t)) : Nat}
233
234def capacity_view_t(len, t, d, h):
235  +hf = C.ok_full(len, t, d, h)
236  +X = Nat.pow(2n, d)
237  %Equal.sym(Array<U32> & U32, Array.size(U32, P.fromT(U32, t)), (P.fromT(U32, t), U32.shln(1, d)), P.size_tree(U32, d, t, hf)) :
238    {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity.fin(len, _))) == D.cap(C.BT(len, t)) : Nat}
239  %Equal.sym(Nat, List.length(&2, U32, C.WL(t)), X, P.view_length(U32, d, t, hf)) :
240    {U32.to_nat(U32.shln(U32.shln(1, d), 2n)) == Nat.mul(4n, _) : Nat}
241  %Equal.sym(Nat, Nat.mul(Nat.mul(2n, 2n), X), Nat.mul(2n, Nat.mul(2n, X)), N.mul_assoc(2n, 2n, X)) :
242    {U32.to_nat(U32.shln(U32.shln(1, d), 2n)) == _ : Nat}
243  I.size_n(Nat.add(2n, d), C.he32(d, C.ok_d(len, t, d, h)))
244
245law truncate_view_t:
246  for +len: U32
247  for +t: P.Tree<U32>
248  for +n: U32
249  for +h: {Nat.is_le(U32.to_nat(n), D.size(C.BT(len, t))) == True{} : Bool}
250  {D.view(B.truncate(C.BT(len, t), n)) == List.take(&2, U32, D.view(C.BT(len, t)), U32.to_nat(n)) : List<&2, U32>}
251
252def truncate_view_t(len, t, n, h):
253  +U = D.unpack(C.WL(t))
254  Equal.sym(List<&2, U32>, List.take(&2, U32, List.take(&2, U32, U, U32.to_nat(len)), U32.to_nat(n)), List.take(&2, U32, U, U32.to_nat(n)),
255    Q.take_take(U, U32.to_nat(len), U32.to_nat(n), h))
256
257law truncate_ok_t:
258  for +len: U32
259  for +t: P.Tree<U32>
260  for +d: Nat
261  for +n: U32
262  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
263  for +hn: {Nat.is_le(U32.to_nat(n), D.size(C.BT(len, t))) == True{} : Bool}
264  {D.ok(B.truncate(C.BT(len, t), n), d) == True{} : Bool}
265
266def truncate_ok_t(len, t, d, n, h, hn):
267  C.ok_mk(n, t, d, C.ok_full(len, t, d, h), C.ok_d(len, t, d, h),
268    N.le_trans(U32.to_nat(n), U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), hn, C.ok_len(len, t, d, h)))