proofs/containers/doubly_linked_list/hrd.bend checks

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

21 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/array.bend as AR
import ../../lib/array_ext.bend as AX
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 ./lv.bend as LV
import ./link.bend as LN
import ./insg.bend as IG
import ./ok.bend as OK
import ../../lib/words32.bend as W32

Definitions

def lt_f source · line 26 · raw

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

def lt_t source · line 29 · raw

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

def upd_upd source · line 69 · raw

@-X:Data -> @+xs:List<&2, X> -> @+i:Nat -> @+v:X -> @+w:X -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(X, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(X, xs, i, v), i, w) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(X, xs, i, w) : List<&2, X>}

def upd_self source · line 78 · raw

@-X:Data -> @+xs:List<&2, X> -> @+i:Nat -> @+x:X -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(X, xs, i) == Some{x} : Maybe<&2, X>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(X, xs, i, x) == xs : List<&2, X>}

Templates

template i_lt 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 -> @+hlt:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(fresh)) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool}

template get_hi source · line 40 · 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 -> @+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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}, 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>)}

template get_pre source · line 43 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+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 -> @+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} -> {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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.value_result(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.get_fin(T, tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, sl), head, tail, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nT), (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id))))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}

template get_none source · line 49 · 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 -> @+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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}, 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>)}

template get_live source · line 52 · raw

@-T:Data -> @+tag:U32 -> @+cap:U32 -> @+fresh:U32 -> @+free:U32 -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+vT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+nT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+gT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+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 -> @+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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}, 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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}))

template set_hi source · line 60 · 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 -> @+x: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)) == 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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}) == (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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}, 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>)}

template set_pre source · line 63 · 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 -> @+x: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} -> {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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.unit_result(T, tag, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, gT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.set_fin(T, tag, fresh, free, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Nat, sl), head, tail, depth, cap, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, pT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(U32, nT), id, x, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), Some{x})), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, vT), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id))))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)}

template set_back source · line 88 · 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 -> @+x:T -> @+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>} -> {Array.set(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(Maybe<&2, T>, depth, vT, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id), Some{x})), id, None{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, vT) : Array<Maybe<&2, T>>}

writing None back over a vacant slot restores the block

template set_none source · line 99 · 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 -> @+x: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} -> @+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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}) == (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, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}, 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>)}

template set_live source · line 104 · 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 -> @+x: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} -> @+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}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(id)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.dispatch(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, x}))