proofs/containers/lru/elfr.bend
bend-collections-laws-containers@1.0.0.0 · 54 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/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
5import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as TL
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/lists.bend as LS
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touch.bend as TO
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
12
13# Writes to a value cell off the list, and the model after a removal.
14
15
16def live_el(~V: Data, +el: List<&2, Maybe<&2, V>>, +y: Nat, +m: Maybe<&2, V>, +x: Nat, +h: {Nat.is_eq(y, x) == False{} : Bool}) -> {ST.live(~V, SC.update(Maybe<&2, V>, el, y, m), x) == ST.live(~V, el, x) : Bool}:
17 Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, SC.update(Maybe<&2, V>, el, y, m), x), HT.nthm(~V, el, x), TL.nthm_upd_other(~V, el, y, x, m, h))
18
19def slok_el(~V: Data, +el: List<&2, Maybe<&2, V>>, +y: Nat, +m: Maybe<&2, V>, +fr: Nat, +xs: List<&2, Nat>, +hy: {NL.memn(y, xs) == False{} : Bool}) -> {ST.slok(~V, xs, fr, SC.update(Maybe<&2, V>, el, y, m)) == ST.slok(~V, xs, fr, el) : Bool}:
20 match xs:
21 case Nil{}:
22 {==}
23 case Con{+x, +t}:
24 +hyx = NL.ne_sym(x, y, NL.or_ff_l(Nat.is_eq(x, y), NL.memn(y, t), hy))
25 +e1 = Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Nat.is_lt(x, fr), z), ST.slok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, m))), ST.live(~V, SC.update(Maybe<&2, V>, el, y, m), x), ST.live(~V, el, x), live_el(~V, el, y, m, x, hyx))
26 Equal.trans(Bool, ST.slok(~V, Con{x, t}, fr, SC.update(Maybe<&2, V>, el, y, m)), Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), ST.slok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, m))), ST.slok(~V, Con{x, t}, fr, el), e1, Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(~V, el, x)), z), ST.slok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, m)), ST.slok(~V, t, fr, el), slok_el(~V, el, y, m, fr, t, NL.or_ff_r(Nat.is_eq(x, y), NL.memn(y, t), hy))))
27
28def flok_el(~V: Data, +el: List<&2, Maybe<&2, V>>, +y: Nat, +m: Maybe<&2, V>, +fr: Nat, +xs: List<&2, Nat>, +hy: {NL.memn(y, xs) == False{} : Bool}) -> {ST.flok(~V, xs, fr, SC.update(Maybe<&2, V>, el, y, m)) == ST.flok(~V, xs, fr, el) : Bool}:
29 match xs:
30 case Nil{}:
31 {==}
32 case Con{+x, +t}:
33 +hyx = NL.ne_sym(x, y, NL.or_ff_l(Nat.is_eq(x, y), NL.memn(y, t), hy))
34 +e1 = Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Nat.is_lt(x, fr), Bool.not(z)), ST.flok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, m))), ST.live(~V, SC.update(Maybe<&2, V>, el, y, m), x), ST.live(~V, el, x), live_el(~V, el, y, m, x, hyx))
35 Equal.trans(Bool, ST.flok(~V, Con{x, t}, fr, SC.update(Maybe<&2, V>, el, y, m)), Bool.and(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(~V, el, x))), ST.flok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, m))), ST.flok(~V, Con{x, t}, fr, el), e1, Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(~V, el, x))), z), ST.flok(~V, t, fr, SC.update(Maybe<&2, V>, el, y, m)), ST.flok(~V, t, fr, el), flok_el(~V, el, y, m, fr, t, NL.or_ff_r(Nat.is_eq(x, y), NL.memn(y, t), hy))))
36
37def es_el(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +y: Nat, +m: Maybe<&2, V>, +xs: List<&2, Nat>, +hy: {NL.memn(y, xs) == False{} : Bool}) -> {ST.es(~V, ll, kl, SC.update(Maybe<&2, V>, el, y, m), xs) == ST.es(~V, ll, kl, el, xs) : List<&2, SP.Ent<V>>}:
38 match xs:
39 case Nil{}:
40 {==}
41 case Con{+x, +t}:
42 +hyx = NL.ne_sym(x, y, NL.or_ff_l(Nat.is_eq(x, y), NL.memn(y, t), hy))
43 +e1 = Equal.cong(Maybe<&2, V>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, x, z), ST.es(~V, ll, kl, SC.update(Maybe<&2, V>, el, y, m), t)), HT.nthm(~V, SC.update(Maybe<&2, V>, el, y, m), x), HT.nthm(~V, el, x), TL.nthm_upd_other(~V, el, y, x, m, hyx))
44 Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, ll, kl, SC.update(Maybe<&2, V>, el, y, m), Con{x, t}), SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, x, HT.nthm(~V, el, x)), ST.es(~V, ll, kl, SC.update(Maybe<&2, V>, el, y, m), t)), ST.es(~V, ll, kl, el, Con{x, t}), e1, Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, x, HT.nthm(~V, el, x)), z), ST.es(~V, ll, kl, SC.update(Maybe<&2, V>, el, y, m), t), ST.es(~V, ll, kl, el, t), es_el(~V, ll, kl, el, y, m, t, NL.or_ff_r(Nat.is_eq(x, y), NL.memn(y, t), hy))))
45
46# THEOREM (model side of a removal): dropping key's entry is the model of a ++ b
47def spec_drop(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +v: V, +hm: {HT.nthm(~V, el, s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +hnd: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})))) == True{} : Bool}) -> {SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key) == ST.es(~V, ll, kl, el, SC.append(Nat, a, b)) : List<&2, SP.Ent<V>>}:
48 +E = TO.ev(~V, ll, kl, s, v)
49 +hl = L.subst(Maybe<&2, V>, z => {HT.some_b(~V, z) == True{} : Bool}, Some{v}, HT.nthm(~V, el, s), Equal.sym(Maybe<&2, V>, HT.nthm(~V, el, s), Some{v}, hm), {==})
50 +e1 = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}), LS.es_app(~V, ll, kl, el, a, Con{s, b}), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), z), ST.es(~V, ll, kl, el, Con{s, b}), Con{E, ST.es(~V, ll, kl, el, b)}, TO.es_cons(~V, ll, kl, el, s, v, hm, b)))
51 +d1 = LS.drop_app(~V, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}, key, TO.enk_a(~V, ll, kl, el, a, s, b, hl, key, hk, hnd))
52 +d2 = L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent<V>>, z, ST.es(~V, ll, kl, el, b), Con{E, SP.drop(~V, ST.es(~V, ll, kl, el, b), key)}) == ST.es(~V, ll, kl, el, b) : List<&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), {==})
53 +d3 = Equal.trans(List<&2, SP.Ent<V>>, SP.drop(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}), key), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), SP.drop(~V, Con{E, ST.es(~V, ll, kl, el, b)}, key)), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), d1, Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), z), SP.drop(~V, Con{E, ST.es(~V, ll, kl, el, b)}, key), ST.es(~V, ll, kl, el, b), d2))
54 Equal.trans(List<&2, SP.Ent<V>>, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), Equal.trans(List<&2, SP.Ent<V>>, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SP.drop(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}), key), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SP.drop(~V, z, key), ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}), e1), d3), Equal.sym(List<&2, SP.Ent<V>>, ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), LS.es_app(~V, ll, kl, el, a, b)))