1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/array.bend as AR 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/doubly_linked_list.bend as S 7 import ../../lib/u32div.bend as UD 8 import ../../../src/containers/doubly_linked_list.bend as D 9 import ../../../src/containers/internal/dlist_storage.bend as R 10 import ../../../src/containers/types/internal_dlist.bend as I 11 import ../../../src/containers/types/doubly_linked_list.bend as E 12 import ./state.bend as ST 13 import ./rel.bend as RL 14 import ./vals.bend as VA 15 import ./link.bend as LN 16 import ./ok.bend as OK 17 import ./hrd.bend as HR 18 import ../../lib/nat_list.bend as NL 19 import ../../lib/links.bend as LK 20 import ../../lib/words32.bend as W32 21 import ../../lib/u32_tree.bend as UT 22 23 # next and prev on a handle: the neighbour links of a live element. 24 25 26 # ---- the specification's neighbours in a list without repeats ---- 27 28 def after_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.after(SC.append(Nat, a, Con{s, b}), s) == S.first(b) : Maybe<&2, Nat>}: 29 match a: 30 case Nil{}: 31 Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, S.first(b), S.after(b, s)), Nat.is_eq(s, s), True{}, N.is_eq_refl(s)) 32 case Con{+x, +t}: 33 Equal.trans(Maybe<&2, Nat>, S.after(SC.append(Nat, Con{x, t}, Con{s, b}), s), S.after(SC.append(Nat, t, Con{s, b}), s), S.first(b), Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, S.first(SC.append(Nat, t, Con{s, b})), S.after(SC.append(Nat, t, Con{s, b}), s)), Nat.is_eq(x, s), False{}, NL.or_ff_l(Nat.is_eq(x, s), NL.memn(s, t), h)), after_mid(t, s, b, NL.or_ff_r(Nat.is_eq(x, s), NL.memn(s, t), h))) 34 35 def bm(a: List<&2, Nat>, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>: 36 match a: 37 case Nil{}: 38 p 39 case Con{+x, t}: 40 bm(t, Some{x}) 41 42 def before_mid(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>, +h: {NL.memn(s, a) == False{} : Bool}) -> {S.before(SC.append(Nat, a, Con{s, b}), s, p) == bm(a, p) : Maybe<&2, Nat>}: 43 match a: 44 case Nil{}: 45 Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, p, S.before(b, s, Some{s})), Nat.is_eq(s, s), True{}, N.is_eq_refl(s)) 46 case Con{+x, +t}: 47 Equal.trans(Maybe<&2, Nat>, S.before(SC.append(Nat, Con{x, t}, Con{s, b}), s, p), S.before(SC.append(Nat, t, Con{s, b}), s, Some{x}), bm(t, Some{x}), Equal.cong(Bool, Maybe<&2, Nat>, z => S.pick_maybe(z, p, S.before(SC.append(Nat, t, Con{s, b}), s, Some{x})), Nat.is_eq(x, s), False{}, NL.or_ff_l(Nat.is_eq(x, s), NL.memn(s, t), h)), before_mid(t, s, b, Some{x}, NL.or_ff_r(Nat.is_eq(x, s), NL.memn(s, t), h))) 48 49 def bm_last(+t: List<&2, Nat>, +x: Nat) -> {bm(t, Some{x}) == Some{NL.lastn(t, x)} : Maybe<&2, Nat>}: 50 match t: 51 case Nil{}: 52 {==} 53 case Con{+y, +t2}: 54 bm_last(t2, y) 55 56 # ---- the storage's checks ---- 57 58 59 def nb_hi(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == False{} : Bool}) -> {D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}) : D.DList & E.Obs}: 60 Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}), Equal.cong(Bool, D.DList & E.Obs, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), False{}, HR.lt_f(id, fresh, hlt)), Equal.cong(Bool, D.DList & E.Obs, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, z)), U32.is_eq(owner, tag), True{}, ho)) 61 62 def nb_pre(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +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, +af: Bool, +ho: {U32.is_eq(owner, tag) == True{} : Bool}, +hlt: {Nat.is_lt(UD.v(id), UD.v(fresh)) == True{} : Bool}) -> {D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))) == D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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))))) : D.DList & E.Obs}: 63 +e1 = Equal.cong(Bool, D.DList & E.Obs, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), U32.is_lt(id, fresh), True{}, HR.lt_t(id, fresh, hlt)) 64 +e2 = Equal.cong(Bool, D.DList & E.Obs, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, z)), U32.is_eq(owner, tag), True{}, ho) 65 +e3 = Equal.cong(Array> & Maybe<&2, T>, D.DList & E.Obs, r => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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 Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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))))), e1, Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, True{})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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))))), e2, e3)) 67 68 def nb_none_c(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +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, +af: Bool) -> {D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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), None{}))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}) : D.DList & E.Obs}: 69 match af: 70 case True{}: 71 {==} 72 case False{}: 73 {==} 74 75 def nb_none(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +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, +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.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))) == (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}) : D.DList & E.Obs}: 76 Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_checked(~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, U32.is_eq(owner, tag))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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}), E.ONbr{Fail{E.StaleHandle{}}}), nb_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, af, ho, hlt), Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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), None{}))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Fail{E.StaleHandle{}}}), Equal.cong(Maybe<&2, T>, D.DList & E.Obs, m => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, af, 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), nb_none_c(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, af))) 77 78 # ---- the neighbour's handle ---- 79 80 81 def x_lt(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +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: Nat, +hx: {Nat.is_lt(x, UD.v(fresh)) == True{} : Bool}) -> {Nat.is_lt(x, SC.pow2(depth)) == True{} : Bool}: 82 +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)) 83 N.lt_le_trans(x, UD.v(fresh), SC.pow2(depth), hx, 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))) 84 85 86 # the link of a live id: its handle with its generation 87 def nb_link(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +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}, +x: Nat, +hxf: {Nat.is_lt(x, UD.v(fresh)) == True{} : Bool}) -> OK.POK(~T, E.Obs, (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), Some{x})}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle(tag, LK.lnk(x))}))): 88 +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg) 89 +hn = x_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl, hg, owner, id, g, x, hxf) 90 +ev = LN.fn_v(x, depth, hd, hn) 91 +e1 = Equal.cong(Bool, D.DList & E.Obs, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle_go(tag, LK.lnk(x), z)})), U32.is_eq(LK.lnk(x), 0), False{}, RL.lnk_nz(one, h1, x, depth, hd, hn)) 92 +e2 = Equal.cong(U32, D.DList & E.Obs, z => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{Some{I.H{tag, z}}})), R.slot(LK.lnk(x)), U32.from_nat(x), LN.slot_fn(one, h1, x, depth, hd, hn)) 93 +e3 = Equal.cong(Array & U32, D.DList & E.Obs, r => D.neighbour_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)}, tag, U32.from_nat(x), r), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(x)), (AR.thaw(U32, gT), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(x)))), 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), U32.from_nat(x), LN.fn_lt(x, depth, hd, hn))) 94 +e4 = Equal.cong(Nat, D.DList & E.Obs, z => (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), z)}}}}), UD.v(U32.from_nat(x)), x, ev) 95 +er = Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle(tag, LK.lnk(x))})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{Some{I.H{tag, R.slot(LK.lnk(x))}}})), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), x)}}}}), e1, Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{Some{I.H{tag, R.slot(LK.lnk(x))}}})), D.neighbour_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)}, tag, U32.from_nat(x), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(x))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), x)}}}}), e2, Equal.trans(D.DList & E.Obs, D.neighbour_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)}, tag, U32.from_nat(x), Array.get(U32, AR.thaw(U32, gT), U32.from_nat(x))), D.neighbour_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)}, tag, U32.from_nat(x), (AR.thaw(U32, gT), W32.nth0(AR.slots(U32, gT), UD.v(U32.from_nat(x))))), (ST.real(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{ 96 +es = Equal.cong(U32, S.DS & E.Obs, z => (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), z}}}}), S.gen_of(SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), x), W32.nth0(AR.slots(U32, gT), x), VA.gen_take(AR.slots(U32, gT), UD.v(fresh), x, hxf)) 97 (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.ONbr{Done{Some{E.H{tag, U32.from_nat(x), W32.nth0(AR.slots(U32, gT), x)}}}}, (er, (es, hg)))) 98 99 def nb_nil(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +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, (ST.model(~T, ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), None{})}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (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)}, Done{R.handle(tag, 0)}))): 100 (ST.LS{tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, sl, fl}, (E.ONbr{Done{None{}}}, ({==}, ({==}, hg)))) 101 102 # ---- next ---- 103 104 105 def nx_fin(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {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}, +one: Nat, +h1: {one == 1n : Nat}, +hb: {ST.slok(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}) -> OK.POK(~T, E.Obs, (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), S.first(b))}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))}))): 106 match b: 107 case Nil{}: 108 nb_nil(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g) 109 case Con{+b0, +t}: 110 nb_link(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, one, h1, b0, L.and_left(Nat.is_lt(b0, UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), b0), L.and_left(Bool.and(Nat.is_lt(b0, UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), b0)), ST.slok(~T, t, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), hb))) 111 112 def pv_fin(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {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}, +one: Nat, +h1: {one == 1n : Nat}, +ha: {ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}) -> OK.POK(~T, E.Obs, (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), bm(a, None{}))}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))}))): 113 match a: 114 case Nil{}: 115 nb_nil(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g) 116 case Con{+a0, +t}: 117 +z = NL.lastn(t, a0) 118 +hz = L.and_left(Nat.is_lt(z, UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), z), RL.slok_mem(~T, z, Con{a0, t}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT), ha, NL.lastn_mem(t, a0))) 119 p = nb_link(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, one, h1, z, hz) 120 OK.pok_eq(~T, E.Obs, (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), bm(Con{a0, t}, None{}))}}), (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), Some{z})}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(Con{a0, t}, 0))})), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.lnk(z))})), Equal.cong(Maybe<&2, Nat>, S.DS & E.Obs, m => (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), m)}}), bm(t, Some{a0}), Some{z}, bm_last(t, a0)), Equal.cong(U32, D.DList & E.Obs, l => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, l)})), LK.last_or(t, LK.lnk(a0)), LK.lnk(z), LK.last_lnk(t, a0)), p) 121 122 123 def ab_facts_a(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {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}) -> {ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}: 124 L.and_left(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), RL.to_eq(ST.slok(~T, SC.append(Nat, a, Con{UD.v(id), b}), UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))) 125 126 def ab_facts_b(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {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}) -> {ST.slok(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}: 127 +h = L.and_right(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), RL.to_eq(ST.slok(~T, SC.append(Nat, a, Con{UD.v(id), b}), UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, Con{UD.v(id), b}, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), ST.g_csl(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))) 128 L.and_right(Bool.and(Nat.is_lt(UD.v(id), UD.v(fresh)), ST.live(T, AR.slots(Maybe<&2, T>, vT), UD.v(id))), ST.slok(~T, b, UD.v(fresh), AR.slots(Maybe<&2, T>, vT)), h) 129 130 def i_off_a(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {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}) -> {NL.memn(UD.v(id), a) == False{} : Bool}: 131 NL.nd_dj(a, Con{UD.v(id), b}, ST.g_cnd(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), UD.v(id), RL.self_in(UD.v(id), b)) 132 133 def nx_ab(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {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}, +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>}) -> OK.POK(~T, E.Obs, 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}), 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, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Next{E.H{owner, id, g}})): 134 +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg) 135 +e0 = nb_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, True{}, ho, hlt) 136 +e1 = Equal.cong(Maybe<&2, T>, D.DList & E.Obs, m => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 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)), Some{vv}, hv) 137 +e2 = Equal.cong(Array & U32, D.DList & E.Obs, r => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_n(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), r)), Array.get(U32, AR.thaw(U32, nT), id), (AR.thaw(U32, nT), W32.nth0(AR.slots(U32, nT), UD.v(id))), UT.uget(depth, RL.hd0(depth, hd), nT, ST.g_cpn(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, hlt))) 138 +e3 = Equal.cong(U32, D.DList & E.Obs, l => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, l)})), W32.nth0(AR.slots(U32, nT), UD.v(id)), LK.fst_or(b, 0), RL.unl_n(AR.slots(U32, pT), AR.slots(U32, nT), a, UD.v(id), b, ST.g_cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))) 139 +er = Equal.trans(D.DList & E.Obs, 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}), E.Next{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 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))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))})), e0, Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 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))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))})), e1, Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, True{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, 140 +es = Equal.cong(Maybe<&2, Nat>, S.DS & E.Obs, m => (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), m)}}), S.after(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id)), S.first(b), after_mid(a, UD.v(id), b, i_off_a(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg))) 141 OK.pok_eq(~T, E.Obs, 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}), E.Next{E.H{owner, id, g}}, UD.v(id)), (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), S.first(b))}}), 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}), E.Next{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.fst_or(b, 0))})), es, er, nx_fin(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, one, h1, ab_facts_b(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg))) 142 143 def pv_ab(~T: Data, +tag: U32, +cap: U32, +fresh: U32, +free: U32, +head: U32, +tail: U32, +depth: Nat, +vT: AR.Tree>, +pT: AR.Tree, +nT: AR.Tree, +gT: AR.Tree, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +owner: U32, +id: U32, +g: U32, +hg: {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}, +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>}) -> OK.POK(~T, E.Obs, 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}), 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, SC.append(Nat, a, Con{UD.v(id), b}), fl}), E.Prev{E.H{owner, id, g}})): 144 +hd = ST.g_cdep(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg) 145 +e0 = nb_pre(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, False{}, ho, hlt) 146 +e1 = Equal.cong(Maybe<&2, T>, D.DList & E.Obs, m => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 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)), Some{vv}, hv) 147 +e2 = Equal.cong(Array & U32, D.DList & E.Obs, r => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_p(~T, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, nT), r)), Array.get(U32, AR.thaw(U32, pT), id), (AR.thaw(U32, pT), W32.nth0(AR.slots(U32, pT), UD.v(id))), UT.uget(depth, RL.hd0(depth, hd), pT, ST.g_cpp(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg), id, HR.i_lt(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg, owner, id, g, hlt))) 148 +e3 = Equal.cong(U32, D.DList & E.Obs, l => D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, l)})), W32.nth0(AR.slots(U32, pT), UD.v(id)), LK.last_or(a, 0), RL.unl_p(AR.slots(U32, pT), AR.slots(U32, nT), a, UD.v(id), b, ST.g_cseg(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, SC.append(Nat, a, Con{UD.v(id), b}), fl, hg))) 149 +er = Equal.trans(D.DList & E.Obs, 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}), E.Prev{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 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))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))})), e0, Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), 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))))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))})), e1, Equal.trans(D.DList & E.Obs, D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), R.nbr_read(~T, False{}, tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(U32, pT), AR.thaw(U32, nT), id, (AR.thaw(Maybe<&2, T>, vT), Some{vv}))), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, 150 +es = Equal.cong(Maybe<&2, Nat>, S.DS & E.Obs, m => (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), m)}}), S.before(SC.append(Nat, a, Con{UD.v(id), b}), UD.v(id), None{}), bm(a, None{}), before_mid(a, UD.v(id), b, None{}, i_off_a(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg))) 151 OK.pok_eq(~T, E.Obs, 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}), E.Prev{E.H{owner, id, g}}, UD.v(id)), (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}), E.ONbr{Done{S.nbr(tag, SC.take(U32, AR.slots(U32, gT), UD.v(fresh)), bm(a, None{}))}}), 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}), E.Prev{E.H{owner, id, g}}), D.neighbour_result(~T, tag, depth, cap, AR.thaw(U32, gT), (R.DL{tag, fresh, free, SC.length(Nat, SC.append(Nat, a, Con{UD.v(id), b})), head, tail, depth, cap, AR.thaw(Maybe<&2, T>, vT), AR.thaw(U32, pT), AR.thaw(U32, nT)}, Done{R.handle(tag, LK.last_or(a, 0))})), es, er, pv_fin(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg, one, h1, ab_facts_a(~T, tag, cap, fresh, free, head, tail, depth, vT, pT, nT, gT, a, b, fl, owner, id, g, hg)))