proofs/lib/lemmas/proofs/refresh_lookup.bend
bend-collections-laws-containers@1.0.0.0 · 117 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as C
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/protocol.bend as P
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
5
6def item(-K: Data, -V: Data, step: C.Step<K, V>) -> Maybe<&2, T.Entry<K, V>>:
7 C.Out{cache, result, flag, events} = step
8 result
9
10# Recency and hit accounting cannot change any lookup.
11law live_lookup:
12 for -K: Data
13 for -V: Data
14 for c: C.Cache<K, V>
15 for code: String
16 for entry: T.Entry<K, V>
17 for tracked: Bool
18 for query: String
19 {C.lookup(K, V, C.step_cache(K, V, C.read_live(K, V, c, code, entry, tracked)), query) == C.lookup(K, V, c, query) : Maybe<&2, T.Entry<K, V>>}
20def live_lookup(K, V, c, code, entry, tracked, query):
21 C.State{cap, table, order, life, counts, cb} = c
22 {==}
23
24law miss_lookup:
25 for -K: Data
26 for -V: Data
27 for c: C.Cache<K, V>
28 for query: String
29 {C.lookup(K, V, P.finish_miss(K, V, c, True{}), query) == C.lookup(K, V, c, query) : Maybe<&2, T.Entry<K, V>>}
30def miss_lookup(K, V, c, query):
31 C.State{cap, table, order, life, counts, cb} = c
32 {==}
33
34law live_item:
35 for -K: Data
36 for -V: Data
37 for c: C.Cache<K, V>
38 for code: String
39 for entry: T.Entry<K, V>
40 {item(K, V, C.read_live(K, V, c, code, entry, True{})) == Some{entry} : Maybe<&2, T.Entry<K, V>>}
41def live_item(K, V, c, code, entry):
42 C.State{cap, table, order, life, counts, cb} = c
43 {==}
44
45law prepare_found:
46 for -K: Data
47 for -V: Data
48 for +c: C.Cache<K, V>
49 for +code: String
50 for found: Maybe<&2, T.Entry<K, V>>
51 for decision: {C.lookup(K, V, c, code) == found : Maybe<&2, T.Entry<K, V>>}
52 {C.lookup(K, V, C.step_cache(K, V, P.refresh_prepare_found(K, V, c, code, found)), code) == item(K, V, P.refresh_prepare_found(K, V, c, code, found)) : Maybe<&2, T.Entry<K, V>>}
53def prepare_found(K, V, c, code, found, decision):
54 match found:
55 case None{}:
56 Equal.trans(Maybe<&2, T.Entry<K, V>>, C.lookup(K, V, P.finish_miss(K, V, c, True{}), code), C.lookup(K, V, c, code), None{}, miss_lookup(K, V, c, code), decision)
57 case Some{+entry}:
58 %Equal.sym(Maybe<&2, T.Entry<K, V>>, item(K, V, C.read_live(K, V, c, code, entry, True{})), Some{entry}, live_item(K, V, c, code, entry)) : {C.lookup(K, V, C.step_cache(K, V, C.read_live(K, V, c, code, entry, True{})), code) == _ : Maybe<&2, T.Entry<K, V>>}
59 Equal.trans(Maybe<&2, T.Entry<K, V>>, C.lookup(K, V, C.step_cache(K, V, C.read_live(K, V, c, code, entry, True{})), code), C.lookup(K, V, c, code), Some{entry}, live_lookup(K, V, c, code, entry, True{}, code), decision)
60
61# Arbitrary actual preparation returns the binding still stored in its output
62# state. No validity, expiration or assumed successful-transport premise.
63law prepare:
64 for -K: Data
65 for -V: Data
66 for +c: C.Cache<K, V>
67 for +code: String
68 {C.lookup(K, V, C.step_cache(K, V, P.refresh_prepare(K, V, c, code)), code) == item(K, V, P.refresh_prepare(K, V, c, code)) : Maybe<&2, T.Entry<K, V>>}
69def prepare(K, V, c, code):
70 prepare_found(K, V, c, code, C.lookup(K, V, c, code), {==})
71
72law successful_prepare:
73 for -K: Data
74 for -V: Data
75 for +c: C.Cache<K, V>
76 for +code: String
77 for entry: T.Entry<K, V>
78 for returned: {item(K, V, P.refresh_prepare(K, V, c, code)) == Some{entry} : Maybe<&2, T.Entry<K, V>>}
79 {C.lookup(K, V, C.step_cache(K, V, P.refresh_prepare(K, V, c, code)), code) == Some{entry} : Maybe<&2, T.Entry<K, V>>}
80def successful_prepare(K, V, c, code, entry, returned):
81 Equal.trans(Maybe<&2, T.Entry<K, V>>, C.lookup(K, V, C.step_cache(K, V, P.refresh_prepare(K, V, c, code)), code), item(K, V, P.refresh_prepare(K, V, c, code)), Some{entry}, prepare(K, V, c, code), returned)
82
83def flag(-K: Data, -V: Data, step: C.Step<K, V>) -> Bool:
84 C.Out{cache, result, success, events} = step
85 success
86
87law live_flag:
88 for -K: Data
89 for -V: Data
90 for c: C.Cache<K, V>
91 for code: String
92 for entry: T.Entry<K, V>
93 {flag(K, V, C.read_live(K, V, c, code, entry, True{})) == Maybe.is_some(&2, T.Entry<K, V>, item(K, V, C.read_live(K, V, c, code, entry, True{}))) : Bool}
94def live_flag(K, V, c, code, entry):
95 C.State{cap, table, order, life, counts, cb} = c
96 {==}
97
98law found_flag:
99 for -K: Data
100 for -V: Data
101 for c: C.Cache<K, V>
102 for code: String
103 for found: Maybe<&2, T.Entry<K, V>>
104 {flag(K, V, P.refresh_prepare_found(K, V, c, code, found)) == Maybe.is_some(&2, T.Entry<K, V>, item(K, V, P.refresh_prepare_found(K, V, c, code, found))) : Bool}
105def found_flag(K, V, c, code, found):
106 match found:
107 case None{}: {==}
108 case Some{entry}: live_flag(K, V, c, code, entry)
109
110law prepare_flag:
111 for -K: Data
112 for -V: Data
113 for +c: C.Cache<K, V>
114 for +code: String
115 {flag(K, V, P.refresh_prepare(K, V, c, code)) == Maybe.is_some(&2, T.Entry<K, V>, item(K, V, P.refresh_prepare(K, V, c, code))) : Bool}
116def prepare_flag(K, V, c, code):
117 found_flag(K, V, c, code, C.lookup(K, V, c, code))