import Base
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./prim.bend as PR

# The TreeMap's mirror over its shadow (generated by
# tools/generators/tm_mirror.py from src/containers/balanced_search_tree.bend;
# the array-level primitives come from tools/generators/tm_hand).
# Every mirror function is its implementation function with the map
# replaced by the shadow, whose node and payload arrays are item lists.

type MCursor<-K: Data, -V: Data> is Data:
  MC{sh: ST.Sh<K, V>, next: Nat, current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, forward: Bool}

type MView<-K: Data, -V: Data> is Data:
  MV{sh: ST.Sh<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, descending: Bool}

type MInvalid<-K: Data, -V: Data> is Data:
  MI{sh: ST.Sh<K, V>, error: M.Error}

# ---- realizations ----

def rc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: MCursor<K, V>) -> M.Cursor<K, V, cmp>:
  match c:
    case MC{s, next, current, lower, upper, forward}:
      M.Cursor{ST.real(~K, ~V, ~cmp, s), next, current, lower, upper, forward}

def rv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MView<K, V>) -> M.View<K, V, cmp>:
  match w:
    case MV{s, lower, upper, descending}:
      M.View{ST.real(~K, ~V, ~cmp, s), lower, upper, descending}

def ri(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, w: MInvalid<K, V>) -> M.InvalidView<K, V, cmp>:
  match w:
    case MI{s, e}:
      M.InvalidView{ST.real(~K, ~V, ~cmp, s), e}

def rr(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Result<&1, &1, MInvalid<K, V>, MView<K, V>>) -> Result<&1, &1, M.InvalidView<K, V, cmp>, M.View<K, V, cmp>>:
  match r:
    case Done{w}:
      Done{rv(~K, ~V, ~cmp, w)}
    case Fail{w}:
      Fail{ri(~K, ~V, ~cmp, w)}

def rp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Type, p: ST.Sh<K, V> & X) -> M.TreeMap<K, V, cmp> & X:
  match p:
    case Tuple{s, x}:
      (ST.real(~K, ~V, ~cmp, s), x)

def rcp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Type, p: MCursor<K, V> & X) -> M.Cursor<K, V, cmp> & X:
  match p:
    case Tuple{c, x}:
      (rc(~K, ~V, ~cmp, c), x)

def rvp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Type, p: MView<K, V> & X) -> M.View<K, V, cmp> & X:
  match p:
    case Tuple{w, x}:
      (rv(~K, ~V, ~cmp, w), x)

# ---- the arrays' layout ----

def dg(-K: Data, -V: Data, s: ST.Sh<K, V>) -> Bool:
  match s:
    case ST.SH{n, root, lo, hi, free, +l, +d, +nl, +pl, t, fl}:
      Bool.and(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(Nat.is_le(SC.length(M.Node<K>, nl), SC.pow2(d)), Nat.is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl)))))

def dgc(-K: Data, -V: Data, c: MCursor<K, V>) -> Bool:
  match c:
    case MC{s, next, current, lower, upper, forward}:
      dg(K, V, s)

def dgv(-K: Data, -V: Data, w: MView<K, V>) -> Bool:
  match w:
    case MV{s, lower, upper, descending}:
      dg(K, V, s)

def dgi(-K: Data, -V: Data, w: MInvalid<K, V>) -> Bool:
  match w:
    case MI{s, e}:
      dg(K, V, s)

def dgr(-K: Data, -V: Data, r: Result<&1, &1, MInvalid<K, V>, MView<K, V>>) -> Bool:
  match r:
    case Done{w}:
      dgv(K, V, w)
    case Fail{w}:
      dgi(K, V, w)

def dgp(-K: Data, -V: Data, -X: Type, p: ST.Sh<K, V> & X) -> Bool:
  match p:
    case Tuple{s, x}:
      dg(K, V, s)

def dgcp(-K: Data, -V: Data, -X: Type, p: MCursor<K, V> & X) -> Bool:
  match p:
    case Tuple{c, x}:
      dgc(K, V, c)

def dgvp(-K: Data, -V: Data, -X: Type, p: MView<K, V> & X) -> Bool:
  match p:
    case Tuple{w, x}:
      dgv(K, V, w)

# ---- field access ----

def nl_of(-K: Data, -V: Data, s: ST.Sh<K, V>) -> List<&2, M.Node<K>>:
  match s:
    case ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}:
      nl

def pl_of(-K: Data, -V: Data, s: ST.Sh<K, V>) -> List<&2, Maybe<&2, V>>:
  match s:
    case ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}:
      pl

# ---- the array-level primitives ----

def new(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp) -> ST.Sh<K, V>:
  ST.SH{0n, 0n, 0n, 0n, 0n, 31n, 0n, Nil{}, Nil{}, ST.TE{}, Nil{}}

def read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & M.Node<K>:
  match m:
    case ST.SH{n, root, lo, hi, free, l, d, +nl, pl, t, fl}:
      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, ST.nd(K, nl, id))

def get_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & Maybe<&2, V>:
  match m:
    case ST.SH{n, root, lo, hi, free, l, d, nl, +pl, t, fl}:
      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, ST.pv(V, pl, id))

def write(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:
  match m:
    case ST.SH{n, root, lo, hi, free, l, d, +nl, pl, t, fl}:
      ST.SH{n, root, lo, hi, free, l, d, PR.wr_nl(K, nl, id, node), pl, t, fl}

# ---- field writes (hand-written: the implementation writes one field array) ----

def set_left_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:
  match node:
    case M.Free{px2}:
      m
    case M.N{px3, px4, px5, px6, px7}:
      write(~K, ~V, ~cmp, m, id, M.N{px3, v, px5, px6, px7})

def set_right_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:
  match node:
    case M.Free{px2}:
      m
    case M.N{px3, px4, px5, px6, px7}:
      write(~K, ~V, ~cmp, m, id, M.N{px3, px4, v, px6, px7})

def set_parent_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:
  match node:
    case M.Free{px2}:
      m
    case M.N{px3, px4, px5, px6, px7}:
      write(~K, ~V, ~cmp, m, id, M.N{px3, px4, px5, v, px7})

def set_red_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Bool, +node: M.Node<K>) -> ST.Sh<K, V>:
  match node:
    case M.Free{px2}:
      m
    case M.N{px3, px4, px5, px6, px7}:
      write(~K, ~V, ~cmp, m, id, M.N{v, px4, px5, px6, px7})

def set_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +node) = pair_result
  set_left_node(~K, ~V, ~cmp, m1, id, v, node)

def set_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +node) = pair_result
  set_right_node(~K, ~V, ~cmp, m1, id, v, node)

def set_parent_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +node) = pair_result
  set_parent_node(~K, ~V, ~cmp, m1, id, v, node)

def set_red_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +v: Bool, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +node) = pair_result
  set_red_node(~K, ~V, ~cmp, m1, id, v, node)

def set_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat) -> ST.Sh<K, V>:
  set_left_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))

def set_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat) -> ST.Sh<K, V>:
  set_right_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))

def set_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Nat) -> ST.Sh<K, V>:
  set_parent_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))

def set_red(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +v: Bool) -> ST.Sh<K, V>:
  set_red_1(~K, ~V, ~cmp, id, v, read(~K, ~V, ~cmp, m, id))


def exchange(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +value: Maybe<&2, V>) -> ST.Sh<K, V> & Maybe<&2, V>:
  match m:
    case ST.SH{n, root, lo, hi, free, l, d, nl, +pl, t, fl}:
      (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, id, value), t, fl}, ST.pv(V, pl, id))

def clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V>:
  match m:
    case ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}:
      ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, t, fl}

def app_room(~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>, +k: K, +v: V, +p: Nat, +room: Bool, +grow: Bool) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:
  match room grow:
    case True{} _:
      (ST.SH{n, root, lo, hi, free, l, d, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, p, k}), SC.snoc(Maybe<&2, V>, pl, Some{v}), t, fl}, Done{1n+SC.length(M.Node<K>, nl)})
    case False{} True{}:
      (ST.SH{n, root, lo, hi, free, l, 1n+d, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, p, k}), SC.snoc(Maybe<&2, V>, pl, Some{v}), t, fl}, Done{1n+SC.length(M.Node<K>, nl)})
    case False{} False{}:
      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})

