~/bend-docscommunity

proofs/lib/lemmas/proofs/extensional_states.bend checks

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

6 imports
import Base
import ../spec/cache.bend as S
import ../spec/operations.bend as O
import ../spec/equivalence.bend as E
import ../types/model.bend as T
import ./spec_lookup.bend as Lookup

Definitions

def string_reflexive source · line 17 · raw

@-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, s, s)

def string_symmetric source · line 20 · raw

@-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, b, a)

def string_transitive source · line 23 · raw

@-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @first:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, a, b) -> @second:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, b, c) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, a, c)

def with_life source · line 28 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.Canonical<K, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.Canonical<K, V>

Configuration updates preserve the finite-map relation without assuming any agreement between the two binding-list enumeration orders.

def recency_length source · line 32 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.Canonical<K, V> -> Nat

def string_set_lifetime source · line 46 · raw

@-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.set_lifetime(String, V, a, ns), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.set_lifetime(String, V, b, ns))

def string_length source · line 49 · raw

@-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<String, V> -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, a, b) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.length(String, V, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.length(String, V, b) : Nat}

def string_observation_reflexive source · line 56 · raw

@-V:Data -> @result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<String, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, result, result)

def miss_counts source · line 59 · raw

@counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> @tracked:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics

def with_counts source · line 65 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.Canonical<K, V> -> @counts:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.Canonical<K, V>

def counts_of source · line 69 · raw

@-K:Data -> @-V:Data -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.Canonical<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Metrics

def string_expired_result source · line 86 · raw

@-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<String, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<String, V> -> @tracked:Bool -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/proofs/spec_lookup.string_same, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/operations.expired_result(String, V, a, tracked), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/operations.expired_result(String, V, b, tracked))

Templates

template reflexive source · line 8 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, s, s)

template symmetric source · line 11 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, b, a)

template transitive source · line 14 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @first:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, a, b) -> @second:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, b, c) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, a, c)

template set_lifetime source · line 36 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @+ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.set_lifetime(K, V, a, ns), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.set_lifetime(K, V, b, ns))

template length source · line 41 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, a, b) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.length(K, V, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.length(K, V, b) : Nat}

template observation_reflexive source · line 52 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(K, same, V, result, result)

template count_miss source · line 73 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @+tracked:Bool -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.states(K, same, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/operations.count_miss(K, V, a, tracked), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/operations.count_miss(K, V, b, tracked))

template expired_result source · line 80 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @tracked:Bool -> @proof:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(K, same, V, a, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(K, same, V, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/operations.expired_result(K, V, a, tracked), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/operations.expired_result(K, V, b, tracked))

template from_equal source · line 89 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @equal:{a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(K, same, V, a, b)

template observation_transitive source · line 93 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @first:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(K, same, V, a, b) -> @second:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(K, same, V, b, c) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/equivalence.observations(K, same, V, a, c)