Skip to main content

🦏 Sc_rollup_outbox_message_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 :=
  let msg :=
    "Failed to encode a rollup management protocol outbox message value" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "sc_rollup_outbox_message_repr.error_encoding_outbox_message" msg msg
      (Some
        (fun (fmt : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf fmt
              (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_encode_outbox_message" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Error_encode_outbox_message" unit tt) in
  let msg :=
    "Failed to decode a rollup management protocol outbox message value" in
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_outbox_message_repr.error_decoding_outbox_message" msg msg
    (Some
      (fun (fmt : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf fmt
            (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_decode_outbox_message" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Error_decode_outbox_message" unit tt).

Module transaction.
  Record record : Set := Build {
    unparsed_parameters : Script_repr.expr;
    destination : Contract_hash.t;
    entrypoint : Entrypoint_repr.t;
  }.
  Definition with_unparsed_parameters unparsed_parameters (r : record) :=
    Build unparsed_parameters r.(destination) r.(entrypoint).
  Definition with_destination destination (r : record) :=
    Build r.(unparsed_parameters) destination r.(entrypoint).
  Definition with_entrypoint entrypoint (r : record) :=
    Build r.(unparsed_parameters) r.(destination) entrypoint.
End transaction.
Definition transaction := transaction.record.

Records for the constructor parameters
Module ConstructorRecords_t.
  Module t.
    Module Atomic_transaction_batch.
      Record record {transactions : Set} : Set := Build {
        transactions : transactions;
      }.
      Arguments record : clear implicits.
      Definition with_transactions {t_transactions} transactions
        (r : record t_transactions) :=
        Build t_transactions transactions.
    End Atomic_transaction_batch.
    Definition Atomic_transaction_batch_skeleton :=
      Atomic_transaction_batch.record.
  End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.

Reserved Notation "'t.Atomic_transaction_batch".

Inductive t : Set :=
| Atomic_transaction_batch : 't.Atomic_transaction_batch t

where "'t.Atomic_transaction_batch" :=
  (t.Atomic_transaction_batch_skeleton (list transaction)).

Module t.
  Include ConstructorRecords_t.t.
  Definition Atomic_transaction_batch := 't.Atomic_transaction_batch.
End t.

Definition transaction_encoding : Data_encoding.encoding transaction :=
  Data_encoding.conv
    (fun (function_parameter : transaction) ⇒
      let '{|
        transaction.unparsed_parameters := unparsed_parameters;
          transaction.destination := destination;
          transaction.entrypoint := entrypoint
          |} := function_parameter in
      (unparsed_parameters, destination, entrypoint))
    (fun (function_parameter :
      Script_repr.expr × Contract_hash.t × Entrypoint_repr.t) ⇒
      let '(unparsed_parameters, destination, entrypoint) := function_parameter
        in
      {| transaction.unparsed_parameters := unparsed_parameters;
        transaction.destination := destination;
        transaction.entrypoint := entrypoint; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None None "parameters" Script_repr.expr_encoding)
      (Data_encoding.req None None "destination"
        Contract_repr.originated_encoding)
      (Data_encoding.dft None None "entrypoint" Entrypoint_repr.simple_encoding
        Entrypoint_repr.default)).

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
    (Data_encoding.union None
      [
        Data_encoding.case_value "Atomic_transaction_batch" None
          (Data_encoding.Tag 0)
          (Data_encoding.obj1
            (Data_encoding.req None None "transactions"
              (Data_encoding.list_value None transaction_encoding)))
          (fun (function_parameter : t) ⇒
            let
              'Atomic_transaction_batch {|
                t.Atomic_transaction_batch.transactions := transactions
                  |} := function_parameter in
            Some transactions)
          (fun (transactions : list transaction) ⇒
            Atomic_transaction_batch
              {|
                t.Atomic_transaction_batch.transactions :=
                  transactions; |})
      ]).

Definition pp_transaction
  (fmt : Format.formatter) (function_parameter : transaction) : unit :=
  let '{|
    transaction.unparsed_parameters := unparsed_parameters;
      transaction.destination := destination;
      transaction.entrypoint := entrypoint
      |} := function_parameter in
  let json_value :=
    Data_encoding.Json.construct None Script_repr.expr_encoding
      unparsed_parameters in
  Format.fprintf fmt
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            CamlinternalFormatBasics.End_of_format ""))
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.Formatting_lit
            (CamlinternalFormatBasics.Break "@;" 1 0)
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@;" 1 0)
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Formatting_lit
                    CamlinternalFormatBasics.Close_box
                    CamlinternalFormatBasics.End_of_format)))))))
      "@[%a@;%a@;%a@]") Contract_hash.pp destination Entrypoint_repr.pp
    entrypoint Data_encoding.Json.pp json_value.

Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
  let
    'Atomic_transaction_batch {|
      t.Atomic_transaction_batch.transactions := transactions |} :=
    function_parameter in
  Format.pp_print_list (Some Format.pp_print_space) pp_transaction fmt
    transactions.

Definition serialized : Set := string.

Definition deserialize (data : string) : M? t :=
  match Data_encoding.Binary.of_string_opt encoding data with
  | Some x_valuereturn? x_value
  | None
    Error_monad.Tzresult_syntax.fail
      (Build_extensible "Error_decode_outbox_message" unit tt)
  end.

Definition serialize (outbox_message : t) : M? string :=
  match Data_encoding.Binary.to_string_opt None encoding outbox_message with
  | Some strreturn? str
  | None
    Error_monad.Tzresult_syntax.fail
      (Build_extensible "Error_encode_outbox_message" unit tt)
  end.

Definition unsafe_of_string {A : Set} (s_value : A) : A := s_value.

Definition unsafe_to_string {A : Set} (s_value : A) : A := s_value.