def append(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V, +p: Nat) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}:
      app_room(~K, ~V, n, root, lo, hi, free, l, d, nl, pl, t, fl, k, v, p, Nat.is_lt(SC.length(M.Node<K>, nl), SC.pow2(d)), Nat.is_lt(d, l))

# the neighbour walks over the node list
def asc_step(-K: Data, +x: Nat, +p: Nat, +forward: Bool, node: M.Node<K>) -> M.Ascend:
  match node:
    case M.Free{next}:
      M.Ascend{0n, 0n, True{}}
    case M.N{c, +l, +r, +q, key}:
      M.ascend_choice(p, p, q, Nat.is_eq(x, M.pick(Nat, forward, l, r)))

def asc_loop(-K: Data, +fuel: Nat, +nl: List<&2, M.Node<K>>, +forward: Bool, st: M.Ascend) -> Nat:
  match fuel st:
    case 0n _:
      0n
    case 1n+f M.Ascend{x, p, True{}}:
      p
    case 1n+f M.Ascend{+x, +p, False{}}:
      asc_loop(K, f, nl, forward, asc_step(K, x, p, forward, ST.nd(K, nl, p)))

def ext_loop(~K: Data, +fuel: Nat, +nl: List<&2, M.Node<K>>, +forward: Bool, +id: Nat, +next: Nat) -> Nat:
  match fuel next:
    case 0n _:
      id
    case 1n+f 0n:
      id
    case 1n+f 1n+ +j:
      ext_loop(~K, f, nl, forward, 1n+j, M.child(~K, ST.nd(K, nl, 1n+j), forward))

def nbs(~K: Data, +nl: List<&2, M.Node<K>>, +n: Nat, +id: Nat, +p: Nat, +forward: Bool, +c: Nat) -> Nat:
  match c:
    case 0n:
      asc_loop(K, 1n+n, nl, forward, M.Ascend{id, p, False{}})
    case 1n+ +j:
      ext_loop(~K, 1n+n, nl, Bool.not(forward), 1n+j, M.child(~K, ST.nd(K, nl, 1n+j), Bool.not(forward)))

def neighbor_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Nat:
  match r:
    case Tuple{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +t, +fl}, +node}:
      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, t, fl}, nbs(~K, nl, n, id, M.node_parent(~K, node), forward, M.child(~K, node, forward)))

# ---- generated mirrors ----

def size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, n)

def root_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, root)

def first_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, lo)

def last_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Nat:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, hi)

def set_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +root: Nat) -> ST.Sh<K, V>:
  match m:
    case ST.SH{+n, +old, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}

def probe_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & (M.Node<K> & Cmp):
  match r:
    case Tuple{px2, M.Free{px4}}:
      (px2, (M.Free{px4}, EQ{}))
    case Tuple{px2, M.N{px5, px6, px7, px8, +px9}}:
      (px2, (M.N{px5, px6, px7, px8, px9}, cmp(k, px9)))

def free_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +free: Nat) -> ST.Sh<K, V>:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +old, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}

def reuse_slot_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:
  (m1, old) = pair_result
  (m1, Done{id})

def put_replaced(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  (m, old) = r
  (m, Done{old})

def contains_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Bool:
  (m, M.Search{id, p, left}) = r
  (m, Nat.is_lt(0n, id))

def move_successor_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +source: Nat, pair_result: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Nat:
  (m3, old) = pair_result
  (m3, source)

def release_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V>:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      ST.SH{Nat.sub(n, 1n), root, lo, hi, id, l_0, d_0, nl_0, pl_0, t_0, fl_0}

def set_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +lo: Nat, +hi: Nat) -> ST.Sh<K, V>:
  match m:
    case ST.SH{+n, +root, +oldlo, +oldhi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}

def is_empty_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Bool:
  (m1, +n) = pair_result
  (m1, Nat.is_eq(n, 0n))

def entry_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, k: Maybe<&2, K>, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  match k r:
    case Some{px3} Tuple{px4, Some{px6}}:
      (px4, Some{M.Entry{px3, px6}})
    case None{} Tuple{px7, None{}}:
      (px7, None{})
    case None{} Tuple{px7, Some{px9}}:
      (px7, None{})
    case Some{px3} Tuple{px4, None{}}:
      (px4, None{})

def default_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fallback: V, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & V:
  match r:
    case Tuple{px2, None{}}:
      (px2, fallback)
    case Tuple{px2, Some{px4}}:
      (px2, px4)

def view_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> Result<&1, &1, MInvalid<K, V>, MView<K, V>>:
  match valid:
    case True{}:
      Done{MV{m, lower, upper, descending}}
    case False{}:
      Fail{MI{m, M.InvalidBounds{}}}

def head_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, upper: M.Bound<K>) -> MView<K, V>:
  MV{m, M.Unbounded{}, upper, False{}}

def tail_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, lower: M.Bound<K>) -> MView<K, V>:
  MV{m, lower, M.Unbounded{}, False{}}

def descending_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MView<K, V>:
  MV{m, M.Unbounded{}, M.Unbounded{}, True{}}

def view_reverse(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V>:
  MV{m, lower, upper, descending} = view
  MV{m, lower, upper, Bool.not(descending)}

def view_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> ST.Sh<K, V>:
  MV{m, lower, upper, descending} = view
  m

def view_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, r: ST.Sh<K, V> & Maybe<&2, V>) -> MView<K, V> & Maybe<&2, V>:
  (m, v) = r
  (MV{m, lower, upper, descending}, v)

def view_put_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, r: ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>) -> MView<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  (m, status) = r
  (MV{m, lower, upper, descending}, status)

def cursor_started(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & Nat) -> MCursor<K, V>:
  (m, id) = r
  MC{m, id, 0n, lower, upper, forward}

def iterator_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> ST.Sh<K, V>:
  MC{m, next, current, lower, upper, forward} = cursor
  m

def iterator_view(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MView<K, V>:
  MC{m, next, current, lower, upper, forward} = cursor
  MV{m, lower, upper, Bool.not(forward)}

def iterator_yield(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, entry: M.Entry<K, V>, r: ST.Sh<K, V> & Nat) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:
  (m, next) = r
  (MC{m, next, id, lower, upper, forward}, Some{entry})

def iterator_set_done(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & Maybe<&2, V>) -> MCursor<K, V> & Result<&2, &2, M.Error, V>:
  match r:
    case Tuple{px2, Some{px4}}:
      (MC{px2, next, current, lower, upper, forward}, Done{px4})
    case Tuple{px2, None{}}:
      (MC{px2, next, current, lower, upper, forward}, Fail{M.NoCurrent{}})

def iterator_relocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, removed: Maybe<&2, V>, r: ST.Sh<K, V> & M.Search) -> MCursor<K, V> & Maybe<&2, V>:
  (m, M.Search{id, p, on_left}) = r
  (MC{m, id, 0n, lower, upper, forward}, removed)

def iterator_key_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MCursor<K, V> & Maybe<&2, K>:
  match r:
    case Tuple{px2, None{}}:
      (px2, None{})
    case Tuple{px2, Some{M.Entry{px5, px6}}}:
      (px2, Some{px5})

def iterator_value_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MCursor<K, V> & Maybe<&2, V>:
  match r:
    case Tuple{px2, None{}}:
      (px2, None{})
    case Tuple{px2, Some{M.Entry{px5, px6}}}:
      (px2, Some{px6})

def changed_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Bool:
  match r:
    case Tuple{px2, None{}}:
      (px2, False{})
    case Tuple{px2, Some{px4}}:
      (px2, True{})

def view_contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MView<K, V> & Maybe<&2, V>) -> MView<K, V> & Bool:
  match r:
    case Tuple{px2, None{}}:
      (px2, False{})
    case Tuple{px2, Some{px4}}:
      (px2, True{})

def view_entry_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, entry: M.Entry<K, V>, +valid: Bool) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  match valid:
    case True{}:
      (MV{m, lower, upper, descending}, Some{entry})
    case False{}:
      (MV{m, lower, upper, descending}, None{})

