1	import Base
2	import ../src/cache.bend as C
3	import ../src/protocol.bend as P
4	import ../types/model.bend as T
5	
6	def 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.
11	law 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>>}
20	def live_lookup(K, V, c, code, entry, tracked, query):
21	  C.State{cap, table, order, life, counts, cb} = c
22	  {==}
23	
24	law 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>>}
30	def miss_lookup(K, V, c, query):
31	  C.State{cap, table, order, life, counts, cb} = c
32	  {==}
33	
34	law 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>>}
41	def live_item(K, V, c, code, entry):
42	  C.State{cap, table, order, life, counts, cb} = c
43	  {==}
44	
45	law 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>>}
53	def 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.
63	law 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>>}
69	def prepare(K, V, c, code):
70	  prepare_found(K, V, c, code, C.lookup(K, V, c, code), {==})
71	
72	law 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>>}
80	def 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	
83	def flag(-K: Data, -V: Data, step: C.Step<K, V>) -> Bool:
84	  C.Out{cache, result, success, events} = step
85	  success
86	
87	law 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}
94	def live_flag(K, V, c, code, entry):
95	  C.State{cap, table, order, life, counts, cb} = c
96	  {==}
97	
98	law 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}
105	def 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	
110	law 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}
116	def prepare_flag(K, V, c, code):
117	  found_flag(K, V, c, code, C.lookup(K, V, c, code))