Skip to main content

🐆 Tx_rollup_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "rollup.invalid_tx_rollup_notation" "Invalid tx rollup notation"
    "A malformed tx rollup notation was given to an RPC or in a script."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (x_value : string) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Invalid tx rollup notation "
                (CamlinternalFormatBasics.Caml_string
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format))
              "Invalid tx rollup notation %S") x_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "notation" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_rollup_notation" then
          let loc_value := cast string payload in
          Some loc_value
        else None
      end)
    (fun (loc_value : string) ⇒
      Build_extensible "Invalid_rollup_notation" string loc_value).

Module Hash.
  Definition rollup_hash : string :=
    Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.b58check_prefix).

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "Rollup_hash" in
      let title := "A rollup ID" in
      let b58check_prefix := rollup_hash in
      let size_value :=
        Some Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.hash_size)
        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]
  Definition to_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.to_path).

  Definition of_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.of_path).

  Definition path_length :=
    Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
End Hash.

Definition t : Set := Hash.t.

Definition tx_rollup : Set := t.

Definition Compare_impl :=
  Compare.Make
    (let t : Set := t in
    let compare (r1 : Hash.t) (r2 : Hash.t) : int :=
      Hash.compare r1 r2 in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_impl]
Definition op_eq := Compare_impl.(Compare.S.op_eq).

Definition op_ltgt := Compare_impl.(Compare.S.op_ltgt).

Definition op_lt := Compare_impl.(Compare.S.op_lt).

Definition op_lteq := Compare_impl.(Compare.S.op_lteq).

Definition op_gteq := Compare_impl.(Compare.S.op_gteq).

Definition op_gt := Compare_impl.(Compare.S.op_gt).

Definition compare := Compare_impl.(Compare.S.compare).

Definition equal := Compare_impl.(Compare.S.equal).

Definition max := Compare_impl.(Compare.S.max).

Definition min := Compare_impl.(Compare.S.min).

Definition in_memory_size {A : Set} (function_parameter : A)
  : Saturation_repr.t :=
  let '_ := function_parameter in
  Cache_memory_helpers.op_plusexclamation
    (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
      Cache_memory_helpers.word_size)
    (Cache_memory_helpers.string_size_gen
      Tx_rollup_prefixes.rollup_address.(Tx_rollup_prefixes.t.hash_size)).

Definition to_b58check (rollup : Hash.t) : string := Hash.to_b58check rollup.

Definition of_b58check_opt (s_value : string) : option Hash.t :=
  match Base58.decode s_value with
  | Some data
    match data with
    | Build_extensible tag _ payload
      if String.eqb tag "Data" then
        let hash_value := cast Hash.t payload in
        Some hash_value
      else None
    end
  | _None
  end.

Definition of_b58check (s_value : string) : M? Hash.t :=
  match of_b58check_opt s_value with
  | Some hash_valuereturn? hash_value
  | _
    Error_monad.error_value
      (Build_extensible "Invalid_rollup_notation" string s_value)
  end.

Definition pp (ppf : Format.formatter) (hash_value : Hash.t) : unit :=
  Hash.pp ppf hash_value.

Definition encoding : Data_encoding.encoding Hash.t :=
  Data_encoding.def "tx_rollup_id" (Some "A tx rollup handle")
    (Some
      "A tx rollup notation as given to an RPC or inside scripts, is a base58 tx rollup hash")
    (Data_encoding.splitted
      (Data_encoding.conv to_b58check
        (fun (s_value : string) ⇒
          match of_b58check s_value with
          | Pervasives.Ok s_values_value
          | Pervasives.Error _
            Data_encoding.Json.cannot_destruct
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid tx rollup notation."
                  CamlinternalFormatBasics.End_of_format)
                "Invalid tx rollup notation.")
          end) None Data_encoding.string_value) Hash.encoding).

Definition originated_tx_rollup (nonce_value : Origination_nonce.t) : Hash.t :=
  let data :=
    Data_encoding.Binary.to_bytes_exn None Origination_nonce.encoding
      nonce_value in
  Hash.hash_bytes None [ data ].

Definition rpc_arg : RPC_arg.arg Hash.t :=
  let construct := to_b58check in
  let destruct (hash_value : string) : Pervasives.result Hash.t string :=
    Result.map_error
      (fun (function_parameter : Error_monad.trace Error_monad._error) ⇒
        let '_ := function_parameter in
        "Cannot parse tx rollup id") (of_b58check hash_value) in
  RPC_arg.make (Some "A tx rollup identifier encoded in b58check.")
    "tx_rollup_id" destruct construct tt.

Module Index.
  Definition t : Set := tx_rollup.

  Definition path_length : int := 1.

  Definition to_path (c_value : Hash.t) (l_value : list string) : list string :=
    let raw_key := Data_encoding.Binary.to_bytes_exn None 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) : option Hash.t :=
    match function_parameter with
    | cons key_value []
      Option.bind (Hex.to_bytes (Hex.Hex key_value))
        (Data_encoding.Binary.of_bytes_opt encoding)
    | _None
    end.

  Definition rpc_arg : RPC_arg.arg Hash.t := rpc_arg.

  Definition encoding : Data_encoding.encoding Hash.t := encoding.

  Definition compare : t t int := 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 deposit_entrypoint : Entrypoint_repr.t :=
  Entrypoint_repr.of_string_strict_exn "deposit".

Definition _Set :=
  _Set.Make
    (let t : Set := tx_rollup in
    let op_eq := Compare_impl.(Compare.S.op_eq) in
    let op_ltgt := Compare_impl.(Compare.S.op_ltgt) in
    let op_lt := Compare_impl.(Compare.S.op_lt) in
    let op_lteq := Compare_impl.(Compare.S.op_lteq) in
    let op_gteq := Compare_impl.(Compare.S.op_gteq) in
    let op_gt := Compare_impl.(Compare.S.op_gt) in
    let compare := Compare_impl.(Compare.S.compare) in
    let equal := Compare_impl.(Compare.S.equal) in
    let max := Compare_impl.(Compare.S.max) in
    let min := Compare_impl.(Compare.S.min) in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Definition Map :=
  Map.Make
    (let t : Set := tx_rollup in
    let op_eq := Compare_impl.(Compare.S.op_eq) in
    let op_ltgt := Compare_impl.(Compare.S.op_ltgt) in
    let op_lt := Compare_impl.(Compare.S.op_lt) in
    let op_lteq := Compare_impl.(Compare.S.op_lteq) in
    let op_gteq := Compare_impl.(Compare.S.op_gteq) in
    let op_gt := Compare_impl.(Compare.S.op_gt) in
    let compare := Compare_impl.(Compare.S.compare) in
    let equal := Compare_impl.(Compare.S.equal) in
    let max := Compare_impl.(Compare.S.max) in
    let min := Compare_impl.(Compare.S.min) in
    {|
      Compare.COMPARABLE.compare := compare
    |}).