import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ../hash_table/keys.bend as K
import ../hash_table/table.bend as TB
import ../hash_table/buckets.bend as B
import ./state.bend as ST
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32

# The table and the recency list: a probe that misses means no listed slot
# holds the key; a probe that hits names a listed slot holding it.

# a full bucket's key is its word's key over its slot's stored String
def bkok(+kl: List<&2, String>, b: B.Bk) -> Bool:
  match b:
    case B.BE{}:
      True{}
    case B.BF{+w, +l, +k}:
      S.str_eq(k, TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))))

def bkok_dec(+w: U32, +l: U32, +kl: List<&2, String>, +e: Bool) -> {bkok(kl, TB.dec_c(w, l, kl, e)) == True{} : Bool}:
  match e:
    case True{}:
      {==}
    case False{}:
      K.str_refl(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))))

def bkok_at(+tb: List<&2, U32>, +kl: List<&2, String>, +n: Nat, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}) -> {bkok(kl, B.at(TB.buckets(tb, kl, n), j)) == True{} : Bool}:
  L.subst(B.Bk, z => {bkok(kl, z) == True{} : Bool}, TB.dec(tb, kl, j), B.at(TB.buckets(tb, kl, n), j), Equal.sym(B.Bk, B.at(TB.buckets(tb, kl, n), j), TB.dec(tb, kl, j), TB.at_buckets(tb, kl, n, j, hj)), bkok_dec(W32.nth0(tb, Nat.double(j)), W32.nth0(tb, 1n+Nat.double(j)), kl, U32.is_eq(W32.nth0(tb, Nat.double(j)), 0)))


# ---- the miss ----

def nk_bf(+kl: List<&2, String>, +key: String, +w: U32, +l: U32, +w2: U32, +l2: U32, +k2: String, +hbk: {S.str_eq(k2, TB.keyof(w2, TB.nths(kl, UD.v(H.slot(l2))))) == True{} : Bool}, +hno: {Bool.not(S.str_eq(k2, key)) == True{} : Bool}, +hi: {Bool.and(U32.is_eq(w2, w), U32.is_eq(l2, l)) == True{} : Bool}) -> {Bool.not(S.str_eq(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), key)) == True{} : Bool}:
  +ew = A.eq_of(w2, w, L.and_left(U32.is_eq(w2, w), U32.is_eq(l2, l), hi))
  +el = A.eq_of(l2, l, L.and_right(U32.is_eq(w2, w), U32.is_eq(l2, l), hi))
  +e1 = K.str_eq_of(k2, TB.keyof(w2, TB.nths(kl, UD.v(H.slot(l2)))), hbk)
  +e2 = Equal.cong(U32, String, z => TB.keyof(z, TB.nths(kl, UD.v(H.slot(l2)))), w2, w, ew)
  +e3 = Equal.cong(U32, String, z => TB.keyof(w, TB.nths(kl, UD.v(H.slot(z)))), l2, l, el)
  +e = Equal.trans(String, k2, TB.keyof(w2, TB.nths(kl, UD.v(H.slot(l2)))), TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), e1, Equal.trans(String, TB.keyof(w2, TB.nths(kl, UD.v(H.slot(l2)))), TB.keyof(w, TB.nths(kl, UD.v(H.slot(l2)))), TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), e2, e3))
  L.subst(String, z => {Bool.not(S.str_eq(z, key)) == True{} : Bool}, k2, TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), e, hno)

# a bucket with word w and link l does not hold key: nor does that word's key
def nk_b(+kl: List<&2, String>, +key: String, +w: U32, +l: U32, +b: B.Bk, +hbk: {bkok(kl, b) == True{} : Bool}, +hno: {Bool.not(B.hold(key, b)) == True{} : Bool}, +hi: {ST.isbf(b, w, l) == True{} : Bool}) -> {Bool.not(S.str_eq(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), key)) == True{} : Bool}:
  match b:
    case B.BE{}:
      Empty.absurd({Bool.not(S.str_eq(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), key)) == True{} : Bool}, L.false_true(hi))
    case B.BF{+w2, +l2, +k2}:
      nk_bf(kl, key, w, l, w2, l2, k2, hbk, hno, hi)

