🦏 Sc_rollup_management_protocol.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.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Gas_monad.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Script_cache.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Init function; without side-effects in Coq

Definition init_module : unit :=
  let msg := "Invalid destination" in
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_management_protocol.sc_rollup_invalid_destination" 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 "Sc_rollup_invalid_destination" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Sc_rollup_invalid_destination" unit tt).

Records for the constructor parameters

Module ConstructorRecords_transaction.
  Module transaction.
    Module Transaction.
      Record record {destination entrypoint parameters_ty parameters
        unparsed_parameters : Set} : Set := Build {
        destination : destination;
        entrypoint : entrypoint;
        parameters_ty : parameters_ty;
        parameters : parameters;
        unparsed_parameters : unparsed_parameters;
      }.
      Arguments record : clear implicits.
      Definition with_destination
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} destination
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters destination r.(entrypoint) r.(parameters_ty)
          r.(parameters) r.(unparsed_parameters).
      Definition with_entrypoint
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} entrypoint
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) entrypoint r.(parameters_ty)
          r.(parameters) r.(unparsed_parameters).
      Definition with_parameters_ty
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} parameters_ty
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) r.(entrypoint) parameters_ty
          r.(parameters) r.(unparsed_parameters).
      Definition with_parameters
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} parameters
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
          parameters r.(unparsed_parameters).
      Definition with_unparsed_parameters
        {t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters} unparsed_parameters
        (r :
          record t_destination t_entrypoint t_parameters_ty t_parameters
            t_unparsed_parameters) :=
        Build t_destination t_entrypoint t_parameters_ty t_parameters
          t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
          r.(parameters) unparsed_parameters.
    End Transaction.
    Definition Transaction_skeleton := Transaction.record.
  End transaction.
End ConstructorRecords_transaction.
Import ConstructorRecords_transaction.

Reserved Notation "'transaction.Transaction".

Inductive transaction : Set :=
| Transaction : ∀ {a : Set}, 'transaction.Transaction a → transaction

where "'transaction.Transaction" :=
  (fun (t_a : Set) ⇒ transaction.Transaction_skeleton Contract_hash.t
    Alpha_context.Entrypoint.t Script_typed_ir.ty t_a Alpha_context.Script.expr).

Module transaction.
  Include ConstructorRecords_transaction.transaction.
  Definition Transaction := 'transaction.Transaction.
End transaction.

Module atomic_transaction_batch.
  Record record : Set := Build {
    transactions : list transaction;
  }.
  Definition with_transactions transactions (r : record) :=
    Build transactions.
End atomic_transaction_batch.
Definition atomic_transaction_batch := atomic_transaction_batch.record.

Inductive outbox_message : Set :=
| Atomic_transaction_batch : atomic_transaction_batch → outbox_message.

Definition make_internal_transfer {A : Set}
  (ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty) (payload : A)
  (sender : Contract_hash.t) (source : Alpha_context.public_key_hash)
  (destination : Alpha_context.Sc_rollup.t)
  : M? (Alpha_context.Sc_rollup.Inbox_message.t × Alpha_context.context) :=
  Error_monad.Lwt_result_syntax.op_letplus
    (Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
      ty_value payload)
    (fun function_parameter ⇒
      let '(payload, ctxt) := function_parameter in
      ((Alpha_context.Sc_rollup.Inbox_message.Internal
        (Alpha_context.Sc_rollup.Inbox_message.Transfer
          {|
            Alpha_context.Sc_rollup.Inbox_message.internal_inbox_message.Transfer.payload
              := payload;
            Alpha_context.Sc_rollup.Inbox_message.internal_inbox_message.Transfer.sender
              := sender;
            Alpha_context.Sc_rollup.Inbox_message.internal_inbox_message.Transfer.source
              := source;
            Alpha_context.Sc_rollup.Inbox_message.internal_inbox_message.Transfer.destination
              := destination; |})), ctxt)).

