~/bend-docscommunity

proofs/lib/lemmas/proofs/refinement.bend checks

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

15 imports
import Base
import ./map_set_frame.bend as SetFrame
import ./map_set_critbit.bend as SetCritbit
import ./map_delete_critbit.bend as DeleteCritbit
import ./map_delete_frame.bend as DeleteFrame
import ./map_delete_routes.bend as DeleteRoutes
import ./map_routing.bend as Routes
import ./map_lookup.bend as Lookup
import ./map_seek.bend as Seek
import ./map_delete.bend as Delete
import ./invariants.bend as Invariants
import ./map_insert.bend as Insert
import ../types/model.bend as T
import ../spec/cache.bend as S
import ../src/cache.bend as C

Laws

law initialization provedsource · line 19 · raw

@-K:Data -> @-V:Data -> @cap:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.len(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.length(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.initial(K, V, cap)) : Nat}

Initial refinement is generic in original key/value types. The full abstraction of nonempty maps and its representation invariant remain separate obligations.

law initialization_empty_lookup provedsource · line 27 · raw

@-K:Data -> @-V:Data -> @cap:Nat -> @code:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap), code) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>}

law initialization_metrics provedsource · line 36 · raw

@-K:Data -> @-V:Data -> @cap:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.metrics(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.zero_metrics : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics}

law empty_remove provedsource · line 46 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @cap:Nat -> @key:K -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.remove(K, V, encode, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Out{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap), None{}, False{}, []} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>}

An actual operation law, quantified over every key and encoder, including encoders not yet proved injective (empty lookup does not need injectivity).

law empty_get provedsource · line 56 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @cap:Nat -> @key:K -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.get(K, V, encode, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap), key, now) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Out{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{cap, MTip{}, [], 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.I64{Word.zero(64n)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Counts{Word.zero(64n), Word.zero(64n), Word.zero(64n), Word.zero(64n), Word.inc(64n, Word.zero(64n))}, False{}}, None{}, False{}, []} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V>}

law initial_state_refines provedsource · line 106 · raw

@-K:Data -> @-V:Data -> @capacity:Nat -> {abstract(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, capacity)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.initial(K, V, capacity) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>}

law creation_decision_refines provedsource · line 114 · raw

@-K:Data -> @-V:Data -> @capacity:Nat -> @valid:Bool -> {abstract_created(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.new_checked(K, V, capacity, valid)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.create_decision(K, V, capacity, valid) : Result<&2, &2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>>}

law construct_refines provedsource · line 127 · raw

@-K:Data -> @-V:Data -> @capacity:U32 -> @size:U32 -> @zero:Bool -> @reserved:Bool -> @small:Bool -> {abstract_created(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.construct(K, V, capacity, size, zero, reserved, small)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.construct(K, V, capacity, size, zero, reserved, small) : Result<&2, &2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>>}

law new_with_size_refines provedsource · line 147 · raw

@-K:Data -> @-V:Data -> @+capacity:U32 -> @+size:U32 -> {abstract_created(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.new_with_size(K, V, capacity, size)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.new_with_size(K, V, capacity, size) : Result<&2, &2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>>}

law empty_get_refines provedsource · line 156 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @cap:Nat -> @key:K -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> {observe(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.get(K, V, encode, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap), key, now)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.missing_get(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.initial(K, V, cap)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>}

law empty_remove_refines provedsource · line 167 · raw

@-K:Data -> @-V:Data -> @encode:(@_:K -> String) -> @cap:Nat -> @key:K -> {observe(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.remove(K, V, encode, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.init(K, V, cap), key)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.missing_remove(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.initial(K, V, cap)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>}

law set_lifetime_refines provedsource · line 179 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> {abstract(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.set_lifetime(K, V, c, ns)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.set_lifetime(K, V, abstract(K, V, c), ns) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>}

These are universal actual-operation refinements, for every state. They do not establish or assume preservation of the still-unproved map invariant.

law reset_metrics_refines provedsource · line 194 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> {abstract_reset(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.reset_metrics(K, V, c)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.reset_metrics(K, V, abstract(K, V, c)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics)}

law lookup_projection_bridge provedsource · line 204 · raw

@-K:Data -> @-V:Data -> @result:Pair(Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup_result(K, V, result) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.value(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>, result) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>}

law store_lookup provedsource · line 216 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> @+key:K -> @+value:V -> @+deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @flag:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.store(K, V, c, code, key, value, deadline, flag, events)), code) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Item{key, value, deadline}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>}

Actual native-Map write is observable through the actual cache lookup. This is a same-key storage property, not other-key or full operation refinement.

law lookup_enumerated provedsource · line 236 · raw

@-K:Data -> @-V:Data -> @+capacity:Nat -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>> -> @+order:List<&2, String> -> @+lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @+counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @+cb:Bool -> @+code:String -> @+entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{capacity, table, order, lifetime, counts, cb}, code) == Some{entry} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_lookup.listed(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>, Map.to_list(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>, table), code, entry)

Every successful actual cache lookup names a real exact binding in native storage enumeration. This direction holds even before valid-tree preservation is established; it does not claim that all enumerated bindings are findable.

law removed_key_absent provedsource · line 253 · raw

@-K:Data -> @-V:Data -> @capacity:Nat -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>> -> @order:List<&2, String> -> @lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @cb:Bool -> @+code:String -> @evict:Bool -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @invariant:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/invariants.critbit(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>, table) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.remove_present(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{capacity, table, order, lifetime, counts, cb}, code, evict, entry)), code) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>}

The actual core removal, not a disconnected model of native deletion.

law cache_lookup_seeks_key provedsource · line 270 · raw

@-K:Data -> @-V:Data -> @+capacity:Nat -> @+table:Map<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>> -> @+order:List<&2, String> -> @+lifetime:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @+counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @+cb:Bool -> @+code:String -> @+entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @found:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.State{capacity, table, order, lifetime, counts, cb}, code) == Some{entry} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_insert.seek_found(Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>, Map.seek(&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>, table, code)) == Some{code} : Maybe<&2, String>}

