proofs/containers/balanced_search_tree/prim.bend
bend-collections-laws-containers@1.0.0.0 · 140 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
6import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as D
7import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as DE
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/da.bend as DA
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/arr.bend as AB
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsl.bend as NSL
12
13# The TreeMap's node and payload accesses over the shadow: a read returns
14# the list's node, a write or exchange updates the list in range.
15
16
17def or_else(-X: Data, m: Maybe<&2, X>, +dv: X) -> X:
18 match m:
19 case None{}:
20 dv
21 case Some{x}:
22 x
23
24def nth_or_nth(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X) -> {ST.nth_or(X, xs, i, dv) == or_else(X, SC.nth(X, xs, i), dv) : X}:
25 match xs i:
26 case Nil{} _:
27 {==}
28 case Con{x, t} 0n:
29 {==}
30 case Con{x, +t} 1n+p:
31 nth_or_nth(X, t, p, dv)
32
33def pl_cap(~K: Data, ~V: Data, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {Nat.is_le(SC.length(Maybe<&2, V>, pl), SC.pow2(d)) == True{} : Bool}:
34 L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, pl), Equal.sym(Nat, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), N.eq_from_is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hp)), hc)
35
36def nth_hi(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X, +h: {Nat.is_lt(i, SC.length(X, xs)) == False{} : Bool}) -> {ST.nth_or(X, xs, i, dv) == dv : X}:
37 match xs i:
38 case Nil{} _:
39 {==}
40 case Con{x, t} 0n:
41 Empty.absurd({x == dv : X}, L.true_false(h))
42 case Con{x, +t} 1n+p:
43 nth_hi(X, t, p, dv, h)
44
45# ---- read ----
46
47def rf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +m: Maybe<&2, M.Node<K>>) -> {M.read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), (ST.nodes(~K, l, d, nl), DA.item(M.Node<K>, m))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), or_else(M.Node<K>, m, M.Free{0n})) : M.TreeMap<K, V, cmp> & M.Node<K>}:
48 match m:
49 case None{}:
50 {==}
51 case Some{x}:
52 {==}
53
54
55def read_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat) -> {M.read(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.nd(K, nl, id)) : M.TreeMap<K, V, cmp> & M.Node<K>}:
56 match id:
57 case 0n:
58 {==}
59 case 1n+i:
60 %Equal.sym(M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>, M.ns_get(~K, ST.nodes(~K, l, d, nl), i), (ST.nodes(~K, l, d, nl), DA.item(M.Node<K>, SC.nth(M.Node<K>, nl, i))), NSL.ns_get_ok(~K, l, d, nl, hl, hd, hc, i)) : {M.read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.nd(K, nl, 1n+i)) : M.TreeMap<K, V, cmp> & M.Node<K>}
61 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, nl, i, M.Free{0n}), or_else(M.Node<K>, SC.nth(M.Node<K>, nl, i), M.Free{0n}), nth_or_nth(M.Node<K>, nl, i, M.Free{0n})) : {M.read_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), (ST.nodes(~K, l, d, nl), DA.item(M.Node<K>, SC.nth(M.Node<K>, nl, i)))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), _) : M.TreeMap<K, V, cmp> & M.Node<K>}
62 rf(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, SC.nth(M.Node<K>, nl, i))
63
64# ---- the payload read ----
65
66def gf2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +m: Maybe<&2, Maybe<&2, V>>) -> {M.get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, pl), DA.item(Maybe<&2, V>, m))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), or_else(Maybe<&2, V>, m, None{})) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
67 match m:
68 case None{}:
69 {==}
70 case Some{x}:
71 {==}
72
73def get_id_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat) -> {M.get_id(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.pv(V, pl, id)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
74 match id:
75 case 0n:
76 {==}
77 case 1n+i:
78 %Equal.sym(D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>, D.get_at(~Maybe<&2, V>, ST.pays(~V, l, d, pl), i), (ST.pays(~V, l, d, pl), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i))), AB.blk_get(~Maybe<&2, V>, l, d, pl, hl, hd, pl_cap(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp), i)) : {M.get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
79 %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, pl, i, None{}), or_else(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i), None{}), nth_or_nth(Maybe<&2, V>, pl, i, None{})) : {M.get_id_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, pl), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i)))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), _) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
80 gf2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, SC.nth(Maybe<&2, V>, pl, i))
81
82# ---- write ----
83
84# the shadow's write: the node of id replaced when id names a slot
85def wr_nl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +x: M.Node<K>) -> List<&2, M.Node<K>>:
86 match id:
87 case 0n:
88 nl
89 case 1n+i:
90 ST.pk(List<&2, M.Node<K>>, Nat.is_lt(i, SC.length(M.Node<K>, nl)), SC.update(M.Node<K>, nl, i, x), nl)
91
92def wr_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +i: Nat, +x: M.Node<K>, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == b : Bool}) -> {M.write(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), 1n+i, x) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, ST.pk(List<&2, M.Node<K>>, b, SC.update(M.Node<K>, nl, i, x), nl), pl, t, fl}) : M.TreeMap<K, V, cmp>}:
93 match b:
94 case True{}:
95 %Equal.sym(M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, M.ns_set(~K, ST.nodes(~K, l, d, nl), i, x), (ST.nodes(~K, l, d, SC.update(M.Node<K>, nl, i, x)), Done{Unit{}}), NSL.ns_set_in(~K, l, d, nl, hl, hd, hc, i, x, hb)) : {M.write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), _) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SC.update(M.Node<K>, nl, i, x), pl, t, fl}) : M.TreeMap<K, V, cmp>}
96 {==}
97 case False{}:
98 %Equal.sym(M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, M.ns_set(~K, ST.nodes(~K, l, d, nl), i, x), (ST.nodes(~K, l, d, nl), Fail{DE.IndexOutOfRange{}}), NSL.ns_set_out(~K, l, d, nl, hl, hd, hc, i, x, hb)) : {M.write_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.pays(~V, l, d, pl), _) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}) : M.TreeMap<K, V, cmp>}
99 {==}
100
101def write_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat, +x: M.Node<K>) -> {M.write(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id, x) == ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, wr_nl(K, nl, id, x), pl, t, fl}) : M.TreeMap<K, V, cmp>}:
102 match id:
103 case 0n:
104 {==}
105 case 1n+i:
106 wr_c2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp, i, x, Nat.is_lt(i, SC.length(M.Node<K>, nl)), {==})
107
108# ---- exchange ----
109
110def ex_pl(-V: Data, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Maybe<&2, V>) -> List<&2, Maybe<&2, V>>:
111 match id:
112 case 0n:
113 pl
114 case 1n+i:
115 ST.pk(List<&2, Maybe<&2, V>>, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)), SC.update(Maybe<&2, V>, pl, i, v), pl)
116
117def ef(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +pl2: List<&2, Maybe<&2, V>>, +m: Maybe<&2, Maybe<&2, V>>) -> {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, pl2), DA.item(Maybe<&2, V>, m))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl2, t, fl}), or_else(Maybe<&2, V>, m, None{})) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
118 match m:
119 case None{}:
120 {==}
121 case Some{x}:
122 {==}
123
124def ex_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +i: Nat, +v: Maybe<&2, V>, +b: Bool, +hb: {Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)) == b : Bool}) -> {M.exchange(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), 1n+i, v) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, ST.pk(List<&2, Maybe<&2, V>>, b, SC.update(Maybe<&2, V>, pl, i, v), pl), t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
125 match b:
126 case True{}:
127 %Equal.sym(D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>, D.swap_at(~Maybe<&2, V>, ST.pays(~V, l, d, pl), i, v), (ST.pays(~V, l, d, SC.update(Maybe<&2, V>, pl, i, v)), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i))), AB.blk_swap(~Maybe<&2, V>, l, d, pl, hl, hd, pl_cap(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp), i, v, hb)) : {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, SC.update(Maybe<&2, V>, pl, i, v), t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
128 %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, pl, i, None{}), or_else(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i), None{}), nth_or_nth(Maybe<&2, V>, pl, i, None{})) : {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), (ST.pays(~V, l, d, SC.update(Maybe<&2, V>, pl, i, v)), DA.item(Maybe<&2, V>, SC.nth(Maybe<&2, V>, pl, i)))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, SC.update(Maybe<&2, V>, pl, i, v), t, fl}), _) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
129 ef(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, SC.update(Maybe<&2, V>, pl, i, v), SC.nth(Maybe<&2, V>, pl, i))
130 case False{}:
131 %Equal.sym(D.DynArray<&2, Maybe<&2, V>> & Result<&2, &2, DE.Error, Maybe<&2, V>>, D.swap_at(~Maybe<&2, V>, ST.pays(~V, l, d, pl), i, v), (ST.pays(~V, l, d, pl), Fail{DE.IndexOutOfRange{}}), AB.blk_swap_out(~Maybe<&2, V>, l, d, pl, hl, hd, pl_cap(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp), i, v, hb)) : {M.exchange_finish(~K, ~V, ~cmp, n, root, lo, hi, free, ST.nodes(~K, l, d, nl), _) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), ST.pv(V, pl, 1n+i)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
132 %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, pl, i, None{}), None{}, nth_hi(Maybe<&2, V>, pl, i, None{}, hb)) : {(ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), None{}) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), _) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}
133 {==}
134
135def exchange_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +fl: List<&2, Nat>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)) == True{} : Bool}, +hp: {Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)) == True{} : Bool}, +id: Nat, +v: Maybe<&2, V>) -> {M.exchange(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}), id, v) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, ex_pl(V, pl, id, v), t, fl}), ST.pv(V, pl, id)) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}:
136 match id:
137 case 0n:
138 {==}
139 case 1n+i:
140 ex_c2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, t, fl, hl, hd, hc, hp, i, v, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)), {==})