Skip to main content

🔗 Skip_list_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.FallbackArray.

Module Cell.
  Module Valid.
    Import Proto_alpha.Skip_list_repr.S.

A cell is valid when it is produced either using the [genesis] or the [next] operator.
    Inductive t {cell : Set Set Set} {content ptr : Set}
      {L : Skip_list_repr.S (cell := cell)}
      {deref : ptr option (cell content ptr)}
      : cell content ptr Prop :=
    | Is_genesis content : t (L.(genesis) content)
    | Is_next prev_cell prev_ptr content :
      t prev_cell
      deref prev_ptr = Some prev_cell
      t (L.(next) prev_cell prev_ptr content).
  End Valid.
End Cell.

Module Deref.
  Module Valid.
    Import Proto_alpha.Skip_list_repr.S.

The dereferencing operator is valid when all its target cells are valid.
    Definition t {cell : Set Set Set} {content ptr : Set}
      (L : Skip_list_repr.S (cell := cell))
      (deref : ptr option (cell content ptr)) : Prop :=
       ptr cell, deref ptr = Some cell
      Cell.Valid.t (L := L) (deref := deref) cell.
  End Valid.
End Deref.

We split properties described in this module into individual lemmas, Using `{FArgs} to represent the current functor parameters without having to repeat it
Module S.
  Module Valid.
    Import Proto_alpha.Skip_list_repr.S.

The validity of a skip list implementation.
    Record t {cell : Set Set Set} {content ptr : Set}
      {L : Skip_list_repr.S (cell := cell)}
      {deref : ptr option (cell content ptr)} : Prop := {
      equal equal_content equal_ptr :
        Compare.Equal.Valid.t (a := content) (fun _True) equal_content
        Compare.Equal.Valid.t (a := ptr) (fun _True) equal_ptr
        Compare.Equal.Valid.t (fun _True)
          (L.(equal) equal_content equal_ptr);
      encoding encoding_ptr encoding_cell :
        Data_encoding.Valid.t (a := ptr) (fun _True) encoding_ptr
        Data_encoding.Valid.t (a := content) (fun _True) encoding_cell
        Data_encoding.Valid.t (fun _True)
          (L.(encoding) encoding_ptr encoding_cell);
      back_pointer (cell : cell content ptr) index :
        L.(back_pointer) cell index = List.nth (L.(back_pointers) cell) index;
      back_pointers (cell : cell content ptr) :
        List.Forall (fun ptrderef ptr None)
          (L.(back_pointers) cell);
      genesis_content (content : content) :
        L.(Skip_list_repr.S.content) (L.(genesis) (ptr := ptr) content) =
        content;
      genesis_index (content : content) :
        L.(index_value) (L.(genesis) (ptr := ptr) content) =
        0;
      next_content prev_cell (prev_ptr : ptr) (content : content) :
        L.(Skip_list_repr.S.content) (L.(next) prev_cell prev_ptr content) =
        content;
      next_index prev_cell (prev_ptr : ptr) (content : content) :
        L.(index_value) (L.(next) prev_cell prev_ptr content) =
        L.(index_value) prev_cell +i 1;
      
The primitive [back_path] produces a valid path according to [valid_back_path].
      back_path_is_valid equal_ptr cell_ptr target_ptr target_cell path :
        Compare.Equal.Valid.t (fun _True) equal_ptr
        deref target_ptr = Some target_cell
        let target_index := L.(index_value) target_cell in
        L.(back_path) deref cell_ptr target_index = Some path
        L.(valid_back_path) equal_ptr deref cell_ptr target_ptr path = true;
      
The path produced by [back_path] is the only acceptable one for [valid_back_path].
      back_path_is_uniq equal_ptr cell_ptr target_ptr target_cell path :
        Compare.Equal.Valid.t (fun _True) equal_ptr
        deref target_ptr = Some target_cell
        let target_index := L.(index_value) target_cell in
        L.(valid_back_path) equal_ptr deref cell_ptr target_ptr path = true
        L.(back_path) deref cell_ptr target_index = Some path;
    }.
    Arguments t {_ _ _}.
  End Valid.
End S.

Module Make.
  Import Proto_alpha.Skip_list_repr.Make.

  Module Back_pointers.
    Module Valid.
Validity of the back-pointers array, given its list of items.
      Record t {ptr : Set} (items : list ptr)
        (x : FallbackArray.t (option ptr)) : Prop := {
        of_list : x = FallbackArray.of_list None Some items;
        int_length : List.Int_length.t items;
      }.
    End Valid.
  End Back_pointers.

  Module Cell.
    Import Proto_alpha.Skip_list_repr.Make.cell.

    Module Valid.
Validity of a cell.
      Record t `{FArgs} {content ptr : Set} (value : cell content ptr) : Prop := {
          v_items : items, Back_pointers.Valid.t items value.(back_pointers)
                               value.(cell.index) = List.length items;
          v_index_int : Pervasives.Int31.Valid.t value.(cell.index);
          v_all_not_none : Forall (fun itemitem None)
                             value.(cell.back_pointers).(FallbackArray.t.items);
          v_default_none : value.(cell.back_pointers).(FallbackArray.t.default)
                           = None }.
    End Valid.
  End Cell.

Simplified definition of the equality check between two list of items. Note that we actually check that [items1] is a prefix of [items2].
  Fixpoint equal_back_pointers_simple {ptr : Set}
    (equal_ptr : ptr ptr bool) (items1 items2 : list ptr) :=
    match items1, items2 with
    | [], _true
    | item1 :: items1, item2 :: items2
      equal_ptr item1 item2 &&
      equal_back_pointers_simple equal_ptr items1 items2
    | _ :: _, []false
    end.

[equal_back_pointers_simple] is reflexive.
  Lemma equal_back_pointers_simple_refl {ptr : Set}
    (equal_ptr : ptr ptr bool) items :
    ( item, equal_ptr item item = true)
    equal_back_pointers_simple equal_ptr items items = true.
  Proof.
    intros; induction items; hauto lq: on.
  Qed.

[equal_back_pointers_simple] is anti-symmetric for two lists of the same length.
  Lemma equal_back_pointers_simple_anti_sym {ptr : Set}
    (equal_ptr : ptr ptr bool) items1 items2 :
    ( item1 item2, equal_ptr item1 item2 = true item1 = item2)
    Lists.List.length items1 = Lists.List.length items2
    equal_back_pointers_simple equal_ptr items1 items2 = true
    items1 = items2.
  Proof.
    intros H_equal_ptr; generalize items2; clear items2.
    induction items1 as [|item1 items1]; simpl; intros items2 H_length H_eq.
    { sauto lq: on. }
    { destruct items2 as [|item2 items2].
      { sfirstorder. }
      { destruct (andb_prop _ _ H_eq) as [H_eq_item H_eq_items].
        hauto q: on.
      }
    }
  Qed.

A reduction step for [equal_back_pointers_simple] to use later in a proof by induction.
  Lemma equal_back_pointers_simple_step {ptr : Set}
    (equal_ptr : ptr ptr bool) items1 x1 items2 :
    List.Int_length.t items1
    equal_back_pointers_simple equal_ptr (items1 ++ [x1]) items2 =
    (equal_back_pointers_simple equal_ptr items1 items2 &&
    match List.nth items2 (List.length items1) with
    | Some x2equal_ptr x1 x2
    | Nonefalse
    end).
  Proof.
    generalize items2; clear items2.
    induction items1 as [|item1 items1]; simpl; intros.
    { destruct items2; simpl; [reflexivity|].
      now rewrite Bool.andb_true_r.
    }
    { destruct items2 as [|item2 items2]; simpl; [reflexivity|].
      rewrite <- Bool.andb_assoc; f_equal; [hauto lq: on|].
      unfold List.Int_length.t in H; simpl in H.
      rewrite IHitems1 by lia.
      f_equal; [hauto lq: on|].
      replace (List.length items1 +i 1 - 1) with (List.length items1).
      2: {
        rewrite List.length_eq.
        lia.
      }
      destruct (List.length items1 +i 1) eqn:?;
        rewrite List.length_eq in *; lia.
    }
  Qed.

A generalized version of the equality check of two arrays of pointers.
  Definition equal_back_pointers_generalized {ptr : Set}
    (equal_ptr : ptr ptr bool) (rev_prefix1 suffix1 items2 : list ptr) :=
    List.fold_left
      (fun acc item1
        (let '(equal, i) := acc in
        fun opt_item1
          (
            equal && Option.equal equal_ptr opt_item1 (List.nth items2 i),
            i +i 1
          )
        ) (Some item1)
      )
      (
        equal_back_pointers_simple equal_ptr (List.rev rev_prefix1) items2,
        List.length rev_prefix1
      )
      suffix1.

[equal_back_pointers_generalized] expressed with [equal_back_pointers_simple].
  Lemma equal_back_pointers_generalized_eq {ptr : Set}
    (equal_ptr : ptr ptr bool) rev_prefix1 suffix1 items2 :
    List.Int_length.t (rev_prefix1 ++ suffix1)
    let items1 := (List.rev rev_prefix1 ++ suffix1)%list in
    equal_back_pointers_generalized equal_ptr rev_prefix1 suffix1 items2 =
    (
      equal_back_pointers_simple equal_ptr items1 items2,
      List.length items1
    ).
  Proof.
    generalize rev_prefix1; clear rev_prefix1.
    induction suffix1 as [|item1 suffix1]; simpl; intros; cbn.
    { now rewrite List.app_nil_r, List.length_rev_eq. }
    { pose proof (IHsuffix1 (item1 :: rev_prefix1)) as H_ind.
      unfold equal_back_pointers_generalized in H_ind.
      rewrite <- List.length_rev_eq.
      rewrite <- equal_back_pointers_simple_step.
      2: {
        unfold List.Int_length.t in ×.
        rewrite List.app_length in ×.
        unfold List.rev, Lists.List.rev'.
        rewrite <- List.rev_alt.
        rewrite List.rev_length.
        lia.
      }
      repeat rewrite <- List.rev_head_app_eq.
      simpl in H_ind.
      rewrite <- H_ind.
      2: {
        unfold List.Int_length.t in ×.
        simpl.
        rewrite List.app_length in ×.
        simpl in ×.
        lia.
      }
      f_equal.
      now rewrite List.app_nil_r, List.length_rev_eq.
    }
  Qed.

Definition extracted from the generated Coq code of [equal].
  Definition equal_back_pointers {ptr : Set}
    (equal_ptr : ptr ptr bool)
    (b1 : FallbackArray.t (option ptr)) (b2 : FallbackArray.t (option ptr))
    : bool :=
    ((FallbackArray.length b1) =i (FallbackArray.length b2)) &&
    (Pervasives.fst
      (FallbackArray.fold
        (fun (function_parameter : bool × int) ⇒
          let '(equal, i_value) := function_parameter in
          fun (h1 : option ptr) ⇒
            ((equal &&
            (Option.equal equal_ptr h1 (FallbackArray.get b2 i_value))),
              (i_value +i 1))) b1 (true, 0))).

