proofs/containers/doubly_linked_list/valid.bend source

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

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../lib/u32alg.bend as Aimport ../../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/doubly_linked_list.bend as Eimport ./state.bend as STimport ./rel.bend as RLimport ./vals.bend as VAimport ./ok.bend as OKimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# Handle validation. The public list checks the owner, the id against its# capacity and the generation, then the storage checks the id against its# counter and the value slot; the specification checks the owner, the value# and the generation. Every combination gives the same verdict.# ---- the public list's verdict ----def iv_foreign(~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, +hc: {U32.is_eq(tag, owner) == False{} : Bool}) -> {D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), Some{E.ForeignHandle{}}) : D.DList<T> & Maybe<&2, E.Error>}:  Equal.cong(Bool, D.DList<T> & Maybe<&2, E.Error>, z => D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, z, U32.is_lt(id, cap)), U32.is_eq(tag, owner), False{}, hc)def iv_cap(~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, +hc: {U32.is_eq(tag, owner) == True{} : Bool}, +hcap: {U32.is_lt(id, cap) == False{} : Bool}) -> {D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), Some{E.StaleHandle{}}) : D.DList<T> & Maybe<&2, E.Error>}:  Equal.trans(D.DList<T> & Maybe<&2, E.Error>, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, True{}, U32.is_lt(id, cap)), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), Some{E.StaleHandle{}}), Equal.cong(Bool, D.DList<T> & Maybe<&2, E.Error>, z => D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, z, U32.is_lt(id, cap)), U32.is_eq(tag, owner), True{}, hc), Equal.cong(Bool, D.DList<T> & Maybe<&2, E.Error>, z => D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, True{}, z), U32.is_lt(id, cap), False{}, hcap))def iv_gen(~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, +hc: {U32.is_eq(tag, owner) == True{} : Bool}, +hcap: {U32.is_lt(id, cap) == True{} : Bool}) -> {D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.generation_error(U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g))) : D.DList<T> & Maybe<&2, E.Error>}:  +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)  +hi = L.subst(Nat, z => {Nat.is_lt(UD.v(id), z) == True{} : Bool}, UD.v(cap), SC.pow2(depth), N.eq_from_is_eq(UD.v(cap), SC.pow2(depth), ST.g_ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)), Equal.trans(Bool, Nat.is_lt(UD.v(id), UD.v(cap)), U32.is_lt(id, cap), True{}, Equal.sym(Bool, U32.is_lt(id, cap), Nat.is_lt(UD.v(id), UD.v(cap)), U.is_lt_nat(id, cap)), hcap))  +e1 = Equal.cong(Bool, D.DList<T> & Maybe<&2, E.Error>, z => D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, z, U32.is_lt(id, cap)), U32.is_eq(tag, owner), True{}, hc)  +e2 = Equal.cong(Bool, D.DList<T> & Maybe<&2, E.Error>, z => D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, True{}, z), U32.is_lt(id, cap), True{}, hcap)  +e3 = Equal.cong(Array<U32> & U32, D.DList<T> & Maybe<&2, E.Error>, r => D.valid_gen(~T, tag, depth, cap, R.DL{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)}, g, r), Array.get(U32, AR.thaw(U32, gT), id), (AR.thaw(U32, gT), W32.nth0(AR.slots(U32, gT), UD.v(id))), UT.uget(depth, RL.hd0(depth, hd), gT, ST.g_cpg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, hi))  Equal.trans(D.DList<T> & Maybe<&2, E.Error>, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, True{}, U32.is_lt(id, cap)), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.generation_error(U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g))), e1, Equal.trans(D.DList<T> & Maybe<&2, E.Error>, D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, True{}, U32.is_lt(id, cap)), D.valid_bounds(~T, tag, depth, cap, R.DL{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)}, AR.thaw(U32, gT), id, g, True{}, True{}), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.generation_error(U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g))), e2, e3))# ---- the specification's verdict ----def len_vlf(~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) -> {SC.length(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh))) == UD.v(fresh) : Nat}:  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(depth), ST.g_ccap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, UD.v(cap), SC.pow2(depth), e2d, ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))  LL.sc_length_take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), L.subst(Nat, z => {Nat.is_le(UD.v(fresh), z) == True{} : Bool}, SC.pow2(depth), SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT)), Equal.sym(Nat, SC.length(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT)), SC.pow2(depth), AR.slots_length(Maybe<&2, T>, depth, vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))), hfr2))def sv_foreign(~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, +hc: {U32.is_eq(owner, tag) == False{} : Bool}) -> {S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}) == Some{E.ForeignHandle{}} : Maybe<&2, E.Error>}:  Equal.cong(Bool, Maybe<&2, E.Error>, z => S.valid_own(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), g, z), U32.is_eq(owner, tag), False{}, hc)def sv_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, +hc: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}) == Some{E.StaleHandle{}} : Maybe<&2, E.Error>}:  +hle = L.subst(Nat, z => {Nat.is_le(z, UD.v(id)) == True{} : Bool}, UD.v(fresh), SC.length(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh))), Equal.sym(Nat, SC.length(Maybe<&2, T>, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh))), UD.v(fresh), len_vlf(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)), N.not_lt_le(UD.v(id), UD.v(fresh), hlt))  +e1 = Equal.cong(Bool, Maybe<&2, E.Error>, z => S.valid_own(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), g, z), U32.is_eq(owner, tag), True{}, hc)  +e2 = Equal.cong(Maybe<&2, T>, Maybe<&2, E.Error>, m => S.live_gen(T, m, U32.is_eq(S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), g)), S.val_of(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id)), None{}, VA.val_hi(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id), hle))  Equal.trans(Maybe<&2, E.Error>, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), S.valid_own(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), g, True{}), Some{E.StaleHandle{}}, e1, e2)def sv_lo(~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, +hc: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}) == S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g)) : Maybe<&2, E.Error>}:  +e1 = Equal.cong(Bool, Maybe<&2, E.Error>, z => S.valid_own(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), g, z), U32.is_eq(owner, tag), True{}, hc)  +e2 = Equal.cong(Maybe<&2, T>, Maybe<&2, E.Error>, m => S.live_gen(T, m, U32.is_eq(S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), g)), S.val_of(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), UD.v(id)), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), VA.val_take(T, AR.slots(Maybe<&2, T>, vT), UD.v(fresh), UD.v(id), hlt))  +e3 = Equal.cong(U32, Maybe<&2, E.Error>, z => S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(z, g)), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), W32.nth0(AR.slots(U32, gT), UD.v(id)), VA.gen_take(AR.slots(U32, gT), UD.v(fresh), UD.v(id), hlt))  Equal.trans(Maybe<&2, E.Error>, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), S.valid_own(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), g, True{}), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g)), e1, Equal.trans(Maybe<&2, E.Error>, S.valid_own(T, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id), g, True{}), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), UD.v(id)), g)), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g)), e2, e3))def lg_false(-T: Data, +m: Maybe<&2, T>) -> {S.live_gen(T, m, False{}) == Some{E.StaleHandle{}} : Maybe<&2, E.Error>}:  match m:    case None{}:      {==}    case Some{v}:      {==}# ---- the verdicts' results ----# both sides fail with edef v_close(~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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.Obs<T>}, +e: E.Error, +he: {D.failed(~T, op, e) == S.failed(T, op, e) : E.Obs<T>}, +er: {D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 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, op, e)) : D.DList<T> & E.Obs<T>}, +es: {S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})) == (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), S.failed(T, op, e)) : S.DS<T> & E.Obs<T>}) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  +es2 = Equal.trans(S.DS<T> & E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), S.failed(T, op, e)), (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, e)), es, Equal.cong(E.Obs<T>, S.DS<T> & E.Obs<T>, o => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), o), S.failed(T, op, e), D.failed(~T, op, e), Equal.sym(E.Obs<T>, D.failed(~T, op, e), S.failed(T, op, e), he)))  (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (D.failed(~T, op, e), (er, (es2, hg))))# the value slot, the generation currentdef v_val(~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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.Obs<T>}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hgt: {U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g) == True{} : Bool}, +er0: {D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})) == D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op) : D.DList<T> & E.Obs<T>}, +es0: {S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}) == S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}) : Maybe<&2, E.Error>}, stale_none: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, live: @+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}), 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)), +m: Maybe<&2, T>, +hm: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == m : Maybe<&2, T>}) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  match m:    case None{}:      +es = Equal.cong(Maybe<&2, E.Error>, S.DS<T> & E.Obs<T>, v => S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, v), S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), Some{E.StaleHandle{}}, Equal.trans(Maybe<&2, E.Error>, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}), Some{E.StaleHandle{}}, es0, Equal.cong(Maybe<&2, T>, Maybe<&2, E.Error>, z => S.live_gen(T, z, True{}), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hm)))      v_close(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, E.StaleHandle{}, hfS, Equal.trans(D.DList<T> & E.Obs<T>, D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})), er0, stale_none(ho, hlt, hm)), es)    case Some{+vv}:      +es = Equal.cong(Maybe<&2, E.Error>, S.DS<T> & E.Obs<T>, v => S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, v), S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), None{}, Equal.trans(Maybe<&2, E.Error>, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}), None{}, es0, Equal.cong(Maybe<&2, T>, Maybe<&2, E.Error>, z => S.live_gen(T, z, True{}), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hm)))      +hgen = Equal.sym(U32, W32.nth0(AR.slots(U32, gT), UD.v(id)), g, A.eq_of(W32.nth0(AR.slots(U32, gT), UD.v(id)), g, hgt))      OK.pok_eq(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), 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.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op), es, er0, live(ho, hlt, vv, hm, hgen))# the generation current: the storage decidesdef v_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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.Obs<T>}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hgt: {U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g) == True{} : Bool}, +er0: {D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})) == D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op) : D.DList<T> & E.Obs<T>}, stale_hi: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, stale_none: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, live: @+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}), 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)), +c: Bool, +hc: {Nat.is_lt(UD.v(id), UD.v(fresh)) == c : Bool}) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  match c:    case False{}:      v_close(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, E.StaleHandle{}, hfS, Equal.trans(D.DList<T> & E.Obs<T>, D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})), er0, stale_hi(ho, hc)), Equal.cong(Maybe<&2, E.Error>, S.DS<T> & E.Obs<T>, v => S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, v), S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), Some{E.StaleHandle{}}, sv_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hc)))    case True{}:      +es0 = Equal.trans(Maybe<&2, E.Error>, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g)), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}), sv_lo(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hc), Equal.cong(Bool, Maybe<&2, E.Error>, z => S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), z), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g), True{}, hgt))      v_val(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, ho, hc, hgt, er0, es0, stale_none, live, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), {==})# the generation stale: both rejectdef v_genf(~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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.Obs<T>}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hgf: {U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g) == False{} : Bool}, +er: {D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), 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, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, +c: Bool, +hc: {Nat.is_lt(UD.v(id), UD.v(fresh)) == c : Bool}) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  match c:    case False{}:      v_close(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, E.StaleHandle{}, hfS, er, Equal.cong(Maybe<&2, E.Error>, S.DS<T> & E.Obs<T>, v => S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, v), S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), Some{E.StaleHandle{}}, sv_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hc)))    case True{}:      +es0 = Equal.trans(Maybe<&2, E.Error>, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g)), Some{E.StaleHandle{}}, sv_lo(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hc), Equal.trans(Maybe<&2, E.Error>, S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g)), S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), False{}), Some{E.StaleHandle{}}, Equal.cong(Bool, Maybe<&2, E.Error>, z => S.live_gen(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), z), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g), False{}, hgf), lg_false(T, S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)))))      v_close(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, E.StaleHandle{}, hfS, er, Equal.cong(Maybe<&2, E.Error>, S.DS<T> & E.Obs<T>, v => S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, v), S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), Some{E.StaleHandle{}}, es0))def v_gen(~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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.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(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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, stale_none: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, live: @+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}), 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)), +c: Bool, +hc: {U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g) == c : Bool}) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  match c:    case False{}:      +ev = iv_gen(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hc1, hcap)      v_genf(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, ho, hc, Equal.cong(D.DList<T> & Maybe<&2, E.Error>, D.DList<T> & E.Obs<T>, r => D.checked(~T, op, r), D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), Some{E.StaleHandle{}}), Equal.trans(D.DList<T> & Maybe<&2, E.Error>, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.generation_error(U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), Some{E.StaleHandle{}}), ev, Equal.cong(Bool, D.DList<T> & Maybe<&2, E.Error>, z => (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.generation_error(z)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g), False{}, hc))), Nat.is_lt(UD.v(id), UD.v(fresh)), {==})    case True{}:      +ev = iv_gen(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hc1, hcap)      v_go(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, ho, hc, Equal.cong(D.DList<T> & Maybe<&2, E.Error>, D.DList<T> & E.Obs<T>, r => D.checked(~T, op, r), D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), None{}), Equal.trans(D.DList<T> & Maybe<&2, E.Error>, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.generation_error(U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), None{}), ev, Equal.cong(Bool, D.DList<T> & Maybe<&2, E.Error>, z => (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.generation_error(z)), U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g), True{}, hc))), stale_hi, stale_none, live, Nat.is_lt(UD.v(id), UD.v(fresh)), {==})# the id at or above the capacity is above every issued iddef cap_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, +hcap: {U32.is_lt(id, cap) == False{} : Bool}) -> {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}:  +hle = N.not_lt_le(UD.v(id), UD.v(cap), Equal.trans(Bool, Nat.is_lt(UD.v(id), UD.v(cap)), U32.is_lt(id, cap), False{}, Equal.sym(Bool, U32.is_lt(id, cap), Nat.is_lt(UD.v(id), UD.v(cap)), U.is_lt_nat(id, cap)), hcap))  N.le_not_lt(UD.v(id), UD.v(fresh), N.le_trans(UD.v(fresh), UD.v(cap), UD.v(id), ST.g_cfr(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), hle))def v_cap(~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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.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(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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, stale_none: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, live: @+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}), 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)), +c: Bool, +hc: {U32.is_lt(id, cap) == c : Bool}) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  match c:    case False{}:      v_close(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, E.StaleHandle{}, hfS, Equal.cong(D.DList<T> & Maybe<&2, E.Error>, D.DList<T> & E.Obs<T>, r => D.checked(~T, op, r), D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), Some{E.StaleHandle{}}), iv_cap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hc1, hc)), Equal.cong(Maybe<&2, E.Error>, S.DS<T> & E.Obs<T>, v => S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, v), S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), Some{E.StaleHandle{}}, sv_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, cap_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hc))))    case True{}:      v_gen(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, ho, hc1, hc, stale_hi, stale_none, live, U32.is_eq(W32.nth0(AR.slots(U32, gT), UD.v(id)), g), {==})def v_own(~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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.Obs<T>}, stale_hi: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, stale_none: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, live: @+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}), 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)), +c: Bool, +hc: {U32.is_eq(tag, owner) == c : Bool}) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  match c:    case False{}:      +hs = Equal.trans(Bool, U32.is_eq(owner, tag), U32.is_eq(tag, owner), False{}, W32.eq_sym_u32(owner, tag), hc)      v_close(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, E.ForeignHandle{}, hfF, Equal.cong(D.DList<T> & Maybe<&2, E.Error>, D.DList<T> & E.Obs<T>, r => D.checked(~T, op, r), D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), Some{E.ForeignHandle{}}), iv_foreign(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hc)), Equal.cong(Maybe<&2, E.Error>, S.DS<T> & E.Obs<T>, v => S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, v), S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}), Some{E.ForeignHandle{}}, sv_foreign(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hs)))    case True{}:      +hs = Equal.trans(Bool, U32.is_eq(owner, tag), U32.is_eq(tag, owner), True{}, W32.eq_sym_u32(owner, tag), hc)      v_cap(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, hs, hc, stale_hi, stale_none, live, U32.is_lt(id, cap), {==})# 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 otherwisedef vstep(~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>, +hfF: {D.failed(~T, op, E.ForeignHandle{}) == S.failed(T, op, E.ForeignHandle{}) : E.Obs<T>}, +hfS: {D.failed(~T, op, E.StaleHandle{}) == S.failed(T, op, E.StaleHandle{}) : E.Obs<T>}, stale_hi: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, stale_none: @+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}), op) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, op, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}, live: @+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}), 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))) -> OK.POK(~T, E.Obs<T>, S.checked(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, E.H{owner, id, g}, S.validate(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g})), D.checked(~T, op, D.validate(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.H{owner, id, g}))):  v_own(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, hfF, hfS, stale_hi, stale_none, live, U32.is_eq(tag, owner), {==})