def nk_c(+tb: List<&2, U32>, +kl: List<&2, String>, +n: Nat, +key: String, +w: U32, +l: U32, +j: Nat, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +hno: {Bool.not(B.hold(key, B.at(TB.buckets(tb, kl, n), j))) == True{} : Bool}, +c: Bool, +hc: {ST.isbf(B.at(TB.buckets(tb, kl, n), j), w, l) == c : Bool}, +ho: {Bool.or(c, ST.anyb(TB.buckets(tb, kl, n), j, l, w)) == True{} : Bool}, rec: @h: {ST.anyb(TB.buckets(tb, kl, n), j, l, w) == True{} : Bool} -> {Bool.not(S.str_eq(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), key)) == True{} : Bool}) -> {Bool.not(S.str_eq(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), key)) == True{} : Bool}:
  match c:
    case True{}:
      nk_b(kl, key, w, l, B.at(TB.buckets(tb, kl, n), j), bkok_at(tb, kl, n, j, hj), hno, hc)
    case False{}:
      rec(ho)

# no bucket holds key, one has word w and link l: that word's key is not key
def anyb_nk(+tb: List<&2, U32>, +kl: List<&2, String>, +n: Nat, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(tb, kl, n), key}, n) == True{} : Bool}, +w: U32, +l: U32, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}, +ha: {ST.anyb(TB.buckets(tb, kl, n), m, l, w) == True{} : Bool}) -> {Bool.not(S.str_eq(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), key)) == True{} : Bool}:
  match m:
    case 0n:
      Empty.absurd({Bool.not(S.str_eq(TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), key)) == True{} : Bool}, L.false_true(ha))
    case 1n+j:
      +hj = N.succ_le_lt(j, n, hm)
      nk_c(tb, kl, n, key, w, l, j, hj, B.all_inst(B.PNo{TB.buckets(tb, kl, n), key}, n, hno, j, hj), ST.isbf(B.at(TB.buckets(tb, kl, n), j), w, l), {==}, ha, h => anyb_nk(tb, kl, n, key, hno, w, l, j, N.lt_le(j, n, hj), h))

# the slot of a slot's link

# THEOREM (table side, miss): no bucket holds key, so no listed slot does
def nokey_of(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +tb: List<&2, U32>, +kl: List<&2, String>, +n: Nat, +key: String, +hno: {B.all_lt(B.PNo{TB.buckets(tb, kl, n), key}, n) == True{} : Bool}, +ll: List<&2, U32>, +el: List<&2, Maybe<&2, V>>, +sd: Nat, +hsd: {Nat.is_lt(1n+sd, 32n) == True{} : Bool}, +fr: Nat, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +sl: List<&2, Nat>, +hs: {ST.slok(~V, sl, fr, el) == True{} : Bool}, +hh: {ST.hasall(~V, TB.buckets(tb, kl, n), n, ll, sl) == True{} : Bool}) -> {ST.nokey(~V, ll, kl, sl, key) == True{} : Bool}:
  match sl:
    case Nil{}:
      {==}
    case Con{+s, +t}:
      +h0 = L.and_left(Bool.and(Nat.is_lt(s, fr), ST.live(~V, el, s)), ST.slok(~V, t, fr, el), hs)
      +hlt = N.lt_le_trans(s, fr, SC.pow2(sd), L.and_left(Nat.is_lt(s, fr), ST.live(~V, el, s), h0), hfr)
      +nk = anyb_nk(tb, kl, n, key, hno, ST.lw(ll, s, 2n), LK.lnk(s), n, N.le_refl(n), L.and_left(ST.anyb(TB.buckets(tb, kl, n), n, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, TB.buckets(tb, kl, n), n, ll, t), hh))
      +nk2 = L.subst(Nat, z => {Bool.not(S.str_eq(TB.keyof(ST.lw(ll, s, 2n), TB.nths(kl, z)), key)) == True{} : Bool}, UD.v(H.slot(LK.lnk(s))), s, LK.slot_lnk(one, h1, s, sd, hsd, hlt), nk)
      L.and_intro(Bool.not(S.str_eq(ST.skey(ll, kl, s), key)), ST.nokey(~V, ll, kl, t, key), nk2, nokey_of(~V, one, h1, tb, kl, n, key, hno, ll, el, sd, hsd, fr, hfr, t, L.and_right(Bool.and(Nat.is_lt(s, fr), ST.live(~V, el, s)), ST.slok(~V, t, fr, el), hs), L.and_right(ST.anyb(TB.buckets(tb, kl, n), n, LK.lnk(s), ST.lw(ll, s, 2n)), ST.hasall(~V, TB.buckets(tb, kl, n), n, ll, t), hh)))