def insert_header(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +p: Nat, +on_left: Bool) -> ST.Sh<K, V>:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      ST.SH{1n+n, root, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(on_left, Nat.is_eq(p, lo))), id, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(on_left), Nat.is_eq(p, hi))), id, hi), free, l_0, d_0, nl_0, pl_0, t_0, fl_0}

def ascend_step_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Ascend:
  match r:
    case Tuple{px2, M.Free{px4}}:
      (px2, M.Ascend{0n, 0n, True{}})
    case Tuple{px2, M.N{px5, px6, px7, px8, px9}}:
      (px2, M.ascend_choice(p, p, px8, Nat.is_eq(x, M.pick(Nat, forward, px6, px7))))

def refresh_ends_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo: Nat, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:
  (m3, +hi) = pair_result
  set_ends(~K, ~V, ~cmp, m3, lo, hi)

def is_empty(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Bool:
  is_empty_1(~K, ~V, ~cmp, size(~K, ~V, ~cmp, m))

def key_finish(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Maybe<&2, K>:
  (m, node) = r
  (m, M.node_key(~K, node))

def range_unbounded(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +forward: Bool) -> ST.Sh<K, V> & Nat:
  match forward:
    case True{}:
      first_id(~K, ~V, ~cmp, m)
    case False{}:
      last_id(~K, ~V, ~cmp, m)

def iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:
  cursor_started(~K, ~V, ~cmp, M.Unbounded{}, M.Unbounded{}, True{}, first_id(~K, ~V, ~cmp, m))

def descending_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:
  cursor_started(~K, ~V, ~cmp, M.Unbounded{}, M.Unbounded{}, False{}, last_id(~K, ~V, ~cmp, m))

def get_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Maybe<&2, V>:
  (m, M.Search{id, p, on_left}) = r
  get_id(~K, ~V, ~cmp, m, id)

def replace_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +v: V, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Maybe<&2, V>:
  match r:
    case Tuple{px2, M.Search{0n, px5, px6}}:
      (px2, None{})
    case Tuple{px2, M.Search{1n+px7, px5, px6}}:
      exchange(~K, ~V, ~cmp, px2, 1n+px7, Some{v})

def sub_map(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +lower: M.Bound<K>, +upper: M.Bound<K>) -> Result<&1, &1, MInvalid<K, V>, MView<K, V>>:
  view_checked(~K, ~V, ~cmp, m, lower, upper, False{}, M.bounds_valid(~K, ~V, ~cmp, lower, upper))

def iterator_set_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>, +v: V) -> MCursor<K, V> & Result<&2, &2, M.Error, V>:
  match cursor:
    case MC{px2, px3, 0n, px5, px6, px7}:
      (MC{px2, px3, 0n, px5, px6, px7}, Fail{M.NoCurrent{}})
    case MC{px2, px3, 1n+ +px8, px5, px6, px7}:
      iterator_set_done(~K, ~V, ~cmp, px3, 1n+px8, px5, px6, px7, exchange(~K, ~V, ~cmp, px2, 1n+px8, Some{v}))

def entry_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:
  iterator(~K, ~V, ~cmp, m)

def key_set(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:
  iterator(~K, ~V, ~cmp, m)

def values(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> MCursor<K, V>:
  iterator(~K, ~V, ~cmp, m)

def replace_if_apply(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +replacement: V, +equal: Bool) -> ST.Sh<K, V> & Bool:
  match equal:
    case False{}:
      (m, False{})
    case True{}:
      changed_value(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, m, id, Some{replacement}))

def replace_if_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +id: Nat, +expected: V, +replacement: V, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Bool:
  match r:
    case Tuple{px2, None{}}:
      (px2, False{})
    case Tuple{px2, Some{px4}}:
      replace_if_apply(~K, ~V, ~cmp, px2, id, replacement, eq(px4, expected))

def iterator_has_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +next: Nat, +current: Nat, +lower: M.Bound<K>, +upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> MCursor<K, V> & Bool:
  match r:
    case Tuple{px2, M.Free{px4}}:
      (MC{px2, next, current, lower, upper, forward}, False{})
    case Tuple{px2, M.N{px5, px6, px7, px8, px9}}:
      (MC{px2, next, current, lower, upper, forward}, M.in_range(~K, ~V, ~cmp, px9, lower, upper))

def view_entry_result(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lower: M.Bound<K>, +upper: M.Bound<K>, +descending: Bool, r: ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  match r:
    case Tuple{px2, None{}}:
      (MV{px2, lower, upper, descending}, None{})
    case Tuple{px2, Some{M.Entry{+px5, px6}}}:
      view_entry_checked(~K, ~V, ~cmp, px2, lower, upper, descending, M.Entry{px5, px6}, M.in_range(~K, ~V, ~cmp, px5, lower, upper))

def attach_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +x: Nat, +on_left: Bool) -> ST.Sh<K, V>:
  match p on_left:
    case 0n True{}:
      set_root(~K, ~V, ~cmp, m, x)
    case 0n False{}:
      set_root(~K, ~V, ~cmp, m, x)
    case 1n+px3 True{}:
      set_left(~K, ~V, ~cmp, m, 1n+px3, x)
    case 1n+px3 False{}:
      set_right(~K, ~V, ~cmp, m, 1n+px3, x)

def replace_if_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +expected: V, +replacement: V, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Bool:
  (m, M.Search{+id, p, on_left}) = r
  replace_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))

def attach(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +x: Nat, +on_left: Bool) -> ST.Sh<K, V>:
  set_parent(~K, ~V, ~cmp, attach_side(~K, ~V, ~cmp, m, p, x, on_left), x, p)

def black_root_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:
  (m1, +r) = pair_result
  set_red(~K, ~V, ~cmp, m1, r, False{})

def reuse_slot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +next: Nat, +p: Nat, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:
  reuse_slot_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, write(~K, ~V, ~cmp, free_header(~K, ~V, ~cmp, m, next), id, M.N{True{}, 0n, 0n, p, k}), id, Some{v}))

def set_key_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +k: K, +node: M.Node<K>) -> ST.Sh<K, V>:
  match node:
    case M.Free{px2}:
      m
    case M.N{px3, px4, px5, px6, px7}:
      write(~K, ~V, ~cmp, m, id, M.N{px3, px4, px5, px6, k})

def recycle(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V>:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      release_header(~K, ~V, ~cmp, write(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, id, M.Free{free}), id)

# the mirror of entry_snapshot reads the whole node (the implementation reads
# the key and the value; sim/entry_snapshot.part)
def entry_snapshot_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, id: Nat, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  (m, node) = r
  entry_value(~K, ~V, ~cmp, M.node_key(~K, node), get_id(~K, ~V, ~cmp, m, id))

def entry_snapshot(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  (m, +id) = r
  entry_snapshot_value(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))


def rotate_left_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, +yn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m3, +pn) = pair_result
  set_parent(~K, ~V, ~cmp, set_left(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, set_parent(~K, ~V, ~cmp, set_right(~K, ~V, ~cmp, m3, x, M.node_left(~K, yn)), M.node_left(~K, yn), x), M.node_parent(~K, xn), M.node_right(~K, xn), Nat.is_eq(M.node_left(~K, pn), x)), M.node_right(~K, xn), x), x, M.node_right(~K, xn))

def rotate_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, +yn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m3, +pn) = pair_result
  set_parent(~K, ~V, ~cmp, set_right(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, set_parent(~K, ~V, ~cmp, set_left(~K, ~V, ~cmp, m3, x, M.node_right(~K, yn)), M.node_right(~K, yn), x), M.node_parent(~K, xn), M.node_left(~K, xn), Nat.is_eq(M.node_left(~K, pn), x)), M.node_left(~K, xn), x), x, M.node_left(~K, xn))

def black_root(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V>:
  black_root_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))

def alloc_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +p: Nat, +k: K, +v: V, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:
  match r:
    case Tuple{px2, M.Free{px4}}:
      reuse_slot(~K, ~V, ~cmp, px2, id, px4, p, k, v)
    case Tuple{px2, M.N{px5, px6, px7, px8, px9}}:
      (px2, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})

def set_key_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +k: K, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +node) = pair_result
  set_key_node(~K, ~V, ~cmp, m1, id, k, node)

def first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))

def last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))

def probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +k: K) -> ST.Sh<K, V> & (M.Node<K> & Cmp):
  probe_node(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))

