~/jendhub

proofs/containers/doubly_linked_list/valid.bend

bend-collections-laws-containers@1.0.0.0 · 144 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as A
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as S
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
11import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
12import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
13import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/rel.bend as RL
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/vals.bend as VA
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/ok.bend as OK
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
19import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
20
21# Handle validation. The public list checks the owner, the id against its
22# capacity and the generation, then the storage checks the id against its
23# counter and the value slot; the specification checks the owner, the value
24# and the generation. Every combination gives the same verdict.
25
26
27# ---- the public list's verdict ----
28
29def 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>}:
30  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)
31
32def 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>}:
33  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))
34
35def 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>}:
36  +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)
37  +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))
38  +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)
39  +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)
40  +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))
41  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))
42
43# ---- the specification's verdict ----
44
45def 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}:
46  +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))
47  +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))
48  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))
49
50def 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>}:
51  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)
52
53def 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>}:
54  +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))
55  +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)
56  +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))
57  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)
58
59def 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>}:
60  +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)
61  +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))
62  +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))
63  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))
64
65def lg_false(-T: Data, +m: Maybe<&2, T>) -> {S.live_gen(T, m, False{}) == Some{E.StaleHandle{}} : Maybe<&2, E.Error>}:
66  match m:
67    case None{}:
68      {==}
69    case Some{v}:
70      {==}
71
72# ---- the verdicts' results ----
73
74
75# both sides fail with e
76def 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}))):
77  +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)))
78  (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (D.failed(~T, op, e), (er, (es2, hg))))
79
80
81# the value slot, the generation current
82def 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}))):
83  match m:
84    case None{}:
85      +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)))
86      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)
87    case Some{+vv}:
88      +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)))
89      +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))
90      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))
91
92# the generation current: the storage decides
93def 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}))):
94  match c:
95    case False{}:
96      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)))
97    case True{}:
98      +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))
99      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)), {==})
100
101# the generation stale: both reject
102def 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}))):
103  match c:
104    case False{}:
105      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)))
106    case True{}:
107      +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)))))
108      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))
109
110def 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}))):
111  match c:
112    case False{}:
113      +ev = iv_gen(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hc1, hcap)
114      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)), {==})
115    case True{}:
116      +ev = iv_gen(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hc1, hcap)
117      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)), {==})
118
119# the id at or above the capacity is above every issued id
120def 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}:
121  +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))
122  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))
123
124def 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}))):
125  match c:
126    case False{}:
127      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))))
128    case True{}:
129      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), {==})
130
131def 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}))):
132  match c:
133    case False{}:
134      +hs = Equal.trans(Bool, U32.is_eq(owner, tag), U32.is_eq(tag, owner), False{}, W32.eq_sym_u32(owner, tag), hc)
135      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)))
136    case True{}:
137      +hs = Equal.trans(Bool, U32.is_eq(owner, tag), U32.is_eq(tag, owner), True{}, W32.eq_sym_u32(owner, tag), hc)
138      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), {==})
139
140# THEOREM (validation): an operation on a handle refines the specification's
141# when its storage part does, on a live element with a current handle, and
142# fails as the specification's otherwise
143def 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}))):
144  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), {==})