[equal_back_pointers] expressed with [equal_back_pointers_simple].
  Lemma equal_back_pointers_eq {ptr : Set}
    (equal_ptr : ptr ptr bool) items1 items2 :
    let b1 := FallbackArray.of_list None Some items1 in
    let b2 := FallbackArray.of_list None Some items2 in
    List.Int_length.t items1
    equal_back_pointers equal_ptr b1 b2 =
      (List.length items1 =? List.length items2) &&
      equal_back_pointers_simple equal_ptr items1 items2.
  Proof.
    unfold equal_back_pointers; simpl; intros.
    repeat rewrite FallbackArray.Of_list.length_eq.
    f_equal; [hauto lq: on|].
    rewrite FallbackArray.Of_list.fold_eq.
    replace (FallbackArray.get _) with (List.nth items2).
    2: {
      apply FunctionalExtensionality.functional_extensionality; intro.
      now rewrite FallbackArray.Of_list.get_eq.
    }
    pose proof (equal_back_pointers_generalized_eq equal_ptr [] items1 items2)
      as H_eq.
    unfold equal_back_pointers_generalized in H_eq; simpl in H_eq.
    sauto lq: on.
  Qed.

The equality function [equal_back_pointers] is valid.
  Lemma equal_back_pointers_is_valid {ptr : Set}
    (equal_ptr : ptr ptr bool) :
    Compare.Equal.Valid.t (fun _True) equal_ptr
    Compare.Equal.Valid.t
      (fun b items, Back_pointers.Valid.t items b)
      (equal_back_pointers equal_ptr).
  Proof.
    intros H_equal_ptr b1 b2
      [items1 [H_b1_eq H_b1_length]]
[items2 [H_b2_eq H_b2_length]].
    rewrite H_b1_eq, H_b2_eq.
    rewrite equal_back_pointers_eq by trivial.
    split; intro H.
    { pose proof (FallbackArray.Of_list.of_list_inj _ _ H) as H_eq.
      rewrite <- H_eq.
      apply andb_true_intro; split; [lia|].
      apply equal_back_pointers_simple_refl.
      intro item.
      destruct (H_equal_ptr item item); hauto l: on.
    }
    { assert (items1 = items2); [|congruence].
      destruct (andb_prop _ _ H) as [H_length H_simple].
      apply (equal_back_pointers_simple_anti_sym equal_ptr).
      { intros item1 item2; destruct (H_equal_ptr item1 item2); hauto l: on. }
      { assert (H_length_eq : List.length items1 = List.length items2) by lia.
        repeat rewrite List.length_eq in H_length_eq.
        lia.
      }
      { trivial. }
    }
  Qed.

The equality function [equal] is valid.
  Lemma equal_is_valid `{FArgs} {content ptr : Set} equal_content equal_ptr :
    Compare.Equal.Valid.t (a := content) (fun _True) equal_content
    Compare.Equal.Valid.t (a := ptr) (fun _True) equal_ptr
    Compare.Equal.Valid.t Cell.Valid.t (equal equal_ptr equal_content).
  Proof.
    intros H_content H_ptr.
    replace (equal _ _) with (
      Compare.Equal.projection (fun cell
        let '{|
          cell.content := content;
          cell.back_pointers := back_pointers;
          cell.index := index
        |} := cell in
        (content, index, back_pointers)
      )
      (Compare.Equal.couple
        (Compare.Equal.couple
          equal_content
          Compare.Int.equal)
        (equal_back_pointers equal_ptr)
      )
    ).
    2: {
      do 2 (apply FunctionalExtensionality.functional_extensionality; intro).
      unfold equal; cbn.
      now destruct equal_content.
    }
    eapply Compare.Equal.Valid.implies.
    2: {
      apply Compare.Equal.projection_is_valid; [|sauto lq: on].
      repeat apply Compare.Equal.couple_is_valid;
        try apply H_content;
        try (apply equal_back_pointers_is_valid; apply H_ptr);
        try apply Compare.Equal.int_is_valid.
    }
    sauto l: on.
  Qed.

  Definition back_pointers_to_list_generalized `{FArgs} {A : Set}
    (rev_prefix : list A) (array : FallbackArray.t (option A)) : list A :=
    List.rev
      (FallbackArray.fold
         (fun l item
            match item with
            | Some itemitem :: l
            | Noneassert (list A) false
            end)
         array rev_prefix).

  Lemma back_pointers_to_list_generalized_eq `{FArgs} {A : Set}
    (rev_prefix l : list A) :
    let array := FallbackArray.of_list None Some l in
    back_pointers_to_list_generalized rev_prefix array =
      (List.rev rev_prefix ++ l)%list.
  Proof.
    unfold back_pointers_to_list_generalized.
    generalize rev_prefix; clear rev_prefix.
    induction l as [|x l]; intros; rewrite FallbackArray.Of_list.fold_eq; simpl.
    { now rewrite List.app_nil_r. }
    { pose proof (IHl (x :: rev_prefix)) as H_ind.
      rewrite FallbackArray.Of_list.fold_eq in H_ind.
      rewrite H_ind.
      unfold List.rev, Lists.List.rev'.
      repeat rewrite List.rev_append_rev; simpl.
      repeat rewrite List.app_nil_r.
      now rewrite <- List.app_assoc.
    }
  Qed.

  Lemma back_pointers_to_list_eq `{FArgs} {A : Set} (l : list A) :
    let array := FallbackArray.of_list None Some l in
    back_pointers_to_list array = l.
  Proof.
    apply back_pointers_to_list_generalized_eq.
  Qed.

Below we prove that encoding function [encoding] is valid, in order to do so, we need some auxillary definitions and lemmas
Generalized version of [back_pointers_of_list] function, we need it to generalize accumulator [rev_prefix : list ptr]
  Definition back_pointers_of_list_generalized `{FArgs} {ptr : Set}
    (rev_prefix : list ptr) (array : FallbackArray.t (option ptr)) :
    FallbackArray.t (option ptr) :=
    {|
      t.items :=
        Lists.List.map Some
          (rev
             (FallbackArray.fold
                (fun (l_value : list ptr) (function_parameter : M× ptr) ⇒
                   match function_parameter with
                   | Some ptr0ptr0 :: l_value
                   | Noneassert (list ptr) false
                   end) array rev_prefix));
      t.default := None
    |}.

We show equality of result of work of [back_pointers_of_list_generalized] in combination with any initial array [rev_prefix]. We will use this definition for [rewrite] tactic in the proof of Lemma [back_pointers_of_list_to_list], which, in turn, will be used to prove the main lemma: [encoding_pt_cell].
  Lemma back_pointers_of_list_generalized_eq `{FArgs} {ptr : Set}
    (rev_prefix : list ptr) (array : FallbackArray.t (option ptr)):
    array.(FallbackArray.t.default) = None
    Forall (fun itemitem None) (array.(FallbackArray.t.items))
    back_pointers_of_list_generalized rev_prefix array =
      {| t.items :=
          List.rev (Lists.List.map Some rev_prefix) ++
            array.(FallbackArray.t.items) ;
        t.default := array.(FallbackArray.t.default) |}.
  Proof.
    intros.
    unfold back_pointers_of_list_generalized.
    generalize rev_prefix. clear rev_prefix.
    destruct array. induction items as [| x items].
    intros. simpl. rewrite List.app_nil_r. cbn.
    simpl in H0. rewrite H0. f_equal.
    unfold rev, rev'. induction rev_prefix; try reflexivity; simpl.
    rewrite rev_append_rev.
    replace [a] with ([] ++ [a])%list by reflexivity.
    rewrite app_assoc, <- rev_append_rev, map_app, IHrev_prefix,
      rev_append_rev, app_nil_r, rev_append_rev; reflexivity.
    { (* inductive case  *)
      intros. f_equal. simpl in H0. specialize (IHitems H0).
      simpl. destruct x eqn:Destruct_X. cbn. apply Forall_inv_tail in H1.
      specialize (IHitems H1 (p::rev_prefix)). cbn in IHitems.
      injection IHitems as IHitems. rewrite IHitems.
      unfold rev, rev'. rewrite rev_append_rev, <- app_assoc, rev_append_rev,
        app_nil_r; sfirstorder. apply Forall_inv in H1; sfirstorder.
      sfirstorder. }
  Qed.

We will need this property in the main [encoding_pt_cell] lemma
  Lemma back_pointers_of_list_to_list `{FArgs} {ptr : Set}
    ( bp : FallbackArray.t (M× ptr)) :
    bp.(FallbackArray.t.default) = None
    Forall (fun itemitem None) (bp.(FallbackArray.t.items))
    of_list None Some (back_pointers_to_list bp) = bp.
    intros.
    apply back_pointers_of_list_generalized_eq; trivial.
  Qed.

In the lemma [encoding_pt_cell] we prove validity of encoding function.
  Lemma encoding_pt_cell `{FArgs} {content ptr : Set}
    encoding_ptr encoding_cell :
    Data_encoding.Valid.t (a := ptr) (fun _True) encoding_ptr
    Data_encoding.Valid.t (a := content) (fun _True) encoding_cell
    Data_encoding.Valid.t Cell.Valid.t (encoding encoding_ptr encoding_cell).
  Proof.
    intros. split. intros value H2. destruct value.
    eapply Data_encoding.Valid.of_bytes_opt_to_bytes_opt.
    Data_encoding.Valid.data_encoding_auto.
    split. simpl. split. destruct H2. tauto.
    split; [apply I |]. apply List.Forall_True. trivial.
    simpl in ×. inversion H2.
    pose proof (back_pointers_of_list_to_list back_pointers0 v_default_none v_all_not_none).
    hauto lq: on.
    eapply Data_encoding.Valid.to_bytes_opt_of_bytes_opt.
    Data_encoding.Valid.data_encoding_auto.
    intros [] []; simpl in ×.
    rewrite back_pointers_of_list_to_list by easy.
    hauto l: on.
  Qed.
  #[global] Hint Resolve encoding_pt_cell : Data_encoding_db.

  Lemma back_pointer_lst_nth `{FArgs} {content ptr : Set}
    (cell : cell content ptr) index :
    Cell.Valid.t cell
    back_pointer cell index = List.nth (back_pointers cell) index.
  Proof.
    intros.
    unfold back_pointer.
    match goal with
    | H : Cell.Valid.t _ |- _
        inversion H
    end.
    destruct v_items. repeat destruct H1.
    rewrite of_list, FallbackArray.Of_list.get_eq.
    f_equal; unfold back_pointers; rewrite of_list.
    now rewrite back_pointers_to_list_eq.
  Qed.

  Module Back_pointers_valid.
    Module Valid.
      Definition t `{FArgs} {content_type ptr_type c : Set}
        (cell : cell content_type ptr_type)
        (deref : ptr_type option c) : Prop :=
        List.Forall (fun ptrderef ptr None) (back_pointers cell).
    End Valid.
  End Back_pointers_valid.

  Lemma back_pointers `{FArgs} {content_type ptr_type : Set}
    {deref : ptr_type option (cell content_type ptr_type)}
    (cell : cell content_type ptr_type) :
    Back_pointers_valid.Valid.t cell deref
    List.Forall (fun ptrderef ptr None)
      (back_pointers cell).
  Proof.
    intros. inversion H0.
    apply Forall_nil.
    apply Forall_cons; trivial.
  Qed.

  Lemma genesis_content `{FArgs} {content_type ptr_type : Set}
    (content_value : content_type) :
    content (genesis (B := ptr_type) content_value) = content_value.
  Proof.
    reflexivity.
  Qed.

  Lemma genesis_index `{FArgs} {content_type ptr_type : Set}
    (content : content_type)
    (ptr : ptr_type) :
    index_value (genesis (B := ptr_type) content) = 0.
  Proof.
    reflexivity.
  Qed.

  Lemma next_content `{FArgs} {content_type ptr_type : Set}
    (prev_ptr : ptr_type) (content_value : content_type) prev_cell :
    content (next (A := content_type) prev_cell prev_ptr content_value) =
      content_value.
  Proof.
    reflexivity.
  Qed.

  Lemma next_index `{FArgs} {content_type ptr_type : Set}
    prev_cell
    (prev_ptr : ptr_type) (content : content_type) :
    index_value (next (A := content_type) prev_cell prev_ptr content) =
      index_value prev_cell +i 1.
  Proof.
    reflexivity.
  Qed.

Here starts the proof of the [Lemma back_path_is_valid]. We decompose all the functions to the smaller ones, getting rid of nested definitions. This will make it easier to do formal reasoning in proofs. To be able to run reduction we equip functions, marked in source code by [bypass ] with [fuel].
We retrieve inner function aux out of back_path and equip it with fuel
  Fixpoint aux' `{FArgs} {A B : Set}
    (deref : A option (cell B A)) (powers : FallbackArray.t int)
    (target_index : int) (path : list A) (ptr : A)
    (cell_value : option (cell B A)) (fuel : nat) {struct fuel} :
    option (list A) :=
    match fuel with
    | Datatypes.ONone
    | Datatypes.S fuel
        let path := cons ptr path in
        Option.bind cell_value
          (fun (cell_value : cell B A) ⇒
            let index_value := cell_value.(cell.index) in
            if Compare.Int.(Compare.S.op_eq) target_index index_value then
              Some (List.rev path)
            else
              if Compare.Int.(Compare.S.op_gt) target_index index_value then
                None
              else
                Option.bind (best_skip cell_value target_index powers)
                  (fun (best_idx : int) ⇒
                    Option.bind (back_pointer cell_value best_idx)
                      (fun (ptr : A) ⇒
                         aux' deref powers target_index path ptr
                           (deref ptr) fuel)))
    end.

