Skip to main content

🇿 Zk_rollup_errors.v

Translated OCaml

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.Saturation_repr.

Module Ticket_payload_size_limit_exceeded.
  Record record : Set := Build {
    payload_size : Saturation_repr.t;
    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.

Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.zk_rollup_deposit_as_external"
      "Zk_rollup: attempted a deposit through an external op"
      "Zk_rollup: attempted a deposit through an external op"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Zk_rollup: attempted a deposit through an external op"
                  CamlinternalFormatBasics.End_of_format)
                "Zk_rollup: attempted a deposit through an external op")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Deposit_as_external" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Deposit_as_external" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.zk_rollup_invalid_deposit_amount"
      "Zk_rollup: attempted a deposit with an invalid amount"
      "Zk_rollup: attempted a deposit with an invalid amount"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Zk_rollup: attempted a deposit with an invalid amount"
                  CamlinternalFormatBasics.End_of_format)
                "Zk_rollup: attempted a deposit with an invalid amount")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_deposit_amount" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_deposit_amount" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "operation.zk_rollup_invalid_deposit_ticket"
      "Zk_rollup: attempted a deposit with an invalid ticket"
      "Zk_rollup: attempted a deposit with an invalid ticket"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Zk_rollup: attempted a deposit with an invalid ticket"
                  CamlinternalFormatBasics.End_of_format)
                "Zk_rollup: attempted a deposit with an invalid ticket")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_deposit_ticket" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_deposit_ticket" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.zk_rollup_wrong_deposit_parameters"
      "Zk_rollup: attempted a deposit with invalid parameters"
      "Zk_rollup: attempted a deposit with invalid parameters"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Zk_rollup: attempted a deposit with an invalid parameters"
                  CamlinternalFormatBasics.End_of_format)
                "Zk_rollup: attempted a deposit with an invalid parameters")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Wrong_deposit_parameters" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Wrong_deposit_parameters" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "zk_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" Saturation_repr.n_encoding)
        (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 : Saturation_repr.t × 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.Temporary
      "operation.zk_rollup_failed_verification"
      "Zk_rollup_update: failed verification"
      "Zk_rollup_update: failed verification"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The proof verification failed"
                  CamlinternalFormatBasics.End_of_format)
                "The proof verification failed"))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_verification" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_verification" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.zk_rollup_invalid_circuit" "Zk_rollup_update: invalid circuit"
      "Zk_rollup_update: invalid circuit"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid circuit in proof verification"
                  CamlinternalFormatBasics.End_of_format)
                "Invalid circuit in proof verification"))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_circuit" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_circuit" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "operation.zk_rollup_inconsistent_state_update"
      "Zk_rollup_update: inconsistent state update"
      "Zk_rollup_update: new state is of incorrect size"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Zk_rollup_update: new state is of incorrect size"
                  CamlinternalFormatBasics.End_of_format)
                "Zk_rollup_update: new state is of incorrect size")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inconsistent_state_update" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Inconsistent_state_update" unit tt) in
  Error_monad.register_error_kind Error_monad.Temporary
    "operation.zk_rollup_pending_bound"
    "Zk_rollup_update: update with fewer pending ops than allowed"
    "Zk_rollup_update: update with fewer pending ops than allowed"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Zk_rollup_update: update with fewer pending ops than allowed"
                CamlinternalFormatBasics.End_of_format)
              "Zk_rollup_update: update with fewer pending ops than allowed")))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Pending_bound" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Pending_bound" unit tt).