proofs/lib/lemmas/src/cache.bend source
proofs/lib/lemmas/src/cache.bend on the hub · documented module
import Baseimport ../types/model.bend as Timport ./time.bend as Time# The list is oldest first; it contains only encoded keys, never values.type Cache<-K: Data, -V: Data> is Data: State{capacity: Nat, table: Map<&2, Maybe<&2, T.Entry<K, V>>>, order: List<&2, String>, lifetime: T.Int64, counts: T.Metrics, callback: Bool}type Step<-K: Data, -V: Data> is Data: Out{cache: Cache<K, V>, item: Maybe<&2, T.Entry<K, V>>, flag: Bool, events: List<&2, T.LruEvent<K, V>>}def init(-K: Data, -V: Data, capacity: Nat) -> Cache<K, V>: State{capacity, Map.new(&2, Maybe<&2, T.Entry<K, V>>), Nil{}, T.I64{Word.zero(64n)}, T.zero_metrics(), False{}}def new_checked(-K: Data, -V: Data, capacity: Nat, valid: Bool) -> Result<&2, &2, String, Cache<K, V>>: match valid: case False{}: Fail{"invalid capacity or size"} case True{}: Done{init(K, V, capacity)}def construct(-K: Data, -V: Data, capacity: U32, size: U32, zero: Bool, reserved: Bool, small: Bool) -> Result<&2, &2, String, Cache<K, V>>: match zero reserved small: case True{} a b: Fail{"capacity must be positive"} case False{} True{} b: Fail{"size must not be 0XFFFFFFFF"} case False{} False{} True{}: Fail{"size (" ++ U32.show(size) ++ ") is smaller than capacity (" ++ U32.show(capacity) ++ ")"} case False{} False{} False{}: Done{init(K, V, U32.to_nat(capacity))}def new_with_size(-K: Data, -V: Data, +capacity: U32, +size: U32) -> Result<&2, &2, String, Cache<K, V>>: construct(K, V, capacity, size, U32.is_eq(capacity, 0), U32.is_eq(size, 4294967295), U32.is_lt(size, capacity))def new(-K: Data, -V: Data, +capacity: U32) -> Result<&2, &2, String, Cache<K, V>>: new_with_size(K, V, capacity, capacity)def len(-K: Data, -V: Data, +c: Cache<K, V>) -> Nat: State{cap, m, order, life, counts, cb} = c List.length(&2, String, order)law without: for xs: List<&2, String> for +key: String List<&2, String>def without_keep(h: String, tail: List<&2, String>, eq: Bool) -> List<&2, String>: match eq: case True{}: tail case False{}: Con{h, tail}def without(xs, key): match xs: case Nil{}: Nil{} case Con{+h, tail}: without_keep(h, without(tail, key), String.eq(h, key))def events(-K: Data, -V: Data, cb: Bool, e: T.Entry<K, V>) -> List<&2, T.LruEvent<K, V>>: match cb: case False{}: Nil{} case True{}: T.Item{k, v, d} = e Con{T.Evicted{k, v}, Nil{}}def removal_counts(m: T.Metrics, capacity_eviction: Bool) -> T.Metrics: T.Counts{i, e, r, h, s} = m match capacity_eviction: case True{}: T.Counts{i, Word.inc(64n, e), r, h, s} case False{}: T.Counts{i, e, Word.inc(64n, r), h, s}def lookup_result(-K: Data, -V: Data, result: Map<&2, Maybe<&2, T.Entry<K, V>>> & Maybe<&2, T.Entry<K, V>>) -> Maybe<&2, T.Entry<K, V>>: (m, found) = result founddef lookup(-K: Data, -V: Data, c: Cache<K, V>, code: String) -> Maybe<&2, T.Entry<K, V>>: State{cap, m, order, life, counts, cb} = c lookup_result(K, V, Map.get(Maybe<&2, T.Entry<K, V>>, None{}, m, code))def remove_present(-K: Data, -V: Data, c: Cache<K, V>, +key: String, evict: Bool, +entry: T.Entry<K, V>) -> Step<K, V>: State{cap, m, order, life, counts, +cb} = c Out{State{cap, Map.del(&2, Maybe<&2, T.Entry<K, V>>, m, key), without(order, key), life, removal_counts(counts, evict), cb}, Some{entry}, True{}, events(K, V, cb, entry)}def remove_found(-K: Data, -V: Data, c: Cache<K, V>, key: String, evict: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>: match found: case None{}: Out{c, None{}, False{}, Nil{}} case Some{entry}: remove_present(K, V, c, key, evict, entry)def remove_encoded(-K: Data, -V: Data, +c: Cache<K, V>, +key: String, evict: Bool) -> Step<K, V>: remove_found(K, V, c, key, evict, lookup(K, V, c, key))def remove(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K) -> Step<K, V>: remove_encoded(K, V, c, encode(key), False{})def oldest_remove(-K: Data, -V: Data, +c: Cache<K, V>, order: List<&2, String>, evict: Bool) -> Step<K, V>: match order: case Nil{}: Out{c, None{}, False{}, Nil{}} case Con{k, rest}: remove_encoded(K, V, c, k, evict)def remove_oldest(-K: Data, -V: Data, +c: Cache<K, V>, evict: Bool) -> Step<K, V>: State{cap, m, order, life, counts, cb} = c oldest_remove(K, V, c, order, evict)def store(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, key: K, value: V, deadline: T.Int64, flag: Bool, evs: List<&2, T.LruEvent<K, V>>) -> Step<K, V>: State{cap, m, order, life, counts, cb} = c T.Counts{i, e, r, h, s} = counts Out{State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, m, code, Some{T.Item{key, value, deadline}}), List.append(&2, String, without(order, code), Con{code, Nil{}}), life, T.Counts{Word.inc(64n, i), e, r, h, s}, cb}, None{}, flag, evs}def store_after_evict(-K: Data, -V: Data, code: String, key: K, value: V, deadline: T.Int64, step: Step<K, V>) -> Step<K, V>: Out{c, item, flag, evs} = step store(K, V, c, code, key, value, deadline, flag, evs)def add_room(-K: Data, -V: Data, +c: Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, full: Bool) -> Step<K, V>: match full: case False{}: store(K, V, c, code, key, value, deadline, False{}, Nil{}) case True{}: store_after_evict(K, V, code, key, value, deadline, remove_oldest(K, V, c, True{}))def capacity(-K: Data, -V: Data, c: Cache<K, V>) -> Nat: State{cap, m, order, life, counts, cb} = c capdef add_found(-K: Data, -V: Data, +c: Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>: match found: case None{}: add_room(K, V, c, code, key, value, deadline, Nat.is_ge(len(K, V, c), capacity(K, V, c))) case Some{T.Item{original, old, expiry}}: store(K, V, c, code, original, value, deadline, False{}, Nil{})def add_with_lifetime(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, +key: K, value: V, ns: T.Int64, now: T.Int64) -> Step<K, V>: +code = encode(key) add_found(K, V, c, code, key, value, Time.deadline(now, ns), lookup(K, V, c, code))def add(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, value: V, now: T.Int64) -> Step<K, V>: State{cap, m, order, life, counts, cb} = c add_with_lifetime(K, V, encode, c, key, value, life, now)def hit_counts(m: T.Metrics, +tracked: Bool, hit: Bool) -> T.Metrics: T.Counts{i, e, r, h, s} = m match tracked hit: case False{} unused: T.Counts{i, e, r, h, s} case True{} True{}: T.Counts{i, e, r, Word.inc(64n, h), s} case True{} False{}: T.Counts{i, e, r, h, Word.inc(64n, s)}def counted(-K: Data, -V: Data, step: Step<K, V>, +tracked: Bool, hit: Bool) -> Step<K, V>: Out{State{cap, m, order, life, counts, cb}, item, flag, evs} = step Out{State{cap, m, order, life, hit_counts(counts, tracked, hit), cb}, item, flag, evs}def miss_after_remove(-K: Data, -V: Data, step: Step<K, V>, +tracked: Bool) -> Step<K, V>: Out{c, item, flag, evs} = step counted(K, V, Out{c, item, False{}, evs}, tracked, False{})def touch_order(order: List<&2, String>, +code: String, touch: Bool) -> List<&2, String>: match touch: case False{}: order case True{}: List.append(&2, String, without(order, code), Con{code, Nil{}})def read_live(-K: Data, -V: Data, +c: Cache<K, V>, code: String, +entry: T.Entry<K, V>, +tracked: Bool) -> Step<K, V>: State{cap, m, order, life, counts, cb} = c Out{State{cap, m, touch_order(order, code, tracked), life, hit_counts(counts, tracked, True{}), cb}, Some{entry}, True{}, Nil{}}def read_expiry(-K: Data, -V: Data, +c: Cache<K, V>, code: String, entry: T.Entry<K, V>, +tracked: Bool, expired: Bool) -> Step<K, V>: match expired: case False{}: read_live(K, V, c, code, entry, tracked) case True{}: miss_after_remove(K, V, remove_encoded(K, V, c, code, False{}), tracked)def read_found(-K: Data, -V: Data, +c: Cache<K, V>, code: String, now: T.Int64, +tracked: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>: match found: case None{}: counted(K, V, Out{c, None{}, False{}, Nil{}}, tracked, False{}) case Some{T.Item{k, v, +d}}: read_expiry(K, V, c, code, T.Item{k, v, d}, tracked, Time.expired(d, now))def read_encoded(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, now: T.Int64, +tracked: Bool) -> Step<K, V>: read_found(K, V, c, code, now, tracked, lookup(K, V, c, code))def get(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, now: T.Int64) -> Step<K, V>: read_encoded(K, V, c, encode(key), now, True{})def peek(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, now: T.Int64) -> Step<K, V>: read_encoded(K, V, c, encode(key), now, False{})def refresh_present(-K: Data, -V: Data, c: Cache<K, V>, +code: String, +entry: T.Entry<K, V>) -> Step<K, V>: State{cap, m, order, life, counts, cb} = c read_live(K, V, State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, m, code, Some{entry}), order, life, counts, cb}, code, entry, True{})def refresh_found(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>: match found: case None{}: counted(K, V, Out{c, None{}, False{}, Nil{}}, True{}, False{}) case Some{T.Item{k, v, old}}: +entry = {T.Item{k, v, deadline} : T.Entry<K, V>} refresh_present(K, V, c, code, entry)def get_and_refresh(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, ns: T.Int64, now: T.Int64) -> Step<K, V>: +code = encode(key) refresh_found(K, V, c, code, Time.deadline(now, ns), lookup(K, V, c, code))def set_lifetime(-K: Data, -V: Data, +c: Cache<K, V>, ns: T.Int64) -> Cache<K, V>: State{cap, m, order, life, counts, cb} = c State{cap, m, order, ns, counts, cb}def metrics(-K: Data, -V: Data, +c: Cache<K, V>) -> T.Metrics: State{cap, m, order, life, counts, cb} = c countsdef reset_metrics(-K: Data, -V: Data, +c: Cache<K, V>) -> Cache<K, V> & T.Metrics: State{cap, m, order, life, counts, cb} = c (State{cap, m, order, life, T.zero_metrics(), cb}, counts)def oldest_read(-K: Data, -V: Data, +c: Cache<K, V>, order: List<&2, String>, now: T.Int64) -> Step<K, V>: match order: case Nil{}: Out{c, None{}, False{}, Nil{}} case Con{k, rest}: read_encoded(K, V, c, k, now, False{})def get_oldest(-K: Data, -V: Data, +c: Cache<K, V>, now: T.Int64) -> Step<K, V>: State{cap, m, order, life, counts, cb} = c oldest_read(K, V, c, order, now)def step_cache(-K: Data, -V: Data, s: Step<K, V>) -> Cache<K, V>: Out{c, item, flag, evs} = s cdef step_events(-K: Data, -V: Data, s: Step<K, V>) -> List<&2, T.LruEvent<K, V>>: Out{c, item, flag, evs} = s evsdef clear_metrics(-K: Data, -V: Data, c: Cache<K, V>) -> Cache<K, V>: State{cap, m, order, life, counts, cb} = c State{cap, m, order, life, T.zero_metrics(), cb}# No accumulated event log is stored in the cache itself.def purge_loop(-K: Data, -V: Data, fuel: Nat, c: Cache<K, V>) -> Step<K, V>: match fuel: case 0n: Out{clear_metrics(K, V, c), None{}, False{}, Nil{}} case 1n+p: +step = remove_oldest(K, V, c, False{}) +rest = purge_loop(K, V, p, step_cache(K, V, step)) Out{step_cache(K, V, rest), None{}, False{}, List.append(&2, T.LruEvent<K, V>, step_events(K, V, step), step_events(K, V, rest))}def purge(-K: Data, -V: Data, +c: Cache<K, V>) -> Step<K, V>: purge_loop(K, V, len(K, V, c), c)def first_entry(-K: Data, -V: Data, c: Cache<K, V>, order: List<&2, String>) -> Maybe<&2, T.Entry<K, V>>: match order: case Nil{}: None{} case Con{k, rest}: lookup(K, V, c, k)def oldest_entry(-K: Data, -V: Data, +c: Cache<K, V>) -> Maybe<&2, T.Entry<K, V>>: State{cap, m, order, life, counts, cb} = c first_entry(K, V, c, order)def finite_entry(-K: Data, -V: Data, e: Maybe<&2, T.Entry<K, V>>) -> Bool: match e: case None{}: False{} case Some{T.Item{k, v, d}}: Bool.not(Time.is_zero(d))# One oldest inspection. Immortal or empty means stop and consumes no clock read.def purge_needs_clock(-K: Data, -V: Data, c: Cache<K, V>) -> Bool: finite_entry(K, V, oldest_entry(K, V, c))def collect_entry(-K: Data, -V: Data, entry: Maybe<&2, T.Entry<K, V>>, rest: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>: match entry: case None{}: rest case Some{e}: Con{e, rest}def entries_go(-K: Data, -V: Data, order: List<&2, String>, +table: Map<&2, Maybe<&2, T.Entry<K, V>>>) -> List<&2, T.Entry<K, V>>: match order: case Nil{}: Nil{} case Con{k, rest}: collect_entry(K, V, lookup_result(K, V, Map.get(Maybe<&2, T.Entry<K, V>>, None{}, table, k)), entries_go(K, V, rest, table))# Raw enumeration. Public protocol Keys/Values first finish the oldest-only purge.def entries(-K: Data, -V: Data, c: Cache<K, V>) -> List<&2, T.Entry<K, V>>: State{cap, table, order, life, counts, cb} = c entries_go(K, V, order, table)def map_size(-K: Data, -V: Data, c: Cache<K, V>) -> Nat: State{cap, m, order, life, counts, cb} = c Map.size(&2, Maybe<&2, T.Entry<K, V>>, m)