proofs/lib/lemmas/types/model.bend source

proofs/lib/lemmas/types/model.bend on the hub · documented module

import Base# Negative{n} denotes -(n+1), so zero has exactly one representation.type Integer is Data:  Positive{magnitude: Nat}  Negative{predecessor: Nat}type Int64 is Data:  I64{bits: Word(64n)}type Metrics is Data:  Counts{inserts: Word(64n), evictions: Word(64n), removals: Word(64n), hits: Word(64n), misses: Word(64n)}type Entry<-K: Data, -V: Data> is Data:  Item{key: K, value: V, deadline: Int64}type LruEvent<-K: Data, -V: Data> is Data:  Evicted{key: K, value: V}def zero_metrics() -> Metrics:  Counts{Word.zero(64n), Word.zero(64n), Word.zero(64n), Word.zero(64n), Word.zero(64n)}