1	import Base
2	import ../types/model.bend as T
3	import ./cache.bend as S
4	import ./numeric.bend as N
5	
6	# Independent finite-map transition semantics. No implementation/proof imports.
7	# Supplied 'now' is the explicit sample at the operation's clock-read point.
8	# User callbacks are excluded. Legacy event fields are inert on initial states.
9	def write(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K, value: V, deadline: T.Int64, evicted: Bool, events: List<&2, T.LruEvent<K, V>>) -> S.Observation<K, V>:
10	  S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
11	  S.Observed{S.Abstract{cap, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, bindings, key)}, List.append(&2, K, S.unlist(~K, ~same, order, key), Con{key, Nil{}}), life, T.Counts{Word.inc(64n, i), e, r, h, m}, cb}, None{}, evicted, events}
12	
13	# Abstract state immediately after capacity eviction, before the new write.
14	# This factors the state already used by after_eviction below; no clock is read.
15	def evicted_state(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K) -> S.Model<K, V>:
16	  S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
17	  S.Abstract{cap, S.erase(~K, ~same, V, bindings, key), S.unlist(~K, ~same, order, key), life, T.Counts{i, Word.inc(64n, e), r, h, m}, cb}
18	
19	def after_eviction(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, old: T.Entry<K, V>) -> S.Observation<K, V>:
20	  S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, +cb} = s
21	  T.Item{+oldkey, oldvalue, olddeadline} = old
22	  write(~K, ~same, V, S.Abstract{cap, S.erase(~K, ~same, V, bindings, oldkey), S.unlist(~K, ~same, order, oldkey), life, T.Counts{i, Word.inc(64n, e), r, h, m}, cb}, key, value, deadline, True{}, S.callbacks(K, V, Con{T.Item{oldkey, oldvalue, olddeadline}, Nil{}}, cb))
23	
24	def evict_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, old: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
25	  match old:
26	    case None{}:
27	      write(~K, ~same, V, s, key, value, deadline, False{}, Nil{})
28	    case Some{entry}:
29	      after_eviction(~K, ~same, V, s, key, value, deadline, entry)
30	
31	def evict_first(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>) -> S.Observation<K, V>:
32	  match order:
33	    case Nil{}:
34	      write(~K, ~same, V, s, key, value, deadline, False{}, Nil{})
35	    case Con{old, tail}:
36	      evict_found(~K, ~same, V, s, key, value, deadline, S.find(~K, ~same, V, bindings, old))
37	
38	def new_room(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>, full: Bool) -> S.Observation<K, V>:
39	  match full:
40	    case False{}:
41	      write(~K, ~same, V, s, key, value, deadline, False{}, Nil{})
42	    case True{}:
43	      evict_first(~K, ~same, V, s, key, value, deadline, bindings, order)
44	
45	def absent_add(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, value: V, deadline: T.Int64) -> S.Observation<K, V>:
46	  S.Abstract{cap, bindings, +order, life, counts, cb} = s
47	  new_room(~K, ~same, V, s, key, value, deadline, bindings, order, Nat.is_ge(List.length(&2, K, order), cap))
48	
49	def add_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
50	  match found:
51	    case None{}:
52	      absent_add(~K, ~same, V, s, key, value, deadline)
53	    case Some{T.Item{original, oldvalue, olddeadline}}:
54	      write(~K, ~same, V, s, original, value, deadline, False{}, Nil{})
55	
56	def add_with_lifetime(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, +key: K, value: V, ns: T.Int64, now: T.Int64) -> S.Observation<K, V>:
57	  S.Abstract{cap, bindings, order, life, counts, cb} = s
58	  add_found(~K, ~same, V, s, key, value, N.deadline(now, ns), S.find(~K, ~same, V, bindings, key))
59	
60	def add(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, value: V, now: T.Int64) -> S.Observation<K, V>:
61	  S.Abstract{cap, bindings, order, life, counts, cb} = s
62	  add_with_lifetime(~K, ~same, V, s, key, value, life, now)
63	
64	def count_miss(-K: Data, -V: Data, s: S.Model<K, V>, tracked: Bool) -> S.Model<K, V>:
65	  S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
66	  match tracked:
67	    case False{}:
68	      S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb}
69	    case True{}:
70	      S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, Word.inc(64n, m)}, cb}
71	
72	def expired_result(-K: Data, -V: Data, result: S.Observation<K, V>, tracked: Bool) -> S.Observation<K, V>:
73	  S.Observed{s, item, flag, events} = result
74	  S.Observed{count_miss(K, V, s, tracked), item, False{}, events}
75	
76	def hit_state(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K, tracked: Bool) -> S.Model<K, V>:
77	  S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
78	  match tracked:
79	    case False{}:
80	      S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb}
81	    case True{}:
82	      S.Abstract{cap, bindings, List.append(&2, K, S.unlist(~K, ~same, order, key), Con{key, Nil{}}), life, T.Counts{i, e, r, Word.inc(64n, h), m}, cb}
83	
84	def read_decide(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, +key: K, entry: T.Entry<K, V>, tracked: Bool, expired: Bool) -> S.Observation<K, V>:
85	  match expired:
86	    case True{}:
87	      expired_result(K, V, S.remove(~K, ~same, V, s, key), tracked)
88	    case False{}:
89	      S.Observed{hit_state(~K, ~same, V, s, key, tracked), Some{entry}, True{}, Nil{}}
90	
91	def read_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, now: T.Int64, tracked: Bool, found: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
92	  match found:
93	    case None{}:
94	      S.Observed{count_miss(K, V, s, tracked), None{}, False{}, Nil{}}
95	    case Some{T.Item{k, v, +d}}:
96	      read_decide(~K, ~same, V, s, key, T.Item{k, v, d}, tracked, N.expired(d, now))
97	
98	def read(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, +key: K, now: T.Int64, tracked: Bool) -> S.Observation<K, V>:
99	  S.Abstract{cap, bindings, order, life, counts, cb} = s
100	  read_found(~K, ~same, V, s, key, now, tracked, S.find(~K, ~same, V, bindings, key))
101	
102	def refreshed(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, entry: T.Entry<K, V>, +deadline: T.Int64) -> S.Observation<K, V>:
103	  S.Abstract{cap, bindings, order, life, counts, cb} = s
104	  T.Item{+k, +v, olddeadline} = entry
105	  S.Observed{hit_state(~K, ~same, V, S.Abstract{cap, Con{T.Item{k, v, deadline}, S.erase(~K, ~same, V, bindings, k)}, order, life, counts, cb}, k, True{}), Some{T.Item{k, v, deadline}}, True{}, Nil{}}
106	
107	def refresh_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, ns: T.Int64, now: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> S.Observation<K, V>:
108	  match found:
109	    case None{}:
110	      S.missing_get(K, V, s)
111	    case Some{entry}:
112	      refreshed(~K, ~same, V, s, entry, N.deadline(now, ns))
113	
114	def refresh(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, ns: T.Int64, now: T.Int64) -> S.Observation<K, V>:
115	  S.Abstract{cap, bindings, order, life, counts, cb} = s
116	  refresh_found(~K, ~same, V, s, ns, now, S.find(~K, ~same, V, bindings, key))
117	
118	def oldest_remove(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, order: List<&2, K>) -> S.Observation<K, V>:
119	  match order:
120	    case Nil{}:
121	      S.missing_remove(K, V, s)
122	    case Con{k, tail}:
123	      S.remove(~K, ~same, V, s, k)
124	
125	def remove_oldest(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>) -> S.Observation<K, V>:
126	  S.Abstract{cap, bindings, order, life, counts, cb} = s
127	  oldest_remove(~K, ~same, V, s, order)
128	
129	def oldest_read(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, order: List<&2, K>, now: T.Int64) -> S.Observation<K, V>:
130	  match order:
131	    case Nil{}:
132	      S.Observed{s, None{}, False{}, Nil{}}
133	    case Con{k, tail}:
134	      read(~K, ~same, V, s, k, now, False{})
135	
136	# Internal snapshot only. public_oldest.bend supplies the complete public
137	# key/value/found observation, clock consumption and missing-input failures.
138	def get_oldest(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, now: T.Int64) -> S.Observation<K, V>:
139	  S.Abstract{cap, bindings, order, life, counts, cb} = s
140	  oldest_read(~K, ~same, V, s, order, now)
141	
142	def collect(-K: Data, -V: Data, found: Maybe<&2, T.Entry<K, V>>, rest: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>:
143	  match found:
144	    case None{}:
145	      rest
146	    case Some{e}:
147	      Con{e, rest}
148	
149	def ordered(~K: Data, ~same: K -> K -> Bool, -V: Data, order: List<&2, K>, +bindings: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>:
150	  match order:
151	    case Nil{}:
152	      Nil{}
153	    case Con{k, tail}:
154	      collect(K, V, S.find(~K, ~same, V, bindings, k), ordered(~K, ~same, V, tail, bindings))
155	
156	def all_entries(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>) -> List<&2, T.Entry<K, V>>:
157	  S.Abstract{cap, bindings, order, life, counts, cb} = s
158	  ordered(~K, ~same, V, order, bindings)
159	
160	def observed_state(-K: Data, -V: Data, result: S.Observation<K, V>) -> S.Model<K, V>:
161	  S.Observed{s, item, present, callbacks} = result
162	  s
163	
164	def remove_entries(~K: Data, ~same: K -> K -> Bool, -V: Data, entries: List<&2, T.Entry<K, V>>, s: S.Model<K, V>) -> S.Model<K, V>:
165	  match entries:
166	    case Nil{}:
167	      s
168	    case Con{T.Item{k, v, d}, tail}:
169	      remove_entries(~K, ~same, V, tail, observed_state(K, V, S.remove(~K, ~same, V, s, k)))
170	
171	type AggregateFailure<-K: Data, -V: Data> is Data:
172	  AggregateFailed{error: String, state: S.Model<K, V>, unused_clock: List<&2, T.Int64>}
173	
174	type AggregateResult<-K: Data, -V: Data> is Data:
175	  Aggregate{state: S.Model<K, V>, keys: List<&2, K>, values: List<&2, V>, callbacks: List<&2, T.LruEvent<K, V>>, unused_clock: List<&2, T.Int64>}
176	
177	def entry_keys(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>) -> List<&2, K>:
178	  match entries:
179	    case Nil{}:
180	      Nil{}
181	    case Con{T.Item{k, v, d}, tail}:
182	      Con{k, entry_keys(K, V, tail)}
183	
184	def entry_values(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>) -> List<&2, V>:
185	  match entries:
186	    case Nil{}:
187	      Nil{}
188	    case Con{T.Item{k, v, d}, tail}:
189	      Con{v, entry_values(K, V, tail)}
190	
191	# The aggregate exposes both projections so Keys and Values share exactly the
192	# same expiry/removal/clock semantics; consumers choose the return field.
193	def prefix_result(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, enabled: Bool, prefix: Result<&2, &2, S.PrefixFailure<K, V>, S.ExpiredPrefix<K, V>>) -> Result<&2, &2, AggregateFailure<K, V>, AggregateResult<K, V>>:
194	  match prefix:
195	    case Fail{S.PrefixFailed{err, removed, retained, times}}:
196	      Fail{AggregateFailed{err, remove_entries(~K, ~same, V, removed, s), times}}
197	    case Done{S.Prefix{+removed, +retained, times}}:
198	      Done{Aggregate{remove_entries(~K, ~same, V, removed, s), entry_keys(K, V, retained), entry_values(K, V, retained), S.callbacks(K, V, removed, enabled), times}}
199	
200	def purge_expired(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, times: List<&2, T.Int64>) -> Result<&2, &2, AggregateFailure<K, V>, AggregateResult<K, V>>:
201	  S.Abstract{cap, bindings, order, life, counts, cb} = s
202	  prefix_result(~K, ~same, V, s, cb, S.expired_prefix(K, V, all_entries(~K, ~same, V, s), times))
203	
204	def purge(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>) -> AggregateResult<K, V>:
205	  S.Abstract{cap, bindings, order, life, counts, cb} = s
206	  Aggregate{S.purged(K, V, s), Nil{}, Nil{}, S.callbacks(K, V, all_entries(~K, ~same, V, s), cb), Nil{}}