1	import Base
2	import ../types/model.bend as T
3	import ./cache.bend as S
4	import ./operations.bend as O
5	import ./numeric.bend as N
6	import ./clock.bend as Clock
7	
8	# Independent Add/refresh clock effects, including the state committed before a
9	# failed request. No implementation or proof import and no successful-transport
10	# premise occurs here. Public marshalling and host composition remain separate.
11	type Outcome<-K: Data, -V: Data> is Data:
12	  Returned{observation: S.Observation<K, V>, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
13	  Failed{state: S.Model<K, V>, error: Clock.Error, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
14	
15	type PreparedAdd<-K: Data, -V: Data> is Data:
16	  Prepared{state: S.Model<K, V>, original: K, evicted: Bool}
17	
18	def evicted(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, old: T.Entry<K, V>) -> PreparedAdd<K, V>:
19	  S.Abstract{cap, bindings, order, life, T.Counts{i, e, r, h, m}, cb} = s
20	  T.Item{+oldkey, oldvalue, olddeadline} = old
21	  Prepared{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, True{}}
22	
23	def evict_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, old: Maybe<&2, T.Entry<K, V>>) -> PreparedAdd<K, V>:
24	  match old:
25	    case None{}: Prepared{s, key, False{}}
26	    case Some{entry}: evicted(~K, ~same, V, s, key, entry)
27	
28	def evict_first(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>) -> PreparedAdd<K, V>:
29	  match order:
30	    case Nil{}: Prepared{s, key, False{}}
31	    case Con{old, tail}: evict_found(~K, ~same, V, s, key, S.find(~K, ~same, V, bindings, old))
32	
33	def room(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>, full: Bool) -> PreparedAdd<K, V>:
34	  match full:
35	    case False{}: Prepared{s, key, False{}}
36	    case True{}: evict_first(~K, ~same, V, s, key, bindings, order)
37	
38	def absent_add(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K) -> PreparedAdd<K, V>:
39	  S.Abstract{cap, bindings, +order, life, counts, cb} = s
40	  room(~K, ~same, V, s, key, bindings, order, Nat.is_ge(List.length(&2, K, order), cap))
41	
42	def prepare_found(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, found: Maybe<&2, T.Entry<K, V>>) -> PreparedAdd<K, V>:
43	  match found:
44	    case Some{T.Item{original, value, deadline}}: Prepared{s, original, False{}}
45	    case None{}: absent_add(~K, ~same, V, s, key)
46	
47	def prepare_add(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, +key: K) -> PreparedAdd<K, V>:
48	  S.Abstract{cap, bindings, order, life, counts, cb} = s
49	  prepare_found(~K, ~same, V, s, key, S.find(~K, ~same, V, bindings, key))
50	
51	def sampled_add(~K: Data, ~same: K -> K -> Bool, -V: Data, prepared: PreparedAdd<K, V>, value: V, ns: T.Int64, reply: Clock.Reply) -> Outcome<K, V>:
52	  Prepared{s, key, was_evicted} = prepared
53	  match reply:
54	    case Clock.Rejected{error, remaining}: Failed{s, error, remaining, 1n}
55	    case Clock.Accepted{now, remaining}: Returned{O.write(~K, ~same, V, s, key, value, N.deadline(now, ns), was_evicted, Nil{}), remaining, 1n}
56	
57	def immortal_add(~K: Data, ~same: K -> K -> Bool, -V: Data, prepared: PreparedAdd<K, V>, value: V, events: List<&2, Clock.ClockEvent>) -> Outcome<K, V>:
58	  Prepared{s, key, was_evicted} = prepared
59	  Returned{O.write(~K, ~same, V, s, key, value, T.I64{Word.zero(64n)}, was_evicted, Nil{}), events, 0n}
60	
61	def add_lifetime(~K: Data, ~same: K -> K -> Bool, -V: Data, prepared: PreparedAdd<K, V>, value: V, ns: T.Int64, events: List<&2, Clock.ClockEvent>, immortal: Bool) -> Outcome<K, V>:
62	  match immortal:
63	    case True{}: immortal_add(~K, ~same, V, prepared, value, events)
64	    case False{}: sampled_add(~K, ~same, V, prepared, value, ns, Clock.request(events))
65	
66	def add_with_lifetime(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, value: V, ns: T.Int64, events: List<&2, Clock.ClockEvent>) -> Outcome<K, V>:
67	  T.I64{+bits} = ns
68	  add_lifetime(~K, ~same, V, prepare_add(~K, ~same, V, s, key), value, T.I64{bits}, events, N.zero(bits))
69	
70	def add(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, value: V, events: List<&2, Clock.ClockEvent>) -> Outcome<K, V>:
71	  S.Abstract{cap, bindings, order, life, counts, cb} = s
72	  add_with_lifetime(~K, ~same, V, s, key, value, life, events)
73	
74	# Refresh has already moved recency and counted the hit when its clock is read.
75	# Updating the deadline must not count that hit a second time.
76	def refresh_deadline(~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>:
77	  S.Abstract{cap, bindings, order, life, counts, cb} = s
78	  T.Item{+key, +value, old} = entry
79	  S.Observed{S.Abstract{cap, Con{T.Item{key, value, deadline}, S.erase(~K, ~same, V, bindings, key)}, order, life, counts, cb}, Some{T.Item{key, value, deadline}}, True{}, Nil{}}
80	
81	def sampled_refresh(~K: Data, ~same: K -> K -> Bool, -V: Data, prepared: S.Model<K, V>, entry: T.Entry<K, V>, ns: T.Int64, reply: Clock.Reply) -> Outcome<K, V>:
82	  match reply:
83	    case Clock.Rejected{error, remaining}: Failed{prepared, error, remaining, 1n}
84	    case Clock.Accepted{now, remaining}: Returned{refresh_deadline(~K, ~same, V, prepared, entry, N.deadline(now, ns)), remaining, 1n}
85	
86	def refresh_lifetime(~K: Data, ~same: K -> K -> Bool, -V: Data, prepared: S.Model<K, V>, entry: T.Entry<K, V>, ns: T.Int64, events: List<&2, Clock.ClockEvent>, immortal: Bool) -> Outcome<K, V>:
87	  match immortal:
88	    case True{}: Returned{refresh_deadline(~K, ~same, V, prepared, entry, T.I64{Word.zero(64n)}), events, 0n}
89	    case False{}: sampled_refresh(~K, ~same, V, prepared, entry, ns, Clock.request(events))
90	
91	def refresh_hit(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, ns: T.Int64, events: List<&2, Clock.ClockEvent>, entry: T.Entry<K, V>) -> Outcome<K, V>:
92	  T.I64{+bits} = ns
93	  T.Item{+key, value, deadline} = entry
94	  refresh_lifetime(~K, ~same, V, O.hit_state(~K, ~same, V, s, key, True{}), T.Item{key, value, deadline}, T.I64{bits}, events, N.zero(bits))
95	
96	def refresh_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, ns: T.Int64, events: List<&2, Clock.ClockEvent>, found: Maybe<&2, T.Entry<K, V>>) -> Outcome<K, V>:
97	  match found:
98	    case None{}: Returned{S.missing_get(K, V, s), events, 0n}
99	    case Some{entry}: refresh_hit(~K, ~same, V, s, ns, events, entry)
100	
101	def refresh(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, key: K, ns: T.Int64, events: List<&2, Clock.ClockEvent>) -> Outcome<K, V>:
102	  S.Abstract{cap, bindings, order, life, counts, cb} = s
103	  refresh_found(~K, ~same, V, s, ns, events, S.find(~K, ~same, V, bindings, key))
104	
105	# Get/Peek/Contains sample only for a present finite deadline. Their state is
106	# unchanged if the request fails; hit/miss accounting occurs after that point.
107	def sampled_read(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, entry: T.Entry<K, V>, tracked: Bool, reply: Clock.Reply) -> Outcome<K, V>:
108	  match reply:
109	    case Clock.Rejected{error, remaining}: Failed{s, error, remaining, 1n}
110	    case Clock.Accepted{now, remaining}: Returned{O.read_found(~K, ~same, V, s, key, now, tracked, Some{entry}), remaining, 1n}
111	
112	def read_lifetime(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, entry: T.Entry<K, V>, tracked: Bool, events: List<&2, Clock.ClockEvent>, immortal: Bool) -> Outcome<K, V>:
113	  match immortal:
114	    case True{}: Returned{O.read_decide(~K, ~same, V, s, key, entry, tracked, False{}), events, 0n}
115	    case False{}: sampled_read(~K, ~same, V, s, key, entry, tracked, Clock.request(events))
116	
117	def read_found(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, key: K, tracked: Bool, events: List<&2, Clock.ClockEvent>, found: Maybe<&2, T.Entry<K, V>>) -> Outcome<K, V>:
118	  match found:
119	    case None{}: Returned{S.Observed{O.count_miss(K, V, s, tracked), None{}, False{}, Nil{}}, events, 0n}
120	    case Some{T.Item{original, value, T.I64{+bits}}}: read_lifetime(~K, ~same, V, s, key, T.Item{original, value, T.I64{bits}}, tracked, events, N.zero(bits))
121	
122	def read(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, +key: K, tracked: Bool, events: List<&2, Clock.ClockEvent>) -> Outcome<K, V>:
123	  S.Abstract{cap, bindings, order, life, counts, cb} = s
124	  read_found(~K, ~same, V, s, key, tracked, events, S.find(~K, ~same, V, bindings, key))