proofs/lib/lemmas/types/model.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend as Model
1 import
import Base
Types
type Integer source · line 4 · raw
Data
Negative{n} denotes -(n+1), so zero has exactly one representation.
Positive@magnitude:Nat -> Integer
Negative@predecessor:Nat -> Integer
type Int64 source · line 8 · raw
Data
I64@bits:Word(64n) -> Int64
type Metrics source · line 11 · raw
Data
Counts@inserts:Word(64n) -> @evictions:Word(64n) -> @removals:Word(64n) -> @hits:Word(64n) -> @misses:Word(64n) -> Metrics
type Entry source · line 14 · raw
@-K:Data -> @-V:Data -> Data
Item@-K:Data -> @-V:Data -> @key:K -> @value:V -> @deadline:Int64 -> Entry<K, V>
type LruEvent source · line 17 · raw
@-K:Data -> @-V:Data -> Data
Evicted@-K:Data -> @-V:Data -> @key:K -> @value:V -> LruEvent<K, V>
Definitions
def zero_metrics source · line 20 · raw
Metrics