proofs/lib/lemmas/src/driver.bend checks

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

5 imports

import Base
import ../types/model.bend as T
import ../spec/clock.bend as Clock
import ./cache.bend as C
import ./public.bend as Pub

Types

type Outcome source · line 11 · raw

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

Deterministic model of the host clock loop over an explicit provider-event list. Only the neutral Clock.ClockEvent/Clock.Error datatypes are imported from the clock specification; no specification function is used. The adapter runs this machine through src/host.bend begin/answer (proofs/host_loop.bend).

Returned

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @answer:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/public.Answer<K, V> -> @remaining:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> Outcome<K, V>

Failed

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<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 Step source · line 23 · raw

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

One step: the provider event answering a Waiting progress either resumes the machine or stops it with the retained state and the error. drive is its iteration (drive_advance in END_TO_END.bend); src/host.bend answer uses it.

Continue

@-K:Data -> @-V:Data -> @progress:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/public.Progress<K, V> -> Step<K, V>

Stopped

@-K:Data -> @-V:Data -> @cache:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @error:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.Error -> Step<K, V>

type Trace source · line 60 · raw

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

A caller may catch a failed command and continue from the retained state.

Ran

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

Definitions

def bump source · line 15 · raw

@-K:Data -> @-V:Data -> @outcome:Outcome<K, V> -> Outcome<K, V>

def advance source · line 27 · raw

@-K:Data -> @-V:Data -> @zero_value:V -> @pending:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/public.Pending<K, V> -> @event:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent -> Step<K, V>

def drive source · line 33 · raw

@-K:Data -> @-V:Data -> @+zero_value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @progress:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/public.Progress<K, V> -> Outcome<K, V>

def cache source · line 44 · raw

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

def remaining source · line 49 · raw

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

def requests source · line 54 · raw

@-K:Data -> @-V:Data -> @outcome:Outcome<K, V> -> Nat

def prepend source · line 63 · raw

@-K:Data -> @-V:Data -> @+outcome:Outcome<K, V> -> @rest:Trace<K, V> -> Trace<K, V>

Templates

template execute source · line 41 · raw

@-K:Data -> @-encode:(@_:K -> String) -> @-V:Data -> @zero_key:K -> @+zero_value:V -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @request:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/public.Request<K, V> -> Outcome<K, V>

template run source · line 67 · raw

@-K:Data -> @-encode:(@_:K -> String) -> @-V:Data -> @requests:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/public.Request<K, V>> -> @c:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/src/cache.Cache<K, V> -> @+zero_key:K -> @+zero_value:V -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> Trace<K, V>