Skip to main content

🔗 Skip_list_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.

Module S.
  Record signature {cell : Set Set Set} : Set := {
    cell := cell;
    equal :
       {content ptr : Set},
      (content content bool) (ptr ptr bool)
      cell content ptr cell content ptr bool;
    encoding :
       {content ptr : Set},
      Data_encoding.t ptr Data_encoding.t content
      Data_encoding.t (cell content ptr);
    index_value : {content ptr : Set}, cell content ptr int;
    content : {content ptr : Set}, cell content ptr content;
    back_pointer :
       {content ptr : Set}, cell content ptr int option ptr;
    back_pointers : {content ptr : Set}, cell content ptr list ptr;
    genesis : {content ptr : Set}, content cell content ptr;
    next :
       {content ptr : Set},
      cell content ptr ptr content cell content ptr;
    back_path :
       {content ptr : Set},
      (ptr option (cell content ptr)) ptr int option (list ptr);
    valid_back_path :
       {content ptr : Set},
      (ptr ptr bool) (ptr option (cell content ptr)) ptr
      ptr list ptr bool;
  }.
End S.
Definition S := @S.signature.
Arguments S {_}.

Module S_Parameters.
  Record signature : Set := {
    basis : int;
  }.
End S_Parameters.
Definition S_Parameters := S_Parameters.signature.

Module Make.
  Class FArgs := {
    Parameters : S_Parameters;
  }.

