Skip to main content

🐆 Tx_rollup_errors_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.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_message_result_hash_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.

Inductive error_or_commitment : Set :=
| Inbox : error_or_commitment
| Commitment : error_or_commitment.

Inductive valid_path_or_hash : Set :=
| Valid_path :
  Tx_rollup_commitment_repr.Merkle_hash.t int valid_path_or_hash
| Hash : Tx_rollup_message_result_hash_repr.t valid_path_or_hash.

Module Submit_batch_burn_exceeded.
  Record record : Set := Build {
    burn : Tez_repr.t;
    limit : Tez_repr.t;
  }.
  Definition with_burn burn (r : record) :=
    Build burn r.(limit).
  Definition with_limit limit (r : record) :=
    Build r.(burn) limit.
End Submit_batch_burn_exceeded.
Definition Submit_batch_burn_exceeded := Submit_batch_burn_exceeded.record.

Module Commitment_too_early.
  Record record : Set := Build {
    provided : Tx_rollup_level_repr.t;
    expected : Tx_rollup_level_repr.t;
  }.
  Definition with_provided provided (r : record) :=
    Build provided r.(expected).
  Definition with_expected expected (r : record) :=
    Build r.(provided) expected.
End Commitment_too_early.
Definition Commitment_too_early := Commitment_too_early.record.

Module Wrong_predecessor_hash.
  Record record : Set := Build {
    provided : option Tx_rollup_commitment_repr.Hash.t;
    expected : option Tx_rollup_commitment_repr.Hash.t;
  }.
  Definition with_provided provided (r : record) :=
    Build provided r.(expected).
  Definition with_expected expected (r : record) :=
    Build r.(provided) expected.
End Wrong_predecessor_hash.
Definition Wrong_predecessor_hash := Wrong_predecessor_hash.record.

Module Wrong_message_position.
  Record record : Set := Build {
    level : Tx_rollup_level_repr.t;
    position : int;
    length : int;
  }.
  Definition with_level level (r : record) :=
    Build level r.(position) r.(length).
  Definition with_position position (r : record) :=
    Build r.(level) position r.(length).
  Definition with_length length (r : record) :=
    Build r.(level) r.(position) length.
End Wrong_message_position.
Definition Wrong_message_position := Wrong_message_position.record.

Module Wrong_path_depth.
  Record record : Set := Build {
    kind : error_or_commitment;
    provided : int;
    limit : int;
  }.
  Definition with_kind kind (r : record) :=
    Build kind r.(provided) r.(limit).
  Definition with_provided provided (r : record) :=
    Build r.(kind) provided r.(limit).
  Definition with_limit limit (r : record) :=
    Build r.(kind) r.(provided) limit.
End Wrong_path_depth.
Definition Wrong_path_depth := Wrong_path_depth.record.

Module Wrong_message_path.
  Record record : Set := Build {
    expected : Tx_rollup_inbox_repr.Merkle.root;
  }.
  Definition with_expected expected (r : record) :=
    Build expected.
End Wrong_message_path.
Definition Wrong_message_path := Wrong_message_path.record.

Module No_finalized_commitment_for_level.
  Record record : Set := Build {
    level : Tx_rollup_level_repr.t;
    window : option (Tx_rollup_level_repr.t × Tx_rollup_level_repr.t);
  }.
  Definition with_level level (r : record) :=
    Build level r.(window).
  Definition with_window window (r : record) :=
    Build r.(level) window.
End No_finalized_commitment_for_level.
Definition No_finalized_commitment_for_level :=
  No_finalized_commitment_for_level.record.

Module Cannot_reject_level.
  Record record : Set := Build {
    provided : Tx_rollup_level_repr.t;
    accepted_range : option (Tx_rollup_level_repr.t × Tx_rollup_level_repr.t);
  }.
  Definition with_provided provided (r : record) :=
    Build provided r.(accepted_range).
  Definition with_accepted_range accepted_range (r : record) :=
    Build r.(provided) accepted_range.
