1	import Base
2	import ../src/cache.bend as C
3	import ../src/codec.bend as Codec
4	import ../src/public.bend as Pub
5	import ../src/protocol.bend as P
6	import ../src/driver.bend as D
7	import ../spec/cache.bend as S
8	import ../spec/clock.bend as Clock
9	import ../spec/operations.bend as O
10	import ../spec/public_commands.bend as PC
11	import ../spec/equivalence.bend as E
12	import ../types/model.bend as T
13	import ./refinement.bend as F
14	import ./invariants.bend as Inv
15	import ./spec_lookup.bend as Lookup
16	import ./ordered_entries.bend as Ordered
17	import ./public_relation.bend as R
18	import ./public_drive.bend as Drive
19	import ./map_routing.bend as Routing
20	
21	def projection(-K: Data, shape: Pub.Shape<K>) -> PC.Projection<K>:
22	  match shape:
23	    case Pub.Flag{}: PC.Flag{}
24	    case Pub.ValueOnly{}: PC.ValueOnly{}
25	    case Pub.Captured{k}: PC.CapturedOldest{k}
26	    case Pub.Nothing{}: PC.Nothing{}
27	    case Pub.AllKeys{}: PC.Keys{}
28	    case Pub.AllValues{}: PC.Values{}
29	
30	def value_projection(-K: Data, -V: Data, zero: V, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> {Pub.item_value(K, V, zero, item, present) == PC.value(K, V, zero, item, present) : V}:
31	  match item present:
32	    case Some{T.Item{k, v, d}} True{}: {==}
33	    case Some{T.Item{k, v, d}} False{}: {==}
34	    case None{} True{}: {==}
35	    case None{} False{}: {==}
36	
37	def key_projection(-K: Data, -V: Data, zero: K, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> {Pub.item_key(K, V, zero, item, present) == PC.key(K, V, zero, item, present) : K}:
38	  match item present:
39	    case Some{T.Item{k, v, d}} True{}: {==}
40	    case Some{T.Item{k, v, d}} False{}: {==}
41	    case None{} True{}: {==}
42	    case None{} False{}: {==}
43	
44	# Shapes whose reply is a projection of the returned item/flag. Enumerating
45	# shapes are handled with the aggregate proof, because a function-valued
46	# extensional premise is affine and cannot be queried once per listed key.
47	def returned(-V: Data, zero_value: V, step: C.Step<String, V>, shape: Pub.Shape<String>, events: List<&2, Clock.ClockEvent>, count: Nat) -> D.Outcome<String, V>:
48	  C.Out{+c, item, flag, evs} = step
49	  D.Returned{c, Pub.shaped(String, V, zero_value, c, item, flag, shape), events, count}
50	
51	def simple(-K: Data, shape: Pub.Shape<K>) -> Bool:
52	  match shape:
53	    case Pub.AllKeys{}: False{}
54	    case Pub.AllValues{}: False{}
55	    case other: True{}
56	
57	def simple_reply(~K: Data, ~same: K -> K -> Bool, -V: Data, zero_key: K, +zero_value: V, c: C.Cache<K, V>, s: S.Model<K, V>, +item: Maybe<&2, T.Entry<K, V>>, +flag: Bool, shape: Pub.Shape<K>, plain: {simple(K, shape) == True{} : Bool}) -> {R.reply(K, V, Pub.shaped(K, V, zero_value, c, item, flag, shape)) == PC.project(~K, ~same, V, s, zero_key, zero_value, item, flag, projection(K, shape)) : PC.Reply<K, V>}:
58	  match shape:
59	    case Pub.Flag{}: {==}
60	    case Pub.ValueOnly{}: Equal.cong(V, PC.Reply<K, V>, v => PC.Value{v, flag}, Pub.item_value(K, V, zero_value, item, flag), PC.value(K, V, zero_value, item, flag), value_projection(K, V, zero_value, item, flag))
61	    case Pub.Captured{+k}: Equal.cong(V, PC.Reply<K, V>, v => PC.Oldest{k, v, flag}, Pub.item_value(K, V, zero_value, item, flag), PC.value(K, V, zero_value, item, flag), value_projection(K, V, zero_value, item, flag))
62	    case Pub.Nothing{}: {==}
63	    case Pub.AllKeys{}: Empty.absurd({R.reply(K, V, Pub.shaped(K, V, zero_value, c, item, flag, Pub.AllKeys{})) == PC.project(~K, ~same, V, s, zero_key, zero_value, item, flag, projection(K, Pub.AllKeys{})) : PC.Reply<K, V>}, Routing.false_true(plain))
64	    case Pub.AllValues{}: Empty.absurd({R.reply(K, V, Pub.shaped(K, V, zero_value, c, item, flag, Pub.AllValues{})) == PC.project(~K, ~same, V, s, zero_key, zero_value, item, flag, projection(K, Pub.AllValues{})) : PC.Reply<K, V>}, Routing.false_true(plain))
65	
66	# A finished native step whose observation refines an independent observation
67	# yields a refining public result, for any event remainder and request count.
68	def finished(-V: Data, zero_key: String, +zero_value: V, step: C.Step<String, V>, shape: Pub.Shape<String>, expected: S.Observation<String, V>, +events: List<&2, Clock.ClockEvent>, +count: Nat, plain: {simple(String, shape) == True{} : Bool}, proof: E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, step), expected)) -> R.results(~String, ~Lookup.string_same, V, returned(V, zero_value, step, shape, events, count), PC.observation(~String, ~Lookup.string_same, V, zero_key, zero_value, projection(String, shape), expected, events, count)):
69	  C.Out{+c, +item, +flag, evs} = step
70	  S.Observed{+s, expected_item, expected_flag, expected_events} = expected
71	  (related, same_item, same_flag, same_events) = proof
72	  %same_item : R.results(~String, ~Lookup.string_same, V, D.Returned{c, Pub.shaped(String, V, zero_value, c, item, flag, shape), events, count}, PC.Returned{s, PC.project(~String, ~Lookup.string_same, V, s, zero_key, zero_value, _, expected_flag, projection(String, shape)), events, count})
73	  %same_flag : R.results(~String, ~Lookup.string_same, V, D.Returned{c, Pub.shaped(String, V, zero_value, c, item, flag, shape), events, count}, PC.Returned{s, PC.project(~String, ~Lookup.string_same, V, s, zero_key, zero_value, item, _, projection(String, shape)), events, count})
74	  (related, simple_reply(~String, ~Lookup.string_same, V, zero_key, zero_value, c, s, item, flag, shape, plain), {==}, {==})
75	
76	def drive_step(-V: Data, +zero_value: V, step: C.Step<String, V>, shape: Pub.Shape<String>, events: List<&2, Clock.ClockEvent>) -> {D.drive(String, V, zero_value, events, Pub.finish_step(String, V, zero_value, step, shape)) == returned(V, zero_value, step, shape, events, 0n) : D.Outcome<String, V>}:
77	  C.Out{+c, item, flag, evs} = step
78	  Drive.finished(String, V, zero_value, events, c, Pub.shaped(String, V, zero_value, c, item, flag, shape))
79	
80	def bump_step(-V: Data, +zero_value: V, step: C.Step<String, V>, shape: Pub.Shape<String>, events: List<&2, Clock.ClockEvent>) -> {D.bump(String, V, D.drive(String, V, zero_value, events, Pub.finish_step(String, V, zero_value, step, shape))) == returned(V, zero_value, step, shape, events, 1n) : D.Outcome<String, V>}:
81	  C.Out{+c, item, flag, evs} = step
82	  Equal.cong(D.Outcome<String, V>, D.Outcome<String, V>, outcome => D.bump(String, V, outcome), D.drive(String, V, zero_value, events, Pub.Finished{c, Pub.shaped(String, V, zero_value, c, item, flag, shape)}), D.Returned{c, Pub.shaped(String, V, zero_value, c, item, flag, shape), events, 0n}, Drive.finished(String, V, zero_value, events, c, Pub.shaped(String, V, zero_value, c, item, flag, shape)))