~/bend-docscommunity

spec/containers/lru.bend source

spec/containers/lru.bend on the hub · documented module

import Baseimport ../../src/math/u64.bend as Wimport ./hash_table.bend as HT# Independent model of the LRU cache: a list of entries, oldest first, with a# capacity, a lifetime and five 64-bit counters. Nothing here refers to# buckets, slots, links or arrays; key equality is the association list's# (HT.str_eq), 64-bit arithmetic is src/math/u64.bend's (proved in# proofs/math/u64.bend and proofs/math/u64div.bend).## Semantics (as benchmarks/native/lru.c): add replaces a present key in place# and makes it the newest, or appends a new key after evicting the oldest# when full, counting an insertion (and an eviction); get touches and counts# a hit or a miss; peek and contains neither touch nor count; a read that# finds an expired entry removes it (a removal) and reads as a miss; remove# counts a removal; purge clears entries and counters; resize(0) fails;# resize(c) evicts the oldest until the cache fits; keys first drops the# expired oldest prefix (removals); new rejects 0 and 0xFFFFFFFF.# t = 1: timed, due at dl; t = 0: immortaltype Ent<-V: Data> is Data:  LE{key: String, val: V, t: U32, dl: W.U64}type Ctr is Data:  CT{ins: W.U64, ev: W.U64, rm: W.U64, hit: W.U64, miss: W.U64}# on != 0: entries get a lifetime of `life` millisecondstype Lru<-V: Data> is Data:  L{cap: U32, on: U32, life: W.U64, es: List<&2, Ent<V>>, +c: Ctr}type Made<-V: Data> is Data:  Made{l: Lru<V>}  Rejected{reason: String}# ---- counters ----def inc_hi(+lo: U32, +hi: U32, wrap: Bool) -> W.U64:  match wrap:    case True{}:      W.U64{lo, U32.inc(hi)}    case False{}:      W.U64{lo, hi}# x + 1, wrapping at 2^64def inc64(x: W.U64) -> W.U64:  match x:    case W.U64{+lo, +hi}:      inc_hi(U32.inc(lo), hi, U32.is_eq(U32.inc(lo), 0))def zero_ctr() -> Ctr:  CT{W.zero(), W.zero(), W.zero(), W.zero(), W.zero()}def c_ins(c: Ctr) -> Ctr:  match c:    case CT{a, b, d, e, f}:      CT{inc64(a), b, d, e, f}def c_ev(c: Ctr) -> Ctr:  match c:    case CT{a, b, d, e, f}:      CT{a, inc64(b), d, e, f}def c_rm(c: Ctr) -> Ctr:  match c:    case CT{a, b, d, e, f}:      CT{a, b, inc64(d), e, f}def c_hit(c: Ctr) -> Ctr:  match c:    case CT{a, b, d, e, f}:      CT{a, b, d, inc64(e), f}def c_miss(c: Ctr) -> Ctr:  match c:    case CT{a, b, d, e, f}:      CT{a, b, d, e, inc64(f)}def c_miss_if(c: Ctr, tracked: Bool) -> Ctr:  match tracked:    case True{}:      c_miss(c)    case False{}:      c# ---- lifetimes ----# a zero deadline never expires; otherwise deadline <= now (signed)def expired(+d: W.U64, now: W.U64) -> Bool:  Bool.pick(Bool, W.is_zero(d), False{}, W.le_signed(d, now))def gone(~V: Data, e: Ent<V>, now: W.U64) -> Bool:  match e:    case LE{k, v, +t, +d}:      Bool.pick(Bool, U32.is_eq(t, 0), False{}, expired(d, now))# the entry add stores: immortal without a lifetime, else due at now + lifedef mk_c(~V: Data, +life: W.U64, +key: String, v: V, +now: W.U64, off: Bool) -> Ent<V>:  match off:    case True{}:      LE{key, v, 0, W.zero()}    case False{}:      LE{key, v, 1, W.add(now, life)}def mk(~V: Data, +on: U32, +life: W.U64, +key: String, v: V, +now: W.U64) -> Ent<V>:  mk_c(~V, life, key, v, now, U32.is_eq(on, 0))# ---- the entry list ----def keys_of(~V: Data, es: List<&2, Ent<V>>) -> List<&2, String>:  match es:    case Nil{}:      Nil{}    case Con{LE{k, v, t, d}, r}:      Con{k, keys_of(~V, r)}def find(~V: Data, es: List<&2, Ent<V>>, +key: String) -> Maybe<&2, Ent<V>>:  match es:    case Nil{}:      None{}    case Con{+e, r}:      match e:        case LE{+k, +v, +t, +d}:          Bool.pick(Maybe<&2, Ent<V>>, HT.str_eq(k, key), Some{LE{k, v, t, d}}, find(~V, r, key))# the list without key's entrydef drop(~V: Data, es: List<&2, Ent<V>>, +key: String) -> List<&2, Ent<V>>:  match es:    case Nil{}:      Nil{}    case Con{+e, +r}:      match e:        case LE{+k, +v, +t, +d}:          Bool.pick(List<&2, Ent<V>>, HT.str_eq(k, key), r, Con{LE{k, v, t, d}, drop(~V, r, key)})def snoc(~V: Data, es: List<&2, Ent<V>>, e: Ent<V>) -> List<&2, Ent<V>>:  match es:    case Nil{}:      Con{e, Nil{}}    case Con{h, t}:      Con{h, snoc(~V, t, e)}def length(~V: Data, es: List<&2, Ent<V>>) -> Nat:  match es:    case Nil{}:      0n    case Con{h, t}:      1n+length(~V, t)def tail(~V: Data, es: List<&2, Ent<V>>) -> List<&2, Ent<V>>:  match es:    case Nil{}:      Nil{}    case Con{h, t}:      tdef val_of(~V: Data, e: Ent<V>) -> V:  match e:    case LE{k, v, t, d}:      v# ---- operations ----def new_c(~V: Data, +cap: U32, zero: Bool, reserved: Bool) -> Made<V>:  match zero reserved:    case True{} r:      Rejected{"capacity must be positive"}    case False{} True{}:      Rejected{"size must not be 0XFFFFFFFF"}    case False{} False{}:      Made{L{cap, 0, W.zero(), Nil{}, zero_ctr()}}def new(~V: Data, +cap: U32) -> Made<V>:  new_c(~V, cap, U32.is_eq(cap, 0), U32.is_eq(cap, 4294967295))def capacity(~V: Data, l: Lru<V>) -> U32:  match l:    case L{cap, on, life, es, c}:      capdef len(~V: Data, l: Lru<V>) -> U32:  match l:    case L{cap, on, life, es, c}:      U32.from_nat(length(~V, es))def counters(~V: Data, l: Lru<V>) -> Ctr:  match l:    case L{cap, on, life, es, c}:      cdef set_lifetime(~V: Data, l: Lru<V>, +ns: W.U64) -> Lru<V>:  match l:    case L{cap, on, life, es, c}:      L{cap, W.carry(Bool.not(W.is_zero(ns))), W.div_small_signed(ns, 1000000), es, c}# drop the oldest entry, counted by fdef drop_oldest(~V: Data, l: Lru<V>) -> Lru<V>:  match l:    case L{cap, on, life, es, c}:      L{cap, on, life, tail(~V, es), c}def add_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, es: List<&2, Ent<V>>, +c: Ctr, e: Ent<V>, full: Bool) -> Lru<V> & Bool:  match full:    case True{}:      (L{cap, on, life, snoc(~V, tail(~V, es), e), c_ins(c_ev(c))}, True{})    case False{}:      (L{cap, on, life, snoc(~V, es, e), c_ins(c)}, False{})def add_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, e: Ent<V>, m: Maybe<&2, Ent<V>>) -> Lru<V> & Bool:  match m:    case Some{old}:      (L{cap, on, life, snoc(~V, drop(~V, es, key), e), c_ins(c)}, False{})    case None{}:      add_absent(~V, cap, on, life, es, c, e, U32.is_le(cap, U32.from_nat(length(~V, es))))# insert or replace key; the Bool reports whether an entry was evicteddef add(~V: Data, l: Lru<V>, +key: String, v: V, +now: W.U64) -> Lru<V> & Bool:  match l:    case L{+cap, +on, +life, +es, +c}:      add_found(~V, cap, on, life, es, c, key, mk(~V, on, life, key, v, now), find(~V, es, key))def read_live(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +e: Ent<V>, tracked: Bool) -> Lru<V> & Maybe<&2, V>:  match tracked:    case True{}:      (L{cap, on, life, snoc(~V, drop(~V, es, key), e), c_hit(c)}, Some{val_of(~V, e)})    case False{}:      (L{cap, on, life, es, c}, Some{val_of(~V, e)})def read_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +tracked: Bool, m: Maybe<&2, Ent<V>>) -> Lru<V> & Maybe<&2, V>:  match m:    case None{}:      (L{cap, on, life, es, c_miss_if(c, tracked)}, None{})    case Some{+e}:      Bool.pick(Lru<V> & Maybe<&2, V>, gone(~V, e, now), (L{cap, on, life, drop(~V, es, key), c_miss_if(c_rm(c), tracked)}, None{}), read_live(~V, cap, on, life, es, c, key, e, tracked))# tracked (get): touch, count a hit or a miss; untracked (peek): neitherdef read(~V: Data, l: Lru<V>, +key: String, +now: W.U64, +tracked: Bool) -> Lru<V> & Maybe<&2, V>:  match l:    case L{+cap, +on, +life, +es, +c}:      read_found(~V, cap, on, life, es, c, key, now, tracked, find(~V, es, key))def get(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Maybe<&2, V>:  read(~V, l, key, now, True{})def peek(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Maybe<&2, V>:  read(~V, l, key, now, False{})def contains_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, m: Maybe<&2, Ent<V>>) -> Lru<V> & Bool:  match m:    case None{}:      (L{cap, on, life, es, c}, False{})    case Some{+e}:      Bool.pick(Lru<V> & Bool, gone(~V, e, now), (L{cap, on, life, drop(~V, es, key), c_rm(c)}, False{}), (L{cap, on, life, es, c}, True{}))def contains(~V: Data, l: Lru<V>, +key: String, +now: W.U64) -> Lru<V> & Bool:  match l:    case L{+cap, +on, +life, +es, +c}:      contains_found(~V, cap, on, life, es, c, key, now, find(~V, es, key))def remove_found(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, m: Maybe<&2, Ent<V>>) -> Lru<V> & Maybe<&2, V>:  match m:    case None{}:      (L{cap, on, life, es, c}, None{})    case Some{e}:      (L{cap, on, life, drop(~V, es, key), c_rm(c)}, Some{val_of(~V, e)})def remove(~V: Data, l: Lru<V>, +key: String) -> Lru<V> & Maybe<&2, V>:  match l:    case L{+cap, +on, +life, +es, +c}:      remove_found(~V, cap, on, life, es, c, key, find(~V, es, key))def purge(~V: Data, l: Lru<V>) -> Lru<V> & U32:  match l:    case L{+cap, +on, +life, +es, +c}:      (L{cap, on, life, Nil{}, zero_ctr()}, U32.from_nat(length(~V, es)))# evict the oldest until the cache fits, counting themdef shrink(~V: Data, fuel: Nat, l: Lru<V>, +ev: U32) -> Lru<V> & U32:  match fuel:    case 0n:      (l, ev)    case 1n+p:      match l:        case L{+cap, +on, +life, +es, +c}:          Bool.pick(Lru<V> & U32, U32.is_lt(cap, U32.from_nat(length(~V, es))), shrink(~V, p, L{cap, on, life, tail(~V, es), c_ev(c)}, U32.inc(ev)), (L{cap, on, life, es, c}, ev))def rs_done(~V: Data, r: Lru<V> & U32) -> Lru<V> & Result<&2, &2, String, U32>:  match r:    case Tuple{l, +ev}:      (l, Done{ev})def resize_c(~V: Data, +c0: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +cap: U32, zero: Bool) -> Lru<V> & Result<&2, &2, String, U32>:  match zero:    case True{}:      (L{c0, on, life, es, c}, Fail{"capacity must be positive"})    case False{}:      rs_done(~V, shrink(~V, length(~V, es), L{cap, on, life, es, c}, 0))# capacity 0 fails; otherwise evict the oldest until the cache fitsdef resize(~V: Data, l: Lru<V>, +cap: U32) -> Lru<V> & Result<&2, &2, String, U32>:  match l:    case L{+c0, +on, +life, +es, +c}:      resize_c(~V, c0, on, life, es, c, cap, U32.is_eq(cap, 0))# drop the expired oldest prefix, each a removaldef expire(~V: Data, fuel: Nat, l: Lru<V>, +now: W.U64) -> Lru<V>:  match fuel:    case 0n:      l    case 1n+p:      match l:        case L{+cap, +on, +life, +es, +c}:          match es:            case Nil{}:              L{cap, on, life, Nil{}, c}            case Con{+e, +r}:              Bool.pick(Lru<V>, gone(~V, e, now), expire(~V, p, L{cap, on, life, r, c_rm(c)}, now), L{cap, on, life, Con{e, r}, c})def keys_fin(~V: Data, l: Lru<V>) -> Lru<V> & List<&2, String>:  match l:    case L{+cap, +on, +life, +es, +c}:      (L{cap, on, life, es, c}, keys_of(~V, es))# the keys oldest first, after the expired oldest prefix is droppeddef keys(~V: Data, l: Lru<V>, +now: W.U64) -> Lru<V> & List<&2, String>:  match l:    case L{+cap, +on, +life, +es, +c}:      keys_fin(~V, expire(~V, length(~V, es), L{cap, on, life, es, c}, now))# ---- contract (SPARK formal containers) ----# Each `<Subprogram>.<clause>` definition below states one Post clause of# that SPARK subprogram, as a proposition on this model; the table names the# clauses. proofs/containers/lru/ proves every clause under its clause name,# and its `impl` lemma carries them to the implementation.## Contracts of the LRU cache in the style of SPARK's formal hashed maps# (SPARKlib src/spark-containers-formal-hashed_maps.ads, AdaCore/SPARKlib# master), extended with the recency order an LRU adds. They are stated on# the independent model (this file: the entries oldest first, a capacity,# counters); proof.bend's refinement theorems (new_ok, capacity_ok, len_ok,# get_ok, peek_ok, contains_ok, add_ok, remove_ok, resize_ok, purge_ok,# keys_ok) show that the implementation returns exactly the model's result,# so every clause below holds of the implementation.##   SPARK subprogram (.ads line)     ours       clauses#   Empty_Map (103)                  new        new_empty, new_rejects_zero, new_rejects_max#   Length (117)                     len        length_value#   Capacity (400)                   capacity   capacity_value#   Include (729), present key       add        add_present_order, add_present_newest, add_present_length#   Include / Insert (619), room     add        add_room_order, add_room_newest, add_room_length#   Include, full (LRU eviction)     add        add_evict_order, add_evict_newest, add_evict_length#   Element (1039) + touch           get        get_hit, get_hit_newest, get_miss#   Element (1039), no touch         peek       peek_hit, peek_miss#   Contains (1032)                  contains   contains_live, contains_absent, contains_expired#   Delete (891) / Exclude (851)     remove     remove_present, remove_absent#   Clear (427)                      purge      purge_value#   Iter_Model (1078)                keys       keys_fin_value# Expiry: an entry past its deadline reads as absent and is removed# (read_expired, contains_expired). Not in this API: "=", Is_Empty, Assign/# Copy/Move, cursors (First/Next/Has_Element/Key/Element by cursor), Find,# Replace (fails if absent), Insert that fails if present. The model's keys# are unique (every add drops the old entry first), but that invariant is# not re-exported here, so clauses are stated through find/drop rather than# as pointwise lookup frames.def last_go(~V: Data, t: List<&2, Ent<V>>, h: Ent<V>) -> Maybe<&2, Ent<V>>:  match t:    case Nil{}:      Some{h}    case Con{h2, t2}:      last_go(~V, t2, h2)def last(~V: Data, es: List<&2, Ent<V>>) -> Maybe<&2, Ent<V>>:  match es:    case Nil{}:      None{}    case Con{h, t}:      last_go(~V, t, h)def es_of(~V: Data, l: Lru<V>) -> List<&2, Ent<V>>:  match l:    case L{cap, on, life, es, c}:      es# Empty_Map (103)def Empty_Map.new_empty(~V: Data, +cap: U32, +hz: {U32.is_eq(cap, 0) == False{} : Bool}, +hm: {U32.is_eq(cap, 4294967295) == False{} : Bool}) -> Type:  {new(~V, cap) == Made{L{cap, 0, W.zero(), Nil{}, zero_ctr()}} : Made<V>}# Empty_Map (103)def Empty_Map.new_rejects_zero(~V: Data) -> Type:  {new(~V, 0) == Rejected{"capacity must be positive"} : Made<V>}# Empty_Map (103)def Empty_Map.new_rejects_max(~V: Data) -> Type:  {new(~V, 4294967295) == Rejected{"size must not be 0XFFFFFFFF"} : Made<V>}# Length (117)def Length.length_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:  {len(~V, L{cap, on, life, es, c}) == U32.from_nat(length(~V, es)) : U32}# Capacity (400)def Capacity.capacity_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:  {capacity(~V, L{cap, on, life, es, c}) == cap : U32}# Include (729), present keydef Include.add_present_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +old: Ent<V>, +hf: {find(~V, es, key) == Some{old} : Maybe<&2, Ent<V>>}) -> Type:  {add(~V, L{cap, on, life, es, c}, key, v, now) == (L{cap, on, life, snoc(~V, drop(~V, es, key), mk(~V, on, life, key, v, now)), c_ins(c)}, False{}) : Lru<V> & Bool}# Include (729), present keydef Include.add_present_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +old: Ent<V>, +hf: {find(~V, es, key) == Some{old} : Maybe<&2, Ent<V>>}) -> Type:  {last(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == Some{mk(~V, on, life, key, v, now)} : Maybe<&2, Ent<V>>}# Include (729), present keydef Include.add_present_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +old: Ent<V>, +hf: {find(~V, es, key) == Some{old} : Maybe<&2, Ent<V>>}) -> Type:  {length(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == 1n+length(~V, drop(~V, es, key)) : Nat}# Include / Insert (619), roomdef Include.add_room_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(length(~V, es))) == False{} : Bool}) -> Type:  {add(~V, L{cap, on, life, es, c}, key, v, now) == (L{cap, on, life, snoc(~V, es, mk(~V, on, life, key, v, now)), c_ins(c)}, False{}) : Lru<V> & Bool}# Include / Insert (619), roomdef Include.add_room_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(length(~V, es))) == False{} : Bool}) -> Type:  {last(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == Some{mk(~V, on, life, key, v, now)} : Maybe<&2, Ent<V>>}# Include / Insert (619), roomdef Include.add_room_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(length(~V, es))) == False{} : Bool}) -> Type:  {length(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == 1n+length(~V, es) : Nat}# Include, full (LRU eviction)def Include.add_evict_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(length(~V, es))) == True{} : Bool}) -> Type:  {add(~V, L{cap, on, life, es, c}, key, v, now) == (L{cap, on, life, snoc(~V, tail(~V, es), mk(~V, on, life, key, v, now)), c_ins(c_ev(c))}, True{}) : Lru<V> & Bool}# Include, full (LRU eviction)def Include.add_evict_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(length(~V, es))) == True{} : Bool}) -> Type:  {last(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, es, c}, key, v, now)))) == Some{mk(~V, on, life, key, v, now)} : Maybe<&2, Ent<V>>}# Include, full (LRU eviction)def Include.add_evict_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +h: Ent<V>, +t: List<&2, Ent<V>>, +c: Ctr, +key: String, +v: V, +now: W.U64, +hf: {find(~V, Con{h, t}, key) == None{} : Maybe<&2, Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(length(~V, Con{h, t}))) == True{} : Bool}) -> Type:  {length(~V, es_of(~V, Pair.fst(Lru<V>, Bool, add(~V, L{cap, on, life, Con{h, t}, c}, key, v, now)))) == length(~V, Con{h, t}) : Nat}# Element (1039) + touchdef Element.get_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:  {get(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, snoc(~V, drop(~V, es, key), e), c_hit(c)}, Some{val_of(~V, e)}) : Lru<V> & Maybe<&2, V>}# Element (1039) + touchdef Element.get_hit_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:  {last(~V, es_of(~V, Pair.fst(Lru<V>, Maybe<&2, V>, get(~V, L{cap, on, life, es, c}, key, now)))) == Some{e} : Maybe<&2, Ent<V>>}# Element (1039) + touchdef Element.get_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:  {get(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c_miss_if(c, True{})}, None{}) : Lru<V> & Maybe<&2, V>}# Iter_Model (1078)def Iter_Model.read_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +tracked: Bool, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == True{} : Bool}) -> Type:  {read(~V, L{cap, on, life, es, c}, key, now, tracked) == (L{cap, on, life, drop(~V, es, key), c_miss_if(c_rm(c), tracked)}, None{}) : Lru<V> & Maybe<&2, V>}# Element (1039), no touchdef Element.peek_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:  {peek(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c}, Some{val_of(~V, e)}) : Lru<V> & Maybe<&2, V>}# Element (1039), no touchdef Element.peek_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:  {peek(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c_miss_if(c, False{})}, None{}) : Lru<V> & Maybe<&2, V>}# Contains (1032)def Contains.contains_live(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == False{} : Bool}) -> Type:  {contains(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c}, True{}) : Lru<V> & Bool}# Contains (1032)def Contains.contains_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}, +hg: {gone(~V, e, now) == True{} : Bool}) -> Type:  {contains(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, drop(~V, es, key), c_rm(c)}, False{}) : Lru<V> & Bool}# Contains (1032)def Contains.contains_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +now: W.U64, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:  {contains(~V, L{cap, on, life, es, c}, key, now) == (L{cap, on, life, es, c}, False{}) : Lru<V> & Bool}# Delete (891) / Exclude (851)def Delete.remove_present(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +e: Ent<V>, +hf: {find(~V, es, key) == Some{e} : Maybe<&2, Ent<V>>}) -> Type:  {remove(~V, L{cap, on, life, es, c}, key) == (L{cap, on, life, drop(~V, es, key), c_rm(c)}, Some{val_of(~V, e)}) : Lru<V> & Maybe<&2, V>}# Delete (891) / Exclude (851)def Delete.remove_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr, +key: String, +hf: {find(~V, es, key) == None{} : Maybe<&2, Ent<V>>}) -> Type:  {remove(~V, L{cap, on, life, es, c}, key) == (L{cap, on, life, es, c}, None{}) : Lru<V> & Maybe<&2, V>}# Clear (427)def Clear.purge_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:  {purge(~V, L{cap, on, life, es, c}) == (L{cap, on, life, Nil{}, zero_ctr()}, U32.from_nat(length(~V, es))) : Lru<V> & U32}# Iter_Model (1078)def Iter_Model.keys_fin_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, Ent<V>>, +c: Ctr) -> Type:  {keys_fin(~V, L{cap, on, life, es, c}) == (L{cap, on, life, es, c}, keys_of(~V, es)) : Lru<V> & List<&2, String>}