Init function; without side-effects in Coq
  Definition init_module_repr `{FArgs} : unit :=
    (* ❌ Assert instruction is not handled. *)
    assert unit (Parameters.(S_Parameters.basis) i 2).

  Module cell.
    Record record `{FArgs} {content ptr : Set} : Set := Build {
      content : content;
      back_pointers : FallbackArray.t (option ptr);
      index : int;
    }.
    Arguments record {_}.
    Definition with_content `{FArgs} {t_content t_ptr} content
      (r : record t_content t_ptr) :=
      Build _ t_content t_ptr content r.(back_pointers) r.(index).
    Definition with_back_pointers `{FArgs} {t_content t_ptr} back_pointers
      (r : record t_content t_ptr) :=
      Build _ t_content t_ptr r.(content) back_pointers r.(index).
    Definition with_index `{FArgs} {t_content t_ptr} index
      (r : record t_content t_ptr) :=
      Build _ t_content t_ptr r.(content) r.(back_pointers) index.
  End cell.
  Definition cell `{FArgs} := cell.record.

  Definition equal `{FArgs} {A B C : Set}
    (equal_content : A B bool) (equal_ptr : C C bool)
    (cell1 : cell A C) (cell2 : cell B C) : bool :=
    let equal_back_pointers
      (b1 : FallbackArray.t (option C)) (b2 : FallbackArray.t (option C))
      : 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 C) ⇒
              ((equal &&
              (Option.equal equal_ptr h1 (FallbackArray.get b2 i_value))),
                (i_value +i 1))) b1 (true, 0))) in
    let '{|
      cell.content := content;
        cell.back_pointers := back_pointers;
        cell.index := index_value
        |} := cell1 in
    (equal_content content cell2.(cell.content)) &&
    ((equal_back_pointers back_pointers cell2.(cell.back_pointers)) &&
    (Compare.Int.equal index_value cell2.(cell.index))).

  Definition index_value `{FArgs} {A B : Set} (cell_value : cell A B) : int :=
    cell_value.(cell.index).

  Definition back_pointers_to_list `{FArgs} {A : Set}
    (a_value : FallbackArray.t (option A)) : list A :=
    List.rev
      (FallbackArray.fold
        (fun (l_value : list A) ⇒
          fun (function_parameter : option A) ⇒
            match function_parameter with
            | Some ptrcons ptr l_value
            | None
              (* ❌ Assert instruction is not handled. *)
              assert (list _) false
            end) a_value nil).

  Definition encoding `{FArgs} {A B : Set}
    (ptr_encoding : Data_encoding.encoding A)
    (content_encoding : Data_encoding.encoding B)
    : Data_encoding.encoding (cell B A) :=
    let of_list :=
      FallbackArray.of_list None (fun (c_value : A) ⇒ Some c_value) in
    let to_list {C : Set} : FallbackArray.t (option C) list C :=
      back_pointers_to_list in
    Data_encoding.conv
      (fun (function_parameter : cell B A) ⇒
        let '{|
          cell.content := content;
            cell.back_pointers := back_pointers;
            cell.index := index_value
            |} := function_parameter in
        (index_value, content, (to_list back_pointers)))
      (fun (function_parameter : int × B × list A) ⇒
        let '(index_value, content, back_pointers) := function_parameter in
        {| cell.content := content; cell.back_pointers := of_list back_pointers;
          cell.index := index_value; |}) None
      (Data_encoding.obj3
        (Data_encoding.req None None "index" Data_encoding.int31)
        (Data_encoding.req None None "content" content_encoding)
        (Data_encoding.req None None "back_pointers"
          (Data_encoding.list_value None ptr_encoding))).

  Definition content `{FArgs} {A B : Set} (cell_value : cell A B) : A :=
    cell_value.(cell.content).

  Definition back_pointers `{FArgs} {A B : Set} (cell_value : cell A B)
    : list B := back_pointers_to_list cell_value.(cell.back_pointers).

  Definition genesis `{FArgs} {A B : Set} (content : A) : cell A B :=
    {| cell.content := content; cell.back_pointers := FallbackArray.make 0 None;
      cell.index := 0; |}.

  Definition back_pointer `{FArgs} {A B : Set}
    (cell_value : cell A B) (i_value : int) : option B :=
    FallbackArray.get cell_value.(cell.back_pointers) i_value.

  Definition back_pointer_unsafe `{FArgs} {A B : Set}
    (cell_value : cell A B) (i_value : int) : B :=
    match FallbackArray.get cell_value.(cell.back_pointers) i_value with
    | Some ptrptr
    | None
      (* ❌ Assert instruction is not handled. *)
      assert _ false
    end.

  #[bypass_check(guard)]
  Definition next `{FArgs} {A B C : Set}
    (prev_cell : cell A B) (prev_cell_ptr : B) (content : C) : cell C B :=
    let index_value := prev_cell.(cell.index) +i 1 in
    let back_pointers :=
      let fix aux (power : int) (accu_value : list B) (i_value : int)
        {struct power} : list B :=
        if index_value <i power then
          List.rev accu_value
        else
          let back_pointer_i :=
            if (Pervasives._mod index_value power) =i 0 then
              prev_cell_ptr
            else
              back_pointer_unsafe prev_cell i_value in
          let accu_value := cons back_pointer_i accu_value in
          aux (power ×i Parameters.(S_Parameters.basis)) accu_value
            (i_value +i 1) in
      aux 1 nil 0 in
    let back_pointers :=
      FallbackArray.of_list None (fun (x_value : B) ⇒ Some x_value)
        back_pointers in
    {| cell.content := content; cell.back_pointers := back_pointers;
      cell.index := index_value; |}.

  #[bypass_check(guard)]
  Definition best_skip `{FArgs} {A B : Set}
    (cell_value : cell A B) (target_index : int) : option int :=
    let index_value := cell_value.(cell.index) in
    let fix aux
      (idx : int) (pow : int) (best_idx : option int) (best_skip : option int)
      {struct idx} : option int :=
      if idx i (FallbackArray.length cell_value.(cell.back_pointers)) then
        best_idx
      else
        let idx_index := (index_value -i (Pervasives._mod index_value pow)) -i 1
          in
        let skip := index_value -i idx_index in
        if
          (idx_index <i target_index) ||
          (Option.equal Compare.Int.equal (Some skip) best_skip)
        then
          best_idx
        else
          aux (idx +i 1) (Parameters.(S_Parameters.basis) ×i pow) (Some idx)
            (Some skip) in
    aux 0 1 None None.

  #[bypass_check(guard)]
  Definition back_path `{FArgs} {A B : Set}
    (deref : A option (cell B A)) (cell_ptr : A) (target_index : int)
    : option (list A) :=
    let fix aux (path : list A) (ptr : A) {struct ptr} : option (list A) :=
      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 target_index =i index_value then
            Some (List.rev path)
          else
            if target_index >i index_value then
              None
            else
              Option.bind (best_skip cell_value target_index)
                (fun (best_idx : int) ⇒
                  Option.bind (back_pointer cell_value best_idx)
                    (fun (ptr : A) ⇒ aux path ptr))) in
    aux nil cell_ptr.

  #[bypass_check(guard)]
  Definition mem `{FArgs} {A B : Set}
    (equal : A B bool) (x_value : A)
    (l_value : FallbackArray.t (option B)) : bool :=
    let n_value := FallbackArray.length l_value in
    let fix aux (idx : int) {struct idx} : bool :=
      if idx i n_value then
        false
      else
        match FallbackArray.get l_value idx with
        | Noneaux (idx +i 1)
        | Some y_value
          if equal x_value y_value then
            true
          else
            aux (idx +i 1)
        end in
    aux 0.

  Definition assume_some `{FArgs} {A : Set}
    (o_value : option A) (f_value : A bool) : bool :=
    match o_value with
    | Nonefalse
    | Some x_valuef_value x_value
    end.

  #[bypass_check(guard)]
  Definition valid_back_path `{FArgs} {A B : Set}
    (equal_ptr : A A bool) (deref : A option (cell B A)) (cell_ptr : A)
    (target_ptr : A) (path : list A) : bool :=
    assume_some (deref target_ptr)
      (fun (target : cell B A) ⇒
        assume_some (deref cell_ptr)
          (fun (cell_value : cell B A) ⇒
            let target_index : int :=
              index_value target
            in let cell_index : int :=
              index_value cell_value in
            let fix valid_path
              (index_value : int) (cell_ptr : A) (path : list A) {struct path}
              : bool :=
              match (cell_ptr, path) with
              | (final_cell, [])
                (equal_ptr target_ptr final_cell) &&
                (index_value =i target_index)
              | (cell_ptr, cons cell_ptr' path)
                assume_some (deref cell_ptr)
                  (fun (cell_value : cell B A) ⇒
                    assume_some (deref cell_ptr')
                      (fun (cell' : cell B A) ⇒
                        (mem equal_ptr cell_ptr' cell_value.(cell.back_pointers))
                        &&
                        (assume_some (best_skip cell_value target_index)
                          (fun (best_idx : int) ⇒
                            assume_some (back_pointer cell_value best_idx)
                              (fun (best_ptr : A) ⇒
                                let minimal := equal_ptr best_ptr cell_ptr' in
                                let index' := cell'.(cell.index) in
                                minimal && (valid_path index' cell_ptr' path))))))
              end in
            match path with
            | []false
            | cons first_cell_ptr path
              (equal_ptr first_cell_ptr cell_ptr) &&
              (valid_path cell_index cell_ptr path)
            end)).

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      S.equal _ _ := equal;
      S.encoding _ _ := encoding;
      S.index_value _ _ := index_value;
      S.content _ _ := content;
      S.back_pointer _ _ := back_pointer;
      S.back_pointers _ _ := back_pointers;
      S.genesis _ _ := genesis;
      S.next _ _ := next;
      S.back_path _ _ := back_path;
      S.valid_back_path _ _ := valid_back_path
    |}.
End Make.
Definition Make (Parameters : S_Parameters) : S (cell := _) :=
  let '_ := Make.Build_FArgs Parameters in
  Make.functor.