def search_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +id: Nat, +p: Nat, +on_left: Bool, st: ST.Sh<K, V> & (M.Node<K> & Cmp)) -> ST.Sh<K, V> & M.Search:
  match fuel st:
    case 0n Tuple{px4, Tuple{M.Free{px8}, LT{}}}:
      (px4, M.Search{0n, p, on_left})
    case 0n Tuple{px4, Tuple{M.Free{px8}, EQ{}}}:
      (px4, M.Search{0n, p, on_left})
    case 0n Tuple{px4, Tuple{M.Free{px8}, GT{}}}:
      (px4, M.Search{0n, p, on_left})
    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, LT{}}}:
      (px4, M.Search{0n, p, on_left})
    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, EQ{}}}:
      (px4, M.Search{0n, p, on_left})
    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, GT{}}}:
      (px4, M.Search{0n, p, on_left})
    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, LT{}}}:
      (px14, M.Search{0n, p, on_left})
    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, EQ{}}}:
      (px14, M.Search{0n, p, on_left})
    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, GT{}}}:
      (px14, M.Search{0n, p, on_left})
    case 1n+px3 Tuple{px14, Tuple{M.N{px19, +px20, px21, px22, px23}, LT{}}}:
      search_loop(~K, ~V, ~cmp, px3, k, px20, id, True{}, probe(~K, ~V, ~cmp, px14, px20, k))
    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, +px21, px22, px23}, GT{}}}:
      search_loop(~K, ~V, ~cmp, px3, k, px21, id, False{}, probe(~K, ~V, ~cmp, px14, px21, k))
    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, px21, px22, px23}, EQ{}}}:
      (px14, M.Search{id, p, on_left})

# the mirror of search (the implementation reads two fields per level; sim/search.part)
def search(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & M.Search:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      search_loop(~K, ~V, ~cmp, 1n+n, k, root, 0n, False{}, probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, root, k))

def get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Maybe<&2, V>:
  get_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))

def contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Bool:
  contains_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))

# the mirror of extreme reads whole nodes (the implementation reads a tag and
# one child per level; sim/extreme.part)
def extreme_probe(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Nat:
  (m, node) = r
  (m, M.child(~K, node, forward))

def extreme_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, +id: Nat, st: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Nat:
  match fuel st:
    case 0n Tuple{px4, 0n}:
      (px4, id)
    case 0n Tuple{px4, 1n+px6}:
      (px4, id)
    case 1n+px3 Tuple{px7, 0n}:
      (px7, id)
    case 1n+px3 Tuple{px7, 1n+ +px9}:
      extreme_loop(~K, ~V, ~cmp, px3, forward, 1n+px9, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, px7, 1n+px9)))

def extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +forward: Bool) -> ST.Sh<K, V> & Nat:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      extreme_loop(~K, ~V, ~cmp, 1n+n, forward, id, extreme_probe(~K, ~V, ~cmp, forward, read(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, id)))


def replace(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V) -> ST.Sh<K, V> & Maybe<&2, V>:
  replace_found(~K, ~V, ~cmp, v, search(~K, ~V, ~cmp, m, k))

def iterator_reseek(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, k: Maybe<&2, K>, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & Maybe<&2, V>) -> MCursor<K, V> & Maybe<&2, V>:
  match k r:
    case None{} Tuple{px4, px5}:
      (MC{px4, 0n, 0n, lower, upper, forward}, px5)
    case Some{px3} Tuple{px6, px7}:
      iterator_relocated(~K, ~V, ~cmp, lower, upper, forward, px7, search(~K, ~V, ~cmp, px6, px3))

def replace_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: ST.Sh<K, V>, +k: K, +expected: V, +replacement: V) -> ST.Sh<K, V> & Bool:
  replace_if_found(~K, ~V, ~cmp, ~eq, expected, replacement, search(~K, ~V, ~cmp, m, k))

def rotate_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m2, +yn) = pair_result
  rotate_left_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, M.node_parent(~K, xn)))

def rotate_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +xn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m2, +yn) = pair_result
  rotate_right_3(~K, ~V, ~cmp, x, xn, yn, read(~K, ~V, ~cmp, m2, M.node_parent(~K, xn)))

def ascend_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +forward: Bool, st: ST.Sh<K, V> & M.Ascend) -> ST.Sh<K, V> & Nat:
  match fuel st:
    case 0n Tuple{px4, px5}:
      (px4, 0n)
    case 1n+px3 Tuple{px6, M.Ascend{px8, px9, True{}}}:
      (px6, px9)
    case 1n+px3 Tuple{px6, M.Ascend{+px8, +px9, False{}}}:
      ascend_loop(~K, ~V, ~cmp, px3, forward, ascend_step_node(~K, ~V, ~cmp, px8, px9, forward, read(~K, ~V, ~cmp, px6, px9)))

def neighbor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +forward: Bool) -> ST.Sh<K, V> & Nat:
  neighbor_node(~K, ~V, ~cmp, id, forward, read(~K, ~V, ~cmp, m, id))

def set_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +k: K) -> ST.Sh<K, V>:
  set_key_1(~K, ~V, ~cmp, id, k, read(~K, ~V, ~cmp, m, id))

def refresh_ends_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +r: Nat, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:
  (m2, +lo) = pair_result
  refresh_ends_3(~K, ~V, ~cmp, lo, extreme(~K, ~V, ~cmp, m2, r, True{}))

def key_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Maybe<&2, K>:
  (m, id) = r
  key_finish(~K, ~V, ~cmp, read(~K, ~V, ~cmp, m, id))

def get_or_default(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +fallback: V) -> ST.Sh<K, V> & V:
  default_value(~K, ~V, ~cmp, fallback, get(~K, ~V, ~cmp, m, k))

def view_get_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> MView<K, V> & Maybe<&2, V>:
  match valid:
    case True{}:
      view_value(~K, ~V, ~cmp, lower, upper, descending, get(~K, ~V, ~cmp, m, k))
    case False{}:
      (MV{m, lower, upper, descending}, None{})

def iterator_has_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Bool:
  MC{m, +next, current, lower, upper, forward} = cursor
  iterator_has_checked(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))

def rotate_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +xn) = pair_result
  rotate_left_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, M.node_right(~K, xn)))

def rotate_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +xn) = pair_result
  rotate_right_2(~K, ~V, ~cmp, x, xn, read(~K, ~V, ~cmp, m1, M.node_left(~K, xn)))

def copy_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +target: Nat, +node: M.Node<K>) -> ST.Sh<K, V>:
  match node:
    case M.Free{px2}:
      m
    case M.N{px3, px4, px5, px6, px7}:
      set_key(~K, ~V, ~cmp, m, target, px7)

def refresh_ends_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:
  (m1, +r) = pair_result
  refresh_ends_2(~K, ~V, ~cmp, r, extreme(~K, ~V, ~cmp, m1, r, False{}))

def nav_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +higher: Bool, +inclusive: Bool) -> ST.Sh<K, V> & Nat:
  match inclusive:
    case True{}:
      (m, id)
    case False{}:
      neighbor(~K, ~V, ~cmp, m, id, higher)

def first_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))

def last_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))

def view_get(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, V>:
  MV{m, +lower, +upper, descending} = view
  view_get_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, M.in_range(~K, ~V, ~cmp, k, lower, upper))

def rotate_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat) -> ST.Sh<K, V>:
  rotate_left_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))

def rotate_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat) -> ST.Sh<K, V>:
  rotate_right_1(~K, ~V, ~cmp, x, read(~K, ~V, ~cmp, m, x))

def move_successor_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, +source_node: M.Node<K>, pair_result: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Nat:
  (m2, value) = pair_result
  move_successor_3(~K, ~V, ~cmp, source, exchange(~K, ~V, ~cmp, copy_key(~K, ~V, ~cmp, m2, target, source_node), target, value))