Generalization of fuel
  Parameter bp_compute_fuel : `{FArgs} {A B : Set}
    (deref : A option (cell B A)) (powers : FallbackArray.t int)
    (cell_ptr : A) (target_index : int),
      Datatypes.nat.

We define [back_path'] - the simulation of [back_path]
  Definition back_path' `{FArgs} {A B : Set}
    (deref : A option (cell B A)) (cell_ptr : A) (target_index : int)
    : option (list A) :=
      Option.bind (deref cell_ptr)
        (fun (cell_value : cell B A) ⇒
          let powers := list_powers cell_value in
            aux' deref powers target_index nil cell_ptr
              (deref cell_ptr)
              (bp_compute_fuel deref powers cell_ptr target_index)).

We axiomatize equality of our simulation and initial [back_path]
  Axiom back_path_eq : `{FArgs} {A B : Set}
    (deref : A option (cell B A)) (cell_ptr : A)
    (target_index : int),
      back_path deref cell_ptr target_index =
        back_path' deref cell_ptr target_index.

Another way of defining the inner function - for some lemmas it is more useful to use that definition, but it is not exactly the same as the [back_path] inner [aux], so instead of axiomatizing we prove its equivalence
  Fixpoint aux'' `{H : FArgs} {A B : Set} (fuel : Datatypes.nat)
    (deref : A option (cell B A)) (powers : FallbackArray.t int)
    (target_index : int) (path : list A) (ptr : A) : option (list A) :=
  match fuel with
  | Datatypes.ONone
  | Datatypes.S fuel
      let path := cons ptr path in
      Option.bind (deref ptr)
        (fun (cell_value : cell B A) ⇒
          let index_value := cell_value.(cell.index) in
          if Compare.Int.(Compare.S.op_eq) target_index index_value then
            Some (List.rev path)
          else
            if Compare.Int.(Compare.S.op_gt) target_index index_value then
              None
            else
              Option.bind (best_skip cell_value target_index powers)
                (fun (best_idx : int) ⇒
                  Option.bind (back_pointer cell_value best_idx)
                    (fun (ptr : A) ⇒
                       aux'' fuel deref powers target_index path ptr)))
  end.

