proofs/lib/lemmas/spec/effectful_operations.bend checks

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

6 imports

import Base
import ../types/model.bend as T
import ./cache.bend as S
import ./operations.bend as O
import ./numeric.bend as N
import ./clock.bend as Clock

Types

type Outcome source · line 11 · raw

@-K:Data -> @-V:Data -> Data

Independent Add/refresh clock effects, including the state committed before a failed request. No implementation or proof import and no successful-transport premise occurs here. Public marshalling and host composition remain separate.

Returned

@-K:Data -> @-V:Data -> @observation:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @remaining:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> Outcome<K, V>

Failed

@-K:Data -> @-V:Data -> @state:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @error:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.Error -> @remaining:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> Outcome<K, V>

type PreparedAdd source · line 15 · raw

@-K:Data -> @-V:Data -> Data

Prepared

@-K:Data -> @-V:Data -> @state:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @original:K -> @evicted:Bool -> PreparedAdd<K, V>

Templates

template evicted source · line 18 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @old:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> PreparedAdd<K, V>

template evict_found source · line 23 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @old:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> PreparedAdd<K, V>

template evict_first source · line 28 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @order:List<&2, K> -> PreparedAdd<K, V>

template room source · line 33 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @order:List<&2, K> -> @full:Bool -> PreparedAdd<K, V>

template absent_add source · line 38 · raw

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

template prepare_found source · line 42 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> PreparedAdd<K, V>

template prepare_add source · line 47 · raw

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

template sampled_add source · line 51 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @prepared:PreparedAdd<K, V> -> @value:V -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @reply:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.Reply -> Outcome<K, V>

template immortal_add source · line 57 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @prepared:PreparedAdd<K, V> -> @value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> Outcome<K, V>

template add_lifetime source · line 61 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @prepared:PreparedAdd<K, V> -> @value:V -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @immortal:Bool -> Outcome<K, V>

template add_with_lifetime source · line 66 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @value:V -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> Outcome<K, V>

template add source · line 70 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> Outcome<K, V>

template refresh_deadline source · line 76 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @+deadline:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V>

Refresh has already moved recency and counted the hit when its clock is read. Updating the deadline must not count that hit a second time.

template sampled_refresh source · line 81 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @prepared:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @reply:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.Reply -> Outcome<K, V>

template refresh_lifetime source · line 86 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @prepared:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @immortal:Bool -> Outcome<K, V>

template refresh_hit source · line 91 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> Outcome<K, V>

template refresh_found source · line 96 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Outcome<K, V>

template refresh source · line 101 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> Outcome<K, V>

template sampled_read source · line 107 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @tracked:Bool -> @reply:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.Reply -> Outcome<K, V>

Get/Peek/Contains sample only for a present finite deadline. Their state is unchanged if the request fails; hit/miss accounting occurs after that point.

template read_lifetime source · line 112 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @tracked:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @immortal:Bool -> Outcome<K, V>

template read_found source · line 117 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @key:K -> @tracked:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> Outcome<K, V>

template read source · line 122 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @+key:K -> @tracked:Bool -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> Outcome<K, V>