def refresh_ends(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V>:
  refresh_ends_1(~K, ~V, ~cmp, root_id(~K, ~V, ~cmp, m))

def nav_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +k: K, +higher: Bool, +inclusive: Bool, +id: Nat, +best: Nat, st: ST.Sh<K, V> & (M.Node<K> & Cmp)) -> ST.Sh<K, V> & Nat:
  match fuel st:
    case 0n Tuple{px4, Tuple{M.Free{px8}, LT{}}}:
      (px4, best)
    case 0n Tuple{px4, Tuple{M.Free{px8}, EQ{}}}:
      (px4, best)
    case 0n Tuple{px4, Tuple{M.Free{px8}, GT{}}}:
      (px4, best)
    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, LT{}}}:
      (px4, best)
    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, EQ{}}}:
      (px4, best)
    case 0n Tuple{px4, Tuple{M.N{px9, px10, px11, px12, px13}, GT{}}}:
      (px4, best)
    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, LT{}}}:
      (px14, best)
    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, EQ{}}}:
      (px14, best)
    case 1n+px3 Tuple{px14, Tuple{M.Free{px18}, GT{}}}:
      (px14, best)
    case 1n+px3 Tuple{px14, Tuple{M.N{px19, +px20, px21, px22, px23}, LT{}}}:
      nav_loop(~K, ~V, ~cmp, px3, k, higher, inclusive, px20, M.pick(Nat, higher, id, best), probe(~K, ~V, ~cmp, px14, px20, k))
    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, +px21, px22, px23}, GT{}}}:
      nav_loop(~K, ~V, ~cmp, px3, k, higher, inclusive, px21, M.pick(Nat, higher, best, id), probe(~K, ~V, ~cmp, px14, px21, k))
    case 1n+px3 Tuple{px14, Tuple{M.N{px19, px20, px21, px22, px23}, EQ{}}}:
      nav_equal(~K, ~V, ~cmp, px14, id, higher, inclusive)

def view_contains_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Bool:
  view_contains_value(~K, ~V, ~cmp, view_get(~K, ~V, ~cmp, view, k))

def insert_black_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> ST.Sh<K, V> & M.Fix:
  match triangle:
    case True{}:
      (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, m, p), z, False{}), g, True{}), g), M.Fix{0n, False{}})
    case False{}:
      (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), M.Fix{0n, False{}})

def insert_black_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +triangle: Bool) -> ST.Sh<K, V> & M.Fix:
  match triangle:
    case True{}:
      (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, m, p), z, False{}), g, True{}), g), M.Fix{0n, False{}})
    case False{}:
      (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), g, True{}), g), M.Fix{0n, False{}})

def move_successor_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, +source: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Nat:
  (m1, +source_node) = pair_result
  move_successor_2(~K, ~V, ~cmp, target, source, source_node, exchange(~K, ~V, ~cmp, m1, source, None{}))

def delete_borrow_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, M.node_red(~K, pn)), p, False{}), M.node_right(~K, wn), False{}), p), M.DF{0n, 0n, False{}})

def delete_borrow_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, M.node_red(~K, pn)), p, False{}), M.node_left(~K, wn), False{}), p), M.DF{0n, 0n, False{}})

# the mirror of navigate (the implementation reads two fields per level; sim/navigate.part)
def navigate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +higher: Bool, +inclusive: Bool) -> ST.Sh<K, V> & Nat:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      nav_loop(~K, ~V, ~cmp, 1n+n, k, higher, inclusive, root, 0n, probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, root, k))

def insert_uncle_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  match uncle:
    case M.N{True{}, px4, px5, px6, px7}:
      (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), M.Fix{g, True{}})
    case M.Free{px2}:
      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)
    case M.N{False{}, px4, px5, px6, px7}:
      insert_black_left(~K, ~V, ~cmp, m, z, p, g, triangle)

def insert_uncle_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +u: Nat, +triangle: Bool, +uncle: M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  match uncle:
    case M.N{True{}, px4, px5, px6, px7}:
      (set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, p, False{}), u, False{}), g, True{}), M.Fix{g, True{}})
    case M.Free{px2}:
      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)
    case M.N{False{}, px4, px5, px6, px7}:
      insert_black_right(~K, ~V, ~cmp, m, z, p, g, triangle)

def move_successor(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +target: Nat, +source: Nat) -> ST.Sh<K, V> & Nat:
  move_successor_1(~K, ~V, ~cmp, target, source, read(~K, ~V, ~cmp, m, source))

def delete_borrow_read_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m2, +wn) = pair_result
  delete_borrow_left(~K, ~V, ~cmp, m2, p, M.node_right(~K, pn), pn, wn)

def delete_borrow_read_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m2, +wn) = pair_result
  delete_borrow_right(~K, ~V, ~cmp, m2, p, M.node_left(~K, pn), pn, wn)

def lower_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))

def floor_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))

def ceiling_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))

def higher_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Maybe<&2, K>:
  key_id(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))

def lower_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, False{}))

def floor_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, False{}, True{}))

def ceiling_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, True{}))

def higher_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, k: K) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  entry_snapshot(~K, ~V, ~cmp, navigate(~K, ~V, ~cmp, m, k, True{}, False{}))

def range_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, bound: M.Bound<K>, +forward: Bool) -> ST.Sh<K, V> & Nat:
  match bound:
    case M.Unbounded{}:
      range_unbounded(~K, ~V, ~cmp, m, forward)
    case M.Inclusive{px2}:
      navigate(~K, ~V, ~cmp, m, px2, forward, True{})
    case M.Exclusive{px3}:
      navigate(~K, ~V, ~cmp, m, px3, forward, False{})

def insert_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  (m1, +un) = pair_result
  insert_uncle_left(~K, ~V, ~cmp, m1, z, p, g, M.node_right(~K, gn), Nat.is_eq(z, M.node_right(~K, pn)), un)

def insert_side_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  (m1, +un) = pair_result
  insert_uncle_right(~K, ~V, ~cmp, m1, z, p, g, M.node_left(~K, gn), Nat.is_eq(z, M.node_left(~K, pn)), un)

def allocate(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      match free:
        case 0n:
          append(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, 0n, l_0, d_0, nl_0, pl_0, t_0, fl_0}, k, v, p)
        case 1n+ +px2:
          alloc_read(~K, ~V, ~cmp, 1n+px2, p, k, v, read(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, 1n+px2, l_0, d_0, nl_0, pl_0, t_0, fl_0}, 1n+px2))

def successor_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +target: Nat, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Nat:
  (m, source) = r
  move_successor(~K, ~V, ~cmp, m, target, source)

def delete_borrow_read_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m1, +pn) = pair_result
  delete_borrow_read_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_right(~K, pn)))

def delete_borrow_read_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m1, +pn) = pair_result
  delete_borrow_read_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_left(~K, pn)))

def view_iterator(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MCursor<K, V>:
  MV{m, +lower, +upper, +descending} = view
  cursor_started(~K, ~V, ~cmp, lower, upper, Bool.not(descending), range_start(~K, ~V, ~cmp, m, M.pick(M.Bound<K>, descending, upper, lower), Bool.not(descending)))

def view_nav_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, lower: M.Bound<K>, upper: M.Bound<K>, +higher: Bool, +inclusive: Bool, +within: Bool) -> ST.Sh<K, V> & Nat:
  match within:
    case True{}:
      navigate(~K, ~V, ~cmp, m, k, higher, inclusive)
    case False{}:
      range_start(~K, ~V, ~cmp, m, M.pick(M.Bound<K>, higher, lower, upper), higher)

def view_extreme(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +first: Bool) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  MV{m, +lower, +upper, +descending} = view
  +up = M.pick(Bool, descending, Bool.not(first), first)
  view_entry_result(~K, ~V, ~cmp, lower, upper, descending, entry_snapshot(~K, ~V, ~cmp, range_start(~K, ~V, ~cmp, m, M.pick(M.Bound<K>, up, lower, upper), up)))

def insert_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  insert_side_left_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, M.node_right(~K, gn)))

def insert_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  insert_side_right_1(~K, ~V, ~cmp, z, p, g, pn, gn, read(~K, ~V, ~cmp, m, M.node_left(~K, gn)))

def delete_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Nat:
  match r:
    case Tuple{px2, M.N{px5, 1n+px10, 1n+px11, px8, px9}}:
      successor_ready(~K, ~V, ~cmp, id, extreme(~K, ~V, ~cmp, px2, 1n+px11, False{}))
    case Tuple{px2, M.Free{px4}}:
      (px2, id)
    case Tuple{px2, M.N{px5, 0n, 0n, px8, px9}}:
      (px2, id)
    case Tuple{px2, M.N{px5, 0n, 1n+px12, px8, px9}}:
      (px2, id)
    case Tuple{px2, M.N{px5, 1n+px10, 0n, px8, px9}}:
      (px2, id)

