find ~deref ~cell_ptr ~target_index returns Some cell where cell is the cell at position target_index. This is done by dereferencing the last pointer of the path returned by back_path.

back_path ~deref ~cell_ptr ~target_index returns Some path where path is a sequence of back pointers to traverse to go from cell_ptr to the cell at position target_index in the sequence denoted by (deref, cell_ptr).

valid_back_path ~equal_ptr ~deref ~cell_ptr ~target_ptr path returns true iff path is a valid and minimal path from cell_ptr to target_ptr in the skip list denoted by (deref, cell_ptr).

search ~deref ~compare ~cell allows to find a cell of the skip list according to its content. This function assumes that the content of the cells is in increasing order according to the ordering defined by the function compare. In other words, this function assumes that compare is a function that returns a negative integer for cells before the target and a positive integer for cells after the target. The value returned by this function is {rev_path; last_cell} such that.

• rev_path = [] if and only if compare (content cell) > 0

• For all the cases below, if there is a path from cell A to cell B, rev_path contains the list of cells to go from B to A. Consequently, the first element of rev_path is B. Except for Nearest_lower, this path is a minimal path.

• last_pointer = Deref_returned_none if deref fails to associate a cell to a pointer during the search. In that case, rev_path is a path from cell to candidate where candidate is the last cell for which candidate did not fail and such that compare (content (candidate)) > 0.

• last_pointer = No_exact_or_lower_ptr if for all cell of the skip list, compare (content cell) > 0. In that case, rev_path is a path from cell to the genesis cell.

• last_pointer = Found target if there is a cell target such that compare (content target) = 0 and a path from cell to target. In that case, rev_path is the minimal path from cell to target.

• last_pointer = Nearest_lower {lower;upper} if there is no cell in the skip list such that compare (content cell) = 0. In that case lower is the unique cell such that compare (content lower) < 0 and for all other cells candidate such that compare (content candidate) < 0 then there is a path from lower to candidate. upper, if it exists is the successor cell to lower, i.e. deref ((back_pointer upper) 0) = Some lower. In that case, rev_path is a path from cell to lower. This path is *NOT* minimal but almost. The path is minimal from cell to upper=Some up. By minimality, the path is logarithmic. Consequently, since there is a direct pointer from up to lower, the passe to lower is also logarithmic.

If a target cell target_cell exists, i.e. there is a cell such that compare target_cell = 0, then it is not necessary for deref to return Some cell for all cell such that compare cell < 0. If a target_cell does not exist, the lowest bound for which deref must return Some cell is unknown.