~/bend-docscommunity

proofs/containers/doubly_linked_list/hins.bend checks

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

23 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
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/doubly_linked_list.bend as E
import ./state.bend as ST
import ./rel.bend as RL
import ./link.bend as LN
import ./ok.bend as OK
import ./insp.bend as IP
import ./ins.bend as IN
import ./hrd.bend as HR
import ./hnb.bend as NB
import ./hlive.bend as HL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Templates

template rel_read source · line 29 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free: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> -> @+fl:List<&2, Nat> -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == True{} : Bool} -> @+vv:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) == Some{vv} : Maybe<&2, T>} -> @+x:T -> @+af:Bool -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.relative_result(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.insert_checked_reuse(T, af, U32.is_lt(id, fresh), tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> 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), id, x, U32.is_eq(owner, tag))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.relative_result(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.ins_live2_reuse(T, af, tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b)), head, tail, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), id, x, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}

the neighbours read for a relative insertion

template lnk_id source · line 38 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free: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> -> @+fl:List<&2, Nat> -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.link(id) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32}

template ib_ab source · line 43 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free: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> -> @+fl:List<&2, Nat> -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == True{} : Bool} -> @+vv:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) == Some{vv} : Maybe<&2, T>} -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_op(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.dispatch(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}))

template ia_ab source · line 52 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free: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> -> @+fl:List<&2, Nat> -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.goodF(T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl) == True{} : Bool} -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+cz:Nat -> @+hcz:{cz == 29n : Nat} -> @+hroom:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(cz)) == True{} : Bool} -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == True{} : Bool} -> @+vv:T -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) == Some{vv} : Maybe<&2, T>} -> @+x:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_op(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.model(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.dispatch(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}))