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 ../types/model.bend as T
6	import ./refinement.bend as F
7	import ./invariants.bend as Inv
8	import ./spec_lookup.bend as Lookup
9	import ./abstraction_lookup.bend as Abstract
10	import ./abstraction_bindings.bend as B
11	import ./abstraction_identity.bend as Identity
12	import ./cache_key_identity.bend as Key
13	import ./representation_access.bend as Access
14	import ./map_routing.bend as Logic
15	import ./recency_unique.bend as Unique
16	import ./map_key_membership.bend as Keys
17	
18	def reflects(~K: Data, ~same: K -> K -> Bool) -> Type:
19	  @+a: K -> @+b: K -> {same(a)(b) == True{} : Bool} -> {a == b : K}
20	
21	def reflexive(~K: Data, ~same: K -> K -> Bool) -> Type:
22	  @+a: K -> {same(a)(a) == True{} : Bool}
23	
24	def matching(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, entry: T.Entry<K, V>, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, reflection: reflects(~K, ~same), proof: B.contains(T.Entry<K, V>, B.model_bindings(K, V, F.abstract(K, V, c)), entry) & {same(Lookup.key(K, V, entry))(query) == True{} : Bool}) -> {C.lookup(K, V, c, encode(query)) == Some{entry} : Maybe<&2, T.Entry<K, V>>}:
25	  T.Item{+original, +value, +deadline} = entry
26	  (member, matched) = proof
27	  eq = reflection(original, query, matched)
28	  Equal.trans(Maybe<&2, T.Entry<K, V>>, C.lookup(K, V, c, encode(query)), C.lookup(K, V, c, encode(original)), Some{T.Item{original, value, deadline}}, Equal.cong(K, Maybe<&2, T.Entry<K, V>>, k => C.lookup(K, V, c, encode(k)), query, original, Equal.sym(K, original, query, eq)), Abstract.binding(~K, ~encode, V, c, T.Item{original, value, deadline}, valid, member))
29	
30	def model_found(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, +entry: T.Entry<K, V>, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, reflection: reflects(~K, ~same), found: {S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) == Some{entry} : Maybe<&2, T.Entry<K, V>>}) -> {C.lookup(K, V, c, encode(query)) == Some{entry} : Maybe<&2, T.Entry<K, V>>}:
31	  matching(~K, ~encode, ~same, V, c, query, entry, valid, reflection, Lookup.returned(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query, entry, found))
32	
33	def native_present(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, entry: T.Entry<K, V>, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflexivity: reflexive(~K, ~same), +found: {C.lookup(K, V, c, encode(query)) == Some{entry} : Maybe<&2, T.Entry<K, V>>}) -> {Maybe.is_some(&2, T.Entry<K, V>, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query)) == True{} : Bool}:
34	  T.Item{+original, +value, +deadline} = entry
35	  eq = Key.lookup_original_key(~K, ~encode, V, c, query, original, value, deadline, injective, Access.get_identities(~K, ~encode, V, c, valid), found)
36	  matched = Equal.trans(Bool, same(original)(query), same(query)(query), True{}, Equal.cong(K, Bool, k => same(k)(query), original, query, Equal.sym(K, query, original, eq)), reflexivity(query))
37	  Lookup.member_present(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query, T.Item{original, value, deadline}, matched, B.lookup_retained_by_abstraction(K, V, c, encode(query), T.Item{original, value, deadline}, found))
38	
39	def native_missing(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflexivity: reflexive(~K, ~same), missing: {S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) == None{} : Maybe<&2, T.Entry<K, V>>}, native: Maybe<&2, T.Entry<K, V>>, checked: {C.lookup(K, V, c, encode(query)) == native : Maybe<&2, T.Entry<K, V>>}) -> {C.lookup(K, V, c, encode(query)) == None{} : Maybe<&2, T.Entry<K, V>>}:
40	  match native:
41	    case None{}: checked
42	    case Some{entry}:
43	      Empty.absurd({C.lookup(K, V, c, encode(query)) == None{} : Maybe<&2, T.Entry<K, V>>}, Logic.false_true(Equal.trans(Bool, False{}, Maybe.is_some(&2, T.Entry<K, V>, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query)), True{}, Equal.sym(Bool, Maybe.is_some(&2, T.Entry<K, V>, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query)), False{}, Equal.cong(Maybe<&2, T.Entry<K, V>>, Bool, m => Maybe.is_some(&2, T.Entry<K, V>, m), S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query), None{}, missing)), native_present(~K, ~encode, ~same, V, c, query, entry, valid, injective, reflexivity, checked))))
44	
45	def decision(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflection: reflects(~K, ~same), reflexivity: reflexive(~K, ~same), model: Maybe<&2, T.Entry<K, V>>, checked: {S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) == model : Maybe<&2, T.Entry<K, V>>}) -> {C.lookup(K, V, c, encode(query)) == model : Maybe<&2, T.Entry<K, V>>}:
46	  match model:
47	    case None{}: native_missing(~K, ~encode, ~same, V, c, query, valid, injective, reflexivity, checked, C.lookup(K, V, c, encode(query)), {==})
48	    case Some{entry}: model_found(~K, ~encode, ~same, V, c, query, entry, valid, reflection, checked)
49	
50	# Exact finite-map lookup, including absence, with independently specified key
51	# equality. Representation and custom-codec/equality contracts are explicit.
52	def correspondence(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflection: reflects(~K, ~same), reflexivity: reflexive(~K, ~same)) -> {C.lookup(K, V, c, encode(query)) == S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) : Maybe<&2, T.Entry<K, V>>}:
53	  decision(~K, ~encode, ~same, V, c, query, valid, injective, reflection, reflexivity, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query), {==})
54	
55	def string_reflexive(+key: String) -> {String.eq(key, key) == True{} : Bool}:
56	  Keys.eq_true(key, key, {==})
57	
58	def string_lookup(-V: Data, c: C.Cache<String, V>, query: String, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {C.lookup(String, V, c, Codec.string_encode(query)) == S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), query) : Maybe<&2, T.Entry<String, V>>}:
59	  correspondence(~String, ~Codec.string_encode, ~Lookup.string_same, V, c, query, valid, Codec.string_injective, Unique.equal_boolean, string_reflexive)