From 154d09e82a8e9cdb44af88196e35c9a8f699b197 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Thir=C3=A9?=
 <francois.thire@nomadic-labs.com>
Date: Wed, 5 Oct 2022 10:44:57 +0200
Subject: [PATCH] Protocol/DAL: Fix and test the specification of search

---
 .../lib_protocol/skip_list_repr.mli           | 12 ++--
 .../test/unit/test_skip_list_repr.ml          | 61 +++++++++++++++++++
 2 files changed, 69 insertions(+), 4 deletions(-)

diff --git a/src/proto_alpha/lib_protocol/skip_list_repr.mli b/src/proto_alpha/lib_protocol/skip_list_repr.mli
index 489d6e74f914..44c69663959d 100644
--- a/src/proto_alpha/lib_protocol/skip_list_repr.mli
+++ b/src/proto_alpha/lib_protocol/skip_list_repr.mli
@@ -151,8 +151,8 @@ module type S = sig
 
      - 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] and the
-     path is minimal.
+     [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,
@@ -176,8 +176,12 @@ module type S = sig
      [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 the minimal path from [cell]
-     to [lower]. *)
+     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. *)
   val search :
     deref:('ptr -> ('content, 'ptr) cell option) ->
     compare:('content -> int Lwt.t) ->
diff --git a/src/proto_alpha/lib_protocol/test/unit/test_skip_list_repr.ml b/src/proto_alpha/lib_protocol/test/unit/test_skip_list_repr.ml
index f482fdf12c29..4a6fad10255b 100644
--- a/src/proto_alpha/lib_protocol/test/unit/test_skip_list_repr.ml
+++ b/src/proto_alpha/lib_protocol/test/unit/test_skip_list_repr.ml
@@ -304,6 +304,61 @@ let test_minimal_back_path () =
          (M.back_path l start target, expected_path))
        cases)
 
+let test_search_non_minimal_back_path () =
+  let basis = 2 in
+  let module M = TestNat (struct
+    let basis = basis
+  end) in
+  let l = M.nlist basis 100 in
+  let index_of_content candidate =
+    match List.find (fun (_, cell) -> cell = candidate) l.cells with
+    | None -> assert false
+    | Some (x, _) -> x
+  in
+  let deref x = match M.deref l x with None -> assert false | Some x -> x in
+  (* This target is chosen to demonstrate that the path is not always
+     minimal, but this happens only on the very last node. [target]
+     must be odd to ensure the content is not in the list. *)
+  let target = 17 in
+  let start_index = 100 in
+  let start = deref start_index in
+  (* Since we are only checking the minimality of the path returned by
+     search, we assume the other part of the [search] specification to
+     be correct below (hence the [assert false]). *)
+  match M.search l start target with
+  | M.{last_cell = Nearest {lower; upper = Some upper}; rev_path} -> (
+      match rev_path with
+      | [] ->
+          (* By specification of the function [search]. *)
+          assert false
+      | _lower :: upper_path as lower_path -> (
+          (* We check the upper path is minimal. *)
+          let upper_index = index_of_content upper in
+          match M.back_path l start_index upper_index with
+          | None ->
+              (* By specification of the function [search]. *)
+              assert false
+          | Some upper_expected_path ->
+              if List.rev upper_path = List.map deref upper_expected_path then
+                (* We check the lower path is not minimal. *)
+                let lower_index = index_of_content lower in
+                match M.back_path l start_index lower_index with
+                | None ->
+                    (* By specification of the function [search]. *)
+                    assert false
+                | Some lower_expected_path ->
+                    if List.rev lower_path = List.map deref lower_expected_path
+                    then
+                      failwith
+                        "The path returned is minimal while it should not be \
+                         the case."
+                    else return ()
+              else (* By specification of the function [search]. *)
+                assert false))
+  | _ ->
+      (* The cell does not exist in the list. *)
+      assert false
+
 let test_skip_list_nat_check_path_with_search (basis, i, j) =
   let module M = TestNat (struct
     let basis = basis
@@ -369,4 +424,10 @@ let tests =
         let* i = 0 -- 10 in
         return (basis, i))
       test_skip_list_nat_check_invalid_path_with_search;
+    (* We cheat here to avoid mixing non-pbt tests with pbt tests. *)
+    Tztest.tztest_qcheck2
+      ~name:"Skip list: `seearch` may not produce minimal path"
+      ~count:10
+      QCheck2.Gen.unit
+      test_search_non_minimal_back_path;
   ]
-- 
GitLab