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

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

5 imports

import Base
import ../types/model.bend as T
import ./cache.bend as C
import ./time.bend as Time
import ./entry_ops.bend as Entry

Types

type Read source · line 61 · raw

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

Reading

@-K:Data -> @-V:Data -> @step:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V> -> @removed:Bool -> Read<K, V>

type Mode source · line 85 · raw

Data

All
```
Mode
```
Expired
```
Mode
```
KeyList
```
Mode
```
ValueList
```
Mode
```

type Aggregate source · line 93 · raw

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

Closed aggregate mode prevents invalid numeric mode values. These are internal removal and clock requests. No user code runs at removal.

Complete

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @keys:List<&2, K> -> @values:List<&2, V> -> Aggregate<K, V>

NeedClock

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @kind:Mode -> Aggregate<K, V>

RemovalReady

@-K:Data -> @-V:Data -> @step:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V> -> @remaining:Nat -> @kind:Mode -> Aggregate<K, V>

Definitions

def detach_present source · line 12 · raw

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

At this explicit removal boundary the key is absent and Len is decremented, but Removals/Evictions/Misses/Inserts have NOT yet changed.

def detach_found source · line 16 · raw

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

def detach source · line 23 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def detach_first source · line 26 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @order:List<&2, String> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def detach_oldest source · line 33 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def finish_removal source · line 37 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @evict:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>

def finish_miss source · line 41 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @tracked:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>

def prepare_room source · line 44 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @full:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def prepare_found source · line 51 · raw

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

def prepare_add source · line 58 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def expired_read source · line 64 · raw

@-K:Data -> @-V:Data -> @step:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V> -> Read<K, V>

def decide_read source · line 68 · raw

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

def read_found source · line 75 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.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>> -> Read<K, V>

def read source · line 82 · raw

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

def keys_of source · line 98 · raw

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

def values_of source · line 101 · raw

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

def complete source · line 104 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @kind:Mode -> Aggregate<K, V>

def need_clock source · line 115 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @kind:Mode -> @finite:Bool -> Aggregate<K, V>

def aggregate_next source · line 122 · raw

@-K:Data -> @-V:Data -> @remaining:Nat -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @kind:Mode -> Aggregate<K, V>

def after_removal source · line 131 · raw

@-K:Data -> @-V:Data -> @remaining:Nat -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @kind:Mode -> Aggregate<K, V>

def clock_decide source · line 134 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @kind:Mode -> @expired:Bool -> Aggregate<K, V>

def clock_entry source · line 141 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @kind:Mode -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @entry:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Aggregate<K, V>

def after_clock source · line 148 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @kind:Mode -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Aggregate<K, V>

def purge source · line 151 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> Aggregate<K, V>

def purge_expired source · line 154 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> Aggregate<K, V>

def keys source · line 157 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> Aggregate<K, V>

def values source · line 160 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> Aggregate<K, V>

def refresh_prepare_found source · line 163 · raw

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

def refresh_prepare source · line 166 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

def refresh_at source · line 169 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>

def finish_detached source · line 174 · raw

@-K:Data -> @-V:Data -> @step:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V> -> @evict:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>

Pure fold of detach and count-update phases. The callback-free host performs these internal phases without invoking user code.