🇿 Zk_rollup_errors.v
Translated 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.
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).
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).