Skip to main content

🦏 Sc_rollup_inbox_merkelized_payload_hashes_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.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bounded_history_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_inbox_message_repr.merkelized_payload_hashes_proof_error"
    "Internal error: error occurred during proof production or validation"
    "A merkelized payload hashes proof error."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (e_value : string) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Proof error: "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format)) "Proof error: %s")
            e_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "error" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Merkelized_payload_hashes_proof_error" then
          let e_value := cast string payload in
          Some e_value
        else None
      end)
    (fun (e_value : string) ⇒
      Build_extensible "Merkelized_payload_hashes_proof_error" string e_value).

Module Skip_list_parameters.
  Definition basis : int := 2.

  (* Skip_list_parameters *)
  Definition module :=
    {|
      Skip_list_repr.S_Parameters.basis := basis
    |}.
End Skip_list_parameters.
Definition Skip_list_parameters := Skip_list_parameters.module.

Definition Skip_list := Skip_list_repr.Make Skip_list_parameters.

Definition hash_prefix : string :=
  String.String "003"
    (String.String "250"
      (String.String "174" (String.String "238" (String.String "238" "")))).

Module Hash.
  Definition prefix : string := "scib2".

  Definition encoded_size : int := 55.

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "merkelized_payload_hashes_hash" in
      let title :=
        "The merkelized payload hashes' hash of the smart contract rollup inbox"
        in
      let b58check_prefix := hash_prefix in
      let size_value {A : Set} : option A :=
        None in
      {|
        Blake2B.PrefixedName.name := name;
        Blake2B.PrefixedName.title := title;
        Blake2B.PrefixedName.size_value := size_value;
        Blake2B.PrefixedName.b58check_prefix := b58check_prefix
      |}).

Inclusion of the module [H]
  Definition t := H.(S.HASH.t).

  Definition name := H.(S.HASH.name).

  Definition title := H.(S.HASH.title).

  Definition pp := H.(S.HASH.pp).

  Definition pp_short := H.(S.HASH.pp_short).

  Definition op_eq := H.(S.HASH.op_eq).

  Definition op_ltgt := H.(S.HASH.op_ltgt).

  Definition op_lt := H.(S.HASH.op_lt).

  Definition op_lteq := H.(S.HASH.op_lteq).

  Definition op_gteq := H.(S.HASH.op_gteq).

  Definition op_gt := H.(S.HASH.op_gt).

  Definition compare := H.(S.HASH.compare).

  Definition equal := H.(S.HASH.equal).

  Definition max := H.(S.HASH.max).

  Definition min := H.(S.HASH.min).

  Definition hash_bytes := H.(S.HASH.hash_bytes).

  Definition hash_string := H.(S.HASH.hash_string).

  Definition zero := H.(S.HASH.zero).

  Definition size_value := H.(S.HASH.size_value).

  Definition to_bytes := H.(S.HASH.to_bytes).

  Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).

  Definition to_b58check := H.(S.HASH.to_b58check).

  Definition to_short_b58check := H.(S.HASH.to_short_b58check).

  Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).

  Definition b58check_encoding := H.(S.HASH.b58check_encoding).

  Definition encoding := H.(S.HASH.encoding).

  Definition rpc_arg := H.(S.HASH.rpc_arg).

Init function; without side-effects in Coq
  Definition init_module_repr : unit :=
    Base58.check_encoded_prefix b58check_encoding prefix encoded_size.
End Hash.

Definition t : Set :=
  Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t.

Definition equal
  : Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
  
  Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
   bool :=
  Skip_list.(Skip_list_repr.S.equal) Hash.equal
    Sc_rollup_inbox_message_repr.Hash.equal.

Definition hash_value
  (merkelized :
    Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
  : Hash.t :=
  let payload_hash := Skip_list.(Skip_list_repr.S.content) merkelized in
  let back_pointers_hashes :=
    Skip_list.(Skip_list_repr.S.back_pointers) merkelized in
  Hash.hash_bytes None
    (cons (Sc_rollup_inbox_message_repr.Hash.to_bytes payload_hash)
      (List.map Hash.to_bytes back_pointers_hashes)).

Definition pp
  : Format.formatter
  Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t
   unit :=
  Skip_list.(Skip_list_repr.S.pp) Hash.pp Sc_rollup_inbox_message_repr.Hash.pp.

Definition encoding
  : Data_encoding.t
    (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
      Hash.t) :=
  Skip_list.(Skip_list_repr.S.encoding) Hash.encoding
    Sc_rollup_inbox_message_repr.Hash.encoding.

Module merkelized_and_payload.
  Record record : Set := Build {
    merkelized : t;
    payload : Sc_rollup_inbox_message_repr.serialized;
  }.
  Definition with_merkelized merkelized (r : record) :=
    Build merkelized r.(payload).
  Definition with_payload payload (r : record) :=
    Build r.(merkelized) payload.
End merkelized_and_payload.
Definition merkelized_and_payload := merkelized_and_payload.record.

Definition equal_merkelized_and_payload
  (function_parameter : merkelized_and_payload)
  : merkelized_and_payload bool :=
  let '{|
    merkelized_and_payload.merkelized := merkelized;
      merkelized_and_payload.payload := payload
      |} := function_parameter in
  fun (mp2 : merkelized_and_payload) ⇒
    (equal merkelized mp2.(merkelized_and_payload.merkelized)) &&
    (String.equal payload mp2.(merkelized_and_payload.payload)).

