~/bend-docscommunity

proofs/containers/doubly_linked_list/walk.bend checks

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

16 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/internal/dlist_storage.bend as R
import ./state.bend as ST
import ./rel.bend as RL
import ./link.bend as LN
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def racc source · line 30 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @back:List<&2, Nat> -> @acc:List<&2, T> -> List<&2, T>

the values of back prepended to acc, one by one

def cs_app source · line 37 · raw

@-T:Data -> @+m:Maybe<&2, T> -> @+xs:List<&2, T> -> @+acc:List<&2, T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.cons_some(T, m, xs), acc) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.cons_some(T, m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, xs, acc)) : List<&2, T>}

def ra_rapp source · line 44 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+l:List<&2, Nat> -> @+b:List<&2, Nat> -> @+acc:List<&2, T> -> {racc(T, vl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.rapp(l, b), acc) == racc(T, vl, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.values(T, vl, l), acc)) : List<&2, T>}

def step_live source · line 70 · raw

@-T:Data -> @+acc:List<&2, T> -> @+at:U32 -> @+m:Maybe<&2, T> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, m) == True{} : Bool} -> @-vals:Array<Maybe<&2, T>> -> @-prevs:Array<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.step_m(T, vals, prevs, acc, at, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.step_p(T, vals, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.cons_some(T, m, acc), Array.get(U32, prevs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.slot(at))) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.Cur<T>}

Templates

template rok source · line 22 · raw

@-T:Data -> @+pl:List<&2, U32> -> @back:List<&2, Nat> -> @+fr:Nat -> @+vl:List<&2, Maybe<&2, T>> -> Bool

every id of back is below fr and live, and its prev is the next id of back

template rok_app source · line 52 · raw

@-T:Data -> @+pl:List<&2, U32> -> @+nl:List<&2, U32> -> @+vl:List<&2, Maybe<&2, T>> -> @+l:List<&2, Nat> -> @+b:List<&2, Nat> -> @+fr:Nat -> @+p:U32 -> @+q:U32 -> @+hs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(pl, nl, l, p, q) == True{} : Bool} -> @+hl:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, l, fr, vl) == True{} : Bool} -> @+hb:{rok(T, pl, b, fr, vl) == True{} : Bool} -> @+hp:{U32.is_eq(p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)) == True{} : Bool} -> {rok(T, pl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.rapp(l, b), fr, vl) == True{} : Bool}

a linked live list, reversed onto a back list, keeps its links backwards

template wstep source · line 78 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+pp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, pT) == True{} : Bool} -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:Nat -> @+r:List<&2, Nat> -> @+acc:List<&2, T> -> @+hx:{Bool.and(Bool.and(Nat.is_lt(x, fr), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), x)), Bool.and(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(r, 0)), rok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), r, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)))) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.step_back(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.C{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(x)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.C{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.cons_some(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), x), acc), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(r, 0)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.Cur<T>}

one step: the value of x is prepended and the walk moves to x's prev

template walk source · line 92 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+pp:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(U32, d, pT) == True{} : Bool} -> @+fr:Nat -> @+hfr:{Nat.is_le(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+back:List<&2, Nat> -> @+acc:List<&2, T> -> @+hr:{rok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), back, fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.walk(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, back), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.C{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), acc, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(back, 0)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.C{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), racc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), back, acc), 0} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.Cur<T>}

THEOREM: the walk from the first id of back, for its length, prepends the values of back one by one