def delete_borrow_read_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.DeleteFix:
  delete_borrow_read_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

def delete_borrow_read_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.DeleteFix:
  delete_borrow_read_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

# the mirror of iterator_next reads the whole node (the implementation reads
# four fields; sim/iterator_next.part)
def iterator_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, +node: M.Node<K>, entry: M.Entry<K, V>, +valid: Bool) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:
  match valid:
    case True{}:
      iterator_yield(~K, ~V, ~cmp, id, lower, upper, forward, entry, neighbor_node(~K, ~V, ~cmp, id, forward, (m, node)))
    case False{}:
      (MC{m, 0n, current, lower, upper, forward}, None{})

def iterator_read(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +current: Nat, +lower: M.Bound<K>, +upper: M.Bound<K>, +forward: Bool, +node: M.Node<K>, r: ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:
  match r:
    case Tuple{px2, None{}}:
      (MC{px2, 0n, current, lower, upper, forward}, None{})
    case Tuple{px2, Some{M.Entry{+px5, px6}}}:
      iterator_checked(~K, ~V, ~cmp, px2, id, current, lower, upper, forward, node, M.Entry{px5, px6}, M.in_range(~K, ~V, ~cmp, px5, lower, upper))

def iterator_node(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, r: ST.Sh<K, V> & M.Node<K>) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:
  (m, +node) = r
  iterator_read(~K, ~V, ~cmp, id, current, lower, upper, forward, node, entry_value(~K, ~V, ~cmp, M.node_key(~K, node), get_id(~K, ~V, ~cmp, m, id)))

def iterator_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:
  MC{m, +next, current, lower, upper, forward} = cursor
  iterator_node(~K, ~V, ~cmp, next, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))


def view_nav(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K, +higher: Bool, +inclusive: Bool) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  MV{m, +lower, +upper, +descending} = view
  +up = M.pick(Bool, descending, Bool.not(higher), higher)
  view_entry_result(~K, ~V, ~cmp, lower, upper, descending, entry_snapshot(~K, ~V, ~cmp, view_nav_start(~K, ~V, ~cmp, m, k, lower, upper, up, inclusive, M.pick(Bool, up, M.above_lower(~K, ~V, ~cmp, k, lower), M.below_upper(~K, ~V, ~cmp, k, upper)))))

def view_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  view_extreme(~K, ~V, ~cmp, view, True{})

def view_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  view_extreme(~K, ~V, ~cmp, view, False{})

def insert_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +g: Nat, +pn: M.Node<K>, +gn: M.Node<K>, +on_left: Bool) -> ST.Sh<K, V> & M.Fix:
  match on_left:
    case True{}:
      insert_side_left(~K, ~V, ~cmp, m, z, p, g, pn, gn)
    case False{}:
      insert_side_right(~K, ~V, ~cmp, m, z, p, g, pn, gn)

def delete_far_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +far_red: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match far_red:
    case True{}:
      delete_borrow_left(~K, ~V, ~cmp, m, p, w, pn, wn)
    case False{}:
      delete_borrow_read_left(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, M.node_left(~K, wn), False{}), w, True{}), w), p)

def delete_far_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +far_red: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match far_red:
    case True{}:
      delete_borrow_right(~K, ~V, ~cmp, m, p, w, pn, wn)
    case False{}:
      delete_borrow_read_right(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, M.node_right(~K, wn), False{}), w, True{}), w), p)

def iterator_next_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Maybe<&2, K>:
  iterator_key_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))

def iterator_next_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Maybe<&2, V>:
  iterator_value_result(~K, ~V, ~cmp, iterator_next(~K, ~V, ~cmp, cursor))

def contains_value_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +fuel: Nat, +wanted: V, +found: Bool, st: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> ST.Sh<K, V> & Bool:
  match fuel found st:
    case 0n True{} Tuple{px4, None{}}:
      (iterator_finish(~K, ~V, ~cmp, px4), True{})
    case 0n True{} Tuple{px4, Some{px7}}:
      (iterator_finish(~K, ~V, ~cmp, px4), True{})
    case 1n+px6 True{} Tuple{px4, None{}}:
      (iterator_finish(~K, ~V, ~cmp, px4), True{})
    case 1n+px6 True{} Tuple{px4, Some{px7}}:
      (iterator_finish(~K, ~V, ~cmp, px4), True{})
    case 0n False{} Tuple{px9, None{}}:
      (iterator_finish(~K, ~V, ~cmp, px9), False{})
    case 0n False{} Tuple{px9, Some{px11}}:
      (iterator_finish(~K, ~V, ~cmp, px9), False{})
    case 1n+px8 False{} Tuple{px12, None{}}:
      (iterator_finish(~K, ~V, ~cmp, px12), False{})
    case 1n+px8 False{} Tuple{px12, Some{M.Entry{px15, px16}}}:
      contains_value_loop(~K, ~V, ~cmp, ~eq, px8, wanted, eq(px16, wanted), iterator_next(~K, ~V, ~cmp, px12))

def view_lower_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, False{}, False{})

def view_floor_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, False{}, True{})

def view_ceiling_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, True{}, True{})

def view_higher_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, M.Entry<K, V>>:
  view_nav(~K, ~V, ~cmp, view, k, True{}, False{})

def view_count_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, +count: Nat, st: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MView<K, V> & Nat:
  match fuel st:
    case 0n Tuple{px4, None{}}:
      (iterator_view(~K, ~V, ~cmp, px4), count)
    case 0n Tuple{px4, Some{px6}}:
      (iterator_view(~K, ~V, ~cmp, px4), count)
    case 1n+px3 Tuple{px7, None{}}:
      (iterator_view(~K, ~V, ~cmp, px7), count)
    case 1n+px3 Tuple{px7, Some{px9}}:
      view_count_loop(~K, ~V, ~cmp, px3, 1n+count, iterator_next(~K, ~V, ~cmp, px7))

def view_clear_next(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: MCursor<K, V> & Maybe<&2, V>) -> MCursor<K, V> & Maybe<&2, M.Entry<K, V>>:
  (cursor, removed) = r
  iterator_next(~K, ~V, ~cmp, cursor)

def insert_grand_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  (m1, +gn) = pair_result
  insert_side(~K, ~V, ~cmp, m1, z, p, M.node_parent(~K, pn), pn, gn, Nat.is_eq(p, M.node_left(~K, gn)))

def delete_children_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_red: Bool, +far_red: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match near_red far_red:
    case False{} False{}:
      (set_red(~K, ~V, ~cmp, m, w, True{}), M.DF{p, M.node_parent(~K, pn), True{}})
    case True{} True{}:
      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
    case True{} False{}:
      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
    case False{} True{}:
      delete_far_left(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)

def delete_children_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_red: Bool, +far_red: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match near_red far_red:
    case False{} False{}:
      (set_red(~K, ~V, ~cmp, m, w, True{}), M.DF{p, M.node_parent(~K, pn), True{}})
    case True{} True{}:
      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
    case True{} False{}:
      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)
    case False{} True{}:
      delete_far_right(~K, ~V, ~cmp, m, p, w, pn, wn, far_red)

def contains_value_start(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +wanted: V, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Bool:
  (m, n) = r
  contains_value_loop(~K, ~V, ~cmp, ~eq, 1n+n, wanted, False{}, iterator_next(~K, ~V, ~cmp, iterator(~K, ~V, ~cmp, m)))

def view_size(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V> & Nat:
  match view:
    case MV{ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}, lower, upper, descending}:
      view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, MV{ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, lower, upper, descending})))

def insert_grand(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +pn: M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  insert_grand_1(~K, ~V, ~cmp, z, p, pn, read(~K, ~V, ~cmp, m, M.node_parent(~K, pn)))

def delete_sibling_left_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_node: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m4, +far_node) = pair_result
  delete_children_left(~K, ~V, ~cmp, m4, p, M.node_right(~K, pn), pn, wn, M.node_red(~K, near_node), M.node_red(~K, far_node))

