1	import Base
2	import ../src/cache.bend as C
3	import ../src/codec.bend as Codec
4	import ../spec/cache.bend as S
5	import ../spec/operations.bend as O
6	import ../types/model.bend as T
7	import ./refinement.bend as F
8	import ./invariants.bend as Inv
9	import ./lookup_refinement.bend as L
10	import ./spec_lookup.bend as Lookup
11	import ./spec_write_lookup.bend as Write
12	import ./abstraction_bindings.bend as B
13	import ./removal_lookup.bend as Storage
14	import ./recency_unique.bend as Unique
15	
16	def target(-V: Data, s: S.Model<String, V>, key: String, value: V, deadline: T.Int64, flag: Bool, events: List<&2, T.LruEvent<String, V>>, query: String) -> Maybe<&2, T.Entry<String, V>>:
17	  S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, O.observed_state(String, V, O.write(~String, ~Lookup.string_same, V, s, key, value, deadline, flag, events))), query)
18	
19	def same(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +deadline: T.Int64, +flag: Bool, +events: List<&2, T.LruEvent<String, V>>) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), key) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, key) : Maybe<&2, T.Entry<String, V>>}:
20	  Equal.trans(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), key), Some{T.Item{key, value, deadline}}, target(V, F.abstract(String, V, c), key, value, deadline, flag, events, key), F.store_lookup(String, V, c, key, key, value, deadline, flag, events), Equal.sym(Maybe<&2, T.Entry<String, V>>, target(V, F.abstract(String, V, c), key, value, deadline, flag, events, key), Some{T.Item{key, value, deadline}}, Write.same(V, F.abstract(String, V, c), key, value, deadline, flag, events)))
21	
22	def other(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +deadline: T.Int64, +flag: Bool, +events: List<&2, T.LruEvent<String, V>>, +query: String, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, +different: {String.eq(key, query) == False{} : Bool}) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query) : Maybe<&2, T.Entry<String, V>>}:
23	  Equal.trans(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query), C.lookup(String, V, c, query), target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query), F.store_other_lookup(String, V, c, key, key, value, deadline, flag, events, query, Write.reverse_false(key, query, different), Storage.valid_storage(V, c, valid)), Equal.trans(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, c, query), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), query), target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query), L.string_lookup(V, c, query, valid), Equal.sym(Maybe<&2, T.Entry<String, V>>, target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), query), Write.other(V, F.abstract(String, V, c), key, value, deadline, flag, events, query, different))))
24	
25	def decide(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +deadline: T.Int64, +flag: Bool, +events: List<&2, T.LruEvent<String, V>>, +query: String, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, equal: Bool, decision: {String.eq(key, query) == equal : Bool}) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query) : Maybe<&2, T.Entry<String, V>>}:
26	  match equal:
27	    case False{}: other(V, c, key, value, deadline, flag, events, query, valid, decision)
28	    case True{}:
29	      %Unique.equal_boolean(key, query, decision) : {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), _) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, _) : Maybe<&2, T.Entry<String, V>>}
30	      same(V, c, key, value, deadline, flag, events)
31	
32	def correspondence(-V: Data, c: C.Cache<String, V>, +key: String, value: V, deadline: T.Int64, flag: Bool, events: List<&2, T.LruEvent<String, V>>, +query: String, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query) : Maybe<&2, T.Entry<String, V>>}:
33	  decide(V, c, key, value, deadline, flag, events, query, valid, String.eq(key, query), {==})