proofs/containers/lru/proof.bend
bend-collections-laws-containers@1.0.0.0 · 243 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
6import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/new.bend as NW
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/basic.bend as BA
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rmat.bend as RM
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/read.bend as RD
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/contains.bend as CT
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/add.bend as AD
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/remove.bend as RV
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/resize.bend as RZ
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/purge.bend as PU
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/keys.bend as KY
18
19# LRU cache (src/containers/lru.bend): public proof entry point.
20# shadow ST.Sh: the cache's U32 fields, the table and arena exponents,
21# a mirror tree for each array, and two ghost lists: the
22# recency list (oldest first) and the free list;
23# ST.real(sh) is the cache
24# abstraction ST.model(sh): the capacity, the lifetime words, the entries
25# of the recency list in order, and the counters, as a
26# proofs/spec/lru.bend cache
27# invariant ST.good(sh): the hash table's clusters, check words, unique
28# keys and links, count and load; every full bucket's slot on
29# the recency list with its hash word, and a bucket for every
30# listed slot; the recency list linked both ways with its head
31# and tail, live and without repeats, keys unique; the free
32# list linked, vacant and without repeats; every slot below
33# fresh on exactly one of the two lists
34# (proofs/lru/state.bend, generated by
35# tools/generators/lru_state.py)
36#
37# Every operation is proved for every shadow satisfying the invariant, keys
38# of every length, every value type V (Data) and every clock value:
39# new the specification's new (or its rejection)
40# capacity/len the specification's answer; cache and model kept
41# counters the specification's counters
42# set_lifetime the specification's set_lifetime
43# get/peek the specification's read: an expired entry is
44# removed, a live one returned (and, for get, touched
45# and counted)
46# contains the specification's contains
47# add insert or replace; a full cache evicts its oldest
48# entry first (precondition: 2 (len + 1) <= 2^29, i.e.
49# the table stays below 2^30 buckets)
50# remove the specification's remove
51# resize the specification's resize, evicting the oldest
52# entries while over capacity
53# purge the specification's purge
54# keys the keys oldest first, after the expired oldest
55# prefix is removed
56# and each result shadow satisfies the invariant again.
57
58def new_ok(~V: Data, +cap: U32) -> NW.MadeOK(~V, LR.new(&2, V, cap), SP.new(~V, cap)):
59 NW.new_ok(~V, cap)
60
61def capacity_ok(~V: Data, +sh: ST.Sh<V>) -> {LR.capacity(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), SP.capacity(~V, ST.model(~V, sh))) : LR.LRU<&2, V> & U32}:
62 BA.capacity_ok(~V, sh)
63
64def len_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> {LR.len(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), SP.len(~V, ST.model(~V, sh))) : LR.LRU<&2, V> & U32}:
65 BA.len_ok(~V, sh, hg)
66
67def counters_ok(~V: Data, +sh: ST.Sh<V>) -> {LR.counters(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), AR.thaw(U32, BA.mtree(~V, sh))) : LR.LRU<&2, V> & Array<U32>} & {ST.ctr(AR.slots(U32, BA.mtree(~V, sh))) == SP.counters(~V, ST.model(~V, sh)) : SP.Ctr}:
68 BA.counters_ok(~V, sh)
69
70def set_lifetime_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +ns: W.U64) -> BA.SetOK(~V, sh, SP.set_lifetime(~V, ST.model(~V, sh), ns), LR.set_lifetime_packed(&2, V, ST.real(~V, sh), ns)):
71 BA.set_lifetime_ok(~V, sh, hg, ns)
72
73def get_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, +now: W.U64) -> RM.POK(~V, Maybe<&2, V>, SP.get(~V, ST.model(~V, sh), key, now), LR.get(V, ST.real(~V, sh), key, now)):
74 RD.read_ok(~V, 1n, {==}, sh, hg, key, now, True{})
75
76def peek_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, +now: W.U64) -> RM.POK(~V, Maybe<&2, V>, SP.peek(~V, ST.model(~V, sh), key, now), LR.peek(V, ST.real(~V, sh), key, now)):
77 RD.read_ok(~V, 1n, {==}, sh, hg, key, now, False{})
78
79def contains_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, +now: W.U64) -> RM.POK(~V, Bool, SP.contains(~V, ST.model(~V, sh), key, now), LR.contains(&2, V, ST.real(~V, sh), key, now)):
80 CT.contains_ok(~V, 1n, {==}, sh, hg, key, now)
81
82def add_ok(~V: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+SP.length(~V, ST.lru_es(~V, ST.model(~V, sh)))), SC.pow2(cz)) == True{} : Bool}, +key: String, +v: V, +now: W.U64) -> RM.POK(~V, Bool, SP.add(~V, ST.model(~V, sh), key, v, now), LR.add(&2, V, ST.real(~V, sh), key, v, now)):
83 AD.add_spec_ok(~V, 1n, {==}, cz, hcz, sh, hg, hcap, key, v, now)
84
85def remove_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> RM.POK(~V, Maybe<&2, V>, SP.remove(~V, ST.model(~V, sh), key), LR.remove(&2, V, ST.real(~V, sh), key)):
86 RV.remove_ok(~V, 1n, {==}, sh, hg, key)
87
88def resize_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cap2: U32) -> RM.POK(~V, Result<&2, &2, String, U32>, SP.resize(~V, ST.model(~V, sh), cap2), LR.resize(&2, V, ST.real(~V, sh), cap2)):
89 RZ.resize_ok(~V, 1n, {==}, sh, hg, cap2)
90
91def purge_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> RM.POK(~V, U32, SP.purge(~V, ST.model(~V, sh)), LR.purge(&2, V, ST.real(~V, sh))):
92 PU.purge_ok(~V, 1n, {==}, sh, hg)
93
94def keys_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +now: W.U64) -> RM.POK(~V, List<&2, String>, SP.keys(~V, ST.model(~V, sh), now), LR.keys(&2, V, ST.real(~V, sh), now)):
95 KY.keys_ok(~V, 1n, {==}, now, sh, hg)
96
97# ==== the contract of lru (stated in spec/containers/lru.bend) ====================
98
99# ---- list facts ----
100def lg_snoc(~V: Data, +t: List<&2, SP.Ent<V>>, +h: SP.Ent<V>, +e: SP.Ent<V>) -> {SP.last_go(~V, SP.snoc(~V, t, e), h) == Some{e} : Maybe<&2, SP.Ent<V>>}:
101 match t:
102 case Nil{}:
103 {==}
104 case Con{+h2, +t2}:
105 lg_snoc(~V, t2, h2, e)
106
107# the appended entry is the newest (the SP.last of the recency order)
108def snoc_last(~V: Data, +es: List<&2, SP.Ent<V>>, +e: SP.Ent<V>) -> {SP.last(~V, SP.snoc(~V, es, e)) == Some{e} : Maybe<&2, SP.Ent<V>>}:
109 match es:
110 case Nil{}:
111 {==}
112 case Con{+h, +t}:
113 lg_snoc(~V, t, h, e)
114
115def snoc_length(~V: Data, +es: List<&2, SP.Ent<V>>, +e: SP.Ent<V>) -> {SP.length(~V, SP.snoc(~V, es, e)) == 1n+SP.length(~V, es) : Nat}:
116 match es:
117 case Nil{}:
118 {==}
119 case Con{+h, +t}:
120 Equal.cong(Nat, Nat, x => 1n+x, SP.length(~V, SP.snoc(~V, t, e)), 1n+SP.length(~V, t), snoc_length(~V, t, e))
121
122# ---- Empty_Map, Length, Capacity ----
123def new_empty(~V: Data, +cap: U32, +hz: {U32.is_eq(cap, 0) == False{} : Bool}, +hm: {U32.is_eq(cap, 4294967295) == False{} : Bool}) -> SP.Empty_Map.new_empty(~V, cap, hz, hm):
124 %Equal.sym(Bool, U32.is_eq(cap, 0), False{}, hz) : {SP.new_c(~V, cap, _, U32.is_eq(cap, 4294967295)) == SP.Made{SP.L{cap, 0, W.zero(), Nil{}, SP.zero_ctr()}} : SP.Made<V>}
125 %Equal.sym(Bool, U32.is_eq(cap, 4294967295), False{}, hm) : {SP.new_c(~V, cap, False{}, _) == SP.Made{SP.L{cap, 0, W.zero(), Nil{}, SP.zero_ctr()}} : SP.Made<V>}
126 {==}
127
128def new_rejects_zero(~V: Data) -> SP.Empty_Map.new_rejects_zero(~V):
129 {==}
130
131def new_rejects_max(~V: Data) -> SP.Empty_Map.new_rejects_max(~V):
132 {==}
133
134def length_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Length.length_value(~V, cap, on, life, es, c):
135 {==}
136
137def capacity_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Capacity.capacity_value(~V, cap, on, life, es, c):
138 {==}
139
140# ---- Include (add) ----
141# a present key: its old entry is dropped and the new one is the newest
142def add_present_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +old: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{old} : Maybe<&2, SP.Ent<V>>}) -> SP.Include.add_present_order(~V, cap, on, life, es, c, key, v, now, old, hf):
143 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{old}, hf) : {SP.add_found(~V, cap, on, life, es, c, key, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}) : SP.Lru<V> & Bool}
144 {==}
145
146def add_present_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +old: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{old} : Maybe<&2, SP.Ent<V>>}) -> SP.Include.add_present_newest(~V, cap, on, life, es, c, key, v, now, old, hf):
147 %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_present_order(~V, cap, on, life, es, c, key, v, now, old, hf)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == Some{SP.mk(~V, on, life, key, v, now)} : Maybe<&2, SP.Ent<V>>}
148 snoc_last(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now))
149
150def add_present_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +old: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{old} : Maybe<&2, SP.Ent<V>>}) -> SP.Include.add_present_length(~V, cap, on, life, es, c, key, v, now, old, hf):
151 %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_present_order(~V, cap, on, life, es, c, key, v, now, old, hf)) : {SP.length(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == 1n+SP.length(~V, SP.drop(~V, es, key)) : Nat}
152 snoc_length(~V, SP.drop(~V, es, key), SP.mk(~V, on, life, key, v, now))
153
154# an absent key with room: appended as the newest, nothing evicted
155def add_room_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == False{} : Bool}) -> SP.Include.add_room_order(~V, cap, on, life, es, c, key, v, now, hf, hr):
156 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.add_found(~V, cap, on, life, es, c, key, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}) : SP.Lru<V> & Bool}
157 %Equal.sym(Bool, U32.is_le(cap, U32.from_nat(SP.length(~V, es))), False{}, hr) : {SP.add_absent(~V, cap, on, life, es, c, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}) : SP.Lru<V> & Bool}
158 {==}
159
160def add_room_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == False{} : Bool}) -> SP.Include.add_room_newest(~V, cap, on, life, es, c, key, v, now, hf, hr):
161 %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_room_order(~V, cap, on, life, es, c, key, v, now, hf, hr)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == Some{SP.mk(~V, on, life, key, v, now)} : Maybe<&2, SP.Ent<V>>}
162 snoc_last(~V, es, SP.mk(~V, on, life, key, v, now))
163
164def add_room_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hr: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == False{} : Bool}) -> SP.Include.add_room_length(~V, cap, on, life, es, c, key, v, now, hf, hr):
165 %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, es, SP.mk(~V, on, life, key, v, now)), SP.c_ins(c)}, False{}), add_room_order(~V, cap, on, life, es, c, key, v, now, hf, hr)) : {SP.length(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == 1n+SP.length(~V, es) : Nat}
166 snoc_length(~V, es, SP.mk(~V, on, life, key, v, now))
167
168# an absent key when full: the oldest is evicted (reported), the new one is newest
169def add_evict_order(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == True{} : Bool}) -> SP.Include.add_evict_order(~V, cap, on, life, es, c, key, v, now, hf, hfu):
170 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.add_found(~V, cap, on, life, es, c, key, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}) : SP.Lru<V> & Bool}
171 %Equal.sym(Bool, U32.is_le(cap, U32.from_nat(SP.length(~V, es))), True{}, hfu) : {SP.add_absent(~V, cap, on, life, es, c, SP.mk(~V, on, life, key, v, now), _) == (SP.L{cap, on, life, SP.snoc(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}) : SP.Lru<V> & Bool}
172 {==}
173
174def add_evict_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(SP.length(~V, es))) == True{} : Bool}) -> SP.Include.add_evict_newest(~V, cap, on, life, es, c, key, v, now, hf, hfu):
175 %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, es, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}), add_evict_order(~V, cap, on, life, es, c, key, v, now, hf, hfu)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == Some{SP.mk(~V, on, life, key, v, now)} : Maybe<&2, SP.Ent<V>>}
176 snoc_last(~V, SP.tail(~V, es), SP.mk(~V, on, life, key, v, now))
177
178# eviction keeps the length (the cache holds at least the evicted entry)
179def add_evict_length(~V: Data, +cap: U32, +on: U32, +life: W.U64, +h: SP.Ent<V>, +t: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +v: V, +now: W.U64, +hf: {SP.find(~V, Con{h, t}, key) == None{} : Maybe<&2, SP.Ent<V>>}, +hfu: {U32.is_le(cap, U32.from_nat(SP.length(~V, Con{h, t}))) == True{} : Bool}) -> SP.Include.add_evict_length(~V, cap, on, life, h, t, c, key, v, now, hf, hfu):
180 %Equal.sym(SP.Lru<V> & Bool, SP.add(~V, SP.L{cap, on, life, Con{h, t}, c}, key, v, now), (SP.L{cap, on, life, SP.snoc(~V, t, SP.mk(~V, on, life, key, v, now)), SP.c_ins(SP.c_ev(c))}, True{}), add_evict_order(~V, cap, on, life, Con{h, t}, c, key, v, now, hf, hfu)) : {SP.length(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Bool, _))) == SP.length(~V, Con{h, t}) : Nat}
181 snoc_length(~V, t, SP.mk(~V, on, life, key, v, now))
182
183# ---- Element: get (touches) and peek (does not) ----
184# a live hit returns the value and makes the key the newest
185def get_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Element.get_hit(~V, cap, on, life, es, c, key, now, e, hf, hg):
186 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, True{}, _) == (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), e), SP.c_hit(c)}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}
187 %Equal.sym(Bool, SP.gone(~V, e, now), False{}, hg) : {Bool.pick(SP.Lru<V> & Maybe<&2, V>, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), True{})}, None{}), SP.read_live(~V, cap, on, life, es, c, key, e, True{})) == (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), e), SP.c_hit(c)}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}
188 {==}
189
190def get_hit_newest(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Element.get_hit_newest(~V, cap, on, life, es, c, key, now, e, hf, hg):
191 %Equal.sym(SP.Lru<V> & Maybe<&2, V>, SP.get(~V, SP.L{cap, on, life, es, c}, key, now), (SP.L{cap, on, life, SP.snoc(~V, SP.drop(~V, es, key), e), SP.c_hit(c)}, Some{SP.val_of(~V, e)}), get_hit(~V, cap, on, life, es, c, key, now, e, hf, hg)) : {SP.last(~V, SP.es_of(~V, Pair.fst(SP.Lru<V>, Maybe<&2, V>, _))) == Some{e} : Maybe<&2, SP.Ent<V>>}
192 snoc_last(~V, SP.drop(~V, es, key), e)
193
194# a miss leaves the entries unchanged and reads as absent
195def get_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Element.get_miss(~V, cap, on, life, es, c, key, now, hf):
196 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, True{}, _) == (SP.L{cap, on, life, es, SP.c_miss_if(c, True{})}, None{}) : SP.Lru<V> & Maybe<&2, V>}
197 {==}
198
199# an expired entry reads as absent and is removed
200def read_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +tracked: Bool, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == True{} : Bool}) -> SP.Iter_Model.read_expired(~V, cap, on, life, es, c, key, now, tracked, e, hf, hg):
201 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, tracked, _) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), tracked)}, None{}) : SP.Lru<V> & Maybe<&2, V>}
202 %Equal.sym(Bool, SP.gone(~V, e, now), True{}, hg) : {Bool.pick(SP.Lru<V> & Maybe<&2, V>, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), tracked)}, None{}), SP.read_live(~V, cap, on, life, es, c, key, e, tracked)) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), tracked)}, None{}) : SP.Lru<V> & Maybe<&2, V>}
203 {==}
204
205# peek: a live hit returns the value and changes nothing
206def peek_hit(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Element.peek_hit(~V, cap, on, life, es, c, key, now, e, hf, hg):
207 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, False{}, _) == (SP.L{cap, on, life, es, c}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}
208 %Equal.sym(Bool, SP.gone(~V, e, now), False{}, hg) : {Bool.pick(SP.Lru<V> & Maybe<&2, V>, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_miss_if(SP.c_rm(c), False{})}, None{}), SP.read_live(~V, cap, on, life, es, c, key, e, False{})) == (SP.L{cap, on, life, es, c}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}
209 {==}
210
211def peek_miss(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Element.peek_miss(~V, cap, on, life, es, c, key, now, hf):
212 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.read_found(~V, cap, on, life, es, c, key, now, False{}, _) == (SP.L{cap, on, life, es, SP.c_miss_if(c, False{})}, None{}) : SP.Lru<V> & Maybe<&2, V>}
213 {==}
214
215# ---- Contains ----
216def contains_live(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == False{} : Bool}) -> SP.Contains.contains_live(~V, cap, on, life, es, c, key, now, e, hf, hg):
217 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.contains_found(~V, cap, on, life, es, c, key, now, _) == (SP.L{cap, on, life, es, c}, True{}) : SP.Lru<V> & Bool}
218 %Equal.sym(Bool, SP.gone(~V, e, now), False{}, hg) : {Bool.pick(SP.Lru<V> & Bool, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}), (SP.L{cap, on, life, es, c}, True{})) == (SP.L{cap, on, life, es, c}, True{}) : SP.Lru<V> & Bool}
219 {==}
220
221def contains_expired(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}, +hg: {SP.gone(~V, e, now) == True{} : Bool}) -> SP.Contains.contains_expired(~V, cap, on, life, es, c, key, now, e, hf, hg):
222 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.contains_found(~V, cap, on, life, es, c, key, now, _) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}) : SP.Lru<V> & Bool}
223 %Equal.sym(Bool, SP.gone(~V, e, now), True{}, hg) : {Bool.pick(SP.Lru<V> & Bool, _, (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}), (SP.L{cap, on, life, es, c}, True{})) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, False{}) : SP.Lru<V> & Bool}
224 {==}
225
226def contains_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +now: W.U64, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Contains.contains_absent(~V, cap, on, life, es, c, key, now, hf):
227 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.contains_found(~V, cap, on, life, es, c, key, now, _) == (SP.L{cap, on, life, es, c}, False{}) : SP.Lru<V> & Bool}
228 {==}
229
230# ---- Delete / Exclude (remove), Clear (purge), Iter_Model (keys) ----
231def remove_present(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +e: SP.Ent<V>, +hf: {SP.find(~V, es, key) == Some{e} : Maybe<&2, SP.Ent<V>>}) -> SP.Delete.remove_present(~V, cap, on, life, es, c, key, e, hf):
232 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), Some{e}, hf) : {SP.remove_found(~V, cap, on, life, es, c, key, _) == (SP.L{cap, on, life, SP.drop(~V, es, key), SP.c_rm(c)}, Some{SP.val_of(~V, e)}) : SP.Lru<V> & Maybe<&2, V>}
233 {==}
234
235def remove_absent(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr, +key: String, +hf: {SP.find(~V, es, key) == None{} : Maybe<&2, SP.Ent<V>>}) -> SP.Delete.remove_absent(~V, cap, on, life, es, c, key, hf):
236 %Equal.sym(Maybe<&2, SP.Ent<V>>, SP.find(~V, es, key), None{}, hf) : {SP.remove_found(~V, cap, on, life, es, c, key, _) == (SP.L{cap, on, life, es, c}, None{}) : SP.Lru<V> & Maybe<&2, V>}
237 {==}
238
239def purge_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Clear.purge_value(~V, cap, on, life, es, c):
240 {==}
241
242def keys_fin_value(~V: Data, +cap: U32, +on: U32, +life: W.U64, +es: List<&2, SP.Ent<V>>, +c: SP.Ctr) -> SP.Iter_Model.keys_fin_value(~V, cap, on, life, es, c):
243 {==}