1 import Base 2 import ./defs.bend as D 3 import ./bytes.bend as B 4 import ./proof_seq.bend as Q 5 import ./proof_core.bend as C 6 import lawful-words@0.1.0.0/defs.bend as W 7 import lawful-words@0.1.0.0/proof_nat.bend as N 8 import lawful-arrays@0.1.0.0/defs.bend as A 9 import lawful-arrays@0.1.0.0/proof_base.bend as AB 10 import lawful-arrays@0.1.0.0/proof_tree.bend as P 11 import 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. 18 law ulen: 19 for +t: P.Tree 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 24 def 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 34 law view_size_t: 35 for +len: U32 36 for +t: P.Tree 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 41 def 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 48 law view_bytes_t: 49 for +len: U32 50 for +t: P.Tree 51 {D.all_bytes(D.view(C.BT(len, t))) == True{} : Bool} 52 53 def 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 56 law cap_ok_t: 57 for +len: U32 58 for +t: P.Tree 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 63 def 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 71 law set_eq_t: 72 for +len: U32 73 for +t: P.Tree 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 78 def 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, 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, 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 87 law set_view_t: 88 for +len: U32 89 for +t: P.Tree 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 98 def 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 115 law set_ok_t: 116 for +len: U32 117 for +t: P.Tree 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 124 def 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 131 law push_eq_t: 132 for +len: U32 133 for +t: P.Tree 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 137 def 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, 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, 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. 147 law push_room: 148 for +len: U32 149 for +t: P.Tree 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 155 def 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 159 law push_view_t: 160 for +len: U32 161 for +t: P.Tree 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 169 def 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 192 law push_ok_t: 193 for +len: U32 194 for +t: P.Tree 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 201 def 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 217 law capacity_pair_t: 218 for +len: U32 219 for +t: P.Tree 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 222 def capacity_pair_t(len, t): 223 %Equal.sym(Array & U32, Array.size(U32, P.fromT(U32, t)), (P.fromT(U32, t), Pair.snd(Array, 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 227 law capacity_view_t: 228 for +len: U32 229 for +t: P.Tree 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 234 def 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, 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 245 law truncate_view_t: 246 for +len: U32 247 for +t: P.Tree 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 252 def 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 257 law truncate_ok_t: 258 for +len: U32 259 for +t: P.Tree 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 266 def 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)))