~/jendhub

proofs/containers/doubly_linked_list/insg.bend

bend-collections-laws-containers@1.0.0.0 · 101 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/proofs/lib/u32div.bend as UD
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/links.bend as LK
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/rel.bend as RL
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/vals.bend as VA
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/lv.bend as LV
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LKx
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
16
17# The invariant after an id is linked in (the ready state: after any growth
18# or free-stack pop, before the link).
19
20
21# nn off a ++ b is off a and off b
22def off_l(+nn: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}) -> {NL.memn(nn, a) == False{} : Bool}:
23  NL.or_ff_l(NL.memn(nn, a), NL.memn(nn, b), L.subst(Bool, z => {z == False{} : Bool}, NL.memn(nn, SC.append(Nat, a, b)), Bool.or(NL.memn(nn, a), NL.memn(nn, b)), NL.memn_app(nn, a, b), h))
24
25def off_r(+nn: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}) -> {NL.memn(nn, b) == False{} : Bool}:
26  NL.or_ff_r(NL.memn(nn, a), NL.memn(nn, b), L.subst(Bool, z => {z == False{} : Bool}, NL.memn(nn, SC.append(Nat, a, b)), Bool.or(NL.memn(nn, a), NL.memn(nn, b)), NL.memn_app(nn, a, b), h))
27
28def len_is(-X: Data, +xs: List<&2, X>, +m: Nat, +e: {SC.length(X, xs) == m : Nat}, +i: Nat, +h: {Nat.is_lt(i, m) == True{} : Bool}) -> {Nat.is_lt(i, SC.length(X, xs)) == True{} : Bool}:
29  L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, m, SC.length(X, xs), Equal.sym(Nat, SC.length(X, xs), m, e), h)
30
31def fst_len(+b: List<&2, Nat>, +xs: List<&2, U32>, +m: Nat, +e: {SC.length(U32, xs) == m : Nat}, +h: {RL.fstlt(b, m) == True{} : Bool}) -> {RL.fstlt(b, SC.length(U32, xs)) == True{} : Bool}:
32  L.subst(Nat, z => {RL.fstlt(b, z) == True{} : Bool}, m, SC.length(U32, xs), Equal.sym(Nat, SC.length(U32, xs), m, e), h)
33
34def last_len(+a: List<&2, Nat>, +xs: List<&2, U32>, +m: Nat, +e: {SC.length(U32, xs) == m : Nat}, +h: {RL.lastlt(a, m) == True{} : Bool}) -> {RL.lastlt(a, SC.length(U32, xs)) == True{} : Bool}:
35  L.subst(Nat, z => {RL.lastlt(a, z) == True{} : Bool}, m, SC.length(U32, xs), Equal.sym(Nat, SC.length(U32, xs), m, e), h)
36
37
38# the links of the new lists, from the list-level theorem
39def ig_seg(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: U32, +d: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +nn: Nat, +x: T, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +pn: {AR.perfect(U32, d, nT) == True{} : Bool}, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == True{} : Bool}, +hs: {ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.seg(AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), SC.append(Nat, a, Con{nn, b}), 0, 0) == True{} : Bool}:
40  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)
41  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)
42  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)
43  +hsp = RL.to_eq(ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsl)
44  +hfb = RL.fstlt_of(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_right(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))
45  +hla = RL.lastlt_of(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_left(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))
46  +lp = AR.slots_length(U32, d, pT, pp)
47  +ln = AR.slots_length(U32, d, nT, pn)
48  +lpm = Equal.trans(Nat, SC.length(U32, SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0))), SC.length(U32, AR.slots(U32, pT)), SC.pow2(d), LL.length_update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), lp)
49  +lnm = Equal.trans(Nat, SC.length(U32, SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0))), SC.length(U32, AR.slots(U32, nT)), SC.pow2(d), LL.length_update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), ln)
50  +hl = RL.ins_seg(AR.slots(U32, pT), AR.slots(U32, nT), a, b, nn, hs, hnd, off_l(nn, a, b, hns), off_r(nn, a, b, hns), len_is(U32, AR.slots(U32, pT), SC.pow2(d), lp, nn, hn), len_is(U32, AR.slots(U32, nT), SC.pow2(d), ln, nn, hn), fst_len(b, SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), SC.pow2(d), lpm, hfb), last_len(a, SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), SC.pow2(d), lnm, hla))
51  +esp = Equal.trans(List<&2, U32>, AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), RL.upd_first(AR.slots(U32, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0))), b, LKx.lnk(nn)), RL.upd_first(SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tf_s(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), UT.uset_p(d, pT, pp, nn, LKx.last_or(a, 0)), b, hfb, LKx.lnk(nn)), Equal.cong(List<&2, U32>, List<&2, U32>, z => RL.upd_first(z, b, LKx.lnk(nn)), AR.slots(U32, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0))), SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), UT.uset_s(d, pT, pp, nn, hn, LKx.last_or(a, 0))))
52  +esn = Equal.trans(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), a, LKx.lnk(nn)), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), RL.tl_s(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), UT.uset_p(d, nT, pn, nn, LKx.fst_or(b, 0)), a, hla, LKx.lnk(nn)), Equal.cong(List<&2, U32>, List<&2, U32>, z => RL.upd_last(z, a, LKx.lnk(nn)), AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), UT.uset_s(d, nT, pn, nn, hn, LKx.fst_or(b, 0))))
53  +h2 = L.subst(List<&2, U32>, z => {ST.seg(z, RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), SC.append(Nat, a, Con{nn, b}), 0, 0) == True{} : Bool}, RL.upd_first(SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), RL.upd_first(SC.update(U32, AR.slots(U32, pT), nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), esp), hl)
54  L.subst(List<&2, U32>, z => {ST.seg(AR.slots(U32, RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn))), z, SC.append(Nat, a, Con{nn, b}), 0, 0) == True{} : Bool}, RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), esn), h2)
55
56
57# the free stack is off the writes
58def ig_fll(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: U32, +d: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +nn: Nat, +x: T, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +pn: {AR.perfect(U32, d, nT) == True{} : Bool}, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == True{} : Bool}, +hs: {ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.fll(AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), fl) == True{} : Bool}:
59  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)
60  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)
61  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)
62  +hsp = RL.to_eq(ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsl)
63  +hla = RL.lastlt_of(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT), SC.pow2(d), hfr2, L.and_left(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))
64  +esn = Equal.trans(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), a, LKx.lnk(nn)), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), RL.tl_s(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), UT.uset_p(d, nT, pn, nn, LKx.fst_or(b, 0)), a, hla, LKx.lnk(nn)), Equal.cong(List<&2, U32>, List<&2, U32>, z => RL.upd_last(z, a, LKx.lnk(nn)), AR.slots(U32, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0))), SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), UT.uset_s(d, nT, pn, nn, hn, LKx.fst_or(b, 0))))
65  +e1 = RL.fll_lfn(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn), fl, LV.lin_vac(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT), fl, hsl, hfl))
66  +e2 = LK.fll_fn(AR.slots(U32, nT), nn, LKx.fst_or(b, 0), fl, hnfl)
67  +h2 = RL.by_eq(ST.fll(RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), fl), ST.fll(AR.slots(U32, nT), fl), Equal.trans(Bool, ST.fll(RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), fl), ST.fll(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), fl), ST.fll(AR.slots(U32, nT), fl), e1, e2), hfll)
68  L.subst(List<&2, U32>, z => {ST.fll(z, fl) == True{} : Bool}, RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), Equal.sym(List<&2, U32>, AR.slots(U32, RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn))), RL.upd_last(SC.update(U32, AR.slots(U32, nT), nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), esn), h2)
69
70# the value facts over the written value list
71def ig_sl(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: U32, +d: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +nn: Nat, +x: T, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +pn: {AR.perfect(U32, d, nT) == True{} : Bool}, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == True{} : Bool}, +hs: {ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.slok(~T, SC.append(Nat, a, Con{nn, b}), UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})) == True{} : Bool}:
72  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)
73  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)
74  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)
75  +hlv0 = len_is(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), SC.pow2(d), AR.slots_length(Maybe<&2, T>, d, vT, pv), nn, hn)
76  +hsp = RL.to_eq(ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)), Bool.and(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT))), RL.slok_app(~T, a, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsl)
77  +sa = LV.slok_upd(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hlv0, {==}, L.and_left(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))
78  +sb = LV.slok_upd(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hlv0, {==}, L.and_right(ST.slok(~T, a, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), ST.slok(~T, b, UD.v(fr), AR.slots(Maybe<&2, T>, vT)), hsp))
79  +sn = L.and_intro(Nat.is_lt(nn, UD.v(fr)), ST.live(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), nn), hnf, RL.by_eq(ST.live(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), nn), True{}, LV.live_same(T, AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hlv0), {==}))
80  RL.by_eq(ST.slok(~T, SC.append(Nat, a, Con{nn, b}), UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), Bool.and(ST.slok(~T, a, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), ST.slok(~T, Con{nn, b}, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}))), RL.slok_app(~T, a, Con{nn, b}, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), L.and_intro(ST.slok(~T, a, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), ST.slok(~T, Con{nn, b}, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), sa, L.and_intro(Bool.and(Nat.is_lt(nn, UD.v(fr)), ST.live(T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), nn)), ST.slok(~T, b, UD.v(fr), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x})), sn, sb)))
81
82def ig_lv(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: U32, +d: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +nn: Nat, +x: T, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +pn: {AR.perfect(U32, d, nT) == True{} : Bool}, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == True{} : Bool}, +hs: {ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.lvin(~T, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), 0n, SC.append(Nat, a, Con{nn, b})) == True{} : Bool}:
83  +hm = RL.by_eq(NL.memn(nn, SC.append(Nat, a, Con{nn, b})), Bool.or(NL.memn(nn, SC.append(Nat, a, b)), Nat.is_eq(nn, nn)), NL.memn_mid(nn, a, nn, b), NL.or_tr(NL.memn(nn, SC.append(Nat, a, b)), Nat.is_eq(nn, nn), N.is_eq_refl(nn)))
84  VA.lvin_upd(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, Con{nn, b}), nn, Some{x}, VA.lvin_sub(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b), SC.append(Nat, a, Con{nn, b}), hlv, VA.subn_ins(a, b, nn)), hm)
85
86# THEOREM: the linked state keeps the invariant
87def ins_good(~T: Data, +one: Nat, +h1: {one == 1n : Nat}, +tag: U32, +cap: U32, +fr: U32, +free: U32, +d: Nat, +vT: AR.Tree<Maybe<&2, T>>, +pT: AR.Tree<U32>, +nT: AR.Tree<U32>, +gT: AR.Tree<U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +fl: List<&2, Nat>, +nn: Nat, +x: T, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}, +pv: {AR.perfect(Maybe<&2, T>, d, vT) == True{} : Bool}, +pp: {AR.perfect(U32, d, pT) == True{} : Bool}, +pn: {AR.perfect(U32, d, nT) == True{} : Bool}, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +hfr: {Nat.is_le(UD.v(fr), UD.v(cap)) == True{} : Bool}, +hnf: {Nat.is_lt(nn, UD.v(fr)) == True{} : Bool}, +hs: {ST.seg(AR.slots(U32, pT), AR.slots(U32, nT), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hns: {NL.memn(nn, SC.append(Nat, a, b)) == False{} : Bool}, +hsl: {ST.slok(~T, SC.append(Nat, a, b), UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfree: {U32.is_eq(free, LKx.fst_or(fl, 0)) == True{} : Bool}, +hfll: {ST.fll(AR.slots(U32, nT), fl) == True{} : Bool}, +hfl: {ST.flok(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT)) == True{} : Bool}, +hfnd: {NL.nodupn(fl) == True{} : Bool}, +hnfl: {NL.memn(nn, fl) == False{} : Bool}, +hgz: {ST.gz(AR.slots(U32, gT), UD.v(fr)) == True{} : Bool}, +hlv: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, SC.append(Nat, a, b)) == True{} : Bool}) -> {ST.goodF(~T, tag, cap, fr, free, LKx.fst_or(SC.append(Nat, a, Con{nn, b}), 0), LKx.last_or(SC.append(Nat, a, Con{nn, b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), gT, SC.append(Nat, a, Con{nn, b}), fl) == True{} : Bool}:
88  +e2d = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)
89  +hfr2 = L.subst(Nat, z => {Nat.is_le(UD.v(fr), z) == True{} : Bool}, UD.v(cap), SC.pow2(d), e2d, hfr)
90  +hn = N.lt_le_trans(nn, UD.v(fr), SC.pow2(d), hnf, hfr2)
91  +esv = AR.upd_slots(Maybe<&2, T>, d, vT, nn, Some{x}, hn, pv)
92  +hsg = ig_seg(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)
93  +hfl2 = ig_fll(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)
94  +s1 = ig_sl(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)
95  +s2 = LV.flok_off(~T, fl, UD.v(fr), AR.slots(Maybe<&2, T>, vT), nn, Some{x}, hnfl, hfl)
96  +s3 = ig_lv(~T, one, h1, tag, cap, fr, free, d, vT, pT, nT, gT, a, b, fl, nn, x, hd, hcap, pv, pp, pn, pg, hfr, hnf, hs, hnd, hns, hsl, hfree, hfll, hfl, hfnd, hnfl, hgz, hlv)
97  +r1 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.slok(~T, SC.append(Nat, a, Con{nn, b}), UD.v(fr), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), esv), s1)
98  +r2 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.flok(~T, fl, UD.v(fr), z) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), esv), s2)
99  +r3 = L.subst(List<&2, Maybe<&2, T>>, z => {ST.lvin(~T, z, 0n, SC.append(Nat, a, Con{nn, b})) == True{} : Bool}, SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x})), SC.update(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), nn, Some{x}), esv), s3)
100  +hnd2 = RL.by_eq(NL.nodupn(SC.append(Nat, a, Con{nn, b})), Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(nn, SC.append(Nat, a, b)))), NL.nd_mid(a, nn, b), L.and_intro(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(nn, SC.append(Nat, a, b))), hnd, NL.not_f(NL.memn(nn, SC.append(Nat, a, b)), hns)))
101  ST.good_intro(~T, tag, cap, fr, free, LKx.fst_or(SC.append(Nat, a, Con{nn, b}), 0), LKx.last_or(SC.append(Nat, a, Con{nn, b}), 0), d, AR.upd(Maybe<&2, T>, d, vT, nn, Some{x}), RL.tu_first(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tu_last(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), gT, SC.append(Nat, a, Con{nn, b}), fl, hd, hcap, AR.upd_perfect(Maybe<&2, T>, d, vT, nn, Some{x}, pv), RL.tf_p(d, AR.upd(U32, d, pT, nn, LKx.last_or(a, 0)), UT.uset_p(d, pT, pp, nn, LKx.last_or(a, 0)), b, LKx.lnk(nn)), RL.tl_p(d, AR.upd(U32, d, nT, nn, LKx.fst_or(b, 0)), UT.uset_p(d, nT, pn, nn, LKx.fst_or(b, 0)), a, LKx.lnk(nn)), pg, hfr, hsg, LKx.u_refl(LKx.fst_or(SC.append(Nat, a, Con{nn, b}), 0)), LKx.u_refl(LKx.last_or(SC.append(Nat, a, Con{nn, b}), 0)), hnd2, r1, hfree, hfl2, r2, hfnd, hgz, r3)