1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/hash_table.bend as S 8 import ../../lib/u32div.bend as UD 9 import ../../../src/containers/hash_table.bend as H 10 import ./table.bend as TB 11 import ./buckets.bend as B 12 import ./inv.bend as IV 13 import ./state.bend as ST 14 15 # size: the stored count is the number of entries of the model. 16 17 def size_app(~V: Data, +a: List<&2, S.Entry>, +b: List<&2, S.Entry>) -> {S.size(~V, SC.append(S.Entry, a, b)) == Nat.add(S.size(~V, a), S.size(~V, b)) : Nat}: 18 match a: 19 case Nil{}: 20 {==} 21 case Con{e, t}: 22 N.succ_cong(S.size(~V, SC.append(S.Entry, t, b)), Nat.add(S.size(~V, t), S.size(~V, b)), size_app(~V, t, b)) 23 24 def absm_snoc(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +q: Nat, +j: Nat) -> {ST.absm(~V, bs, vsl, 1n+q, j) == SC.append(S.Entry, ST.absm(~V, bs, vsl, q, j), ST.ent(~V, B.at(bs, Nat.add(j, q)), vsl)) : List<&2, S.Entry>}: 25 match q: 26 case 0n: 27 +e = ST.ent(~V, B.at(bs, j), vsl) 28 Equal.trans(List<&2, S.Entry>, SC.append(S.Entry, e, Nil{}), e, ST.ent(~V, B.at(bs, Nat.add(j, 0n)), vsl), LL.append_nil(S.Entry, e), Equal.cong(Nat, List<&2, S.Entry>, z => ST.ent(~V, B.at(bs, z), vsl), j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)))) 29 case 1n+p: 30 +e = ST.ent(~V, B.at(bs, j), vsl) 31 +last = ST.ent(~V, B.at(bs, Nat.add(1n+j, p)), vsl) 32 Equal.trans(List<&2, S.Entry>, SC.append(S.Entry, e, ST.absm(~V, bs, vsl, 1n+p, 1n+j)), SC.append(S.Entry, e, SC.append(S.Entry, ST.absm(~V, bs, vsl, p, 1n+j), last)), SC.append(S.Entry, ST.absm(~V, bs, vsl, 1n+p, j), ST.ent(~V, B.at(bs, Nat.add(j, 1n+p)), vsl)), 33 Equal.cong(List<&2, S.Entry>, List<&2, S.Entry>, z => SC.append(S.Entry, e, z), ST.absm(~V, bs, vsl, 1n+p, 1n+j), SC.append(S.Entry, ST.absm(~V, bs, vsl, p, 1n+j), last), absm_snoc(~V, bs, vsl, p, 1n+j)), 34 Equal.trans(List<&2, S.Entry>, SC.append(S.Entry, e, SC.append(S.Entry, ST.absm(~V, bs, vsl, p, 1n+j), last)), SC.append(S.Entry, SC.append(S.Entry, e, ST.absm(~V, bs, vsl, p, 1n+j)), last), SC.append(S.Entry, ST.absm(~V, bs, vsl, 1n+p, j), ST.ent(~V, B.at(bs, Nat.add(j, 1n+p)), vsl)), 35 Equal.sym(List<&2, S.Entry>, SC.append(S.Entry, SC.append(S.Entry, e, ST.absm(~V, bs, vsl, p, 1n+j)), last), SC.append(S.Entry, e, SC.append(S.Entry, ST.absm(~V, bs, vsl, p, 1n+j), last)), LL.append_assoc(S.Entry, e, ST.absm(~V, bs, vsl, p, 1n+j), last)), 36 Equal.cong(Nat, List<&2, S.Entry>, z => SC.append(S.Entry, ST.absm(~V, bs, vsl, 1n+p, j), ST.ent(~V, B.at(bs, z), vsl)), Nat.add(1n+j, p), Nat.add(j, 1n+p), Equal.sym(Nat, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p))))) 37 38 def size_m(~V: Data, +k: String, +m: Maybe<&2, V>, +h: {ST.some_b(~V, m) == True{} : Bool}) -> {S.size(~V, ST.ent_m(~V, k, m)) == 1n : Nat}: 39 match m: 40 case None{}: 41 Empty.absurd({S.size(~V, ST.ent_m(~V, k, None{})) == 1n : Nat}, L.false_true(h)) 42 case Some{v}: 43 {==} 44 45 # a live bucket has one entry, an empty bucket none 46 def size_ent(~V: Data, +b: B.Bk, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +hl: {B.live_b(ST.lvs(~V, vsl), fr, b) == True{} : Bool}) -> {S.size(~V, ST.ent(~V, b, vsl)) == IV.bitv(B.occ(b)) : Nat}: 47 match b: 48 case B.BE{}: 49 {==} 50 case B.BF{w, +l, +k}: 51 +hn = L.and_left(B.nthb(ST.lvs(~V, vsl), UD.v(H.slot(l))), Nat.is_lt(UD.v(H.slot(l)), fr), hl) 52 size_m(~V, k, ST.nthm(~V, vsl, UD.v(H.slot(l))), Equal.trans(Bool, ST.some_b(~V, ST.nthm(~V, vsl, UD.v(H.slot(l)))), B.nthb(ST.lvs(~V, vsl), UD.v(H.slot(l))), True{}, Equal.sym(Bool, B.nthb(ST.lvs(~V, vsl), UD.v(H.slot(l))), ST.some_b(~V, ST.nthm(~V, vsl, UD.v(H.slot(l)))), ST.lvs_nth(~V, vsl, UD.v(H.slot(l)))), hn)) 53 54 # the number of entries is the number of full buckets 55 def size_absm(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +n: Nat, +hl: {B.all_lt(B.PLive{bs, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, n) == True{} : Bool}) -> {S.size(~V, ST.absm(~V, bs, vsl, q, 0n)) == IV.occn(bs, q) : Nat}: 56 match q: 57 case 0n: 58 {==} 59 case 1n+p: 60 +hp = N.succ_le_lt(p, n, hq) 61 +e1 = Equal.cong(List<&2, S.Entry>, Nat, z => S.size(~V, z), ST.absm(~V, bs, vsl, 1n+p, 0n), SC.append(S.Entry, ST.absm(~V, bs, vsl, p, 0n), ST.ent(~V, B.at(bs, p), vsl)), absm_snoc(~V, bs, vsl, p, 0n)) 62 +e2 = size_app(~V, ST.absm(~V, bs, vsl, p, 0n), ST.ent(~V, B.at(bs, p), vsl)) 63 +e3 = Equal.cong(Nat, Nat, z => Nat.add(z, S.size(~V, ST.ent(~V, B.at(bs, p), vsl))), S.size(~V, ST.absm(~V, bs, vsl, p, 0n)), IV.occn(bs, p), size_absm(~V, bs, vsl, fr, n, hl, p, N.lt_le(p, n, hp))) 64 +e4 = Equal.cong(Nat, Nat, z => Nat.add(IV.occn(bs, p), z), S.size(~V, ST.ent(~V, B.at(bs, p), vsl)), IV.bitv(B.occ(B.at(bs, p))), size_ent(~V, B.at(bs, p), vsl, fr, B.all_inst(B.PLive{bs, ST.lvs(~V, vsl), fr}, n, hl, p, hp))) 65 Equal.trans(Nat, S.size(~V, ST.absm(~V, bs, vsl, 1n+p, 0n)), Nat.add(IV.occn(bs, p), IV.bitv(B.occ(B.at(bs, p)))), IV.occn(bs, 1n+p), Equal.trans(Nat, S.size(~V, ST.absm(~V, bs, vsl, 1n+p, 0n)), Nat.add(S.size(~V, ST.absm(~V, bs, vsl, p, 0n)), S.size(~V, ST.ent(~V, B.at(bs, p), vsl))), Nat.add(IV.occn(bs, p), IV.bitv(B.occ(B.at(bs, p)))), Equal.trans(Nat, S.size(~V, ST.absm(~V, bs, vsl, 1n+p, 0n)), S.size(~V, SC.append(S.Entry, ST.absm(~V, bs, vsl, p, 0n), ST.ent(~V, B.at(bs, p), vsl))), Nat.add(S.size(~V, ST.absm(~V, bs, vsl, p, 0n)), S.size(~V, ST.ent(~V, B.at(bs, p), vsl))), e1, e2), Equal.trans(Nat, Nat.add(S.size(~V, ST.absm(~V, bs, vsl, p, 0n)), S.size(~V, ST.ent(~V, B.at(bs, p), vsl))), Nat.add(IV.occn(bs, p), S.size(~V, ST.ent(~V, B.at(bs, p), vsl))), Nat.add(IV.occn(bs, p), IV.bitv(B.occ(B.at(bs, p)))), e3, e4)), N.add_comm(IV.occn(bs, p), IV.bitv(B.occ(B.at(bs, p))))) 66 67 # THEOREM: size hands back the map unchanged and the model's size. 68 def size_ok(~V: Data, +sh: ST.Sh, +hg: {ST.good(~V, sh) == True{} : Bool}) -> {H.size(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) : H.HashMap<&2, V> & U32} & {UD.v(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) == S.size(~V, ST.model(~V, sh)) : Nat}: 69 match sh: 70 case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}: 71 +kl = AR.slots(String, ksT) 72 +pk = AR.perfect(String, sd, ksT) 73 +bs = TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)) 74 +vsl = AR.slots(Maybe<&2, V>, vsT) 75 +cn = N.eq_from_is_eq(UD.v(n), IV.occn(bs, SC.pow2(k)), ST.g_cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg)) 76 +sa = size_absm(~V, bs, vsl, UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg), SC.pow2(k), N.le_refl(SC.pow2(k))) 77 ({==}, Equal.trans(Nat, UD.v(n), IV.occn(bs, SC.pow2(k)), S.size(~V, ST.absm(~V, bs, vsl, SC.pow2(k), 0n)), cn, Equal.sym(Nat, S.size(~V, ST.absm(~V, bs, vsl, SC.pow2(k), 0n)), IV.occn(bs, SC.pow2(k)), sa)))