def delete_sibling_right_4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, +wn: M.Node<K>, +near_node: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m4, +far_node) = pair_result
  delete_children_right(~K, ~V, ~cmp, m4, p, M.node_left(~K, pn), pn, wn, M.node_red(~K, near_node), M.node_red(~K, far_node))

def contains_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: ST.Sh<K, V>, +wanted: V) -> ST.Sh<K, V> & Bool:
  contains_value_start(~K, ~V, ~cmp, ~eq, wanted, size(~K, ~V, ~cmp, m))

def insert_parent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat, +p: Nat, +pn: M.Node<K>, +is_red: Bool) -> ST.Sh<K, V> & M.Fix:
  match is_red:
    case False{}:
      (m, M.Fix{0n, False{}})
    case True{}:
      insert_grand(~K, ~V, ~cmp, m, z, p, pn)

def delete_sibling_left_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, +wn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m3, +near_node) = pair_result
  delete_sibling_left_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, M.node_right(~K, wn)))

def delete_sibling_right_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, +wn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m3, +near_node) = pair_result
  delete_sibling_right_4(~K, ~V, ~cmp, p, pn, wn, near_node, read(~K, ~V, ~cmp, m3, M.node_left(~K, wn)))

def insert_fix_step_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, +zn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  (m2, +pn) = pair_result
  insert_parent(~K, ~V, ~cmp, m2, z, M.node_parent(~K, zn), pn, M.node_red(~K, pn))

def delete_sibling_left_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m2, +wn) = pair_result
  delete_sibling_left_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, M.node_left(~K, wn)))

def delete_sibling_right_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m2, +wn) = pair_result
  delete_sibling_right_3(~K, ~V, ~cmp, p, pn, wn, read(~K, ~V, ~cmp, m2, M.node_right(~K, wn)))

def insert_fix_step_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +z: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.Fix:
  (m1, +zn) = pair_result
  insert_fix_step_2(~K, ~V, ~cmp, z, zn, read(~K, ~V, ~cmp, m1, M.node_parent(~K, zn)))

def delete_sibling_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m1, +pn) = pair_result
  delete_sibling_left_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_right(~K, pn)))

def delete_sibling_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m1, +pn) = pair_result
  delete_sibling_right_2(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m1, M.node_left(~K, pn)))

def insert_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +z: Nat) -> ST.Sh<K, V> & M.Fix:
  insert_fix_step_1(~K, ~V, ~cmp, z, read(~K, ~V, ~cmp, m, z))

def delete_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.DeleteFix:
  delete_sibling_left_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

def delete_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat) -> ST.Sh<K, V> & M.DeleteFix:
  delete_sibling_right_1(~K, ~V, ~cmp, p, read(~K, ~V, ~cmp, m, p))

def insert_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: ST.Sh<K, V> & M.Fix) -> ST.Sh<K, V>:
  match fuel st:
    case 0n Tuple{px4, px5}:
      black_root(~K, ~V, ~cmp, px4)
    case 1n+px3 Tuple{px6, M.Fix{px8, False{}}}:
      black_root(~K, ~V, ~cmp, px6)
    case 1n+px3 Tuple{px6, M.Fix{px8, True{}}}:
      insert_fix_loop(~K, ~V, ~cmp, px3, insert_fix_step(~K, ~V, ~cmp, px6, px8))

def delete_red_sibling_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +red_sibling: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match red_sibling:
    case True{}:
      delete_sibling_left(~K, ~V, ~cmp, rotate_left(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, False{}), p, True{}), p), p)
    case False{}:
      delete_sibling_left(~K, ~V, ~cmp, m, p)

def delete_red_sibling_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +w: Nat, +red_sibling: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match red_sibling:
    case True{}:
      delete_sibling_right(~K, ~V, ~cmp, rotate_right(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, set_red(~K, ~V, ~cmp, m, w, False{}), p, True{}), p), p)
    case False{}:
      delete_sibling_right(~K, ~V, ~cmp, m, p)

def insert_fixed(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:
  (m, n) = r
  insert_fix_loop(~K, ~V, ~cmp, 1n+n, (m, M.Fix{id, True{}}))

def delete_side_left_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m1, +wn) = pair_result
  delete_red_sibling_left(~K, ~V, ~cmp, m1, p, M.node_right(~K, pn), M.node_red(~K, wn))

def delete_side_right_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +pn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m1, +wn) = pair_result
  delete_red_sibling_right(~K, ~V, ~cmp, m1, p, M.node_left(~K, pn), M.node_red(~K, wn))

def put_allocated(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +p: Nat, +on_left: Bool, r: ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Nat>) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  match r:
    case Tuple{px2, Done{+px4}}:
      (insert_fixed(~K, ~V, ~cmp, px4, size(~K, ~V, ~cmp, insert_header(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, px2, p, px4, on_left), px4, p, on_left))), Done{None{}})
    case Tuple{px2, Fail{px5}}:
      (px2, Fail{px5})

def delete_side_left(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +pn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  delete_side_left_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, M.node_right(~K, pn)))

def delete_side_right(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +p: Nat, +pn: M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  delete_side_right_1(~K, ~V, ~cmp, p, pn, read(~K, ~V, ~cmp, m, M.node_left(~K, pn)))

def put_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  match r:
    case Tuple{px2, M.Search{0n, +px5, +px6}}:
      put_allocated(~K, ~V, ~cmp, px5, px6, allocate(~K, ~V, ~cmp, px2, px5, k, v))
    case Tuple{px2, M.Search{1n+px7, px5, px6}}:
      put_replaced(~K, ~V, ~cmp, exchange(~K, ~V, ~cmp, px2, 1n+px7, Some{v}))

def delete_side(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat, +p: Nat, +pn: M.Node<K>, +on_left: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match on_left:
    case True{}:
      delete_side_left(~K, ~V, ~cmp, m, p, pn)
    case False{}:
      delete_side_right(~K, ~V, ~cmp, m, p, pn)

def put_absent_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +v: V, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  match r:
    case Tuple{px2, M.Search{0n, +px5, +px6}}:
      put_allocated(~K, ~V, ~cmp, px5, px6, allocate(~K, ~V, ~cmp, px2, px5, k, v))
    case Tuple{px2, M.Search{1n+px7, px5, px6}}:
      put_replaced(~K, ~V, ~cmp, get_id(~K, ~V, ~cmp, px2, 1n+px7))

def put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  put_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))

def delete_stop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat, +p: Nat, +pn: M.Node<K>, +stop: Bool) -> ST.Sh<K, V> & M.DeleteFix:
  match stop:
    case True{}:
      (set_red(~K, ~V, ~cmp, m, x, False{}), M.DF{0n, 0n, False{}})
    case False{}:
      delete_side(~K, ~V, ~cmp, m, x, p, pn, Nat.is_eq(x, M.node_left(~K, pn)))

def put_if_absent(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V) -> ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  put_absent_found(~K, ~V, ~cmp, k, v, search(~K, ~V, ~cmp, m, k))

def delete_fix_step_3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +root_node: Nat, +xn: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m3, +pn) = pair_result
  delete_stop(~K, ~V, ~cmp, m3, x, p, pn, Bool.or(Nat.is_eq(x, root_node), M.node_red(~K, xn)))

def view_put_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, +v: V, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> MView<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  match valid:
    case True{}:
      view_put_finish(~K, ~V, ~cmp, lower, upper, descending, put(~K, ~V, ~cmp, m, k, v))
    case False{}:
      (MV{m, lower, upper, descending}, Fail{M.Rejected{M.OutOfRange{}, k, v}})

def delete_fix_step_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, +root_node: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & M.DeleteFix:
  (m2, +xn) = pair_result
  delete_fix_step_3(~K, ~V, ~cmp, x, p, root_node, xn, read(~K, ~V, ~cmp, m2, p))

def view_put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K, +v: V) -> MView<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>:
  MV{m, +lower, +upper, descending} = view
  view_put_checked(~K, ~V, ~cmp, m, k, v, lower, upper, descending, M.in_range(~K, ~V, ~cmp, k, lower, upper))

def delete_fix_step_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: Nat, +p: Nat, pair_result: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & M.DeleteFix:
  (m1, +root_node) = pair_result
  delete_fix_step_2(~K, ~V, ~cmp, x, p, root_node, read(~K, ~V, ~cmp, m1, x))

