1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/u32alg.bend as A
5	import ../../../spec/containers/hash_table.bend as S
6	import ../../lib/u32div.bend as UD
7	import ../../../src/math/hash.bend as HS
8	import ./keys.bend as K
9	import ./buckets.bend as B
10	import ./modn.bend as M
11	import ./cyc.bend as CY
12	import ../../../spec/lib/common.bend as SC
13	import ../../../src/containers/hash_table.bend as H
14	
15	# Facts derived from the table invariants for a probed key.
16	
17	def hb_bf(+sd: Nat, +mask: U32, +key: String, +x: U32, +l: U32, +k: String, +hw: {B.wb(sd, B.BF{x, l, k}) == True{} : Bool}, +e: Bool, +he: {S.str_eq(k, key) == e : Bool}) -> {B.implies(e, Nat.is_eq(UD.v(HS.bucket(x, mask)), UD.v(HS.bucket(K.kword(key), mask)))) == True{} : Bool}:
18	  match e:
19	    case False{}:
20	      {==}
21	    case True{}:
22	      +xw = Equal.trans(U32, x, K.kword(k), K.kword(key), A.eq_of(x, K.kword(k), L.and_left(U32.is_eq(x, K.kword(k)), Bool.not(U32.is_eq(l, 0)), L.and_right(Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), Bool.and(U32.is_eq(x, K.kword(k)), Bool.not(U32.is_eq(l, 0))), hw))), Equal.cong(String, U32, z => K.kword(z), k, key, K.str_eq_of(k, key, he)))
23	      L.subst(U32, z => {B.implies(True{}, Nat.is_eq(UD.v(HS.bucket(z, mask)), UD.v(HS.bucket(K.kword(key), mask)))) == True{} : Bool}, K.kword(key), x, Equal.sym(U32, x, K.kword(key), xw), N.is_eq_refl(UD.v(HS.bucket(K.kword(key), mask))))
24	
25	def hb_hold(+sd: Nat, +mask: U32, +key: String, +b: B.Bk, +hw: {B.wb(sd, b) == True{} : Bool}) -> {B.implies(B.hold(key, b), Nat.is_eq(B.hb(mask, b), UD.v(HS.bucket(K.kword(key), mask)))) == True{} : Bool}:
26	  match b:
27	    case B.BE{}:
28	      {==}
29	    case B.BF{+x, +l, +k}:
30	      hb_bf(sd, mask, key, x, l, k, hw, S.str_eq(k, key), {==})
31	
32	
33	# every bucket holding key has key's home
34	def home_all(+bs: List<&2, B.Bk>, +sd: Nat, +mask: U32, +key: String, +n: Nat, +hwell: {B.all_lt(B.PWell{bs, sd}, n) == True{} : Bool}, +m: Nat, +hm: {Nat.is_le(m, n) == True{} : Bool}) -> {B.all_lt(B.PHome{bs, mask, key, UD.v(HS.bucket(K.kword(key), mask))}, m) == True{} : Bool}:
35	  match m:
36	    case 0n:
37	      {==}
38	    case 1n+q:
39	      +hq = N.succ_le_lt(q, n, hm)
40	      L.and_intro(B.eval(B.PHome{bs, mask, key, UD.v(HS.bucket(K.kword(key), mask))}, q), B.all_lt(B.PHome{bs, mask, key, UD.v(HS.bucket(K.kword(key), mask))}, q), hb_hold(sd, mask, key, B.at(bs, q), B.all_inst(B.PWell{bs, sd}, n, hwell, q, hq)), home_all(bs, sd, mask, key, n, hwell, q, N.lt_le(q, n, hq)))
41	
42	# ---- occupancy ----
43	
44	def bitv(b: Bool) -> Nat:
45	  match b:
46	    case True{}:
47	      1n
48	    case False{}:
49	      0n
50	
51	# the number of full buckets among the first m
52	def occn(+bs: List<&2, B.Bk>, +m: Nat) -> Nat:
53	  match m:
54	    case 0n:
55	      0n
56	    case 1n+q:
57	      Nat.add(bitv(B.occ(B.at(bs, q))), occn(bs, q))
58	
59	def Empty0(+bs: List<&2, B.Bk>, +m: Nat) -> Type:
60	  Sigma<&1, &1, Nat, j => {Nat.is_lt(j, m) == True{} : Bool} & {B.at(bs, j) == B.BE{} : B.Bk}>
61	
62	def emp_up(+bs: List<&2, B.Bk>, +q: Nat, e: Empty0(bs, q)) -> Empty0(bs, 1n+q):
63	  match e:
64	    case Tuple{+j, Tuple{hj, hz}}:
65	      (j, (N.lt_trans(j, q, 1n+q, hj, N.lt_succ(q)), hz))
66	
67	def emp_c(+bs: List<&2, B.Bk>, +q: Nat, +b: B.Bk, +hb: {B.at(bs, q) == b : B.Bk}, +h: {Nat.is_lt(Nat.add(bitv(B.occ(b)), occn(bs, q)), 1n+q) == True{} : Bool}, rec: @hq: {Nat.is_lt(occn(bs, q), q) == True{} : Bool} -> Empty0(bs, q)) -> Empty0(bs, 1n+q):
68	  match b:
69	    case B.BE{}:
70	      (q, (N.lt_succ(q), hb))
71	    case B.BF{x, l, k}:
72	      emp_up(bs, q, rec(h))
73	
74	# fewer full buckets than buckets: some bucket is empty
75	def find_empty(+bs: List<&2, B.Bk>, +m: Nat, +h: {Nat.is_lt(occn(bs, m), m) == True{} : Bool}) -> Empty0(bs, m):
76	  match m:
77	    case 0n:
78	      Empty.absurd(Empty0(bs, 0n), N.lt_zero_absurd(occn(bs, 0n), h))
79	    case 1n+q:
80	      emp_c(bs, q, B.at(bs, q), {==}, h, hq => find_empty(bs, q, hq))
81	
82	# the probe theorem for a table size n > 0 started at its home h
83	def pos0(+bp: Nat, +h: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}) -> {M.pos(1n+bp, h, 0n) == h : Nat}:
84	  Equal.trans(Nat, Nat.mod(Nat.add(h, 0n), 1n+bp), Nat.mod(h, 1n+bp), h, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(h, 0n), h, N.add_zero(h)), CY.mod_small(1n+bp, h, hh))
85	
86	def pf_ok_n(+bs: List<&2, B.Bk>, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +mask: U32, +key: String, +h: Nat, +hh: {Nat.is_lt(h, n) == True{} : Bool}, +cl: {B.cluster(bs, n, mask) == True{} : Bool}, +ho: {B.all_lt(B.PHome{bs, mask, key, h}, n) == True{} : Bool}, +e0: Nat, +he0: {Nat.is_lt(e0, n) == True{} : Bool}, +hz0: {B.at(bs, e0) == B.BE{} : B.Bk}) -> B.ResOK(bs, n, h, key, B.pf(key, bs, n, n, B.mstep(key, B.at(bs, h)), h)):
87	  match n:
88	    case 0n:
89	      Empty.absurd(B.ResOK(bs, 0n, h, key, B.pf(key, bs, 0n, 0n, B.mstep(key, B.at(bs, h)), h)), L.false_true(hn))
90	    case 1n+bp:
91	      L.subst(Nat, z => B.ResOK(bs, 1n+bp, h, key, B.pf(key, bs, 1n+bp, 1n+bp, B.mstep(key, B.at(bs, z)), z)), M.pos(1n+bp, h, 0n), h, pos0(bp, h, hh), B.pf_ok(bs, bp, mask, key, h, hh, cl, ho, e0, he0, hz0, 1n+bp, 0n, hn, {==}, {==}))