proofs/containers/hash_table/poplem.bend
bend-collections-laws-containers@1.0.0.0 · 287 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as ST
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/lookup.bend as LK
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as T
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/speclem.bend as SL
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/setv.bend as SV
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insa.bend as IA
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insf.bend as IF
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/rehash.bend as RH
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/delmv.bend as DM
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keysw.bend as KW
22import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
23import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
24
25# Facts for pop: after emptying the bucket i that holds key, the other keys
26# look up as before, key is held nowhere, the model's keys have no repeats,
27# and the vacated slot is free.
28
29
30# ---- the emptied bucket, for a property true of every empty bucket ----
31
32def at_v0(+O: List<&2, B.Bk>, +i: Nat, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +j: Nat, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {B.at(IM.bupd(O, i, B.BE{}), j) == Bool.pick(B.Bk, c, B.BE{}, B.at(O, j)) : B.Bk}:
33 match c:
34 case True{}:
35 IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)
36 case False{}:
37 IM.at_bupd_other(O, i, B.BE{}, j, hc)
38
39def well_rm_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{O, sd}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {B.wb(sd, B.at(IM.bupd(O, i, B.BE{}), j)) == True{} : Bool}:
40 match c:
41 case True{}:
42 L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.BE{}, IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)), {==})
43 case False{}:
44 L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), B.all_inst(B.PWell{O, sd}, n, hw, j, hj))
45
46def well_rm(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{O, sd}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PWell{IM.bupd(O, i, B.BE{}), sd}, m) == True{} : Bool}:
47 match m:
48 case 0n:
49 {==}
50 case 1n+q:
51 +hq = N.succ_le_lt(q, n, hm)
52 L.and_intro(B.wb(sd, B.at(IM.bupd(O, i, B.BE{}), q)), B.all_lt(B.PWell{IM.bupd(O, i, B.BE{}), sd}, q), well_rm_i(O, n, i, hi, hlen, sd, hw, q, hq, Nat.is_eq(i, q), {==}), well_rm(O, n, i, hi, hlen, sd, hw, q, N.lt_le(q, n, hq)))
53
54def wl_at(+obs: List<&2, B.Bk>, +sd: Nat, +j: Nat, +hw: {B.all_lt(B.PWell{obs, sd}, j) == True{} : Bool}, +b: B.Bk, e: RH.EqAt(obs, j, b)) -> {B.wb(sd, b) == True{} : Bool}:
55 match e:
56 case Tuple{+x, Tuple{+hx, +hb}}:
57 L.subst(B.Bk, y => {B.wb(sd, y) == True{} : Bool}, B.at(obs, x), b, hb, B.all_inst(B.PWell{obs, sd}, j, hw, x, hx))
58
59def wb_empty(+sd: Nat, +b: B.Bk, +h: {B.occ(b) == False{} : Bool}) -> {B.wb(sd, b) == True{} : Bool}:
60 match b:
61 case B.BE{}:
62 {==}
63 case B.BF{w, l, k}:
64 Empty.absurd({B.wb(sd, B.BF{w, l, k}) == True{} : Bool}, L.true_false(h))
65
66def wlf_c(+nbs: List<&2, B.Bk>, +obs: List<&2, B.Bk>, +j: Nat, +n2: Nat, +hf: {B.all_lt(B.PFrom{nbs, obs, j}, n2) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{obs, sd}, j) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n2) == True{} : Bool}, +c: Bool, +hc: {B.occ(B.at(nbs, x)) == c : Bool}) -> {B.wb(sd, B.at(nbs, x)) == True{} : Bool}:
67 match c:
68 case False{}:
69 wb_empty(sd, B.at(nbs, x), hc)
70 case True{}:
71 wl_at(obs, sd, j, hw, B.at(nbs, x), RH.from_at(nbs, obs, j, n2, hf, x, hx, hc))
72
73# THEOREM: copies of well-formed buckets are well formed
74def well_from(+nbs: List<&2, B.Bk>, +obs: List<&2, B.Bk>, +j: Nat, +n2: Nat, +hf: {B.all_lt(B.PFrom{nbs, obs, j}, n2) == True{} : Bool}, +sd: Nat, +hw: {B.all_lt(B.PWell{obs, sd}, j) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n2) == True{} : Bool}) -> {B.all_lt(B.PWell{nbs, sd}, m) == True{} : Bool}:
75 match m:
76 case 0n:
77 {==}
78 case 1n+q:
79 +hq = N.succ_le_lt(q, n2, hm)
80 L.and_intro(B.wb(sd, B.at(nbs, q)), B.all_lt(B.PWell{nbs, sd}, q), wlf_c(nbs, obs, j, n2, hf, sd, hw, q, hq, B.occ(B.at(nbs, q)), {==}), well_from(nbs, obs, j, n2, hf, sd, hw, q, N.lt_le(q, n2, hq)))
81
82# ---- slots ----
83
84def nsb_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +t: Nat, +h: {ST.noslot(O, t, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(IM.bupd(O, i, B.BE{}), j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), j)))), t))) == True{} : Bool}:
85 match c:
86 case True{}:
87 L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), t))) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.BE{}, IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)), {==})
88 case False{}:
89 L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), t))) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), IM.noslot_inst(O, t, n, h, j, hj))
90
91# THEOREM: emptying a bucket frees no slot another bucket was using
92def ns_be(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +t: Nat, +h: {ST.noslot(O, t, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {ST.noslot(IM.bupd(O, i, B.BE{}), t, m) == True{} : Bool}:
93 match m:
94 case 0n:
95 {==}
96 case 1n+q:
97 +hq = N.succ_le_lt(q, n, hm)
98 L.and_intro(Bool.not(Bool.and(B.occ(B.at(IM.bupd(O, i, B.BE{}), q)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), q)))), t))), ST.noslot(IM.bupd(O, i, B.BE{}), t, q), nsb_i(O, n, i, hi, hlen, t, h, q, hq, Nat.is_eq(i, q), {==}), ns_be(O, n, i, hi, hlen, t, h, q, N.lt_le(q, n, hq)))
99
100
101def pno_be_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +q: String, +hno: {B.all_lt(B.PNo{O, q}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), j))) == True{} : Bool}:
102 match c:
103 case True{}:
104 L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.BE{}, IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)), {==})
105 case False{}:
106 L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), B.all_inst(B.PNo{O, q}, n, hno, j, hj))
107
108def pno_be(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +q: String, +hno: {B.all_lt(B.PNo{O, q}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, m) == True{} : Bool}:
109 match m:
110 case 0n:
111 {==}
112 case 1n+p:
113 +hp = N.succ_le_lt(p, n, hm)
114 L.and_intro(Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), p))), B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, p), pno_be_i(O, n, i, hi, hlen, q, hno, p, hp, Nat.is_eq(i, p), {==}), pno_be(O, n, i, hi, hlen, q, hno, p, N.lt_le(p, n, hp)))
115
116def hold_eqk(+b: B.Bk, +key: String, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}) -> {B.hold(key, b) == B.hold(q, b) : Bool}:
117 match b:
118 case B.BE{}:
119 {==}
120 case B.BF{w, l, +k}:
121 SL.eq_tr2(k, key, q, hq)
122
123def pnq_i(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), j))) == True{} : Bool}:
124 match c:
125 case True{}:
126 L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.BE{}, IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)), {==})
127 case False{}:
128 +o = LK.other(O, n, key, huq, i, hi, hk, j, hj, N.is_eq_sym_false(i, j, hc))
129 L.subst(B.Bk, y => {Bool.not(B.hold(q, y)) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), IM.at_bupd_other(O, i, B.BE{}, j, hc)), L.subst(Bool, x => {Bool.not(x) == True{} : Bool}, B.hold(key, B.at(O, j)), B.hold(q, B.at(O, j)), hold_eqk(B.at(O, j), key, q, hq), o))
130
131# THEOREM: once its bucket is emptied, the removed key is held nowhere
132def pno_rmq(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, m) == True{} : Bool}:
133 match m:
134 case 0n:
135 {==}
136 case 1n+p:
137 +hp = N.succ_le_lt(p, n, hm)
138 L.and_intro(Bool.not(B.hold(q, B.at(IM.bupd(O, i, B.BE{}), p))), B.all_lt(B.PNo{IM.bupd(O, i, B.BE{}), q}, p), pnq_i(O, n, i, hi, hlen, huq, key, hk, q, hq, p, hp, Nat.is_eq(i, p), {==}), pno_rmq(O, n, i, hi, hlen, huq, key, hk, q, hq, p, N.lt_le(p, n, hp)))
139
140def lkr_h(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +mm: Maybe<&2, V>, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, e0: T.Holder(O, q, n)) -> {S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q) == S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q) : Maybe<&2, V>}:
141 match e0:
142 case Tuple{+j, Tuple{+hj, +hkj}}:
143 +hji = SV.neq_hold(O, key, q, i, j, hk, hq, hkj, Nat.is_eq(j, i), {==})
144 +eat = IM.at_bupd_other(O, i, B.BE{}, j, N.is_eq_sym_false(j, i, hji))
145 +hkj2 = L.subst(B.Bk, y => {B.hold(q, y) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat), hkj)
146 +sj = UD.v(H.slot(B.lnk(B.at(O, j))))
147 +hne = N.is_eq_sym_false(sj, UD.v(H.slot(B.lnk(B.at(O, i)))), T.slot_ne(O, n, huq, i, j, hi, hj, hji, B.hold_occ(key, B.at(O, i), hk), B.hold_occ(q, B.at(O, j), hkj)))
148 Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), j))))), S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), LK.lookup_hit(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), q, n, DM.uq_rm(O, i, hlen, n, huq, n, N.le_refl(n)), j, hj, hkj2), Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), UD.v(H.slot(B.lnk(B.at(IM.bupd(O, i, B.BE{}), j))))), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), sj), S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), Equal.cong(B.Bk, Maybe<&2, V>, y => ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), UD.v(H.slot(B.lnk(y)))), B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat), Equal.trans(Maybe<&2, V>, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), sj), ST.nthm(~V, vsl, sj), S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), T.nthm_upd_other(~V, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), sj, mm, hne), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), ST.nthm(~V, vsl, sj), LK.lookup_hit(~V, O, vsl, q, n, huq, j, hj, hkj)))))
149
150def lkr_c(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +mm: Maybe<&2, V>, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +d: Bool, +hd: {B.all_lt(B.PNo{O, q}, n) == d : Bool}) -> {S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q) == S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q) : Maybe<&2, V>}:
151 match d:
152 case True{}:
153 Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q), None{}, S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), LK.lookup_none(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), q, n, pno_be(O, n, i, hi, hlen, q, hd, n, N.le_refl(n))), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q), None{}, LK.lookup_none(~V, O, vsl, q, n, hd)))
154 case False{}:
155 lkr_h(~V, O, n, i, hi, hlen, huq, key, hk, vsl, mm, q, hq, T.find_hold(O, q, n, hd))
156
157# THEOREM: emptying key's bucket and its slot leaves every other key's lookup
158def lk_rm(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +huq: {B.all_lt(B.PUniq{O}, n) == True{} : Bool}, +key: String, +hk: {B.hold(key, B.at(O, i)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +mm: Maybe<&2, V>, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}) -> {S.lookup(~V, ST.absm(~V, IM.bupd(O, i, B.BE{}), SC.update(Maybe<&2, V>, vsl, UD.v(H.slot(B.lnk(B.at(O, i)))), mm), n, 0n), q) == S.lookup(~V, ST.absm(~V, O, vsl, n, 0n), q) : Maybe<&2, V>}:
159 lkr_c(~V, O, n, i, hi, hlen, huq, key, hk, vsl, mm, q, hq, B.all_lt(B.PNo{O, q}, n), {==})
160
161# ---- liveness with the slot vacated ----
162
163def lvr_b(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +s: Nat, +fr: Nat, +b: B.Bk, +h: {B.live_b(ST.lvs(~V, vsl), fr, b) == True{} : Bool}, +hne: {Bool.not(Bool.and(B.occ(b), Nat.is_eq(UD.v(H.slot(B.lnk(b))), s))) == True{} : Bool}) -> {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, b) == True{} : Bool}:
164 match b:
165 case B.BE{}:
166 {==}
167 case B.BF{w, +l, k}:
168 +t = UD.v(H.slot(l))
169 +ne = N.is_eq_sym_false(t, s, K.not_true_eq(Nat.is_eq(t, s), hne))
170 +e = Equal.trans(Bool, B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), t), ST.some_b(~V, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t)), B.nthb(ST.lvs(~V, vsl), t), ST.lvs_nth(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t), Equal.trans(Bool, ST.some_b(~V, ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t)), ST.some_b(~V, ST.nthm(~V, vsl, t)), B.nthb(ST.lvs(~V, vsl), t), Equal.cong(Maybe<&2, V>, Bool, m => ST.some_b(~V, m), ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, None{}), t), ST.nthm(~V, vsl, t), T.nthm_upd_other(~V, vsl, s, t, None{}, ne)), Equal.sym(Bool, B.nthb(ST.lvs(~V, vsl), t), ST.some_b(~V, ST.nthm(~V, vsl, t)), ST.lvs_nth(~V, vsl, t))))
171 L.and_intro(B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), t), Nat.is_lt(t, fr), Equal.trans(Bool, B.nthb(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), t), B.nthb(ST.lvs(~V, vsl), t), True{}, e, L.and_left(B.nthb(ST.lvs(~V, vsl), t), Nat.is_lt(t, fr), h)), L.and_right(B.nthb(ST.lvs(~V, vsl), t), Nat.is_lt(t, fr), h))
172
173def lvr_i(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +hl: {B.all_lt(B.PLive{O, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +s: Nat, +hns: {ST.noslot(IM.bupd(O, i, B.BE{}), s, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(i, j) == c : Bool}) -> {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, B.at(IM.bupd(O, i, B.BE{}), j)) == True{} : Bool}:
174 match c:
175 case True{}:
176 L.subst(B.Bk, y => {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, y) == True{} : Bool}, B.BE{}, B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.BE{}, IM.at_bu_eq(O, i, B.BE{}, hlen, j, hc)), {==})
177 case False{}:
178 +eat = IM.at_bupd_other(O, i, B.BE{}, j, hc)
179 +hne = L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), s))) == True{} : Bool}, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat, IM.noslot_inst(IM.bupd(O, i, B.BE{}), s, n, hns, j, hj))
180 L.subst(B.Bk, y => {B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, y) == True{} : Bool}, B.at(O, j), B.at(IM.bupd(O, i, B.BE{}), j), Equal.sym(B.Bk, B.at(IM.bupd(O, i, B.BE{}), j), B.at(O, j), eat), lvr_b(~V, vsl, s, fr, B.at(O, j), B.all_inst(B.PLive{O, ST.lvs(~V, vsl), fr}, n, hl, j, hj), hne))
181
182# THEOREM: the other buckets stay live once the removed slot is vacant
183def live_rm(~V: Data, +O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +vsl: List<&2, Maybe<&2, V>>, +fr: Nat, +hl: {B.all_lt(B.PLive{O, ST.lvs(~V, vsl), fr}, n) == True{} : Bool}, +s: Nat, +hns: {ST.noslot(IM.bupd(O, i, B.BE{}), s, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PLive{IM.bupd(O, i, B.BE{}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr}, m) == True{} : Bool}:
184 match m:
185 case 0n:
186 {==}
187 case 1n+q:
188 +hq = N.succ_le_lt(q, n, hm)
189 L.and_intro(B.live_b(ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr, B.at(IM.bupd(O, i, B.BE{}), q)), B.all_lt(B.PLive{IM.bupd(O, i, B.BE{}), ST.lvs(~V, SC.update(Maybe<&2, V>, vsl, s, None{})), fr}, q), lvr_i(~V, O, n, i, hi, hlen, vsl, fr, hl, s, hns, q, hq, Nat.is_eq(i, q), {==}), live_rm(~V, O, n, i, hi, hlen, vsl, fr, hl, s, hns, q, N.lt_le(q, n, hq)))
190
191# ---- the free list after pushing the vacated slot ----
192
193def subl_refl(+xs: List<&2, Nat>) -> {IF.subl(xs, xs) == True{} : Bool}:
194 match xs:
195 case Nil{}:
196 {==}
197 case Con{+x, +t}:
198 L.and_intro(NL.memn(x, Con{x, t}), IF.subl(t, Con{x, t}), L.subst(Bool, b => {Bool.or(b, NL.memn(x, t)) == True{} : Bool}, True{}, Nat.is_eq(x, x), Equal.sym(Bool, Nat.is_eq(x, x), True{}, N.is_eq_refl(x)), {==}), IF.subl_cons(t, t, x, subl_refl(t)))
199
200def mem_self(+t: Nat, +xs: List<&2, Nat>) -> {NL.memn(t, Con{t, xs}) == True{} : Bool}:
201 L.subst(Bool, b => {Bool.or(b, NL.memn(t, xs)) == True{} : Bool}, True{}, Nat.is_eq(t, t), Equal.sym(Bool, Nat.is_eq(t, t), True{}, N.is_eq_refl(t)), {==})
202
203
204# the two orders of visiting s and t
205def subl_sw(+s: Nat, +t: Nat, +seen: List<&2, Nat>) -> {IF.subl(Con{t, Con{s, seen}}, Con{s, Con{t, seen}}) == True{} : Bool}:
206 L.and_intro(NL.memn(t, Con{s, Con{t, seen}}), IF.subl(Con{s, seen}, Con{s, Con{t, seen}}), IF.mem_cons(t, s, Con{t, seen}, mem_self(t, seen)), L.and_intro(NL.memn(s, Con{s, Con{t, seen}}), IF.subl(seen, Con{s, Con{t, seen}}), mem_self(s, Con{t, seen}), IF.subl_cons(seen, Con{t, seen}, s, IF.subl_cons(seen, seen, t, subl_refl(seen)))))
207
208
209# THEOREM: the old free list is still valid after pushing the vacated slot
210def fl_pr(+O: List<&2, B.Bk>, +n: Nat, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hlen: {Nat.is_lt(i, SC.length(B.Bk, O)) == True{} : Bool}, +Vf: List<&2, B.Bk>, +hf: {B.all_lt(B.PFrom{Vf, IM.bupd(O, i, B.BE{}), n}, n) == True{} : Bool}, +hoi: {B.occ(B.at(O, i)) == True{} : Bool}, +nxl: List<&2, U32>, +fv: U32, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>, +h: {ST.fl_ok(O, n, nxl, cnt, f, fr, seen) == True{} : Bool}) -> {ST.fl_ok(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), cnt, f, fr, Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}) == True{} : Bool}:
211 match cnt:
212 case 0n:
213 h
214 case 1n+p:
215 +x1 = Bool.not(U32.is_eq(f, 0))
216 +y = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen))))
217 +tl = ST.fl_ok(O, n, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})
218 +z = Bool.and(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))
219 +a2 = L.and_left(y, tl, L.and_right(x1, Bool.and(y, tl), h))
220 +a5 = L.and_right(y, tl, L.and_right(x1, Bool.and(y, tl), h))
221 +ns = L.and_left(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
222 +nm = L.and_right(ST.noslot(O, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
223 +ne = IM.slot_other(B.at(O, i), UD.v(H.slot(f)), hoi, IM.noslot_inst(O, UD.v(H.slot(f)), n, ns, i, hi))
224 +ns2 = RH.ns_from(Vf, IM.bupd(O, i, B.BE{}), n, n, hf, UD.v(H.slot(f)), ns_be(O, n, i, hi, hlen, UD.v(H.slot(f)), ns, n, N.le_refl(n)), n, N.le_refl(n))
225 +nm2 = L.subst(Bool, b => {Bool.not(Bool.or(b, NL.memn(UD.v(H.slot(f)), seen))) == True{} : Bool}, False{}, Nat.is_eq(UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f))), Equal.sym(Bool, Nat.is_eq(UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f))), False{}, ne), nm)
226 +enx = W32.nth0_upd_other(nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f)), fv, ne)
227 +r0 = fl_pr(O, n, i, hi, hlen, Vf, hf, hoi, nxl, fv, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}, a5)
228 +r1 = L.subst(U32, g => {ST.fl_ok(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), p, g, fr, Con{UD.v(H.slot(B.lnk(B.at(O, i)))), Con{UD.v(H.slot(f)), seen}}) == True{} : Bool}, W32.nth0(nxl, UD.v(H.slot(f))), W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), Equal.sym(U32, W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), W32.nth0(nxl, UD.v(H.slot(f))), enx), r0)
229 +r2 = IF.fl_weak(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), p, W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), fr, Con{UD.v(H.slot(B.lnk(B.at(O, i)))), Con{UD.v(H.slot(f)), seen}}, Con{UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}}, subl_sw(UD.v(H.slot(B.lnk(B.at(O, i)))), UD.v(H.slot(f)), seen), r1)
230 +y2 = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(Vf, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}))))
231 +tl2 = ST.fl_ok(Vf, n, SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), p, W32.nth0(SC.update(U32, nxl, UD.v(H.slot(B.lnk(B.at(O, i)))), fv), UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}})
232 L.and_intro(x1, Bool.and(y2, tl2), L.and_left(x1, Bool.and(y, tl), h), L.and_intro(y2, tl2, L.and_intro(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(Vf, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen}))), L.and_left(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2), L.and_intro(ST.noslot(Vf, UD.v(H.slot(f)), n), Bool.not(NL.memn(UD.v(H.slot(f)), Con{UD.v(H.slot(B.lnk(B.at(O, i)))), seen})), ns2, nm2)), r2))
233
234# ---- the model's keys have no repeats ----
235
236def mk_b(+key: String, +b: B.Bk, +r: List<&2, String>, +hnh: {Bool.not(B.hold(key, b)) == True{} : Bool}, +hr: {S.mem(key, r) == False{} : Bool}) -> {S.mem(key, SC.append(String, KW.kof(b), r)) == False{} : Bool}:
237 match b:
238 case B.BE{}:
239 hr
240 case B.BF{w, l, +k}:
241 L.subst(Bool, x => {Bool.or(x, S.mem(key, r)) == False{} : Bool}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, K.not_true_eq(S.str_eq(k, key), hnh)), hr)
242
243def mem_kb(+bs: List<&2, B.Bk>, +key: String, +m: Nat, +j: Nat, +h: {LK.nob(bs, key, m, j) == True{} : Bool}) -> {S.mem(key, KW.kb(bs, m, j)) == False{} : Bool}:
244 match m:
245 case 0n:
246 {==}
247 case 1n+p:
248 mk_b(key, B.at(bs, j), KW.kb(bs, p, 1n+j), L.and_left(Bool.not(B.hold(key, B.at(bs, j))), LK.nob(bs, key, p, 1n+j), h), mem_kb(bs, key, p, 1n+j, L.and_right(Bool.not(B.hold(key, B.at(bs, j))), LK.nob(bs, key, p, 1n+j), h)))
249
250def nd_b(+bs: List<&2, B.Bk>, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +p: Nat, +hjm: {Nat.is_le(Nat.add(1n+j, p), n) == True{} : Bool}, +b: B.Bk, +hb: {B.at(bs, j) == b : B.Bk}, +hr: {S.nodup(KW.kb(bs, p, 1n+j)) == True{} : Bool}) -> {S.nodup(SC.append(String, KW.kof(b), KW.kb(bs, p, 1n+j))) == True{} : Bool}:
251 match b:
252 case B.BE{}:
253 hr
254 case B.BF{w, l, +k}:
255 +hk = L.subst(B.Bk, y => {B.hold(k, y) == True{} : Bool}, B.BF{w, l, k}, B.at(bs, j), Equal.sym(B.Bk, B.at(bs, j), B.BF{w, l, k}, hb), K.str_refl(k))
256 +nm = mem_kb(bs, k, p, 1n+j, LK.nob_past(bs, n, k, huq, j, hj, hk, p, 1n+j, hjm, N.lt_succ(j)))
257 L.and_intro(Bool.not(S.mem(k, KW.kb(bs, p, 1n+j))), S.nodup(KW.kb(bs, p, 1n+j)), IM.not_f(S.mem(k, KW.kb(bs, p, 1n+j)), nm), hr)
258
259def nodup_kb(+bs: List<&2, B.Bk>, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}) -> {S.nodup(KW.kb(bs, m, j)) == True{} : Bool}:
260 match m:
261 case 0n:
262 {==}
263 case 1n+p:
264 +hj = IA.idx_lt(j, p, n, hjm)
265 +hjm2 = IA.idx_next(j, p, n, hjm)
266 nd_b(bs, n, huq, j, hj, p, hjm2, B.at(bs, j), {==}, nodup_kb(bs, n, huq, p, 1n+j, hjm2))
267
268# THEOREM: the model of a table with unique keys has no repeated key
269def nodup_model(~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}, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}) -> {S.nodup(S.keys(~V, ST.absm(~V, bs, vsl, n, 0n))) == True{} : Bool}:
270 L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, KW.kb(bs, n, 0n), S.keys(~V, ST.absm(~V, bs, vsl, n, 0n)), Equal.sym(List<&2, String>, S.keys(~V, ST.absm(~V, bs, vsl, n, 0n)), KW.kb(bs, n, 0n), KW.keys_absm(~V, bs, vsl, fr, n, hl, n, 0n, N.le_refl(n))), nodup_kb(bs, n, huq, n, 0n, N.le_refl(n)))
271
272# ---- a key cell no bucket uses ----
273
274def kd_i(+tb: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +n: Nat, +hns: {ST.noslot(TB.buckets(tb, kl, n), s, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}) -> {Bool.not(Bool.and(B.occ(TB.dec(tb, kl, i)), Nat.is_eq(UD.v(H.slot(B.lnk(TB.dec(tb, kl, i)))), s))) == True{} : Bool}:
275 L.subst(B.Bk, y => {Bool.not(Bool.and(B.occ(y), Nat.is_eq(UD.v(H.slot(B.lnk(y))), s))) == True{} : Bool}, B.at(TB.buckets(tb, kl, n), i), TB.dec(tb, kl, i), TB.at_buckets(tb, kl, n, i, hi), IM.noslot_inst(TB.buckets(tb, kl, n), s, n, hns, i, hi))
276
277def kd(+tb: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +sk: String, +n: Nat, +hns: {ST.noslot(TB.buckets(tb, kl, n), s, n) == True{} : Bool}, +m: Nat, +i: Nat, +hmi: {Nat.is_le(Nat.add(i, m), n) == True{} : Bool}) -> {TB.dlist(tb, SC.update(String, kl, s, sk), m, i) == TB.dlist(tb, kl, m, i) : List<&2, B.Bk>}:
278 match m:
279 case 0n:
280 {==}
281 case 1n+p:
282 +hi = IA.idx_lt(i, p, n, hmi)
283 IA.con_eq(TB.dec(tb, SC.update(String, kl, s, sk), i), TB.dec(tb, kl, i), TB.dlist(tb, SC.update(String, kl, s, sk), p, 1n+i), TB.dlist(tb, kl, p, 1n+i), IA.dec_same_c(W32.nth0(tb, Nat.double(i)), W32.nth0(tb, 1n+Nat.double(i)), kl, s, sk, U32.is_eq(W32.nth0(tb, Nat.double(i)), 0), kd_i(tb, kl, s, n, hns, i, hi)), kd(tb, kl, s, sk, n, hns, p, 1n+i, IA.idx_next(i, p, n, hmi)))
284
285# THEOREM: rewriting a key cell no bucket uses leaves every bucket
286def bs_key(+tb: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +sk: String, +n: Nat, +hns: {ST.noslot(TB.buckets(tb, kl, n), s, n) == True{} : Bool}) -> {TB.buckets(tb, SC.update(String, kl, s, sk), n) == TB.buckets(tb, kl, n) : List<&2, B.Bk>}:
287 kd(tb, kl, s, sk, n, hns, n, 0n, N.le_refl(n))