1	import Base
2	import ../../../spec/containers/lru.bend as SP
3	import ../../../spec/lib/common.bend as SC
4	import ../../lib/array.bend as AR
5	import ../../../src/math/u64.bend as W
6	import ../../../src/containers/lru.bend as LR
7	import ./state.bend as ST
8	import ./new.bend as NW
9	import ./basic.bend as BA
10	import ./rmat.bend as RM
11	import ./read.bend as RD
12	import ./contains.bend as CT
13	import ./add.bend as AD
14	import ./remove.bend as RV
15	import ./resize.bend as RZ
16	import ./purge.bend as PU
17	import ./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	
58	def 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	
61	def 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	
64	def 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	
67	def 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	
70	def 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	
73	def 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	
76	def 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	
79	def 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	
82	def 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	
85	def 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	
88	def 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	
91	def 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	
94	def 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 ----
100	def 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)
108	def 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	
115	def 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 ----
123	def 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	
128	def new_rejects_zero(~V: Data) -> SP.Empty_Map.new_rejects_zero(~V):
129	  {==}
130	
131	def new_rejects_max(~V: Data) -> SP.Empty_Map.new_rejects_max(~V):
132	  {==}
133	
134	def 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	
137	def 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
142	def 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	
146	def 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	
150	def 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
155	def 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	
160	def 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	
164	def 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
169	def 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	
174	def 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)
179	def 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
185	def 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	
190	def 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
195	def 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
200	def 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
206	def 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	
211	def 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 ----
216	def 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	
221	def 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	
226	def 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) ----
231	def 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	
235	def 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	
239	def 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	
242	def 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	  {==}