~/bend-docscommunity

proofs/containers/lru/proof.bend source

proofs/containers/lru/proof.bend on the hub · documented module

import Baseimport ../../../spec/containers/lru.bend as SPimport ../../../spec/lib/common.bend as SCimport ../../lib/array.bend as ARimport ../../../src/math/u64.bend as Wimport ../../../src/containers/lru.bend as LRimport ./state.bend as STimport ./new.bend as NWimport ./basic.bend as BAimport ./rmat.bend as RMimport ./read.bend as RDimport ./contains.bend as CTimport ./add.bend as ADimport ./remove.bend as RVimport ./resize.bend as RZimport ./purge.bend as PUimport ./keys.bend as KY# LRU cache (src/containers/lru.bend): public proof entry point.#   shadow       ST.Sh: the cache's U32 fields, the table and arena exponents,#                a mirror tree for each array, and two ghost lists: the#                recency list (oldest first) and the free list;#                ST.real(sh) is the cache#   abstraction  ST.model(sh): the capacity, the lifetime words, the entries#                of the recency list in order, and the counters, as a#                proofs/spec/lru.bend cache#   invariant    ST.good(sh): the hash table's clusters, check words, unique#                keys and links, count and load; every full bucket's slot on#                the recency list with its hash word, and a bucket for every#                listed slot; the recency list linked both ways with its head#                and tail, live and without repeats, keys unique; the free#                list linked, vacant and without repeats; every slot below#                fresh on exactly one of the two lists#                (proofs/lru/state.bend, generated by#                tools/generators/lru_state.py)## Every operation is proved for every shadow satisfying the invariant, keys# of every length, every value type V (Data) and every clock value:#   new                 the specification's new (or its rejection)#   capacity/len        the specification's answer; cache and model kept#   counters            the specification's counters#   set_lifetime        the specification's set_lifetime#   get/peek            the specification's read: an expired entry is#                       removed, a live one returned (and, for get, touched#                       and counted)#   contains            the specification's contains#   add                 insert or replace; a full cache evicts its oldest#                       entry first (precondition: 2 (len + 1) <= 2^29, i.e.#                       the table stays below 2^30 buckets)#   remove              the specification's remove#   resize              the specification's resize, evicting the oldest#                       entries while over capacity#   purge               the specification's purge#   keys                the keys oldest first, after the expired oldest#                       prefix is removed# and each result shadow satisfies the invariant again.def new_ok(~V: Data, +cap: U32) -> NW.MadeOK(~V, LR.new(&2, V, cap), SP.new(~V, cap)):  NW.new_ok(~V, cap)def capacity_ok(~V: Data, +sh: ST.Sh<V>) -> {LR.capacity(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), SP.capacity(~V, ST.model(~V, sh))) : LR.LRU<&2, V> & U32}:  BA.capacity_ok(~V, sh)def len_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> {LR.len(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), SP.len(~V, ST.model(~V, sh))) : LR.LRU<&2, V> & U32}:  BA.len_ok(~V, sh, hg)def counters_ok(~V: Data, +sh: ST.Sh<V>) -> {LR.counters(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), AR.thaw(U32, BA.mtree(~V, sh))) : LR.LRU<&2, V> & Array<U32>} & {ST.ctr(AR.slots(U32, BA.mtree(~V, sh))) == SP.counters(~V, ST.model(~V, sh)) : SP.Ctr}:  BA.counters_ok(~V, sh)def set_lifetime_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +ns: W.U64) -> BA.SetOK(~V, sh, SP.set_lifetime(~V, ST.model(~V, sh), ns), LR.set_lifetime_packed(&2, V, ST.real(~V, sh), ns)):  BA.set_lifetime_ok(~V, sh, hg, ns)def get_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, +now: W.U64) -> RM.POK(~V, Maybe<&2, V>, SP.get(~V, ST.model(~V, sh), key, now), LR.get(V, ST.real(~V, sh), key, now)):  RD.read_ok(~V, 1n, {==}, sh, hg, key, now, True{})def peek_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, +now: W.U64) -> RM.POK(~V, Maybe<&2, V>, SP.peek(~V, ST.model(~V, sh), key, now), LR.peek(V, ST.real(~V, sh), key, now)):  RD.read_ok(~V, 1n, {==}, sh, hg, key, now, False{})def contains_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, +now: W.U64) -> RM.POK(~V, Bool, SP.contains(~V, ST.model(~V, sh), key, now), LR.contains(&2, V, ST.real(~V, sh), key, now)):  CT.contains_ok(~V, 1n, {==}, sh, hg, key, now)def add_ok(~V: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+SP.length(~V, ST.lru_es(~V, ST.model(~V, sh)))), SC.pow2(cz)) == True{} : Bool}, +key: String, +v: V, +now: W.U64) -> RM.POK(~V, Bool, SP.add(~V, ST.model(~V, sh), key, v, now), LR.add(&2, V, ST.real(~V, sh), key, v, now)):  AD.add_spec_ok(~V, 1n, {==}, cz, hcz, sh, hg, hcap, key, v, now)def remove_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, sh), key), LR.remove(&2, V, ST.real(~V, sh), key)):  RV.remove_ok(~V, 1n, {==}, sh, hg, key)def resize_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cap2: U32) -> RM.POK(~V, Result<&2, &2, String, U32>, SP.resize(~V, ST.model(~V, sh), cap2), LR.resize(&2, V, ST.real(~V, sh), cap2)):  RZ.resize_ok(~V, 1n, {==}, sh, hg, cap2)def purge_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> RM.POK(~V, U32, SP.purge(~V, ST.model(~V, sh)), LR.purge(&2, V, ST.real(~V, sh))):  PU.purge_ok(~V, 1n, {==}, sh, hg)def keys_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +now: W.U64) -> RM.POK(~V, List<&2, String>, SP.keys(~V, ST.model(~V, sh), now), LR.keys(&2, V, ST.real(~V, sh), now)):  KY.keys_ok(~V, 1n, {==}, now, sh, hg)# ==== the contract of lru (stated in spec/containers/lru.bend) ====================# ---- list facts ----def lg_snoc(~V: Data, +t: List<&2, SP.Ent<V>>, +h: SP.Ent<V>, +e: SP.Ent<V>) -> {SP.last_go(~V, SP.snoc(~V, t, e), h) == Some{e} : Maybe<&2, SP.Ent<V>>}:  match t:    case Nil{}:      {==}    case Con{+h2, +t2}:      lg_snoc(~V, t2, h2, e)# the appended entry is the newest (the SP.last of the recency order)def snoc_last(~V: Data, +es: List<&2, SP.Ent<V>>, +e: SP.Ent<V>) -> {SP.last(~V, SP.snoc(~V, es, e)) == Some{e} : Maybe<&2, SP.Ent<V>>}:  match es:    case Nil{}:      {==}    case Con{+h, +t}:      lg_snoc(~V, t, h, e)def snoc_length(~V: Data, +es: List<&2, SP.Ent<V>>, +e: SP.Ent<V>) -> {SP.length(~V, SP.snoc(~V, es, e)) == 1n+SP.length(~V, es) : Nat}:  match es:    case Nil{}:      {==}    case Con{+h, +t}:      Equal.cong(Nat, Nat, x => 1n+x, SP.length(~V, SP.snoc(~V, t, e)), 1n+SP.length(~V, t), snoc_length(~V, t, e))# ---- Empty_Map, Length, Capacity ----def new_empty(~V: Data, +cap: U32, +hz: {U32.is_eq(cap, 0) == False{} : Bool}, +hm: {U32.is_eq(cap, 4294967295) == False{} : Bool}) -> SP.Empty_Map.new_empty(~V, cap, hz, hm):  %Equal.sym(Bool, U32.is_eq(cap, 0), False{}, hz) : {SP.new_c(~V, cap, _, U32.is_eq(cap, 4294967295)) == SP.Made{SP.L{cap, 0, W.zero(), Nil{}, SP.zero_ctr()}} : SP.Made<V>}  %Equal.sym(Bool, U32.is_eq(cap, 4294967295), False{}, hm) : {SP.new_c(~V, cap, False{}, _) == SP.Made{SP.L{cap, 0, W.zero(), Nil{}, SP.zero_ctr()}} : SP.Made<V>}  {==}def new_rejects_zero(~V: Data) -> SP.Empty_Map.new_rejects_zero(~V):  {==}def new_rejects_max(~V: Data) -> SP.Empty_Map.new_rejects_max(~V):  {==}def length_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Length.length_value(~V, cap, on, life, es, c):  {==}def capacity_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Capacity.capacity_value(~V, cap, on, life, es, c):  {==}# ---- Include (add) ----# a present key: its old entry is dropped and the new one is the newestdef add_present_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +old: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{old} : Maybe<&2, SP.Ent<V>>}) -> SP.Include.add_present_order(~V, cap, on, life, es, c, key, v, now, old, hf):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{old}, hf) : {SP.add_found(~V, cap, on, life, es, c, key, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}) : SP.Lru<V> & Bool}  {==}def add_present_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +old: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{old} : Maybe<&2, SP.Ent<V>>}) -> SP.Include.add_present_newest(~V, cap, on, life, es, c, key, v, now, old, hf):  %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_present_order(~V, cap, on, life, es, c, key, v, now, old, hf)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == Some{SP.mk(~V, on, life, key, v, now)} : Maybe<&2, SP.Ent<V>>}  snoc_last(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now))def add_present_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +old: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{old} : Maybe<&2, SP.Ent<V>>}) -> SP.Include.add_present_length(~V, cap, on, life, es, c, key, v, now, old, hf):  %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_present_order(~V, cap, on, life, es, c, key, v, now, old, hf)) : {SP.length(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == 1n+SP.length(~V, SP.drop(~V, es, key)) : Nat}  snoc_length(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now))# an absent key with room: appended as the newest, nothing evicteddef add_room_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == False{} : Bool}) -> SP.Include.add_room_order(~V, cap, on, life, es, c, key, v, now, hf, hr):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.add_found(~V, cap, on, life, es, c, key, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}) : SP.Lru<V> & Bool}  %Equal.sym(Bool, U32.is_le(cap, U32.from_nat(SP.length(~V, es))), False{}, hr) : {SP.add_absent(~V, cap, on, life, es, c, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}) : SP.Lru<V> & Bool}  {==}def add_room_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == False{} : Bool}) -> SP.Include.add_room_newest(~V, cap, on, life, es, c, key, v, now, hf, hr):  %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_room_order(~V, cap, on, life, es, c, key, v, now, hf, hr)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == Some{SP.mk(~V, on, life, key, v, now)} : Maybe<&2, SP.Ent<V>>}  snoc_last(~V, es, SP.mk(~V, on, life, key, v, now))def add_room_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == False{} : Bool}) -> SP.Include.add_room_length(~V, cap, on, life, es, c, key, v, now, hf, hr):  %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_room_order(~V, cap, on, life, es, c, key, v, now, hf, hr)) : {SP.length(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == 1n+SP.length(~V, es) : Nat}  snoc_length(~V, es, SP.mk(~V, on, life, key, v, now))# an absent key when full: the oldest is evicted (reported), the new one is newestdef add_evict_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == True{} : Bool}) -> SP.Include.add_evict_order(~V, cap, on, life, es, c, key, v, now, hf, hfu):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.add_found(~V, cap, on, life, es, c, key, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}) : SP.Lru<V> & Bool}  %Equal.sym(Bool, U32.is_le(cap, U32.from_nat(SP.length(~V, es))), True{}, hfu) : {SP.add_absent(~V, cap, on, life, es, c, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}) : SP.Lru<V> & Bool}  {==}def add_evict_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == True{} : Bool}) -> SP.Include.add_evict_newest(~V, cap, on, life, es, c, key, v, now, hf, hfu):  %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}), add_evict_order(~V, cap, on, life, es, c, key, v, now, hf, hfu)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == Some{SP.mk(~V, on, life, key, v, now)} : Maybe<&2, SP.Ent<V>>}  snoc_last(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now))# eviction keeps the length (the cache holds at least the evicted entry)def add_evict_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +h: SP.Ent<V>, +t: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, Con{h, t}, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(SP.length(~V, Con{h, t}))) == True{} : Bool}) -> SP.Include.add_evict_length(~V, cap, on, life, h, t, c, key, v, now, hf, hfu):  %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, Con{h, t}, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, t, SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}), add_evict_order(~V, cap, on, life, Con{h, t}, c, key, v, now, hf, hfu)) : {SP.length(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == SP.length(~V, Con{h, t}) : Nat}  snoc_length(~V, t, SP.mk(~V, on, life, key, v, now))# ---- Element: get (touches) and peek (does not) ----# a live hit returns the value and makes the key the newestdef get_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Element.get_hit(~V, cap, on, life, es, c, key, now, e, hf, hg):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, True{}, _) == (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), e), SP.c_hit(c)}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}  %Equal.sym(Bool, SP.gone(~V, e, now), False{}, hg) : {Bool.pick(SP.Lru<V> & Maybe<&2, V>, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), True{})}, None{}), SP.read_live(~V, cap, on, life, es, c, key, e, True{})) == (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), e), SP.c_hit(c)}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}  {==}def get_hit_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Element.get_hit_newest(~V, cap, on, life, es, c, key, now, e, hf, hg):  %Equal.sym(SP.Lru<V> & Maybe<&2, V>, SP.get(~V, SP.L{cap, on, life, es, c}, key, now), (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), e), SP.c_hit(c)}, Some{SP.val_of(~V, e)}), get_hit(~V, cap, on, life, es, c, key, now, e, hf, hg)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Maybe<&2, V>, _))) == Some{e} : Maybe<&2, SP.Ent<V>>}  snoc_last(~V, SP.drop(~V, es, key), e)# a miss leaves the entries unchanged and reads as absentdef get_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Element.get_miss(~V, cap, on, life, es, c, key, now, hf):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, True{}, _) == (SP.L{cap, on, life, es, SP.c_miss_if(c, True{})}, None{}) : SP.Lru<V> & Maybe<&2, V>}  {==}# an expired entry reads as absent and is removeddef read_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +tracked: Bool, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == True{} : Bool}) -> SP.Iter_Model.read_expired(~V, cap, on, life, es, c, key, now, tracked, e, hf, hg):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, tracked, _) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), tracked)}, None{}) : SP.Lru<V> & Maybe<&2, V>}  %Equal.sym(Bool, SP.gone(~V, e, now), True{}, hg) : {Bool.pick(SP.Lru<V> & Maybe<&2, V>, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), tracked)}, None{}), SP.read_live(~V, cap, on, life, es, c, key, e, tracked)) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), tracked)}, None{}) : SP.Lru<V> & Maybe<&2, V>}  {==}# peek: a live hit returns the value and changes nothingdef peek_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Element.peek_hit(~V, cap, on, life, es, c, key, now, e, hf, hg):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, False{}, _) == (SP.L{cap, on, life, es, c}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}  %Equal.sym(Bool, SP.gone(~V, e, now), False{}, hg) : {Bool.pick(SP.Lru<V> & Maybe<&2, V>, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), False{})}, None{}), SP.read_live(~V, cap, on, life, es, c, key, e, False{})) == (SP.L{cap, on, life, es, c}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}  {==}def peek_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Element.peek_miss(~V, cap, on, life, es, c, key, now, hf):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, False{}, _) == (SP.L{cap, on, life, es, SP.c_miss_if(c, False{})}, None{}) : SP.Lru<V> & Maybe<&2, V>}  {==}# ---- Contains ----def contains_live(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Contains.contains_live(~V, cap, on, life, es, c, key, now, e, hf, hg):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.contains_found(~V, cap, on, life, es, c, key, now, _) == (SP.L{cap, on, life, es, c}, True{}) : SP.Lru<V> & Bool}  %Equal.sym(Bool, SP.gone(~V, e, now), False{}, hg) : {Bool.pick(SP.Lru<V> & Bool, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}), (SP.L{cap, on, life, es, c}, True{})) == (SP.L{cap, on, life, es, c}, True{}) : SP.Lru<V> & Bool}  {==}def contains_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == True{} : Bool}) -> SP.Contains.contains_expired(~V, cap, on, life, es, c, key, now, e, hf, hg):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.contains_found(~V, cap, on, life, es, c, key, now, _) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}) : SP.Lru<V> & Bool}  %Equal.sym(Bool, SP.gone(~V, e, now), True{}, hg) : {Bool.pick(SP.Lru<V> & Bool, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}), (SP.L{cap, on, life, es, c}, True{})) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}) : SP.Lru<V> & Bool}  {==}def contains_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Contains.contains_absent(~V, cap, on, life, es, c, key, now, hf):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.contains_found(~V, cap, on, life, es, c, key, now, _) == (SP.L{cap, on, life, es, c}, False{}) : SP.Lru<V> & Bool}  {==}# ---- Delete / Exclude (remove), Clear (purge), Iter_Model (keys) ----def remove_present(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}) -> SP.Delete.remove_present(~V, cap, on, life, es, c, key, e, hf):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.remove_found(~V, cap, on, life, es, c, key, _) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}  {==}def remove_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Delete.remove_absent(~V, cap, on, life, es, c, key, hf):  %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.remove_found(~V, cap, on, life, es, c, key, _) == (SP.L{cap, on, life, es, c}, None{}) : SP.Lru<V> & Maybe<&2, V>}  {==}def purge_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Clear.purge_value(~V, cap, on, life, es, c):  {==}def keys_fin_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Iter_Model.keys_fin_value(~V, cap, on, life, es, c):  {==}