~/bend-docscommunity

proofs/containers/dynamic_array/walk.bend checks

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

10 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/dynamic_array.bend as DA
import ./layout.bend as LY
import ./state.bend as ST

Definitions

def unwrap source · line 18 · raw

@-T:Data -> @m:Maybe<&2, Maybe<&2, T>> -> Maybe<&2, T>

def slot source · line 26 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+j:Nat -> Maybe<&2, T>

the content of slot j

def nth_slot source · line 29 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, xs, j) == Some{slot(T, xs, j)} : Maybe<&2, Maybe<&2, T>>}

def get_slot source · line 38 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+j:Nat -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, t) == True{} : Bool} -> {Array.get(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t), U32.from_nat(j)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t), slot(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), j)) : Pair(Array<Maybe<&2, T>>, Maybe<&2, T>)}

def tvals source · line 49 · raw

@k:Nat -> @-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @acc:List<&2, T> -> List<&2, T>

def dec1_le source · line 56 · raw

@+m:Nat -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.dec1(m), m) == True{} : Bool}

def tl_thaw source · line 63 · raw

@k:Nat -> @-T:Data -> @+l:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @acc:List<&2, T> -> @+hd:{Nat.is_le(d, l) == True{} : Bool} -> @+hl:{Nat.is_le(l, 31n) == True{} : Bool} -> @+hb:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.dec1(k), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.tl_go(k, T, acc, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t), slot(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.dec1(k)))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t), tvals(k, T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), acc)) : Pair(Array<Maybe<&2, T>>, List<&2, T>)}

def take_all source · line 75 · raw

@-T:Data -> @+ys:List<&2, T> -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, ys) == n : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(T, ys, n) == ys : List<&2, T>}

def take_cons_some source · line 86 · raw

@-T:Data -> @+ys:List<&2, T> -> @+m:Nat -> @+acc:List<&2, T> -> @+hm:{Nat.is_lt(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, ys)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(T, ys, m), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.cons_some(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, ys, m), acc)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(T, ys, 1n+m), acc) : List<&2, T>}

def slot_nth source · line 96 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, xs, n) == True{} : Bool} -> @+hm:{Nat.is_lt(m, n) == True{} : Bool} -> {slot(T, xs, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, xs), m) : Maybe<&2, T>}

def tvals_take source · line 100 · raw

@k:Nat -> @-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+acc:List<&2, T> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, xs, n) == True{} : Bool} -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> {tvals(k, T, xs, acc) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, xs), k), acc) : List<&2, T>}

def tvals_model source · line 113 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, xs, n) == True{} : Bool} -> {tvals(n, T, xs, []) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.somes(T, xs) : List<&2, T>}