~/bend-docscommunity

proofs/containers/doubly_linked_list/link.bend checks

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

16 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
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 ../../../src/containers/types/internal_dlist.bend as I
import ./rel.bend as RL
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/u32_tree.bend as UT

Definitions

def nth_val source · line 23 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, vl, i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vl, i)} : Maybe<&2, Maybe<&2, T>>}

def vget source · line 33 · raw

@-T:Data -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Array.get(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i))) : Pair(Array<Maybe<&2, T>>, Maybe<&2, T>)}

def vset source · line 36 · raw

@-T:Data -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:Maybe<&2, T> -> {Array.set(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), i, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)) : Array<Maybe<&2, T>>}

def vswap source · line 39 · raw

@-T:Data -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, vT) == True{} : Bool} -> @+i:U32 -> @+hi:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+x:Maybe<&2, T> -> {Array.swap(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), i, x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, d, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), x)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i))) : Pair(Array<Maybe<&2, T>>, Maybe<&2, T>)}

def fn_v source · line 44 · raw

@+nn:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hn:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.from_nat(nn)) == nn : Nat}

def fn_lt source · line 47 · raw

@+nn:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hn:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(U32.from_nat(nn)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

def fn_of source · line 51 · raw

@+i:U32 -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+h:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(i)) == i : U32}

a U32 below 2^k is the U32 of its value

def slot_fn source · line 55 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+nn:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+hn:{Nat.is_lt(nn, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.slot(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(nn)) == U32.from_nat(nn) : U32}

the slot of an id's link is the id's U32

def pick_f source · line 60 · raw

@+c:Bool -> @+h:{c == False{} : Bool} -> @+x:U32 -> @+y:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.pick_end(c, x, y) == y : U32}

def hd_in source · line 65 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+head:U32 -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.pick_end(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(n), head) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, n <> b), 0) : U32}

the head after linking n between a and b

def tl_in source · line 75 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> @+tail:U32 -> @+ht:{U32.is_eq(tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0)) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.pick_end(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(n), tail) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, n <> b), 0) : U32}

the tail after linking n between a and b

def hd_rm source · line 84 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+head:U32 -> @+hh:{U32.is_eq(head, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.lastlt(a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.pick_end(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), head) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0) : U32}

the head after unlinking s from between a and b

def tl_rm source · line 94 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:Nat -> @+hd:{Nat.is_lt(d, 30n) == True{} : Bool} -> @+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+tail:U32 -> @+ht:{U32.is_eq(tail, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), 0)) == True{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.fstlt(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.pick_end(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), tail) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0) : U32}

the tail after unlinking s from between a and b

def len_mid source · line 104 · raw

@+a:List<&2, Nat> -> @+n:Nat -> @+b:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, n <> b)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) : Nat}

def dl_eq source · line 113 · raw

@-T:Data -> @+tag:U32 -> @+fr:U32 -> @+fe:U32 -> @+c1:Nat -> @+c2:Nat -> @+h1:U32 -> @+h2:U32 -> @+t1:U32 -> @+t2:U32 -> @+d:Nat -> @+cap:U32 -> @-v1:Array<Maybe<&2, T>> -> @+v2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @-p1:Array<U32> -> @+p2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @-n1:Array<U32> -> @+n2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+ec:{c1 == c2 : Nat} -> @+eh:{h1 == h2 : U32} -> @+et:{t1 == t2 : U32} -> @+ev:{v1 == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, v2) : Array<Maybe<&2, T>>} -> @+ep:{p1 == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, p2) : Array<U32>} -> @+en:{n1 == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, n2) : Array<U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fr, fe, c1, h1, t1, d, cap, v1, p1, n1} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fr, fe, c2, h2, t2, d, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, v2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, p2), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, n2)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T>}

Templates