~/bend-docscommunity

proofs/containers/bitlist/trace.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/trace.bend as Trace

10 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitlist.bend as BLI
import ../../../src/containers/types/bitlist.bend as E
import ../dynamic_array/trace.bend as DTR
import ../../../spec/containers/bitlist.bend as S
import ./state.bend as SS
import ./steps.bend as BS

Definitions

def srun_obs source · line 18 · raw

@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>

def srun_state source · line 21 · raw

@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model

def so_sh source · line 24 · raw

@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/steps.StepOK(sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh

def so_obs source · line 29 · raw

@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/steps.StepOK(sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs

def so_step source · line 34 · raw

@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/steps.StepOK(sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(so_sh(sh, op, so)), so_obs(sh, op, so)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)}

def so_good source · line 39 · raw

@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/steps.StepOK(sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(so_sh(sh, op, so)) == True{} : Bool}

def so_spec source · line 44 · raw

@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/steps.StepOK(sh, op) -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(so_sh(sh, op, so)), so_obs(sh, op, so)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(sh), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)}

def spec_run_cons source · line 49 · raw

@+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @+m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model -> @+m1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model -> @+o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs -> @+e:{(m1, o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.step(m, op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.run(op <> rest, m) == (srun_state(rest, m1), o <> srun_obs(rest, m1)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>)}

def RunOK source · line 54 · raw

@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs> -> Type

def ro_sh source · line 57 · raw

@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs> -> @r:RunOK(ops, sh, acc) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh

def ro_run source · line 62 · raw

@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs> -> @r:RunOK(ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.run_acc(ops, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(sh), acc)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(ro_sh(ops, sh, acc, r)), List.reverse.go(&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs, srun_obs(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(sh)), acc)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>)}

def ro_good source · line 67 · raw

@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs> -> @r:RunOK(ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(ro_sh(ops, sh, acc, r)) == True{} : Bool}

def ro_model source · line 72 · raw

@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs> -> @r:RunOK(ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(ro_sh(ops, sh, acc, r)) == srun_state(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(sh)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

def run_ok source · line 77 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @+acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(sh) == True{} : Bool} -> RunOK(ops, sh, acc)

def run_from source · line 100 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(sh0) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.run(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(sh0)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(ro_sh(ops, sh0, [], run_ok(ops, sh0, [], g0))), srun_obs(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(sh0))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>)}

def TraceOK source · line 107 · raw

@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> Type

def trace_from source · line 110 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(sh0) == True{} : Bool} -> TraceOK(ops, sh0)

def initial source · line 118 · raw

@+l:Maybe<&2, Nat> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh

def new_real source · line 121 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.new == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(initial(None{})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist}

def with_limit_real source · line 124 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.with_limit(n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(initial(Some{n})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist}

def initial_good source · line 127 · raw

@+l:Maybe<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(initial(l)) == True{} : Bool}

def new_model source · line 130 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(initial(None{})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.new : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

def with_limit_model source · line 133 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(initial(Some{n})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.with_limit(n) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

def fpush source · line 138 · raw

@p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.from_push(p) == Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.obs_unit(p)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist}

def FromOK source · line 143 · raw

@bs:List<&2, Bool> -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> Type

def from_lift source · line 146 · raw

@+b:Bool -> @+t:List<&2, Bool> -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @+sh1:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @+e1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.from_push(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.push(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(sh), b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(sh1) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist} -> @+m1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(sh1) == Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Push{b})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model} -> @ih:FromOK(t, sh1) -> FromOK(b <> t, sh)

def from_ok source · line 154 · raw

@+bs:List<&2, Bool> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.Sh -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.good(sh) == True{} : Bool} -> FromOK(bs, sh)

def from_bools_ok source · line 165 · raw

@+bs:List<&2, Bool> -> FromOK(bs, initial(None{}))