~/bend-docscommunity

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

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

5 imports
import Base
import ../types/model.bend as T
import ./cache.bend as S
import ./clock.bend as Clock
import ./public_commands.bend as P

Types

type Trace source · line 9 · raw

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

A caller may catch a failure and issue the next command. Each result retains the partial state and exact unused provider events. No failure becomes success.

Definitions

def state source · line 12 · raw

@-K:Data -> @-V:Data -> @result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/public_commands.CmdResult<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V>

def remaining source · line 17 · raw

@-K:Data -> @-V:Data -> @result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/public_commands.CmdResult<K, V> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent>

def requests source · line 22 · raw

@-K:Data -> @-V:Data -> @result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/public_commands.CmdResult<K, V> -> Nat

def prepend source · line 27 · raw

@-K:Data -> @-V:Data -> @+result:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/public_commands.CmdResult<K, V> -> @rest:Trace<K, V> -> Trace<K, V>

Templates

template run source · line 31 · raw

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