1	import Base
2	import ../src/cache.bend as C
3	import ../src/codec.bend as Codec
4	import ../src/time.bend as Time
5	import ../spec/cache.bend as S
6	import ../spec/operations.bend as O
7	import ../spec/equivalence.bend as E
8	import ../types/model.bend as T
9	import ./refinement.bend as F
10	import ./invariants.bend as Inv
11	import ./disabled.bend as Disabled
12	import ./spec_lookup.bend as Lookup
13	import ./lookup_refinement.bend as L
14	import ./abstraction_bindings.bend as B
15	import ./replacement_refinement.bend as Replacement
16	import ./nonfull_add.bend as Nonfull
17	import ./full_add.bend as Full
18	import ./duration_refinement.bend as Duration
19	
20	def absent(-V: Data, c: C.Cache<String, V>, key: String, value: V, deadline: T.Int64, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}, full: Bool, checked: {Nat.is_ge(C.len(String, V, c), C.capacity(String, V, c)) == full : Bool}) -> E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.add_found(String, V, c, key, key, value, deadline, None{})), O.add_found(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, value, deadline, None{})):
21	  match full:
22	    case False{}: Nonfull.branch(V, c, key, value, deadline, valid, checked)
23	    case True{}: Full.branch(V, c, key, value, deadline, valid, disabled, checked)
24	
25	def found(-V: Data, +c: C.Cache<String, V>, +key: String, value: V, deadline: T.Int64, result: Maybe<&2, T.Entry<String, V>>, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}, decision: {C.lookup(String, V, c, key) == result : Maybe<&2, T.Entry<String, V>>}) -> E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.add_found(String, V, c, key, key, value, deadline, result)), O.add_found(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, value, deadline, result)):
26	  match result:
27	    case None{}: absent(V, c, key, value, deadline, valid, disabled, Nat.is_ge(C.len(String, V, c), C.capacity(String, V, c)), {==})
28	    case Some{T.Item{original, old, expiry}}: Replacement.branch(V, c, key, original, old, expiry, value, deadline, valid, decision)
29	
30	def at_deadline(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +deadline: T.Int64, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}) -> E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.add_found(String, V, c, key, key, value, deadline, C.lookup(String, V, c, key))), O.add_found(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, value, deadline, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), key))):
31	  %Equal.sym(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, c, key), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), key), L.string_lookup(V, c, key, valid)) : E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.add_found(String, V, c, key, key, value, deadline, _)), O.add_found(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, value, deadline, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), key)))
32	  found(V, c, key, value, deadline, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), key), valid, disabled, L.string_lookup(V, c, key, valid))
33	
34	# Whole actual native AddWithLifetime: no remaining store-bound, selected-oldest,
35	# codec-identity or numeric-arithmetic premise. Public host effects remain open.
36	def with_lifetime(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +ns: T.Int64, +now: T.Int64, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}) -> E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.add_with_lifetime(String, V, Codec.string_encode, c, key, value, ns, now)), O.add_with_lifetime(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, value, ns, now)):
37	  C.State{+cap, +table, +order, +life, +counts, +cb} = c
38	  %Duration.deadline(now, ns) : E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.add_with_lifetime(String, V, Codec.string_encode, C.State{cap, table, order, life, counts, cb}, key, value, ns, now)), O.add_found(~String, ~Lookup.string_same, V, F.abstract(String, V, C.State{cap, table, order, life, counts, cb}), key, value, _, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, order, life, counts, cb})), key)))
39	  at_deadline(V, C.State{cap, table, order, life, counts, cb}, key, value, Time.deadline(now, ns), valid, disabled)
40	
41	def add(-V: Data, c: C.Cache<String, V>, key: String, value: V, now: T.Int64, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}) -> E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.add(String, V, Codec.string_encode, c, key, value, now)), O.add(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, value, now)):
42	  C.State{cap, table, order, +life, counts, cb} = c
43	  with_lifetime(V, C.State{cap, table, order, life, counts, cb}, key, value, life, now, valid, disabled)