proofs/lib/lemmas/proofs/public_simple.bend
bend-collections-laws-containers@1.0.0.0 · 24 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/driver.bend as D
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/clock.bend as Clock
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/operations.bend as O
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/public_commands.bend as PC
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/equivalence.bend as E
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refinement.bend as F
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/disabled.bend as Disabled
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/public_relation.bend as R
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/public_finish.bend as Finish
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/extensional_states.bend as Ext
19import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/remove_refinement.bend as Remove
20
21# Whole public Remove through the actual start/drive machine, every event list.
22def remove(-V: Data, zero_key: String, +zero_value: V, +c: C.Cache<String, V>, +key: String, +events: List<&2, Clock.ClockEvent>, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}) -> R.results(~String, ~Lookup.string_same, V, D.execute(~String, ~Codec.string_encode, V, zero_key, zero_value, c, events, Pub.Remove{key}), PC.execute(~String, ~Lookup.string_same, V, F.abstract(String, V, c), zero_key, zero_value, events, R.command(String, V, Pub.Remove{key}))):
23 %Equal.sym(D.Outcome<String, V>, D.drive(String, V, zero_value, events, Pub.finish_step(String, V, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{})), Finish.returned(V, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{}, events, 0n), Finish.drive_step(V, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{}, events)) : R.results(~String, ~Lookup.string_same, V, _, PC.observation(~String, ~Lookup.string_same, V, zero_key, zero_value, PC.Flag{}, S.remove(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key), events, 0n))
24 Finish.finished(V, zero_key, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{}, S.remove(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key), events, 0n, {==}, Remove.operation(V, c, key, valid, disabled))