Definition pp_merkelized_and_payload
  (fmt : Format.formatter) (function_parameter : merkelized_and_payload)
  : unit :=
  let '{|
    merkelized_and_payload.merkelized := merkelized;
      merkelized_and_payload.payload := payload
      |} := function_parameter in
  Format.fprintf fmt
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "<hv 2>"
              CamlinternalFormatBasics.End_of_format) "<hv 2>"))
        (CamlinternalFormatBasics.String_literal "merkelized:"
          (CamlinternalFormatBasics.Formatting_lit
            (CamlinternalFormatBasics.Break "@," 0 0)
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@," 0 0)
                (CamlinternalFormatBasics.String_literal "payload: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Formatting_lit
                      CamlinternalFormatBasics.Close_box
                      CamlinternalFormatBasics.End_of_format))))))))
      "@[<hv 2>merkelized:@,%a@,payload: %a@]") pp merkelized
    Format.pp_print_string payload.

Definition merkelized_and_payload_encoding
  : Data_encoding.encoding merkelized_and_payload :=
  Data_encoding.conv
    (fun (function_parameter : merkelized_and_payload) ⇒
      let '{|
        merkelized_and_payload.merkelized := merkelized;
          merkelized_and_payload.payload := payload
          |} := function_parameter in
      (merkelized, payload))
    (fun (function_parameter : t × string) ⇒
      let '(merkelized, payload) := function_parameter in
      {| merkelized_and_payload.merkelized := merkelized;
        merkelized_and_payload.payload :=
          Sc_rollup_inbox_message_repr.unsafe_of_string payload; |}) None
    (Data_encoding.merge_objs encoding
      (Data_encoding.obj1
        (Data_encoding.req None None "payload" Data_encoding.string_value))).

Module History.
  Definition Bounded_history_repr_Make_include :=
    Bounded_history_repr.Make
      (let name := "level_inbox_history" in
      let _sig_NAME := tt in
      {|
        Bounded_history_repr.NAME.name := name;
        Bounded_history_repr.NAME._sig_NAME := _sig_NAME
      |})
      (let t : Set := Hash.t in
      let compare := Hash.compare in
      let pp := Hash.pp in
      let encoding := Hash.encoding in
      let _sig_KEY := tt in
      {|
        Bounded_history_repr.KEY.compare := compare;
        Bounded_history_repr.KEY.pp := pp;
        Bounded_history_repr.KEY.encoding := encoding;
        Bounded_history_repr.KEY._sig_KEY := _sig_KEY
      |})
      (let t : Set := merkelized_and_payload in
      let pp := pp_merkelized_and_payload in
      let equal := equal_merkelized_and_payload in
      let encoding := merkelized_and_payload_encoding in
      {|
        Bounded_history_repr.VALUE.equal := equal;
        Bounded_history_repr.VALUE.pp := pp;
        Bounded_history_repr.VALUE.encoding := encoding
      |}).

Inclusion of the module [Bounded_history_repr_Make_include]
  Definition t := Bounded_history_repr_Make_include.(Bounded_history_repr.S.t).

  Definition key :=
    Bounded_history_repr_Make_include.(Bounded_history_repr.S.key).

  Definition value :=
    Bounded_history_repr_Make_include.(Bounded_history_repr.S.value).

  Definition empty :=
    Bounded_history_repr_Make_include.(Bounded_history_repr.S.empty).

  Definition encoding :=
    Bounded_history_repr_Make_include.(Bounded_history_repr.S.encoding).

  Definition pp :=
    Bounded_history_repr_Make_include.(Bounded_history_repr.S.pp).

  Definition find :=
    Bounded_history_repr_Make_include.(Bounded_history_repr.S.find).

  Definition remember :=
    Bounded_history_repr_Make_include.(Bounded_history_repr.S.remember).

  Definition no_history : t := empty 0.
End History.

