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 ../../../spec/containers/hash_table.bend as S
6	import ../../lib/u32div.bend as UD
7	import ../../../src/containers/hash_table.bend as H
8	import ./keys.bend as K
9	import ./buckets.bend as B
10	import ./state.bend as ST
11	
12	# Lookup in the abstraction: the entries of the buckets, in bucket order.
13	
14	def nohb_c(+bs: List<&2, B.Bk>, +key: String, +q: Nat, +h: {Bool.and(Bool.not(B.hold(key, B.at(bs, q))), B.nohb(bs, key, q)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(j, q) == c : Bool}, rec: @hlt: {Nat.is_lt(j, q) == True{} : Bool} -> {Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}) -> {Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}:
15	  match c:
16	    case True{}:
17	      L.subst(Nat, z => {Bool.not(B.hold(key, B.at(bs, z))) == True{} : Bool}, q, j, Equal.sym(Nat, j, q, N.eq_from_is_eq(j, q, hc)), L.and_left(Bool.not(B.hold(key, B.at(bs, q))), B.nohb(bs, key, q), h))
18	    case False{}:
19	      rec(N.lt_or_eq(j, q, N.lt_succ_le(j, q, hj), hc))
20	
21	def nohb_inst(+bs: List<&2, B.Bk>, +key: String, +m: Nat, +h: {B.nohb(bs, key, m) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, m) == True{} : Bool}) -> {Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}:
22	  match m:
23	    case 0n:
24	      Empty.absurd({Bool.not(B.hold(key, B.at(bs, j))) == True{} : Bool}, N.lt_zero_absurd(j, hj))
25	    case 1n+q:
26	      nohb_c(bs, key, q, h, j, hj, Nat.is_eq(j, q), {==}, hlt => nohb_inst(bs, key, q, L.and_right(Bool.not(B.hold(key, B.at(bs, q))), B.nohb(bs, key, q), h), j, hlt))
27	
28	# bucket b (at index i, i above x) holds key, which bucket x also holds: impossible
29	def uq_clash(+bs: List<&2, B.Bk>, +key: String, +i: Nat, +x: Nat, +hxi: {Nat.is_lt(x, i) == True{} : Bool}, +b: B.Bk, +hu: {B.uq_b(bs, i, b) == True{} : Bool}, +hb: {B.hold(key, b) == True{} : Bool}, +hx: {B.hold(key, B.at(bs, x)) == True{} : Bool}) -> Empty:
30	  match b:
31	    case B.BE{}:
32	      L.false_true(hb)
33	    case B.BF{w, +l, +k}:
34	      +nb = L.and_left(B.nohb(bs, k, i), B.nolb(bs, l, i), hu)
35	      +nx = nohb_inst(bs, k, i, nb, x, hxi)
36	      +ek = K.str_eq_of(k, key, hb)
37	      +hx2 = L.subst(String, z => {B.hold(z, B.at(bs, x)) == True{} : Bool}, key, k, Equal.sym(String, k, key, ek), hx)
38	      L.false_true(L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, B.hold(k, B.at(bs, x)), True{}, hx2, nx))
39	
40	def other_lt(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n) == True{} : Bool}, +hne: {Nat.is_eq(x, i) == False{} : Bool}, +hkx: {B.hold(key, B.at(bs, x)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(x, i) == b : Bool}) -> Empty:
41	  match b:
42	    case True{}:
43	      uq_clash(bs, key, i, x, hb, B.at(bs, i), B.all_inst(B.PUniq{bs}, n, huq, i, hi), hki, hkx)
44	    case False{}:
45	      +hix = N.lt_or_eq(i, x, N.not_lt_le(x, i, hb), N.is_eq_sym_false(x, i, hne))
46	      uq_clash(bs, key, x, i, hix, B.at(bs, x), B.all_inst(B.PUniq{bs}, n, huq, x, hx), hkx, hki)
47	
48	def other_c(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n) == True{} : Bool}, +hne: {Nat.is_eq(x, i) == False{} : Bool}, +c: Bool, +hc: {B.hold(key, B.at(bs, x)) == c : Bool}) -> {Bool.not(c) == True{} : Bool}:
49	  match c:
50	    case False{}:
51	      {==}
52	    case True{}:
53	      Empty.absurd({Bool.not(True{}) == True{} : Bool}, other_lt(bs, n, key, huq, i, hi, hki, x, hx, hne, hc, Nat.is_lt(x, i), {==}))
54	
55	# THEOREM: if bucket i holds key, no other bucket does
56	def other(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +x: Nat, +hx: {Nat.is_lt(x, n) == True{} : Bool}, +hne: {Nat.is_eq(x, i) == False{} : Bool}) -> {Bool.not(B.hold(key, B.at(bs, x))) == True{} : Bool}:
57	  L.subst(Bool, c => {Bool.not(c) == True{} : Bool}, B.hold(key, B.at(bs, x)), B.hold(key, B.at(bs, x)), {==}, other_c(bs, n, key, huq, i, hi, hki, x, hx, hne, B.hold(key, B.at(bs, x)), {==}))
58	
59	# ---- lookup over the entries of a range of buckets ----
60	
61	def lk_skip_m(~V: Data, +k: String, +key: String, +m: Maybe<&2, V>, +r: List<&2, S.Entry<V>>, +h: {S.str_eq(k, key) == False{} : Bool}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent_m(~V, k, m), r), key) == S.lookup(~V, r, key) : Maybe<&2, V>}:
62	  match m:
63	    case None{}:
64	      {==}
65	    case Some{+v}:
66	      L.subst(Bool, c => {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, r, key)) == S.lookup(~V, r, key) : Maybe<&2, V>}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, h), {==})
67	
68	# a bucket not holding key adds nothing to its lookup
69	def lk_skip(~V: Data, +b: B.Bk, +vsl: List<&2, Maybe<&2, V>>, +key: String, +r: List<&2, S.Entry<V>>, +h: {Bool.not(B.hold(key, b)) == True{} : Bool}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, b, vsl), r), key) == S.lookup(~V, r, key) : Maybe<&2, V>}:
70	  match b:
71	    case B.BE{}:
72	      {==}
73	    case B.BF{w, +l, +k}:
74	      lk_skip_m(~V, k, key, ST.nthm(~V, vsl, UD.v(H.slot(l))), r, K.not_true_eq(S.str_eq(k, key), h))
75	
76	def lk_take_m(~V: Data, +k: String, +key: String, +m: Maybe<&2, V>, +r: List<&2, S.Entry<V>>, +h: {S.str_eq(k, key) == True{} : Bool}, +hr: {S.lookup(~V, r, key) == None{} : Maybe<&2, V>}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent_m(~V, k, m), r), key) == m : Maybe<&2, V>}:
77	  match m:
78	    case None{}:
79	      hr
80	    case Some{+v}:
81	      L.subst(Bool, c => {Bool.pick(Maybe<&2, V>, c, Some{v}, S.lookup(~V, r, key)) == Some{v} : Maybe<&2, V>}, True{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), True{}, h), {==})
82	
83	# the bucket holding key decides its lookup
84	def lk_take(~V: Data, +b: B.Bk, +vsl: List<&2, Maybe<&2, V>>, +key: String, +r: List<&2, S.Entry<V>>, +h: {B.hold(key, b) == True{} : Bool}, +hr: {S.lookup(~V, r, key) == None{} : Maybe<&2, V>}) -> {S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, b, vsl), r), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(b)))) : Maybe<&2, V>}:
85	  match b:
86	    case B.BE{}:
87	      Empty.absurd({S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, B.BE{}, vsl), r), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.BE{})))) : Maybe<&2, V>}, L.false_true(h))
88	    case B.BF{w, +l, +k}:
89	      lk_take_m(~V, k, key, ST.nthm(~V, vsl, UD.v(H.slot(l))), r, h, hr)
90	
91	# no bucket in j .. j + m - 1 holds key
92	def nob(+bs: List<&2, B.Bk>, +key: String, +m: Nat, +j: Nat) -> Bool:
93	  match m:
94	    case 0n:
95	      True{}
96	    case 1n+p:
97	      Bool.and(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j))
98	
99	def lk_nob(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +m: Nat, +j: Nat, +h: {nob(bs, key, m, j) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, m, j), key) == None{} : Maybe<&2, V>}:
100	  match m:
101	    case 0n:
102	      {==}
103	    case 1n+p:
104	      Equal.trans(Maybe<&2, V>, S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, B.at(bs, j), vsl), ST.absm(~V, bs, vsl, p, 1n+j)), key), S.lookup(~V, ST.absm(~V, bs, vsl, p, 1n+j), key), None{},
105	        lk_skip(~V, B.at(bs, j), vsl, key, ST.absm(~V, bs, vsl, p, 1n+j), L.and_left(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), h)),
106	        lk_nob(~V, bs, vsl, key, p, 1n+j, L.and_right(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), h)))
107	
108	def nob_pno(+bs: List<&2, B.Bk>, +key: String, +n: Nat, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}) -> {nob(bs, key, m, j) == True{} : Bool}:
109	  match m:
110	    case 0n:
111	      {==}
112	    case 1n+p:
113	      +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
114	      +hj = N.lt_le_trans(j, 1n+Nat.add(j, p), n, N.le_lt_succ(j, Nat.add(j, p), N.le_add_right(j, p)), hjm2)
115	      L.and_intro(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), B.all_inst(B.PNo{bs, key}, n, hno, j, hj), nob_pno(bs, key, n, hno, p, 1n+j, hjm2))
116	
117	# the buckets past the one holding key do not hold it
118	def nob_past(+bs: List<&2, B.Bk>, +n: Nat, +key: String, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}, +hij: {Nat.is_lt(i, j) == True{} : Bool}) -> {nob(bs, key, m, j) == True{} : Bool}:
119	  match m:
120	    case 0n:
121	      {==}
122	    case 1n+p:
123	      +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
124	      +hj = N.lt_le_trans(j, 1n+Nat.add(j, p), n, N.le_lt_succ(j, Nat.add(j, p), N.le_add_right(j, p)), hjm2)
125	      +hne = N.is_eq_sym_false(i, j, N.is_eq_lt(i, j, hij))
126	      L.and_intro(Bool.not(B.hold(key, B.at(bs, j))), nob(bs, key, p, 1n+j), other(bs, n, key, huq, i, hi, hki, j, hj, hne), nob_past(bs, n, key, huq, i, hi, hki, p, 1n+j, hjm2, N.lt_trans(i, j, 1n+j, hij, N.lt_succ(j))))
127	
128	def lk_hit_c(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +p: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, 1n+p), n) == True{} : Bool}, +hji: {Nat.is_le(j, i) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(j, i) == c : Bool}, rec: @hji2: {Nat.is_le(1n+j, i) == True{} : Bool} -> {S.lookup(~V, ST.absm(~V, bs, vsl, p, 1n+j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, 1n+p, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}:
129	  match c:
130	    case True{}:
131	      +eji = N.eq_from_is_eq(j, i, hc)
132	      +hkj = L.subst(Nat, z => {B.hold(key, B.at(bs, z)) == True{} : Bool}, i, j, Equal.sym(Nat, j, i, eji), hki)
133	      +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
134	      +hr = lk_nob(~V, bs, vsl, key, p, 1n+j, nob_past(bs, n, key, huq, i, hi, hki, p, 1n+j, hjm2, L.subst(Nat, z => {Nat.is_lt(z, 1n+j) == True{} : Bool}, j, i, eji, N.lt_succ(j))))
135	      L.subst(Nat, z => {S.lookup(~V, ST.absm(~V, bs, vsl, 1n+p, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, z))))) : Maybe<&2, V>}, j, i, eji, lk_take(~V, B.at(bs, j), vsl, key, ST.absm(~V, bs, vsl, p, 1n+j), hkj, hr))
136	    case False{}:
137	      +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
138	      +hj = N.lt_le_trans(j, 1n+Nat.add(j, p), n, N.le_lt_succ(j, Nat.add(j, p), N.le_add_right(j, p)), hjm2)
139	      +hlt = N.lt_or_eq(j, i, hji, hc)
140	      Equal.trans(Maybe<&2, V>, S.lookup(~V, SC.append(S.Entry<V>, ST.ent(~V, B.at(bs, j), vsl), ST.absm(~V, bs, vsl, p, 1n+j)), key), S.lookup(~V, ST.absm(~V, bs, vsl, p, 1n+j), key), ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))),
141	        lk_skip(~V, B.at(bs, j), vsl, key, ST.absm(~V, bs, vsl, p, 1n+j), other(bs, n, key, huq, i, hi, hki, j, hj, hc)),
142	        rec(N.lt_succ_le_succ(j, i, hlt)))
143	
144	def lk_hit(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}, +m: Nat, +j: Nat, +hjm: {Nat.is_le(Nat.add(j, m), n) == True{} : Bool}, +hji: {Nat.is_le(j, i) == True{} : Bool}, +him: {Nat.is_lt(i, Nat.add(j, m)) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, m, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}:
145	  match m:
146	    case 0n:
147	      Empty.absurd({S.lookup(~V, ST.absm(~V, bs, vsl, 0n, j), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(j, i), False{}, Equal.sym(Bool, Nat.is_le(j, i), True{}, hji), N.lt_not_le(i, j, L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, Nat.add(j, 0n), j, N.add_zero(j), him)))))
148	    case 1n+p:
149	      +hjm2 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), hjm)
150	      lk_hit_c(~V, bs, vsl, key, n, huq, i, hi, hki, p, j, hjm, hji, Nat.is_eq(j, i), {==}, hji2 => lk_hit(~V, bs, vsl, key, n, huq, i, hi, hki, p, 1n+j, hjm2, hji2, L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), him)))
151	
152	# THEOREM: with keys unique, the lookup of the key held by bucket i is the
153	# value in i's slot; with key held nowhere, it is None.
154	def lookup_hit(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hki: {B.hold(key, B.at(bs, i)) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), key) == ST.nthm(~V, vsl, UD.v(H.slot(B.lnk(B.at(bs, i))))) : Maybe<&2, V>}:
155	  lk_hit(~V, bs, vsl, key, n, huq, i, hi, hki, n, 0n, N.le_refl(n), N.zero_le(i), hi)
156	
157	def lookup_none(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +key: String, +n: Nat, +hno: {B.all_lt(B.PNo{bs, key}, n) == True{} : Bool}) -> {S.lookup(~V, ST.absm(~V, bs, vsl, n, 0n), key) == None{} : Maybe<&2, V>}:
158	  lk_nob(~V, bs, vsl, key, n, 0n, nob_pno(bs, key, n, hno, n, 0n, N.le_refl(n)))