law removal_preserves_lookup_routing provedsource · line 292 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @evict:Bool -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @invariant:lookup_routing(K, V, c) -> lookup_routing(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.remove_present(K, V, c, code, evict, entry)))

law removal_preserves_other_lookup provedsource · line 305 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+removed:String -> @+key:String -> @evict:Bool -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @invariant:lookup_routing(K, V, c) -> @distinct:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/map_delete_frame.different(key, removed) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.remove_present(K, V, c, removed, evict, entry)), key) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, c, key) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>}

law removal_preserves_storage_critbit provedsource · line 327 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @evict:Bool -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @invariant:{storage_critbit(K, V, c) == True{} : Bool} -> {storage_critbit(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.remove_present(K, V, c, code, evict, entry))) == True{} : Bool}

law store_preserves_storage_critbit provedsource · line 341 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @code:String -> @key:K -> @value:V -> @deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @flag:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> @invariant:{storage_critbit(K, V, c) == True{} : Bool} -> {storage_critbit(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.store(K, V, c, code, key, value, deadline, flag, events))) == True{} : Bool}

law store_other_lookup provedsource · line 360 · raw

@-K:Data -> @-V:Data -> @+c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+code:String -> @+key:K -> @+value:V -> @+deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @flag:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.LruEvent<K, V>> -> @+query:String -> @unequal:{String.eq(query, code) == False{} : Bool} -> @invariant:{storage_critbit(K, V, c) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.step_cache(K, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.store(K, V, c, code, key, value, deadline, flag, events)), query) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.lookup(K, V, c, query) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>}

The actual store preserves every other encoded-key lookup. Storage validity remains an input premise until full cache reachability is established.

Definitions

def binding_cons source · line 67 · raw

@-K:Data -> @-V:Data -> @item:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def bindings source · line 74 · raw

@-K:Data -> @-V:Data -> @xs:List<&2, Sigma<&2, &2, String, _ => Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

def keys_of source · line 81 · raw

@-K:Data -> @-V:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> List<&2, K>

def abstract source · line 91 · raw

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

Explicit abstraction, not the specification itself. Map validity, no stored None, and map/recency agreement must still be proved to make it faithful for every reachable nonempty state (otherwise inconsistent entries could be lost).

def observe source · line 95 · raw

@-K:Data -> @-V:Data -> @step:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Step<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

def abstract_created source · line 99 · raw

@-K:Data -> @-V:Data -> @result:Result<&2, &2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>> -> Result<&2, &2, String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>>

def abstract_reset source · line 190 · raw

@-K:Data -> @-V:Data -> @result:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics)

def lookup_routing source · line 288 · raw

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

Native deletion preserves the lookup-routing invariant through actual removal. This conditional local fact is not full reachable representation preservation.

def storage_critbit source · line 323 · raw

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

Full native storage predicate through the executed core removal. This does not assert the still-open recency/identity or reachable-state invariants.