~/bend-docscommunity

proofs/lib/lemmas/proofs/cache_oldest_available.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_oldest_available.bend as Cache_oldest_available

13 imports
import Base
import ../src/cache.bend as C
import ../src/protocol.bend as P
import ../types/model.bend as T
import ./invariants.bend as Inv
import ./map_key_lookup.bend as M
import ./map_key_membership.bend as Keys
import ./map_insert.bend as I
import ./refinement.bend as F
import ./cache_populated.bend as Pop
import ./cache_order.bend as O
import ./recency_capacity.bend as B
import ./recency_bounds.bend as Bounds

Laws

law bridge provedsource · line 22 · raw

@-K:Data -> @-V:Data -> @+cap:Nat -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>> -> @+order:List<&2, String> -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @+counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @+cb:Bool -> @+code:String -> @w:Sigma<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>, entry => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.lookup(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>, None{}, table, code) == Some{entry} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>}> -> available(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{cap, table, order, life, counts, cb}, code)

law ordered_lookup provedsource · line 38 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> @valid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/refinement.storage_critbit(K, V, c) == True{} : Bool} -> @populated:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_populated.storage_populated(K, V, c) == True{} : Bool} -> @included:{order_in_keys(K, V, c) == True{} : Bool} -> @member:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_order.ordered(K, V, c, code) == True{} : Bool} -> available(K, V, c, code)

law head_member provedsource · line 53 · raw

@+code:String -> @rest:List<&2, String> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.member(code <> rest, code) == True{} : Bool}

law detach_frees_slot provedsource · line 61 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> @member:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_order.ordered(K, V, c, code) == True{} : Bool} -> @w:available(K, V, c, code) -> {Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.len(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/protocol.detach(K, V, c, code))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.len(K, V, c)) == True{} : Bool}

law oldest_frees_slot provedsource · line 77 · raw

@-K:Data -> @-V:Data -> @+cap:Nat -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>> -> @+code:String -> @+rest:List<&2, String> -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @+counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @+cb:Bool -> @valid:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/refinement.storage_critbit(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{cap, table, code <> rest, life, counts, cb}) == True{} : Bool} -> @populated:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/cache_populated.storage_populated(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{cap, table, code <> rest, life, counts, cb}) == True{} : Bool} -> @included:{order_in_keys(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{cap, table, code <> rest, life, counts, cb}) == True{} : Bool} -> {Nat.is_le(1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.len(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/protocol.detach_oldest(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{cap, table, code <> rest, life, counts, cb}))), 1n+List.length(&2, String, rest)) == True{} : Bool}

No successful lookup is assumed: it follows from the three input storage components. The conclusion concerns the actual facade-used protocol phase.

Definitions

def order_in_keys source · line 15 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> Bool

def available source · line 19 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> Type