proofs/lib/lemmas/proofs/public_finish.bend
bend-collections-laws-containers@1.0.0.0 · 82 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as C
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/codec.bend as Codec
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/public.bend as Pub
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/protocol.bend as P
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/driver.bend as D
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/clock.bend as Clock
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/operations.bend as O
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/public_commands.bend as PC
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/equivalence.bend as E
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refinement.bend as F
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_lookup.bend as Lookup
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/ordered_entries.bend as Ordered
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_relation.bend as R
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_drive.bend as Drive
19import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Routing
20
21def 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
30def 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
37def 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.
47def 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
51def 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
57def 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.
68def 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
76def 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
80def 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)))