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

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

5 imports

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

Types

type Request source · line 11 · raw

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

Callback-free public dispatcher. Through src/host.bend the adapter starts one Request and answers every Waiting progress with exactly one provider event: a validated sample resumes; a failed provider adopts abandon(pending). No user code runs here and no event list is ever produced for the host.

Add

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

AddWithLifetime

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

Get

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

GetAndRefresh

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

Peek

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

Contains

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

Remove

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

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

SetLifetime

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

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

type Answer source · line 31 · raw

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

Empty
```
@-K:Data -> @-V:Data -> Answer<K, V>
```

Boolean

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

Value

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

Oldest

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

KeyList

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

ValueList

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

Length

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

Counters

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

Storage

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

type Shape source · line 42 · raw

@-K:Data -> Data

Flag
```
@-K:Data -> Shape<K>
```
ValueOnly
```
@-K:Data -> Shape<K>
```
Captured
```
@-K:Data -> @key:K -> Shape<K>
```
Nothing
```
@-K:Data -> Shape<K>
```
AllKeys
```
@-K:Data -> Shape<K>
```
AllValues
```
@-K:Data -> Shape<K>
```

type Pending source · line 50 · raw

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

AddWait

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @key:K -> @value:V -> @nanoseconds:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @evicted:Bool -> Pending<K, V>

ReadWait

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @tracked:Bool -> @shape:Shape<K> -> Pending<K, V>

RefreshWait

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

ExpireWait

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @shape:Shape<K> -> Pending<K, V>

type Progress source · line 56 · raw

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

Finished

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @answer:Answer<K, V> -> Progress<K, V>

Waiting

@-K:Data -> @-V:Data -> @pending:Pending<K, V> -> Progress<K, V>

Definitions

def zero_time source · line 60 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64

def item_value source · line 63 · raw

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

def item_key source · line 68 · raw

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

def shaped source · line 73 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+item:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @+present:Bool -> @shape:Shape<K> -> Answer<K, V>

def finish_step source · line 82 · raw

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

def prepare_room source · line 87 · 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>

Add: room is made (and the eviction counted) before the clock is requested.

def prepare_found source · line 92 · 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 97 · 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 retained_key source · line 101 · raw

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

A present key keeps its stored original key; an absent key is inserted as given.

def finish_add source · line 108 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @evicted:Bool -> Progress<K, V>

After the optional clock sample the prepared cache has room (or holds the key), so the insertion is one store; its flag is the pre-clock eviction result.

def add_lifetime source · line 111 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @key:K -> @value:V -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @evicted:Bool -> @immortal:Bool -> Progress<K, V>

def add_prepared source · line 116 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @step:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V> -> @code:String -> @key:K -> @value:V -> @+ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Progress<K, V>

def add_found source · line 120 · raw

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

def add_with_lifetime source · line 123 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> @key:K -> @value:V -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Progress<K, V>

def add source · line 126 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @key:K -> @value:V -> Progress<K, V>

def finish_read source · line 131 · raw

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

Reads request the clock only for a present entry with a finite deadline.

def read_lifetime source · line 134 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @tracked:Bool -> @shape:Shape<K> -> @immortal:Bool -> Progress<K, V>

def read_found source · line 139 · raw

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

def read source · line 144 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> @tracked:Bool -> @shape:Shape<K> -> Progress<K, V>

def oldest_found source · line 149 · raw

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

GetOldest captures the stored original key before the untracked read; an expired oldest entry is removed while its key is still returned.

def oldest_order source · line 154 · raw

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

def get_oldest source · line 159 · raw

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

def finish_refresh source · line 165 · 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> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Progress<K, V>

Refresh counts the hit and moves recency before its clock request. A zero lifetime (only then is the immortal branch taken) stores the zero sentinel.

def refresh_lifetime 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> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @immortal:Bool -> Progress<K, V>

def refresh_prepared source · line 174 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @code:String -> @+ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @step:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V> -> Progress<K, V>

def refresh source · line 179 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Progress<K, V>

def complete source · line 184 · raw

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

Keys, Values and PurgeExpired process only the oldest expired prefix. Each inspected finite oldest entry costs exactly one clock request.

def expire_lifetime source · line 187 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @shape:Shape<K> -> @immortal:Bool -> Progress<K, V>

def expire_entry source · line 192 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @shape:Shape<K> -> @entry:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Progress<K, V>

def expire_next source · line 197 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @shape:Shape<K> -> Progress<K, V>

def expire_decide source · line 202 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @remaining:Nat -> @shape:Shape<K> -> @expired:Bool -> Progress<K, V>

def expire_sampled source · line 207 · raw

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

def expire source · line 212 · raw

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

def purge source · line 216 · raw

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

With no removal observer, full Purge is one native Map.new replacement.

def removed_oldest source · line 220 · raw

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

def start source · line 224 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @zero_key:K -> @zero_value:V -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @request:Request<K, V> -> Progress<K, V>

def resume source · line 246 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @pending:Pending<K, V> -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> Progress<K, V>

Exactly one accepted sample answers one Waiting progress.

def abandon source · line 254 · raw

@-K:Data -> @-V:Data -> @pending:Pending<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>

State retained by the host when the awaited clock request fails.