~/bend-docscommunity

proofs/containers/dynamic_array/trace.bend checks

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

12 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/dynamic_array.bend as S
import ../../../src/containers/dynamic_array.bend as DA
import ../../../src/containers/types/dynamic_array.bend as E
import ./layout.bend as LY
import ./state.bend as ST
import ./steps.bend as SP

Definitions

def so_sh source · line 16 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.StepOK(T, sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T>

def so_obs source · line 21 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.StepOK(T, sh, op) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>

def so_step source · line 26 · raw

@-T:Data -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @-op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @so:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.StepOK(T, sh, op) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, so_sh(T, sh, op, so)), so_obs(T, sh, op, so)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

def so_good source · line 31 · raw

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

def so_spec source · line 36 · raw

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

def spec_run_cons source · line 41 · raw

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

def srun_obs source · line 46 · raw

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

def srun_state source · line 49 · raw

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

def RunOK source · line 53 · raw

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

Running ops from the array of a good shadow, with any accumulator.

def ro_sh source · line 56 · raw

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

def ro_run source · line 61 · raw

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

def ro_good source · line 66 · raw

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

def ro_model source · line 71 · raw

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

def run_ok source · line 76 · raw

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

def initial source · line 101 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T>

def new_real source · line 104 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, initial(T)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}

def new_good source · line 107 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, initial(T)) == True{} : Bool}

def new_model source · line 110 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(T, initial(T)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

def limited source · line 113 · raw

@-T:Data -> @+k:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T>

def clamp_case source · line 116 · raw

@+k:Nat -> @+b:Bool -> @+eb:{Nat.is_lt(k, 31n) == b : Bool} -> Pair({Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, b), 31n) == True{} : Bool}, {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clamp_limit(k, b) == Nat.min(k, 31n) : Nat})