proofs/containers/bitlist/da.bend checks

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

12 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/dynamic_array.bend as D
import ../../../src/containers/types/dynamic_array.bend as DE
import ../../../spec/containers/dynamic_array.bend as DS
import ../dynamic_array/layout.bend as LY
import ../dynamic_array/state.bend as DAS
import ../dynamic_array/steps.bend as DSP
import ../dynamic_array/trace.bend as DTR

Definitions

def items source · line 23 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> List<&2, U32>

def mlim source · line 28 · raw

@m:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> Nat

def ws source · line 34 · raw

@w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> List<&2, U32>

The stored words and the depth limit of a shadow.

def lim source · line 37 · raw

@w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> Nat

def unitem source · line 40 · raw

@o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>

def ununit source · line 51 · raw

@o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>

def unnat source · line 62 · raw

@o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> Nat

def uitem source · line 73 · raw

@p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>)

def uunit source · line 77 · raw

@p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

def unat source · line 81 · raw

@p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)

def uitem_obs source · line 85 · raw

@r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>) -> {uitem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.obs_item(U32, r)) == r : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>)}

def uunit_obs source · line 90 · raw

@r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> {uunit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.obs_unit(U32, r)) == r : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

def unat_obs source · line 95 · raw

@r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat) -> {unat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.obs_nat(U32, r)) == r : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)}

def p_items source · line 102 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @e:{(a, o) == (b, o2) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)} -> {items(a) == items(b) : List<&2, U32>}

def p_lim source · line 105 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @e:{(a, o) == (b, o2) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)} -> {mlim(a) == mlim(b) : Nat}

def p_item source · line 108 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @e:{(a, o) == (b, o2) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)} -> {unitem(o) == unitem(o2) : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>}

def p_unit source · line 111 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @e:{(a, o) == (b, o2) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)} -> {ununit(o) == ununit(o2) : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>}

def p_nat source · line 114 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32> -> @o2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32> -> @e:{(a, o) == (b, o2) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)} -> {unnat(o) == unnat(o2) : Nat}

def ws_len source · line 119 · raw

@+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, U32>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) == n : Nat}

def ws_cap source · line 123 · raw

@+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, U32>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}))) == True{} : Bool}

at most 2^lim words

def wcap source · line 127 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == True{} : Bool}

def gsh source · line 134 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32>

def get_eq source · line 137 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.get(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, w), q) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, gsh(w, g, q)), unitem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{q}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{q}, g)))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>)}

def get_good source · line 142 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, gsh(w, g, q)) == True{} : Bool}

def get_all source · line 145 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, gsh(w, g, q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{q}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{q}, g))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OItem{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.item_result(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, ws(w), q))}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def get_val source · line 150 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> {unitem(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{q}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Get{q}, g))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.item_result(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, ws(w), q)) : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>}

def get_ws source · line 153 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> {ws(gsh(w, g, q)) == ws(w) : List<&2, U32>}

def get_lim source · line 156 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> {lim(gsh(w, g, q)) == lim(w) : Nat}

def lsh source · line 161 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32>

def len_eq source · line 164 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, w)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, lsh(w, g)), unnat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Length{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Length{}, g)))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)}

def len_good source · line 169 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, lsh(w, g)) == True{} : Bool}

def len_all source · line 172 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, lsh(w, g)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Length{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Length{}, g))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.ONat{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w))}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def len_val source · line 177 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {unnat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Length{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Length{}, g))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)) : Nat}

def len_ws source · line 180 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {ws(lsh(w, g)) == ws(w) : List<&2, U32>}

def len_lim source · line 183 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {lim(lsh(w, g)) == lim(w) : Nat}

def dep source · line 186 · raw

@w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> Nat

def sp_set source · line 193 · raw

@+l:Nat -> @+d:Nat -> @+xs:List<&2, U32> -> @+q:Nat -> @+v:U32 -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step_parts(U32, l, d, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{q, v}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, xs, q, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def ssh source · line 197 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> @+v:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32>

def set_eq source · line 200 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, w), q, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, ssh(w, g, q, v)), ununit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{q, v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{q, v}, g)))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

def set_good source · line 205 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, ssh(w, g, q, v)) == True{} : Bool}

