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

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

7 imports

import Base
import ../types/model.bend as T
import ./cache.bend as S
import ./operations.bend as O
import ./clock.bend as Clock
import ./effectful_operations.bend as E
import ./effectful_aggregate.bend as A

Types

type Reply source · line 12 · raw

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

Public callback-free observations. Metrics' storage-dependent Collisions field is always the documented zero/not-applicable adaptation. Diagnostics describe the abstract bound-entry count; refinement establishes the native leaf count.

NoReply
```
@-K:Data -> @-V:Data -> Reply<K, V>
```

Boolean

@-K:Data -> @-V:Data -> @value:Bool -> Reply<K, V>

Value

@-K:Data -> @-V:Data -> @value:V -> @found:Bool -> Reply<K, V>

Oldest

@-K:Data -> @-V:Data -> @key:K -> @value:V -> @found:Bool -> Reply<K, V>

KeyList

@-K:Data -> @-V:Data -> @keys:List<&2, K> -> Reply<K, V>

ValueList

@-K:Data -> @-V:Data -> @values:List<&2, V> -> Reply<K, V>

Length

@-K:Data -> @-V:Data -> @length:Nat -> Reply<K, V>

Counters

@-K:Data -> @-V:Data -> @metrics:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> Reply<K, V>

Storage

@-K:Data -> @-V:Data -> @leaves:Nat -> @recency:Nat -> @capacity:Nat -> @metrics:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> Reply<K, V>

type CmdResult source · line 23 · raw

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

Returned

@-K:Data -> @-V:Data -> @state:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @reply:Reply<K, V> -> @remaining:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> CmdResult<K, V>

Failed

@-K:Data -> @-V:Data -> @state:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @error:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.Error -> @remaining:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> CmdResult<K, V>

type Projection source · line 27 · raw

@-K:Data -> Data

Flag
```
@-K:Data -> Projection<K>
```
ValueOnly
```
@-K:Data -> Projection<K>
```
RemovedOldest
```
@-K:Data -> Projection<K>
```
CapturedOldest
```
@-K:Data -> @key:K -> Projection<K>
```
Nothing
```
@-K:Data -> Projection<K>
```
Keys
```
@-K:Data -> Projection<K>
```
Values
```
@-K:Data -> Projection<K>
```

Definitions

def value source · line 36 · raw

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

def key source · line 41 · raw

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

def metrics source · line 79 · raw

@-K:Data -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> CmdResult<K, V>

def reset source · line 83 · raw

@-K:Data -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> CmdResult<K, V>

Templates

template project source · line 46 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @zero_key:K -> @zero_value:V -> @+item:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @+present:Bool -> @kind:Projection<K> -> Reply<K, V>

template observation source · line 56 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @zero_key:K -> @zero_value:V -> @kind:Projection<K> -> @observed:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> CmdResult<K, V>

template effect source · line 60 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @zero_key:K -> @zero_value:V -> @kind:Projection<K> -> @outcome:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/effectful_operations.Outcome<K, V> -> CmdResult<K, V>

template oldest_binding source · line 65 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @zero_key:K -> @zero_value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> CmdResult<K, V>

template oldest_order source · line 70 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @order:List<&2, K> -> @zero_key:K -> @zero_value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> CmdResult<K, V>

template oldest source · line 75 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @zero_key:K -> @zero_value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> CmdResult<K, V>

template diagnostics source · line 89 · raw

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

Leaves counts the bound keys of the abstract finite map (the entries reachable through the recency list); it is independent of binding-list storage order.

template execute source · line 96 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @zero_key:K -> @zero_value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @command:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Command<K, V> -> CmdResult<K, V>

All typed commands have explicit independent semantics. Invalid transport and rejected host arguments need a separate marshalling relation; they are not silently coerced into one of these legal typed commands.