def delete_fix_step(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat, +p: Nat) -> ST.Sh<K, V> & M.DeleteFix:
  delete_fix_step_1(~K, ~V, ~cmp, x, p, root_id(~K, ~V, ~cmp, m))

def delete_fix_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: ST.Sh<K, V> & M.DeleteFix) -> ST.Sh<K, V>:
  match fuel st:
    case 0n Tuple{px4, px5}:
      black_root(~K, ~V, ~cmp, px4)
    case 1n+px3 Tuple{px6, M.DF{px8, px9, False{}}}:
      black_root(~K, ~V, ~cmp, px6)
    case 1n+px3 Tuple{px6, M.DF{px8, px9, True{}}}:
      delete_fix_loop(~K, ~V, ~cmp, px3, delete_fix_step(~K, ~V, ~cmp, px6, px8, px9))

def delete_repair(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +x: Nat, +p: Nat, +was_red: Bool) -> ST.Sh<K, V>:
  match m:
    case ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}:
      delete_fix_loop(~K, ~V, ~cmp, 1n+n, (ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, M.DF{x, p, Bool.not(was_red)}))

def unlink_2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, +node: M.Node<K>, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m2, +pn) = pair_result
  delete_repair(~K, ~V, ~cmp, recycle(~K, ~V, ~cmp, attach(~K, ~V, ~cmp, m2, M.node_parent(~K, node), M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, node)), M.node_left(~K, node), M.node_right(~K, node)), Nat.is_eq(id, M.node_left(~K, pn))), id), M.pick(Nat, Nat.is_lt(0n, M.node_left(~K, node)), M.node_left(~K, node), M.node_right(~K, node)), M.node_parent(~K, node), M.node_red(~K, node))

def unlink_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V>:
  (m1, +node) = pair_result
  unlink_2(~K, ~V, ~cmp, id, node, read(~K, ~V, ~cmp, m1, M.node_parent(~K, node)))

def unlink(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V>:
  unlink_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))

def unlink_target(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V>:
  (m, id) = r
  refresh_ends(~K, ~V, ~cmp, unlink(~K, ~V, ~cmp, m, id))

def remove_present_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Maybe<&2, V>:
  (m1, value) = pair_result
  (unlink_target(~K, ~V, ~cmp, delete_target(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m1, id))), value)

def remove_present(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & Maybe<&2, V>:
  remove_present_1(~K, ~V, ~cmp, id, exchange(~K, ~V, ~cmp, m, id, None{}))

def remove_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & Maybe<&2, V>:
  match id:
    case 0n:
      (m, None{})
    case 1n+px2:
      remove_present(~K, ~V, ~cmp, m, 1n+px2)

def remove_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Maybe<&2, V>:
  (m, M.Search{id, p, on_left}) = r
  remove_id(~K, ~V, ~cmp, m, id)

def remove_entry_id_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +id: Nat, pair_result: ST.Sh<K, V> & M.Node<K>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  (m1, +node) = pair_result
  entry_value(~K, ~V, ~cmp, M.node_key(~K, node), remove_id(~K, ~V, ~cmp, m1, id))

def iterator_delete_1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool, pair_result: ST.Sh<K, V> & M.Node<K>) -> MCursor<K, V> & Maybe<&2, V>:
  (m1, +node) = pair_result
  iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, node), lower, upper, forward, remove_id(~K, ~V, ~cmp, m1, current))

def remove_if_apply(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat, +replacement: V, +equal: Bool) -> ST.Sh<K, V> & Bool:
  match equal:
    case False{}:
      (m, False{})
    case True{}:
      changed_value(~K, ~V, ~cmp, remove_id(~K, ~V, ~cmp, m, id))

def remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K) -> ST.Sh<K, V> & Maybe<&2, V>:
  remove_found(~K, ~V, ~cmp, search(~K, ~V, ~cmp, m, k))

def remove_entry_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +id: Nat) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  remove_entry_id_1(~K, ~V, ~cmp, id, read(~K, ~V, ~cmp, m, id))

def iterator_delete(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +next: Nat, +current: Nat, lower: M.Bound<K>, upper: M.Bound<K>, +forward: Bool) -> MCursor<K, V> & Maybe<&2, V>:
  iterator_delete_1(~K, ~V, ~cmp, current, lower, upper, forward, read(~K, ~V, ~cmp, m, next))

def remove_if_value(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +id: Nat, +expected: V, +replacement: V, r: ST.Sh<K, V> & Maybe<&2, V>) -> ST.Sh<K, V> & Bool:
  match r:
    case Tuple{px2, None{}}:
      (px2, False{})
    case Tuple{px2, Some{px4}}:
      remove_if_apply(~K, ~V, ~cmp, px2, id, replacement, eq(px4, expected))

def poll_ready(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: ST.Sh<K, V> & Nat) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  (m, id) = r
  remove_entry_id(~K, ~V, ~cmp, m, id)

def view_remove_checked(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>, +k: K, lower: M.Bound<K>, upper: M.Bound<K>, +descending: Bool, +valid: Bool) -> MView<K, V> & Maybe<&2, V>:
  match valid:
    case True{}:
      view_value(~K, ~V, ~cmp, lower, upper, descending, remove(~K, ~V, ~cmp, m, k))
    case False{}:
      (MV{m, lower, upper, descending}, None{})

def iterator_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, cursor: MCursor<K, V>) -> MCursor<K, V> & Maybe<&2, V>:
  MC{m, next, current, lower, upper, forward} = cursor
  iterator_delete(~K, ~V, ~cmp, m, next, current, lower, upper, forward)

def remove_if_found(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, +expected: V, +replacement: V, r: ST.Sh<K, V> & M.Search) -> ST.Sh<K, V> & Bool:
  (m, M.Search{+id, p, on_left}) = r
  remove_if_value(~K, ~V, ~cmp, ~eq, id, expected, replacement, get_id(~K, ~V, ~cmp, m, id))

def poll_first_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  poll_ready(~K, ~V, ~cmp, first_id(~K, ~V, ~cmp, m))

def poll_last_entry(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: ST.Sh<K, V>) -> ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>:
  poll_ready(~K, ~V, ~cmp, last_id(~K, ~V, ~cmp, m))

def view_remove(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>, +k: K) -> MView<K, V> & Maybe<&2, V>:
  MV{m, +lower, +upper, descending} = view
  view_remove_checked(~K, ~V, ~cmp, m, k, lower, upper, descending, M.in_range(~K, ~V, ~cmp, k, lower, upper))

def remove_if_equal(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~eq: V -> V -> Bool, m: ST.Sh<K, V>, +k: K, +expected: V) -> ST.Sh<K, V> & Bool:
  remove_if_found(~K, ~V, ~cmp, ~eq, expected, expected, search(~K, ~V, ~cmp, m, k))

def view_clear_loop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +fuel: Nat, st: MCursor<K, V> & Maybe<&2, M.Entry<K, V>>) -> MView<K, V>:
  match fuel st:
    case 0n Tuple{px4, None{}}:
      iterator_view(~K, ~V, ~cmp, px4)
    case 0n Tuple{px4, Some{px6}}:
      iterator_view(~K, ~V, ~cmp, px4)
    case 1n+px3 Tuple{px7, None{}}:
      iterator_view(~K, ~V, ~cmp, px7)
    case 1n+px3 Tuple{px7, Some{px9}}:
      view_clear_loop(~K, ~V, ~cmp, px3, view_clear_next(~K, ~V, ~cmp, iterator_remove(~K, ~V, ~cmp, px7)))

def view_clear(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, view: MView<K, V>) -> MView<K, V>:
  match view:
    case MV{ST.SH{+n, +root, +lo, +hi, +free, +l_0, +d_0, +nl_0, +pl_0, +t_0, +fl_0}, lower, upper, descending}:
      view_clear_loop(~K, ~V, ~cmp, 1n+n, iterator_next(~K, ~V, ~cmp, view_iterator(~K, ~V, ~cmp, MV{ST.SH{n, root, lo, hi, free, l_0, d_0, nl_0, pl_0, t_0, fl_0}, lower, upper, descending})))