End Cannot_reject_level.
Definition Cannot_reject_level := Cannot_reject_level.record.

Module Wrong_rejection_hash.
  Record record : Set := Build {
    provided : Tx_rollup_message_result_hash_repr.t;
    expected : valid_path_or_hash;
  }.
  Definition with_provided provided (r : record) :=
    Build provided r.(expected).
  Definition with_expected expected (r : record) :=
    Build r.(provided) expected.
End Wrong_rejection_hash.
Definition Wrong_rejection_hash := Wrong_rejection_hash.record.

Module Ticket_payload_size_limit_exceeded.
  Record record : Set := Build {
    payload_size : int;
    limit : int;
  }.
  Definition with_payload_size payload_size (r : record) :=
    Build payload_size r.(limit).
  Definition with_limit limit (r : record) :=
    Build r.(payload_size) limit.
End Ticket_payload_size_limit_exceeded.
Definition Ticket_payload_size_limit_exceeded :=
  Ticket_payload_size_limit_exceeded.record.

Module Proof_invalid_before.
  Record record : Set := Build {
    agreed : Context_hash.t;
    provided : Context_hash.t;
  }.
  Definition with_agreed agreed (r : record) :=
    Build agreed r.(provided).
  Definition with_provided provided (r : record) :=
    Build r.(agreed) provided.
End Proof_invalid_before.
Definition Proof_invalid_before := Proof_invalid_before.record.

