proofs/containers/doubly_linked_list/valid.bend checks

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

19 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/doubly_linked_list.bend as E
import ./state.bend as ST
import ./rel.bend as RL
import ./vals.bend as VA
import ./ok.bend as OK
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT

Definitions

def lg_false source · line 65 · raw

@-T:Data -> @+m:Maybe<&2, T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_gen(T, m, False{}) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>}

Templates

template iv_foreign 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hc:{U32.is_eq(tag, owner) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}) == (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, sl, fl}), Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>)}

template iv_cap source · line 32 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hc:{U32.is_eq(tag, owner) == True{} : Bool} -> @+hcap:{U32.is_lt(id, cap) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}) == (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, sl, fl}), Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>)}

template iv_gen source · line 35 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hc:{U32.is_eq(tag, owner) == True{} : Bool} -> @+hcap:{U32.is_lt(id, cap) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.generation_error(U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), g))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>)}

template len_vlf source · line 45 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(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(fresh) : Nat}

template sv_foreign source · line 50 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hc:{U32.is_eq(owner, tag) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>}

template sv_hi source · line 53 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hc:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>}

template sv_lo source · line 59 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hc:{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} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_gen(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), g)) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>}

template v_close source · line 76 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error -> @+he:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, e) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, e) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+er:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, e)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)} -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, e)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<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.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

both sides fail with e

template v_val source · line 82 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+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} -> @+hgt:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), g) == True{} : Bool} -> @+er0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})) == 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, sl, fl}), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)} -> @+es0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.live_gen(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), True{}) : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @stale_none:(@+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} -> @+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)) == None{} : Maybe<&2, T>} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @live:(@+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>} -> @+hgen:{g == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> 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, sl, fl}), op, 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, sl, fl}), op))) -> @+m:Maybe<&2, T> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) == m : 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.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

the value slot, the generation current

template v_go source · line 93 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hgt:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), g) == True{} : Bool} -> @+er0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})) == 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, sl, fl}), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)} -> @stale_hi:(@+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == False{} : Bool} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @stale_none:(@+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} -> @+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)) == None{} : Maybe<&2, T>} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @live:(@+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>} -> @+hgen:{g == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> 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, sl, fl}), op, 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, sl, fl}), op))) -> @+c:Bool -> @+hc:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == 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.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

the generation current: the storage decides

template v_genf source · line 102 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hgf:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), g) == False{} : Bool} -> @+er:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)} -> @+c:Bool -> @+hc:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == 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.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

the generation stale: both reject

template v_gen source · line 110 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hc1:{U32.is_eq(tag, owner) == True{} : Bool} -> @+hcap:{U32.is_lt(id, cap) == True{} : Bool} -> @stale_hi:(@+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == False{} : Bool} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @stale_none:(@+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} -> @+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)) == None{} : Maybe<&2, T>} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @live:(@+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>} -> @+hgen:{g == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> 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, sl, fl}), op, 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, sl, fl}), op))) -> @+c:Bool -> @+hc:{U32.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), g) == 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.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

template cap_hi source · line 120 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+hcap:{U32.is_lt(id, cap) == False{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == False{} : Bool}

the id at or above the capacity is above every issued id

template v_cap source · line 124 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hc1:{U32.is_eq(tag, owner) == True{} : Bool} -> @stale_hi:(@+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == False{} : Bool} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @stale_none:(@+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} -> @+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)) == None{} : Maybe<&2, T>} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @live:(@+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>} -> @+hgen:{g == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> 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, sl, fl}), op, 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, sl, fl}), op))) -> @+c:Bool -> @+hc:{U32.is_lt(id, cap) == 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.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

template v_own source · line 131 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @stale_hi:(@+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == False{} : Bool} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @stale_none:(@+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} -> @+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)) == None{} : Maybe<&2, T>} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @live:(@+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>} -> @+hgen:{g == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> 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, sl, fl}), op, 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, sl, fl}), op))) -> @+c:Bool -> @+hc:{U32.is_eq(tag, owner) == 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.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

template vstep source · line 143 · 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> -> @+sl: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, sl, fl) == True{} : Bool} -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+hfF:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ForeignHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @+hfS:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>} -> @stale_hi:(@+ho:{U32.is_eq(owner, tag) == True{} : Bool} -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == False{} : Bool} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @stale_none:(@+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} -> @+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)) == None{} : Maybe<&2, T>} -> {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, sl, fl}), op) == (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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.failed(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.StaleHandle{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}) -> @live:(@+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>} -> @+hgen:{g == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)) : U32} -> 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, sl, fl}), op, 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, sl, fl}), op))) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/ok.POK(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.checked(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, sl, fl}), op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, op, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.validate(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, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g})))

THEOREM (validation): an operation on a handle refines the specification's when its storage part does, on a live element with a current handle, and fails as the specification's otherwise