Definition transactions_batch_of_internal
  (ctxt : Alpha_context.context)
  (transactions : list Alpha_context.Sc_rollup.Outbox.Message.transaction)
  : M? (atomic_transaction_batch × Alpha_context.context) :=
  let or_internal_transaction
    (ctxt : Alpha_context.context)
    (function_parameter : Alpha_context.Sc_rollup.Outbox.Message.transaction)
    : M? (transaction × Alpha_context.context) :=
    let '{|
      Sc_rollup_outbox_message_repr.transaction.unparsed_parameters :=
        unparsed_parameters;
        Sc_rollup_outbox_message_repr.transaction.destination := destination;
        Sc_rollup_outbox_message_repr.transaction.entrypoint := entrypoint
        |} := function_parameter in
    let? '(res, ctxt) :=
      let? '(ctxt, _cache_key, cached) := Script_cache.find ctxt destination in
      match cached with
      | Some (_script, ex_script) ⇒ return? (ex_script, ctxt)
      | None ⇒
        Error_monad.Lwt_result_syntax.tzfail
          (Build_extensible "Sc_rollup_invalid_destination" unit tt)
      end in
    let
      'Script_ir_translator.Ex_script
        (Script_typed_ir.Script {|
          Script_typed_ir.script.Script.arg_type := arg_type;
            Script_typed_ir.script.Script.entrypoints := entrypoints
            |}) := res in
    let 'existT _ __Ex_script_'a [entrypoints, arg_type] :=
      cast_exists (Es := Set)
        (fun __Ex_script_'a ⇒
          [Script_typed_ir.entrypoints ** Script_typed_ir.ty])
        [entrypoints, arg_type] in
    let? '(res, ctxt) :=
      Gas_monad.run ctxt
        ((Script_ir_translator.find_entrypoint :
          Script_tc_errors.error_details unit → Script_typed_ir.ty →
          Script_typed_ir.entrypoints → Alpha_context.Entrypoint.t →
          Gas_monad.t (Script_ir_translator.ex_ty_cstr __Ex_script_'a)
            (Error_monad.trace Error_monad._error))
          (Script_tc_errors.Informative tt) arg_type entrypoints entrypoint) in
    let? res := res in
    let
      'Script_ir_translator.Ex_ty_cstr {|
        Script_ir_translator.ex_ty_cstr.Ex_ty_cstr.ty := parameters_ty |} :=
      res in
    let 'existT _ __Ex_ty_cstr_'b parameters_ty :=
      cast_exists (Es := Set) (fun __Ex_ty_cstr_'b ⇒ Script_typed_ir.ty)
        parameters_ty in
    let? '(parameters, ctxt) :=
      (Script_ir_translator.parse_data :
        Script_ir_translator_config.elab_config → Alpha_context.context →
        bool → Script_typed_ir.ty → Alpha_context.Script.node →
        M? (__Ex_ty_cstr_'b × Alpha_context.context))
        (Script_ir_translator_config.make None None false tt) ctxt true
        parameters_ty (Micheline.root_value unparsed_parameters) in
    return?
      ((Transaction
        {| transaction.Transaction.destination := destination;
          transaction.Transaction.entrypoint := entrypoint;
          transaction.Transaction.parameters_ty := parameters_ty;
          transaction.Transaction.parameters := parameters;
          transaction.Transaction.unparsed_parameters := unparsed_parameters; |}),
        ctxt) in
  Error_monad.Lwt_result_syntax.op_letplus
    (List.fold_left_map_es
      (fun (ctxt : Alpha_context.context) ⇒
        fun (msg : Alpha_context.Sc_rollup.Outbox.Message.transaction) ⇒
          Error_monad.Lwt_result_syntax.op_letplus
            (or_internal_transaction ctxt msg)
            (fun function_parameter ⇒
              let '(t_value, ctxt) := function_parameter in
              (ctxt, t_value))) ctxt transactions)
    (fun function_parameter ⇒
      let '(ctxt, transactions) := function_parameter in
      ({| atomic_transaction_batch.transactions := transactions; |}, ctxt)).

Definition outbox_message_of_outbox_message_repr
  (ctxt : Alpha_context.context)
  (function_parameter : Alpha_context.Sc_rollup.Outbox.Message.t)
  : M? (outbox_message × Alpha_context.context) :=
  let
    'Sc_rollup_outbox_message_repr.Atomic_transaction_batch {|
      Alpha_context.Sc_rollup.Outbox.Message.t.Atomic_transaction_batch.transactions
        := transactions
        |} := function_parameter in
  Error_monad.Lwt_result_syntax.op_letplus
    (transactions_batch_of_internal ctxt transactions)
    (fun function_parameter ⇒
      let '(ts, ctxt) := function_parameter in
      ((Atomic_transaction_batch ts), ctxt)).