Skip to main content

🎯 Destination_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.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.

Inductive t : Set :=
| Contract : Contract_repr.t t
| Tx_rollup : Tx_rollup_repr.t t
| Sc_rollup : Sc_rollup_repr.t t
| Zk_rollup : Zk_rollup_repr.t t.

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    let compare (l1 : t) (l2 : t) : int :=
      match (l1, l2) with
      | (Contract k1, Contract k2)Contract_repr.compare k1 k2
      | (Tx_rollup k1, Tx_rollup k2)Tx_rollup_repr.compare k1 k2
      | (Sc_rollup k1, Sc_rollup k2)Sc_rollup_repr.Address.compare k1 k2
      | (Zk_rollup k1, Zk_rollup k2)Zk_rollup_repr.Address.compare k1 k2
      | (Contract _, _) ⇒ (-1)
      | (_, Contract _) ⇒ 1
      | (Tx_rollup _, _) ⇒ (-1)
      | (_, Tx_rollup _) ⇒ 1
      | (Sc_rollup _, _) ⇒ (-1)
      | (_, Sc_rollup _) ⇒ 1
      end in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_Make_include]
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "destination_repr.invalid_b58check" "Destination decoding failed"
    "Failed to read a valid destination from a b58check_encoding data" None
    (Data_encoding.obj1
      (Data_encoding.req None None "input" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_destination_b58check" then
          let x_value := cast string payload in
          Some x_value
        else None
      end)
    (fun (x_value : string) ⇒
      Build_extensible "Invalid_destination_b58check" string x_value).

Definition of_b58data (data : Base58.data) : option t :=
  let decode_on_none {A B : Set}
    (decode : Base58.data option A) (wrap : A B)
    (function_parameter : option B) : option B :=
    match function_parameter with
    | Some x_valueSome x_value
    | NoneOption.map wrap (decode data)
    end in
  decode_on_none Zk_rollup_repr.Address.of_b58data
    (fun (z_value : Zk_rollup_repr.Address.t) ⇒ Zk_rollup z_value)
    (decode_on_none Sc_rollup_repr.Address.of_b58data
      (fun (s_value : Sc_rollup_repr.Address.t) ⇒ Sc_rollup s_value)
      (decode_on_none Tx_rollup_repr.of_b58data
        (fun (t_value : Tx_rollup_repr.t) ⇒ Tx_rollup t_value)
        (decode_on_none Contract_repr.of_b58data
          (fun (c_value : Contract_repr.t) ⇒ Contract c_value) None))).

Definition of_b58check_opt (s_value : string) : option t :=
  Option.bind (Base58.decode s_value) of_b58data.

Definition of_b58check (s_value : string) : M? t :=
  match of_b58check_opt s_value with
  | None
    Error_monad.error_value
      (Build_extensible "Invalid_destination_b58check" string s_value)
  | Some destPervasives.Ok dest
  end.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.def "transaction_destination"
    (Some "A destination of a transaction")
    (Some
      "A destination notation compatible with the contract notation as given to an RPC or inside scripts. Can be a base58 implicit contract hash, a base58 originated contract hash, a base58 originated transaction rollup, or a base58 originated smart-contract rollup.")
    (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 destination notation."
                  CamlinternalFormatBasics.End_of_format)
                "Invalid destination notation.")
          end) None Data_encoding.string_value)
      (Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
        (Pervasives.op_at
          (Contract_repr.cases
            (fun (function_parameter : t) ⇒
              match function_parameter with
              | Contract x_valueSome x_value
              | _None
              end) (fun (x_value : Contract_repr.t) ⇒ Contract x_value))
          [
            Data_encoding.case_value "Tx_rollup" None (Data_encoding.Tag 2)
              (Data_encoding.Fixed.add_padding Tx_rollup_repr.encoding 1)
              (fun (function_parameter : t) ⇒
                match function_parameter with
                | Tx_rollup k_valueSome k_value
                | _None
                end)
              (fun (k_value : Tx_rollup_repr.t) ⇒ Tx_rollup k_value);
            Data_encoding.case_value "Sc_rollup" None (Data_encoding.Tag 3)
              (Data_encoding.Fixed.add_padding
                Sc_rollup_repr.Address.encoding 1)
              (fun (function_parameter : t) ⇒
                match function_parameter with
                | Sc_rollup k_valueSome k_value
                | _None
                end)
              (fun (k_value : Sc_rollup_repr.Address.t) ⇒
                Sc_rollup k_value);
            Data_encoding.case_value "Zk_rollup" None (Data_encoding.Tag 4)
              (Data_encoding.Fixed.add_padding
                Zk_rollup_repr.Address.encoding 1)
              (fun (function_parameter : t) ⇒
                match function_parameter with
                | Zk_rollup k_valueSome k_value
                | _None
                end)
              (fun (k_value : Zk_rollup_repr.Address.t) ⇒
                Zk_rollup k_value)
          ]))).

Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
  match function_parameter with
  | Contract k_valueContract_repr.pp fmt k_value
  | Tx_rollup k_valueTx_rollup_repr.pp fmt k_value
  | Sc_rollup k_valueSc_rollup_repr.pp fmt k_value
  | Zk_rollup k_valueZk_rollup_repr.Address.pp fmt k_value
  end.

Definition in_memory_size (function_parameter : t) : Saturation_repr.t :=
  match function_parameter with
  | Contract k_value
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      (Contract_repr.in_memory_size k_value)
  | Tx_rollup k_value
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      (Tx_rollup_repr.in_memory_size k_value)
  | Sc_rollup k_value
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      (Sc_rollup_repr.in_memory_size k_value)
  | Zk_rollup k_value
    Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.h1w
      (Zk_rollup_repr.in_memory_size k_value)
  end.