Lemma states that we have enough fuel (will be used in one-step-reduction proofs)
  Lemma aux'_sufficient_fuel `{FArgs} {A B : Set} (deref : A M× cell B A)
    (powers : FallbackArray.t int) (target_index : int) (path : list A)
    (ptr : A) (cell : M× cell B A) (fuel fuel' : Datatypes.nat)
    (res : list A) :
    aux' deref powers target_index path ptr cell fuel = Some res
    (fuel fuel')%nat
    aux' deref powers target_index path ptr cell fuel' = Some res.
  Proof.
    intros. revert path ptr cell fuel H0 H1.
    induction fuel'; [ sauto lq: on rew: off |].
    intros. destruct fuel; try discriminate. simpl in ×.
    destruct cell0; try discriminate. simpl in ×.
    destruct (target_index =? c.(cell.index)); trivial.
    destruct (target_index >? c.(cell.index)); try discriminate.
    destruct (best_skip c target_index); try discriminate. simpl in ×.
    destruct (back_pointer c i); try discriminate. simpl in ×.
    apply IHfuel' with fuel; intuition.
  Qed.

Equality of simulations
  Lemma aux''_eq_aux' `{FArgs} {A B : Set}
    (deref : A option (cell B A)) (powers : FallbackArray.t int)
    (target_index : int) (path : list A) (ptr : A) (fuel : nat) :
    aux'' fuel deref powers target_index path ptr =
      aux' deref powers target_index path ptr (deref ptr) fuel.
  Proof.
    revert path ptr. induction fuel; trivial. intros. simpl.
    destruct (deref ptr); trivial. simpl in ×.
    destruct (target_index =? c.(cell.index)); trivial.
    destruct (target_index >? c.(cell.index)); trivial.
    destruct (best_skip c target_index); trivial. simpl in ×.
    destruct (back_pointer c i); trivial. now simpl in ×.
  Qed.

Simulation aux'' has enough fuel for inner one-step-reductions
  Lemma aux''_sufficient_fuel `{FArgs} {A B : Set} (deref : A M× cell B A)
    (powers : FallbackArray.t int) (target_index : int) (path : list A)
    (ptr : A) (fuel fuel' : Datatypes.nat) (res : list A) :
    aux'' fuel deref powers target_index path ptr = Some res
    (fuel fuel')%nat
    aux'' fuel' deref powers target_index path ptr = Some res.
  Proof.
    rewrite aux''_eq_aux', aux''_eq_aux'. apply aux'_sufficient_fuel.
  Qed.

Initial cell of successfully generated path can not be [None]
  Lemma back_path'_cell_not_none `{FArgs} {content_type ptr_type : Set}
      (deref : ptr_type option (cell content_type ptr_type))
      (cell_ptr : ptr_type) target_index (path : list ptr_type) :
  back_path' deref cell_ptr target_index = Some path
   c_cell, deref cell_ptr = Some c_cell.
  Proof.
    intros. destruct (deref cell_ptr) eqn:DC.
    { c; reflexivity. }
    { unfold back_path' in H0. rewrite DC in ×. discriminate. }
  Qed.

(* @TODO move to lists library*)
  Lemma list_rev_not_nil {A : Set} : (acc : list A) p,
    rev (p :: acc) = [] False.
  Proof.
    intros. replace (rev (p :: acc))%list with
     ((rev (p :: acc) ++ []))%list in H by hauto lq: on.
    rewrite List.rev_head_app_eq in H.
    symmetry in H.
    apply app_cons_not_nil in H. inversion H.
  Qed.

Result path can not be empty, proved for auxiliary function
  Fixpoint aux'_not_nil `{FArgs} {content_type ptr_type : Set}
      (deref : ptr_type option (cell content_type ptr_type))
      (powers : FallbackArray.t int) target_index (acc_path : list ptr_type)
      cell_ptr (cell : option (cell content_type ptr_type)) fuel {struct fuel} :
    aux' deref powers target_index acc_path cell_ptr cell fuel = Some []
    False.
  Proof.
    unfold aux'.
    destruct fuel. scongruence.
    destruct cell; try scongruence.
    simpl. destruct (target_index =? c.(cell.index)) eqn:TI.
    intro H0. injection H0 as H0.
    apply list_rev_not_nil in H0. inversion H0.
    destruct (target_index >? c.(cell.index)); try scongruence.
    destruct (best_skip c target_index); try scongruence.
    simpl. destruct (back_pointer c i); try scongruence.
    simpl. hauto l: on.
  Qed.

Result path can not be empty, proved for main function
  Fixpoint back_path'_not_nil `{FArgs} {content_type ptr_type : Set}
      (deref : ptr_type option (cell content_type ptr_type))
      (cell_ptr : ptr_type) target_index (path : list ptr_type) :
    back_path' deref cell_ptr target_index = Some [] False.
  Proof.
    unfold back_path'.
    destruct deref; simpl; [| discriminate ].
    apply (aux'_not_nil
      deref (list_powers c) target_index nil cell_ptr (Some c)).
  Qed.

(* @TODO move to lists library*)
  Fact list_rev_cons {A : Set} (a : A) (l : list A) :
    List.rev (a::l) = (List.rev l ++ [a])%list.
  Proof.
    sauto lq: on use: app_nil_r, List.rev_head_app_eq.
  Qed.

Result of sucessfull work of second simulation [aux'']
  Lemma aux''_nonempty_success `{FArgs} {content_type ptr_type : Set}
    (deref : ptr_type option (cell content_type ptr_type))
    (powers : FallbackArray.t int) (cell_ptr : ptr_type)
    (path' : list ptr_type) (target_index : int) (fuel : Datatypes.nat) :
    ( l, aux'' fuel deref powers target_index path' cell_ptr = Some l)
     l,
      aux'' fuel deref powers target_index path' cell_ptr
      = Some (rev path' ++ cell_ptr :: l)%list.
  Proof.
    revert cell_ptr path'.
    induction fuel; intros cell_ptr path' []; try discriminate.
    simpl in ×.
    destruct (deref cell_ptr); try discriminate.
    simpl in ×.
    destruct (target_index =? c.(cell.index)).
    { hauto lq: on use: list_rev_cons. }
    { destruct (target_index >? c.(cell.index)); try discriminate.
      destruct (best_skip c target_index); try discriminate.
      simpl in ×.
      destruct (back_pointer c i); try discriminate.
      simpl in ×.
      specialize IHfuel with p (cell_ptr :: path').
      hauto q: on use: List.app_assoc, list_rev_cons.
    }
  Qed.

Head pointers are equal - one of conditions of valid_path
  Lemma aux''_equal_head `{FArgs} {content_type ptr_type : Set}
    (deref : ptr_type option (cell content_type ptr_type))
    (powers : FallbackArray.t int) (target_index : int)
    (acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
    (fuel : Datatypes.nat) (equal_ptr : ptr_type ptr_type bool) :
      Compare.Equal.Valid.t (fun _True) equal_ptr
      aux'' fuel deref powers target_index acc_path cell_ptr =
        Some (rev acc_path ++ (ptr::rest_path))%list
      equal_ptr ptr cell_ptr = true.
  Proof.
    intros.
    destruct (aux''_nonempty_success
      deref powers cell_ptr acc_path target_index fuel);
    eauto.
    rewrite H1 in H2.
    unfold Compare.Equal.Valid.t in H0.
    hauto lq: on use: List.app_inv_head.
  Qed.

First auxiliary simulation. Proof of it's successfull result
  Lemma aux'_nonempty_success `{FArgs} {content_type ptr_type : Set}
    (deref : ptr_type option (cell content_type ptr_type))
    (powers : FallbackArray.t int) (cell_ptr : ptr_type)
    (path' : list ptr_type) (target_index : int)
    (cell : M× cell content_type ptr_type) (fuel : Datatypes.nat) :
    ( l,
       aux' deref powers target_index path' cell_ptr cell fuel = Some l)
     l,
      aux' deref powers target_index path' cell_ptr cell fuel
      = Some (rev path' ++ cell_ptr :: l)%list.
  Proof.
    revert cell_ptr cell path'.
    induction fuel; intros cell_ptr cell path' []; try discriminate.
    simpl in ×.
    destruct cell; try discriminate.
    simpl in ×.
    destruct (target_index =? c.(cell.index)).
    { hauto lq: on use: list_rev_cons. }
    { destruct (target_index >? c.(cell.index)); try discriminate.
      destruct (best_skip c target_index); try discriminate.
      simpl in ×.
      destruct (back_pointer c i); try discriminate.
      simpl in ×.
      specialize IHfuel with p (deref p) (cell_ptr :: path').
      hauto q: on use: List.app_assoc, list_rev_cons.
    }
  Qed.

[cell_ptr] argument is the head of the successful result of (the first simulation of) [aux] (discarding the accumulator [acc])
  Lemma aux'_equal_Prop_head `{FArgs} {content_type ptr_type : Set}
    (deref : ptr_type option (cell content_type ptr_type))
    (powers : FallbackArray.t int) (target_index : int)
    (acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
    (cell : M× cell content_type ptr_type) (fuel : Datatypes.nat) :
      aux' deref powers target_index acc_path cell_ptr cell fuel =
        Some (rev acc_path ++ (ptr::rest_path))%list
      ptr = cell_ptr.
  Proof.
    intros.
    destruct (aux'_nonempty_success
      deref powers cell_ptr acc_path target_index cell fuel);
    eauto.
    rewrite H0 in H1.
    unfold Compare.Equal.Valid.t in H0.
    hauto lq: on use: List.app_inv_head.
  Qed.

[cell_ptr] is the head of the successful result of [back_path]
  Lemma back_path'_equal_Prop_head `{FArgs} {content_type ptr_type : Set}
      (deref : ptr_type option (cell content_type ptr_type))
      (cell_ptr ptr : ptr_type) (target_index : int) (path : list ptr_type) :
    back_path' deref cell_ptr target_index = Some (ptr :: path)
    ptr = cell_ptr.
  Proof.
    unfold back_path'. destruct deref; simpl; [| discriminate ].
    hauto l: on use: aux'_equal_Prop_head.
  Qed.

Auxiliary function for equality of headers
  Lemma aux'_equal_head `{FArgs} {content_type ptr_type : Set}
    (deref : ptr_type option (cell content_type ptr_type))
    (powers : FallbackArray.t int) (target_index : int)
    (acc_path rest_path : list ptr_type) (cell_ptr ptr : ptr_type)
    (cell : M× cell content_type ptr_type) (fuel : Datatypes.nat)
    (equal_ptr : ptr_type ptr_type bool) :
      Compare.Equal.Valid.t (fun _True) equal_ptr
      aux' deref powers target_index acc_path cell_ptr cell fuel =
        Some (rev acc_path ++ (ptr::rest_path))%list
      equal_ptr ptr cell_ptr = true.
  Proof.
    unfold Compare.Equal.Valid.t. intros. apply H0; trivial.
    hauto lq: on use: aux'_equal_Prop_head.
  Qed.

Auxiliary function for equality of head and a parameter
  Lemma back_path'_equal_head `{FArgs} {content_type ptr_type : Set} equal_ptr
      (deref : ptr_type option (cell content_type ptr_type))
      (cell_ptr ptr : ptr_type) (target_index : int) (path : list ptr_type) :
    Compare.Equal.Valid.t (fun _True) equal_ptr
    back_path' deref cell_ptr target_index = Some (ptr :: path)
    equal_ptr ptr cell_ptr = true.
  Proof.
    unfold back_path'. destruct deref; simpl; [| discriminate ].
    hauto l: on use: aux'_equal_head.
  Qed.

Step of decomposition. We retrieve all nested definitions in order to be able to do different kind of manipulations with them.
  Fixpoint valid_path' `{FArgs} {content_type ptr_type : Set}
    equal_ptr target_ptr (target_cell : cell content_type ptr_type)
    (deref : ptr_type option (cell content_type ptr_type))
    (powers : FallbackArray.t int) (index_value : int) (cell_ptr : ptr_type)
    (path : list ptr_type) {struct path} : bool :=
      let target_index := Skip_list_repr.Make.index_value target_cell in
      match path with
      | []
        (equal_ptr target_ptr cell_ptr) &&
        (Compare.Int.(Compare.S.op_eq) index_value target_index)
      | cell_ptr' :: path
          assume_some (deref cell_ptr)
            (fun (cell_value : cell content_type ptr_type) ⇒
             assume_some (deref cell_ptr')
               (fun (cell' : cell content_type ptr_type) ⇒
                mem equal_ptr cell_ptr' cell_value.(cell.back_pointers) &&
                  assume_some (best_skip cell_value target_index powers)
                    (fun (best_idx : int) ⇒
                     assume_some (back_pointer cell_value best_idx)
                       (fun (best_ptr : ptr_type) ⇒
                        let minimal := equal_ptr best_ptr cell_ptr' in
                        let index' := cell'.(cell.index) in
                          minimal &&
                            (valid_path' equal_ptr target_ptr target_cell deref
                               powers index' cell_ptr' path)))))
       end.

We prove equality of retrieved function and piece of original code, we will use this equality in [rewrite] tactic this in the main proof.
  Fixpoint valid_path_eq
     `{FArgs} {content_type ptr_type : Set}
      (equal_ptr : ptr_type ptr_type bool) (target_ptr : ptr_type)
      (target_cell : cell content_type ptr_type)
      (deref : ptr_type option (cell content_type ptr_type))
      (powers : FallbackArray.t int) (index_value : int) (cell_ptr : ptr_type)
      (path : list ptr_type) :
    (fix valid_path
       (index_value : int) (cell_ptr0 : ptr_type) (path0 : list ptr_type)
         {struct path0} : bool :=
       let target_index := Skip_list_repr.Make.index_value target_cell in
       match path0 with
       | []
           equal_ptr target_ptr cell_ptr0 &&
           (Compare.Int.(Compare.S.op_eq) index_value target_index)
       | cell_ptr' :: path1
           assume_some (deref cell_ptr0)
             (fun (cell_value : cell content_type ptr_type) ⇒
              assume_some (deref cell_ptr')
                (fun (cell' : cell content_type ptr_type) ⇒
                 mem equal_ptr cell_ptr' cell_value.(cell.back_pointers) &&
                   assume_some (best_skip cell_value target_index powers)
                     (fun (best_idx : int) ⇒
                      assume_some (back_pointer cell_value best_idx)
                        (fun (best_ptr : ptr_type) ⇒
                         let minimal := equal_ptr best_ptr cell_ptr' in
                         let index' := cell'.(cell.index) in
                           minimal &&
                             (valid_path index' cell_ptr' path1)))))
       end) index_value cell_ptr path =
      valid_path' equal_ptr target_ptr
        (target_cell : cell content_type ptr_type)
        (deref : ptr_type option (cell content_type ptr_type))
        (powers : FallbackArray.t int) (index_value : int)
        (cell_ptr : ptr_type) (path : list ptr_type).
  Proof.
    destruct path; simpl; [reflexivity|].
    repeat (f_equal; (try apply
              FunctionalExtensionality.functional_extensionality; intro);
                f_equal);
    hauto lq: on.
  Qed.

    (* In this module we have all the auxiliary functions
     for proving back_path'_valid_path'
     which is used in main lemma back_path_is_valid.  *)

  Module Helper_valid.

(* @TODO move to lists library*)
    Fact list_rev_In (A : Set) (a : A) (l : list A) :
      In a l In a (rev l).
    Proof.
      induction l; intuition.
      { hauto q: on use: List.in_app_iff, list_rev_cons. }
      { rewrite list_rev_cons in H1.
        hauto q: on use: List.in_app_iff.
      }
    Qed.

    Lemma rev_one {A : Set} : (a : A), [a] = rev [a].
    Proof.
      sfirstorder.
    Qed.

    (* @TODO move to lists library *)
    Lemma rev_injective {A : Set} :
       (xs ys : list A), rev xs = rev ys xs = ys.
    Proof.
      induction xs; destruct ys; try sfirstorder;
        intro H; unfold rev in H; unfold rev' in H;
        repeat rewrite <- rev_alt in H;
        simpl in H; try (symmetry in H; apply app_cons_not_nil in H);
        try apply app_cons_not_nil in H; try sfirstorder.
      (* inductive case *)
      apply app_inj_tail_iff in H;
      destruct H; unfold rev in IHxs;
      unfold rev' in IHxs;
      repeat rewrite rev_alt in H;
      apply IHxs in H; sfirstorder.
    Qed.

(* @TODO: move to list library *)
    Fact nth_valid_result {A : Set}
      (l : list A) (idx : int) (res : A) :
      nth l idx = Some res
        In res l.
    Proof.
      revert idx. induction l; hauto lq: on.
    Qed.

(* TODO: move to list library *)
    Fact nth_success {A : Set}
      (l : list A) (idx : int) :
      0 idx < Z.of_nat (Datatypes.length l)
         res : A, nth l idx = Some res.
    Proof.
      revert idx. induction l; simpl; intuition.
      destruct idx; intuition. eauto.
    Qed.

(* TODO: move to list library *)
    Fact get_valid_result {A : Set}
      (a : FallbackArray.t A) (idx : int) :
      0 idx < Z.of_nat (Datatypes.length a.(t.items))
        In (FallbackArray.get a idx) a.(t.items).
    Proof.
      destruct a. unfold FallbackArray.get.
      hauto q: on use: nth_success, nth_valid_result.
    Qed.

    Fact normalize_positive_le (i : int) :
      0 i
      normalize_int i i.
    Proof.
      intuition.
    Qed.

(* TODO: move to list library *)
    Fact le_length {A : Set} (l : list A) :
      List.length l Z.of_nat (Datatypes.length l).
    Proof.
      rewrite List.length_eq. apply normalize_positive_le. intuition.
    Qed.

    Fact option_cases {A : Type} (oa : M× A) :
      oa = None ( a : A, oa = Some a).
    Proof.
      destruct oa; eauto.
    Qed.

    Fact to_nat_eq_0_int_le_0 (i : int) :
      Z.to_nat i = 0%nat i 0.
    Proof.
      intuition.
    Qed.

    Fact int_cyclic (i : int) :
      normalize_int (i + two_pow_63) = normalize_int i.
    Proof.
      unfold normalize_int. f_equal. rewrite <- Z.add_assoc.
      rewrite Z.add_comm with two_pow_63 two_pow_62. rewrite Z.add_assoc.
      rewrite <- Z.mul_1_l with two_pow_63. apply Z_mod_plus_full.
    Qed.

    Lemma neg_lt_ind:
       A : BinNums.Z Prop,
      Proper (Logic.eq ==> iff) A
       n : BinNums.Z,
        A (BinInt.Z.pred n)
        ( m : BinNums.Z, m < n A m A (BinInt.Z.pred m))
         m : BinNums.Z, m < n A m.
    Proof.
      intros.
      pose (A' := (fun k'A (- k'))).
      assert ( k, A k A' (- k))
      by (unfold A'; intros; now rewrite Z.opp_involutive).
      apply H3.
      apply Z.lt_ind with (A := A') (n := - n); intuition; unfold A'.
      { now rewrite <- Z.opp_pred, Z.opp_involutive. }
      { rewrite Z.opp_succ. intuition. }
    Qed.

    Lemma neg_le_ind:
       A : BinNums.Z Prop,
      Proper (Logic.eq ==> iff) A
       n : BinNums.Z,
        A n
        ( m : BinNums.Z, m n A m A (BinInt.Z.pred m))
         m : BinNums.Z, m n A m.
    Proof.
      intros.
      apply neg_lt_ind with (n := BinInt.Z.succ n); intuition.
      now rewrite Z.pred_succ.
    Qed.

Inner [mem] equipped with fuel and decomposed
    Fixpoint mem'_aux `{FArgs} {A B : Set} (idx : int)
      (equal : A B bool) (x_value : A)
      (l_value : FallbackArray.t (option B))
      (fuel : Datatypes.nat) {struct fuel}:
      bool :=
        let n_value := FallbackArray.length l_value in
        match fuel with
        | Datatypes.Ofalse
        | Datatypes.S fuel
          if Compare.Int.(Compare.S.op_gteq) idx n_value then
            false
          else
            match FallbackArray.get l_value idx with
            | Nonemem'_aux (idx +i 1) equal x_value l_value fuel
            | Some y_value
              if equal x_value y_value then
                true
              else
                mem'_aux (idx +i 1) equal x_value l_value fuel
            end
        end.

Simulation of [mem] function
    Definition mem' `{FArgs} {A B : Set}
        (equal : A B bool) (x_value : A)
        (l_value : FallbackArray.t (option B))
        (fuel : Datatypes.nat) : bool :=
        mem'_aux 0 equal x_value l_value fuel.

We axiomatize equality of mem function and it's simulation
    Axiom mem_eq : `{FArgs} {A B : Set}
        (equal : A B bool) (x_value : A)
        (l_value : FallbackArray.t (option B))
        (fuel : Datatypes.nat),
        let n_value := FallbackArray.length l_value in
      ((Z.to_nat n_value) fuel)%nat
      mem equal x_value l_value =
      mem' equal x_value l_value fuel.

Inductive predicate for easier case-analysis reasoning
    Inductive mem_aux_Prop `{FArgs} {A B : Set} (idx : int)
      (equal : A B bool) (x_value : A)
      (l_value : FallbackArray.t (option B)) : Prop :=
    | maP_None :
        idx >=? FallbackArray.length l_value = false
        FallbackArray.get l_value idx = None
        mem_aux_Prop (idx +i 1) equal x_value l_value
          mem_aux_Prop idx equal x_value l_value
    | maP_Some_eq :
         (y_value : B),
        idx >=? FallbackArray.length l_value = false
        FallbackArray.get l_value idx = Some y_value
        equal x_value y_value = true
          mem_aux_Prop idx equal x_value l_value
    | maP_Some_neq :
         (y_value : B),
        idx >=? FallbackArray.length l_value = false
        FallbackArray.get l_value idx = Some y_value
        equal x_value y_value = false
        mem_aux_Prop (idx +i 1) equal x_value l_value
          mem_aux_Prop idx equal x_value l_value.

    (* if the length of an array does not exceed the upper bound of int,
       then FallbackArray.length gives the real length in result *)

    (* this fact is important for the following lemmas *)
    Fact length_of_list_length (A : Set) (l : FallbackArray.t A) :
      Z.of_nat (Datatypes.length l.(t.items)) Pervasives.max_int
      FallbackArray.length l = Z.of_nat (Datatypes.length l.(t.items)).
    Proof.
      destruct l. cbn. destruct items; trivial. simpl.
      induction items; trivial. simpl. rewrite Pos2Z.inj_succ. intros.
      rewrite IHitems; intuition.
      unfold "+i". rewrite Z.add_1_r. apply Pervasives.normalize_identity.
      intuition.
    Qed.

    (* if the length of an array is less then the upper bound of int,
       then the result of FallbackArray.length is also less then that *)

    (* this fact is obvious but also important for the following lemmas *)
    Fact stronger_length_limit (A : Set) (l : FallbackArray.t A) :
      Z.of_nat (Datatypes.length l.(t.items)) < Pervasives.max_int
      FallbackArray.length l < Pervasives.max_int.
    Proof.
      intros. rewrite length_of_list_length; intuition.
    Qed.

If inductive predicate exists then result of work of function [mem] can not be equal to false
    Lemma mem_aux_of_Prop `{FArgs} {A B : Set}
      (equal : A B bool) (x_value : A)
      (l_value : FallbackArray.t (option B))
      (idx : int) (fuel : Datatypes.nat) :
        Pervasives.Int.Valid.t idx
        let n_value := FallbackArray.length l_value in
        (Z.to_nat (n_value - idx) fuel)%nat
        mem_aux_Prop idx equal x_value l_value
          mem'_aux idx equal x_value l_value fuel = true.
    Proof.
      intros idx_valid ? le_fuel HmaP.
      revert le_fuel. revert fuel.
      induction HmaP; (destruct fuel; simpl; intro le_fuel; [intuition |]);
        [ rewrite H0, H1 | now rewrite H0, H1, H2 | rewrite H0, H1, H2 ].
      all: apply IHHmaP; [ intuition |]; unfold "+i";
           rewrite Pervasives.normalize_identity;
           [ fold n_value;
             rewrite Z.sub_add_distr, Z2Nat.inj_sub; [| intuition ];
             destruct Z.to_nat; intuition
           | rewrite Z.geb_leb in H0; apply Z.leb_gt in H0;
             unfold FallbackArray.length in *;
             pose (Compare.length_is_valid l_value.(t.items)); intuition
           ].
    Qed.

Opposite statement : if auxiliary function returned true then predicate holds and exists (inhabited)
    Lemma mem_aux_Prop_of_mem'_aux `{FArgs} {A B : Set}
      (idx : int) (equal : A B bool) (x : A) (l : FallbackArray.t (M× B))
      (fuel : Datatypes.nat) :
      mem'_aux idx equal x l fuel = true
        mem_aux_Prop idx equal x l.
    Proof.
      revert idx. induction fuel; try discriminate.
      simpl. intro.
      destruct (idx >=? FallbackArray.length l) eqn:idxGT; try discriminate.
      destruct FallbackArray.get eqn:GET; intros;
      [ destruct equal eqn:EQUAL | ].
      { apply maP_Some_eq with b; trivial. }
      { apply maP_Some_neq with b; intuition. }
      { apply maP_None; intuition. }
    Qed.

    Lemma mem_aux_Prop_exists `{FArgs} {A B : Set}
      (equal : A B bool) (x_value : A)
      (l_value : FallbackArray.t (option B)) (idx : int) (ptr : B) :
      l_value.(t.default) = None
      FallbackArray.get l_value idx = Some ptr
      equal x_value ptr = true
      0 idx < FallbackArray.length l_value
        mem_aux_Prop idx equal x_value l_value.
    Proof.
      intros. apply maP_Some_eq with ptr; intuition. cbn. rewrite Z.geb_leb.
      now apply Z.leb_gt.
    Qed.

    Lemma get_for_valid_idx {A : Set}
      (idx : int) (l_value : FallbackArray.t (option A)) (ptr : A) :
      l_value.(t.default) = None
      FallbackArray.get l_value idx = Some ptr
        0 idx < Z.of_nat (Datatypes.length l_value.(t.items)).
    Proof.
      destruct l_value. cbn. unfold FallbackArray.get. simpl. intros.
      assert (nth items idx = Some (Some ptr)) by hauto lq: on.
      rewrite H1 in H0. intuition; revert idx H1; induction items;
        try discriminate; [ hfcrush |].
      cbn in ×. rewrite Zpos_P_of_succ_nat. destruct idx; intuition.
      apply IHitems in H1. intuition.
    Qed.

We need appropriate level of generalization in order to be able to use our predicate in the proofs
    Lemma mem_aux_Prop_exists_general `{FArgs} {A B : Set}
      (equal : A B bool) (x_value : A) (ptr : B)
      (l_value : FallbackArray.t (option B)) (idx : int) (idx' : int) :
        idx < FallbackArray.length l_value
        l_value.(t.default) = None
        FallbackArray.get l_value idx = Some ptr
        equal x_value ptr = true
        0 idx' idx
          mem_aux_Prop idx' equal x_value l_value.
    Proof.
      intros. pose (Compare.length_is_valid l_value.(t.items)).
      apply mem_aux_Prop_exists with equal x_value l_value idx ptr in H1;
      trivial; try lia.
      destruct H4. revert H4.
      apply neg_le_ind with (m := idx') (n := idx); intuition.
      rewrite <- Z.sub_1_r.
      destruct (FallbackArray.get l_value (m - 1)) eqn:getValue;
      [ destruct (equal x_value b) eqn:equalValue;
        [ apply maP_Some_eq with b | apply maP_Some_neq with b ]
      | apply maP_None ]; trivial; try lia.
      all: unfold FallbackArray.length, "+i" in *;
           rewrite Pervasives.normalize_identity; rewrite Z.sub_add;
           intuition.
    Qed.

[binary_search] function for [best_skip] retrieved
    Fixpoint binary_search `{FArgs} {A B : Set}
      (cell_value : cell A B) (target_index : int)
      (powers : FallbackArray.t int) (start_idx : int) (end_idx : int)
      (fuel : Datatypes.nat) {struct fuel} : option int :=
      let pointed_cell_index (i_value : int) : int :=
        (cell_value.(cell.index) -i
        (Pervasives._mod cell_value.(cell.index)
          (FallbackArray.get powers i_value))) -i 1 in
      match fuel with
      | Datatypes.ONone
      | Datatypes.S fuel
          if Compare.Int.(Compare.S.op_gteq) start_idx end_idx then
            Some start_idx
          else
            let mid_idx := start_idx +i ((end_idx -i start_idx) /i 2) in
            let mid_cell_index := pointed_cell_index mid_idx in
            if Compare.Int.(Compare.S.op_eq) mid_cell_index target_index then
              Some mid_idx
            else
              if Compare.Int.(Compare.S.op_lt) mid_cell_index target_index then
                binary_search
                  cell_value target_index powers start_idx (mid_idx -i 1) fuel
              else
                let prev_mid_cell_index := pointed_cell_index (mid_idx +i 1) in
                if Compare.Int.(Compare.S.op_eq)
                     prev_mid_cell_index target_index
                then
                  Some (mid_idx +i 1)
                else
                  if Compare.Int.(Compare.S.op_lt)
                       prev_mid_cell_index target_index
                  then
                    Some mid_idx
                  else
                    binary_search
                     cell_value target_index powers (mid_idx +i 1) end_idx fuel
      end.

Simulation of [best_skip]
    Definition best_skip' `{FArgs} {A B : Set}
      (cell_value : cell A B) (target_index : int)
      (powers : FallbackArray.t int) (fuel : Datatypes.nat) :
      option int :=
        binary_search cell_value target_index powers 0
          ((FallbackArray.length cell_value.(cell.back_pointers)) -i 1) fuel.

Equality of initial function and simulation
    Axiom best_skip'_eq : `{FArgs} {A B : Set}
      (cell_value : cell A B) (target_index : int)
      (powers : FallbackArray.t int) (fuel : Datatypes.nat),
      (Z.to_nat (FallbackArray.length cell_value.(cell.back_pointers))
         fuel)%nat
        best_skip cell_value target_index powers =
          best_skip' cell_value target_index powers fuel.
    (* here the real lower bound for fuel
       is the logarithm of FallbackArray.length,
       but it makes no harm
       since it would always be less then the current limit *)


Values between valid integers are also valid
    Fact between_valid (i j k : int) :
      i k j
      Pervasives.Int.Valid.t i
      Pervasives.Int.Valid.t j
        Pervasives.Int.Valid.t k.
    Proof.
      intuition.
    Qed.

Validity of result of work of [best_skip'_aux] function
    Lemma binary_search_result_valid `{FArgs} {A B : Set}
      (cell_value : cell A B) (target_index start_idx end_idx res : int)
      (powers : FallbackArray.t int) (fuel : Datatypes.nat) :
      Pervasives.Int.Valid.t start_idx
      Pervasives.Int.Valid.t end_idx
      binary_search cell_value target_index powers start_idx end_idx fuel
        = Some res
        Pervasives.Int.Valid.t res.
    Proof.
      revert cell_value target_index powers start_idx end_idx res.
      induction fuel; try discriminate. cbn. intros ? ? ? ? ? ? Hstart Hend.
      step; [ congruence |].
      step.
      { intro eq_res. inversion eq_res. clear. intuition. }
      { step; [ apply IHfuel; hauto l: on use: Pervasives.int_add_valid |].
        step; [| step ].
        1-2: (intro eq_res; inversion eq_res; clear; intuition).
        apply IHfuel; hauto l: on use: Pervasives.int_add_valid.
      }
    Qed.

Validity of result of work of [best_skip'_aux] function
    Lemma best_skip_result_valid `{FArgs} {A B : Set}
      (cell_value : cell A B) (target_index res : int)
      (powers : FallbackArray.t int) :
      best_skip cell_value target_index powers = Some res
        Pervasives.Int.Valid.t res.
    Proof.
      erewrite best_skip'_eq; trivial. unfold best_skip'.
      apply binary_search_result_valid; intuition.
    Qed.

Validity of the index of a cell - our interpretation of how dereferencing operator should work
    Module Cell_Index.
      Module Valid.
        Definition t `{FArgs} {content_type ptr_type : Set}
                      (deref : ptr_type option (cell content_type ptr_type))
                      : Prop :=
                (cell_1_ptr cell_2_ptr : ptr_type)
                      (cell1 cell2 : cell content_type ptr_type),
               deref cell_1_ptr = Some cell1
               deref cell_2_ptr = Some cell2
               cell1.(cell.index) =i cell2.(cell.index) = true
               cell_1_ptr = cell_2_ptr.
      End Valid.
    End Cell_Index.

    Section Helper_section.

    Context `{FArgs} {content_type ptr_type : Set}
      (deref : ptr_type option (cell content_type ptr_type)).

If indexes of two cells are equal, then pointers to the cells equal too, so this is one and the same cell, because index of each cell in the structure is unique.
    Hypothesis index_ptr_eq : Cell_Index.Valid.t deref.

    Lemma ptr_index_eq
      (cell_1_ptr cell_2_ptr : ptr_type)
      (cell1 cell2 : cell content_type ptr_type) :
      deref cell_1_ptr = Some cell1
      deref cell_2_ptr = Some cell2
      cell_1_ptr = cell_2_ptr
        cell1.(cell.index) =i cell2.(cell.index) = true.
    Proof.
      intros deref1 deref2 cell_eq.
      rewrite cell_eq in deref1.
      rewrite deref1 in deref2.
      hauto lq: on use: Z.eqb_refl.
    Qed.

Path can not consist out of just one pointer. it should have more elements, so assumption is False
    Fixpoint aux'_contra
      (equal_ptr : ptr_type ptr_type bool)
        (cell_ptr target_ptr : ptr_type)
        (target_cell : cell content_type ptr_type) target_index
        (powers : FallbackArray.t int) (acc : list ptr_type) fuel p
        {struct fuel} :
      acc nil
        aux' deref powers target_index acc p
          (deref p) fuel = Some [cell_ptr] False.
    Proof. intro not_nil_acc.
           destruct fuel; try scongruence.
           unfold aux'. destruct (deref p); try scongruence; simpl.
           step.
           { intro H0. injection H0 as H0. rewrite rev_one in H0.
             apply rev_injective in H0. hauto l: on. }
           { step; try scongruence.
             destruct best_skip eqn:G; try scongruence; simpl.
             destruct back_pointer eqn:BP; try scongruence; simpl.
             apply aux'_contra.
             { hauto l: on. }
             { scongruence. }
             { scongruence. }
             { pose proof (nil_cons). hauto l: on. } }
    Qed.

If we have just one pointer in the path, this pointer points to the target_ cell
    Lemma one_cell_valid (equal_ptr : ptr_type ptr_type bool)
        (cell_ptr target_ptr : ptr_type) target_cell p x :
       Compare.Equal.Valid.t (fun _True) equal_ptr
       deref target_ptr = Some target_cell
       deref cell_ptr = Some x
       equal_ptr p cell_ptr = true
       let target_index := index_value target_cell in
       back_path' deref cell_ptr target_index = Some [p]
       (equal_ptr target_ptr cell_ptr
          && (index_value x =i index_value target_cell))%bool = true.
    Proof. intros.
           unfold Compare.Equal.Valid.t in H0.
           apply H0 in H3. 2, 3 : apply I. subst.
           match goal with
           | |- (?x && _)%bool = trueassert (G : x = true)
           end.
           { revert H4. unfold back_path'. rewrite H2. simpl.
             destruct bp_compute_fuel; [sfirstorder|].
             simpl. step.
             { intros. clear H4. apply H0; try apply I.
               apply (index_ptr_eq
                        target_ptr cell_ptr target_cell x H1 H2 Heqb). }
             { intros. apply H0; try apply I.
               revert H4.
               step; try scongruence.
               destruct best_skip eqn:Best; try scongruence; simpl.
               destruct back_pointer eqn:N; try scongruence; simpl.
               match goal with
               | |- aux' _ _ _ ?acc _ _ _ = _ _
                 intros; assert (G : acc nil) by hfcrush
               end.
               revert H4. unfold target_index.
               match goal with
               | |- context[aux' _ ?pow (?iv ?tc) ?acc ?p' _ ?n'] ⇒
                 match goal with
                 | |- _ ?tp = ?cp
                   pose proof (aux'_contra equal_ptr cp tp tc (iv tc)
                                 pow acc n' p') G
                 end
               end.
               hauto q: on.
             }
           }
           match goal with
           | |- (_ && ?x)%bool = trueassert (G2 : x = true)
           end.
           { revert H4. unfold back_path'. apply H0 in G; trivial.
             intro aux. eapply ptr_index_eq.
             { apply H2. }
             { apply H1. }
             { scongruence. }
           }
           hauto lq: on.
    Qed.

If path was generated by [back_path'] - all elements are (Some ..) generalized version
    Lemma all_elements_not_none_general
      (cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
      (powers : FallbackArray.t int) (fuel : Datatypes.nat) (p_any : ptr_type)
      path init_path :
        let target_index := index_value target_cell in
        aux'' fuel deref powers target_index init_path cell_ptr = Some path
        ( p, In p init_path deref p = None False)
        In p_any path
          deref p_any = None False.
    Proof.
      intros.
      revert H0 H1.
      revert init_path cell_ptr.
      induction fuel; [ discriminate |].
      intros ? ?.
      simpl in ×.
      destruct (deref cell_ptr) eqn:DC; [| discriminate ].
      simpl in ×. step.
      { qauto l: on use: list_rev_cons, list_rev_In, List.in_app_iff. }
      { step; try discriminate.
        destruct best_skip; [| discriminate ]. simpl in ×.
        destruct back_pointer; [| discriminate ].
        hauto q: on.
      }
    Qed.

If path was generated by [back_path'] - all elements are (Some ..)
    Lemma all_elements_not_none
      (cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
      (powers : FallbackArray.t int) (fuel : Datatypes.nat) (p_any : ptr_type)
      (path : list ptr_type) :
        let target_index := index_value target_cell in
        aux'' fuel deref powers target_index nil cell_ptr = Some path
        In p_any path
          deref p_any = None False.
    Proof.
      hauto l: on use: all_elements_not_none_general.
    Qed.

Generalized version of headers equality
    Lemma aux'_head_equal_general
      (cell_ptr : ptr_type) (cell : M× cell content_type ptr_type)
      (target_index : int) (powers : FallbackArray.t int)
      (equal_ptr : ptr_type ptr_type bool) (p : ptr_type)
      (l acc : list ptr_type) (fuel : nat) :
        Compare.Equal.Valid.t (fun _ : ptr_typeTrue) equal_ptr
        aux' deref powers target_index acc cell_ptr cell fuel =
          Some (rev acc ++ p :: l)%list
          p = cell_ptr.
    Proof.
      intro Hequal.
      match goal with
      | |- aux' ?der ?pow ?ti ?acc ?cp ?cell ?fuel = _ _
        pose proof (Ha'ns := aux'_nonempty_success der pow cp acc ti cell fuel)
      end.
      intro Haux.
      destruct Ha'ns; eauto. rewrite Haux in H0.
      hauto lq: on use: List.app_inv_head.
    Qed.

Generalized version of headers equality. Boolean
    Lemma aux'_head_true_general
      (cell_ptr : ptr_type) (cell : M× cell content_type ptr_type)
      (target_index : int) (powers : FallbackArray.t int)
      (equal_ptr : ptr_type ptr_type bool) (p : ptr_type)
      (l acc : list ptr_type) (fuel : Datatypes.nat) :
      Compare.Equal.Valid.t (fun _True) equal_ptr
      aux' deref powers target_index acc cell_ptr cell fuel =
        Some (rev acc ++ p :: l)%list
      equal_ptr p cell_ptr = true.
    Proof.
      intro Hequal.
      match goal with
      | |- aux' ?der ?pow ?ti ?acc ?cp ?cell ?fuel = _ _
        intro Haux;
        destruct (aux'_nonempty_success der pow cp acc ti cell fuel); eauto
      end.
      rewrite Haux in H0.
      unfold Compare.Equal.Valid.t in Hequal.
      hauto lq: on use: List.app_inv_head.
    Qed.

Result of work of [mem] function equals true
    Lemma member_true'
      (equal_ptr : ptr_type ptr_type bool)
      (cell_ptr : ptr_type) (target_cell : cell content_type ptr_type)
      (powers : FallbackArray.t int) (path init_path : list ptr_type)
      (fuel : Datatypes.nat) (p p0 : ptr_type)
      (x : cell content_type ptr_type) :
        let target_index := index_value target_cell in
        aux'' fuel deref powers target_index init_path cell_ptr =
          Some (rev init_path ++ p :: p0 :: path)%list
        Compare.Equal.Valid.t (fun _True) equal_ptr
        deref cell_ptr = Some x
         (idx : int) (ptr : ptr_type),
          FallbackArray.get x.(cell.back_pointers) idx = Some ptr
          equal_ptr p0 ptr = true
          Pervasives.Int.Valid.t idx.
    Proof.
      intro. rewrite aux''_eq_aux'. intros.
      assert (cell_ptr = p)
      by now apply aux'_head_equal_general
         with (equal_ptr := equal_ptr) in H0.
      revert H0. revert init_path.
      induction fuel; try discriminate.
      intros. simpl in ×.
      destruct deref; try discriminate.
      simpl in ×. inversion H2. rewrite H5 in ×. revert H0. step.
      { rewrite list_rev_cons. hauto q: on use: List.app_inv_head. }
      { step; try discriminate.
        destruct best_skip eqn:BSkip; try discriminate.
        simpl in ×. apply best_skip_result_valid in BSkip.
        destruct back_pointer eqn:BP; try discriminate.
        hecrush use: aux'_head_true_general,
          (List.rev_head_app_eq init_path (p0 :: path) p).
      }
    Qed.

Result of work of [mem] function equals true, auxiliary statement
    Lemma member_true'' (equal_ptr : ptr_type ptr_type bool)
      (cell_ptr : ptr_type) (powers : FallbackArray.t int)
      (target_cell : cell content_type ptr_type)
      (path init_path : list ptr_type) (fuel : Datatypes.nat) (p p0 : ptr_type)
      (x : cell content_type ptr_type) :
        let target_index := index_value target_cell in
        aux'' fuel deref powers target_index init_path cell_ptr =
          Some (rev init_path ++ p :: p0 :: path)%list
        Compare.Equal.Valid.t (fun _True) equal_ptr
        deref cell_ptr = Some x
        x.(cell.back_pointers).(t.default) = None
         (idx : int) (ptr : ptr_type),
          FallbackArray.get x.(cell.back_pointers) idx = Some ptr
          equal_ptr p0 ptr = true 0 idx.
    Proof.
      intros.
      destruct (
        member_true'
          equal_ptr cell_ptr target_cell powers path init_path fuel p p0 x
      ); trivial.
      destruct H4, H4.
      apply get_for_valid_idx in H4 as H4'; hauto lq: on rew: off.
    Qed.

This lemma requires that an array it uses was shorter than [max_int], due to the integer overflows in [mem]
    Lemma member_true_general (equal_ptr : ptr_type ptr_type bool)
      (cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
      (target_cell : cell content_type ptr_type) (path acc : list ptr_type)
      (fuel fuel' : Datatypes.nat) (p p0 : ptr_type)
      (x : cell content_type ptr_type) :
      let target_index := index_value target_cell in
      aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel
        = Some (rev acc ++ p :: p0 :: path)%list
      Compare.Equal.Valid.t (fun _True) equal_ptr
      deref cell_ptr = Some x
      Cell.Valid.t x
      Z.of_nat (Datatypes.length x.(cell.back_pointers).(t.items))
        < Pervasives.max_int
      let n_value := FallbackArray.length x.(cell.back_pointers) in
      ((Z.to_nat n_value) fuel')%nat
      mem' equal_ptr p0 x.(cell.back_pointers) fuel' = true.
    Proof.
      unfold mem'. rewrite <- aux''_eq_aux'. intros. destruct H3.
      apply mem_aux_of_Prop; try hfcrush use: stronger_length_limit. revert H0.
      match goal with
      | |- context[aux'' ?fuel ?der ?pow (?iv ?tc) ?acc ?cp =
                     Some (_ ++ ?p' :: ?p'' :: ?path)%list] ⇒
        pose (member_true'' equal_ptr cp pow tc path acc fuel p' p'' x)
      end.
      pose stronger_length_limit. intro. destruct e; intuition. destruct H3.
      apply mem_aux_Prop_exists_general with x1 x0; try hfcrush.
      destruct H3. apply get_for_valid_idx in H3; intuition.
      rewrite length_of_list_length; intuition.
    Qed.

This lemma requires that an array it uses was shorter than [max_int], due to the integer overflows in [mem]
    Lemma member_true (equal_ptr : ptr_type ptr_type bool)
      (cell_ptr target_ptr : ptr_type)
      (target_cell : cell content_type ptr_type) (path : list ptr_type)
      (fuel' : Datatypes.nat) (p p0 : ptr_type)
      (x : cell content_type ptr_type) :
      let target_index := index_value target_cell in
      back_path' deref cell_ptr target_index = Some (p :: p0 :: path)
      Compare.Equal.Valid.t (fun _True) equal_ptr
      deref cell_ptr = Some x
      Cell.Valid.t x
      Z.of_nat (Datatypes.length x.(cell.back_pointers).(t.items))
        < Pervasives.max_int
      let n_value := FallbackArray.length x.(cell.back_pointers) in
      ((Z.to_nat n_value) fuel')%nat
      mem' equal_ptr p0 x.(cell.back_pointers) fuel' = true.
    Proof.
      unfold back_path'. destruct deref eqn:D; simpl; [| discriminate ].
      hauto l: on use: member_true_general.
    Qed.

Lemma states that auxiliary function [best_skip'] could not return [None] result
    Lemma best_skip'_always_some
      (cell_ptr p p0 : ptr_type) (target_cell x : cell content_type ptr_type)
      (powers : FallbackArray.t int) (l acc : list ptr_type)
      (fuel fuel' : Datatypes.nat) :
      let target_index := index_value target_cell in
      aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel =
           Some (rev acc ++ p :: p0 :: l)%list
      deref cell_ptr = Some x
      (Z.to_nat (FallbackArray.length x.(cell.back_pointers)) fuel')%nat
      best_skip' x (index_value target_cell) powers fuel' = None False.
    Proof.
      destruct fuel; try discriminate.
      intros. simpl in ×. rewrite H1 in H0. simpl in H0. revert H0. step.
      { intro. inversion H0.
        rewrite <- List.app_nil_r with (l := rev (cell_ptr :: acc)) in H5.
        rewrite List.rev_head_app_eq in H5. apply app_inv_head in H5.
        inversion H5.
      }
      { step; try discriminate. intro.
        rewrite best_skip'_eq with (fuel0 := fuel') in H0; trivial.
        unfold target_index in H0. rewrite H3 in H0. discriminate.
      }
    Qed.

Lemma states that auxiliary function [FallbackArray.get] could not return [None] result : generalized version
    Lemma get_always_some_general
      (cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
      (target_cell x : cell content_type ptr_type)
      (fuel : Datatypes.nat) (i start_idx end_idx : int) :
      let target_index := index_value target_cell in
      0 start_idx
      start_idx end_idx
      end_idx < FallbackArray.length x.(cell.back_pointers)
      deref cell_ptr = Some x
      Cell.Valid.t x
      binary_search x target_index powers start_idx end_idx fuel = Some i
       best_ptr, (FallbackArray.get x.(cell.back_pointers) i) =
        Some best_ptr.
    Proof.
      (* @TODO *)
    Admitted.

Lemma states that auxiliary function [get] could not return [None] result
    Lemma get_always_some
      (cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
      (target_cell x : cell content_type ptr_type) (fuel : Datatypes.nat)
      (i : int) :
      let target_index := index_value target_cell in
      deref cell_ptr = Some x
      Cell.Valid.t x
      binary_search x target_index powers 0
        ((FallbackArray.length x.(cell.back_pointers)) -i 1) fuel =
        Some i
       best_ptr, (FallbackArray.get x.(cell.back_pointers) i) =
        Some best_ptr.
    Proof.
      (* @TODO *)
    Admitted.

Lemma states that auxiliary function [back_pointer] could not return [None] result
    Lemma back_pointer_always_some
      (cell_ptr target_ptr : ptr_type) (powers : FallbackArray.t int)
      (target_cell x : cell content_type ptr_type)
      (fuel : Datatypes.nat) (i : int) :
      let target_index := index_value target_cell in
      deref cell_ptr = Some x
      Cell.Valid.t x
      best_skip' x (index_value target_cell) powers fuel = Some i
       best_ptr, (back_pointer x i) = Some best_ptr.
    Proof.
      unfold best_skip', back_pointer. now apply get_always_some.
    Qed.

Lemma shows equality of pointers in certain conditions
    Fixpoint best_ptr_eq
      (equal_ptr : ptr_type ptr_type bool) (powers : FallbackArray.t int)
      (cell_ptr target_ptr p p0 best_ptr : ptr_type)
      (target_cell x c : cell content_type ptr_type) (l acc : list ptr_type)
      (fuel fuel' : Datatypes.nat) (i : int) {struct fuel} :
      let target_index := index_value target_cell in
      aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel =
           Some (rev acc ++ p :: p0 :: l)%list
      Compare.Equal.Valid.t (fun _True) equal_ptr
      deref target_ptr = Some target_cell
      deref cell_ptr = Some x
      equal_ptr p cell_ptr = true
      (Z.to_nat (FallbackArray.length x.(cell.back_pointers)) fuel')%nat
      best_skip' x target_index powers fuel' = Some i
      deref p0 = Some c
      back_pointer x i = Some best_ptr
      equal_ptr best_ptr p0 = true.
    Proof.
           destruct fuel, fuel'; try discriminate.
           intros; simpl in ×. revert H0. rewrite H3. simpl. step.
      { intro. inversion H0.
        rewrite <- List.app_nil_r with (l := rev (cell_ptr :: acc)) in H10.
        rewrite List.rev_head_app_eq in H10. apply app_inv_head in H10.
        inversion H10.
      }
      { step; try discriminate.
        rewrite best_skip'_eq with (fuel0 := Datatypes.S fuel'); trivial.
        rewrite H6. simpl.
        rewrite H8. simpl.
        apply H1 in H4. 2, 3 : apply I.
        rewrite H4.
        assert (T
          : (rev acc ++ cell_ptr :: p0 :: l
             = rev (cell_ptr :: acc) ++ p0 :: l)%list) by
        (symmetry; apply List.rev_head_app_eq). rewrite T.
        clear T. intro.
        pose proof (aux'_head_true_general best_ptr (deref best_ptr)
                      target_index powers equal_ptr p0 l (cell_ptr :: acc) fuel H1
                      H0).
        apply H1 in H9; trivial. now apply H1. }
    Qed.

    (* We do one step reduction inside path-building.
       We will need this statement in the main proof *)

    Lemma one_step
      (equal_ptr : ptr_type ptr_type bool)
      (cell_ptr target_ptr p p0 : ptr_type) (powers : FallbackArray.t int)
      (target_cell x c : cell content_type ptr_type)
      (l acc : list ptr_type) (fuel : Datatypes.nat) (i : int) :
      let target_index := index_value target_cell in
      deref p = Some x
      best_skip x (index_value target_cell) powers = Some i
      mem equal_ptr p0 x.(cell.back_pointers) = true
      deref p0 = Some c
      back_pointer x i = Some p0
      aux' deref powers target_index acc p (deref p) fuel =
           Some (rev acc ++ p :: p0 :: l)%list
      aux' deref powers (index_value target_cell) (p :: acc) p0 (deref p0)
        (Datatypes.S fuel) = Some (rev (p :: acc) ++ p0 :: l)%list.
    Proof.
      intros.
      unfold aux' in H5. destruct fuel. inversion H5. revert H5.
      rewrite H0. simpl. step.
      { intro. injection H5 as H5.
        assert (B1 : rev (p :: acc)%list = (rev (p :: acc) ++ [])%list)
          by scongruence use: app_nil_r. rewrite B1 in H5.
        rewrite List.rev_head_app_eq in H5. apply List.app_inv_head_iff in H5.
        scongruence.
      }
      { step.
        { intro. inversion H5. }
        { assert (H6 : target_index = index_value target_cell) by scongruence.
          rewrite <- H6 in H1. rewrite H1. simpl. rewrite H4. simpl.
          assert (T : (rev acc ++ p :: p0 :: l = rev (p :: acc) ++ p0 :: l)%list)
            by (symmetry; apply List.rev_head_app_eq).
          rewrite T. intro. apply (aux'_sufficient_fuel _ _ _ _ _ _ fuel
                                     (Datatypes.S (Datatypes.S fuel))).
          apply H5. hauto l: on.
        }
      }
    Qed.

Lemma states that last index of the path equals to [target_index]
    Lemma aux''_last_index_is_target
      (cell_ptr ptr : ptr_type) (target_cell : cell content_type ptr_type)
      (powers : FallbackArray.t int) (path path' : list ptr_type)
      (fuel : Datatypes.nat) :
      let target_index := index_value target_cell in
      aux'' fuel deref powers target_index path' cell_ptr
        = Some (path ++ [ptr])%list
       c, deref ptr = Some c
      target_index =i index_value c = true.
    Proof.
      intros.
      revert path' cell_ptr H0.
      induction fuel; try discriminate.
      intros ? ?. simpl. destruct (deref cell_ptr) eqn:H'; try discriminate.
      simpl. step.
      { qauto l: on use: app_inj_tail, list_rev_cons, index_ptr_eq. }
      { step; try discriminate.
        destruct best_skip; try discriminate. simpl.
        destruct back_pointer; try discriminate. simpl.
        intro. now apply IHfuel in H0.
      }
    Qed.

Lemma states that last index of the path equals to [target_index]
    Lemma aux''_last_is_target
      (cell_ptr target_ptr ptr : ptr_type) (powers : FallbackArray.t int)
      (target_cell : cell content_type ptr_type) (path path' : list ptr_type)
      (fuel : Datatypes.nat) :
      deref target_ptr = Some target_cell
      let target_index := index_value target_cell in
      aux'' fuel deref powers target_index path' cell_ptr
        = Some (path ++ [ptr])%list
      target_ptr = ptr.
    Proof.
      hauto l: on use: aux''_last_index_is_target.
    Qed.

Lemma states that last index of the path equals to [target_index] boolean version
    Lemma aux''_last_is_target_bool
      (equal_ptr : ptr_type ptr_type bool)
      (cell_ptr target_ptr ptr : ptr_type) (powers : FallbackArray.t int)
      (target_cell : cell content_type ptr_type) (path path' : list ptr_type)
      (fuel : Datatypes.nat) :
      Compare.Equal.Valid.t (fun _True) equal_ptr
      deref target_ptr = Some target_cell
      let target_index := index_value target_cell in
      aux'' fuel deref powers target_index path' cell_ptr
        = Some (path ++ [ptr])%list
      equal_ptr target_ptr ptr = true.
    Proof.
      unfold Compare.Equal.Valid.t. hauto l: on use: aux''_last_is_target.
    Qed.

Heart of the proof - we prove by induction that function [valid_path'] will return true if path was byilt by [back_path].
    Lemma back_path'_valid_path'
      (equal_ptr : ptr_type ptr_type bool)
      (cell_ptr target_ptr p : ptr_type) (powers : FallbackArray.t int)
      (target_cell x : cell content_type ptr_type) (path acc : list ptr_type)
      (fuel : Datatypes.nat)
      (path_valid : p x,
                      In p path deref p = Some x Cell.Valid.t x) :
      ( cptr cval,
         In cptr (rev acc ++ p :: path)%list
         deref cptr = Some cval
           Z.of_nat (Datatypes.length cval.(cell.back_pointers).(t.items))
           < Pervasives.max_int)
      let target_index := index_value target_cell in
      aux' deref powers target_index acc cell_ptr (deref cell_ptr) fuel
        = Some (rev acc ++ p :: path)%list
      ( p1 : ptr_type, In p1 acc deref p1 = None False)
      Compare.Equal.Valid.t (fun _True) equal_ptr
      Cell.Valid.t x
      deref target_ptr = Some target_cell
      deref cell_ptr = Some x
      p = cell_ptr
      valid_path' equal_ptr target_ptr target_cell deref powers (index_value x)
        cell_ptr path = true.
    Proof.
      revert equal_ptr cell_ptr target_ptr target_cell acc fuel p x path_valid.
      induction path as [|p0 l]; intros; unfold valid_path'.
      { rewrite <- aux''_eq_aux' in H1. rewrite H7 in ×.
        apply aux''_last_is_target_bool
          with (equal_ptr := equal_ptr) (target_ptr := target_ptr)
          in H1 as H1';
        trivial.
        apply aux''_last_index_is_target in H1. destruct H1. rewrite H6 in ×.
        destruct H1. inversion H1. rewrite H10 in ×. rewrite H1'. cbn in ×.
        now rewrite Z.eqb_sym.
      }
      { rewrite H6; simpl. destruct (deref p0) eqn:DP0; simpl;
        [| rewrite <- aux''_eq_aux' in H1;
           apply all_elements_not_none_general with (p_any := p0) in H1;
           intuition ].
        assert ((mem equal_ptr p0 x.(cell.back_pointers)) = true).
        { rewrite mem_eq
            with (fuel0 :=
                    Z.to_nat (FallbackArray.length x.(cell.back_pointers)));
          [| intuition ].
          apply member_true_general
            with cell_ptr powers target_cell l acc fuel p;
          trivial.
          apply H0 with cell_ptr; trivial.
          rewrite <- aux''_eq_aux' in H1.
          destruct (aux''_nonempty_success
                      deref powers cell_ptr acc target_index fuel).
          { hauto l: on. }
          { rewrite H8 in H1. inversion H1. apply List.app_inv_head in H10.
            intuition.
          }
        }
        { rewrite H8. rewrite Bool.andb_true_l.
          rewrite best_skip'_eq
            with (fuel0 :=
                    (Z.to_nat (FallbackArray.length x.(cell.back_pointers))));
          [| intuition ].
          pose proof (
            best_skip'_always_some
              cell_ptr p p0 target_cell x powers l acc fuel
              (Z.to_nat (FallbackArray.length x.(cell.back_pointers))) H1 H6).
          destruct (best_skip' x (index_value target_cell)) eqn:Best_skip;
            [simpl|hauto lq: on rew: off].
          destruct (back_pointer x i) eqn:Back_P;
            [ simpl
            | pose proof (
                back_pointer_always_some cell_ptr target_ptr powers target_cell
                  x (Z.to_nat (FallbackArray.length x.(cell.back_pointers)))
                  i H6 H4 Best_skip); destruct H10; scongruence].
          assert (equal_ptr p1 p0 = true).
          { assert (EP : equal_ptr p cell_ptr = true)
              by (apply H3; hauto l: on).
            apply (best_ptr_eq equal_ptr powers cell_ptr target_ptr p p0 p1
                     target_cell x c l acc fuel
                     (Z.to_nat (FallbackArray.length x.(cell.back_pointers)))
                     i H1 H3 H5 H6 EP
                     (Nat.le_refl
                      (Z.to_nat (FallbackArray.length x.(cell.back_pointers))))
                     Best_skip DP0 Back_P).
          }
          { rewrite H10. rewrite Bool.andb_true_l.
            assert (T : (deref p = Some x)) by scongruence.
            assert (p0 = p1) by (apply H3 in H10; hauto l: on).
            assert (T1 : (back_pointer x i = Some p0)) by scongruence.
            assert (equal_ptr p0 p0 = true) by scongruence.
            assert (PR : aux' deref powers (index_value target_cell) (p :: acc)
                           p0 (deref p0) (Datatypes.S (Datatypes.S fuel)) =
                           Some (rev (p :: acc) ++ p0 :: l)%list).
            { (* Proving PR with one_step *)
              assert (U2: back_pointer x i = Some p0) by scongruence.
              pose Best_skip as B_skip.
              rewrite <- best_skip'_eq in B_skip; [| intuition ].
              apply (one_step equal_ptr cell_ptr target_ptr p p0 powers
                       target_cell x c l acc (Datatypes.S fuel) i T
                       B_skip H8 DP0 U2).
              assert (Y : (index_value target_cell) = target_index)
                by scongruence.
              rewrite Y. rewrite H7 in ×. rewrite <- H11 in ×.
              apply (aux'_sufficient_fuel _ _ _ _ _ _ _ (Datatypes.S fuel))
                in H1;
              [ apply H1 | hauto l: on ].
            }
            { fold (valid_path'
                      equal_ptr target_ptr target_cell
                      deref powers c.(cell.index) p0 l). fold (index_value c).
              assert ( (p : ptr_type) (x : cell content_type ptr_type),
                        In p l deref p = Some x Cell.Valid.t x) by
                (intros; apply path_valid with p2; intuition).
              rewrite <- List.rev_head_app_eq in H0.
              apply (IHl equal_ptr p0 target_ptr target_cell (p :: acc)%list _
                       p0 c H13 H0 PR); trivial.
              { cbn. intros. destruct H14.
                { rewrite <- H14 in H15. rewrite H15 in T. discriminate. }
                { intuition. }
              }
              { apply path_valid with p0; intuition. }
            }
          }
        }
      }
    Qed.

    End Helper_section.

  End Helper_valid.

Main lemma [back_path_is_valid]
  Lemma back_path_is_valid `{FArgs} {content_type ptr_type : Set}
    (equal_ptr : ptr_type ptr_type bool)
    (cell_ptr target_ptr : ptr_type)
    (target_cell : cell content_type ptr_type) (path : list ptr_type)
    (deref : ptr_type option (cell content_type ptr_type)) (fuel : nat)
    (cell_index_spec : Helper_valid.Cell_Index.Valid.t deref)
    (path_valid : p x,
                    In p path deref p = Some x Cell.Valid.t x)
    (array_len_valid :
        cptr cval,
         In cptr path
         deref cptr = Some cval
           Z.of_nat (Datatypes.length cval.(cell.back_pointers).(t.items))
           < Pervasives.max_int) :
    Compare.Equal.Valid.t (fun _True) equal_ptr
    deref target_ptr = Some target_cell
    let target_index := index_value target_cell in
    back_path deref cell_ptr target_index = Some path
    valid_back_path equal_ptr deref cell_ptr target_ptr path = true.
  Proof.
    intros. rewrite (back_path_eq deref cell_ptr target_index) in H2.
    unfold valid_back_path. rewrite H1. simpl.
    remember H2 as H3; clear HeqH3. apply back_path'_cell_not_none in H2.
    destruct H2; rewrite H2; simpl. remember H3 as H4; clear HeqH4.
    pose proof (back_path'_not_nil deref cell_ptr target_index path).
    assert (G : path []) by scongruence. destruct path; try scongruence.
    remember H3 as H6; clear HeqH6. apply back_path'_equal_Prop_head
      in H6. rewrite H6. apply Bool.andb_true_iff.
    split; try apply H0; trivial.
    rewrite valid_path_eq. unfold back_path' in H3.
    assert (W : aux' deref (list_powers x) target_index nil cell_ptr
                  (deref cell_ptr)
                  (bp_compute_fuel deref (list_powers x) cell_ptr
                     target_index) =
                  Some (rev nil ++ p :: path)%list)
      by (revert H4; hauto lq: on).
    apply Helper_valid.back_path'_valid_path'
      with p nil (bp_compute_fuel deref (list_powers x) cell_ptr target_index);
    hauto lq: on.
  Qed.

Proof of [back_path_is_uniq] starts here

  Fixpoint back_path_is_uniq `{FArgs} {content_type ptr_type : Set} equal_ptr
    cell_ptr target_ptr target_cell path
    (deref : ptr_type option (cell content_type ptr_type)) {struct path}:
    Compare.Equal.Valid.t (fun _True) equal_ptr
    deref target_ptr = Some target_cell
    let target_index := index_value target_cell in
    valid_back_path equal_ptr deref cell_ptr target_ptr path = true
    back_path deref cell_ptr target_index = Some path.
  Proof.
    (* @TODO: prove in Proto_J first *)
  Admitted.
End Make.