Skip to main content

🦏 Sc_rollup_inbox_message_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.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let msg := "Failed to encode a rollup management protocol inbox message value"
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "sc_rollup_inbox_message_repr.error_encoding_inbox_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_inbox_message" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Error_encode_inbox_message" unit tt) in
  let msg := "Failed to decode a rollup management protocol inbox message value"
    in
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_inbox_message_repr.error_decoding_inbox_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_inbox_message" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Error_decode_inbox_message" unit tt).

Module internal_inbox_message.
  Record record : Set := Build {
    payload : Script_repr.expr;
    sender : Contract_hash.t;
    source : Signature.public_key_hash;
  }.
  Definition with_payload payload (r : record) :=
    Build payload r.(sender) r.(source).
  Definition with_sender sender (r : record) :=
    Build r.(payload) sender r.(source).
  Definition with_source source (r : record) :=
    Build r.(payload) r.(sender) source.
End internal_inbox_message.
Definition internal_inbox_message := internal_inbox_message.record.

Inductive t : Set :=
| Internal : internal_inbox_message t
| External : string t.

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 "Internal" None (Data_encoding.Tag 0)
          (Data_encoding.obj3
            (Data_encoding.req None None "payload"
              Script_repr.expr_encoding)
            (Data_encoding.req None None "sender" Contract_hash.encoding)
            (Data_encoding.req None None "source"
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
          (fun (function_parameter : t) ⇒
            match function_parameter with
            |
              Internal {|
                internal_inbox_message.payload := payload;
                  internal_inbox_message.sender := sender;
                  internal_inbox_message.source := source
                  |} ⇒ Some (payload, sender, source)
            | External _None
            end)
          (fun (function_parameter :
            Script_repr.expr × Contract_hash.t ×
              Signature.public_key_hash) ⇒
            let '(payload, sender, source) := function_parameter in
            Internal
              {| internal_inbox_message.payload := payload;
                internal_inbox_message.sender := sender;
                internal_inbox_message.source := source; |});
        Data_encoding.case_value "External" None (Data_encoding.Tag 1)
          Data_encoding._Variable.string_value
          (fun (function_parameter : t) ⇒
            match function_parameter with
            | External msgSome msg
            | Internal _None
            end) (fun (msg : string) ⇒ External msg)
      ]).

Definition serialized : Set := string.

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

Definition deserialize (s_value : string) : M? t :=
  match Data_encoding.Binary.of_string_opt encoding s_value with
  | None
    Error_monad.Tzresult_syntax.fail
      (Build_extensible "Error_decode_inbox_message" unit tt)
  | Some msgreturn? msg
  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.