# ---- the hit ----

def bsl_c(+bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +ll: List<&2, U32>, +q: Nat, +h: {Bool.and(ST.bslb(sl, ll, B.at(bs, q)), ST.bsl(bs, sl, ll, q)) == True{} : Bool}, +i: Nat, +c: Bool, +hc: {Nat.is_eq(i, q) == c : Bool}, rec: @hq: {Nat.is_lt(i, q) == True{} : Bool} -> {ST.bslb(sl, ll, B.at(bs, i)) == True{} : Bool}, +hi: {Nat.is_lt(i, 1n+q) == True{} : Bool}) -> {ST.bslb(sl, ll, B.at(bs, i)) == True{} : Bool}:
  match c:
    case True{}:
      L.subst(Nat, z => {ST.bslb(sl, ll, B.at(bs, z)) == True{} : Bool}, q, i, Equal.sym(Nat, i, q, N.eq_from_is_eq(i, q, hc)), L.and_left(ST.bslb(sl, ll, B.at(bs, q)), ST.bsl(bs, sl, ll, q), h))
    case False{}:
      rec(N.lt_or_eq(i, q, N.lt_succ_le(i, q, hi), hc))

def bsl_inst(+bs: List<&2, B.Bk>, +sl: List<&2, Nat>, +ll: List<&2, U32>, +m: Nat, +h: {ST.bsl(bs, sl, ll, m) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, m) == True{} : Bool}) -> {ST.bslb(sl, ll, B.at(bs, i)) == True{} : Bool}:
  match m:
    case 0n:
      Empty.absurd({ST.bslb(sl, ll, B.at(bs, i)) == True{} : Bool}, N.lt_zero_absurd(i, hi))
    case 1n+q:
      bsl_c(bs, sl, ll, q, h, i, Nat.is_eq(i, q), {==}, hq => bsl_inst(bs, sl, ll, q, L.and_right(ST.bslb(sl, ll, B.at(bs, q)), ST.bsl(bs, sl, ll, q), h), i, hq), hi)

# a full bucket holding key: its slot is listed
def hit_mem(+sl: List<&2, Nat>, +ll: List<&2, U32>, +key: String, +b: B.Bk, +hh: {B.hold(key, b) == True{} : Bool}, +hb: {ST.bslb(sl, ll, b) == True{} : Bool}) -> {NL.memn(UD.v(H.slot(B.lnk(b))), sl) == True{} : Bool}:
  match b:
    case B.BE{}:
      Empty.absurd({NL.memn(UD.v(H.slot(B.lnk(B.BE{}))), sl) == True{} : Bool}, L.false_true(hh))
    case B.BF{+w, +l, +k}:
      L.and_left(NL.memn(UD.v(H.slot(l)), sl), U32.is_eq(ST.lw(ll, UD.v(H.slot(l)), 2n), w), hb)

