proofs/containers/hash_table/insf.bend
bend-collections-laws-containers@1.0.0.0 · 155 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/proofs/lib/u32div.bend as UD
6import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/words.bend as WR
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
13
14# The free list across an insertion: its slots stay unused when the new
15# bucket takes a slot not on it, and forgetting visited slots keeps it valid.
16
17
18def mem_ne_c(+a: Nat, +t: Nat, +seen: List<&2, Nat>, +ha: {NL.memn(a, seen) == True{} : Bool}, +ht: {Bool.not(NL.memn(t, seen)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(a, t) == c : Bool}) -> {c == False{} : Bool}:
19 match c:
20 case False{}:
21 {==}
22 case True{}:
23 +h2 = L.subst(Nat, z => {NL.memn(z, seen) == True{} : Bool}, a, t, N.eq_from_is_eq(a, t, hc), ha)
24 Empty.absurd({True{} == False{} : Bool}, L.false_true(L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, NL.memn(t, seen), True{}, h2, ht)))
25
26# a slot on the list and a slot not on it differ
27def mem_ne(+a: Nat, +t: Nat, +seen: List<&2, Nat>, +ha: {NL.memn(a, seen) == True{} : Bool}, +ht: {Bool.not(NL.memn(t, seen)) == True{} : Bool}) -> {Nat.is_eq(a, t) == False{} : Bool}:
28 mem_ne_c(a, t, seen, ha, ht, Nat.is_eq(a, t), {==})
29
30def mem_cons(+a: Nat, +t: Nat, +seen: List<&2, Nat>, +ha: {NL.memn(a, seen) == True{} : Bool}) -> {NL.memn(a, Con{t, seen}) == True{} : Bool}:
31 L.subst(Bool, b => {Bool.or(Nat.is_eq(t, a), b) == True{} : Bool}, True{}, NL.memn(a, seen), Equal.sym(Bool, NL.memn(a, seen), True{}, ha), WR.or_true(Nat.is_eq(t, a)))
32
33# THEOREM: filling bucket e with a slot the list has visited keeps the list valid
34def fl_tr(+bs: List<&2, B.Bk>, +e: Nat, +he: {Nat.is_lt(e, SC.length(B.Bk, bs)) == True{} : Bool}, +w: U32, +L: U32, +key: String, +nb: Nat, +nxl: List<&2, U32>, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>, +hm: {NL.memn(UD.v(H.slot(L)), seen) == True{} : Bool}, +h: {ST.fl_ok(bs, nb, nxl, cnt, f, fr, seen) == True{} : Bool}) -> {ST.fl_ok(IM.bupd(bs, e, B.BF{w, L, key}), nb, nxl, cnt, f, fr, seen) == True{} : Bool}:
35 match cnt:
36 case 0n:
37 h
38 case 1n+p:
39 +x1 = Bool.not(U32.is_eq(f, 0))
40 +x2 = Bool.and(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))), ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}))
41 +y = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen))))
42 +z = Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))
43 +a1 = L.and_left(x1, x2, h)
44 +a2 = L.and_left(y, ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}), L.and_right(x1, x2, h))
45 +a5 = L.and_right(y, ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}), L.and_right(x1, x2, h))
46 +lt = L.and_left(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2)
47 +ns = L.and_left(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
48 +nm = L.and_right(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
49 +ns2 = IM.noslot_up(bs, e, he, w, L, key, UD.v(H.slot(f)), mem_ne(UD.v(H.slot(L)), UD.v(H.slot(f)), seen, hm, nm), nb, ns)
50 +r5 = fl_tr(bs, e, he, w, L, key, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}, mem_cons(UD.v(H.slot(L)), UD.v(H.slot(f)), seen, hm), a5)
51 L.and_intro(x1, Bool.and(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(IM.bupd(bs, e, B.BF{w, L, key}), UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))), ST.fl_ok(IM.bupd(bs, e, B.BF{w, L, key}), nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})), a1, L.and_intro(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(IM.bupd(bs, e, B.BF{w, L, key}), UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))), ST.fl_ok(IM.bupd(bs, e, B.BF{w, L, key}), nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}), L.and_intro(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(IM.bupd(bs, e, B.BF{w, L, key}), UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen))), lt, L.and_intro(ST.noslot(IM.bupd(bs, e, B.BF{w, L, key}), UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), ns2, nm)), r5))
52
53# ---- forgetting visited slots ----
54
55def subl(+xs: List<&2, Nat>, +ys: List<&2, Nat>) -> Bool:
56 match xs:
57 case Nil{}:
58 True{}
59 case Con{+x, t}:
60 Bool.and(NL.memn(x, ys), subl(t, ys))
61
62def ms_c(+t: Nat, +x: Nat, +r: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {NL.memn(x, ys) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(x, t) == c : Bool}, +hm: {Bool.or(c, NL.memn(t, r)) == True{} : Bool}, rec: @hr: {NL.memn(t, r) == True{} : Bool} -> {NL.memn(t, ys) == True{} : Bool}) -> {NL.memn(t, ys) == True{} : Bool}:
63 match c:
64 case True{}:
65 L.subst(Nat, z => {NL.memn(z, ys) == True{} : Bool}, x, t, N.eq_from_is_eq(x, t, hc), hx)
66 case False{}:
67 rec(hm)
68
69def memn_sub(+t: Nat, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +hs: {subl(xs, ys) == True{} : Bool}, +hm: {NL.memn(t, xs) == True{} : Bool}) -> {NL.memn(t, ys) == True{} : Bool}:
70 match xs:
71 case Nil{}:
72 Empty.absurd({NL.memn(t, ys) == True{} : Bool}, L.false_true(hm))
73 case Con{+x, r}:
74 ms_c(t, x, r, ys, L.and_left(NL.memn(x, ys), subl(r, ys), hs), Nat.is_eq(x, t), {==}, hm, hr => memn_sub(t, r, ys, L.and_right(NL.memn(x, ys), subl(r, ys), hs), hr))
75
76def nm_c(+t: Nat, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +hs: {subl(xs, ys) == True{} : Bool}, +h: {Bool.not(NL.memn(t, ys)) == True{} : Bool}, +c: Bool, +hc: {NL.memn(t, xs) == c : Bool}) -> {Bool.not(c) == True{} : Bool}:
77 match c:
78 case False{}:
79 {==}
80 case True{}:
81 Empty.absurd({Bool.not(True{}) == True{} : Bool}, L.false_true(L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, NL.memn(t, ys), True{}, memn_sub(t, xs, ys, hs, hc), h)))
82
83def subl_cons(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +y: Nat, +h: {subl(xs, ys) == True{} : Bool}) -> {subl(xs, Con{y, ys}) == True{} : Bool}:
84 match xs:
85 case Nil{}:
86 {==}
87 case Con{+x, r}:
88 L.and_intro(NL.memn(x, Con{y, ys}), subl(r, Con{y, ys}), mem_cons(x, y, ys, L.and_left(NL.memn(x, ys), subl(r, ys), h)), subl_cons(r, ys, y, L.and_right(NL.memn(x, ys), subl(r, ys), h)))
89
90def subl_both(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +t: Nat, +h: {subl(xs, ys) == True{} : Bool}) -> {subl(Con{t, xs}, Con{t, ys}) == True{} : Bool}:
91 L.and_intro(NL.memn(t, Con{t, ys}), subl(xs, Con{t, ys}), L.subst(Bool, b => {Bool.or(b, NL.memn(t, ys)) == True{} : Bool}, True{}, Nat.is_eq(t, t), Equal.sym(Bool, Nat.is_eq(t, t), True{}, N.is_eq_refl(t)), {==}), subl_cons(xs, ys, t, h))
92
93# THEOREM: a valid list stays valid when fewer slots count as visited
94def fl_weak(+bs: List<&2, B.Bk>, +nb: Nat, +nxl: List<&2, U32>, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>, +seen2: List<&2, Nat>, +hs: {subl(seen2, seen) == True{} : Bool}, +h: {ST.fl_ok(bs, nb, nxl, cnt, f, fr, seen) == True{} : Bool}) -> {ST.fl_ok(bs, nb, nxl, cnt, f, fr, seen2) == True{} : Bool}:
95 match cnt:
96 case 0n:
97 h
98 case 1n+p:
99 +x1 = Bool.not(U32.is_eq(f, 0))
100 +x2 = Bool.and(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))), ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}))
101 +y = Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen))))
102 +z = Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))
103 +a2 = L.and_left(y, ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}), L.and_right(x1, x2, h))
104 +a5 = L.and_right(y, ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}), L.and_right(x1, x2, h))
105 +nm = L.and_right(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2))
106 +nm2 = nm_c(UD.v(H.slot(f)), seen2, seen, hs, nm, NL.memn(UD.v(H.slot(f)), seen2), {==})
107 L.and_intro(x1, Bool.and(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen2)))), ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen2})), L.and_left(x1, x2, h), L.and_intro(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen2)))), ST.fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen2}), L.and_intro(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen2))), L.and_left(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2), L.and_intro(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen2)), L.and_left(ST.noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)), L.and_right(Nat.is_lt(UD.v(H.slot(f)), fr), z, a2)), nm2)), fl_weak(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen}, Con{UD.v(H.slot(f)), seen2}, subl_both(seen2, seen, UD.v(H.slot(f)), hs), a5)))
108
109# ---- the list's length ----
110
111# an empty list (link 0) has no links
112def cnt_zero(+bs: List<&2, B.Bk>, +nb: Nat, +nxl: List<&2, U32>, +cnt: Nat, +fr: Nat, +seen: List<&2, Nat>, +h: {ST.fl_ok(bs, nb, nxl, cnt, 0, fr, seen) == True{} : Bool}) -> {cnt == 0n : Nat}:
113 match cnt:
114 case 0n:
115 {==}
116 case 1n+p:
117 Empty.absurd({1n+p == 0n : Nat}, L.false_true(h))
118
119# a list that is not empty has a first link
120def cnt_pos(+bs: List<&2, B.Bk>, +nb: Nat, +nxl: List<&2, U32>, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>, +hf: {U32.is_eq(f, 0) == False{} : Bool}, +h: {ST.fl_ok(bs, nb, nxl, cnt, f, fr, seen) == True{} : Bool}) -> Sigma<&1, &1, Nat, p => {cnt == 1n+p : Nat}>:
121 match cnt:
122 case 0n:
123 Empty.absurd(Sigma<&1, &1, Nat, p => {0n == 1n+p : Nat}>, L.false_true(Equal.trans(Bool, False{}, U32.is_eq(f, 0), True{}, Equal.sym(Bool, U32.is_eq(f, 0), False{}, hf), h)))
124 case 1n+p:
125 (p, {==})
126
127# with n <= fr and fr - n = 0: fr = n
128def sub_zero_eq(+fr: Nat, +n: Nat, +hle: {Nat.is_le(n, fr) == True{} : Bool}, +h: {Nat.sub(fr, n) == 0n : Nat}) -> {fr == n : Nat}:
129 Equal.trans(Nat, fr, Nat.add(n, Nat.sub(fr, n)), n, Equal.sym(Nat, Nat.add(n, Nat.sub(fr, n)), fr, N.sub_add(fr, n, hle)), Equal.trans(Nat, Nat.add(n, Nat.sub(fr, n)), Nat.add(n, 0n), n, Equal.cong(Nat, Nat, z => Nat.add(n, z), Nat.sub(fr, n), 0n, h), N.add_zero(n)))
130
131# with n <= fr and fr - n = p + 1: n + 1 <= fr and fr - (n + 1) = p
132def sub_step(+fr: Nat, +n: Nat, +p: Nat, +hle: {Nat.is_le(n, fr) == True{} : Bool}, +h: {Nat.sub(fr, n) == 1n+p : Nat}) -> {Nat.sub(fr, 1n+n) == p : Nat} & {Nat.is_le(1n+n, fr) == True{} : Bool}:
133 +efr = Equal.trans(Nat, fr, Nat.add(n, Nat.sub(fr, n)), Nat.add(n, 1n+p), Equal.sym(Nat, Nat.add(n, Nat.sub(fr, n)), fr, N.sub_add(fr, n, hle)), Equal.cong(Nat, Nat, z => Nat.add(n, z), Nat.sub(fr, n), 1n+p, h))
134 +efr2 = Equal.trans(Nat, fr, Nat.add(n, 1n+p), 1n+Nat.add(n, p), efr, N.add_succ(n, p))
135 +es = L.subst(Nat, z => {Nat.sub(z, 1n+n) == p : Nat}, 1n+Nat.add(n, p), fr, Equal.sym(Nat, fr, 1n+Nat.add(n, p), efr2), N.add_sub_cancel(n, p))
136 +el = L.subst(Nat, z => {Nat.is_le(1n+n, z) == True{} : Bool}, 1n+Nat.add(n, p), fr, Equal.sym(Nat, fr, 1n+Nat.add(n, p), efr2), N.le_add_right(n, p))
137 (es, el)
138
139# ---- a fresh slot is used by no bucket ----
140
141def ns_live_b(+lv: List<&2, Bool>, +fr: Nat, +b: B.Bk, +h: {B.live_b(lv, fr, b) == True{} : Bool}) -> {Bool.not(Bool.and(B.occ(b), Nat.is_eq(UD.v(H.slot(B.lnk(b))), fr))) == True{} : Bool}:
142 match b:
143 case B.BE{}:
144 {==}
145 case B.BF{w, +l, k}:
146 IM.not_f(Nat.is_eq(UD.v(H.slot(l)), fr), N.is_eq_lt(UD.v(H.slot(l)), fr, L.and_right(B.nthb(lv, UD.v(H.slot(l))), Nat.is_lt(UD.v(H.slot(l)), fr), h)))
147
148# THEOREM: every bucket's slot is below fresh, so fresh is unused
149def noslot_live(+bs: List<&2, B.Bk>, +lv: List<&2, Bool>, +fr: Nat, +n: Nat, +hl: {B.all_lt(B.PLive{bs, lv, fr}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {ST.noslot(bs, fr, m) == True{} : Bool}:
150 match m:
151 case 0n:
152 {==}
153 case 1n+j:
154 +hj = N.succ_le_lt(j, n, hm)
155 L.and_intro(Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), fr))), ST.noslot(bs, fr, j), ns_live_b(lv, fr, B.at(bs, j), B.all_inst(B.PLive{bs, lv, fr}, n, hl, j, hj)), noslot_live(bs, lv, fr, n, hl, j, N.lt_le(j, n, hj)))