proofs/lib/lemmas/proofs/add_refinement.bend

bend-collections-laws-containers@1.0.0.0 · 43 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/time.bend as Time
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/operations.bend as O
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/equivalence.bend as E
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refinement.bend as F
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/disabled.bend as Disabled
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_lookup.bend as Lookup
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/lookup_refinement.bend as L
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_bindings.bend as B
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/replacement_refinement.bend as Replacement
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nonfull_add.bend as Nonfull
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/full_add.bend as Full
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/duration_refinement.bend as Duration
19
20def 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
25def 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
30def 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.
36def 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
41def 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)