proofs/lib/lemmas/src/entry_ops.bend

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

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as C
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time
5
6# Shared entry operations used by the callback-free public machine.
7# The historical phase protocol forwards here to retain its checked proofs.
8# This module does not depend on that protocol or its aggregate/eviction phases.
9
10def finish_miss(-K: Data, -V: Data, c: C.Cache<K, V>, tracked: Bool) -> C.Cache<K, V>:
11  C.State{cap, table, order, life, counts, cb} = c
12  C.State{cap, table, order, life, C.hit_counts(counts, tracked, False{}), cb}
13
14def keys_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, K>:
15  match xs:
16    case Nil{}:
17      Nil{}
18    case Con{T.Item{k, v, d}, rest}:
19      Con{k, keys_of(K, V, rest)}
20
21def values_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, V>:
22  match xs:
23    case Nil{}:
24      Nil{}
25    case Con{T.Item{k, v, d}, rest}:
26      Con{v, values_of(K, V, rest)}
27
28def refresh_prepare_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
29  match found:
30    case None{}:
31      C.Out{finish_miss(K, V, c, True{}), None{}, False{}, Nil{}}
32    case Some{entry}:
33      C.read_live(K, V, c, code, entry, True{})
34
35def refresh_prepare(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String) -> C.Step<K, V>:
36  refresh_prepare_found(K, V, c, code, C.lookup(K, V, c, code))
37
38def refresh_at(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, lifetime: T.Int64, now: T.Int64) -> C.Cache<K, V>:
39  C.State{cap, table, order, life, counts, cb} = c
40  T.Item{k, v, old} = entry
41  C.State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, table, code, Some{T.Item{k, v, Time.deadline(now, lifetime)}}), order, life, counts, cb}