~/bend-docscommunity

proofs/containers/doubly_linked_list/rm.bend checks

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

26 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 ./links.bend as LK
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 LKx
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def del_mid source · line 35 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, a) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.delete(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b) : List<&2, Nat>}

def s_in source · line 45 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool}

def s_off source · line 48 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == False{} : Bool}

def nd_rm source · line 52 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.nodupn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool}

def sub1 source · line 120 · raw

@+x:Nat -> {Nat.sub(1n+x, 1n) == x : Nat}

Templates

template s_live source · line 56 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {Bool.and(Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.live(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id))) == True{} : Bool}

template s_lt source · line 59 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool}

template fr2d source · line 64 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool}

template a_ok source · line 68 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool}

template b_ok source · line 71 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT)) == True{} : Bool}

template slots_pr source · line 75 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, pT, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.upd_first(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, pT), b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)) : List<&2, U32>}

template slots_nr source · line 78 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.upd_last(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, nT), a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)) : List<&2, U32>}

template rg_seg source · line 82 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.seg(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, pT, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0, 0) == True{} : Bool}

the unlinked list's links

template rg_fll source · line 91 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))), fl) == True{} : Bool}

template s_nf source · line 95 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), fl) == False{} : Bool}

template vslots source · line 98 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{}) : List<&2, Maybe<&2, T>>}

template rg_sl source · line 101 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.slok(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{}))) == True{} : Bool}

template rg_lv source · line 106 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{})), 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool}

template rg_fl source · line 113 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.flok(T, fl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{}))) == True{} : Bool}

template rm_raw source · line 123 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> @+owner:U32 -> @+ho:{U32.is_eq(owner, tag) == 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>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.remove(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{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)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.H{owner, id}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, pT, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)))}, Done{vv}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)}

template del_eq source · line 145 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.delete(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b) : List<&2, Nat>}

template vals_eq source · line 148 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) : List<&2, Maybe<&2, T>>}

template rm_ex source · line 152 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> @+owner:U32 -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+generation:U32 -> @+hgen:{generation == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> @+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>} -> @+hc:{U32.is_eq(generation, 4294967295) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.removed(T, tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> 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/proofs/lib/u32div.v(id), vv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.retire(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), fl, generation, U32.is_eq(generation, 4294967295))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.retire(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, pT, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), id, generation, vv, True{}))

the generation exhausted: the id is retired

template rc_fll source · line 163 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.fll(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), free), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> fl) == True{} : Bool}

template rc_good source · line 172 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> @+owner:U32 -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+generation:U32 -> @+hgen:{generation == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> @+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>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, pT, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), free), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(U32, depth, gT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), U32.inc(generation)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> fl}) == True{} : Bool}

template rm_rc source · line 186 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> @+owner:U32 -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+generation:U32 -> @+hgen:{generation == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> @+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>} -> @+hc:{U32.is_eq(generation, 4294967295) == False{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.removed(T, tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> 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/proofs/lib/u32div.v(id), vv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.retire(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), fl, generation, U32.is_eq(generation, 4294967295))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.retire(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, pT, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), id, generation, vv, False{}))

the id recycled: the next generation, the id on top of the free stack

template rm_fin source · line 204 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> @+owner:U32 -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+generation:U32 -> @+hgen:{generation == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> @+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>} -> @+c:Bool -> @+hc:{U32.is_eq(generation, 4294967295) == c : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.removed(T, tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> 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/proofs/lib/u32div.v(id), vv, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.retire(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), fl, generation, U32.is_eq(generation, 4294967295))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.retire(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0), depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), None{})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_first(depth, pT, b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.last_or(a, 0))), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/rel.tu_last(depth, nT, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/links.fst_or(b, 0)))}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), id, generation, vv, c))

template rm_ok source · line 212 · raw

@-T:Data -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+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> -> @+id:U32 -> @+b:List<&2, Nat> -> @+fl:List<&2, Nat> -> @+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} -> @+owner:U32 -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+generation:U32 -> @+hgen:{generation == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> @+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>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.remove_live(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id) <> 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)), fl}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.removed(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), id, generation, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.remove(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DL{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)}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.H{owner, id})))

THEOREM (remove): a live element with a current handle is removed