1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../../spec/lib/common.bend as SC 5 import ../../lib/u32div.bend as UD 6 import ../../../src/containers/hash_table.bend as H 7 import ./words.bend as WR 8 import ./buckets.bend as B 9 import ./state.bend as ST 10 import ./insm.bend as IM 11 import ../../lib/nat_list.bend as NL 12 import ../../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 18 def 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 27 def 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 30 def 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 34 def 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 55 def 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 62 def 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 69 def 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 76 def 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 83 def 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 90 def 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 94 def 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 112 def 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 120 def 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 128 def 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 132 def 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 141 def 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 149 def 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)))