Definition check_path_depth
  (kind_value : error_or_commitment) (provided : int) (count_limit : int)
  : M? unit :=
  let limit := Merkle_list.max_depth count_limit in
  Error_monad.error_when (limit <i provided)
    (Build_extensible "Wrong_path_depth" Wrong_path_depth
      {| Wrong_path_depth.kind := kind_value;
        Wrong_path_depth.provided := provided; Wrong_path_depth.limit := limit;
        |}).

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.tx_rollup_submit_batch_burn_exceeded"
      "Submit batch exceeded burn limit"
      "The submit batch would exceed the burn limit, we withdraw the submit."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Tez_repr.t × Tez_repr.t) ⇒
            let '(burn, limit) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Cannot submit the batch of L2 operations as the cost ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      ") would exceed the burn limit ("
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Char_literal ")" % char
                          CamlinternalFormatBasics.End_of_format)))))
                "Cannot submit the batch of L2 operations as the cost (%a) would exceed the burn limit (%a)")
              Tez_repr.pp burn Tez_repr.pp limit))
      (Data_encoding.obj2 (Data_encoding.req None None "burn" Tez_repr.encoding)
        (Data_encoding.req None None "limit" Tez_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Submit_batch_burn_exceeded" then
            let '{|
              Submit_batch_burn_exceeded.burn := burn;
                Submit_batch_burn_exceeded.limit := limit
                |} := cast Submit_batch_burn_exceeded payload in
            Some (burn, limit)
          else None
        end)
      (fun (function_parameter : Tez_repr.t × Tez_repr.t) ⇒
        let '(burn, limit) := function_parameter in
        Build_extensible "Submit_batch_burn_exceeded" Submit_batch_burn_exceeded
          {| Submit_batch_burn_exceeded.burn := burn;
            Submit_batch_burn_exceeded.limit := limit; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_inbox_does_not_exist" "Missing transaction rollup inbox"
      "The transaction rollup does not have an inbox at this level"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Tx_rollup_repr.t × Tx_rollup_level_repr.level) ⇒
            let '(addr, level) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Transaction rollup "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " does not have an inbox at level "
                      (CamlinternalFormatBasics.Alpha
                        CamlinternalFormatBasics.End_of_format))))
                "Transaction rollup %a does not have an inbox at level %a")
              Tx_rollup_repr.pp addr Tx_rollup_level_repr.pp level))
      (Data_encoding.obj2
        (Data_encoding.req None None "tx_rollup_address" Tx_rollup_repr.encoding)
        (Data_encoding.req None None "raw_level" Tx_rollup_level_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inbox_does_not_exist" then
            let '(rollup, level) :=
              cast (Tx_rollup_repr.t × Tx_rollup_level_repr.t) payload in
            Some (rollup, level)
          else None
        end)
      (fun (function_parameter : Tx_rollup_repr.t × Tx_rollup_level_repr.level)
        ⇒
        let '(rollup, level) := function_parameter in
        Build_extensible "Inbox_does_not_exist"
          (Tx_rollup_repr.t × Tx_rollup_level_repr.level) (rollup, level)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_inbox_size_would_exceed_limit"
      ("Transaction rollup inbox" ++
        String.String "226"
          (String.String "128"
            (String.String "153" "s size would exceed the limit")))
      ("Transaction rollup inbox" ++
        String.String "226"
          (String.String "128"
            (String.String "153" "s size in bytes would exceed the limit")))
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (addr : Tx_rollup_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Adding the submitted message would make the inbox of "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " exceed the authorized size in bytes at this level"
                      CamlinternalFormatBasics.End_of_format)))
                "Adding the submitted message would make the inbox of %a exceed the authorized size in bytes at this level")
              Tx_rollup_repr.pp addr))
      (Data_encoding.obj1
        (Data_encoding.req None None "tx_rollup_address" Tx_rollup_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inbox_size_would_exceed_limit" then
            let rollup := cast Tx_rollup_repr.t payload in
            Some rollup
          else None
        end)
      (fun (rollup : Tx_rollup_repr.t) ⇒
        Build_extensible "Inbox_size_would_exceed_limit" Tx_rollup_repr.t rollup)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_inbox_count_would_exceed_limit"
      ("Transaction rollup inbox" ++
        String.String "226"
          (String.String "128"
            (String.String "153" "s message count would exceed the limit")))
      ("Transaction rollup inbox" ++
        String.String "226"
          (String.String "128"
            (String.String "153" "s message count would exceed the limit")))
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (addr : Tx_rollup_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Adding the submitted message would make the inbox of "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " exceed the authorized message count at this level"
                      CamlinternalFormatBasics.End_of_format)))
                "Adding the submitted message would make the inbox of %a exceed the authorized message count at this level")
              Tx_rollup_repr.pp addr))
      (Data_encoding.obj1
        (Data_encoding.req None None "tx_rollup_address" Tx_rollup_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inbox_count_would_exceed_limit" then
            let rollup := cast Tx_rollup_repr.t payload in
            Some rollup
          else None
        end)
      (fun (rollup : Tx_rollup_repr.t) ⇒
        Build_extensible "Inbox_count_would_exceed_limit" Tx_rollup_repr.t
          rollup) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_no_uncommitted_inbox"
      "There is no inbox awaiting a commitment."
      "There is no inbox awaiting a commitment." None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "No_uncommitted_inbox" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "No_uncommitted_inbox" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_message_size_exceeds_limit"
      "A message submitted to a transaction rollup inbox exceeds limit"
      "A message submitted to a transaction rollup inbox exceeds limit" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Message_size_exceeds_limit" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Message_size_exceeds_limit" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_too_many_inboxes"
      "Cannot create a new inbox because there are too many already"
      "Cannot create a new inbox because there are too many already" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Too_many_inboxes" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_inboxes" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_too_many_commitments" "Too many commitments"
      "Cannot create a new commitment because there are too many already" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Too_many_commitments" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_commitments" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_too_many_withdrawals" "Cannot dispatch that many withdrawals"
      "Cannot dispatch that many withdrawals" None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Too_many_withdrawals" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_withdrawals" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_wrong_batch_count"
      "This commitment has the wrong number of batches"
      "This commitment has a different number of batches than its inbox" None
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_batch_count" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Wrong_batch_count" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_commitment_too_early"
      "Cannot submit a commitment for this level yet"
      "It is not possible to submit a commitment for this level just yet." None
      (Data_encoding.obj2
        (Data_encoding.req None None "provided" Tx_rollup_level_repr.encoding)
        (Data_encoding.req None None "expected" Tx_rollup_level_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Commitment_too_early" then
            let '{|
              Commitment_too_early.provided := provided;
                Commitment_too_early.expected := expected
                |} := cast Commitment_too_early payload in
            Some (provided, expected)
          else None
        end)
      (fun (function_parameter :
        Tx_rollup_level_repr.level × Tx_rollup_level_repr.level) ⇒
        let '(provided, expected) := function_parameter in
        Build_extensible "Commitment_too_early" Commitment_too_early
          {| Commitment_too_early.provided := provided;
            Commitment_too_early.expected := expected; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_level_already_has_commitment"
      "This commitment is for a level that already has a commitment"
      "This commitment is for a level that already has a commitment" None
      (Data_encoding.obj1
        (Data_encoding.req None None "level" Tx_rollup_level_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Level_already_has_commitment" then
            let level := cast Tx_rollup_level_repr.t payload in
            Some level
          else None
        end)
      (fun (level : Tx_rollup_level_repr.level) ⇒
        Build_extensible "Level_already_has_commitment"
          Tx_rollup_level_repr.level level) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "Wrong_inbox_hash"
      "This commitment has the wrong inbox hash"
      "This commitment has a different hash than its inbox" None
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_inbox_hash" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Wrong_inbox_hash" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_bond_does_not_exist"
      "This account does not have a bond for this rollup"
      "This account does not have a bond for this rollup" None
      (Data_encoding.obj1
        (Data_encoding.req None None "contract"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Bond_does_not_exist" then
            let contract := cast Signature.public_key_hash payload in
            Some contract
          else None
        end)
      (fun (contract : Signature.public_key_hash) ⇒
        Build_extensible "Bond_does_not_exist" Signature.public_key_hash
          contract) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_bond_in_use"
      "This account's bond is in use for one or more commitments"
      "This account's bond is in use for one or more commitments" None
      (Data_encoding.obj1
        (Data_encoding.req None None "contract"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Bond_in_use" then
            let contract := cast Signature.public_key_hash payload in
            Some contract
          else None
        end)
      (fun (contract : Signature.public_key_hash) ⇒
        Build_extensible "Bond_in_use" Signature.public_key_hash contract) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_no_commitment_to_finalize" "There is no commitment to finalize"
      "There is no commitment to finalize" None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "No_commitment_to_finalize" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "No_commitment_to_finalize" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_no_commitment_to_remove" "There is no commitment to remove"
      "There is no commitment to remove" None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "No_commitment_to_remove" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "No_commitment_to_remove" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_remove_commitment_too_early"
      "It's too early to try to remove a commitment"
      "It's too early to try to remove the oldest final commitment" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Remove_commitment_too_early" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Remove_commitment_too_early" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_commitment_does_not_exist"
      "There is no commitment at the requested level"
      "There is no commitment at the requested level" None
      (Data_encoding.obj1
        (Data_encoding.req None None "provided" Tx_rollup_level_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Commitment_does_not_exist" then
            let l_value := cast Tx_rollup_level_repr.t payload in
            Some l_value
          else None
        end)
      (fun (l_value : Tx_rollup_level_repr.level) ⇒
        Build_extensible "Commitment_does_not_exist" Tx_rollup_level_repr.level
          l_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_wrong_predecessor_hash"
      "The commitment refers to a commitment that is not in the context"
      "The commitment refers to a commitment that is not in the context" None
      (Data_encoding.obj2
        (Data_encoding.req None None "provided"
          (Data_encoding.option_value Tx_rollup_commitment_repr.Hash.encoding))
        (Data_encoding.req None None "expected"
          (Data_encoding.option_value Tx_rollup_commitment_repr.Hash.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_predecessor_hash" then
            let '{|
              Wrong_predecessor_hash.provided := provided;
                Wrong_predecessor_hash.expected := expected
                |} := cast Wrong_predecessor_hash payload in
            Some (provided, expected)
          else None
        end)
      (fun (function_parameter :
        option Tx_rollup_commitment_repr.Hash.t ×
          option Tx_rollup_commitment_repr.Hash.t) ⇒
        let '(provided, expected) := function_parameter in
        Build_extensible "Wrong_predecessor_hash" Wrong_predecessor_hash
          {| Wrong_predecessor_hash.provided := provided;
            Wrong_predecessor_hash.expected := expected; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_already_exists" "Transaction rollup was already created"
      "The protocol tried to originate the same transaction rollup twice"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (addr : Tx_rollup_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Transaction rollup "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " is already used for an existing transaction rollup. This should not happen, and indicates there is a bug in the protocol. If you can, please report this bug (https://gitlab.com/tezos/tezos/-/issues.)"
                      CamlinternalFormatBasics.End_of_format)))
                "Transaction rollup %a is already used for an existing transaction rollup. This should not happen, and indicates there is a bug in the protocol. If you can, please report this bug (https://gitlab.com/tezos/tezos/-/issues.)")
              Tx_rollup_repr.pp addr))
      (Data_encoding.obj1
        (Data_encoding.req None None "rollup_address" Tx_rollup_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Tx_rollup_already_exists" then
            let rollup := cast Tx_rollup_repr.t payload in
            Some rollup
          else None
        end)
      (fun (rollup : Tx_rollup_repr.t) ⇒
        Build_extensible "Tx_rollup_already_exists" Tx_rollup_repr.t rollup) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_does_not_exist" "Transaction rollup does not exist"
      "An invalid transaction rollup address was submitted"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (addr : Tx_rollup_repr.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid transaction rollup address "
                  (CamlinternalFormatBasics.Alpha
                    CamlinternalFormatBasics.End_of_format))
                "Invalid transaction rollup address %a") Tx_rollup_repr.pp addr))
      (Data_encoding.obj1
        (Data_encoding.req None None "rollup_address" Tx_rollup_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Tx_rollup_does_not_exist" then
            let rollup := cast Tx_rollup_repr.t payload in
            Some rollup
          else None
        end)
      (fun (rollup : Tx_rollup_repr.t) ⇒
        Build_extensible "Tx_rollup_does_not_exist" Tx_rollup_repr.t rollup) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_internal_error" "An internal error occurred"
      "An internal error occurred" None
      (Data_encoding.obj1
        (Data_encoding.req None None "description" Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Internal_error" then
            let str := cast string payload in
            Some str
          else None
        end)
      (fun (str : string) ⇒ Build_extensible "Internal_error" string str) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_wrong_message_position" "Wrong message index in rejection"
      "The rejection references the {position}^th message of the inbox {l} which contains only {inbox_length} messages"
      None
      (Data_encoding.obj3
        (Data_encoding.req None None "level" Tx_rollup_level_repr.encoding)
        (Data_encoding.req None None "position" Data_encoding.int31)
        (Data_encoding.req None None "length" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_message_position" then
            let '{|
              Wrong_message_position.level := level;
                Wrong_message_position.position := position;
                Wrong_message_position.length := length
                |} := cast Wrong_message_position payload in
            Some (level, position, length)
          else None
        end)
      (fun (function_parameter : Tx_rollup_level_repr.level × int × int) ⇒
        let '(level, position, length) := function_parameter in
        Build_extensible "Wrong_message_position" Wrong_message_position
          {| Wrong_message_position.level := level;
            Wrong_message_position.position := position;
            Wrong_message_position.length := length; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_wrong_message_path_depth" "Wrong message path depth"
      "A path submitted as argument of this operation exceeds the maximum depth that can be witnessed."
      None
      (Data_encoding.obj3
        (Data_encoding.req None None "target"
          (Data_encoding.union None
            [
              Data_encoding.case_value "Inbox" None (Data_encoding.Tag 0)
                (Data_encoding.constant "inbox")
                (fun (function_parameter : error_or_commitment) ⇒
                  match function_parameter with
                  | InboxSome tt
                  | _None
                  end)
                (fun (function_parameter : unit) ⇒
                  let '_ := function_parameter in
                  Inbox);
              Data_encoding.case_value "Commitment" None (Data_encoding.Tag 1)
                (Data_encoding.constant "commitment")
                (fun (function_parameter : error_or_commitment) ⇒
                  match function_parameter with
                  | CommitmentSome tt
                  | _None
                  end)
                (fun (function_parameter : unit) ⇒
                  let '_ := function_parameter in
                  Commitment)
            ])) (Data_encoding.req None None "provided" Data_encoding.int31)
        (Data_encoding.req None None "limit" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_path_depth" then
            let '{|
              Wrong_path_depth.kind := kind_value;
                Wrong_path_depth.provided := provided;
                Wrong_path_depth.limit := limit
                |} := cast Wrong_path_depth payload in
            Some (kind_value, provided, limit)
          else None
        end)
      (fun (function_parameter : error_or_commitment × int × int) ⇒
        let '(kind_value, provided, limit) := function_parameter in
        Build_extensible "Wrong_path_depth" Wrong_path_depth
          {| Wrong_path_depth.kind := kind_value;
            Wrong_path_depth.provided := provided;
            Wrong_path_depth.limit := limit; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_wrong_message_path" "Wrong message path in rejection."
      "This rejection has sent a message and a path that does not fit the current merkle root hash in the corresponding inbox"
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "expected_merkle_root"
          Tx_rollup_inbox_repr.Merkle.root_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_message_path" then
            let '{| Wrong_message_path.expected := expected |} :=
              cast Wrong_message_path payload in
            Some expected
          else None
        end)
      (fun (expected : Tx_rollup_inbox_repr.Merkle.root) ⇒
        Build_extensible "Wrong_message_path" Wrong_message_path
          {| Wrong_message_path.expected := expected; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.tx_rollup_no_finalized_commitment_for_level"
      "Operation is about a commitment that is not yet finalized"
      "This operation must be about a finalized commitment"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Tx_rollup_level_repr.level ×
              option (Tx_rollup_level_repr.t × Tx_rollup_level_repr.t)) ⇒
            let '(level, window) := function_parameter in
            match window with
            | Some (first, last)
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal
                    "This operation is only allowed on finalized and existing commitments, but its level "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal
                        " is not in the existing and finalized window of commitments: ["
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.String_literal "; "
                            (CamlinternalFormatBasics.Alpha
                              (CamlinternalFormatBasics.String_literal "]."
                                CamlinternalFormatBasics.End_of_format)))))))
                  "This operation is only allowed on finalized and existing commitments, but its level %a is not in the existing and finalized window of commitments: [%a; %a].")
                Tx_rollup_level_repr.pp level Tx_rollup_level_repr.pp first
                Tx_rollup_level_repr.pp last
            | None
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal
                    "This operation was about level "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal
                        " but no finalized commitment exists yet."
                        CamlinternalFormatBasics.End_of_format)))
                  "This operation was about level %a but no finalized commitment exists yet.")
                Tx_rollup_level_repr.pp level
            end))
      (Data_encoding.obj2
        (Data_encoding.req None None "received" Tx_rollup_level_repr.encoding)
        (Data_encoding.req None None "commitment_head_level"
          (Data_encoding.option_value
            (Data_encoding.tup2 Tx_rollup_level_repr.encoding
              Tx_rollup_level_repr.encoding))))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "No_finalized_commitment_for_level" then
            let '{|
              No_finalized_commitment_for_level.level := level;
                No_finalized_commitment_for_level.window := window
                |} := cast No_finalized_commitment_for_level payload in
            Some (level, window)
          else None
        end)
      (fun (function_parameter :
        Tx_rollup_level_repr.level ×
          option (Tx_rollup_level_repr.t × Tx_rollup_level_repr.t)) ⇒
        let '(level, window) := function_parameter in
        Build_extensible "No_finalized_commitment_for_level"
          No_finalized_commitment_for_level
          {| No_finalized_commitment_for_level.level := level;
            No_finalized_commitment_for_level.window := window; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_withdraw_invalid_path"
      "The validation path submitted for a withdrawal is invalid"
      "The validation path submitted for a withdrawal is not valid for the given withdrawal and message index"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Withdraw_invalid_path" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Withdraw_invalid_path" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_withdrawals_invalid_path"
      "The validation path submitted for a withdrawal is invalid"
      "The validation path submitted for a withdrawal is not valid for the given withdrawal and message index"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Withdrawals_invalid_path" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Withdrawals_invalid_path" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "operation.withdrawals_already_dispatched"
      "withdrawals already dispatched"
      "The withdrawals have already been dispatched to their layer-1 beneficiary"
      None Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Withdrawals_already_dispatched" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Withdrawals_already_dispatched" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.withdraw_already_consumed" "withdraw already consumed"
      "The submitted withdraw has already been consumed"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The submitted withdraw exists but it has already been consumed earlier."
                  CamlinternalFormatBasics.End_of_format)
                "The submitted withdraw exists but it has already been consumed earlier.")))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Withdraw_already_consumed" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Withdraw_already_consumed" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_invalid_committer"
      "Committer cannot propose a commitment for this level"
      "The committer is trying to propose a commitment, but their bond is about to be slashed because a commitment they authored will be overwritten."
      None Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_committer" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_committer" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_commitment_bond_negative"
      "The number of commitments associated with an implicit account is negative"
      "A negative number of commitment is associated with an implicit account and its associated bound. This error is internal and should never happen."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (count : int) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The number of commitments "
                  (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.String_literal
                      " associated with this implicit account is negative"
                      CamlinternalFormatBasics.End_of_format)))
                "The number of commitments %d associated with this implicit account is negative")
              count))
      (Data_encoding.obj1
        (Data_encoding.req None None "count" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Commitment_bond_negative" then
            let count := cast int payload in
            Some count
          else None
        end)
      (fun (count : int) ⇒
        Build_extensible "Commitment_bond_negative" int count) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_cannot_reject_level"
      "Cannot reject a commitment at the requested level"
      "Cannot reject a commitment at the requested level" None
      (Data_encoding.obj2
        (Data_encoding.req None None "provided" Tx_rollup_level_repr.encoding)
        (Data_encoding.req None None "accepted_range"
          (Data_encoding.option_value
            (Data_encoding.obj2
              (Data_encoding.req None None "min" Tx_rollup_level_repr.encoding)
              (Data_encoding.req None None "max" Tx_rollup_level_repr.encoding)))))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Cannot_reject_level" then
            let '{|
              Cannot_reject_level.provided := provided;
                Cannot_reject_level.accepted_range := accepted_range
                |} := cast Cannot_reject_level payload in
            Some (provided, accepted_range)
          else None
        end)
      (fun (function_parameter :
        Tx_rollup_level_repr.level ×
          option (Tx_rollup_level_repr.t × Tx_rollup_level_repr.t)) ⇒
        let '(provided, accepted_range) := function_parameter in
        Build_extensible "Cannot_reject_level" Cannot_reject_level
          {| Cannot_reject_level.provided := provided;
            Cannot_reject_level.accepted_range := accepted_range; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_wrong_rejection_hashes"
      "The message result hash recomputed from the rejection argument is invalid"
      "The message result hash recomputed from the rejection argument is invalid"
      None
      (Data_encoding.obj2
        (Data_encoding.req None None "provided"
          Tx_rollup_message_result_hash_repr.encoding)
        (Data_encoding.req None None "expected"
          (Data_encoding.union None
            [
              Data_encoding.case_value "hash" None (Data_encoding.Tag 0)
                Tx_rollup_message_result_hash_repr.encoding
                (fun (function_parameter : valid_path_or_hash) ⇒
                  match function_parameter with
                  | Hash h_valueSome h_value
                  | _None
                  end)
                (fun (h_value : Tx_rollup_message_result_hash_repr.t)
                  ⇒ Hash h_value);
              Data_encoding.case_value "valid_path" None (Data_encoding.Tag 1)
                (Data_encoding.obj2
                  (Data_encoding.req None None "root"
                    Tx_rollup_commitment_repr.Merkle_hash.encoding)
                  (Data_encoding.req None None "index"
                    Data_encoding.int31))
                (fun (function_parameter : valid_path_or_hash) ⇒
                  match function_parameter with
                  | Valid_path h_value i_value
                    Some (h_value, i_value)
                  | _None
                  end)
                (fun (function_parameter :
                  Tx_rollup_commitment_repr.Merkle_hash.t ×
                    int) ⇒
                  let '(h_value, i_value) :=
                    function_parameter in
                  Valid_path h_value i_value)
            ])))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_rejection_hash" then
            let '{|
              Wrong_rejection_hash.provided := provided;
                Wrong_rejection_hash.expected := expected
                |} := cast Wrong_rejection_hash payload in
            Some (provided, expected)
          else None
        end)
      (fun (function_parameter :
        Tx_rollup_message_result_hash_repr.t × valid_path_or_hash) ⇒
        let '(provided, expected) := function_parameter in
        Build_extensible "Wrong_rejection_hash" Wrong_rejection_hash
          {| Wrong_rejection_hash.provided := provided;
            Wrong_rejection_hash.expected := expected; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_ticket_payload_size_limit_exceeded"
      "The payload of the deposited ticket exceeded the size limit"
      "The payload of the deposited ticket exceeded the size limit" None
      (Data_encoding.obj2
        (Data_encoding.req None None "payload_size" Data_encoding.int31)
        (Data_encoding.req None None "limit" Data_encoding.int31))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Ticket_payload_size_limit_exceeded" then
            let '{|
              Ticket_payload_size_limit_exceeded.payload_size := payload_size;
                Ticket_payload_size_limit_exceeded.limit := limit
                |} := cast Ticket_payload_size_limit_exceeded payload in
            Some (payload_size, limit)
          else None
        end)
      (fun (function_parameter : int × int) ⇒
        let '(payload_size, limit) := function_parameter in
        Build_extensible "Ticket_payload_size_limit_exceeded"
          Ticket_payload_size_limit_exceeded
          {| Ticket_payload_size_limit_exceeded.payload_size := payload_size;
            Ticket_payload_size_limit_exceeded.limit := limit; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_proof_undecodable" "Could not decode the proof"
      "The proof submitted as argument could not be decoded" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_undecodable" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Proof_undecodable" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_proof_failed_to_reject" "Proof failed to reject the commitment"
      "The proof verification failed and was unable to reject the commitment"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_failed_to_reject" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Proof_failed_to_reject" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_proof_produced_rejected_state"
      "Proof produced the rejected state"
      "The proof submitted did not refute the rejected commitment. The proof produced the same committed state"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_produced_rejected_state" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Proof_produced_rejected_state" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_proof_invalid_before" "Proof started from an invalid hash"
      "The proof started from a hash which is not the one agreed on (i.e. in the previous commitment)"
      None
      (Data_encoding.obj2
        (Data_encoding.req None None "agreed" Context_hash.encoding)
        (Data_encoding.req None None "provided" Context_hash.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Proof_invalid_before" then
            let '{|
              Proof_invalid_before.agreed := agreed;
                Proof_invalid_before.provided := provided
                |} := cast Proof_invalid_before payload in
            Some (agreed, provided)
          else None
        end)
      (fun (function_parameter : Context_hash.t × Context_hash.t) ⇒
        let '(agreed, provided) := function_parameter in
        Build_extensible "Proof_invalid_before" Proof_invalid_before
          {| Proof_invalid_before.agreed := agreed;
            Proof_invalid_before.provided := provided; |}) in
  Error_monad.register_error_kind Error_monad.Permanent
    "tx_rollup_no_withdrawals_to_dispatch"
    "Trying to dispatch withdrawals when none happened"
    "Cannot dispatch an empty list of withdrawals" None Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "No_withdrawals_to_dispatch" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "No_withdrawals_to_dispatch" unit tt).