proofs/containers/bitset/trace.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/trace.bend as Trace
10 imports
import Base import ../../lib/logic.bend as L import ../../lib/list.bend as LL import ../../lib/array.bend as A import ../../../spec/lib/common.bend as SC import ../../../src/containers/bitset.bend as B import ../../../spec/containers/bitset.bend as S import ../../../src/containers/types/bitset.bend as E import ./state.bend as ST import ./steps.bend as BS
Definitions
def srun_obs source · line 20 · raw
@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @m:List<&2, Bool> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs>
def srun_state source · line 23 · raw
@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @m:List<&2, Bool> -> List<&2, Bool>
def so_sh source · line 26 · raw
@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh
def so_obs source · line 31 · raw
@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs
def so_step source · line 36 · raw
@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(so_sh(sh, op, so)), so_obs(sh, op, so)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}
def so_good source · line 41 · raw
@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(so_sh(sh, op, so)) == True{} : Bool}
def so_spec source · line 46 · raw
@-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op) -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(so_sh(sh, op, so)), so_obs(sh, op, so)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.step(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh), op) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}
def spec_run_cons source · line 51 · raw
@+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @+rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @+m:List<&2, Bool> -> @+m1:List<&2, Bool> -> @+o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs -> @+e:{(m1, o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.step(m, op) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.run(op <> rest, m) == (srun_state(rest, m1), o <> srun_obs(rest, m1)) : Pair(List<&2, Bool>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs>)}
def RunOK source · line 56 · raw
@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs> -> Type
def ro_sh source · line 59 · raw
@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs> -> @r:RunOK(ops, sh, acc) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh
def ro_run source · line 64 · raw
@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs> -> @r:RunOK(ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.run_acc(ops, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(sh), acc)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(ro_sh(ops, sh, acc, r)), List.reverse.go(&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs, srun_obs(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh)), acc)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs>)}
def ro_good source · line 69 · raw
@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs> -> @r:RunOK(ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(ro_sh(ops, sh, acc, r)) == True{} : Bool}
def ro_model source · line 74 · raw
@-ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs> -> @r:RunOK(ops, sh, acc) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(ro_sh(ops, sh, acc, r)) == srun_state(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh)) : List<&2, Bool>}
def run_ok source · line 79 · raw
@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh) == True{} : Bool} -> RunOK(ops, sh, acc)
def run_from source · line 104 · raw
@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh0) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.run(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(sh0)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(ro_sh(ops, sh0, [], run_ok(ops, sh0, [], g0))), srun_obs(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh0))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs>)}The finished run: B.run reverses the accumulator, which is the spec's own observation list.
def TraceOK source · line 111 · raw
@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> Type
def trace_from source · line 114 · raw
@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @+sh0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+g0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh0) == True{} : Bool} -> TraceOK(ops, sh0)
def initial source · line 122 · raw
@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh
def new_real source · line 125 · raw
@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.new(n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(initial(n)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}
def new_good source · line 128 · raw
@+n:Nat -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(initial(n)) == True{} : Bool}
def new_model source · line 131 · raw
@+n:Nat -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(initial(n)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.new(n) : List<&2, Bool>}