proofs/containers/doubly_linked_list/hlive.bend
bend-collections-laws-containers@1.0.0.0 · 121 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/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as S
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
10import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
11import bend-collections-laws-containers@1.0.0.0/src/containers/types/internal_dlist.bend as I
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/rel.bend as RL
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/vals.bend as VA
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/link.bend as LN
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/containers/doubly_linked_list/insp.bend as IP
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/rm.bend as RM
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hrd.bend as HR
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/hnb.bend as NB
22import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
23import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
24
25# The live element, split out of its list: next, prev, remove, and the
26# insertions before and after it; and the storage's stale answers for
27# remove and the insertions.
28
29
30# ---- splitting the list at the live element ----
31
32def mem_of(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}) -> {NL.memn(UD.v(id), sl) == True{} : Bool}:
33 VA.lvin_elim(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl, ST.g_clv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), UD.v(id), RL.by_eq(ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), True{}, Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), Some{vv}, hv), {==}))
34
35def ws_go(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +op: E.Op<T>, sp: NL.Split(UD.v(id), sl), k: @+a: List<&2, Nat> -> @+b: List<&2, Nat> -> @+hg2: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool} -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op))) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)):
36 match sp:
37 case Tuple{+a, Tuple{+b, e}}:
38 +e2 = {e : {sl == SC.append(Nat, a, Con{UD.v(id), b}) : List<&2, Nat>}}
39 +hg2 = L.subst(List<&2, Nat>, z => {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl) == True{} : Bool}, sl, SC.append(Nat, a, Con{UD.v(id), b}), e2, hg)
40 r = k(a, b, hg2)
41 L.subst(List<&2, Nat>, z => OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, z, fl}), op)), SC.append(Nat, a, Con{UD.v(id), b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{UD.v(id), b}), e2), r)
42
43def with_split(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +op: E.Op<T>, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, k: @+a: List<&2, Nat> -> @+b: List<&2, Nat> -> @+hg2: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl) == True{} : Bool} -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl}), op))) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), op)):
44 ws_go(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, op, NL.split_mem(UD.v(id), sl, mem_of(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, vv, hv)), k)
45
46
47def next_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Next{E.H{owner, id, g}})):
48 with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Next{E.H{owner, id, g}}, vv, hv, a => b => hg2 => NB.nx_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, ho, hlt, vv, hv))
49
50def prev_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Prev{E.H{owner, id, g}})):
51 with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Prev{E.H{owner, id, g}}, vv, hv, a => b => hg2 => NB.pv_ab(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg2, one, h1, ho, hlt, vv, hv))
52
53def rm_live(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +one: Nat, +h1: {one == 1n : Nat}, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +vv: T, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == Some{vv} : Maybe<&2, T>}, +hgen: {g == W32.nth0(AR.slots(U32, gT), UD.v(id)) : U32}) -> OK.POK(~T, E.Obs<T>, S.live_op(T, ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}, UD.v(id)), D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}})):
54 with_split(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, E.Remove{E.H{owner, id, g}}, vv, hv, a => b => hg2 => RM.rm_ok(~T, one, h1, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, id, b, fl, hg2, owner, ho, g, hgen, vv, hv))
55
56# ---- remove: the storage's stale answers ----
57
58
59def rm_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}:
60 Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, HR.lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, z)), U32.is_eq(owner, tag), True{}, ho))
61
62def rm_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {D.dispatch(~T, ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.Remove{E.H{owner, id, g}}) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})) : D.DList<T> & E.Obs<T>}:
63 +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, HR.lt_t(id, fresh, hlt))
64 +e2 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, z)), U32.is_eq(owner, tag), True{}, ho)
65 +e3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, D.DList<T> & E.Obs<T>, r => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, r)), Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), LN.vget(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt)))
66 +e4 = Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv)
67 Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, U32.is_eq(owner, tag))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.remove_checked(~T, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, True{})), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e2, Equal.trans(D.DList<T> & E.Obs<T>, D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id))), D.removed(~T, tag, depth, cap, AR.thaw(U32, gT), id, g, R.rm_found(~T, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), D.failed(~T, E.Remove{E.H{owner, id, g}}, E.StaleHandle{})), e3, e4)))
68
69# ---- insert before / after ----
70
71
72def ins_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:
73 Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, HR.lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, False{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, z)), U32.is_eq(owner, tag), True{}, ho))
74
75def ins_pre(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))) == D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))) : D.DList<T> & E.Obs<T>}:
76 +e1 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, z, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, HR.lt_t(id, fresh, hlt))
77 +e2 = Equal.cong(Bool, D.DList<T> & E.Obs<T>, z => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, z)), U32.is_eq(owner, tag), True{}, ho)
78 +e3 = Equal.cong(Array<Maybe<&2, T>> & Maybe<&2, T>, D.DList<T> & E.Obs<T>, r => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, r)), Array.get(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, vT), id), (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), LN.vget(T, depth, ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), vT, ST.g_cpv(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, hlt)))
79 Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e1, Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, True{}, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, True{})), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), e2, e3))
80
81def ins_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.goodF(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl) == True{} : Bool}, +owner: U32, +id: U32, +g: U32, +x: T, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}, +hv: {S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)) == None{} : Maybe<&2, T>}) -> {D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}) : D.DList<T> & E.Obs<T>}:
82 Equal.trans(D.DList<T> & E.Obs<T>, D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.insert_checked_reuse(~T, af, U32.is_lt(id, fresh), tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, U32.is_eq(owner, tag))), D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.OInsert{Fail{E.StaleHandle{}}}), ins_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, af, ho, hlt), Equal.cong(Maybe<&2, T>, D.DList<T> & E.Obs<T>, m => D.relative_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.ins_found_reuse(~T, af, tag, fresh, free, SC.length(Nat, sl), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, x, (AR.thaw(Maybe<&2, T>, vT), m))), S.val_of(T, AR.slots(Maybe<&2, T>, vT), UD.v(id)), None{}, hv))
83
84# the relative insertion's result is the insertion's
85def rel_done(~T: Data, +tag: U32, +depth: Nat, +cap: U32, -gens: Array<U32>, r: R.DList<T> & I.Handle) -> {D.relative_result(~T, tag, depth, cap, gens, R.done_handle(~T, r)) == D.relative_done(~T, D.inserted(~T, tag, depth, cap, gens, r)) : D.DList<T> & E.Obs<T>}:
86 match r:
87 case Tuple{raw, I.H{o, +i}}:
88 {==}
89
90# a handle result mapped to an observation
91def pok_ins(~T: Data, -sp: S.DS<T> & E.Handle, -rr: D.DList<T> & E.Handle, p: OK.POK(~T, E.Handle, sp, rr)) -> OK.POK(~T, E.Obs<T>, S.ins_obs(T, sp), D.relative_done(~T, rr)):
92 match p:
93 case Tuple{+sh2, Tuple{+o, Tuple{+er, Tuple{+es, hg2}}}}:
94 (sh2, (E.OInsert{Done{o}}, (Equal.cong(D.DList<T> & E.Handle, D.DList<T> & E.Obs<T>, r => D.relative_done(~T, r), rr, (ST.real(~T, sh2), o), er), (Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.ins_obs(T, r), sp, (ST.model(~T, sh2), o), es), hg2))))
95
96def pok_push(~T: Data, -sp: S.DS<T> & E.Handle, -rr: D.DList<T> & E.Handle, p: OK.POK(~T, E.Handle, sp, rr)) -> OK.POK(~T, E.Obs<T>, S.pushed(T, sp), D.pushed_obs(~T, rr)):
97 match p:
98 case Tuple{+sh2, Tuple{+o, Tuple{+er, Tuple{+es, hg2}}}}:
99 (sh2, (E.OHandle{o}, (Equal.cong(D.DList<T> & E.Handle, D.DList<T> & E.Obs<T>, r => D.pushed_obs(~T, r), rr, (ST.real(~T, sh2), o), er), (Equal.cong(S.DS<T> & E.Handle, S.DS<T> & E.Obs<T>, r => S.pushed(T, r), sp, (ST.model(~T, sh2), o), es), hg2))))
100
101# the specification's placement is the placement between a and b
102def ins_pos(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T, +pos: S.Pos, +a: List<&2, Nat>, +b: List<&2, Nat>, e: @+n: Nat -> {S.place_order(pos, order, n) == SC.append(Nat, a, Con{n, b}) : List<&2, Nat>}) -> {S.inserted(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, pos) == IP.insAB(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, a, b) : S.DS<T> & E.Handle}:
103 match free:
104 case Nil{}:
105 Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, SC.snoc(Maybe<&2, T>, vals, None{}), SC.length(Maybe<&2, T>, vals), Some{x}), SC.snoc(U32, gens, 0), Nil{}}, S.handle(tag, SC.snoc(U32, gens, 0), SC.length(Maybe<&2, T>, vals))), S.place_order(pos, order, SC.length(Maybe<&2, T>, vals)), SC.append(Nat, a, Con{SC.length(Maybe<&2, T>, vals), b}), e(SC.length(Maybe<&2, T>, vals)))
106 case Con{+i, +rest}:
107 Equal.cong(List<&2, Nat>, S.DS<T> & E.Handle, z => (S.DS{tag, z, SC.update(Maybe<&2, T>, vals, i, Some{x}), gens, rest}, S.handle(tag, gens, i)), S.place_order(pos, order, i), SC.append(Nat, a, Con{i, b}), e(i))
108
109def ib_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +n: Nat, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.ins_before(SC.append(Nat, a, Con{s, b}), s, n) == SC.append(Nat, a, Con{n, Con{s, b}}) : List<&2, Nat>}:
110 match a:
111 case Nil{}:
112 Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{n, Con{s, b}}, Con{s, S.ins_before(b, s, n)}), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))
113 case Con{+y, +t}:
114 Equal.trans(List<&2, Nat>, S.ins_before(SC.append(Nat, Con{y, t}, Con{s, b}), s, n), Con{y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n)}, SC.append(Nat, Con{y, t}, Con{n, Con{s, b}}), Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{n, Con{y, SC.append(Nat, t, Con{s, b})}}, Con{y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n)}), Nat.is_eq(y, s), False{}, NL.or_ff_l(Nat.is_eq(y, s), NL.memn(s, t), h)), LL.cons_cong(Nat, y, S.ins_before(SC.append(Nat, t, Con{s, b}), s, n), SC.append(Nat, t, Con{n, Con{s, b}}), ib_mid(t, s, b, n, NL.or_ff_r(Nat.is_eq(y, s), NL.memn(s, t), h))))
115
116def ia_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +n: Nat, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.ins_after(SC.append(Nat, a, Con{s, b}), s, n) == SC.append(Nat, a, Con{s, Con{n, b}}) : List<&2, Nat>}:
117 match a:
118 case Nil{}:
119 Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{s, Con{n, b}}, Con{s, S.ins_after(b, s, n)}), Nat.is_eq(s, s), True{}, N.is_eq_refl(s))
120 case Con{+y, +t}:
121 Equal.trans(List<&2, Nat>, S.ins_after(SC.append(Nat, Con{y, t}, Con{s, b}), s, n), Con{y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n)}, SC.append(Nat, Con{y, t}, Con{s, Con{n, b}}), Equal.cong(Bool, List<&2, Nat>, z => S.pick_list(z, Con{y, Con{n, SC.append(Nat, t, Con{s, b})}}, Con{y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n)}), Nat.is_eq(y, s), False{}, NL.or_ff_l(Nat.is_eq(y, s), NL.memn(s, t), h)), LL.cons_cong(Nat, y, S.ins_after(SC.append(Nat, t, Con{s, b}), s, n), SC.append(Nat, t, Con{s, Con{n, b}}), ia_mid(t, s, b, n, NL.or_ff_r(Nat.is_eq(y, s), NL.memn(s, t), h))))