def set_all source · line 208 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> @+v:U32 -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w))) == True{} : Bool} -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, ssh(w, g, q, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{q, v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{q, v}, g))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{lim(w), dep(w), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ws(w), q, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def set_val source · line 214 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> @+v:U32 -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w))) == True{} : Bool} -> {ununit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{q, v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Set{q, v}, g))) == Done{Unit{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>}

def set_ws source · line 217 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> @+v:U32 -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w))) == True{} : Bool} -> {ws(ssh(w, g, q, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, ws(w), q, v) : List<&2, U32>}

def set_lim source · line 220 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+q:Nat -> @+v:U32 -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w))) == True{} : Bool} -> {lim(ssh(w, g, q, v)) == lim(w) : Nat}

def sp_push_c source · line 227 · raw

@+l:Nat -> @+d:Nat -> @+xs:List<&2, U32> -> @+v:U32 -> @c:Bool -> @+ec:{Nat.is_lt(d, l) == c : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == True{} : Bool} -> @+e1:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == False{} : Bool} -> {Bool.pick(Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>), Nat.is_lt(d, l), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, xs, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.ok_unit}), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}}})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, xs, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

below the depth limit a push succeeds (in place, or after one doubling)

def sp_push_b source · line 236 · raw

@+l:Nat -> @+d:Nat -> @+xs:List<&2, U32> -> @+v:U32 -> @b:Bool -> @+eb:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == b : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step_parts(U32, l, d, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, Bool.pick(Nat, Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)), d, 1n+d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, xs, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def sp_full_c source · line 246 · raw

@+l:Nat -> @+d:Nat -> @+xs:List<&2, U32> -> @+v:U32 -> @c:Bool -> @+ec:{Nat.is_lt(d, l) == c : Bool} -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == False{} : Bool} -> {Bool.pick(Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>), Nat.is_lt(d, l), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, 1n+d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, xs, v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.ok_unit}), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}}})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

at the depth limit with every slot used a push is rejected

def sp_full source · line 254 · raw

@+l:Nat -> @+d:Nat -> @+xs:List<&2, U32> -> @+v:U32 -> @+hc:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step_parts(U32, l, d, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{l, d, xs}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def psh source · line 259 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32>

def push_eq source · line 262 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, w), v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, psh(w, g, v)), ununit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, g)))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)}

def push_good source · line 267 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, psh(w, g, v)) == True{} : Bool}

def push_all source · line 271 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == True{} : Bool} -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, psh(w, g, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, g))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{lim(w), Bool.pick(Nat, Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(dep(w))), dep(w), 1n+dep(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, ws(w), v)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def push_val source · line 277 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == True{} : Bool} -> {ununit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, g))) == Done{Unit{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>}

def push_ws source · line 280 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == True{} : Bool} -> {ws(psh(w, g, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, ws(w), v) : List<&2, U32>}

def push_lim source · line 283 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == True{} : Bool} -> {lim(psh(w, g, v)) == lim(w) : Nat}

def full_all source · line 286 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == False{} : Bool} -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, psh(w, g, v)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, g))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{lim(w), dep(w), ws(w)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def full_val source · line 293 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == False{} : Bool} -> {ununit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Push{v}, g))) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>}

def full_ws source · line 296 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == False{} : Bool} -> {ws(psh(w, g, v)) == ws(w) : List<&2, U32>}

def full_lim source · line 299 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+v:U32 -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, ws(w)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(lim(w))) == False{} : Bool} -> {lim(psh(w, g, v)) == lim(w) : Nat}

def csh source · line 304 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32>

def clear_eq source · line 307 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, w)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, csh(w, g)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>}

def clear_good source · line 310 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, csh(w, g)) == True{} : Bool}

def clear_all source · line 313 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.model(U32, csh(w, g)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/trace.so_obs(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Clear{}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/steps.step_ok(U32, w, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Clear{}, g))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.M{lim(w), dep(w), []}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.OUnit{Done{Unit{}}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

def clear_ws source · line 318 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {ws(csh(w, g)) == [] : List<&2, U32>}

def clear_lim source · line 321 · raw

@+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> {lim(csh(w, g)) == lim(w) : Nat}