proofs/lib/lemmas/types/model.bend

bend-collections-laws-containers@1.0.0.0 · 21 lines · 0 definitions

1import Base
2
3# Negative{n} denotes -(n+1), so zero has exactly one representation.
4type Integer is Data:
5  Positive{magnitude: Nat}
6  Negative{predecessor: Nat}
7
8type Int64 is Data:
9  I64{bits: Word(64n)}
10
11type Metrics is Data:
12  Counts{inserts: Word(64n), evictions: Word(64n), removals: Word(64n), hits: Word(64n), misses: Word(64n)}
13
14type Entry<-K: Data, -V: Data> is Data:
15  Item{key: K, value: V, deadline: Int64}
16
17type LruEvent<-K: Data, -V: Data> is Data:
18  Evicted{key: K, value: V}
19
20def zero_metrics() -> Metrics:
21  Counts{Word.zero(64n), Word.zero(64n), Word.zero(64n), Word.zero(64n), Word.zero(64n)}