Definition remember
  (history_value : History.t)
  (merkelized :
    Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
  (payload : Sc_rollup_inbox_message_repr.serialized) : M? History.t :=
  let prev_cell_ptr := hash_value merkelized in
  History.remember prev_cell_ptr
    {| merkelized_and_payload.merkelized := merkelized;
      merkelized_and_payload.payload := payload; |} history_value.

Definition genesis
  (history_value : History.t)
  (payload : Sc_rollup_inbox_message_repr.serialized)
  : M?
    (History.t ×
      Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
        Hash.t) :=
  let payload_hash :=
    Sc_rollup_inbox_message_repr.hash_serialized_message payload in
  let merkelized := Skip_list.(Skip_list_repr.S.genesis) payload_hash in
  Error_monad.Result_syntax.op_letplus
    (remember history_value merkelized payload)
    (fun history_value(history_value, merkelized)).

Definition add_payload
  (history_value : History.t)
  (prev_merkelized :
    Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
  (payload : Sc_rollup_inbox_message_repr.serialized)
  : M?
    (History.t ×
      Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
        Hash.t) :=
  let prev_merkelized_ptr := hash_value prev_merkelized in
  let merkelized :=
    Skip_list.(Skip_list_repr.S.next) prev_merkelized prev_merkelized_ptr
      (Sc_rollup_inbox_message_repr.hash_serialized_message payload) in
  let? history_value := remember history_value merkelized payload in
  return? (history_value, merkelized).

Definition get_payload_hash {A B : Set}
  : Skip_list.(Skip_list_repr.S.cell) A B A :=
  Skip_list.(Skip_list_repr.S.content).

Definition get_index {A B : Set}
  : Skip_list.(Skip_list_repr.S.cell) A B int :=
  Skip_list.(Skip_list_repr.S.index_value).

Definition proof : Set := list t.

Definition pp_proof
  : Format.formatter
  list
    (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
      Hash.t) unit := Format.pp_print_list None pp.

Definition proof_encoding
  : Data_encoding.encoding
    (list
      (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
        Hash.t)) := Data_encoding.list_value None encoding.

Definition produce_proof
  (history_value : History.t) (index_value : int)
  (merkelized :
    Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t Hash.t)
  : option (merkelized_and_payload × list t) :=
  let deref (ptr : History.key) : option t :=
    let× '{|
      merkelized_and_payload.merkelized := merkelized;
        merkelized_and_payload.payload := _
        |} := History.find ptr history_value in
    return× merkelized in
  let current_ptr := hash_value merkelized in
  let lift_ptr :=
    let fix aux (acc_value : list t) (function_parameter : list History.key)
      : option (merkelized_and_payload × list t) :=
      match function_parameter with
      | []None
      | cons last_ptr []
        Error_monad.Option_syntax.op_letplus
          (History.find last_ptr history_value)
          (fun function_parameter
            let
              '{| merkelized_and_payload.merkelized := merkelized |} as
                merkelized_and_payload := function_parameter in
            (merkelized_and_payload, (List.rev (cons merkelized acc_value))))
      | cons ptr rest
        let× merkelized := deref ptr in
        aux (cons merkelized acc_value) rest
      end in
    aux nil in
  let× ptr_path :=
    Skip_list.(Skip_list_repr.S.back_path) deref current_ptr index_value in
  lift_ptr ptr_path.

Definition verify_proof
  (inclusion_proof :
    list
      (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
        Hash.t))
  : M?
    (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
      Hash.t ×
      Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
        Hash.t) :=
  let? cell_value :=
    match inclusion_proof with
    | cons cell_value _return? cell_value
    | []
      Error_monad.error_value
        (Build_extensible "Merkelized_payload_hashes_proof_error" string
          "inclusion proof is empty")
    end in
  let fix aux
    (hash_map_ptr_list :
      Hash.H.(S.HASH.Map).(S.INDEXES_MAP.t)
        (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
          Hash.t) × list Hash.t)
    (l_value :
      list
        (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
          Hash.t))
    : M?
      (Hash.H.(S.HASH.Map).(S.INDEXES_MAP.t)
        (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
          Hash.t) × list Hash.t ×
        Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
          Hash.t × Hash.t) :=
    let '(hash_map, ptr_list) := hash_map_ptr_list in
    match l_value with
    | []
      Error_monad.error_value
        (Build_extensible "Merkelized_payload_hashes_proof_error" string
          "inclusion proof is empty")
    | cons target []
      let target_ptr := hash_value target in
      let hash_map :=
        Hash.H.(HASH.Map).(S.INDEXES_MAP.add) target_ptr target hash_map in
      let ptr_list := List.rev (cons target_ptr ptr_list) in
      return? (hash_map, ptr_list, target, target_ptr)
    | cons merkelized tail
      let ptr := hash_value merkelized in
      aux
        ((Hash.H.(HASH.Map).(S.INDEXES_MAP.add) ptr merkelized hash_map),
          (cons ptr ptr_list)) tail
    end in
  let? '(hash_map, ptr_list, target, target_ptr) :=
    aux (Hash.H.(HASH.Map).(S.INDEXES_MAP.empty), nil) inclusion_proof in
  let deref (ptr : Hash.H.(S.HASH.t))
    : option
      (Skip_list.(Skip_list_repr.S.cell) Sc_rollup_inbox_message_repr.Hash.t
        Hash.t) :=
    Hash.H.(HASH.Map).(S.INDEXES_MAP.find) ptr hash_map in
  let cell_ptr := hash_value cell_value in
  let? '_ :=
    Error_monad.error_unless
      (Skip_list.(Skip_list_repr.S.valid_back_path) Hash.equal deref cell_ptr
        target_ptr ptr_list)
      (Build_extensible "Merkelized_payload_hashes_proof_error" string
        "invalid inclusion proof") in
  return? (target, cell_value).