1 import Base 2 import lawful-bytes@0.1.1.0/defs.bend as D 3 import lawful-bytes@0.1.1.0/bytes.bend as B 4 import ./defs.bend as F 5 import ./fields.bend as FC 6 import lawful-bytes@0.1.1.0/proof_seq.bend as Q 7 import lawful-bytes@0.1.1.0/proof_core.bend as C 8 import lawful-bytes@0.1.1.0/proof_ops.bend as O 9 import lawful-bytes@0.1.1.0/proof_same.bend as SM 10 import lawful-bytes@0.1.1.0/proof_shift.bend as H 11 import lawful-bytes@0.1.1.0/proof_grow.bend as G 12 import lawful-words@0.1.0.0/proof_nat.bend as N 13 import lawful-words@0.1.0.0/proof_u32.bend as U 14 import lawful-arrays@0.1.0.0/proof_base.bend as AB 15 import lawful-arrays@0.1.0.0/proof_tree.bend as P 16 17 # digits and put_dec on the mirror C.BT(len, t) (named `name_t` as in 18 # lawful-bytes@0.1.1.0/proof_ops.bend). 19 20 # digits 21 # ====== 22 23 # Every element is a digit byte (48 to 57). 24 def alld(xs: List<&2, U32>) -> Bool: 25 match xs: 26 case Nil{}: 27 True{} 28 case Con{+x, t}: 29 Bool.and(Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)), alld(t)) 30 31 law and_true: 32 for +a: Bool 33 {Bool.and(a, True{}) == a : Bool} 34 35 def and_true(a): 36 match a: 37 case True{}: 38 {==} 39 case False{}: 40 {==} 41 42 law push_some: 43 for +a: Nat 44 for +x: U32 45 for +b: Bool 46 {Maybe.is_some(&2, Nat, F.dec.push(Some{a}, F.digit.if(x, b))) == b : Bool} 47 48 def push_some(a, x, b): 49 match b: 50 case True{}: 51 {==} 52 case False{}: 53 {==} 54 55 law push_and: 56 for +m: Maybe<&2, Nat> 57 for +x: U32 58 for +r: Bool 59 {Bool.and(Maybe.is_some(&2, Nat, F.dec.push(m, F.digit(x))), r) == Bool.and(Bool.and(Maybe.is_some(&2, Nat, m), Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))), r) : Bool} 60 61 def push_and(m, x, r): 62 match m: 63 case None{}: 64 {==} 65 case Some{+a}: 66 +isd = Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)) 67 %Equal.sym(Bool, Maybe.is_some(&2, Nat, F.dec.push(Some{a}, F.digit.if(x, isd))), isd, push_some(a, x, isd)) : 68 {Bool.and(_, r) == Bool.and(Bool.and(True{}, isd), r) : Bool} 69 {==} 70 71 # dec.go keeps a value exactly while every byte is a digit. 72 law go_some: 73 for +ys: List<&2, U32> 74 for +m: Maybe<&2, Nat> 75 {Maybe.is_some(&2, Nat, F.dec.go(ys, m)) == Bool.and(Maybe.is_some(&2, Nat, m), alld(ys)) : Bool} 76 77 def go_some(ys, m): 78 match ys: 79 case Nil{}: 80 Equal.sym(Bool, Bool.and(Maybe.is_some(&2, Nat, m), True{}), Maybe.is_some(&2, Nat, m), and_true(Maybe.is_some(&2, Nat, m))) 81 case Con{+x, t}: 82 +isd = Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)) 83 +m2 = F.dec.push(m, F.digit(x)) 84 %Equal.sym(Bool, Maybe.is_some(&2, Nat, F.dec.go(t, m2)), Bool.and(Maybe.is_some(&2, Nat, m2), alld(t)), go_some(t, m2)) : 85 {_ == Bool.and(Maybe.is_some(&2, Nat, m), Bool.and(isd, alld(t))) : Bool} 86 %SM.and_assoc(Maybe.is_some(&2, Nat, m), isd, alld(t)) : 87 {Bool.and(Maybe.is_some(&2, Nat, m2), alld(t)) == _ : Bool} 88 push_and(m, x, alld(t)) 89 90 law ne_dec: 91 for +ys: List<&2, U32> 92 for +h: {Nat.is_lt(0n, List.length(&2, U32, ys)) == True{} : Bool} 93 {Maybe.is_some(&2, Nat, F.dec(ys)) == alld(ys) : Bool} 94 95 def ne_dec(ys, h): 96 match ys: 97 case Nil{}: 98 Empty.absurd({Maybe.is_some(&2, Nat, F.dec(Nil{})) == alld(Nil{}) : Bool}, AB.false_ne_true(h)) 99 case Con{+y, t}: 100 go_some(y <> t, Some{0n}) 101 102 law dg_pair: 103 for +n: Nat 104 for +len: U32 105 for +t: P.Tree 106 for +j: U32 107 for +ok: Bool 108 {FC.digits.go(n, B.at(C.BT(len, t), j), j, ok) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits.go(n, B.at(C.BT(len, t), j), j, ok))) : D.Bytes & Bool} 109 110 def dg_pair(n, len, t, j, ok): 111 match n: 112 case 0n: 113 %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)) : 114 {FC.digits.go(0n, _, j, ok) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits.go(0n, _, j, ok))) : D.Bytes & Bool} 115 {==} 116 case 1n+m: 117 +x = C.AT(len, t, j) 118 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) : 119 {FC.digits.go(1n+m, _, j, ok) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits.go(1n+m, _, j, ok))) : D.Bytes & Bool} 120 dg_pair(m, len, t, (j + 1 : U32), Bool.and(ok, Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)))) 121 122 law dg_view: 123 for +n: Nat 124 for +len: U32 125 for +t: P.Tree 126 for +d: Nat 127 for +j: U32 128 for +ok: Bool 129 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 130 for +hs: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool} 131 {Pair.snd(D.Bytes, Bool, FC.digits.go(n, B.at(C.BT(len, t), j), j, ok)) == Bool.and(ok, alld(D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n))) : Bool} 132 133 def dg_view(n, len, t, d, j, ok, h, hs): 134 match n: 135 case 0n: 136 +X = List.drop(&2, U32, D.view(C.BT(len, t)), U32.to_nat(j)) 137 %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)) : 138 {Pair.snd(D.Bytes, Bool, FC.digits.go(0n, _, j, ok)) == Bool.and(ok, alld(List.take(&2, U32, X, 0n))) : Bool} 139 %Equal.sym(List<&2, U32>, List.take(&2, U32, X, 0n), Nil{}, Q.take_zero(X)) : {ok == Bool.and(ok, alld(_)) : Bool} 140 Equal.sym(Bool, Bool.and(ok, True{}), ok, and_true(ok)) 141 case 1n+m: 142 +x = C.AT(len, t, j) 143 +j1 = (j + 1 : U32) 144 +isd = Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)) 145 +xs = D.view(C.BT(len, t)) 146 +RHS = Bool.and(ok, alld(D.slice(xs, U32.to_nat(j), 1n+m))) 147 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) : 148 {Pair.snd(D.Bytes, Bool, FC.digits.go(1n+m, _, j, ok)) == RHS : Bool} 149 %Equal.sym(Bool, Pair.snd(D.Bytes, Bool, FC.digits.go(m, B.at(C.BT(len, t), j1), j1, Bool.and(ok, isd))), 150 Bool.and(Bool.and(ok, isd), alld(D.slice(xs, U32.to_nat(j1), m))), 151 dg_view(m, len, t, d, j1, Bool.and(ok, isd), h, SM.step_le(len, t, d, j, m, h, hs))) : 152 {_ == RHS : Bool} 153 %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(j), 1n+m), x <> D.slice(xs, Nat.add(U32.to_nat(j), 1n), m), 154 SM.slice_cons(xs, U32.to_nat(j), m, x, SM.step_val(len, t, d, j, m, h, hs))) : 155 {Bool.and(Bool.and(ok, isd), alld(D.slice(xs, U32.to_nat(j1), m))) == Bool.and(ok, alld(_)) : Bool} 156 %Equal.sym(Nat, U32.to_nat(j1), Nat.add(U32.to_nat(j), 1n), SM.step_inc(len, t, d, j, m, h, hs)) : 157 {Bool.and(Bool.and(ok, isd), alld(D.slice(xs, _, m))) == Bool.and(ok, Bool.and(isd, alld(D.slice(xs, Nat.add(U32.to_nat(j), 1n), m)))) : Bool} 158 SM.and_assoc(ok, isd, alld(D.slice(xs, Nat.add(U32.to_nat(j), 1n), m))) 159 160 law digits_pair_t: 161 for +len: U32 162 for +t: P.Tree 163 for +from: U32 164 for +to: U32 165 {FC.digits(C.BT(len, t), from, to) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits(C.BT(len, t), from, to))) : D.Bytes & Bool} 166 167 def digits_pair_t(len, t, from, to): 168 dg_pair(Nat.sub(U32.to_nat(to), U32.to_nat(from)), len, t, from, U32.is_lt(from, to)) 169 170 # The start test of digits against the slice it reads. 171 law dtop: 172 for +n: Nat 173 for +from: U32 174 for +to: U32 175 for +xs: List<&2, U32> 176 for +hn: {Nat.sub(U32.to_nat(to), U32.to_nat(from)) == n : Nat} 177 for +hle: {Nat.is_le(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool} 178 for +hlen: {Nat.is_le(Nat.add(U32.to_nat(from), n), List.length(&2, U32, xs)) == True{} : Bool} 179 {Bool.and(U32.is_lt(from, to), alld(D.slice(xs, U32.to_nat(from), n))) == Maybe.is_some(&2, Nat, F.dec(D.slice(xs, U32.to_nat(from), n))) : Bool} 180 181 def dtop(n, from, to, xs, hn, hle, hlen): 182 match n: 183 case 0n: 184 +FF = U32.to_nat(from) 185 +TT = U32.to_nat(to) 186 +X = List.drop(&2, U32, xs, FF) 187 +e1 = AB.subst(Nat, y => {Nat.add(FF, y) == TT : Nat}, Nat.sub(TT, FF), 0n, hn, N.le_sub_add(FF, TT, hle)) 188 +eFT = Equal.trans(Nat, FF, Nat.add(FF, 0n), TT, Equal.sym(Nat, Nat.add(FF, 0n), FF, N.add_zero(FF)), e1) 189 +hlt = Equal.trans(Bool, U32.is_lt(from, to), Nat.is_lt(FF, TT), False{}, U.is_lt_to_nat(from, to), 190 AB.subst(Nat, y => {Nat.is_lt(FF, y) == False{} : Bool}, FF, TT, eFT, N.lt_irrefl(FF))) 191 %Equal.sym(List<&2, U32>, List.take(&2, U32, X, 0n), Nil{}, Q.take_zero(X)) : 192 {Bool.and(U32.is_lt(from, to), alld(_)) == Maybe.is_some(&2, Nat, F.dec(_)) : Bool} 193 %Equal.sym(Bool, U32.is_lt(from, to), False{}, hlt) : {Bool.and(_, True{}) == False{} : Bool} 194 {==} 195 case 1n+k: 196 +FF = U32.to_nat(from) 197 +TT = U32.to_nat(to) 198 +X = List.drop(&2, U32, xs, FF) 199 +S = D.slice(xs, FF, 1n+k) 200 +e1 = AB.subst(Nat, y => {Nat.add(FF, y) == TT : Nat}, Nat.sub(TT, FF), 1n+k, hn, N.le_sub_add(FF, TT, hle)) 201 +hlt = Equal.trans(Bool, U32.is_lt(from, to), Nat.is_lt(FF, TT), True{}, U.is_lt_to_nat(from, to), 202 SM.lt_of_le(FF, k, TT, AB.subst(Nat, y => {Nat.is_le(y, TT) == True{} : Bool}, TT, Nat.add(FF, 1n+k), 203 Equal.sym(Nat, Nat.add(FF, 1n+k), TT, e1), N.le_refl(TT)))) 204 +hx = AB.subst(Nat, y => {Nat.is_le(1n+k, y) == True{} : Bool}, Nat.sub(List.length(&2, U32, xs), FF), List.length(&2, U32, X), 205 Equal.sym(Nat, List.length(&2, U32, X), Nat.sub(List.length(&2, U32, xs), FF), H.drop_length(xs, FF)), 206 N.le_sub_r(FF, 1n+k, List.length(&2, U32, xs), hlen)) 207 +hne = AB.subst(Nat, y => {Nat.is_lt(0n, y) == True{} : Bool}, 1n+k, List.length(&2, U32, S), 208 Equal.sym(Nat, List.length(&2, U32, S), 1n+k, Q.take_length(X, 1n+k, hx)), {==}) 209 %Equal.sym(Bool, U32.is_lt(from, to), True{}, hlt) : {Bool.and(_, alld(S)) == Maybe.is_some(&2, Nat, F.dec(S)) : Bool} 210 Equal.sym(Bool, Maybe.is_some(&2, Nat, F.dec(S)), alld(S), ne_dec(S, hne)) 211 212 law digits_view_t: 213 for +len: U32 214 for +t: P.Tree 215 for +d: Nat 216 for +from: U32 217 for +to: U32 218 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 219 for +hft: {U32.is_le(from, to) == True{} : Bool} 220 for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool} 221 {Pair.snd(D.Bytes, Bool, FC.digits(C.BT(len, t), from, to)) == F.all_digits(D.slice(D.view(C.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool} 222 223 def digits_view_t(len, t, d, from, to, h, hft, ht): 224 +FF = U32.to_nat(from) 225 +TT = U32.to_nat(to) 226 +NN = Nat.sub(TT, FF) 227 +xs = D.view(C.BT(len, t)) 228 +hle = Equal.trans(Bool, Nat.is_le(FF, TT), U32.is_le(from, to), True{}, Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(FF, TT), U.is_le_to_nat(from, to)), hft) 229 +eFT = N.le_sub_add(FF, TT, hle) 230 +hs = AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(len)) == True{} : Bool}, TT, Nat.add(FF, NN), Equal.sym(Nat, Nat.add(FF, NN), TT, eFT), ht) 231 +hlen = AB.subst(Nat, y => {Nat.is_le(Nat.add(FF, NN), y) == True{} : Bool}, U32.to_nat(len), List.length(&2, U32, xs), 232 Equal.sym(Nat, List.length(&2, U32, xs), U32.to_nat(len), O.view_size_t(len, t, d, h)), hs) 233 Equal.trans(Bool, Pair.snd(D.Bytes, Bool, FC.digits(C.BT(len, t), from, to)), Bool.and(U32.is_lt(from, to), alld(D.slice(xs, FF, NN))), 234 Maybe.is_some(&2, Nat, F.dec(D.slice(xs, FF, NN))), 235 dg_view(NN, len, t, d, from, U32.is_lt(from, to), h, hs), dtop(NN, from, to, xs, {==}, hle, hlen)) 236 237 # put_dec: the decimal digits 238 # =========================== 239 240 law eta_nn: 241 for p: Nat & Nat 242 {p == (Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p)) : Nat & Nat} 243 244 def eta_nn(p): 245 (a, b) = p 246 {==} 247 248 # The byte of the last decimal digit of x. 249 def DG(+x: Nat) -> U32: 250 U32.from_nat(Nat.add(48n, Nat.mod(x, 10n))) 251 252 # Nat.show.fin as a list: d is the digit just produced, q what is left. 253 def lgo(f: Nat, +q: Nat, +d: U32, acc: List<&2, U32>) -> List<&2, U32>: 254 match f q: 255 case _ 0n: 256 d <> acc 257 case 0n 1n+p: 258 d <> acc 259 case 1n+g 1n+p: 260 lgo(g, Nat.div(1n+p, 10n), DG(1n+p), d <> acc) 261 262 law show_fin: 263 for +g: Nat 264 for +q: Nat 265 for +d: U32 266 for +sacc: String 267 {F.codes(Nat.show.fin(g, sacc, (Chr{d}, q))) == lgo(g, q, d, F.codes(sacc)) : List<&2, U32>} 268 269 def show_fin(g, q, d, sacc): 270 match g q: 271 case _ 0n: 272 {==} 273 case 0n 1n+p: 274 {==} 275 case 1n+h 1n+p: 276 +S = {SCon{Chr{d}, sacc} : String} 277 %Equal.sym(Nat & Nat, Nat.divmod(1n+p, 10n), (Nat.div(1n+p, 10n), Nat.mod(1n+p, 10n)), eta_nn(Nat.divmod(1n+p, 10n))) : 278 {F.codes(Nat.show.fin(h, S, Nat.show.put(_))) == lgo(1n+h, 1n+p, d, F.codes(sacc)) : List<&2, U32>} 279 show_fin(h, Nat.div(1n+p, 10n), DG(1n+p), S) 280 281 law show_lgo: 282 for +m: Nat 283 {F.codes(Nat.show(m)) == lgo(m, Nat.div(m, 10n), DG(m), Nil{}) : List<&2, U32>} 284 285 def show_lgo(m): 286 %Equal.sym(Nat & Nat, Nat.divmod(m, 10n), (Nat.div(m, 10n), Nat.mod(m, 10n)), eta_nn(Nat.divmod(m, 10n))) : 287 {F.codes(Nat.show.fin(m, SNil{}, Nat.show.put(_))) == lgo(m, Nat.div(m, 10n), DG(m), Nil{}) : List<&2, U32>} 288 show_fin(m, Nat.div(m, 10n), DG(m), SNil{}) 289 290 # A bound on n when put_dec.digits has fuel k: 10^(k+1) - 1, capped at the 291 # largest U32 from k = 9 on (all word constants, never a Nat above 2^32). 292 def BK(k: Nat) -> U32: 293 match k: 294 case 0n: 295 9 296 case 1n+a0: 297 match a0: 298 case 0n: 299 99 300 case 1n+a1: 301 match a1: 302 case 0n: 303 999 304 case 1n+a2: 305 match a2: 306 case 0n: 307 9999 308 case 1n+a3: 309 match a3: 310 case 0n: 311 99999 312 case 1n+a4: 313 match a4: 314 case 0n: 315 999999 316 case 1n+a5: 317 match a5: 318 case 0n: 319 9999999 320 case 1n+a6: 321 match a6: 322 case 0n: 323 99999999 324 case 1n+a7: 325 match a7: 326 case 0n: 327 999999999 328 case 1n+a8: 329 U32.not(0) 330 331 law bk_step: 332 for +k: Nat 333 {U32.is_le(U32.div(BK(1n+k), 10), BK(k)) == True{} : Bool} 334 335 def bk_step(k): 336 match k: 337 case 0n: 338 {==} 339 case 1n+a0: 340 match a0: 341 case 0n: 342 {==} 343 case 1n+a1: 344 match a1: 345 case 0n: 346 {==} 347 case 1n+a2: 348 match a2: 349 case 0n: 350 {==} 351 case 1n+a3: 352 match a3: 353 case 0n: 354 {==} 355 case 1n+a4: 356 match a4: 357 case 0n: 358 {==} 359 case 1n+a5: 360 match a5: 361 case 0n: 362 {==} 363 case 1n+a6: 364 match a6: 365 case 0n: 366 {==} 367 case 1n+a7: 368 match a7: 369 case 0n: 370 {==} 371 case 1n+a8: 372 {==} 373 374 # Digit bytes as numbers 375 # ====================== 376 377 law s48: 378 for +r: Nat 379 for +hr: {Nat.is_lt(r, 10n) == True{} : Bool} 380 {Nat.is_le(Nat.add(r, 48n), Nat.pow(2n, 6n)) == True{} : Bool} 381 382 def s48(r, hr): 383 %N.add_comm(48n, r) : {Nat.is_le(_, Nat.pow(2n, 6n)) == True{} : Bool} 384 N.le_trans(r, 10n, 16n, N.lt_to_le(r, 10n, hr), {==}) 385 386 # Below 64 is below 2^32 (2^32 only meets itself: pow_lt is symbolic). 387 law fits64: 388 for +x: Nat 389 for +hx: {Nat.is_le(x, Nat.pow(2n, 6n)) == True{} : Bool} 390 {Nat.is_lt(x, Nat.pow(2n, 32n)) == True{} : Bool} 391 392 def fits64(x, hx): 393 N.le_lt_trans(x, Nat.pow(2n, 6n), Nat.pow(2n, 32n), hx, AB.pow_lt(6n, 32n, {==})) 394 395 law dgv: 396 for +x: Nat 397 {U32.to_nat(DG(x)) == Nat.add(48n, Nat.mod(x, 10n)) : Nat} 398 399 def dgv(x): 400 +X = Nat.add(48n, Nat.mod(x, 10n)) 401 +hx = N.le_trans(Nat.mod(x, 10n), 10n, 16n, N.lt_to_le(Nat.mod(x, 10n), 10n, N.mod_lt(x, 10n, {==})), {==}) 402 Equal.trans(Nat, U32.to_nat(U32.from_nat(X)), Nat.mod(X, Nat.pow(2n, 32n)), X, U.to_nat_from_nat_p(X), U.wrap_small_p(X, fits64(X, hx))) 403 404 law dg_lt: 405 for +x: Nat 406 {U32.is_lt(DG(x), 256) == True{} : Bool} 407 408 def dg_lt(x): 409 %Equal.sym(Bool, U32.is_lt(DG(x), 256), Nat.is_lt(U32.to_nat(DG(x)), U32.to_nat(256)), U.is_lt_to_nat(DG(x), 256)) : {_ == True{} : Bool} 410 %Equal.sym(Nat, U32.to_nat(DG(x)), Nat.add(48n, Nat.mod(x, 10n)), dgv(x)) : {Nat.is_lt(_, U32.to_nat(256)) == True{} : Bool} 411 N.lt_trans(Nat.mod(x, 10n), 10n, 208n, N.mod_lt(x, 10n, {==}), {==}) 412 413 law dg_eq_n: 414 for +n: U32 415 {U32.to_nat(U32.add(U32.mod(n, 10), 48)) == U32.to_nat(DG(U32.to_nat(n))) : Nat} 416 417 def dg_eq_n(n): 418 +m = U32.to_nat(n) 419 +r = U32.to_nat(U32.mod(n, 10)) 420 +er = U.to_nat_mod(n, 10) 421 +hr = AB.subst(Nat, y => {Nat.is_lt(y, 10n) == True{} : Bool}, Nat.mod(m, 10n), r, Equal.sym(Nat, r, Nat.mod(m, 10n), er), N.mod_lt(m, 10n, {==})) 422 +ea = U.to_nat_add_fits_p(U32.mod(n, 10), 48, fits64(Nat.add(U32.to_nat(U32.mod(n, 10)), U32.to_nat(48)), s48(r, hr))) 423 %Equal.sym(Nat, U32.to_nat(DG(m)), Nat.add(48n, Nat.mod(m, 10n)), dgv(m)) : {U32.to_nat(U32.add(U32.mod(n, 10), 48)) == _ : Nat} 424 %Equal.sym(Nat, U32.to_nat(U32.add(U32.mod(n, 10), 48)), Nat.add(r, U32.to_nat(48)), ea) : {_ == Nat.add(48n, Nat.mod(m, 10n)) : Nat} 425 %Equal.sym(Nat, r, Nat.mod(m, 10n), er) : {Nat.add(_, U32.to_nat(48)) == Nat.add(48n, Nat.mod(m, 10n)) : Nat} 426 N.add_comm(Nat.mod(m, 10n), 48n) 427 428 # The digit byte put_dec writes is DG. 429 law dg_eq: 430 for +n: U32 431 {U32.add(U32.mod(n, 10), 48) == DG(U32.to_nat(n)) : U32} 432 433 def dg_eq(n): 434 U.to_nat_inj(U32.add(U32.mod(n, 10), 48), DG(U32.to_nat(n)), dg_eq_n(n)) 435 436 law lt10: 437 for +n: U32 438 for +hs: {U32.is_lt(n, 10) == True{} : Bool} 439 {Nat.is_lt(U32.to_nat(n), 10n) == True{} : Bool} 440 441 def lt10(n, hs): 442 Equal.trans(Bool, Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U32.is_lt(n, 10), True{}, 443 Equal.sym(Bool, U32.is_lt(n, 10), Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U.is_lt_to_nat(n, 10)), hs) 444 445 law ge10: 446 for +n: U32 447 for +hs: {U32.is_lt(n, 10) == False{} : Bool} 448 {Nat.is_lt(U32.to_nat(n), 10n) == False{} : Bool} 449 450 def ge10(n, hs): 451 Equal.trans(Bool, Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U32.is_lt(n, 10), False{}, 452 Equal.sym(Bool, U32.is_lt(n, 10), Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U.is_lt_to_nat(n, 10)), hs) 453 454 law dg_small_n: 455 for +n: U32 456 for +hs: {U32.is_lt(n, 10) == True{} : Bool} 457 {U32.to_nat(U32.add(n, 48)) == U32.to_nat(DG(U32.to_nat(n))) : Nat} 458 459 def dg_small_n(n, hs): 460 +m = U32.to_nat(n) 461 +hm = lt10(n, hs) 462 +ea = U.to_nat_add_fits_p(n, 48, fits64(Nat.add(U32.to_nat(n), U32.to_nat(48)), s48(m, hm))) 463 %Equal.sym(Nat, U32.to_nat(DG(m)), Nat.add(48n, Nat.mod(m, 10n)), dgv(m)) : {U32.to_nat(U32.add(n, 48)) == _ : Nat} 464 %Equal.sym(Nat, U32.to_nat(U32.add(n, 48)), Nat.add(m, U32.to_nat(48)), ea) : {_ == Nat.add(48n, Nat.mod(m, 10n)) : Nat} 465 %Equal.sym(Nat, Nat.mod(m, 10n), m, N.mod_small(m, 10n, hm)) : {Nat.add(m, U32.to_nat(48)) == Nat.add(48n, _) : Nat} 466 N.add_comm(m, 48n) 467 468 law dg_small: 469 for +n: U32 470 for +hs: {U32.is_lt(n, 10) == True{} : Bool} 471 {U32.add(n, 48) == DG(U32.to_nat(n)) : U32} 472 473 def dg_small(n, hs): 474 U.to_nat_inj(U32.add(n, 48), DG(U32.to_nat(n)), dg_small_n(n, hs)) 475 476 # Bounds for the fuel 477 # =================== 478 479 law lt_add_succ: 480 for +p: Nat 481 for +y: Nat 482 {Nat.is_lt(p, Nat.add(p, 1n+y)) == True{} : Bool} 483 484 def lt_add_succ(p, y): 485 %Equal.sym(Nat, Nat.add(p, 1n+y), 1n+Nat.add(p, y), N.add_succ(p, y)) : {Nat.is_lt(p, _) == True{} : Bool} 486 Equal.trans(Bool, Nat.is_lt(p, 1n+Nat.add(p, y)), Nat.is_le(p, Nat.add(p, y)), True{}, N.lt_succ_iff(p, Nat.add(p, y)), N.le_add_r(p, y)) 487 488 law dlt: 489 for +p: Nat 490 {Nat.is_le(Nat.div(1n+p, 10n), p) == True{} : Bool} 491 492 def dlt(p): 493 +dl = N.div_lt(1n+p, 10n, 1n+p, {==}, lt_add_succ(p, Nat.add(p, Nat.mul(8n, 1n+p)))) 494 Equal.trans(Bool, Nat.is_le(Nat.div(1n+p, 10n), p), Nat.is_lt(Nat.div(1n+p, 10n), 1n+p), True{}, 495 Equal.sym(Bool, Nat.is_lt(Nat.div(1n+p, 10n), 1n+p), Nat.is_le(Nat.div(1n+p, 10n), p), N.lt_succ_iff(Nat.div(1n+p, 10n), p)), dl) 496 497 law hdm: 498 for +m: Nat 499 {Nat.is_le(Nat.div(m, 10n), m) == True{} : Bool} 500 501 def hdm(m): 502 match m: 503 case 0n: 504 {==} 505 case 1n+p: 506 N.le_trans(Nat.div(1n+p, 10n), p, 1n+p, dlt(p), 507 N.lt_to_le(p, 1n+p, Equal.trans(Bool, Nat.is_lt(p, 1n+p), Nat.is_le(p, p), True{}, N.lt_succ_iff(p, p), N.le_refl(p)))) 508 509 law div_mono10: 510 for +a: Nat 511 for +b: Nat 512 for +h: {Nat.is_le(a, b) == True{} : Bool} 513 {Nat.is_le(Nat.div(a, 10n), Nat.div(b, 10n)) == True{} : Bool} 514 515 def div_mono10(a, b, h): 516 +x = Nat.div(b, 10n) 517 +r = Nat.mod(b, 10n) 518 +X = Nat.mul(x, 10n) 519 +hb = AB.subst(Nat, y => {Nat.is_lt(y, Nat.add(10n, X)) == True{} : Bool}, Nat.add(r, X), b, 520 Equal.trans(Nat, Nat.add(r, X), Nat.add(X, r), b, N.add_comm(r, X), N.div_mod(b, 10n)), 521 N.lt_add_mono_r(X, r, 10n, N.mod_lt(b, 10n, {==}))) 522 +ha = N.le_lt_trans(a, b, Nat.add(10n, X), h, hb) 523 +h2 = AB.subst(Nat, y => {Nat.is_lt(a, y) == True{} : Bool}, Nat.mul(1n+x, 10n), Nat.mul(10n, 1n+x), 524 Equal.sym(Nat, Nat.mul(10n, 1n+x), Nat.mul(1n+x, 10n), N.mul_comm(10n, 1n+x)), ha) 525 +dl = N.div_lt(a, 10n, 1n+x, {==}, h2) 526 Equal.trans(Bool, Nat.is_le(Nat.div(a, 10n), x), Nat.is_lt(Nat.div(a, 10n), 1n+x), True{}, 527 Equal.sym(Bool, Nat.is_lt(Nat.div(a, 10n), 1n+x), Nat.is_le(Nat.div(a, 10n), x), N.lt_succ_iff(Nat.div(a, 10n), x)), dl) 528 529 # n <= BK(1 + j) gives n / 10 <= BK(j). 530 law hk_step: 531 for +n: U32 532 for +j: Nat 533 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(1n+j))) == True{} : Bool} 534 {Nat.is_le(U32.to_nat(U32.div(n, 10)), U32.to_nat(BK(j))) == True{} : Bool} 535 536 def hk_step(n, j, hk): 537 +m = U32.to_nat(n) 538 +Bv = U32.to_nat(BK(1n+j)) 539 +bstep = Equal.trans(Bool, Nat.is_le(U32.to_nat(U32.div(BK(1n+j), 10)), U32.to_nat(BK(j))), U32.is_le(U32.div(BK(1n+j), 10), BK(j)), True{}, 540 Equal.sym(Bool, U32.is_le(U32.div(BK(1n+j), 10), BK(j)), Nat.is_le(U32.to_nat(U32.div(BK(1n+j), 10)), U32.to_nat(BK(j))), 541 U.is_le_to_nat(U32.div(BK(1n+j), 10), BK(j))), bk_step(j)) 542 %Equal.sym(Nat, U32.to_nat(U32.div(n, 10)), Nat.div(m, U32.to_nat(10)), U.to_nat_div(n, 10)) : {Nat.is_le(_, U32.to_nat(BK(j))) == True{} : Bool} 543 N.le_trans(Nat.div(m, 10n), Nat.div(Bv, 10n), U32.to_nat(BK(j)), div_mono10(m, Bv, hk), 544 AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(BK(j))) == True{} : Bool}, U32.to_nat(U32.div(BK(1n+j), 10)), Nat.div(Bv, 10n), 545 U.to_nat_div(BK(1n+j), 10), bstep)) 546 547 law ab0: 548 for +n: U32 549 for +hs: {U32.is_lt(n, 10) == False{} : Bool} 550 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(0n))) == True{} : Bool} 551 Empty 552 553 def ab0(n, hs, hk): 554 AB.false_ne_true(N.le_trans(10n, U32.to_nat(n), U32.to_nat(BK(0n)), N.not_lt_le(U32.to_nat(n), 10n, ge10(n, hs)), hk)) 555 556 law lmax: 557 for +x: Nat 558 for +z: Nat 559 for +M: Nat 560 for +hx: {Nat.is_lt(x, M) == True{} : Bool} 561 for +hz: {z == Nat.sub(Nat.sub(M, 1n), U32.to_nat(0)) : Nat} 562 {Nat.is_le(x, z) == True{} : Bool} 563 564 def lmax(x, z, M, hx, hz): 565 match M: 566 case 0n: 567 Empty.absurd({Nat.is_le(x, z) == True{} : Bool}, AB.lt_zero_absurd(x, hx)) 568 case 1n+M1: 569 %Equal.sym(Nat, z, Nat.sub(Nat.sub(1n+M1, 1n), U32.to_nat(0)), hz) : {Nat.is_le(x, _) == True{} : Bool} 570 %Equal.sym(Nat, Nat.sub(Nat.sub(M1, 0n), 0n), Nat.sub(M1, 0n), N.sub_zero(Nat.sub(M1, 0n))) : {Nat.is_le(x, _) == True{} : Bool} 571 %Equal.sym(Nat, Nat.sub(M1, 0n), M1, N.sub_zero(M1)) : {Nat.is_le(x, _) == True{} : Bool} 572 Equal.trans(Bool, Nat.is_le(x, M1), Nat.is_lt(x, 1n+M1), True{}, Equal.sym(Bool, Nat.is_lt(x, 1n+M1), Nat.is_le(x, M1), N.lt_succ_iff(x, M1)), hx) 573 574 # Every word is at most the largest one, BK(k) from k = 9 on. 575 law hkmax: 576 for +n: U32 577 {Nat.is_le(U32.to_nat(n), U32.to_nat(U32.not(0))) == True{} : Bool} 578 579 def hkmax(n): 580 lmax(U32.to_nat(n), U32.to_nat(U32.not(0)), Nat.pow(2n, 32n), U.to_nat_lt_p(n), U.to_nat_not_p(0)) 581 582 # put_dec.digits against the spec 583 # =============================== 584 585 # With n <= BK(k) the fuel k suffices; q = n / 10 and the spec's fuel f >= q. 586 law R: 587 for +k: Nat 588 for +small: Bool 589 for +q: Nat 590 for +f: Nat 591 for +n: U32 592 for +acc: List<&2, U32> 593 for +hs: {U32.is_lt(n, 10) == small : Bool} 594 for +hq: {Nat.div(U32.to_nat(n), 10n) == q : Nat} 595 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(k))) == True{} : Bool} 596 for +hf: {Nat.is_le(q, f) == True{} : Bool} 597 {FC.put_dec.digits(k, small, n, acc) == lgo(f, q, DG(U32.to_nat(n)), acc) : List<&2, U32>} 598 599 def R(k, small, q, f, n, acc, hs, hq, hk, hf): 600 match k small q f: 601 case _ True{} 0n 0n: 602 %dg_small(n, hs) : {U32.add(n, 48) <> acc == _ <> acc : List<&2, U32>} 603 {==} 604 case _ True{} 0n 1n+g: 605 %dg_small(n, hs) : {U32.add(n, 48) <> acc == _ <> acc : List<&2, U32>} 606 {==} 607 case _ True{} 1n+p _: 608 +e0 = Equal.trans(Nat, 0n, Nat.div(U32.to_nat(n), 10n), 1n+p, 609 Equal.sym(Nat, Nat.div(U32.to_nat(n), 10n), 0n, N.div_small(U32.to_nat(n), 10n, lt10(n, hs))), hq) 610 Empty.absurd({FC.put_dec.digits(k, True{}, n, acc) == lgo(f, 1n+p, DG(U32.to_nat(n)), acc) : List<&2, U32>}, 611 AB.succ_ne_zero(p, Equal.sym(Nat, 0n, 1n+p, e0))) 612 case 0n False{} _ _: 613 Empty.absurd({FC.put_dec.digits(0n, False{}, n, acc) == lgo(f, q, DG(U32.to_nat(n)), acc) : List<&2, U32>}, ab0(n, hs, hk)) 614 case 1n+j False{} 0n _: 615 +m = U32.to_nat(n) 616 +edm = AB.subst(Nat, y => {Nat.add(Nat.mul(y, 10n), Nat.mod(m, 10n)) == m : Nat}, Nat.div(m, 10n), 0n, hq, N.div_mod(m, 10n)) 617 +hm = AB.subst(Nat, y => {Nat.is_lt(y, 10n) == True{} : Bool}, Nat.mod(m, 10n), m, edm, N.mod_lt(m, 10n, {==})) 618 Empty.absurd({FC.put_dec.digits(1n+j, False{}, n, acc) == lgo(f, 0n, DG(m), acc) : List<&2, U32>}, 619 AB.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(m, 10n), False{}, Equal.sym(Bool, Nat.is_lt(m, 10n), True{}, hm), ge10(n, hs)))) 620 case 1n+j False{} 1n+p 0n: 621 Empty.absurd({FC.put_dec.digits(1n+j, False{}, n, acc) == lgo(0n, 1n+p, DG(U32.to_nat(n)), acc) : List<&2, U32>}, AB.false_ne_true(hf)) 622 case 1n+j False{} 1n+p 1n+g: 623 +m = U32.to_nat(n) 624 +n1 = U32.div(n, 10) 625 +acc1 = {U32.add(U32.mod(n, 10), 48) <> acc : List<&2, U32>} 626 +e1 = Equal.trans(Nat, U32.to_nat(n1), Nat.div(m, 10n), 1n+p, U.to_nat_div(n, 10), hq) 627 +hf1 = AB.subst(Nat, y => {Nat.is_le(Nat.div(y, 10n), g) == True{} : Bool}, 1n+p, U32.to_nat(n1), Equal.sym(Nat, U32.to_nat(n1), 1n+p, e1), 628 N.le_trans(Nat.div(1n+p, 10n), p, g, dlt(p), hf)) 629 +RHS = lgo(g, Nat.div(1n+p, 10n), DG(1n+p), DG(m) <> acc) 630 %Equal.sym(List<&2, U32>, FC.put_dec.digits(j, U32.is_lt(n1, 10), n1, acc1), lgo(g, Nat.div(U32.to_nat(n1), 10n), DG(U32.to_nat(n1)), acc1), 631 R(j, U32.is_lt(n1, 10), Nat.div(U32.to_nat(n1), 10n), g, n1, acc1, {==}, {==}, hk_step(n, j, hk), hf1)) : 632 {_ == RHS : List<&2, U32>} 633 %Equal.sym(Nat, U32.to_nat(n1), 1n+p, e1) : {lgo(g, Nat.div(_, 10n), DG(_), acc1) == RHS : List<&2, U32>} 634 %Equal.sym(U32, U32.add(U32.mod(n, 10), 48), DG(m), dg_eq(n)) : {lgo(g, Nat.div(1n+p, 10n), DG(1n+p), _ <> acc) == RHS : List<&2, U32>} 635 {==} 636 637 law LN: 638 for +k: Nat 639 for +small: Bool 640 for +j: Nat 641 for +n: U32 642 for +acc: List<&2, U32> 643 for +hs: {U32.is_lt(n, 10) == small : Bool} 644 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(j))) == True{} : Bool} 645 for +hj: {Nat.is_le(j, k) == True{} : Bool} 646 {Nat.is_le(List.length(&2, U32, FC.put_dec.digits(k, small, n, acc)), Nat.add(1n+j, List.length(&2, U32, acc))) == True{} : Bool} 647 648 def LN(k, small, j, n, acc, hs, hk, hj): 649 match k small j: 650 case _ True{} _: 651 N.le_add_l(List.length(&2, U32, acc), j) 652 case 0n False{} 0n: 653 Empty.absurd({Nat.is_le(List.length(&2, U32, FC.put_dec.digits(0n, False{}, n, acc)), Nat.add(1n, List.length(&2, U32, acc))) == True{} : Bool}, 654 ab0(n, hs, hk)) 655 case 0n False{} 1n+i: 656 Empty.absurd({Nat.is_le(List.length(&2, U32, FC.put_dec.digits(0n, False{}, n, acc)), Nat.add(1n+1n+i, List.length(&2, U32, acc))) == True{} : Bool}, 657 AB.false_ne_true(hj)) 658 case 1n+k1 False{} 0n: 659 Empty.absurd({Nat.is_le(List.length(&2, U32, FC.put_dec.digits(1n+k1, False{}, n, acc)), Nat.add(1n, List.length(&2, U32, acc))) == True{} : Bool}, 660 ab0(n, hs, hk)) 661 case 1n+k1 False{} 1n+i: 662 +n1 = U32.div(n, 10) 663 +acc1 = {U32.add(U32.mod(n, 10), 48) <> acc : List<&2, U32>} 664 +L = List.length(&2, U32, acc) 665 +len1 = List.length(&2, U32, FC.put_dec.digits(k1, U32.is_lt(n1, 10), n1, acc1)) 666 AB.subst(Nat, y => {Nat.is_le(len1, 1n+y) == True{} : Bool}, Nat.add(i, 1n+L), 1n+Nat.add(i, L), N.add_succ(i, L), 667 LN(k1, U32.is_lt(n1, 10), i, n1, acc1, {==}, hk_step(n, i, hk), hj)) 668 669 law ab_cons: 670 for +n: U32 671 for +acc: List<&2, U32> 672 for +hacc: {D.all_bytes(acc) == True{} : Bool} 673 {D.all_bytes(U32.add(U32.mod(n, 10), 48) <> acc) == True{} : Bool} 674 675 def ab_cons(n, acc, hacc): 676 %Equal.sym(U32, U32.add(U32.mod(n, 10), 48), DG(U32.to_nat(n)), dg_eq(n)) : {D.all_bytes(_ <> acc) == True{} : Bool} 677 %Equal.sym(Bool, U32.is_lt(DG(U32.to_nat(n)), 256), True{}, dg_lt(U32.to_nat(n))) : {Bool.and(_, D.all_bytes(acc)) == True{} : Bool} 678 hacc 679 680 law AL: 681 for +k: Nat 682 for +small: Bool 683 for +n: U32 684 for +acc: List<&2, U32> 685 for +hs: {U32.is_lt(n, 10) == small : Bool} 686 for +hacc: {D.all_bytes(acc) == True{} : Bool} 687 {D.all_bytes(FC.put_dec.digits(k, small, n, acc)) == True{} : Bool} 688 689 def AL(k, small, n, acc, hs, hacc): 690 match k small: 691 case _ True{}: 692 %Equal.sym(U32, U32.add(n, 48), DG(U32.to_nat(n)), dg_small(n, hs)) : {D.all_bytes(_ <> acc) == True{} : Bool} 693 %Equal.sym(Bool, U32.is_lt(DG(U32.to_nat(n)), 256), True{}, dg_lt(U32.to_nat(n))) : {Bool.and(_, D.all_bytes(acc)) == True{} : Bool} 694 hacc 695 case 0n False{}: 696 hacc 697 case 1n+k1 False{}: 698 AL(k1, U32.is_lt(U32.div(n, 10), 10), U32.div(n, 10), U32.add(U32.mod(n, 10), 48) <> acc, {==}, ab_cons(n, acc, hacc)) 699 700 # The list put_dec writes 701 # ======================= 702 703 law hkb: 704 for +n: U32 705 for +r: Nat 706 {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(9n+r))) == True{} : Bool} 707 708 def hkb(n, r): 709 AB.subst(U32, y => {Nat.is_le(U32.to_nat(n), U32.to_nat(y)) == True{} : Bool}, U32.not(0), BK(9n+r), {==}, hkmax(n)) 710 711 law list_show: 712 for +n: U32 713 {FC.put_dec.list(n) == F.show(n) : List<&2, U32>} 714 715 def list_show(n): 716 +m = U32.to_nat(n) 717 Equal.trans(List<&2, U32>, FC.put_dec.list(n), lgo(m, Nat.div(m, 10n), DG(m), Nil{}), F.show(n), 718 R(10n, U32.is_lt(n, 10), Nat.div(m, 10n), m, n, Nil{}, {==}, {==}, hkb(n, 1n), hdm(m)), 719 Equal.sym(List<&2, U32>, F.show(n), lgo(m, Nat.div(m, 10n), DG(m), Nil{}), show_lgo(m))) 720 721 law list_len: 722 for +n: U32 723 {Nat.is_le(List.length(&2, U32, FC.put_dec.list(n)), 10n) == True{} : Bool} 724 725 def list_len(n): 726 LN(10n, U32.is_lt(n, 10), 9n, n, Nil{}, {==}, hkb(n, 0n), {==}) 727 728 law list_bytes: 729 for +n: U32 730 {D.all_bytes(FC.put_dec.list(n)) == True{} : Bool} 731 732 def list_bytes(n): 733 AL(10n, U32.is_lt(n, 10), n, Nil{}, {==}, {==}) 734 735 law pd_eq: 736 for +xs: List<&2, U32> 737 for -b: D.Bytes 738 {FC.put_dec.go(xs, b) == B.of_list.go(xs, b) : D.Bytes} 739 740 def pd_eq(xs, b): 741 match xs: 742 case Nil{}: 743 {==} 744 case Con{+x, t}: 745 pd_eq(t, B.push(b, x)) 746 747 law pd_room: 748 for +len: U32 749 for +t: P.Tree 750 for +d: Nat 751 for +n: U32 752 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 753 for +hc: {Nat.is_le(Nat.add(D.size(C.BT(len, t)), 10n), D.cap(C.BT(len, t))) == True{} : Bool} 754 {Nat.is_le(Nat.add(U32.to_nat(len), List.length(&2, U32, FC.put_dec.list(n))), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool} 755 756 def pd_room(len, t, d, n, h, hc): 757 +M = Nat.mul(4n, Nat.pow(2n, d)) 758 N.le_trans(Nat.add(U32.to_nat(len), List.length(&2, U32, FC.put_dec.list(n))), Nat.add(U32.to_nat(len), 10n), M, 759 N.le_add_mono_l(U32.to_nat(len), List.length(&2, U32, FC.put_dec.list(n)), 10n, list_len(n)), 760 AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(len), 10n), y) == True{} : Bool}, D.cap(C.BT(len, t)), M, O.cap_ok_t(len, t, d, h), hc)) 761 762 law put_dec_view_t: 763 for +len: U32 764 for +t: P.Tree 765 for +d: Nat 766 for +n: U32 767 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 768 for +hc: {Nat.is_le(Nat.add(D.size(C.BT(len, t)), 10n), D.cap(C.BT(len, t))) == True{} : Bool} 769 {D.view(FC.put_dec(C.BT(len, t), n)) == List.append(&2, U32, D.view(C.BT(len, t)), F.show(n)) : List<&2, U32>} 770 771 def put_dec_view_t(len, t, d, n, h, hc): 772 +L = FC.put_dec.list(n) 773 +V = D.view(C.BT(len, t)) 774 %Equal.sym(D.Bytes, FC.put_dec.go(L, C.BT(len, t)), B.of_list.go(L, C.BT(len, t)), pd_eq(L, C.BT(len, t))) : 775 {D.view(_) == List.append(&2, U32, V, F.show(n)) : List<&2, U32>} 776 %Equal.sym(List<&2, U32>, D.view(B.of_list.go(L, C.BT(len, t))), List.append(&2, U32, V, L), 777 G.ol_go_view(L, len, t, d, h, list_bytes(n), pd_room(len, t, d, n, h, hc))) : 778 {_ == List.append(&2, U32, V, F.show(n)) : List<&2, U32>} 779 %list_show(n) : {List.append(&2, U32, V, L) == List.append(&2, U32, V, _) : List<&2, U32>} 780 {==} 781 782 law put_dec_ok_t: 783 for +len: U32 784 for +t: P.Tree 785 for +d: Nat 786 for +n: U32 787 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} 788 for +hc: {Nat.is_le(Nat.add(D.size(C.BT(len, t)), 10n), D.cap(C.BT(len, t))) == True{} : Bool} 789 {D.ok(FC.put_dec(C.BT(len, t), n), d) == True{} : Bool} 790 791 def put_dec_ok_t(len, t, d, n, h, hc): 792 +L = FC.put_dec.list(n) 793 %Equal.sym(D.Bytes, FC.put_dec.go(L, C.BT(len, t)), B.of_list.go(L, C.BT(len, t)), pd_eq(L, C.BT(len, t))) : 794 {D.ok(_, d) == True{} : Bool} 795 G.ol_go_ok(L, len, t, d, h, pd_room(len, t, d, n, h, hc))