# ... and that slot's key is key
def hit_key(+sl: List<&2, Nat>, +ll: List<&2, U32>, +kl: List<&2, String>, +key: String, +b: B.Bk, +hh: {B.hold(key, b) == True{} : Bool}, +hb: {ST.bslb(sl, ll, b) == True{} : Bool}, +hk: {bkok(kl, b) == True{} : Bool}) -> {S.str_eq(ST.skey(ll, kl, UD.v(H.slot(B.lnk(b)))), key) == True{} : Bool}:
  match b:
    case B.BE{}:
      Empty.absurd({S.str_eq(ST.skey(ll, kl, UD.v(H.slot(B.lnk(B.BE{})))), key) == True{} : Bool}, L.false_true(hh))
    case B.BF{+w, +l, +k}:
      +ew = A.eq_of(ST.lw(ll, UD.v(H.slot(l)), 2n), w, L.and_right(NL.memn(UD.v(H.slot(l)), sl), U32.is_eq(ST.lw(ll, UD.v(H.slot(l)), 2n), w), hb))
      +ek = K.str_eq_of(k, TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), hk)
      +e = Equal.trans(String, ST.skey(ll, kl, UD.v(H.slot(l))), TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), k, Equal.cong(U32, String, z => TB.keyof(z, TB.nths(kl, UD.v(H.slot(l)))), ST.lw(ll, UD.v(H.slot(l)), 2n), w, ew), Equal.sym(String, k, TB.keyof(w, TB.nths(kl, UD.v(H.slot(l)))), ek))
      L.subst(String, z => {S.str_eq(z, key) == True{} : Bool}, k, ST.skey(ll, kl, UD.v(H.slot(l))), Equal.sym(String, ST.skey(ll, kl, UD.v(H.slot(l))), k, e), hh)

def sm_c(~V: Data, +el: List<&2, Maybe<&2, V>>, +fr: Nat, +s: Nat, +s0: Nat, +t: List<&2, Nat>, +h: {Bool.and(Bool.and(Nat.is_lt(s0, fr), ST.live(~V, el, s0)), ST.slok(~V, t, fr, el)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, s) == c : Bool}, +hm: {Bool.or(c, NL.memn(s, t)) == True{} : Bool}, rec: @hs: {ST.slok(~V, t, fr, el) == True{} : Bool} -> @hm2: {NL.memn(s, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(s, fr), ST.live(~V, el, s)) == True{} : Bool}) -> {Bool.and(Nat.is_lt(s, fr), ST.live(~V, el, s)) == True{} : Bool}:
  match c:
    case True{}:
      L.subst(Nat, z => {Bool.and(Nat.is_lt(z, fr), ST.live(~V, el, z)) == True{} : Bool}, s0, s, N.eq_from_is_eq(s0, s, hc), L.and_left(Bool.and(Nat.is_lt(s0, fr), ST.live(~V, el, s0)), ST.slok(~V, t, fr, el), h))
    case False{}:
      rec(L.and_right(Bool.and(Nat.is_lt(s0, fr), ST.live(~V, el, s0)), ST.slok(~V, t, fr, el), h), hm)

# a listed slot is below fr and live
def slok_mem(~V: Data, +el: List<&2, Maybe<&2, V>>, +fr: Nat, +s: Nat, +sl: List<&2, Nat>, +h: {ST.slok(~V, sl, fr, el) == True{} : Bool}, +hm: {NL.memn(s, sl) == True{} : Bool}) -> {Bool.and(Nat.is_lt(s, fr), ST.live(~V, el, s)) == True{} : Bool}:
  match sl:
    case Nil{}:
      Empty.absurd({Bool.and(Nat.is_lt(s, fr), ST.live(~V, el, s)) == True{} : Bool}, L.false_true(hm))
    case Con{+s0, +t}:
      sm_c(~V, el, fr, s, s0, t, h, Nat.is_eq(s0, s), {==}, hm, hs => hm2 => slok_mem(~V, el, fr, s, t, hs, hm2))