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-words@0.1.0.0/proof_u32.bend as U 9 import lawful-arrays@0.1.0.0/defs.bend as A 10 import lawful-arrays@0.1.0.0/proof_base.bend as AB 11 import lawful-arrays@0.1.0.0/proof_tree.bend as P 12 import lawful-arrays@0.1.0.0/proof_index.bend as I 13 14 # The reading loops: to_list, same and same1, on the mirror C.BT(len, t) 15 # (law-shaped, as in proof_ops.bend). Each loop carries the read pair 16 # B.at(BT, s) literally: C.at_pair_t turns it into (BT, AT) so the loop steps, 17 # and the next call reads B.at(BT, s + 1), the same form one index on. 18 19 # List and index facts 20 # ==================== 21 22 def mdisc(m: Maybe<&2, U32>) -> Type: 23 match m: 24 case None{}: 25 Empty 26 case Some{x}: 27 Unit 28 29 law none_some: 30 for -x: U32 31 for e: {None{} == Some{x} : Maybe<&2, U32>} 32 Empty 33 34 def none_some(x, e): 35 %Equal.sym(Maybe<&2, U32>, None{}, Some{x}, e) : mdisc(_) 36 Unit{} 37 38 law drop_zero: 39 for +xs: List<&2, U32> 40 {List.drop(&2, U32, xs, 0n) == xs : List<&2, U32>} 41 42 def drop_zero(xs): 43 match xs: 44 case Nil{}: 45 {==} 46 case Con{x, t}: 47 {==} 48 49 # Dropping j elements, when element j is x: x, then the rest. 50 law drop_get: 51 for +xs: List<&2, U32> 52 for +j: Nat 53 for +x: U32 54 for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>} 55 {List.drop(&2, U32, xs, j) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>} 56 57 def drop_get(xs, j, x, h): 58 match xs j: 59 case Nil{} _: 60 Empty.absurd({List.drop(&2, U32, Nil{}, j) == x <> List.drop(&2, U32, Nil{}, Nat.add(j, 1n)) : List<&2, U32>}, 61 none_some(x, h)) 62 case Con{+y, t} 0n: 63 +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, h) 64 %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) : {y <> t == x <> _ : List<&2, U32>} 65 %Equal.sym(U32, y, x, yx) : {_ <> t == x <> t : List<&2, U32>} 66 {==} 67 case Con{y, t} 1n+p: 68 drop_get(t, p, x, h) 69 70 law slice_cons: 71 for +xs: List<&2, U32> 72 for +j: Nat 73 for +k: Nat 74 for +x: U32 75 for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>} 76 {D.slice(xs, j, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>} 77 78 def slice_cons(xs, j, k, x, h): 79 %Equal.sym(List<&2, U32>, List.drop(&2, U32, xs, j), x <> List.drop(&2, U32, xs, Nat.add(j, 1n)), drop_get(xs, j, x, h)) : 80 {List.take(&2, U32, _, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>} 81 {==} 82 83 # a + 1 + m <= b gives a < b. 84 law lt_of_le: 85 for +a: Nat 86 for +m: Nat 87 for +b: Nat 88 for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool} 89 {Nat.is_lt(a, b) == True{} : Bool} 90 91 def lt_of_le(a, m, b, h): 92 +h1 = AB.subst(Nat, x => {Nat.is_le(x, b) == True{} : Bool}, Nat.add(a, 1n+m), 1n+Nat.add(a, m), AB.add_succ(a, m), h) 93 +h2 = N.le_trans(1n+a, 1n+Nat.add(a, m), b, N.le_add_r(a, m), h1) 94 Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), True{}, Equal.sym(Bool, Nat.is_le(1n+a, b), Nat.is_lt(a, b), N.le_succ_lt(a, b)), h2) 95 96 # a + 1 + m <= b gives (a + 1) + m <= b. 97 law le_step: 98 for +a: Nat 99 for +m: Nat 100 for +b: Nat 101 for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool} 102 {Nat.is_le(Nat.add(Nat.add(a, 1n), m), b) == True{} : Bool} 103 104 def le_step(a, m, b, h): 105 AB.subst(Nat, x => {Nat.is_le(x, b) == True{} : Bool}, Nat.add(a, Nat.add(1n, m)), Nat.add(Nat.add(a, 1n), m), 106 Equal.sym(Nat, Nat.add(Nat.add(a, 1n), m), Nat.add(a, Nat.add(1n, m)), N.add_assoc(a, 1n, m)), h) 107 108 # One step of a read loop at index s with n + 1 left, within a Bytes of size len: 109 # byte s is read, s + 1 does not wrap, and the bound holds one index on. 110 law step_val: 111 for +len: U32 112 for +t: P.Tree 113 for +d: Nat 114 for +s: U32 115 for +m: Nat 116 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 117 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool} 118 {List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s)) == Some{C.AT(len, t, s)} : Maybe<&2, U32>} 119 120 def step_val(len, t, d, s, m, h, hs): 121 Equal.sym(Maybe<&2, U32>, Some{C.AT(len, t, s)}, List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s)), 122 C.at_view_t(len, t, d, s, C.ok_full(len, t, d, h), C.ok_d(len, t, d, h), C.ok_len(len, t, d, h), 123 lt_of_le(U32.to_nat(s), m, U32.to_nat(len), hs))) 124 125 law step_inc: 126 for +len: U32 127 for +t: P.Tree 128 for +d: Nat 129 for +s: U32 130 for +m: Nat 131 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 132 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool} 133 {U32.to_nat((s + 1 : U32)) == Nat.add(U32.to_nat(s), 1n) : Nat} 134 135 def step_inc(len, t, d, s, m, h, hs): 136 C.inc_fits(s, d, C.ok_d(len, t, d, h), 137 N.lt_le_trans(U32.to_nat(s), U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), lt_of_le(U32.to_nat(s), m, U32.to_nat(len), hs), 138 C.ok_len(len, t, d, h))) 139 140 law step_le: 141 for +len: U32 142 for +t: P.Tree 143 for +d: Nat 144 for +s: U32 145 for +m: Nat 146 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 147 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool} 148 {Nat.is_le(Nat.add(U32.to_nat((s + 1 : U32)), m), U32.to_nat(len)) == True{} : Bool} 149 150 def step_le(len, t, d, s, m, h, hs): 151 AB.subst(Nat, x => {Nat.is_le(Nat.add(x, m), U32.to_nat(len)) == True{} : Bool}, Nat.add(U32.to_nat(s), 1n), U32.to_nat((s + 1 : U32)), 152 Equal.sym(Nat, U32.to_nat((s + 1 : U32)), Nat.add(U32.to_nat(s), 1n), step_inc(len, t, d, s, m, h, hs)), 153 le_step(U32.to_nat(s), m, U32.to_nat(len), hs)) 154 155 # to_list 156 # ======= 157 158 # to_list reads from the last byte back, putting each in front of acc, so its 159 # loop is a tail call. The invariant: reading at j = m + s with 1 + m bytes 160 # left gives slice(view, s, 1 + m) followed by acc. 161 162 law tl_pair: 163 for +n: Nat 164 for +len: U32 165 for +t: P.Tree 166 for +j: U32 167 for +acc: List<&2, U32> 168 {B.to_list.go(n, B.at(C.BT(len, t), j), j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(n, B.at(C.BT(len, t), j), j, acc))) : D.Bytes & List<&2, U32>} 169 170 def tl_pair(n, len, t, j, acc): 171 match n: 172 case 0n: 173 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) : 174 {B.to_list.go(0n, _, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, j, acc))) : D.Bytes & List<&2, U32>} 175 {==} 176 case 1n+m: 177 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) : 178 {B.to_list.go(1n+m, _, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, _, j, acc))) : D.Bytes & List<&2, U32>} 179 tl_pair(m, len, t, (j - 1 : U32), C.AT(len, t, j) <> acc) 180 181 law append_nil: 182 for +xs: List<&2, U32> 183 {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>} 184 185 def append_nil(xs): 186 match xs: 187 case Nil{}: 188 {==} 189 case Con{+x, t}: 190 Equal.cong(List<&2, U32>, List<&2, U32>, z => x <> z, List.append(&2, U32, t, Nil{}), t, append_nil(t)) 191 192 law get_drop: 193 for +xs: List<&2, U32> 194 for +i: Nat 195 for +k: Nat 196 {List.get(&2, U32, List.drop(&2, U32, xs, i), k) == List.get(&2, U32, xs, Nat.add(i, k)) : Maybe<&2, U32>} 197 198 def get_drop(xs, i, k): 199 match xs i: 200 case Nil{} _: 201 {==} 202 case Con{x, t} 0n: 203 {==} 204 case Con{x, t} 1n+p: 205 get_drop(t, p, k) 206 207 # Taking k + 1 elements then acc is taking k then element k, then acc. 208 law take_snoc: 209 for +ys: List<&2, U32> 210 for +k: Nat 211 for +x: U32 212 for +acc: List<&2, U32> 213 for +h: {List.get(&2, U32, ys, k) == Some{x} : Maybe<&2, U32>} 214 {List.append(&2, U32, List.take(&2, U32, ys, 1n+k), acc) == List.append(&2, U32, List.take(&2, U32, ys, k), x <> acc) : List<&2, U32>} 215 216 def take_snoc(ys, k, x, acc, h): 217 match ys k: 218 case Nil{} _: 219 Empty.absurd({List.append(&2, U32, List.take(&2, U32, Nil{}, 1n+k), acc) == List.append(&2, U32, List.take(&2, U32, Nil{}, k), x <> acc) : List<&2, U32>}, 220 none_some(x, h)) 221 case Con{+y, t} 0n: 222 +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, h) 223 %Equal.sym(List<&2, U32>, List.take(&2, U32, t, 0n), Nil{}, Q.take_zero(t)) : {y <> List.append(&2, U32, _, acc) == x <> acc : List<&2, U32>} 224 %Equal.sym(U32, y, x, yx) : {_ <> acc == x <> acc : List<&2, U32>} 225 {==} 226 case Con{+y, t} 1n+p: 227 Equal.cong(List<&2, U32>, List<&2, U32>, z => y <> z, List.append(&2, U32, List.take(&2, U32, t, 1n+p), acc), 228 List.append(&2, U32, List.take(&2, U32, t, p), x <> acc), take_snoc(t, p, x, acc, h)) 229 230 law slice_snoc: 231 for +xs: List<&2, U32> 232 for +i: Nat 233 for +k: Nat 234 for +x: U32 235 for +acc: List<&2, U32> 236 for +h: {List.get(&2, U32, xs, Nat.add(k, i)) == Some{x} : Maybe<&2, U32>} 237 {List.append(&2, U32, D.slice(xs, i, 1n+k), acc) == List.append(&2, U32, D.slice(xs, i, k), x <> acc) : List<&2, U32>} 238 239 def slice_snoc(xs, i, k, x, acc, h): 240 +ys = List.drop(&2, U32, xs, i) 241 +g = AB.subst(Nat, z => {List.get(&2, U32, ys, k) == List.get(&2, U32, xs, z) : Maybe<&2, U32>}, Nat.add(i, k), Nat.add(k, i), 242 N.add_comm(i, k), get_drop(xs, i, k)) 243 take_snoc(ys, k, x, acc, Equal.trans(Maybe<&2, U32>, List.get(&2, U32, ys, k), List.get(&2, U32, xs, Nat.add(k, i)), Some{x}, g, h)) 244 245 # Byte j, for j = m + s below len, is element m + s of the view. 246 law tl_val: 247 for +m: Nat 248 for +len: U32 249 for +t: P.Tree 250 for +d: Nat 251 for +s: U32 252 for +j: U32 253 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 254 for +hj: {U32.to_nat(j) == Nat.add(m, U32.to_nat(s)) : Nat} 255 for +hs: {Nat.is_lt(Nat.add(m, U32.to_nat(s)), U32.to_nat(len)) == True{} : Bool} 256 {List.get(&2, U32, D.view(C.BT(len, t)), Nat.add(m, U32.to_nat(s))) == Some{C.AT(len, t, j)} : Maybe<&2, U32>} 257 258 def tl_val(m, len, t, d, s, j, h, hj, hs): 259 +a = Nat.add(m, U32.to_nat(s)) 260 +hi = AB.subst(Nat, z => {Nat.is_lt(z, U32.to_nat(len)) == True{} : Bool}, a, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), a, hj), hs) 261 +e = Equal.sym(Maybe<&2, U32>, Some{C.AT(len, t, j)}, List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(j)), 262 C.at_view_t(len, t, d, j, C.ok_full(len, t, d, h), C.ok_d(len, t, d, h), C.ok_len(len, t, d, h), hi)) 263 AB.subst(Nat, z => {List.get(&2, U32, D.view(C.BT(len, t)), z) == Some{C.AT(len, t, j)} : Maybe<&2, U32>}, U32.to_nat(j), a, hj, e) 264 265 # j - 1 for j = 1 + m + s. 266 law tl_dec: 267 for +m: Nat 268 for +s: U32 269 for +j: U32 270 for +hj: {U32.to_nat(j) == 1n+Nat.add(m, U32.to_nat(s)) : Nat} 271 {U32.to_nat((j - 1 : U32)) == Nat.add(m, U32.to_nat(s)) : Nat} 272 273 def tl_dec(m, s, j, hj): 274 +a = Nat.add(m, U32.to_nat(s)) 275 +hle = Equal.trans(Bool, U32.is_le(1, j), Nat.is_le(U32.to_nat(1), U32.to_nat(j)), True{}, U.is_le_to_nat(1, j), 276 AB.subst(Nat, z => {Nat.is_le(U32.to_nat(1), z) == True{} : Bool}, 1n+a, U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), 1n+a, hj), N.le_zero_l(a))) 277 %Equal.sym(Nat, U32.to_nat((j - 1 : U32)), Nat.sub(U32.to_nat(j), U32.to_nat(1)), U.to_nat_sub_le(j, 1, hle)) : {_ == a : Nat} 278 %Equal.sym(Nat, U32.to_nat(j), 1n+a, hj) : {Nat.sub(_, U32.to_nat(1)) == a : Nat} 279 N.sub_zero(a) 280 281 law tl_lt: 282 for +a: Nat 283 for +b: Nat 284 for +h: {Nat.is_lt(1n+a, b) == True{} : Bool} 285 {Nat.is_lt(a, b) == True{} : Bool} 286 287 def tl_lt(a, b, h): 288 Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), True{}, Equal.sym(Bool, Nat.is_le(1n+a, b), Nat.is_lt(a, b), N.le_succ_lt(a, b)), 289 N.lt_to_le(1n+a, b, h)) 290 291 law tl_view: 292 for +m: Nat 293 for +len: U32 294 for +t: P.Tree 295 for +d: Nat 296 for +s: U32 297 for +j: U32 298 for +acc: List<&2, U32> 299 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 300 for +hj: {U32.to_nat(j) == Nat.add(m, U32.to_nat(s)) : Nat} 301 for +hs: {Nat.is_lt(Nat.add(m, U32.to_nat(s)), U32.to_nat(len)) == True{} : Bool} 302 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, B.at(C.BT(len, t), j), j, acc)) == List.append(&2, U32, D.slice(D.view(C.BT(len, t)), U32.to_nat(s), 1n+m), acc) : List<&2, U32>} 303 304 def tl_view(m, len, t, d, s, j, acc, h, hj, hs): 305 match m: 306 case 0n: 307 +x = C.AT(len, t, j) 308 +j1 = (j - 1 : U32) 309 +xs = D.view(C.BT(len, t)) 310 +ys = List.drop(&2, U32, xs, U32.to_nat(s)) 311 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) : 312 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n, _, j, acc)) == List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n), acc) : List<&2, U32>} 313 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j1), (C.BT(len, t), C.AT(len, t, j1)), C.at_pair_t(len, t, j1)) : 314 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, j1, x <> acc)) == List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n), acc) : List<&2, U32>} 315 %Equal.sym(List<&2, U32>, List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n), acc), List.append(&2, U32, D.slice(xs, U32.to_nat(s), 0n), x <> acc), 316 slice_snoc(xs, U32.to_nat(s), 0n, x, acc, tl_val(0n, len, t, d, s, j, h, hj, hs))) : 317 {x <> acc == _ : List<&2, U32>} 318 %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : {x <> acc == List.append(&2, U32, _, x <> acc) : List<&2, U32>} 319 {==} 320 case 1n+p: 321 +x = C.AT(len, t, j) 322 +j1 = (j - 1 : U32) 323 +xs = D.view(C.BT(len, t)) 324 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) : 325 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+(1n+p), _, j, acc)) == List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n+(1n+p)), acc) : List<&2, U32>} 326 %Equal.sym(List<&2, U32>, List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n+(1n+p)), acc), List.append(&2, U32, D.slice(xs, U32.to_nat(s), 1n+p), x <> acc), 327 slice_snoc(xs, U32.to_nat(s), 1n+p, x, acc, tl_val(1n+p, len, t, d, s, j, h, hj, hs))) : 328 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+p, B.at(C.BT(len, t), j1), j1, x <> acc)) == _ : List<&2, U32>} 329 tl_view(p, len, t, d, s, j1, x <> acc, h, tl_dec(p, s, j, hj), tl_lt(Nat.add(p, U32.to_nat(s)), U32.to_nat(len), hs)) 330 331 # to_list(BT, s, n) with k = n bytes: none, or 1 + p read from s + n - 1. 332 law tl_view_k: 333 for +k: Nat 334 for +len: U32 335 for +t: P.Tree 336 for +d: Nat 337 for +s: U32 338 for +n: U32 339 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 340 for +hk: {U32.to_nat(n) == k : Nat} 341 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), U32.to_nat(len)) == True{} : Bool} 342 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(k, B.at(C.BT(len, t), ((s + n : U32) - 1 : U32)), ((s + n : U32) - 1 : U32), Nil{})) == D.slice(D.view(C.BT(len, t)), U32.to_nat(s), k) : List<&2, U32>} 343 344 def tl_view_k(k, len, t, d, s, n, h, hk, hs): 345 match k: 346 case 0n: 347 +e = ((s + n : U32) - 1 : U32) 348 +xs = D.view(C.BT(len, t)) 349 +ys = List.drop(&2, U32, xs, U32.to_nat(s)) 350 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), e), (C.BT(len, t), C.AT(len, t, e)), C.at_pair_t(len, t, e)) : 351 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, e, Nil{})) == D.slice(xs, U32.to_nat(s), 0n) : List<&2, U32>} 352 Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) 353 case 1n+p: 354 +e = ((s + n : U32) - 1 : U32) 355 +xs = D.view(C.BT(len, t)) 356 +a = Nat.add(p, U32.to_nat(s)) 357 +sn = Nat.add(U32.to_nat(s), U32.to_nat(n)) 358 +E = Equal.trans(Nat, sn, Nat.add(U32.to_nat(s), 1n+p), 1n+a, 359 Equal.cong(Nat, Nat, z => Nat.add(U32.to_nat(s), z), U32.to_nat(n), 1n+p, hk), 360 Equal.trans(Nat, Nat.add(U32.to_nat(s), 1n+p), 1n+Nat.add(U32.to_nat(s), p), 1n+a, N.add_succ(U32.to_nat(s), p), 361 Equal.cong(Nat, Nat, z => 1n+z, Nat.add(U32.to_nat(s), p), a, N.add_comm(U32.to_nat(s), p)))) 362 +hsum = C.add_fits(s, n, d, C.ok_d(len, t, d, h), N.le_trans(sn, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), hs, C.ok_len(len, t, d, h))) 363 +hj = tl_dec(p, s, (s + n : U32), Equal.trans(Nat, U32.to_nat((s + n : U32)), sn, 1n+a, hsum, E)) 364 +hlt = Equal.trans(Bool, Nat.is_lt(a, U32.to_nat(len)), Nat.is_le(1n+a, U32.to_nat(len)), True{}, 365 Equal.sym(Bool, Nat.is_le(1n+a, U32.to_nat(len)), Nat.is_lt(a, U32.to_nat(len)), N.le_succ_lt(a, U32.to_nat(len))), 366 AB.subst(Nat, z => {Nat.is_le(z, U32.to_nat(len)) == True{} : Bool}, sn, 1n+a, E, hs)) 367 +sl = D.slice(xs, U32.to_nat(s), 1n+p) 368 Equal.trans(List<&2, U32>, Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+p, B.at(C.BT(len, t), e), e, Nil{})), List.append(&2, U32, sl, Nil{}), sl, 369 tl_view(p, len, t, d, s, e, Nil{}, h, hj, hlt), append_nil(sl)) 370 371 law to_list_pair_t: 372 for +len: U32 373 for +t: P.Tree 374 for +s: U32 375 for +n: U32 376 {B.to_list(C.BT(len, t), s, n) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list(C.BT(len, t), s, n))) : D.Bytes & List<&2, U32>} 377 378 def to_list_pair_t(len, t, s, n): 379 tl_pair(U32.to_nat(n), len, t, ((s + n : U32) - 1 : U32), Nil{}) 380 381 law to_list_view_t: 382 for +len: U32 383 for +t: P.Tree 384 for +d: Nat 385 for +s: U32 386 for +n: U32 387 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 388 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool} 389 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(C.BT(len, t), s, n)) == D.slice(D.view(C.BT(len, t)), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>} 390 391 def to_list_view_t(len, t, d, s, n, h, hs): 392 tl_view_k(U32.to_nat(n), len, t, d, s, n, h, {==}, hs) 393 394 # same 395 # ==== 396 397 law and_assoc: 398 for +a: Bool 399 for +b: Bool 400 for +c: Bool 401 {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool} 402 403 def and_assoc(a, b, c): 404 match a: 405 case False{}: 406 {==} 407 case True{}: 408 {==} 409 410 # Comparing n more bytes from i of A and from j of B, after an empty prefix: 411 # acc and the comparison of the two slices. 412 law lists_end: 413 for +acc: Bool 414 for +xs: List<&2, U32> 415 for +ys: List<&2, U32> 416 {acc == Bool.and(acc, D.list_eq(List.take(&2, U32, xs, 0n), List.take(&2, U32, ys, 0n))) : Bool} 417 418 def lists_end(acc, xs, ys): 419 %Equal.sym(List<&2, U32>, List.take(&2, U32, xs, 0n), Nil{}, Q.take_zero(xs)) : 420 {acc == Bool.and(acc, D.list_eq(_, List.take(&2, U32, ys, 0n))) : Bool} 421 %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : 422 {acc == Bool.and(acc, D.list_eq(Nil{}, _)) : Bool} 423 Equal.sym(Bool, Bool.and(acc, True{}), acc, N.and_true_r_id(acc)) 424 425 # One step of a comparison loop: the two slices from x and y, with the 426 # accumulated test rebracketed. 427 law lists_step: 428 for +acc: Bool 429 for +xs: List<&2, U32> 430 for +ys: List<&2, U32> 431 for +i: Nat 432 for +j: Nat 433 for +i1: U32 434 for +j1: U32 435 for +k: Nat 436 for +x: U32 437 for +y: U32 438 for +hx: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>} 439 for +hy: {List.get(&2, U32, ys, j) == Some{y} : Maybe<&2, U32>} 440 for +ei: {U32.to_nat(i1) == Nat.add(i, 1n) : Nat} 441 for +ej: {U32.to_nat(j1) == Nat.add(j, 1n) : Nat} 442 {Bool.and(Bool.and(acc, U32.is_eq(x, y)), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, U32.to_nat(j1), k))) 443 == Bool.and(acc, D.list_eq(D.slice(xs, i, 1n+k), D.slice(ys, j, 1n+k))) : Bool} 444 445 def lists_step(acc, xs, ys, i, j, i1, j1, k, x, y, hx, hy, ei, ej): 446 +LHS = Bool.and(Bool.and(acc, U32.is_eq(x, y)), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, U32.to_nat(j1), k))) 447 %Equal.sym(List<&2, U32>, D.slice(xs, i, 1n+k), x <> D.slice(xs, Nat.add(i, 1n), k), slice_cons(xs, i, k, x, hx)) : 448 {LHS == Bool.and(acc, D.list_eq(_, D.slice(ys, j, 1n+k))) : Bool} 449 %Equal.sym(List<&2, U32>, D.slice(ys, j, 1n+k), y <> D.slice(ys, Nat.add(j, 1n), k), slice_cons(ys, j, k, y, hy)) : 450 {LHS == Bool.and(acc, D.list_eq(x <> D.slice(xs, Nat.add(i, 1n), k), _)) : Bool} 451 %ei : {LHS == Bool.and(acc, Bool.and(U32.is_eq(x, y), D.list_eq(D.slice(xs, _, k), D.slice(ys, Nat.add(j, 1n), k)))) : Bool} 452 %ej : {LHS == Bool.and(acc, Bool.and(U32.is_eq(x, y), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, _, k)))) : Bool} 453 and_assoc(acc, U32.is_eq(x, y), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(ys, U32.to_nat(j1), k))) 454 455 law sm_pair: 456 for +n: Nat 457 for +la: U32 458 for +ta: P.Tree 459 for +lb: U32 460 for +tb: P.Tree 461 for +i: U32 462 for +j: U32 463 for +acc: Bool 464 {B.same.go(n, B.at(C.BT(la, ta), i), B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 465 Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(n, B.at(C.BT(la, ta), i), B.at(C.BT(lb, tb), j), i, j, acc))))) : D.Bytes & (D.Bytes & Bool)} 466 467 def sm_pair(n, la, ta, lb, tb, i, j, acc): 468 match n: 469 case 0n: 470 %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), C.AT(la, ta, i)), C.at_pair_t(la, ta, i)) : 471 {B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 472 Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc))))) : D.Bytes & (D.Bytes & Bool)} 473 %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), C.AT(lb, tb, j)), C.at_pair_t(lb, tb, j)) : 474 {B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 475 Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc))))) : D.Bytes & (D.Bytes & Bool)} 476 {==} 477 case 1n+k: 478 %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), C.AT(la, ta, i)), C.at_pair_t(la, ta, i)) : 479 {B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 480 Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc))))) : D.Bytes & (D.Bytes & Bool)} 481 %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), C.AT(lb, tb, j)), C.at_pair_t(lb, tb, j)) : 482 {B.same.go(1n+k, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 483 Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc))))) : D.Bytes & (D.Bytes & Bool)} 484 sm_pair(k, la, ta, lb, tb, (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(C.AT(la, ta, i), C.AT(lb, tb, j))) 485 486 law sm_view: 487 for +n: Nat 488 for +la: U32 489 for +ta: P.Tree 490 for +lb: U32 491 for +tb: P.Tree 492 for +d: Nat 493 for +e: Nat 494 for +i: U32 495 for +j: U32 496 for +acc: Bool 497 for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool} 498 for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool} 499 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(la)) == True{} : Bool} 500 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(lb)) == True{} : Bool} 501 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(n, B.at(C.BT(la, ta), i), B.at(C.BT(lb, tb), j), i, j, acc))) 502 == Bool.and(acc, D.list_eq(D.slice(D.view(C.BT(la, ta)), U32.to_nat(i), n), D.slice(D.view(C.BT(lb, tb)), U32.to_nat(j), n))) : Bool} 503 504 def sm_view(n, la, ta, lb, tb, d, e, i, j, acc, ha, hb, hi, hj): 505 match n: 506 case 0n: 507 +xa = D.view(C.BT(la, ta)) 508 +xb = D.view(C.BT(lb, tb)) 509 +RHS = Bool.and(acc, D.list_eq(D.slice(xa, U32.to_nat(i), 0n), D.slice(xb, U32.to_nat(j), 0n))) 510 %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), C.AT(la, ta, i)), C.at_pair_t(la, ta, i)) : 511 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc))) == RHS : Bool} 512 %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), C.AT(lb, tb, j)), C.at_pair_t(lb, tb, j)) : 513 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc))) == RHS : Bool} 514 lists_end(acc, List.drop(&2, U32, xa, U32.to_nat(i)), List.drop(&2, U32, xb, U32.to_nat(j))) 515 case 1n+k: 516 +xa = D.view(C.BT(la, ta)) 517 +xb = D.view(C.BT(lb, tb)) 518 +x = C.AT(la, ta, i) 519 +y = C.AT(lb, tb, j) 520 +i1 = (i + 1 : U32) 521 +j1 = (j + 1 : U32) 522 +RHS = Bool.and(acc, D.list_eq(D.slice(xa, U32.to_nat(i), 1n+k), D.slice(xb, U32.to_nat(j), 1n+k))) 523 %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), x), C.at_pair_t(la, ta, i)) : 524 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc))) == RHS : Bool} 525 %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), y), C.at_pair_t(lb, tb, j)) : 526 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(1n+k, (C.BT(la, ta), x), _, i, j, acc))) == RHS : Bool} 527 %Equal.sym(Bool, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same.go(k, B.at(C.BT(la, ta), i1), B.at(C.BT(lb, tb), j1), i1, j1, acc && U32.is_eq(x, y)))), 528 Bool.and(acc && U32.is_eq(x, y), D.list_eq(D.slice(xa, U32.to_nat(i1), k), D.slice(xb, U32.to_nat(j1), k))), 529 sm_view(k, la, ta, lb, tb, d, e, i1, j1, acc && U32.is_eq(x, y), ha, hb, 530 step_le(la, ta, d, i, k, ha, hi), step_le(lb, tb, e, j, k, hb, hj))) : 531 {_ == RHS : Bool} 532 lists_step(acc, xa, xb, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y, 533 step_val(la, ta, d, i, k, ha, hi), step_val(lb, tb, e, j, k, hb, hj), 534 step_inc(la, ta, d, i, k, ha, hi), step_inc(lb, tb, e, j, k, hb, hj)) 535 536 law same_pair_t: 537 for +la: U32 538 for +ta: P.Tree 539 for +lb: U32 540 for +tb: P.Tree 541 for +i: U32 542 for +j: U32 543 for +n: U32 544 {B.same(C.BT(la, ta), i, C.BT(lb, tb), j, n) == (C.BT(la, ta), (C.BT(lb, tb), Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(C.BT(la, ta), i, C.BT(lb, tb), j, n))))) : D.Bytes & (D.Bytes & Bool)} 545 546 def same_pair_t(la, ta, lb, tb, i, j, n): 547 sm_pair(U32.to_nat(n), la, ta, lb, tb, i, j, True{}) 548 549 law same_view_t: 550 for +la: U32 551 for +ta: P.Tree 552 for +lb: U32 553 for +tb: P.Tree 554 for +d: Nat 555 for +e: Nat 556 for +i: U32 557 for +j: U32 558 for +n: U32 559 for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool} 560 for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool} 561 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(la, ta))) == True{} : Bool} 562 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(lb, tb))) == True{} : Bool} 563 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(C.BT(la, ta), i, C.BT(lb, tb), j, n))) == D.list_eq(D.slice(D.view(C.BT(la, ta)), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(C.BT(lb, tb)), U32.to_nat(j), U32.to_nat(n))) : Bool} 564 565 def same_view_t(la, ta, lb, tb, d, e, i, j, n, ha, hb, hi, hj): 566 sm_view(U32.to_nat(n), la, ta, lb, tb, d, e, i, j, True{}, ha, hb, hi, hj) 567 568 # same1 (two reads of one buffer per step, through at2) 569 # ===================================================== 570 571 law at2_eq: 572 for +len: U32 573 for +t: P.Tree 574 for +i: U32 575 for +j: U32 576 {B.at2(C.BT(len, t), i, j) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)} 577 578 def at2_eq(len, t, i, j): 579 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), i), (C.BT(len, t), C.AT(len, t, i)), C.at_pair_t(len, t, i)) : 580 {B.at2.fin(j, _) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)} 581 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) : 582 {B.at2.fin2(C.AT(len, t, i), _) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)} 583 {==} 584 585 law s1_pair: 586 for +n: Nat 587 for +len: U32 588 for +t: P.Tree 589 for +i: U32 590 for +j: U32 591 for +acc: Bool 592 {B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc))) : D.Bytes & Bool} 593 594 def s1_pair(n, len, t, i, j, acc): 595 match n: 596 case 0n: 597 %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))), at2_eq(len, t, i, j)) : 598 {B.same1.go(0n, _, i, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1.go(0n, _, i, j, acc))) : D.Bytes & Bool} 599 {==} 600 case 1n+m: 601 %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))), at2_eq(len, t, i, j)) : 602 {B.same1.go(1n+m, _, i, j, acc) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1.go(1n+m, _, i, j, acc))) : D.Bytes & Bool} 603 s1_pair(m, len, t, (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(C.AT(len, t, i), C.AT(len, t, j))) 604 605 law s1_view: 606 for +n: Nat 607 for +len: U32 608 for +t: P.Tree 609 for +d: Nat 610 for +i: U32 611 for +j: U32 612 for +acc: Bool 613 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 614 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(len)) == True{} : Bool} 615 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool} 616 {Pair.snd(D.Bytes, Bool, B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc)) 617 == Bool.and(acc, D.list_eq(D.slice(D.view(C.BT(len, t)), U32.to_nat(i), n), D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n))) : Bool} 618 619 def s1_view(n, len, t, d, i, j, acc, h, hi, hj): 620 match n: 621 case 0n: 622 +xs = D.view(C.BT(len, t)) 623 %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))), at2_eq(len, t, i, j)) : 624 {Pair.snd(D.Bytes, Bool, B.same1.go(0n, _, i, j, acc)) == Bool.and(acc, D.list_eq(D.slice(xs, U32.to_nat(i), 0n), D.slice(xs, U32.to_nat(j), 0n))) : Bool} 625 lists_end(acc, List.drop(&2, U32, xs, U32.to_nat(i)), List.drop(&2, U32, xs, U32.to_nat(j))) 626 case 1n+k: 627 +xs = D.view(C.BT(len, t)) 628 +x = C.AT(len, t, i) 629 +y = C.AT(len, t, j) 630 +i1 = (i + 1 : U32) 631 +j1 = (j + 1 : U32) 632 +RHS = Bool.and(acc, D.list_eq(D.slice(xs, U32.to_nat(i), 1n+k), D.slice(xs, U32.to_nat(j), 1n+k))) 633 %Equal.sym(D.Bytes & (U32 & U32), B.at2(C.BT(len, t), i, j), (C.BT(len, t), (x, y)), at2_eq(len, t, i, j)) : 634 {Pair.snd(D.Bytes, Bool, B.same1.go(1n+k, _, i, j, acc)) == RHS : Bool} 635 %Equal.sym(Bool, Pair.snd(D.Bytes, Bool, B.same1.go(k, B.at2(C.BT(len, t), i1, j1), i1, j1, acc && U32.is_eq(x, y))), 636 Bool.and(acc && U32.is_eq(x, y), D.list_eq(D.slice(xs, U32.to_nat(i1), k), D.slice(xs, U32.to_nat(j1), k))), 637 s1_view(k, len, t, d, i1, j1, acc && U32.is_eq(x, y), h, 638 step_le(len, t, d, i, k, h, hi), step_le(len, t, d, j, k, h, hj))) : 639 {_ == RHS : Bool} 640 lists_step(acc, xs, xs, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y, 641 step_val(len, t, d, i, k, h, hi), step_val(len, t, d, j, k, h, hj), 642 step_inc(len, t, d, i, k, h, hi), step_inc(len, t, d, j, k, h, hj)) 643 644 law same1_pair_t: 645 for +len: U32 646 for +t: P.Tree 647 for +i: U32 648 for +j: U32 649 for +n: U32 650 {B.same1(C.BT(len, t), i, j, n) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, B.same1(C.BT(len, t), i, j, n))) : D.Bytes & Bool} 651 652 def same1_pair_t(len, t, i, j, n): 653 s1_pair(U32.to_nat(n), len, t, i, j, True{}) 654 655 law same1_view_t: 656 for +len: U32 657 for +t: P.Tree 658 for +d: Nat 659 for +i: U32 660 for +j: U32 661 for +n: U32 662 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 663 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool} 664 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool} 665 {Pair.snd(D.Bytes, Bool, B.same1(C.BT(len, t), i, j, n)) == D.list_eq(D.slice(D.view(C.BT(len, t)), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(C.BT(len, t)), U32.to_nat(j), U32.to_nat(n))) : Bool} 666 667 def same1_view_t(len, t, d, i, j, n, h, hi, hj): 668 s1_view(U32.to_nat(n), len, t, d, i, j, True{}, h, hi, hj)