1 import Base 2 import ../../lib/logic.bend as L 3 import ../../../spec/lib/common.bend as SC 4 import ../../../spec/containers/hash_table.bend as S 5 import ../../../spec/containers/lru.bend as SP 6 import ../hash_table/state.bend as HT 7 import ../hash_table/tools.bend as TL 8 import ./state.bend as ST 9 import ./lists.bend as LS 10 import ./touch.bend as TO 11 import ../../lib/nat_list.bend as NL 12 13 # Writes to a value cell off the list, and the model after a removal. 14 15 16 def 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 19 def 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 28 def 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 37 def 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>}: 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>, z => SC.append(SP.Ent, 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>, ST.es(~V, ll, kl, SC.update(Maybe<&2, V>, el, y, m), Con{x, t}), SC.append(SP.Ent, 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>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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 47 def 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>}: 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>, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b})), SC.append(SP.Ent, 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>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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>, 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>}, 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>, SP.drop(~V, SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}), key), SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), SP.drop(~V, Con{E, ST.es(~V, ll, kl, el, b)}, key)), SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), d1, Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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>, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SC.append(SP.Ent, 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>, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SP.drop(~V, SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}), key), SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, z => SP.drop(~V, z, key), ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), Con{E, ST.es(~V, ll, kl, el, b)}), e1), d3), Equal.sym(List<&2, SP.Ent>, ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), LS.es_app(~V, ll, kl, el, a, b)))