proofs/lib/lemmas/spec/effectful_operations.bend
bend-collections-laws-containers@1.0.0.0 · 124 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/operations.bend as O
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as N
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/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.
11type 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
15type PreparedAdd<-K: Data, -V: Data> is Data:
16 Prepared{state: S.Model<K, V>, original: K, evicted: Bool}
17
18def 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
23def 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
28def 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
33def 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
38def 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
42def 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
47def 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
51def 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
57def 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
61def 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
66def 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
70def 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.
76def 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
81def 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
86def 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
91def 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
96def 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
101def 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.
107def 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
112def 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
117def 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
122def 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))