proofs/containers/lru/find.bend
bend-collections-laws-containers@1.0.0.0 · 134 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/spec/containers/hash_table.bend as S
6import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
7import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/words.bend as WR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
13
14# The model's entries along the recency list: find, membership of keys.
15
16
17# slot s's entry as find returns it (m is its value cell)
18def fnd(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, m: Maybe<&2, V>) -> Maybe<&2, SP.Ent<V>>:
19 match m:
20 case None{}:
21 None{}
22 case Some{v}:
23 Some{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}}
24
25def or_r(+a: Bool, +b: Bool, +h: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
26 L.subst(Bool, z => {Bool.or(a, z) == True{} : Bool}, True{}, b, Equal.sym(Bool, b, True{}, h), WR.or_true(a))
27
28# ---- membership of keys ----
29
30def mk_here(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +m: Maybe<&2, V>, +hm: {HT.some_b(~V, m) == True{} : Bool}, +r: List<&2, SP.Ent<V>>) -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), r))) == True{} : Bool}:
31 match m:
32 case None{}:
33 Empty.absurd({S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, None{}), r))) == True{} : Bool}, L.false_true(hm))
34 case Some{v}:
35 L.subst(Bool, z => {Bool.or(z, S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, r))) == True{} : Bool}, True{}, S.str_eq(ST.skey(ll, kl, s), ST.skey(ll, kl, s)), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s), ST.skey(ll, kl, s)), True{}, K.str_refl(ST.skey(ll, kl, s))), {==})
36
37def mk_there(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +x: String, +s0: Nat, +m: Maybe<&2, V>, +r: List<&2, SP.Ent<V>>, +h: {S.mem(x, SP.keys_of(~V, r)) == True{} : Bool}) -> {S.mem(x, SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s0, m), r))) == True{} : Bool}:
38 match m:
39 case None{}:
40 h
41 case Some{v}:
42 L.subst(Bool, z => {Bool.or(S.str_eq(ST.skey(ll, kl, s0), x), z) == True{} : Bool}, True{}, S.mem(x, SP.keys_of(~V, r)), Equal.sym(Bool, S.mem(x, SP.keys_of(~V, r)), True{}, h), WR.or_true(S.str_eq(ST.skey(ll, kl, s0), x)))
43
44def mk_c(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +s0: Nat, +t: List<&2, Nat>, +hl: {ST.live(~V, el, s) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, s) == c : Bool}, +hm: {Bool.or(c, NL.memn(s, t)) == True{} : Bool}, rec: @h: {NL.memn(s, t) == True{} : Bool} -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool}) -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, Con{s0, t}))) == True{} : Bool}:
45 match c:
46 case True{}:
47 +e = N.eq_from_is_eq(s0, s, hc)
48 L.subst(Nat, z => {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, z, HT.nthm(~V, el, z)), ST.es(~V, ll, kl, el, t)))) == True{} : Bool}, s, s0, Equal.sym(Nat, s0, s, e), mk_here(~V, ll, kl, s, HT.nthm(~V, el, s), hl, ST.es(~V, ll, kl, el, t)))
49 case False{}:
50 mk_there(~V, ll, kl, ST.skey(ll, kl, s), s0, HT.nthm(~V, el, s0), ST.es(~V, ll, kl, el, t), rec(hm))
51
52# a live slot on the list has its key among the model's keys
53def mem_keys(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +sl: List<&2, Nat>, +hm: {NL.memn(s, sl) == True{} : Bool}) -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, sl))) == True{} : Bool}:
54 match sl:
55 case Nil{}:
56 Empty.absurd({S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, Nil{}))) == True{} : Bool}, L.false_true(hm))
57 case Con{+s0, +t}:
58 mk_c(~V, ll, kl, el, s, s0, t, hl, Nat.is_eq(s0, s), {==}, hm, h => mem_keys(~V, ll, kl, el, s, hl, t, h))
59
60# ---- find ----
61
62def not_true_f(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
63 K.not_true_eq(b, h)
64
65# an entry whose key is not key is skipped
66def find_skip(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s0: Nat, +m: Maybe<&2, V>, +r: List<&2, SP.Ent<V>>, +key: String, +hk: {Bool.or(Bool.not(HT.some_b(~V, m)), Bool.not(S.str_eq(ST.skey(ll, kl, s0), key))) == True{} : Bool}) -> {SP.find(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s0, m), r), key) == SP.find(~V, r, key) : Maybe<&2, SP.Ent<V>>}:
67 match m:
68 case None{}:
69 {==}
70 case Some{v}:
71 +ef = not_true_f(S.str_eq(ST.skey(ll, kl, s0), key), hk)
72 L.subst(Bool, z => {Bool.pick(Maybe<&2, SP.Ent<V>>, z, Some{SP.LE{ST.skey(ll, kl, s0), v, ST.lw(ll, s0, 3n), W.U64{ST.lw(ll, s0, 4n), ST.lw(ll, s0, 5n)}}}, SP.find(~V, r, key)) == SP.find(~V, r, key) : Maybe<&2, SP.Ent<V>>}, False{}, S.str_eq(ST.skey(ll, kl, s0), key), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s0), key), False{}, ef), {==})
73
74# the entry holding key is found
75def find_here(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +m: Maybe<&2, V>, +hm: {HT.some_b(~V, m) == True{} : Bool}, +r: List<&2, SP.Ent<V>>, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}) -> {SP.find(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), r), key) == fnd(~V, ll, kl, s, m) : Maybe<&2, SP.Ent<V>>}:
76 match m:
77 case None{}:
78 Empty.absurd({SP.find(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, None{}), r), key) == fnd(~V, ll, kl, s, None{}) : Maybe<&2, SP.Ent<V>>}, L.false_true(hm))
79 case Some{v}:
80 L.subst(Bool, z => {Bool.pick(Maybe<&2, SP.Ent<V>>, z, Some{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}}, SP.find(~V, r, key)) == Some{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}} : Maybe<&2, SP.Ent<V>>}, True{}, S.str_eq(ST.skey(ll, kl, s), key), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s), key), True{}, hk), {==})
81
82# the key of an earlier slot differs (keys are unique), and the rest of the
83# keys are unique
84def split_d(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +t: List<&2, Nat>, +hmt: {NL.memn(s, t) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +s0: Nat, +d: Bool, +hd: {S.str_eq(ST.skey(ll, kl, s0), key) == d : Bool}, +hn: {Bool.not(S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t)))) == True{} : Bool}) -> {Bool.not(d) == True{} : Bool}:
85 match d:
86 case False{}:
87 {==}
88 case True{}:
89 +e0 = K.str_eq_of(ST.skey(ll, kl, s0), key, hd)
90 +e1 = K.str_eq_of(ST.skey(ll, kl, s), key, hk)
91 +e = Equal.trans(String, ST.skey(ll, kl, s), key, ST.skey(ll, kl, s0), e1, Equal.sym(String, ST.skey(ll, kl, s0), key, e0))
92 +hin = L.subst(String, z => {S.mem(z, SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool}, ST.skey(ll, kl, s), ST.skey(ll, kl, s0), e, mem_keys(~V, ll, kl, el, s, hl, t, hmt))
93 Empty.absurd({Bool.not(True{}) == True{} : Bool}, L.false_true(L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t))), True{}, hin, hn)))
94
95def split_m1(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +t: List<&2, Nat>, +hmt: {NL.memn(s, t) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +s0: Nat, +m: Maybe<&2, V>, +hnd: {S.nodup(SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s0, m), ST.es(~V, ll, kl, el, t)))) == True{} : Bool}) -> {Bool.or(Bool.not(HT.some_b(~V, m)), Bool.not(S.str_eq(ST.skey(ll, kl, s0), key))) == True{} : Bool}:
96 match m:
97 case None{}:
98 {==}
99 case Some{v}:
100 +hn = L.and_left(Bool.not(S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t)))), S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))), hnd)
101 split_d(~V, ll, kl, el, s, hl, t, hmt, key, hk, s0, S.str_eq(ST.skey(ll, kl, s0), key), {==}, hn)
102
103# the keys after an entry are unique
104def nd_tail(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +t: List<&2, Nat>, +s0: Nat, +m: Maybe<&2, V>, +hnd: {S.nodup(SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s0, m), ST.es(~V, ll, kl, el, t)))) == True{} : Bool}) -> {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool}:
105 match m:
106 case None{}:
107 hnd
108 case Some{v}:
109 L.and_right(Bool.not(S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t)))), S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))), hnd)
110
111def fh_c(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +s0: Nat, +t: List<&2, Nat>, +hnd: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, Con{s0, t}))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, s) == c : Bool}, +hm: {Bool.or(c, NL.memn(s, t)) == True{} : Bool}, rec: @h: {NL.memn(s, t) == True{} : Bool} -> @hn: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool} -> {SP.find(~V, ST.es(~V, ll, kl, el, t), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent<V>>}) -> {SP.find(~V, ST.es(~V, ll, kl, el, Con{s0, t}), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent<V>>}:
112 match c:
113 case True{}:
114 +e = N.eq_from_is_eq(s0, s, hc)
115 L.subst(Nat, z => {SP.find(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, z, HT.nthm(~V, el, z)), ST.es(~V, ll, kl, el, t)), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent<V>>}, s, s0, Equal.sym(Nat, s0, s, e), find_here(~V, ll, kl, s, HT.nthm(~V, el, s), hl, ST.es(~V, ll, kl, el, t), key, hk))
116 case False{}:
117 Equal.trans(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, ll, kl, el, Con{s0, t}), key), SP.find(~V, ST.es(~V, ll, kl, el, t), key), fnd(~V, ll, kl, s, HT.nthm(~V, el, s)), find_skip(~V, ll, kl, s0, HT.nthm(~V, el, s0), ST.es(~V, ll, kl, el, t), key, split_m1(~V, ll, kl, el, s, hl, t, hm, key, hk, s0, HT.nthm(~V, el, s0), hnd)), rec(hm, nd_tail(~V, ll, kl, el, t, s0, HT.nthm(~V, el, s0), hnd)))
118
119# THEOREM (model side): a live listed slot holding key is what find returns
120def find_hit(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +sl: List<&2, Nat>, +hm: {NL.memn(s, sl) == True{} : Bool}, +hnd: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, sl))) == True{} : Bool}) -> {SP.find(~V, ST.es(~V, ll, kl, el, sl), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent<V>>}:
121 match sl:
122 case Nil{}:
123 Empty.absurd({SP.find(~V, ST.es(~V, ll, kl, el, Nil{}), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent<V>>}, L.false_true(hm))
124 case Con{+s0, +t}:
125 fh_c(~V, ll, kl, el, s, hl, key, hk, s0, t, hnd, Nat.is_eq(s0, s), {==}, hm, h => hn => find_hit(~V, ll, kl, el, s, hl, key, hk, t, h, hn))
126
127# no listed slot holds key: find returns nothing
128def find_miss(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +key: String, +sl: List<&2, Nat>, +h: {ST.nokey(~V, ll, kl, sl, key) == True{} : Bool}) -> {SP.find(~V, ST.es(~V, ll, kl, el, sl), key) == None{} : Maybe<&2, SP.Ent<V>>}:
129 match sl:
130 case Nil{}:
131 {==}
132 case Con{+s0, +t}:
133 +h0 = L.and_left(Bool.not(S.str_eq(ST.skey(ll, kl, s0), key)), ST.nokey(~V, ll, kl, t, key), h)
134 Equal.trans(Maybe<&2, SP.Ent<V>>, SP.find(~V, ST.es(~V, ll, kl, el, Con{s0, t}), key), SP.find(~V, ST.es(~V, ll, kl, el, t), key), None{}, find_skip(~V, ll, kl, s0, HT.nthm(~V, el, s0), ST.es(~V, ll, kl, el, t), key, or_r(Bool.not(HT.some_b(~V, HT.nthm(~V, el, s0))), Bool.not(S.str_eq(ST.skey(ll, kl, s0), key)), h0)), find_miss(~V, ll, kl, el, key, t, L.and_right(Bool.not(S.str_eq(ST.skey(ll, kl, s0), key)), ST.nokey(~V, ll, kl, t, key), h)))