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 ./proof_ops.bend as O 7 import lawful-words@0.1.0.0/defs.bend as W 8 import lawful-words@0.1.0.0/proof_nat.bend as N 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 laws about making Bytes: empty, of_list (a loop of pushes) and grow (a 15 # loop copying words into a new block). Blocks made by Array.new are mirrored 16 # by tnew, so every loop runs on mirrors C.BT(len, t). 17 18 # A new block as a tree. 19 def tnew(+d: Nat, +v: U32) -> P.Tree: 20 match d: 21 case 0n: 22 P.TLeaf{v} 23 case 1n+p: 24 P.TNode{tnew(p, v), tnew(p, v)} 25 26 law tnew_eq: 27 for +d: Nat 28 for +v: U32 29 {P.fromT(U32, tnew(d, v)) == Array.new(U32, d, v) : Array} 30 31 def tnew_eq(d, v): 32 match d: 33 case 0n: 34 {==} 35 case 1n+p: 36 P.anode_eq(U32, P.fromT(U32, tnew(p, v)), P.fromT(U32, tnew(p, v)), Array.new(U32, p, v), Array.new(U32, p, v), 37 tnew_eq(p, v), tnew_eq(p, v)) 38 39 law tnew_full: 40 for +d: Nat 41 for +v: U32 42 {A.full(U32, P.fromT(U32, tnew(d, v)), d) == True{} : Bool} 43 44 def tnew_full(d, v): 45 %Equal.sym(Array, P.fromT(U32, tnew(d, v)), Array.new(U32, d, v), tnew_eq(d, v)) : {A.full(U32, _, d) == True{} : Bool} 46 P.new_full(U32, d, v) 47 48 law empty_eq: 49 for +d: Nat 50 {B.empty(d) == C.BT(0, tnew(d, 0)) : D.Bytes} 51 52 def empty_eq(d): 53 %tnew_eq(d, 0) : {D.Bytes{0, _} == C.BT(0, tnew(d, 0)) : D.Bytes} 54 {==} 55 56 # Empty 57 # ===== 58 59 law empty_view: 60 for +d: Nat 61 {D.view(B.empty(d)) == Nil{} : List<&2, U32>} 62 63 def empty_view(d): 64 Q.take_zero(D.unpack(A.view(U32, Array.new(U32, d, 0)))) 65 66 law empty_ok: 67 for +d: Nat 68 for +hd: {Nat.is_le(d, 29n) == True{} : Bool} 69 {D.ok(B.empty(d), d) == True{} : Bool} 70 71 def empty_ok(d, hd): 72 %Equal.sym(D.Bytes, B.empty(d), C.BT(0, tnew(d, 0)), empty_eq(d)) : {D.ok(_, d) == True{} : Bool} 73 C.ok_mk(0, tnew(d, 0), d, tnew_full(d, 0), hd, I.le0(Nat.mul(4n, Nat.pow(2n, d)))) 74 75 # Lists 76 # ===== 77 78 law append_nil: 79 for +xs: List<&2, U32> 80 {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>} 81 82 def append_nil(xs): 83 match xs: 84 case Nil{}: 85 {==} 86 case Con{x, t}: 87 %append_nil(t) : {x <> List.append(&2, U32, t, Nil{}) == x <> _ : List<&2, U32>} 88 {==} 89 90 law app_snoc: 91 for +xs: List<&2, U32> 92 for +x: U32 93 for +r: List<&2, U32> 94 {List.append(&2, U32, List.append(&2, U32, xs, [x]), r) == List.append(&2, U32, xs, x <> r) : List<&2, U32>} 95 96 def app_snoc(xs, x, r): 97 match xs: 98 case Nil{}: 99 {==} 100 case Con{y, t}: 101 %app_snoc(t, x, r) : {y <> List.append(&2, U32, List.append(&2, U32, t, [x]), r) == y <> _ : List<&2, U32>} 102 {==} 103 104 # of_list 105 # ======= 106 107 # Room for one more byte when the rest of the list still fits. 108 law ol_room: 109 for +len: U32 110 for +r: Nat 111 for +m: Nat 112 for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), 1n+r), m) == True{} : Bool} 113 {Nat.is_lt(U32.to_nat(len), m) == True{} : Bool} 114 115 def ol_room(len, r, m, hn): 116 +L = U32.to_nat(len) 117 +h1 = AB.subst(Nat, x => {Nat.is_le(x, m) == True{} : Bool}, Nat.add(L, 1n+r), 1n+Nat.add(L, r), N.add_succ(L, r), hn) 118 +h2 = Equal.trans(Bool, Nat.is_lt(Nat.add(L, r), m), Nat.is_le(1n+Nat.add(L, r), m), True{}, 119 Equal.sym(Bool, Nat.is_le(1n+Nat.add(L, r), m), Nat.is_lt(Nat.add(L, r), m), N.le_succ_lt(Nat.add(L, r), m)), h1) 120 N.le_lt_trans(L, Nat.add(L, r), m, N.le_add_r(L, r), h2) 121 122 # The rest still fits after the push. 123 law ol_rest: 124 for +len: U32 125 for +d: Nat 126 for +r: Nat 127 for +hd: {Nat.is_le(d, 29n) == True{} : Bool} 128 for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), 1n+r), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} 129 {Nat.is_le(Nat.add(U32.to_nat((len + 1 : U32)), r), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} 130 131 def ol_rest(len, d, r, hd, hn): 132 +L = U32.to_nat(len) 133 +M = Nat.mul(4n, Nat.pow(2n, d)) 134 %Equal.sym(Nat, U32.to_nat((len + 1 : U32)), Nat.add(L, 1n), C.inc_fits(len, d, hd, ol_room(len, r, M, hn))) : 135 {Nat.is_le(Nat.add(_, r), M) == True{} : Bool} 136 %Equal.sym(Nat, Nat.add(Nat.add(L, 1n), r), Nat.add(L, Nat.add(1n, r)), N.add_assoc(L, 1n, r)) : {Nat.is_le(_, M) == True{} : Bool} 137 hn 138 139 law ol_go_view: 140 for +xs: List<&2, U32> 141 for +len: U32 142 for +t: P.Tree 143 for +d: Nat 144 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 145 for +hb: {D.all_bytes(xs) == True{} : Bool} 146 for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), List.length(&2, U32, xs)), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} 147 {D.view(B.of_list.go(xs, C.BT(len, t))) == List.append(&2, U32, D.view(C.BT(len, t)), xs) : List<&2, U32>} 148 149 def ol_go_view(xs, len, t, d, h, hb, hn): 150 match xs: 151 case Nil{}: 152 Equal.sym(List<&2, U32>, List.append(&2, U32, D.view(C.BT(len, t)), Nil{}), D.view(C.BT(len, t)), append_nil(D.view(C.BT(len, t)))) 153 case Con{+x, rest}: 154 +k = (len >> 2n : U32) 155 +t2 = I.set_tree(U32, t, k, W.put_byte(C.WD(t, k), U32.to_nat((len .&. 3 : U32)), x)) 156 +l2 = (len + 1 : U32) 157 +M = Nat.mul(4n, Nat.pow(2n, d)) 158 +hd = C.ok_d(len, t, d, h) 159 +hr = ol_room(len, List.length(&2, U32, rest), M, hn) 160 +hc = AB.subst(Nat, y => {Nat.is_lt(U32.to_nat(len), y) == True{} : Bool}, M, D.cap(C.BT(len, t)), 161 Equal.sym(Nat, D.cap(C.BT(len, t)), M, O.cap_ok_t(len, t, d, h)), hr) 162 +pe = O.push_eq_t(len, t, x) 163 +hv = AB.and_true_l(U32.is_lt(x, 256), D.all_bytes(rest), hb) 164 +h2 = AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.push(C.BT(len, t), x), C.BT(l2, t2), pe, 165 O.push_ok_t(len, t, d, x, h, hc)) 166 +pv = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, D.view(C.BT(len, t)), [x]) : List<&2, U32>}, 167 B.push(C.BT(len, t), x), C.BT(l2, t2), pe, O.push_view_t(len, t, d, x, h, hc, hv)) 168 +RHS = List.append(&2, U32, D.view(C.BT(len, t)), x <> rest) 169 %Equal.sym(D.Bytes, B.push(C.BT(len, t), x), C.BT(l2, t2), pe) : {D.view(B.of_list.go(rest, _)) == RHS : List<&2, U32>} 170 %Equal.sym(List<&2, U32>, D.view(B.of_list.go(rest, C.BT(l2, t2))), List.append(&2, U32, D.view(C.BT(l2, t2)), rest), 171 ol_go_view(rest, l2, t2, d, h2, AB.and_true_r(U32.is_lt(x, 256), D.all_bytes(rest), hb), 172 ol_rest(len, d, List.length(&2, U32, rest), hd, hn))) : 173 {_ == RHS : List<&2, U32>} 174 %Equal.sym(List<&2, U32>, D.view(C.BT(l2, t2)), List.append(&2, U32, D.view(C.BT(len, t)), [x]), pv) : 175 {List.append(&2, U32, _, rest) == RHS : List<&2, U32>} 176 app_snoc(D.view(C.BT(len, t)), x, rest) 177 178 law ol_go_ok: 179 for +xs: List<&2, U32> 180 for +len: U32 181 for +t: P.Tree 182 for +d: Nat 183 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 184 for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), List.length(&2, U32, xs)), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} 185 {D.ok(B.of_list.go(xs, C.BT(len, t)), d) == True{} : Bool} 186 187 def ol_go_ok(xs, len, t, d, h, hn): 188 match xs: 189 case Nil{}: 190 h 191 case Con{+x, rest}: 192 +k = (len >> 2n : U32) 193 +t2 = I.set_tree(U32, t, k, W.put_byte(C.WD(t, k), U32.to_nat((len .&. 3 : U32)), x)) 194 +l2 = (len + 1 : U32) 195 +M = Nat.mul(4n, Nat.pow(2n, d)) 196 +hd = C.ok_d(len, t, d, h) 197 +hr = ol_room(len, List.length(&2, U32, rest), M, hn) 198 +hc = AB.subst(Nat, y => {Nat.is_lt(U32.to_nat(len), y) == True{} : Bool}, M, D.cap(C.BT(len, t)), 199 Equal.sym(Nat, D.cap(C.BT(len, t)), M, O.cap_ok_t(len, t, d, h)), hr) 200 +pe = O.push_eq_t(len, t, x) 201 +h2 = AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.push(C.BT(len, t), x), C.BT(l2, t2), pe, 202 O.push_ok_t(len, t, d, x, h, hc)) 203 %Equal.sym(D.Bytes, B.push(C.BT(len, t), x), C.BT(l2, t2), pe) : {D.ok(B.of_list.go(rest, _), d) == True{} : Bool} 204 ol_go_ok(rest, l2, t2, d, h2, ol_rest(len, d, List.length(&2, U32, rest), hd, hn)) 205 206 law of_list_view: 207 for +d: Nat 208 for +xs: List<&2, U32> 209 for +hd: {Nat.is_le(d, 29n) == True{} : Bool} 210 for +hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} 211 for +hb: {D.all_bytes(xs) == True{} : Bool} 212 {D.view(B.of_list(d, xs)) == xs : List<&2, U32>} 213 214 def of_list_view(d, xs, hd, hn, hb): 215 +t0 = tnew(d, 0) 216 %Equal.sym(D.Bytes, B.empty(d), C.BT(0, t0), empty_eq(d)) : {D.view(B.of_list.go(xs, _)) == xs : List<&2, U32>} 217 %Equal.sym(List<&2, U32>, D.view(B.of_list.go(xs, C.BT(0, t0))), List.append(&2, U32, D.view(C.BT(0, t0)), xs), 218 ol_go_view(xs, 0, t0, d, C.ok_mk(0, t0, d, tnew_full(d, 0), hd, I.le0(Nat.mul(4n, Nat.pow(2n, d)))), hb, hn)) : 219 {_ == xs : List<&2, U32>} 220 %Equal.sym(List<&2, U32>, List.take(&2, U32, D.unpack(C.WL(t0)), 0n), Nil{}, Q.take_zero(D.unpack(C.WL(t0)))) : 221 {List.append(&2, U32, _, xs) == xs : List<&2, U32>} 222 {==} 223 224 law of_list_ok: 225 for +d: Nat 226 for +xs: List<&2, U32> 227 for +hd: {Nat.is_le(d, 29n) == True{} : Bool} 228 for +hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} 229 {D.ok(B.of_list(d, xs), d) == True{} : Bool} 230 231 def of_list_ok(d, xs, hd, hn): 232 +t0 = tnew(d, 0) 233 %Equal.sym(D.Bytes, B.empty(d), C.BT(0, t0), empty_eq(d)) : {D.ok(B.of_list.go(xs, _), d) == True{} : Bool} 234 ol_go_ok(xs, 0, t0, d, C.ok_mk(0, t0, d, tnew_full(d, 0), hd, I.le0(Nat.mul(4n, Nat.pow(2n, d)))), hn) 235 236 # grow 237 # ==== 238 239 # The tree grow.go builds from td: words i .. i+n-1 of t written in. 240 def gtree(n: Nat, +t: P.Tree, +td: P.Tree, +i: U32) -> P.Tree: 241 match n: 242 case 0n: 243 td 244 case 1n+k: 245 gtree(k, t, I.set_tree(U32, td, i, C.WD(t, i)), (i + 1 : U32)) 246 247 law ggo: 248 for +n: Nat 249 for +t: P.Tree 250 for +td: P.Tree 251 for +i: U32 252 {B.grow.go(n, Array.get(U32, P.fromT(U32, t), i), P.fromT(U32, td), i) == P.fromT(U32, gtree(n, t, td, i)) : Array} 253 254 def ggo(n, t, td, i): 255 match n: 256 case 0n: 257 %Equal.sym(Array & U32, Array.get(U32, P.fromT(U32, t), i), (P.fromT(U32, t), C.WD(t, i)), P.get_pair_t(U32, t, i)) : 258 {B.grow.go(0n, _, P.fromT(U32, td), i) == P.fromT(U32, td) : Array} 259 {==} 260 case 1n+k: 261 +w = C.WD(t, i) 262 +i1 = (i + 1 : U32) 263 %Equal.sym(Array & U32, Array.get(U32, P.fromT(U32, t), i), (P.fromT(U32, t), w), P.get_pair_t(U32, t, i)) : 264 {B.grow.go(1n+k, _, P.fromT(U32, td), i) == P.fromT(U32, gtree(1n+k, t, td, i)) : Array} 265 %Equal.sym(Array, Array.set(U32, P.fromT(U32, td), i, w), P.fromT(U32, I.set_tree(U32, td, i, w)), I.set_tree_eq(U32, td, i, w)) : 266 {B.grow.go(k, Array.get(U32, P.fromT(U32, t), i1), _, i1) == P.fromT(U32, gtree(k, t, I.set_tree(U32, td, i, w), i1)) : Array} 267 ggo(k, t, I.set_tree(U32, td, i, w), i1) 268 269 law grow_eq: 270 for +len: U32 271 for +t: P.Tree 272 for +d: Nat 273 for +e: Nat 274 for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool} 275 {B.grow(C.BT(len, t), e) == C.BT(len, gtree(U32.to_nat(U32.shln(1, d)), t, tnew(e, 0), 0)) : D.Bytes} 276 277 def grow_eq(len, t, d, e, hf): 278 +N0 = U32.to_nat(U32.shln(1, d)) 279 %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)) : 280 {B.grow.fin(len, e, _) == C.BT(len, gtree(N0, t, tnew(e, 0), 0)) : D.Bytes} 281 %tnew_eq(e, 0) : {D.Bytes{len, B.grow.go(N0, Array.get(U32, P.fromT(U32, t), 0), _, 0)} == C.BT(len, gtree(N0, t, tnew(e, 0), 0)) : D.Bytes} 282 %Equal.sym(Array, B.grow.go(N0, Array.get(U32, P.fromT(U32, t), 0), P.fromT(U32, tnew(e, 0)), 0), 283 P.fromT(U32, gtree(N0, t, tnew(e, 0), 0)), ggo(N0, t, tnew(e, 0), 0)) : 284 {D.Bytes{len, _} == C.BT(len, gtree(N0, t, tnew(e, 0), 0)) : D.Bytes} 285 {==} 286 287 law gfull: 288 for +n: Nat 289 for +t: P.Tree 290 for +td: P.Tree 291 for +i: U32 292 for +e: Nat 293 for +hf: {A.full(U32, P.fromT(U32, td), e) == True{} : Bool} 294 {A.full(U32, P.fromT(U32, gtree(n, t, td, i)), e) == True{} : Bool} 295 296 def gfull(n, t, td, i, e, hf): 297 match n: 298 case 0n: 299 hf 300 case 1n+k: 301 gfull(k, t, I.set_tree(U32, td, i, C.WD(t, i)), (i + 1 : U32), e, C.full_set(td, e, i, C.WD(t, i), hf)) 302 303 def mtag(m: Maybe<&2, U32>) -> Bool: 304 match m: 305 case None{}: 306 False{} 307 case Some{x}: 308 True{} 309 310 law take_succ_get: 311 for +xs: List<&2, U32> 312 for +j: Nat 313 for +w: U32 314 for +hg: {List.get(&2, U32, xs, j) == Some{w} : Maybe<&2, U32>} 315 {List.take(&2, U32, xs, Nat.add(j, 1n)) == List.append(&2, U32, List.take(&2, U32, xs, j), [w]) : List<&2, U32>} 316 317 def take_succ_get(xs, j, w, hg): 318 match xs j: 319 case Nil{} _: 320 Empty.absurd({List.take(&2, U32, Nil{}, Nat.add(j, 1n)) == List.append(&2, U32, Nil{}, [w]) : List<&2, U32>}, 321 AB.false_ne_true(Equal.cong(Maybe<&2, U32>, Bool, m => mtag(m), None{}, Some{w}, hg))) 322 case Con{+x, r} 0n: 323 +xw = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, x, m), Some{x}, Some{w}, hg) 324 %Equal.sym(List<&2, U32>, List.take(&2, U32, r, 0n), Nil{}, Q.take_zero(r)) : {x <> _ == [w] : List<&2, U32>} 325 %Equal.sym(U32, x, w, xw) : {_ <> Nil{} == [w] : List<&2, U32>} 326 {==} 327 case Con{+x, r} 1n+p: 328 %take_succ_get(r, p, w, hg) : {x <> List.take(&2, U32, r, Nat.add(p, 1n)) == x <> _ : List<&2, U32>} 329 {==} 330 331 law take_all: 332 for +xs: List<&2, U32> 333 {List.take(&2, U32, xs, List.length(&2, U32, xs)) == xs : List<&2, U32>} 334 335 def take_all(xs): 336 match xs: 337 case Nil{}: 338 {==} 339 case Con{x, r}: 340 %take_all(r) : {x <> List.take(&2, U32, r, List.length(&2, U32, r)) == x <> _ : List<&2, U32>} 341 {==} 342 343 # Only the first q words matter for the first m <= 4q bytes. 344 law ut: 345 for +ws: List<&2, U32> 346 for +q: Nat 347 for +m: Nat 348 for +h: {Nat.is_le(m, Nat.mul(q, 4n)) == True{} : Bool} 349 {List.take(&2, U32, D.unpack(ws), m) == List.take(&2, U32, D.unpack(List.take(&2, U32, ws, q)), m) : List<&2, U32>} 350 351 def ut(ws, q, m, h): 352 match ws q m: 353 case Nil{} _ _: 354 {==} 355 case Con{w, r} 0n 0n: 356 {==} 357 case Con{w, r} 0n 1n+m1: 358 Empty.absurd({List.take(&2, U32, D.unpack(w <> r), 1n+m1) == Nil{} : List<&2, U32>}, AB.false_ne_true(h)) 359 case Con{+w, r} 1n+p 0n: 360 {==} 361 case Con{+w, r} 1n+p 1n+m1: 362 match m1: 363 case 0n: 364 {==} 365 case 1n+m2: 366 match m2: 367 case 0n: 368 {==} 369 case 1n+m3: 370 match m3: 371 case 0n: 372 {==} 373 case 1n+m4: 374 %ut(r, p, m4, h) : 375 {W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> List.take(&2, U32, D.unpack(r), m4) == 376 W.byte(w, 0n) <> W.byte(w, 1n) <> W.byte(w, 2n) <> W.byte(w, 3n) <> _ : List<&2, U32>} 377 {==} 378 379 # Writing word i keeps the copied prefix and extends it by one word. 380 law ginv: 381 for +t: P.Tree 382 for +td: P.Tree 383 for +i: U32 384 for +d: Nat 385 for +e: Nat 386 for +hft: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool} 387 for +hfd: {A.full(U32, P.fromT(U32, td), e) == True{} : Bool} 388 for +hd: {Nat.is_le(d, 29n) == True{} : Bool} 389 for +he29: {Nat.is_le(e, 29n) == True{} : Bool} 390 for +hjd: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool} 391 for +hje: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, e)) == True{} : Bool} 392 for +ei1: {U32.to_nat((i + 1 : U32)) == Nat.add(U32.to_nat(i), 1n) : Nat} 393 for +hinv: {List.take(&2, U32, C.WL(td), U32.to_nat(i)) == List.take(&2, U32, C.WL(t), U32.to_nat(i)) : List<&2, U32>} 394 {List.take(&2, U32, C.WL(I.set_tree(U32, td, i, C.WD(t, i))), U32.to_nat((i + 1 : U32))) == List.take(&2, U32, C.WL(t), U32.to_nat((i + 1 : U32))) : List<&2, U32>} 395 396 def ginv(t, td, i, d, e, hft, hfd, hd, he29, hjd, hje, ei1, hinv): 397 +j = U32.to_nat(i) 398 +w = C.WD(t, i) 399 +td2 = I.set_tree(U32, td, i, w) 400 %Equal.sym(Nat, U32.to_nat((i + 1 : U32)), Nat.add(j, 1n), ei1) : 401 {List.take(&2, U32, C.WL(td2), _) == List.take(&2, U32, C.WL(t), _) : List<&2, U32>} 402 %Equal.sym(List<&2, U32>, C.WL(td2), List.set(&2, U32, C.WL(td), j, w), C.wl_set(td, e, i, w, hfd, he29, hje)) : 403 {List.take(&2, U32, _, Nat.add(j, 1n)) == List.take(&2, U32, C.WL(t), Nat.add(j, 1n)) : List<&2, U32>} 404 +hlen = AB.subst(Nat, x => {Nat.is_lt(j, x) == True{} : Bool}, Nat.pow(2n, e), List.length(&2, U32, C.WL(td)), 405 Equal.sym(Nat, List.length(&2, U32, C.WL(td)), Nat.pow(2n, e), P.view_length(U32, e, td, hfd)), hje) 406 %Equal.sym(List<&2, U32>, List.take(&2, U32, List.set(&2, U32, C.WL(td), j, w), Nat.add(j, 1n)), 407 List.append(&2, U32, List.take(&2, U32, C.WL(td), j), [w]), Q.take_set_succ(C.WL(td), j, w, hlen)) : 408 {_ == List.take(&2, U32, C.WL(t), Nat.add(j, 1n)) : List<&2, U32>} 409 %Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(td), j), List.take(&2, U32, C.WL(t), j), hinv) : 410 {List.append(&2, U32, _, [w]) == List.take(&2, U32, C.WL(t), Nat.add(j, 1n)) : List<&2, U32>} 411 Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(t), Nat.add(j, 1n)), List.append(&2, U32, List.take(&2, U32, C.WL(t), j), [w]), 412 take_succ_get(C.WL(t), j, w, C.wd_get(t, d, i, hft, hd, hjd))) 413 414 # The loop copies words i .. i+n-1 of t. 415 law gtake: 416 for +n: Nat 417 for +t: P.Tree 418 for +td: P.Tree 419 for +i: U32 420 for +d: Nat 421 for +e: Nat 422 for +hft: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool} 423 for +hfd: {A.full(U32, P.fromT(U32, td), e) == True{} : Bool} 424 for +hd: {Nat.is_le(d, 29n) == True{} : Bool} 425 for +he: {Nat.is_le(d, e) == True{} : Bool} 426 for +he29: {Nat.is_le(e, 29n) == True{} : Bool} 427 for +hn: {Nat.is_le(Nat.add(U32.to_nat(i), n), Nat.pow(2n, d)) == True{} : Bool} 428 for +hinv: {List.take(&2, U32, C.WL(td), U32.to_nat(i)) == List.take(&2, U32, C.WL(t), U32.to_nat(i)) : List<&2, U32>} 429 {List.take(&2, U32, C.WL(gtree(n, t, td, i)), Nat.add(U32.to_nat(i), n)) == List.take(&2, U32, C.WL(t), Nat.add(U32.to_nat(i), n)) : List<&2, U32>} 430 431 def gtake(n, t, td, i, d, e, hft, hfd, hd, he, he29, hn, hinv): 432 match n: 433 case 0n: 434 +j = U32.to_nat(i) 435 %Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)) : 436 {List.take(&2, U32, C.WL(td), _) == List.take(&2, U32, C.WL(t), _) : List<&2, U32>} 437 hinv 438 case 1n+k: 439 +j = U32.to_nat(i) 440 +w = C.WD(t, i) 441 +i1 = (i + 1 : U32) 442 +td2 = I.set_tree(U32, td, i, w) 443 +Pd = Nat.pow(2n, d) 444 +hjd = ol_room(i, k, Pd, hn) 445 +hje = N.lt_le_trans(j, Pd, Nat.pow(2n, e), hjd, N.pow_le(d, e, he)) 446 +hj4 = N.lt_le_trans(j, Pd, Nat.mul(4n, Pd), hjd, N.le_add_r(Pd, Nat.mul(3n, Pd))) 447 +ei1 = C.inc_fits(i, d, hd, hj4) 448 +ek = Equal.trans(Nat, Nat.add(U32.to_nat(i1), k), Nat.add(Nat.add(j, 1n), k), Nat.add(j, 1n+k), 449 Equal.cong(Nat, Nat, x => Nat.add(x, k), U32.to_nat(i1), Nat.add(j, 1n), ei1), N.add_assoc(j, 1n, k)) 450 %ek : {List.take(&2, U32, C.WL(gtree(k, t, td2, i1)), _) == List.take(&2, U32, C.WL(t), _) : List<&2, U32>} 451 gtake(k, t, td2, i1, d, e, hft, C.full_set(td, e, i, w, hfd), hd, he, he29, 452 AB.subst(Nat, x => {Nat.is_le(x, Pd) == True{} : Bool}, Nat.add(j, 1n+k), Nat.add(U32.to_nat(i1), k), 453 Equal.sym(Nat, Nat.add(U32.to_nat(i1), k), Nat.add(j, 1n+k), ek), hn), 454 ginv(t, td, i, d, e, hft, hfd, hd, he29, hjd, hje, ei1, hinv)) 455 456 law grow_view_t: 457 for +len: U32 458 for +t: P.Tree 459 for +d: Nat 460 for +e: Nat 461 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 462 for +he: {Nat.is_le(d, e) == True{} : Bool} 463 for +he29: {Nat.is_le(e, 29n) == True{} : Bool} 464 {D.view(B.grow(C.BT(len, t), e)) == D.view(C.BT(len, t)) : List<&2, U32>} 465 466 def grow_view_t(len, t, d, e, h, he, he29): 467 +hf = C.ok_full(len, t, d, h) 468 +hd = C.ok_d(len, t, d, h) 469 +L = U32.to_nat(len) 470 +N0 = U32.to_nat(U32.shln(1, d)) 471 +Pd = Nat.pow(2n, d) 472 +t0 = tnew(e, 0) 473 +GTR = gtree(N0, t, t0, 0) 474 +RHS = D.view(C.BT(len, t)) 475 +hl4 = AB.subst(Nat, x => {Nat.is_le(L, x) == True{} : Bool}, Nat.mul(4n, Pd), Nat.mul(Pd, 4n), N.mul_comm(4n, Pd), 476 C.ok_len(len, t, d, h)) 477 +hn0 = AB.subst(Nat, x => {Nat.is_le(x, Pd) == True{} : Bool}, Pd, N0, 478 Equal.sym(Nat, N0, Pd, I.size_n(d, C.lt32(d, hd))), N.le_refl(Pd)) 479 +hinv0 = Equal.trans(List<&2, U32>, List.take(&2, U32, C.WL(t0), 0n), Nil{}, List.take(&2, U32, C.WL(t), 0n), 480 Q.take_zero(C.WL(t0)), Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(t), 0n), Nil{}, Q.take_zero(C.WL(t)))) 481 +g1 = AB.subst(Nat, x => {List.take(&2, U32, C.WL(GTR), x) == List.take(&2, U32, C.WL(t), x) : List<&2, U32>}, N0, Pd, 482 I.size_n(d, C.lt32(d, hd)), gtake(N0, t, t0, 0, d, e, hf, tnew_full(e, 0), hd, he, he29, hn0, hinv0)) 483 +tall = AB.subst(Nat, x => {List.take(&2, U32, C.WL(t), x) == C.WL(t) : List<&2, U32>}, List.length(&2, U32, C.WL(t)), Pd, 484 P.view_length(U32, d, t, hf), take_all(C.WL(t))) 485 +e1 = Equal.trans(List<&2, U32>, List.take(&2, U32, C.WL(GTR), Pd), List.take(&2, U32, C.WL(t), Pd), C.WL(t), g1, tall) 486 %Equal.sym(D.Bytes, B.grow(C.BT(len, t), e), C.BT(len, GTR), grow_eq(len, t, d, e, hf)) : {D.view(_) == RHS : List<&2, U32>} 487 %Equal.sym(List<&2, U32>, List.take(&2, U32, D.unpack(C.WL(GTR)), L), List.take(&2, U32, D.unpack(List.take(&2, U32, C.WL(GTR), Pd)), L), 488 ut(C.WL(GTR), Pd, L, hl4)) : 489 {_ == RHS : List<&2, U32>} 490 %Equal.sym(List<&2, U32>, List.take(&2, U32, C.WL(GTR), Pd), C.WL(t), e1) : 491 {List.take(&2, U32, D.unpack(_), L) == RHS : List<&2, U32>} 492 {==} 493 494 law grow_ok_t: 495 for +len: U32 496 for +t: P.Tree 497 for +d: Nat 498 for +e: Nat 499 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 500 for +he: {Nat.is_le(d, e) == True{} : Bool} 501 for +he29: {Nat.is_le(e, 29n) == True{} : Bool} 502 {D.ok(B.grow(C.BT(len, t), e), e) == True{} : Bool} 503 504 def grow_ok_t(len, t, d, e, h, he, he29): 505 +hf = C.ok_full(len, t, d, h) 506 +N0 = U32.to_nat(U32.shln(1, d)) 507 +GTR = gtree(N0, t, tnew(e, 0), 0) 508 %Equal.sym(D.Bytes, B.grow(C.BT(len, t), e), C.BT(len, GTR), grow_eq(len, t, d, e, hf)) : {D.ok(_, e) == True{} : Bool} 509 C.ok_mk(len, GTR, e, gfull(N0, t, tnew(e, 0), 0, e, tnew_full(e, 0)), he29, 510 N.le_trans(U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), Nat.mul(4n, Nat.pow(2n, e)), C.ok_len(len, t, d, h), 511 N.le_mul_l(4n, Nat.pow(2n, d), Nat.pow(2n, e), N.pow_le(d, e, he))))