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

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

4 imports

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

Types

type AggregateFailure source · line 171 · raw

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

AggregateFailed

@-K:Data -> @-V:Data -> @error:String -> @state:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @unused_clock:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> AggregateFailure<K, V>

type AggregateResult source · line 174 · raw

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

Aggregate

@-K:Data -> @-V:Data -> @state:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @keys:List<&2, K> -> @values:List<&2, V> -> @callbacks:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> @unused_clock:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> AggregateResult<K, V>

Definitions

def count_miss source · line 64 · raw

@-K:Data -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @tracked:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>

def expired_result source · line 72 · raw

@-K:Data -> @-V:Data -> @result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @tracked:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

def collect source · line 142 · raw

@-K:Data -> @-V:Data -> @found: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 observed_state source · line 160 · raw

@-K:Data -> @-V:Data -> @result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>

def entry_keys source · line 177 · raw

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

def entry_values source · line 184 · raw

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

Templates

template write source · line 9 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @+key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @evicted:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

Independent finite-map transition semantics. No implementation/proof imports. Supplied 'now' is the explicit sample at the operation's clock-read point. User callbacks are excluded. Legacy event fields are inert on initial states.

template evicted_state source · line 15 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @+key:K -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>

Abstract state immediately after capacity eviction, before the new write. This factors the state already used by after_eviction below; no clock is read.

template after_eviction source · line 19 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @old:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

template evict_found source · line 24 · raw

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

template evict_first source · line 31 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @order:List<&2, K> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

template new_room source · line 38 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @order:List<&2, K> -> @full:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

template absent_add source · line 45 · raw

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

template add_found source · line 49 · raw

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

template add_with_lifetime source · line 56 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @+key:K -> @value:V -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

template add source · line 60 · raw

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

template hit_state source · line 76 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @+key:K -> @tracked:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>

template read_decide source · line 84 · raw

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

template read_found source · line 91 · raw

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

template read source · line 98 · raw

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

template refreshed source · line 102 · raw

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

template refresh_found source · line 107 · raw

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

template refresh source · line 114 · raw

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

template oldest_remove source · line 118 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @order:List<&2, K> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

template remove_oldest source · line 125 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

template oldest_read source · line 129 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @order:List<&2, K> -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

template get_oldest source · line 138 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

Internal snapshot only. public_oldest.bend supplies the complete public key/value/found observation, clock consumption and missing-input failures.

template ordered source · line 149 · raw

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

template all_entries source · line 156 · raw

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

template remove_entries source · line 164 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @entries:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>

template prefix_result source · line 193 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @enabled:Bool -> @prefix:Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.PrefixFailure<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.ExpiredPrefix<K, V>> -> Result<&2, &2, AggregateFailure<K, V>, AggregateResult<K, V>>

The aggregate exposes both projections so Keys and Values share exactly the same expiry/removal/clock semantics; consumers choose the return field.

template purge_expired source · line 200 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @times:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64> -> Result<&2, &2, AggregateFailure<K, V>, AggregateResult<K, V>>

template purge source · line 204 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> AggregateResult<K, V>