~/bend-docscommunity

proofs/containers/doubly_linked_list/insp.bend checks

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

25 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/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/internal_dlist.bend as I
import ../../../src/containers/types/doubly_linked_list.bend as E
import ./state.bend as ST
import ./rel.bend as RL
import ./vals.bend as VA
import ./lv.bend as LV
import ./link.bend as LN
import ./insg.bend as IG
import ./ok.bend as OK
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 placeAB source · line 32 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T> -> @+n:Nat -> @x:T -> @a:List<&2, Nat> -> @b:List<&2, Nat> -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle)

the specification's insertion at the allocated id, between a and b

def insAB source · line 37 · raw

@-T:Data -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, Nat) -> @x:T -> @a:List<&2, Nat> -> @b:List<&2, Nat> -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle)

def u_ne_c source · line 44 · raw

@+a:U32 -> @+b:U32 -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b)) == False{} : Bool} -> @+c:Bool -> @+hc:{U32.is_eq(a, b) == c : Bool} -> {c == False{} : Bool}

def u_ne source · line 52 · raw

@+a:U32 -> @+b:U32 -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b)) == False{} : Bool} -> {U32.is_eq(a, b) == False{} : Bool}

def u_eqv source · line 55 · raw

@+a:U32 -> @+b:U32 -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(b) : Nat} -> {U32.is_eq(a, b) == True{} : Bool}

Templates

template pop_raw source · line 60 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+f0:Nat -> @+fl2:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(f0), head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), f0 <> fl2) == True{} : Bool} -> @+x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.insert_between_free(T, tag, fresh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(f0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), head, tail, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fresh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(fl2, 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, f0 <> b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, f0 <> b), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, f0 <> b), 0), depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, f0, Some{x})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, depth, pT, f0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)), b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(f0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, depth, nT, f0, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)), a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(f0)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.H{tag, U32.from_nat(f0)}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)}

the storage pop: the top of the free stack is linked in

template ins_pop source · line 83 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+f0:Nat -> @+fl2:List<&2, Nat> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(f0), head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), f0 <> fl2) == True{} : Bool} -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle, insAB(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.alloc(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)), f0 <> fl2}), x, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.inserted(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.insert_between_free(T, tag, fresh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(f0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), head, tail, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0), x)))

THEOREM (insert, a free id): the top of the free stack takes the element