~/bend-docscommunity

proofs/containers/doubly_linked_list/hlive.bend source

proofs/containers/doubly_linked_list/hlive.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../lib/list.bend as LLimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/doubly_linked_list.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/containers/doubly_linked_list.bend as Dimport ../../../src/containers/internal/dlist_storage.bend as Rimport ../../../src/containers/types/internal_dlist.bend as Iimport ../../../src/containers/types/doubly_linked_list.bend as Eimport ./state.bend as STimport ./rel.bend as RLimport ./vals.bend as VAimport ./link.bend as LNimport ./ok.bend as OKimport ./insp.bend as IPimport ./rm.bend as RMimport ./hrd.bend as HRimport ./hnb.bend as NBimport ../../lib/nat_list.bend as NLimport ../../lib/words32.bend as W32# The live element, split out of its list: next, prev, remove, and the# insertions before and after it; and the storage's stale answers for# remove and the insertions.# ---- splitting the list at the live element ----def mem_of(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}) -> {NL.memn(UD.v(id), sl) == True{} : Bool}:  VA.lvin_elim(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl, ST.g_clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), UD.v(id), RL.by_eq(ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}, Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv), {==}))def ws_go(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +op: E.Op<T>, sp: NL.Split(UD.v(id), sl), k: @+a: List<&2, Nat> -> @+b: List<&2, Nat> -> @+hg2: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool} -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op))) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)):  match sp:    case Tuple{+a, Tuple{+b, e}}:      +e2 = {e : {sl == SC.append(Nat, a, Con{UD.v(id), b}) : List<&2, Nat>}}      +hg2 = L.subst(List<&2, Nat>, z => {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl) == True{} : Bool}, sl, SC.append(Nat, a, Con{UD.v(id), b}), e2, hg)      r = k(a, b, hg2)      L.subst(List<&2, Nat>, z => OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl}), op)), SC.append(Nat, a, Con{UD.v(id), b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{UD.v(id), b}), e2), r)def with_split(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +op: E.Op<T>, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, k: @+a: List<&2, Nat> -> @+b: List<&2, Nat> -> @+hg2: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool} -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op))) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)):  ws_go(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, NL.split_mem(UD.v(id), sl, mem_of(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, vv, hv)), k)def next_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}})):  with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Next{E.H{owner, id, g}}, vv, hv, a => b => hg2 => NB.nx_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, ho, hlt, vv, hv))def prev_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}})):  with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Prev{E.H{owner, id, g}}, vv, hv, a => b => hg2 => NB.pv_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, ho, hlt, vv, hv))def rm_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}})):  with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Remove{E.H{owner, id, g}}, vv, hv, a => b => hg2 => RM.rm_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg2, owner, ho, g, hgen, vv, hv))# ---- remove: the storage's stale answers ----def rm_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.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(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, HR.lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, z)), U32.is_eq(owner, tag), True{}, ho))def rm_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.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(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}:  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, HR.lt_t(id, fresh, hlt))  +e2 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, z)), U32.is_eq(owner, tag), True{}, ho)  +e3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, D.DList<T> & E.Obs<T>, r => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, r)), Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), LN.vget(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt)))  +e4 = Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv)  Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, True{})), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e2, Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e3, e4)))# ---- insert before / after ----def ins_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, HR.lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, z)), U32.is_eq(owner, tag), True{}, ho))def ins_pre(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))) == D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))) : D.DList<T> & E.Obs<T>}:  +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, HR.lt_t(id, fresh, hlt))  +e2 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, z)), U32.is_eq(owner, tag), True{}, ho)  +e3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, D.DList<T> & E.Obs<T>, r => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, r)), Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), LN.vget(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt)))  Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, True{})), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e2, e3))def ins_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:  Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}), ins_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, af, ho, hlt), Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv))# the relative insertion's result is the insertion'sdef rel_done(~T: Data, +tag: U32, +depth: Nat, +cap: U32, -gens: Array<U32>, r: R.DList<T> & I.Handle) -> {D.relative_result(~T, tag, depth, cap, gens, R.done_handle(~T, r)) == D.relative_done(~T, D.inserted(~T, tag, depth, cap, gens, r)) : D.DList<T> & E.Obs<T>}:  match r:    case Tuple{raw, I.H{o, +i}}:      {==}# a handle result mapped to an observationdef pok_ins(~T: Data, -sp: S.DS<T> & E.Handle, -rr: D.DList<T> & E.Handle, p: OK.POK(~T, E.Handle, sp, rr)) -> OK.POK(~T, E.Obs<T>, S.ins_obs(T, sp), D.relative_done(~T, rr)):  match p:    case Tuple{+sh2, Tuple{+o, Tuple{+er, Tuple{+es, hg2}}}}:      (sh2, (E.OInsert{Done{o}}, (Equal.cong(D.DList<T> & E.Handle, D.DList<T> & E.Obs<T>, r => D.relative_done(~T, r), rr, (ST.real(~T, sh2), o), er), (Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.ins_obs(T, r), sp, (ST.model(~T, sh2), o), es), hg2))))def pok_push(~T: Data, -sp: S.DS<T> & E.Handle, -rr: D.DList<T> & E.Handle, p: OK.POK(~T, E.Handle, sp, rr)) -> OK.POK(~T, E.Obs<T>, S.pushed(T, sp), D.pushed_obs(~T, rr)):  match p:    case Tuple{+sh2, Tuple{+o, Tuple{+er, Tuple{+es, hg2}}}}:      (sh2, (E.OHandle{o}, (Equal.cong(D.DList<T> & E.Handle, D.DList<T> & E.Obs<T>, r => D.pushed_obs(~T, r), rr, (ST.real(~T, sh2), o), er), (Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.pushed(T, r), sp, (ST.model(~T, sh2), o), es), hg2))))# the specification's placement is the placement between a and bdef ins_pos(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T, +pos: S.Pos, +a: List<&2, Nat>, +b: List<&2, Nat>, e: @+n: Nat -> {S.place_order(pos, order, n) == SC.append(Nat, a, Con{n, b}) : List<&2, Nat>}) -> {S.inserted(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, pos) == IP.insAB(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, a, b) : S.DS<T> & E.Handle}:  match free:    case Nil{}:      Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, SC.snoc(Maybe<&2, T>, vals, None{}), SC.length(Maybe<&2, T>, vals), Some{x}), SC.snoc(U32, gens, 0), Nil{}}, S.handle(tag, SC.snoc(U32, gens, 0), SC.length(Maybe<&2, T>, vals))), S.place_order(pos, order, SC.length(Maybe<&2, T>, vals)), SC.append(Nat, a, Con{SC.length(Maybe<&2, T>, vals), b}), e(SC.length(Maybe<&2, T>, vals)))    case Con{+i, +rest}:      Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, vals, i, Some{x}), gens, rest}, S.handle(tag, gens, i)), S.place_order(pos, order, i), SC.append(Nat, a, Con{i, b}), e(i))def ib_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +n: Nat, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.ins_before(SC.append(Nat, a, Con{s, b}), s, n) == SC.append(Nat, a, Con{n, Con{s, b}}) : List<&2, Nat>}:  match a:    case Nil{}:      Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{n, Con{s, b}}, Con{s, S.ins_before(b, s, n)}), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))    case Con{+y, +t}:      Equal.trans(List<&2, Nat>, S.ins_before(SC.append(Nat, Con{y, t}, Con{s, b}), s, n), Con{y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n)}, SC.append(Nat, Con{y, t}, Con{n, Con{s, b}}), Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{n, Con{y, SC.append(Nat, t, Con{s, b})}}, Con{y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n)}), Nat.is_eq(y, s), False{}, NL.or_ff_l(Nat.is_eq(y, s), NL.memn(s, t), h)), LL.cons_cong(Nat, y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n), SC.append(Nat, t, Con{n, Con{s, b}}), ib_mid(t, s, b, n, NL.or_ff_r(Nat.is_eq(y, s), NL.memn(s, t), h))))def ia_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +n: Nat, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.ins_after(SC.append(Nat, a, Con{s, b}), s, n) == SC.append(Nat, a, Con{s, Con{n, b}}) : List<&2, Nat>}:  match a:    case Nil{}:      Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{s, Con{n, b}}, Con{s, S.ins_after(b, s, n)}), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))    case Con{+y, +t}:      Equal.trans(List<&2, Nat>, S.ins_after(SC.append(Nat, Con{y, t}, Con{s, b}), s, n), Con{y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n)}, SC.append(Nat, Con{y, t}, Con{s, Con{n, b}}), Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{y, Con{n, SC.append(Nat, t, Con{s, b})}}, Con{y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n)}), Nat.is_eq(y, s), False{}, NL.or_ff_l(Nat.is_eq(y, s), NL.memn(s, t), h)), LL.cons_cong(Nat, y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n), SC.append(Nat, t, Con{s, Con{n, b}}), ia_mid(t, s, b, n, NL.or_ff_r(Nat.is_eq(y, s), NL.memn(s, t), h))))