proofs/containers/doubly_linked_list/step.bend
bend-collections-laws-containers@1.0.0.0 · 184 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/u32alg.bend as A
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as S
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
10import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
11import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
12import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/vals.bend as VA
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/ok.bend as OK
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/insp.bend as IP
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/ins.bend as IN
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/valid.bend as VD
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hrd.bend as HR
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hnb.bend as NB
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hlive.bend as HL
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hins.bend as HI
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/walk.bend as WL
24import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
25import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
26
27# THEOREM (one step): every operation, on every good shadow with fewer than
28# 2^cz issued ids, refines the specification's step.
29
30
31# ---- length and to_list ----
32
33def len_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Length{}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Length{})):
34 (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.ONat{SC.length(Nat, sl)}, ({==}, ({==}, hg))))
35
36def values_take(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}) -> {S.values(T, SC.take(Maybe<&2, T>, vl, fr), xs) == S.values(T, vl, xs) : List<&2, T>}:
37 match xs:
38 case Nil{}:
39 {==}
40 case Con{+x, +t}:
41 +hx = L.and_left(Nat.is_lt(x, fr), ST.live(T, vl, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h))
42 +ih = values_take(~T, t, fr, vl, L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h))
43 Equal.trans(List<&2, T>, S.cons_some(T, S.val_of(T, SC.take(Maybe<&2, T>, vl, fr), x), S.values(T, SC.take(Maybe<&2, T>, vl, fr), t)), S.cons_some(T, S.val_of(T, vl, x), S.values(T, SC.take(Maybe<&2, T>, vl, fr), t)), S.cons_some(T, S.val_of(T, vl, x), S.values(T, vl, t)), Equal.cong(Maybe<&2, T>, List<&2, T>, m => S.cons_some(T, m, S.values(T, SC.take(Maybe<&2, T>, vl, fr), t)), S.val_of(T, SC.take(Maybe<&2, T>, vl, fr), x), S.val_of(T, vl, x), VA.val_take(T, vl, fr, x, hx)), Equal.cong(List<&2, T>, List<&2, T>, z => S.cons_some(T, S.val_of(T, vl, x), z), S.values(T, SC.take(Maybe<&2, T>, vl, fr), t), S.values(T, vl, t), ih))
44
45
46# the storage's to_list: the values of the list's ids in order
47def raw_list(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}) -> {R.to_list(~T, 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)}) == (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)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)) : R.DList<T> & List<&2, T>}:
48 +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))
49 +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))
50 +ec = Equal.sym(Nat, SC.length(Nat, NL.rapp(sl, Nil{})), SC.length(Nat, sl), Equal.trans(Nat, SC.length(Nat, NL.rapp(sl, Nil{})), Nat.add(SC.length(Nat, sl), 0n), SC.length(Nat, sl), NL.len_rapp(sl, Nil{}), N.add_zero(SC.length(Nat, sl))))
51 +et = Equal.trans(U32, tail, LK.last_or(sl, 0), LK.fst_or(NL.rapp(sl, Nil{}), 0), A.eq_of(tail, LK.last_or(sl, 0), ST.g_ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)), Equal.sym(U32, LK.fst_or(NL.rapp(sl, Nil{}), 0), LK.last_or(sl, 0), LK.fo_rapp(sl, Nil{}, 0)))
52 +hrok = WL.rok_app(~T, AR.slots(U32, pT), AR.slots(U32, nT), AR.slots(Maybe<&2, T>, vT), sl, Nil{}, UD.v(fresh), 0, 0, ST.g_cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), {==}, LK.u_refl(0))
53 +ew = WL.walk(~T, one, h1, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, pT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), ST.g_cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), UD.v(fresh), hfr2, NL.rapp(sl, Nil{}), Nil{}, hrok)
54 +er1 = Equal.cong(Nat, R.DList<T> & List<&2, T>, n => R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, n, R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), SC.length(Nat, sl), SC.length(Nat, NL.rapp(sl, Nil{})), ec)
55 +er2 = Equal.cong(U32, R.DList<T> & List<&2, T>, z => R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, z})), tail, LK.fst_or(NL.rapp(sl, Nil{}), 0), et)
56 +er3 = Equal.cong(R.Cur<T>, R.DList<T> & List<&2, T>, c => R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), c), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, LK.fst_or(NL.rapp(sl, Nil{}), 0)}), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{}), 0}, ew)
57 +ev = Equal.trans(List<&2, T>, WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{}), SC.append(T, S.values(T, AR.slots(Maybe<&2, T>, vT), sl), Nil{}), S.values(T, AR.slots(Maybe<&2, T>, vT), sl), WL.ra_rapp(T, AR.slots(Maybe<&2, T>, vT), sl, Nil{}, Nil{}), LL.append_nil(T, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)))
58 +er4 = Equal.cong(List<&2, T>, R.DList<T> & List<&2, T>, z => (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)}, z), WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{}), S.values(T, AR.slots(Maybe<&2, T>, vT), sl), ev)
59 Equal.trans(R.DList<T> & List<&2, T>, R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, sl), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), (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)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), er1, Equal.trans(R.DList<T> & List<&2, T>, R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, tail})), R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, LK.fst_or(NL.rapp(sl, Nil{}), 0)})), (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)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), er2, Equal.trans(R.DList<T> & List<&2, T>, R.tl_fin(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, nT), R.walk(~T, SC.length(Nat, NL.rapp(sl, Nil{})), R.C{AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), Nil{}, LK.fst_or(NL.rapp(sl, Nil{}), 0)})), (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)}, WL.racc(T, AR.slots(Maybe<&2, T>, vT), NL.rapp(sl, Nil{}), Nil{})), (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)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), er3, er4)))
60
61def spec_list(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}) -> {S.list_of(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl})) == S.values(T, AR.slots(Maybe<&2, T>, vT), sl) : List<&2, T>}:
62 values_take(~T, sl, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))
63
64def list_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ToList{}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ToList{})):
65 +er = Equal.cong(R.DList<T> & List<&2, T>, D.DList<T> & E.Obs<T>, r => D.list_result(~T, tag, depth, cap, AR.thaw(U32, gT), r), R.to_list(~T, 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)}), (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)}, S.values(T, AR.slots(Maybe<&2, T>, vT), sl)), raw_list(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))
66 +es = Equal.cong(List<&2, T>, S.DS<T> & E.Obs<T>, z => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OList{z}), S.list_of(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl})), S.values(T, AR.slots(Maybe<&2, T>, vT), sl), spec_list(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))
67 (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.OList{S.values(T, AR.slots(Maybe<&2, T>, vT), sl)}, (er, (es, hg))))
68
69# ---- the pushes ----
70
71
72
73def front_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_front(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_front(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x)):
74 p = IN.ins_ok(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, Nil{}, sl, cz, hcz, free, fl, hg, hroom, x)
75 +eh = A.eq_of(head, LK.fst_or(sl, 0), ST.g_chead(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))
76 +er = Equal.cong(U32, D.DList<T> & E.Handle, z => D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, 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), 0, z, x)), head, LK.fst_or(sl, 0), eh)
77 +es = HL.ins_pos(T, tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl, x, S.PFront{}, Nil{}, sl, n => {==})
78 OK.pok_eq(~T, E.Handle, S.push_front(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), IP.insAB(T, S.alloc(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl})), x, Nil{}, sl), D.push_front(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, 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), 0, LK.fst_or(sl, 0), x)), es, er, p)
79
80def front_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushFront{x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushFront{x})):
81 HL.pok_push(~T, S.push_front(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_front(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), front_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x))
82
83
84def back_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x)):
85 +ean = LL.append_nil(Nat, sl)
86 +hg3 = L.subst(List<&2, Nat>, z => {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl) == True{} : Bool}, sl, SC.append(Nat, sl, Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, sl, Nil{}), sl, ean), hg)
87 p = IN.ins_ok(~T, one, h1, tag, cap, fresh, head, tail, depth, vT, pT, nT, gT, sl, Nil{}, cz, hcz, free, fl, hg3, hroom, x)
88 +et = A.eq_of(tail, LK.last_or(sl, 0), ST.g_ctail(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg))
89 +er1 = Equal.cong(U32, D.DList<T> & E.Handle, z => D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, 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), z, 0, x)), tail, LK.last_or(sl, 0), et)
90 +er2 = Equal.cong(List<&2, Nat>, D.DList<T> & E.Handle, z => D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, z), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(sl, 0), 0, x)), sl, SC.append(Nat, sl, Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, sl, Nil{}), sl, ean))
91 +er = Equal.trans(D.DList<T> & E.Handle, D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, 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), LK.last_or(sl, 0), 0, x)), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, sl, Nil{})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(sl, 0), 0, x)), er1, er2)
92 +es1 = HL.ins_pos(T, tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl, x, S.PBack{}, sl, Nil{}, n => LL.snoc_append(Nat, sl, n))
93 +es2 = Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => IP.insAB(T, S.alloc(T, S.DS{tag, z, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), sl, SC.append(Nat, sl, Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, sl, Nil{}), sl, ean))
94 +es = Equal.trans(S.DS<T> & E.Handle, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), IP.insAB(T, S.alloc(T, S.DS{tag, sl, SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, sl, Nil{}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), es1, es2)
95 OK.pok_eq(~T, E.Handle, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), IP.insAB(T, S.alloc(T, S.DS{tag, SC.append(Nat, sl, Nil{}), SC.take(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), UD.v(fresh)), SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), fl}), x, sl, Nil{}), D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.inserted(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_between_free(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, sl, Nil{})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), LK.last_or(sl, 0), 0, x)), es, er, p)
96
97def back_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushBack{x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.PushBack{x})):
98 HL.pok_push(~T, S.push_back(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), D.push_back(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), x), back_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x))
99
100# ---- the handle operations ----
101
102
103def get_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{E.H{owner, id, g}})):
104 VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Get{E.H{owner, id, g}}, {==}, {==}, ho => hlt => HR.get_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt), ho => hlt => hv => HR.get_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt, hv), ho => hlt => vv => hv => hgen => HR.get_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt, vv, hv, hgen))
105
106def set_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{E.H{owner, id, g}, x})):
107 VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Set{E.H{owner, id, g}, x}, {==}, {==}, ho => hlt => HR.set_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt), ho => hlt => hv => HR.set_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt, hv), ho => hlt => vv => hv => hgen => HR.set_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, ho, hlt, vv, hv, hgen))
108
109def next_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}})):
110 VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Next{E.H{owner, id, g}}, {==}, {==}, ho => hlt => NB.nb_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, True{}, ho, hlt), ho => hlt => hv => NB.nb_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, True{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.next_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, one, h1, ho, hlt, vv, hv, hgen))
111
112def prev_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}})):
113 VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Prev{E.H{owner, id, g}}, {==}, {==}, ho => hlt => NB.nb_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, False{}, ho, hlt), ho => hlt => hv => NB.nb_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, False{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.prev_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, one, h1, ho, hlt, vv, hv, hgen))
114
115def remove_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}})):
116 VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Remove{E.H{owner, id, g}}, {==}, {==}, ho => hlt => HL.rm_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt), ho => hlt => hv => HL.rm_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.rm_live(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, one, h1, ho, hlt, vv, hv, hgen))
117
118def before_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{E.H{owner, id, g}, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{E.H{owner, id, g}, x})):
119 VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertBefore{E.H{owner, id, g}, x}, {==}, {==}, ho => hlt => HL.ins_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, False{}, ho, hlt), ho => hlt => hv => HL.ins_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, False{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertBefore{E.H{owner, id, g}, x}, vv, hv, a => b => hg2 => HI.ib_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, cz, hcz, hroom, ho, hlt, vv, hv, x)))
120
121def after_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{E.H{owner, id, g}, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{E.H{owner, id, g}, x})):
122 VD.vstep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertAfter{E.H{owner, id, g}, x}, {==}, {==}, ho => hlt => HL.ins_hi(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, True{}, ho, hlt), ho => hlt => hv => HL.ins_none(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, True{}, ho, hlt, hv), ho => hlt => vv => hv => hgen => HL.with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.InsertAfter{E.H{owner, id, g}, x}, vv, hv, a => b => hg2 => HI.ia_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, cz, hcz, hroom, ho, hlt, vv, hv, x)))
123
124# ---- every operation ----
125
126def get_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Get{h})):
127 match h:
128 case E.H{+owner, +id, +g}:
129 get_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)
130
131def set_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}, +h: E.Handle, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{h, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Set{h, x})):
132 match h:
133 case E.H{+owner, +id, +g}:
134 set_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x)
135
136def next_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{h})):
137 match h:
138 case E.H{+owner, +id, +g}:
139 next_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)
140
141def prev_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{h})):
142 match h:
143 case E.H{+owner, +id, +g}:
144 prev_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)
145
146def remove_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +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}, +h: E.Handle) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{h}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{h})):
147 match h:
148 case E.H{+owner, +id, +g}:
149 remove_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g)
150
151def before_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +h: E.Handle, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{h, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertBefore{h, x})):
152 match h:
153 case E.H{+owner, +id, +g}:
154 before_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, owner, id, g, x)
155
156def after_h(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +h: E.Handle, +x: T) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{h, x}), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.InsertAfter{h, x})):
157 match h:
158 case E.H{+owner, +id, +g}:
159 after_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, owner, id, g, x)
160
161def step_ok(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +cz: Nat, +hcz: {cz == 29n : Nat}, +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}, +hroom: {Nat.is_lt(UD.v(fresh), SC.pow2(cz)) == True{} : Bool}, +op: E.Op<T>) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op), D.step(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)):
162 match op:
163 case E.Length{}:
164 len_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)
165 case E.PushFront{+x}:
166 front_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x)
167 case E.PushBack{+x}:
168 back_ok(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, x)
169 case E.InsertBefore{+h, +x}:
170 before_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, h, x)
171 case E.InsertAfter{+h, +x}:
172 after_h(~T, one, h1, cz, hcz, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, hroom, h, x)
173 case E.Remove{+h}:
174 remove_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h)
175 case E.Get{+h}:
176 get_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h)
177 case E.Set{+h, +x}:
178 set_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h, x)
179 case E.Next{+h}:
180 next_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h)
181 case E.Prev{+h}:
182 prev_h(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, h)
183 case E.ToList{}:
184 list_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg)