proofs/containers/hash_table/size.bend
bend-collections-laws-containers@1.0.0.0 · 77 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as IV
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as ST
14
15# size: the stored count is the number of entries of the model.
16
17def size_app(~V: Data, +a: List<&2, S.Entry<V>>, +b: List<&2, S.Entry<V>>) -> {S.size(~V, SC.append(S.Entry<V>, 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<V>, t, b)), Nat.add(S.size(~V, t), S.size(~V, b)), size_app(~V, t, b))
23
24def 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<V>, ST.absm(~V, bs, vsl, q, j), ST.ent(~V, B.at(bs, Nat.add(j, q)), vsl)) : List<&2, S.Entry<V>>}:
25 match q:
26 case 0n:
27 +e = ST.ent(~V, B.at(bs, j), vsl)
28 Equal.trans(List<&2, S.Entry<V>>, SC.append(S.Entry<V>, e, Nil{}), e, ST.ent(~V, B.at(bs, Nat.add(j, 0n)), vsl), LL.append_nil(S.Entry<V>, e), Equal.cong(Nat, List<&2, S.Entry<V>>, 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<V>>, SC.append(S.Entry<V>, e, ST.absm(~V, bs, vsl, 1n+p, 1n+j)), SC.append(S.Entry<V>, e, SC.append(S.Entry<V>, ST.absm(~V, bs, vsl, p, 1n+j), last)), SC.append(S.Entry<V>, 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<V>>, List<&2, S.Entry<V>>, z => SC.append(S.Entry<V>, e, z), ST.absm(~V, bs, vsl, 1n+p, 1n+j), SC.append(S.Entry<V>, ST.absm(~V, bs, vsl, p, 1n+j), last), absm_snoc(~V, bs, vsl, p, 1n+j)),
34 Equal.trans(List<&2, S.Entry<V>>, SC.append(S.Entry<V>, e, SC.append(S.Entry<V>, ST.absm(~V, bs, vsl, p, 1n+j), last)), SC.append(S.Entry<V>, SC.append(S.Entry<V>, e, ST.absm(~V, bs, vsl, p, 1n+j)), last), SC.append(S.Entry<V>, 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<V>>, SC.append(S.Entry<V>, SC.append(S.Entry<V>, e, ST.absm(~V, bs, vsl, p, 1n+j)), last), SC.append(S.Entry<V>, e, SC.append(S.Entry<V>, ST.absm(~V, bs, vsl, p, 1n+j), last)), LL.append_assoc(S.Entry<V>, e, ST.absm(~V, bs, vsl, p, 1n+j), last)),
36 Equal.cong(Nat, List<&2, S.Entry<V>>, z => SC.append(S.Entry<V>, 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
38def 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
46def 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
55def 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<V>>, Nat, z => S.size(~V, z), ST.absm(~V, bs, vsl, 1n+p, 0n), SC.append(S.Entry<V>, 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<V>, 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.
68def size_ok(~V: Data, +sh: ST.Sh<V>, +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)))