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 reading loops: to_list, same and same1, on the mirror C.BT(len, t) 14 # (law-shaped, as in proof_ops.bend). Each loop carries the read pair 15 # B.at(BT, s) literally: C.at_pair_t turns it into (BT, AT) so the loop steps, 16 # and the next call reads B.at(BT, s + 1), the same form one index on. 17 18 # List and index facts 19 # ==================== 20 21 def mdisc(m: Maybe<&2, U32>) -> Type: 22 match m: 23 case None{}: 24 Empty 25 case Some{x}: 26 Unit 27 28 law none_some: 29 for -x: U32 30 for e: {None{} == Some{x} : Maybe<&2, U32>} 31 Empty 32 33 def none_some(x, e): 34 %Equal.sym(Maybe<&2, U32>, None{}, Some{x}, e) : mdisc(_) 35 Unit{} 36 37 law drop_zero: 38 for +xs: List<&2, U32> 39 {List.drop(&2, U32, xs, 0n) == xs : List<&2, U32>} 40 41 def drop_zero(xs): 42 match xs: 43 case Nil{}: 44 {==} 45 case Con{x, t}: 46 {==} 47 48 # Dropping j elements, when element j is x: x, then the rest. 49 law drop_get: 50 for +xs: List<&2, U32> 51 for +j: Nat 52 for +x: U32 53 for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>} 54 {List.drop(&2, U32, xs, j) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>} 55 56 def drop_get(xs, j, x, h): 57 match xs j: 58 case Nil{} _: 59 Empty.absurd({List.drop(&2, U32, Nil{}, j) == x <> List.drop(&2, U32, Nil{}, Nat.add(j, 1n)) : List<&2, U32>}, 60 none_some(x, h)) 61 case Con{+y, t} 0n: 62 +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, h) 63 %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) : {y <> t == x <> _ : List<&2, U32>} 64 %Equal.sym(U32, y, x, yx) : {_ <> t == x <> t : List<&2, U32>} 65 {==} 66 case Con{y, t} 1n+p: 67 drop_get(t, p, x, h) 68 69 law slice_cons: 70 for +xs: List<&2, U32> 71 for +j: Nat 72 for +k: Nat 73 for +x: U32 74 for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>} 75 {D.slice(xs, j, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>} 76 77 def slice_cons(xs, j, k, x, h): 78 %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)) : 79 {List.take(&2, U32, _, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>} 80 {==} 81 82 # a + 1 + m <= b gives a < b. 83 law lt_of_le: 84 for +a: Nat 85 for +m: Nat 86 for +b: Nat 87 for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool} 88 {Nat.is_lt(a, b) == True{} : Bool} 89 90 def lt_of_le(a, m, b, h): 91 +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) 92 +h2 = N.le_trans(1n+a, 1n+Nat.add(a, m), b, N.le_add_r(a, m), h1) 93 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) 94 95 # a + 1 + m <= b gives (a + 1) + m <= b. 96 law le_step: 97 for +a: Nat 98 for +m: Nat 99 for +b: Nat 100 for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool} 101 {Nat.is_le(Nat.add(Nat.add(a, 1n), m), b) == True{} : Bool} 102 103 def le_step(a, m, b, h): 104 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), 105 Equal.sym(Nat, Nat.add(Nat.add(a, 1n), m), Nat.add(a, Nat.add(1n, m)), N.add_assoc(a, 1n, m)), h) 106 107 # One step of a read loop at index s with n + 1 left, within a Bytes of size len: 108 # byte s is read, s + 1 does not wrap, and the bound holds one index on. 109 law step_val: 110 for +len: U32 111 for +t: P.Tree 112 for +d: Nat 113 for +s: U32 114 for +m: Nat 115 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 116 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool} 117 {List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s)) == Some{C.AT(len, t, s)} : Maybe<&2, U32>} 118 119 def step_val(len, t, d, s, m, h, hs): 120 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)), 121 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), 122 lt_of_le(U32.to_nat(s), m, U32.to_nat(len), hs))) 123 124 law step_inc: 125 for +len: U32 126 for +t: P.Tree 127 for +d: Nat 128 for +s: U32 129 for +m: Nat 130 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 131 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool} 132 {U32.to_nat((s + 1 : U32)) == Nat.add(U32.to_nat(s), 1n) : Nat} 133 134 def step_inc(len, t, d, s, m, h, hs): 135 C.inc_fits(s, d, C.ok_d(len, t, d, h), 136 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), 137 C.ok_len(len, t, d, h))) 138 139 law step_le: 140 for +len: U32 141 for +t: P.Tree 142 for +d: Nat 143 for +s: U32 144 for +m: Nat 145 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 146 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+m), U32.to_nat(len)) == True{} : Bool} 147 {Nat.is_le(Nat.add(U32.to_nat((s + 1 : U32)), m), U32.to_nat(len)) == True{} : Bool} 148 149 def step_le(len, t, d, s, m, h, hs): 150 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)), 151 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)), 152 le_step(U32.to_nat(s), m, U32.to_nat(len), hs)) 153 154 # to_list 155 # ======= 156 157 law tl_pair: 158 for +n: Nat 159 for +len: U32 160 for +t: P.Tree 161 for +s: U32 162 {B.to_list.go(n, B.at(C.BT(len, t), s), s) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(n, B.at(C.BT(len, t), s), s))) : D.Bytes & List<&2, U32>} 163 164 def tl_pair(n, len, t, s): 165 match n: 166 case 0n: 167 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), C.AT(len, t, s)), C.at_pair_t(len, t, s)) : 168 {B.to_list.go(0n, _, s) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, s))) : D.Bytes & List<&2, U32>} 169 {==} 170 case 1n+m: 171 +s1 = (s + 1 : U32) 172 +x = C.AT(len, t, s) 173 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), x), C.at_pair_t(len, t, s)) : 174 {B.to_list.go(1n+m, _, s) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, _, s))) : D.Bytes & List<&2, U32>} 175 %Equal.sym(D.Bytes & List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1), 176 (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1))), tl_pair(m, len, t, s1)) : 177 {B.to_list.cons(x, _) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, B.to_list.cons(x, _))) : D.Bytes & List<&2, U32>} 178 {==} 179 180 law tl_view: 181 for +n: Nat 182 for +len: U32 183 for +t: P.Tree 184 for +d: Nat 185 for +s: U32 186 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 187 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), n), U32.to_nat(len)) == True{} : Bool} 188 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(n, B.at(C.BT(len, t), s), s)) == D.slice(D.view(C.BT(len, t)), U32.to_nat(s), n) : List<&2, U32>} 189 190 def tl_view(n, len, t, d, s, h, hs): 191 match n: 192 case 0n: 193 +X = List.drop(&2, U32, D.view(C.BT(len, t)), U32.to_nat(s)) 194 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), C.AT(len, t, s)), C.at_pair_t(len, t, s)) : 195 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(0n, _, s)) == List.take(&2, U32, X, 0n) : List<&2, U32>} 196 Equal.sym(List<&2, U32>, List.take(&2, U32, X, 0n), Nil{}, Q.take_zero(X)) 197 case 1n+m: 198 +s1 = (s + 1 : U32) 199 +x = C.AT(len, t, s) 200 +xs = D.view(C.BT(len, t)) 201 +G = Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1)) 202 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), s), (C.BT(len, t), x), C.at_pair_t(len, t, s)) : 203 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.go(1n+m, _, s)) == D.slice(xs, U32.to_nat(s), 1n+m) : List<&2, U32>} 204 %Equal.sym(D.Bytes & List<&2, U32>, B.to_list.go(m, B.at(C.BT(len, t), s1), s1), (C.BT(len, t), G), tl_pair(m, len, t, s1)) : 205 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list.cons(x, _)) == D.slice(xs, U32.to_nat(s), 1n+m) : List<&2, U32>} 206 %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(s), 1n+m), x <> D.slice(xs, Nat.add(U32.to_nat(s), 1n), m), 207 slice_cons(xs, U32.to_nat(s), m, x, step_val(len, t, d, s, m, h, hs))) : 208 {x <> G == _ : List<&2, U32>} 209 %step_inc(len, t, d, s, m, h, hs) : {x <> G == x <> D.slice(xs, _, m) : List<&2, U32>} 210 %tl_view(m, len, t, d, s1, h, step_le(len, t, d, s, m, h, hs)) : {x <> G == x <> _ : List<&2, U32>} 211 {==} 212 213 law to_list_pair_t: 214 for +len: U32 215 for +t: P.Tree 216 for +s: U32 217 for +n: U32 218 {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>} 219 220 def to_list_pair_t(len, t, s, n): 221 tl_pair(U32.to_nat(n), len, t, s) 222 223 law to_list_view_t: 224 for +len: U32 225 for +t: P.Tree 226 for +d: Nat 227 for +s: U32 228 for +n: U32 229 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 230 for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool} 231 {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>} 232 233 def to_list_view_t(len, t, d, s, n, h, hs): 234 tl_view(U32.to_nat(n), len, t, d, s, h, hs) 235 236 # same 237 # ==== 238 239 law and_assoc: 240 for +a: Bool 241 for +b: Bool 242 for +c: Bool 243 {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool} 244 245 def and_assoc(a, b, c): 246 match a: 247 case False{}: 248 {==} 249 case True{}: 250 {==} 251 252 # Comparing n more bytes from i of A and from j of B, after an empty prefix: 253 # acc and the comparison of the two slices. 254 law lists_end: 255 for +acc: Bool 256 for +xs: List<&2, U32> 257 for +ys: List<&2, U32> 258 {acc == Bool.and(acc, D.list_eq(List.take(&2, U32, xs, 0n), List.take(&2, U32, ys, 0n))) : Bool} 259 260 def lists_end(acc, xs, ys): 261 %Equal.sym(List<&2, U32>, List.take(&2, U32, xs, 0n), Nil{}, Q.take_zero(xs)) : 262 {acc == Bool.and(acc, D.list_eq(_, List.take(&2, U32, ys, 0n))) : Bool} 263 %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : 264 {acc == Bool.and(acc, D.list_eq(Nil{}, _)) : Bool} 265 Equal.sym(Bool, Bool.and(acc, True{}), acc, N.and_true_r_id(acc)) 266 267 # One step of a comparison loop: the two slices from x and y, with the 268 # accumulated test rebracketed. 269 law lists_step: 270 for +acc: Bool 271 for +xs: List<&2, U32> 272 for +ys: List<&2, U32> 273 for +i: Nat 274 for +j: Nat 275 for +i1: U32 276 for +j1: U32 277 for +k: Nat 278 for +x: U32 279 for +y: U32 280 for +hx: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>} 281 for +hy: {List.get(&2, U32, ys, j) == Some{y} : Maybe<&2, U32>} 282 for +ei: {U32.to_nat(i1) == Nat.add(i, 1n) : Nat} 283 for +ej: {U32.to_nat(j1) == Nat.add(j, 1n) : Nat} 284 {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))) 285 == Bool.and(acc, D.list_eq(D.slice(xs, i, 1n+k), D.slice(ys, j, 1n+k))) : Bool} 286 287 def lists_step(acc, xs, ys, i, j, i1, j1, k, x, y, hx, hy, ei, ej): 288 +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))) 289 %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)) : 290 {LHS == Bool.and(acc, D.list_eq(_, D.slice(ys, j, 1n+k))) : Bool} 291 %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)) : 292 {LHS == Bool.and(acc, D.list_eq(x <> D.slice(xs, Nat.add(i, 1n), k), _)) : Bool} 293 %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} 294 %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} 295 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))) 296 297 law sm_pair: 298 for +n: Nat 299 for +la: U32 300 for +ta: P.Tree 301 for +lb: U32 302 for +tb: P.Tree 303 for +i: U32 304 for +j: U32 305 for +acc: Bool 306 {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), 307 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)} 308 309 def sm_pair(n, la, ta, lb, tb, i, j, acc): 310 match n: 311 case 0n: 312 %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)) : 313 {B.same.go(0n, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 314 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)} 315 %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)) : 316 {B.same.go(0n, (C.BT(la, ta), C.AT(la, ta, i)), _, i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 317 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)} 318 {==} 319 case 1n+k: 320 %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)) : 321 {B.same.go(1n+k, _, B.at(C.BT(lb, tb), j), i, j, acc) == (C.BT(la, ta), (C.BT(lb, tb), 322 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)} 323 %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)) : 324 {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), 325 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)} 326 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))) 327 328 law sm_view: 329 for +n: Nat 330 for +la: U32 331 for +ta: P.Tree 332 for +lb: U32 333 for +tb: P.Tree 334 for +d: Nat 335 for +e: Nat 336 for +i: U32 337 for +j: U32 338 for +acc: Bool 339 for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool} 340 for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool} 341 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(la)) == True{} : Bool} 342 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(lb)) == True{} : Bool} 343 {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))) 344 == 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} 345 346 def sm_view(n, la, ta, lb, tb, d, e, i, j, acc, ha, hb, hi, hj): 347 match n: 348 case 0n: 349 +xa = D.view(C.BT(la, ta)) 350 +xb = D.view(C.BT(lb, tb)) 351 +RHS = Bool.and(acc, D.list_eq(D.slice(xa, U32.to_nat(i), 0n), D.slice(xb, U32.to_nat(j), 0n))) 352 %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)) : 353 {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} 354 %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)) : 355 {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} 356 lists_end(acc, List.drop(&2, U32, xa, U32.to_nat(i)), List.drop(&2, U32, xb, U32.to_nat(j))) 357 case 1n+k: 358 +xa = D.view(C.BT(la, ta)) 359 +xb = D.view(C.BT(lb, tb)) 360 +x = C.AT(la, ta, i) 361 +y = C.AT(lb, tb, j) 362 +i1 = (i + 1 : U32) 363 +j1 = (j + 1 : U32) 364 +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))) 365 %Equal.sym(D.Bytes & U32, B.at(C.BT(la, ta), i), (C.BT(la, ta), x), C.at_pair_t(la, ta, i)) : 366 {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} 367 %Equal.sym(D.Bytes & U32, B.at(C.BT(lb, tb), j), (C.BT(lb, tb), y), C.at_pair_t(lb, tb, j)) : 368 {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} 369 %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)))), 370 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))), 371 sm_view(k, la, ta, lb, tb, d, e, i1, j1, acc && U32.is_eq(x, y), ha, hb, 372 step_le(la, ta, d, i, k, ha, hi), step_le(lb, tb, e, j, k, hb, hj))) : 373 {_ == RHS : Bool} 374 lists_step(acc, xa, xb, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y, 375 step_val(la, ta, d, i, k, ha, hi), step_val(lb, tb, e, j, k, hb, hj), 376 step_inc(la, ta, d, i, k, ha, hi), step_inc(lb, tb, e, j, k, hb, hj)) 377 378 law same_pair_t: 379 for +la: U32 380 for +ta: P.Tree 381 for +lb: U32 382 for +tb: P.Tree 383 for +i: U32 384 for +j: U32 385 for +n: U32 386 {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)} 387 388 def same_pair_t(la, ta, lb, tb, i, j, n): 389 sm_pair(U32.to_nat(n), la, ta, lb, tb, i, j, True{}) 390 391 law same_view_t: 392 for +la: U32 393 for +ta: P.Tree 394 for +lb: U32 395 for +tb: P.Tree 396 for +d: Nat 397 for +e: Nat 398 for +i: U32 399 for +j: U32 400 for +n: U32 401 for +ha: {D.ok(C.BT(la, ta), d) == True{} : Bool} 402 for +hb: {D.ok(C.BT(lb, tb), e) == True{} : Bool} 403 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(la, ta))) == True{} : Bool} 404 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(lb, tb))) == True{} : Bool} 405 {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} 406 407 def same_view_t(la, ta, lb, tb, d, e, i, j, n, ha, hb, hi, hj): 408 sm_view(U32.to_nat(n), la, ta, lb, tb, d, e, i, j, True{}, ha, hb, hi, hj) 409 410 # same1 (two reads of one buffer per step, through at2) 411 # ===================================================== 412 413 law at2_eq: 414 for +len: U32 415 for +t: P.Tree 416 for +i: U32 417 for +j: U32 418 {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)} 419 420 def at2_eq(len, t, i, j): 421 %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)) : 422 {B.at2.fin(j, _) == (C.BT(len, t), (C.AT(len, t, i), C.AT(len, t, j))) : D.Bytes & (U32 & U32)} 423 %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)) : 424 {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)} 425 {==} 426 427 law s1_pair: 428 for +n: Nat 429 for +len: U32 430 for +t: P.Tree 431 for +i: U32 432 for +j: U32 433 for +acc: Bool 434 {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} 435 436 def s1_pair(n, len, t, i, j, acc): 437 match n: 438 case 0n: 439 %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)) : 440 {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} 441 {==} 442 case 1n+m: 443 %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)) : 444 {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} 445 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))) 446 447 law s1_view: 448 for +n: Nat 449 for +len: U32 450 for +t: P.Tree 451 for +d: Nat 452 for +i: U32 453 for +j: U32 454 for +acc: Bool 455 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 456 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), n), U32.to_nat(len)) == True{} : Bool} 457 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool} 458 {Pair.snd(D.Bytes, Bool, B.same1.go(n, B.at2(C.BT(len, t), i, j), i, j, acc)) 459 == 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} 460 461 def s1_view(n, len, t, d, i, j, acc, h, hi, hj): 462 match n: 463 case 0n: 464 +xs = D.view(C.BT(len, t)) 465 %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)) : 466 {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} 467 lists_end(acc, List.drop(&2, U32, xs, U32.to_nat(i)), List.drop(&2, U32, xs, U32.to_nat(j))) 468 case 1n+k: 469 +xs = D.view(C.BT(len, t)) 470 +x = C.AT(len, t, i) 471 +y = C.AT(len, t, j) 472 +i1 = (i + 1 : U32) 473 +j1 = (j + 1 : U32) 474 +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))) 475 %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)) : 476 {Pair.snd(D.Bytes, Bool, B.same1.go(1n+k, _, i, j, acc)) == RHS : Bool} 477 %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))), 478 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))), 479 s1_view(k, len, t, d, i1, j1, acc && U32.is_eq(x, y), h, 480 step_le(len, t, d, i, k, h, hi), step_le(len, t, d, j, k, h, hj))) : 481 {_ == RHS : Bool} 482 lists_step(acc, xs, xs, U32.to_nat(i), U32.to_nat(j), i1, j1, k, x, y, 483 step_val(len, t, d, i, k, h, hi), step_val(len, t, d, j, k, h, hj), 484 step_inc(len, t, d, i, k, h, hi), step_inc(len, t, d, j, k, h, hj)) 485 486 law same1_pair_t: 487 for +len: U32 488 for +t: P.Tree 489 for +i: U32 490 for +j: U32 491 for +n: U32 492 {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} 493 494 def same1_pair_t(len, t, i, j, n): 495 s1_pair(U32.to_nat(n), len, t, i, j, True{}) 496 497 law same1_view_t: 498 for +len: U32 499 for +t: P.Tree 500 for +d: Nat 501 for +i: U32 502 for +j: U32 503 for +n: U32 504 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 505 for +hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool} 506 for +hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(C.BT(len, t))) == True{} : Bool} 507 {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} 508 509 def same1_view_t(len, t, d, i, j, n, h, hi, hj): 510 s1_view(U32.to_nat(n), len, t, d, i, j, True{}, h, hi, hj)