proofs/lib/lemmas/src/cache.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as Cache

3 imports

import Base
import ../types/model.bend as T
import ./time.bend as Time

Laws

law without provedsource · line 43 · raw

@xs:List<&2, String> -> @+key:String -> List<&2, String>

Types

type Cache source · line 6 · raw

@-K:Data -> @-V:Data -> Data

The list is oldest first; it contains only encoded keys, never values.

State

@-K:Data -> @-V:Data -> @capacity:Nat -> @table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>> -> @order:List<&2, String> -> @lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @callback:Bool -> Cache<K, V>

type Step source · line 9 · raw

@-K:Data -> @-V:Data -> Data

Out

@-K:Data -> @-V:Data -> @cache:Cache<K, V> -> @item:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @flag:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> Step<K, V>

Definitions

def init source · line 12 · raw

@-K:Data -> @-V:Data -> @capacity:Nat -> Cache<K, V>

def new_checked source · line 15 · raw

@-K:Data -> @-V:Data -> @capacity:Nat -> @valid:Bool -> Result<&2, &2, String, Cache<K, V>>

def construct source · line 22 · raw

@-K:Data -> @-V:Data -> @capacity:U32 -> @size:U32 -> @zero:Bool -> @reserved:Bool -> @small:Bool -> Result<&2, &2, String, Cache<K, V>>

def new_with_size source · line 33 · raw

@-K:Data -> @-V:Data -> @+capacity:U32 -> @+size:U32 -> Result<&2, &2, String, Cache<K, V>>

def new source · line 36 · raw

@-K:Data -> @-V:Data -> @+capacity:U32 -> Result<&2, &2, String, Cache<K, V>>

def len source · line 39 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> Nat

def without_keep source · line 48 · raw

@h:String -> @tail:List<&2, String> -> @eq:Bool -> List<&2, String>

def events source · line 62 · raw

@-K:Data -> @-V:Data -> @cb:Bool -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>>

def removal_counts source · line 70 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @capacity_eviction:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics

def lookup_result source · line 78 · raw

@-K:Data -> @-V:Data -> @result:Pair(Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>) -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def lookup source · line 82 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> @code:String -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def remove_present source · line 86 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> @+key:String -> @evict:Bool -> @+entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> Step<K, V>

def remove_found source · line 90 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> @key:String -> @evict:Bool -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Step<K, V>

def remove_encoded source · line 97 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @+key:String -> @evict:Bool -> Step<K, V>

def remove source · line 100 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @+c:Cache<K, V> -> @key:K -> Step<K, V>

def oldest_remove source · line 103 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @order:List<&2, String> -> @evict:Bool -> Step<K, V>

def remove_oldest source · line 110 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @evict:Bool -> Step<K, V>

def store source · line 114 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @+code:String -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @flag:Bool -> @evs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> Step<K, V>

def store_after_evict source · line 119 · raw

@-K:Data -> @-V:Data -> @code:String -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @step:Step<K, V> -> Step<K, V>

def add_room source · line 123 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @code:String -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @full:Bool -> Step<K, V>

def capacity source · line 130 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> Nat

def add_found source · line 134 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @code:String -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Step<K, V>

def add_with_lifetime source · line 141 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @+c:Cache<K, V> -> @+key:K -> @value:V -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Step<K, V>

def add source · line 145 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @+c:Cache<K, V> -> @key:K -> @value:V -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Step<K, V>

def hit_counts source · line 149 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @+tracked:Bool -> @hit:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics

def counted source · line 159 · raw

@-K:Data -> @-V:Data -> @step:Step<K, V> -> @+tracked:Bool -> @hit:Bool -> Step<K, V>

def miss_after_remove source · line 163 · raw

@-K:Data -> @-V:Data -> @step:Step<K, V> -> @+tracked:Bool -> Step<K, V>

def touch_order source · line 167 · raw

@order:List<&2, String> -> @+code:String -> @touch:Bool -> List<&2, String>

def read_live source · line 174 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @code:String -> @+entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @+tracked:Bool -> Step<K, V>

def read_expiry source · line 178 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @code:String -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @+tracked:Bool -> @expired:Bool -> Step<K, V>

def read_found source · line 185 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @code:String -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @+tracked:Bool -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Step<K, V>

def read_encoded source · line 192 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @+code:String -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @+tracked:Bool -> Step<K, V>

def get source · line 195 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @+c:Cache<K, V> -> @key:K -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Step<K, V>

def peek source · line 198 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @+c:Cache<K, V> -> @key:K -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Step<K, V>

def refresh_present source · line 201 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> @+code:String -> @+entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> Step<K, V>

def refresh_found source · line 205 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @+code:String -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Step<K, V>

def get_and_refresh source · line 213 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @+c:Cache<K, V> -> @key:K -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Step<K, V>

def set_lifetime source · line 217 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Cache<K, V>

def metrics source · line 221 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics

def reset_metrics source · line 225 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> Pair(Cache<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics)

def oldest_read source · line 229 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @order:List<&2, String> -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Step<K, V>

def get_oldest source · line 236 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Step<K, V>

def step_cache source · line 240 · raw

@-K:Data -> @-V:Data -> @s:Step<K, V> -> Cache<K, V>

def step_events source · line 244 · raw

@-K:Data -> @-V:Data -> @s:Step<K, V> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>>

def clear_metrics source · line 248 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> Cache<K, V>

def purge_loop source · line 253 · raw

@-K:Data -> @-V:Data -> @fuel:Nat -> @c:Cache<K, V> -> Step<K, V>

No accumulated event log is stored in the cache itself.

def purge source · line 262 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> Step<K, V>

def first_entry source · line 265 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> @order:List<&2, String> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def oldest_entry source · line 272 · raw

@-K:Data -> @-V:Data -> @+c:Cache<K, V> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def finite_entry source · line 276 · raw

@-K:Data -> @-V:Data -> @e:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Bool

def purge_needs_clock source · line 284 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> Bool

One oldest inspection. Immortal or empty means stop and consumes no clock read.

def collect_entry source · line 287 · raw

@-K:Data -> @-V:Data -> @entry:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def entries_go source · line 294 · raw

@-K:Data -> @-V:Data -> @order:List<&2, String> -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def entries source · line 302 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

Raw enumeration. Public protocol Keys/Values first finish the oldest-only purge.

def map_size source · line 306 · raw

@-K:Data -> @-V:Data -> @c:Cache<K, V> -> Nat