Skip to main content

🇿 Zk_rollup_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.V7.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_scalar.

Module Address.
  Definition prefix : string := "zkr1".

  Definition encoded_size : int := 37.

  Definition decoded_prefix : string :=
    String.String "001" (String.String "171" ("T" ++ String.String "251" "")).

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "Zk_rollup_hash" in
      let title := "A zk rollup address" in
      let b58check_prefix := decoded_prefix in
      let size_value := Some 20 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
Inclusion of the module [Path_encoding_Make_hex_include]
Init function; without side-effects in Coq
  Definition init_module2 : unit :=
    let msg := "Error while generating rollup address" in
    Error_monad.register_error_kind Error_monad.Permanent
      "rollup.error_zk_rollup_address_generation" msg msg
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") msg))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Error_zk_rollup_address_generation" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Error_zk_rollup_address_generation" unit tt).

  Definition from_nonce (nonce_value : Origination_nonce.t) : M? t :=
    (fun (function_parameter : option bytes) ⇒
      match function_parameter with
      | None
        Error_monad.error_value
          (Build_extensible "Error_zk_rollup_address_generation" unit tt)
      | Some nonce_valuereturn? (hash_bytes None [ nonce_value ])
      end)
      (Data_encoding.Binary.to_bytes_opt None Origination_nonce.encoding
        nonce_value).

  Definition of_b58data (function_parameter : Base58.data)
    : option H.(S.HASH.t) :=
    match function_parameter with
    | Build_extensible tag _ payload
      if String.eqb tag "Data" then
        let h_value := cast H.(S.HASH.t) payload in
        Some h_value
      else None
    end.
End Address.

Definition t : Set := Address.t.

Definition to_scalar (x_value : Address.t) : Zk_rollup_scalar.t :=
  Zk_rollup_scalar.of_bits
    (Data_encoding.Binary.to_string_exn None Address.encoding x_value).

Records for the constructor parameters
Module ConstructorRecords_pending_list.
  Module pending_list.
    Module Empty.
      Record record {next_index : Set} : Set := Build {
        next_index : next_index;
      }.
      Arguments record : clear implicits.
      Definition with_next_index {t_next_index} next_index
        (r : record t_next_index) :=
        Build t_next_index next_index.
    End Empty.
    Definition Empty_skeleton := Empty.record.

    Module Pending.
      Record record {next_index length : Set} : Set := Build {
        next_index : next_index;
        length : length;
      }.
      Arguments record : clear implicits.
      Definition with_next_index {t_next_index t_length} next_index
        (r : record t_next_index t_length) :=
        Build t_next_index t_length next_index r.(length).
      Definition with_length {t_next_index t_length} length
        (r : record t_next_index t_length) :=
        Build t_next_index t_length r.(next_index) length.
    End Pending.
    Definition Pending_skeleton := Pending.record.
  End pending_list.
End ConstructorRecords_pending_list.
Import ConstructorRecords_pending_list.

Reserved Notation "'pending_list.Empty".
Reserved Notation "'pending_list.Pending".

Inductive pending_list : Set :=
| Empty : 'pending_list.Empty pending_list
| Pending : 'pending_list.Pending pending_list

where "'pending_list.Empty" := (pending_list.Empty_skeleton int64)
and "'pending_list.Pending" := (pending_list.Pending_skeleton int64 int).

Module pending_list.
  Include ConstructorRecords_pending_list.pending_list.
  Definition Empty := 'pending_list.Empty.
  Definition Pending := 'pending_list.Pending.
End pending_list.

Definition pending_list_encoding : Data_encoding.t pending_list :=
  let '(empty_tag, pending_tag) := (0, 1) in
  let empty_encoding :=
    Data_encoding.obj1
      (Data_encoding.req None None "next_index"
        (Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
          Data_encoding.Compact.int64_value)) in
  let pending_encoding :=
    Data_encoding.obj2
      (Data_encoding.req None None "next_index"
        (Data_encoding.Compact.make (Some (Variant.Build "Uint8" unit tt))
          Data_encoding.Compact.int64_value))
      (Data_encoding.req None None "length" Data_encoding.uint16) in
  Data_encoding.matching None
    (fun (function_parameter : pending_list) ⇒
      match function_parameter with
      | Empty {| pending_list.Empty.next_index := next_index |} ⇒
        Data_encoding.matched None empty_tag empty_encoding next_index
      |
        Pending {|
          pending_list.Pending.next_index := next_index;
            pending_list.Pending.length := length
            |} ⇒
        Data_encoding.matched None pending_tag pending_encoding
          (next_index, length)
      end)
    [
      Data_encoding.case_value "Empty" None (Data_encoding.Tag empty_tag)
        empty_encoding
        (fun (function_parameter : pending_list) ⇒
          match function_parameter with
          | Empty {| pending_list.Empty.next_index := next_index |} ⇒
            Some next_index
          | _None
          end)
        (fun (next_index : int64) ⇒
          Empty {| pending_list.Empty.next_index := next_index; |});
      Data_encoding.case_value "Pending" None (Data_encoding.Tag pending_tag)
        pending_encoding
        (fun (function_parameter : pending_list) ⇒
          match function_parameter with
          |
            Pending {|
              pending_list.Pending.next_index := next_index;
                pending_list.Pending.length := length
                |} ⇒ Some (next_index, length)
          | _None
          end)
        (fun (function_parameter : int64 × int) ⇒
          let '(next_index, length) := function_parameter in
          Pending
            {| pending_list.Pending.next_index := next_index;
              pending_list.Pending.length := length; |})
    ].

Module Index.
  Definition t : Set := t.

  Definition path_length : M? int := return? 1.

  Definition to_path (c_value : Address.t) (l_value : list string)
    : list string :=
    let raw_key :=
      Data_encoding.Binary.to_bytes_exn None Address.encoding c_value in
    let 'Hex.Hex key_value := Hex.of_bytes None raw_key in
    cons key_value l_value.

  Definition of_path (function_parameter : list string)
    : M? (option Address.t) :=
    match function_parameter with
    | cons key_value []
      return?
        (Option.bind (Hex.to_bytes (Hex.Hex key_value))
          (Data_encoding.Binary.of_bytes_opt Address.encoding))
    | _return? None
    end.

  Definition rpc_arg : RPC_arg.t Address.t := Address.rpc_arg.

  Definition encoding : Data_encoding.t Address.t := Address.encoding.

  Definition compare : Address.t Address.t int := Address.compare.

  (* Index *)
  Definition module :=
    {|
      Storage_description.INDEX.path_length := path_length;
      Storage_description.INDEX.to_path := to_path;
      Storage_description.INDEX.of_path := of_path;
      Storage_description.INDEX.rpc_arg := rpc_arg;
      Storage_description.INDEX.encoding := encoding;
      Storage_description.INDEX.compare := compare
    |}.
End Index.
Definition Index := Index.module.

Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
  let '_ := function_parameter in
  Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
    (Cache_memory_helpers.string_size_gen Address.size_value).