1	import Base
2	import ./numeric.bend as N
3	import ../types/model.bend as T
4	
5	# Independent abstract finite-map representation. Well-formed states have one
6	# binding per key and a recency permutation of exactly those keys. No native Map,
7	# implementation, codec, or proof imports occur in this specification.
8	# Binding-list order is not observable: full refinement must compare finite-map
9	# lookup extensionally (or canonicalize bindings), while recency order is exact.
10	type Model<-K: Data, -V: Data> is Data:
11	  Abstract{capacity: Nat, bindings: List<&2, T.Entry<K, V>>, recency: List<&2, K>, lifetime: T.Int64, counts: T.Metrics, callback: Bool}
12	
13	type Observation<-K: Data, -V: Data> is Data:
14	  Observed{state: Model<K, V>, returned: Maybe<&2, T.Entry<K, V>>, present: Bool, callbacks: List<&2, T.LruEvent<K, V>>}
15	
16	def initial(-K: Data, -V: Data, capacity: Nat) -> Model<K, V>:
17	  Abstract{capacity, Nil{}, Nil{}, T.I64{Word.zero(64n)}, T.zero_metrics(), False{}}
18	
19	def length(-K: Data, -V: Data, s: Model<K, V>) -> Nat:
20	  Abstract{cap, bindings, recency, life, counts, cb} = s
21	  List.length(&2, K, recency)
22	
23	def set_lifetime(-K: Data, -V: Data, s: Model<K, V>, lifetime: T.Int64) -> Model<K, V>:
24	  Abstract{cap, bindings, recency, old, counts, cb} = s
25	  Abstract{cap, bindings, recency, lifetime, counts, cb}
26	
27	def reset_metrics(-K: Data, -V: Data, s: Model<K, V>) -> Model<K, V> & T.Metrics:
28	  Abstract{cap, bindings, recency, life, counts, cb} = s
29	  (Abstract{cap, bindings, recency, life, T.zero_metrics(), cb}, counts)
30	
31	def missing_get(-K: Data, -V: Data, s: Model<K, V>) -> Observation<K, V>:
32	  Abstract{cap, bindings, recency, life, T.Counts{i, e, r, h, m}, cb} = s
33	  Observed{Abstract{cap, bindings, recency, life, T.Counts{i, e, r, h, Word.inc(64n, m)}, cb}, None{}, False{}, Nil{}}
34	
35	def missing_remove(-K: Data, -V: Data, s: Model<K, V>) -> Observation<K, V>:
36	  Observed{s, None{}, False{}, Nil{}}
37	
38	# Signed comparisons, including sentinel, specified independently.
39	def is_expired(deadline: T.Int64, now: T.Int64) -> Bool:
40	  N.expired(deadline, now)
41	
42	# Legacy pure event metadata. Supported initial states disable it and expose
43	# no registration command; no user function is represented or executed here.
44	def callbacks(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>, +enabled: Bool) -> List<&2, T.LruEvent<K, V>>:
45	  match entries enabled:
46	    case Nil{} b:
47	      Nil{}
48	    case Con{entry, tail} False{}:
49	      Nil{}
50	    case Con{T.Item{k, v, deadline}, tail} True{}:
51	      Con{T.Evicted{k, v}, callbacks(K, V, tail, True{})}
52	
53	# Full purge is defined from the ordered entries, not from implementation steps.
54	def purged(-K: Data, -V: Data, s: Model<K, V>) -> Model<K, V>:
55	  Abstract{cap, bindings, recency, life, counts, cb} = s
56	  Abstract{cap, Nil{}, Nil{}, life, T.zero_metrics(), cb}
57	
58	# Typed public commands. Independent observations and clock effects are defined
59	# in public_commands.bend, and finite caller traces in traces.bend.
60	type Command<-K: Data, -V: Data> is Data:
61	  Add{key: K, value: V}
62	  AddWithLifetime{key: K, value: V, nanoseconds: T.Int64}
63	  Get{key: K}
64	  GetAndRefresh{key: K, nanoseconds: T.Int64}
65	  Peek{key: K}
66	  Contains{key: K}
67	  Remove{key: K}
68	  RemoveOldest{}
69	  GetOldest{}
70	  Keys{}
71	  Values{}
72	  Purge{}
73	  PurgeExpired{}
74	  Len{}
75	  SetLifetime{nanoseconds: T.Int64}
76	  Metrics{}
77	  ResetMetrics{}
78	  Diagnostics{}
79	
80	# Abstract finite-map operations use user-key equality, never encoding or Map.
81	def choose_entry(-K: Data, -V: Data, entry: T.Entry<K, V>, rest: Maybe<&2, T.Entry<K, V>>, equal: Bool) -> Maybe<&2, T.Entry<K, V>>:
82	  match equal:
83	    case True{}:
84	      Some{entry}
85	    case False{}:
86	      rest
87	
88	def find(~K: Data, ~same: K -> K -> Bool, -V: Data, bindings: List<&2, T.Entry<K, V>>, +key: K) -> Maybe<&2, T.Entry<K, V>>:
89	  match bindings:
90	    case Nil{}:
91	      None{}
92	    case Con{T.Item{+k, v, d}, tail}:
93	      choose_entry(K, V, T.Item{k, v, d}, find(~K, ~same, V, tail, key), same(k)(key))
94	
95	def omit_entry(-K: Data, -V: Data, entry: T.Entry<K, V>, rest: List<&2, T.Entry<K, V>>, equal: Bool) -> List<&2, T.Entry<K, V>>:
96	  match equal:
97	    case True{}:
98	      rest
99	    case False{}:
100	      Con{entry, rest}
101	
102	def erase(~K: Data, ~same: K -> K -> Bool, -V: Data, bindings: List<&2, T.Entry<K, V>>, +key: K) -> List<&2, T.Entry<K, V>>:
103	  match bindings:
104	    case Nil{}:
105	      Nil{}
106	    case Con{T.Item{+k, v, d}, tail}:
107	      omit_entry(K, V, T.Item{k, v, d}, erase(~K, ~same, V, tail, key), same(k)(key))
108	
109	def omit_key(-K: Data, key: K, rest: List<&2, K>, equal: Bool) -> List<&2, K>:
110	  match equal:
111	    case True{}:
112	      rest
113	    case False{}:
114	      Con{key, rest}
115	
116	def unlist(~K: Data, ~same: K -> K -> Bool, order: List<&2, K>, +key: K) -> List<&2, K>:
117	  match order:
118	    case Nil{}:
119	      Nil{}
120	    case Con{+h, tail}:
121	      omit_key(K, h, unlist(~K, ~same, tail, key), same(h)(key))
122	
123	def remove_existing(~K: Data, ~same: K -> K -> Bool, -V: Data, s: Model<K, V>, +key: K, +entry: T.Entry<K, V>) -> Observation<K, V>:
124	  Abstract{cap, bindings, recency, life, T.Counts{i, e, r, h, m}, +cb} = s
125	  Observed{Abstract{cap, erase(~K, ~same, V, bindings, key), unlist(~K, ~same, recency, key), life, T.Counts{i, e, Word.inc(64n, r), h, m}, cb}, Some{entry}, True{}, callbacks(K, V, Con{entry, Nil{}}, cb)}
126	
127	def remove_decision(~K: Data, ~same: K -> K -> Bool, -V: Data, s: Model<K, V>, key: K, found: Maybe<&2, T.Entry<K, V>>) -> Observation<K, V>:
128	  match found:
129	    case None{}:
130	      missing_remove(K, V, s)
131	    case Some{entry}:
132	      remove_existing(~K, ~same, V, s, key, entry)
133	
134	def remove(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: Model<K, V>, +key: K) -> Observation<K, V>:
135	  Abstract{cap, bindings, recency, life, counts, cb} = s
136	  remove_decision(~K, ~same, V, s, key, find(~K, ~same, V, bindings, key))
137	
138	# Expiration consumes a clock sample only when the current oldest deadline is
139	# finite. A finite future deadline stops; an immortal oldest also stops without
140	# looking at any subsequent binding. This model returns removed oldest entries
141	# plus unused clock samples; transport exhaustion is an explicit failure.
142	type PrefixFailure<-K: Data, -V: Data> is Data:
143	  PrefixFailed{error: String, removed: List<&2, T.Entry<K, V>>, retained: List<&2, T.Entry<K, V>>, unused_clock: List<&2, T.Int64>}
144	
145	type ExpiredPrefix<-K: Data, -V: Data> is Data:
146	  Prefix{removed: List<&2, T.Entry<K, V>>, retained: List<&2, T.Entry<K, V>>, unused_clock: List<&2, T.Int64>}
147	
148	def prefix_prepend(-K: Data, -V: Data, entry: T.Entry<K, V>, rest: Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
149	  match rest:
150	    case Fail{PrefixFailed{err, removed, retained, times}}:
151	      Fail{PrefixFailed{err, Con{entry, removed}, retained, times}}
152	    case Done{Prefix{removed, retained, times}}:
153	      Done{Prefix{Con{entry, removed}, retained, times}}
154	
155	def prefix_decide(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, times: List<&2, T.Int64>, expired: Bool, rest: Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
156	  match expired:
157	    case False{}:
158	      Done{Prefix{Nil{}, Con{entry, tail}, times}}
159	    case True{}:
160	      prefix_prepend(K, V, entry, rest)
161	
162	def prefix_missing(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, immortal: Bool) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
163	  match immortal:
164	    case True{}:
165	      Done{Prefix{Nil{}, Con{entry, tail}, Nil{}}}
166	    case False{}:
167	      Fail{PrefixFailed{"clock sample missing", Nil{}, Con{entry, tail}, Nil{}}}
168	
169	def prefix_sampled(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, now: T.Int64, times: List<&2, T.Int64>, expired: Bool, rest: Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>, immortal: Bool) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
170	  match immortal:
171	    case True{}:
172	      Done{Prefix{Nil{}, Con{entry, tail}, Con{now, times}}}
173	    case False{}:
174	      prefix_decide(K, V, entry, tail, times, expired, rest)
175	
176	def expired_prefix(-K: Data, -V: Data, ordered: List<&2, T.Entry<K, V>>, times: List<&2, T.Int64>) -> Result<&2, &2, PrefixFailure<K, V>, ExpiredPrefix<K, V>>:
177	  match ordered times:
178	    case Nil{} samples:
179	      Done{Prefix{Nil{}, Nil{}, samples}}
180	    case Con{T.Item{k, v, T.I64{+w}}, tail} Nil{}:
181	      prefix_missing(K, V, T.Item{k, v, T.I64{w}}, tail, N.zero(w))
182	    case Con{T.Item{k, v, T.I64{+w}}, +tail} Con{+now, +samples}:
183	      prefix_sampled(K, V, T.Item{k, v, T.I64{w}}, tail, now, samples, is_expired(T.I64{w}, now), expired_prefix(K, V, tail, samples), N.zero(w))
184	
185	def create_decision(-K: Data, -V: Data, capacity: Nat, valid: Bool) -> Result<&2, &2, String, Model<K, V>>:
186	  match valid:
187	    case False{}:
188	      Fail{"invalid capacity or size"}
189	    case True{}:
190	      Done{initial(K, V, capacity)}
191	
192	def construct(-K: Data, -V: Data, capacity: U32, size: U32, zero: Bool, reserved: Bool, small: Bool) -> Result<&2, &2, String, Model<K, V>>:
193	  match zero reserved small:
194	    case True{} a b:
195	      Fail{"capacity must be positive"}
196	    case False{} True{} b:
197	      Fail{"size must not be 0XFFFFFFFF"}
198	    case False{} False{} True{}:
199	      Fail{"size (" ++ U32.show(size) ++ ") is smaller than capacity (" ++ U32.show(capacity) ++ ")"}
200	    case False{} False{} False{}:
201	      Done{initial(K, V, U32.to_nat(capacity))}
202	
203	def new_with_size(-K: Data, -V: Data, +capacity: U32, +size: U32) -> Result<&2, &2, String, Model<K, V>>:
204	  construct(K, V, capacity, size, U32.is_eq(capacity, 0), U32.is_eq(size, 4294967295), U32.is_lt(size, capacity))