proofs/lib/lemmas/src/entry_ops.bend source

proofs/lib/lemmas/src/entry_ops.bend on the hub · documented module

import Baseimport ../types/model.bend as Timport ./cache.bend as Cimport ./time.bend as Time# Shared entry operations used by the callback-free public machine.# The historical phase protocol forwards here to retain its checked proofs.# This module does not depend on that protocol or its aggregate/eviction phases.def finish_miss(-K: Data, -V: Data, c: C.Cache<K, V>, tracked: Bool) -> C.Cache<K, V>:  C.State{cap, table, order, life, counts, cb} = c  C.State{cap, table, order, life, C.hit_counts(counts, tracked, False{}), cb}def keys_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, K>:  match xs:    case Nil{}:      Nil{}    case Con{T.Item{k, v, d}, rest}:      Con{k, keys_of(K, V, rest)}def values_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, V>:  match xs:    case Nil{}:      Nil{}    case Con{T.Item{k, v, d}, rest}:      Con{v, values_of(K, V, rest)}def refresh_prepare_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:  match found:    case None{}:      C.Out{finish_miss(K, V, c, True{}), None{}, False{}, Nil{}}    case Some{entry}:      C.read_live(K, V, c, code, entry, True{})def refresh_prepare(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String) -> C.Step<K, V>:  refresh_prepare_found(K, V, c, code, C.lookup(K, V, c, code))def refresh_at(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, lifetime: T.Int64, now: T.Int64) -> C.Cache<K, V>:  C.State{cap, table, order, life, counts, cb} = c  T.Item{k, v, old} = entry  C.State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, table, code, Some{T.Item{k, v, Time.deadline(now, lifetime)}}), order, life, counts, cb}