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

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

3 imports

import Base
import ./numeric.bend as N
import ../types/model.bend as T

Types

type Model source · line 10 · raw

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

Independent abstract finite-map representation. Well-formed states have one binding per key and a recency permutation of exactly those keys. No native Map, implementation, codec, or proof imports occur in this specification. Binding-list order is not observable: full refinement must compare finite-map lookup extensionally (or canonicalize bindings), while recency order is exact.

Abstract

@-K:Data -> @-V:Data -> @capacity:Nat -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @recency:List<&2, K> -> @lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @callback:Bool -> Model<K, V>

type Observation source · line 13 · raw

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

Observed

@-K:Data -> @-V:Data -> @state:Model<K, V> -> @returned:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @present:Bool -> @callbacks:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> Observation<K, V>

type Command source · line 60 · raw

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

Typed public commands. Independent observations and clock effects are defined in public_commands.bend, and finite caller traces in traces.bend.

Add

@-K:Data -> @-V:Data -> @key:K -> @value:V -> Command<K, V>

AddWithLifetime

@-K:Data -> @-V:Data -> @key:K -> @value:V -> @nanoseconds:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Command<K, V>

Get

@-K:Data -> @-V:Data -> @key:K -> Command<K, V>

GetAndRefresh

@-K:Data -> @-V:Data -> @key:K -> @nanoseconds:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Command<K, V>

Peek

@-K:Data -> @-V:Data -> @key:K -> Command<K, V>

Contains

@-K:Data -> @-V:Data -> @key:K -> Command<K, V>

Remove

@-K:Data -> @-V:Data -> @key:K -> Command<K, V>

RemoveOldest
```
@-K:Data -> @-V:Data -> Command<K, V>
```
GetOldest
```
@-K:Data -> @-V:Data -> Command<K, V>
```
Keys
```
@-K:Data -> @-V:Data -> Command<K, V>
```
Values
```
@-K:Data -> @-V:Data -> Command<K, V>
```
Purge
```
@-K:Data -> @-V:Data -> Command<K, V>
```
PurgeExpired
```
@-K:Data -> @-V:Data -> Command<K, V>
```
Len
```
@-K:Data -> @-V:Data -> Command<K, V>
```

SetLifetime

@-K:Data -> @-V:Data -> @nanoseconds:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Command<K, V>

Metrics
```
@-K:Data -> @-V:Data -> Command<K, V>
```
ResetMetrics
```
@-K:Data -> @-V:Data -> Command<K, V>
```
Diagnostics
```
@-K:Data -> @-V:Data -> Command<K, V>
```

type PrefixFailure source · line 142 · raw

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

Expiration consumes a clock sample only when the current oldest deadline is finite. A finite future deadline stops; an immortal oldest also stops without looking at any subsequent binding. This model returns removed oldest entries plus unused clock samples; transport exhaustion is an explicit failure.

PrefixFailed

@-K:Data -> @-V:Data -> @error:String -> @removed:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @retained:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @unused_clock:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> PrefixFailure<K, V>

type ExpiredPrefix source · line 145 · raw

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

Prefix

@-K:Data -> @-V:Data -> @removed:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @retained:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @unused_clock:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> ExpiredPrefix<K, V>

Definitions

def initial source · line 16 · raw

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

def length source · line 19 · raw

@-K:Data -> @-V:Data -> @s:Model<K, V> -> Nat

def set_lifetime source · line 23 · raw

@-K:Data -> @-V:Data -> @s:Model<K, V> -> @lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Model<K, V>

def reset_metrics source · line 27 · raw

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

def missing_get source · line 31 · raw

@-K:Data -> @-V:Data -> @s:Model<K, V> -> Observation<K, V>

def missing_remove source · line 35 · raw

@-K:Data -> @-V:Data -> @s:Model<K, V> -> Observation<K, V>

def is_expired source · line 39 · raw

@deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Bool

Signed comparisons, including sentinel, specified independently.

def callbacks source · line 44 · raw

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

Legacy pure event metadata. Supported initial states disable it and expose no registration command; no user function is represented or executed here.

def purged source · line 54 · raw

@-K:Data -> @-V:Data -> @s:Model<K, V> -> Model<K, V>

Full purge is defined from the ordered entries, not from implementation steps.

def choose_entry source · line 81 · raw

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

Abstract finite-map operations use user-key equality, never encoding or Map.

def omit_entry source · line 95 · raw

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

def omit_key source · line 109 · raw

@-K:Data -> @key:K -> @rest:List<&2, K> -> @equal:Bool -> List<&2, K>

def prefix_prepend source · line 148 · raw

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

def prefix_decide source · line 155 · raw

@-K:Data -> @-V:Data -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @tail:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @times:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> @expired:Bool -> @rest:Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>> -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>

def prefix_missing source · line 162 · raw

@-K:Data -> @-V:Data -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @tail:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @immortal:Bool -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>

def prefix_sampled source · line 169 · raw

@-K:Data -> @-V:Data -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @tail:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @times:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> @expired:Bool -> @rest:Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>> -> @immortal:Bool -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>

def expired_prefix source · line 176 · raw

@-K:Data -> @-V:Data -> @ordered:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @times:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>

def create_decision source · line 185 · raw

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

def construct source · line 192 · raw

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

def new_with_size source · line 203 · raw

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

Templates

template find source · line 88 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @+key:K -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

template erase source · line 102 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @+key:K -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

template unlist source · line 116 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @order:List<&2, K> -> @+key:K -> List<&2, K>

template remove_existing source · line 123 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:Model<K, V> -> @+key:K -> @+entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> Observation<K, V>

template remove_decision source · line 127 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:Model<K, V> -> @key:K -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Observation<K, V>

template remove source · line 134 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:Model<K, V> -> @+key:K -> Observation<K, V>