✅ Validate_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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Records for the constructor parameters
Module ConstructorRecords_operation_conflict.
Module operation_conflict.
Module Operation_conflict.
Record record {existing new_operation : Set} : Set := Build {
existing : existing;
new_operation : new_operation;
}.
Arguments record : clear implicits.
Definition with_existing {t_existing t_new_operation} existing
(r : record t_existing t_new_operation) :=
Build t_existing t_new_operation existing r.(new_operation).
Definition with_new_operation {t_existing t_new_operation} new_operation
(r : record t_existing t_new_operation) :=
Build t_existing t_new_operation r.(existing) new_operation.
End Operation_conflict.
Definition Operation_conflict_skeleton := Operation_conflict.record.
End operation_conflict.
End ConstructorRecords_operation_conflict.
Import ConstructorRecords_operation_conflict.
Reserved Notation "'operation_conflict.Operation_conflict".
Inductive operation_conflict : Set :=
| Operation_conflict :
'operation_conflict.Operation_conflict → operation_conflict
where "'operation_conflict.Operation_conflict" :=
(operation_conflict.Operation_conflict_skeleton Operation_hash.t
Operation_hash.t).
Module operation_conflict.
Include ConstructorRecords_operation_conflict.operation_conflict.
Definition Operation_conflict := 'operation_conflict.Operation_conflict.
End operation_conflict.
Definition operation_conflict_encoding
: Data_encoding.encoding operation_conflict :=
Data_encoding.def "operation_conflict" (Some "Conflict error")
(Some "Conflict between two operations")
(Data_encoding.conv
(fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing;
operation_conflict.Operation_conflict.new_operation :=
new_operation
|} := function_parameter in
(existing, new_operation))
(fun (function_parameter : Operation_hash.t × Operation_hash.t) ⇒
let '(existing, new_operation) := function_parameter in
Operation_conflict
{| operation_conflict.Operation_conflict.existing := existing;
operation_conflict.Operation_conflict.new_operation :=
new_operation; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "existing" Operation_hash.encoding)
(Data_encoding.req None None "new_operation" Operation_hash.encoding))).
Module Consensus.
Module operation_conflict.
Module Operation_conflict.
Record record {existing new_operation : Set} : Set := Build {
existing : existing;
new_operation : new_operation;
}.
Arguments record : clear implicits.
Definition with_existing {t_existing t_new_operation} existing
(r : record t_existing t_new_operation) :=
Build t_existing t_new_operation existing r.(new_operation).
Definition with_new_operation {t_existing t_new_operation} new_operation
(r : record t_existing t_new_operation) :=
Build t_existing t_new_operation r.(existing) new_operation.
End Operation_conflict.
Definition Operation_conflict_skeleton := Operation_conflict.record.
End operation_conflict.
End ConstructorRecords_operation_conflict.
Import ConstructorRecords_operation_conflict.
Reserved Notation "'operation_conflict.Operation_conflict".
Inductive operation_conflict : Set :=
| Operation_conflict :
'operation_conflict.Operation_conflict → operation_conflict
where "'operation_conflict.Operation_conflict" :=
(operation_conflict.Operation_conflict_skeleton Operation_hash.t
Operation_hash.t).
Module operation_conflict.
Include ConstructorRecords_operation_conflict.operation_conflict.
Definition Operation_conflict := 'operation_conflict.Operation_conflict.
End operation_conflict.
Definition operation_conflict_encoding
: Data_encoding.encoding operation_conflict :=
Data_encoding.def "operation_conflict" (Some "Conflict error")
(Some "Conflict between two operations")
(Data_encoding.conv
(fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing;
operation_conflict.Operation_conflict.new_operation :=
new_operation
|} := function_parameter in
(existing, new_operation))
(fun (function_parameter : Operation_hash.t × Operation_hash.t) ⇒
let '(existing, new_operation) := function_parameter in
Operation_conflict
{| operation_conflict.Operation_conflict.existing := existing;
operation_conflict.Operation_conflict.new_operation :=
new_operation; |}) None
(Data_encoding.obj2
(Data_encoding.req None None "existing" Operation_hash.encoding)
(Data_encoding.req None None "new_operation" Operation_hash.encoding))).
Module Consensus.
Init function; without side-effects in Coq
Definition init_module1 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.zero_frozen_deposits" "Zero frozen deposits"
"The delegate has zero frozen deposits."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has zero frozen deposits; it is not allowed to bake/preendorse/endorse."
CamlinternalFormatBasics.End_of_format)))
"Delegate %a has zero frozen deposits; it is not allowed to bake/preendorse/endorse.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Zero_frozen_deposits" then
let delegate := cast Signature.public_key_hash payload in
Some delegate
else None
end)
(fun (delegate : Signature.public_key_hash) ⇒
Build_extensible "Zero_frozen_deposits" Signature.public_key_hash
delegate).
Error_monad.register_error_kind Error_monad.Permanent
"validate.zero_frozen_deposits" "Zero frozen deposits"
"The delegate has zero frozen deposits."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has zero frozen deposits; it is not allowed to bake/preendorse/endorse."
CamlinternalFormatBasics.End_of_format)))
"Delegate %a has zero frozen deposits; it is not allowed to bake/preendorse/endorse.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Zero_frozen_deposits" then
let delegate := cast Signature.public_key_hash payload in
Some delegate
else None
end)
(fun (delegate : Signature.public_key_hash) ⇒
Build_extensible "Zero_frozen_deposits" Signature.public_key_hash
delegate).
This type is only used in consensus operation errors to make
them more informative.
Inductive consensus_operation_kind : Set :=
| Preendorsement : consensus_operation_kind
| Endorsement : consensus_operation_kind
| Grandparent_endorsement : consensus_operation_kind
| Dal_attestation : consensus_operation_kind.
Definition consensus_operation_kind_encoding
: Data_encoding.encoding consensus_operation_kind :=
Data_encoding.string_enum
[
("Preendorsement", Preendorsement);
("Endorsement", Endorsement);
("Grandparent_endorsement", Grandparent_endorsement);
("Dal_attestation", Dal_attestation)
].
Definition consensus_operation_kind_pp
(fmt : Format.formatter) (function_parameter : consensus_operation_kind)
: unit :=
match function_parameter with
| Preendorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Preendorsement"
CamlinternalFormatBasics.End_of_format) "Preendorsement")
| Endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Endorsement"
CamlinternalFormatBasics.End_of_format) "Endorsement")
| Grandparent_endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Grandparent endorsement"
CamlinternalFormatBasics.End_of_format) "Grandparent endorsement")
| Dal_attestation ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Dal_attestation"
CamlinternalFormatBasics.End_of_format) "Dal_attestation")
end.
| Preendorsement : consensus_operation_kind
| Endorsement : consensus_operation_kind
| Grandparent_endorsement : consensus_operation_kind
| Dal_attestation : consensus_operation_kind.
Definition consensus_operation_kind_encoding
: Data_encoding.encoding consensus_operation_kind :=
Data_encoding.string_enum
[
("Preendorsement", Preendorsement);
("Endorsement", Endorsement);
("Grandparent_endorsement", Grandparent_endorsement);
("Dal_attestation", Dal_attestation)
].
Definition consensus_operation_kind_pp
(fmt : Format.formatter) (function_parameter : consensus_operation_kind)
: unit :=
match function_parameter with
| Preendorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Preendorsement"
CamlinternalFormatBasics.End_of_format) "Preendorsement")
| Endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Endorsement"
CamlinternalFormatBasics.End_of_format) "Endorsement")
| Grandparent_endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Grandparent endorsement"
CamlinternalFormatBasics.End_of_format) "Grandparent endorsement")
| Dal_attestation ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Dal_attestation"
CamlinternalFormatBasics.End_of_format) "Dal_attestation")
end.
Errors for preendorsements and endorsements.
Module Consensus_operation_for_old_level.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_old_level.
Definition Consensus_operation_for_old_level :=
Consensus_operation_for_old_level.record.
Module Consensus_operation_for_future_level.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_future_level.
Definition Consensus_operation_for_future_level :=
Consensus_operation_for_future_level.record.
Module Consensus_operation_for_old_round.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_old_round.
Definition Consensus_operation_for_old_round :=
Consensus_operation_for_old_round.record.
Module Consensus_operation_for_future_round.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_future_round.
Definition Consensus_operation_for_future_round :=
Consensus_operation_for_future_round.record.
Module Wrong_consensus_operation_branch.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Block_hash.t;
provided : Block_hash.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Wrong_consensus_operation_branch.
Definition Wrong_consensus_operation_branch :=
Wrong_consensus_operation_branch.record.
Module Wrong_payload_hash_for_consensus_operation.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Block_payload_hash.t;
provided : Block_payload_hash.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Wrong_payload_hash_for_consensus_operation.
Definition Wrong_payload_hash_for_consensus_operation :=
Wrong_payload_hash_for_consensus_operation.record.
Module Preendorsement_round_too_high.
Record record : Set := Build {
block_round : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_block_round block_round (r : record) :=
Build block_round r.(provided).
Definition with_provided provided (r : record) :=
Build r.(block_round) provided.
End Preendorsement_round_too_high.
Definition Preendorsement_round_too_high :=
Preendorsement_round_too_high.record.
Module Wrong_slot_used_for_consensus_operation.
Record record : Set := Build {
kind : consensus_operation_kind;
}.
Definition with_kind kind (r : record) :=
Build kind.
End Wrong_slot_used_for_consensus_operation.
Definition Wrong_slot_used_for_consensus_operation :=
Wrong_slot_used_for_consensus_operation.record.
Module Conflicting_consensus_operation.
Record record : Set := Build {
kind : consensus_operation_kind;
conflict : operation_conflict;
}.
Definition with_kind kind (r : record) :=
Build kind r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(kind) conflict.
End Conflicting_consensus_operation.
Definition Conflicting_consensus_operation :=
Conflicting_consensus_operation.record.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_old_level.
Definition Consensus_operation_for_old_level :=
Consensus_operation_for_old_level.record.
Module Consensus_operation_for_future_level.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Raw_level.t;
provided : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_future_level.
Definition Consensus_operation_for_future_level :=
Consensus_operation_for_future_level.record.
Module Consensus_operation_for_old_round.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_old_round.
Definition Consensus_operation_for_old_round :=
Consensus_operation_for_old_round.record.
Module Consensus_operation_for_future_round.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Consensus_operation_for_future_round.
Definition Consensus_operation_for_future_round :=
Consensus_operation_for_future_round.record.
Module Wrong_consensus_operation_branch.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Block_hash.t;
provided : Block_hash.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Wrong_consensus_operation_branch.
Definition Wrong_consensus_operation_branch :=
Wrong_consensus_operation_branch.record.
Module Wrong_payload_hash_for_consensus_operation.
Record record : Set := Build {
kind : consensus_operation_kind;
expected : Block_payload_hash.t;
provided : Block_payload_hash.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(expected) r.(provided).
Definition with_expected expected (r : record) :=
Build r.(kind) expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(kind) r.(expected) provided.
End Wrong_payload_hash_for_consensus_operation.
Definition Wrong_payload_hash_for_consensus_operation :=
Wrong_payload_hash_for_consensus_operation.record.
Module Preendorsement_round_too_high.
Record record : Set := Build {
block_round : Alpha_context.Round.t;
provided : Alpha_context.Round.t;
}.
Definition with_block_round block_round (r : record) :=
Build block_round r.(provided).
Definition with_provided provided (r : record) :=
Build r.(block_round) provided.
End Preendorsement_round_too_high.
Definition Preendorsement_round_too_high :=
Preendorsement_round_too_high.record.
Module Wrong_slot_used_for_consensus_operation.
Record record : Set := Build {
kind : consensus_operation_kind;
}.
Definition with_kind kind (r : record) :=
Build kind.
End Wrong_slot_used_for_consensus_operation.
Definition Wrong_slot_used_for_consensus_operation :=
Wrong_slot_used_for_consensus_operation.record.
Module Conflicting_consensus_operation.
Record record : Set := Build {
kind : consensus_operation_kind;
conflict : operation_conflict;
}.
Definition with_kind kind (r : record) :=
Build kind r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(kind) conflict.
End Conflicting_consensus_operation.
Definition Conflicting_consensus_operation :=
Conflicting_consensus_operation.record.
Init function; without side-effects in Coq
Definition init_module2 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Outdated
"validate.consensus_operation_for_old_level"
"Consensus operation for old level" "Consensus operation for old level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for old level (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for old level (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided"
Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_level" then
let '{|
Consensus_operation_for_old_level.kind := kind_value;
Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided
|} := cast Consensus_operation_for_old_level payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_level"
Consensus_operation_for_old_level
{| Consensus_operation_for_old_level.kind := kind_value;
Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.consensus_operation_for_future_level"
"Consensus operation for future level"
"Consensus operation for future level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for future level (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for future level (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided"
Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_level" then
let '{|
Consensus_operation_for_future_level.kind := kind_value;
Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided
|} := cast Consensus_operation_for_future_level payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_level"
Consensus_operation_for_future_level
{| Consensus_operation_for_future_level.kind := kind_value;
Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.consensus_operation_for_old_round"
"Consensus operation for old round" "Consensus operation for old round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for old round (expected_min: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for old round (expected_min: %a, provided: %a).")
consensus_operation_kind_pp kind_value Alpha_context.Round.pp
expected Alpha_context.Round.pp provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected_min"
Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_round" then
let '{|
Consensus_operation_for_old_round.kind := kind_value;
Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided
|} := cast Consensus_operation_for_old_round payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_round"
Consensus_operation_for_old_round
{| Consensus_operation_for_old_round.kind := kind_value;
Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.consensus_operation_for_future_round"
"Consensus operation for future round"
"Consensus operation for future round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for future round (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for future round (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value Alpha_context.Round.pp
expected Alpha_context.Round.pp provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected_max"
Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_round" then
let '{|
Consensus_operation_for_future_round.kind := kind_value;
Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided
|} := cast Consensus_operation_for_future_round payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_round"
Consensus_operation_for_future_round
{| Consensus_operation_for_future_round.kind := kind_value;
Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.wrong_consensus_operation_branch"
"Wrong consensus operation branch"
"Trying to include an endorsement or preendorsement which points to the wrong block. It should be the predecessor for preendorsements and the grandfather for endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Block_hash.t × Block_hash.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" with wrong branch (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a with wrong branch (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value Block_hash.pp expected
Block_hash.pp provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected" Block_hash.encoding)
(Data_encoding.req None None "provided" Block_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_consensus_operation_branch" then
let '{|
Wrong_consensus_operation_branch.kind := kind_value;
Wrong_consensus_operation_branch.expected := expected;
Wrong_consensus_operation_branch.provided := provided
|} := cast Wrong_consensus_operation_branch payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Block_hash.t × Block_hash.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Wrong_consensus_operation_branch"
Wrong_consensus_operation_branch
{| Wrong_consensus_operation_branch.kind := kind_value;
Wrong_consensus_operation_branch.expected := expected;
Wrong_consensus_operation_branch.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.wrong_payload_hash_for_consensus_operation"
"Wrong payload hash for consensus operation"
"Wrong payload hash for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Block_payload_hash.t ×
Block_payload_hash.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" with wrong payload hash (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a with wrong payload hash (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value
Block_payload_hash.pp_short expected Block_payload_hash.pp_short
provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected" Block_payload_hash.encoding)
(Data_encoding.req None None "provided" Block_payload_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_payload_hash_for_consensus_operation" then
let '{|
Wrong_payload_hash_for_consensus_operation.kind := kind_value;
Wrong_payload_hash_for_consensus_operation.expected :=
expected;
Wrong_payload_hash_for_consensus_operation.provided :=
provided
|} :=
cast Wrong_payload_hash_for_consensus_operation payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Block_payload_hash.t × Block_payload_hash.t)
⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Wrong_payload_hash_for_consensus_operation"
Wrong_payload_hash_for_consensus_operation
{| Wrong_payload_hash_for_consensus_operation.kind := kind_value;
Wrong_payload_hash_for_consensus_operation.expected := expected;
Wrong_payload_hash_for_consensus_operation.provided := provided;
|}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.unexpected_preendorsement_in_block"
"Unexpected preendorsement in block"
"Unexpected preendorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected preendorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected preendorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_preendorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_preendorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.unexpected_endorsement_in_block"
"Unexpected endorsement in block" "Unexpected endorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected endorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected endorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_endorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_endorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.preendorsement_round_too_high" "Preendorsement round too high"
"Preendorsement round too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(block_round, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Preendorsement round too high (block_round: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Preendorsement round too high (block_round: %a, provided: %a).")
Alpha_context.Round.pp block_round Alpha_context.Round.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "block_round"
Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Preendorsement_round_too_high" then
let '{|
Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided
|} := cast Preendorsement_round_too_high payload in
Some (block_round, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(block_round, provided) := function_parameter in
Build_extensible "Preendorsement_round_too_high"
Preendorsement_round_too_high
{| Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.wrong_slot_for_consensus_operation"
"Wrong slot for consensus operation"
"Wrong slot used for a preendorsement or endorsement."
(Some
(fun (ppf : Format.formatter) ⇒
fun (kind_value : consensus_operation_kind) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong slot used for a "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Wrong slot used for a %a.") consensus_operation_kind_pp
kind_value))
(Data_encoding.obj1
(Data_encoding.req None None "kind" consensus_operation_kind_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_slot_used_for_consensus_operation" then
let '{|
Wrong_slot_used_for_consensus_operation.kind := kind_value
|} := cast Wrong_slot_used_for_consensus_operation payload in
Some kind_value
else None
end)
(fun (kind_value : consensus_operation_kind) ⇒
Build_extensible "Wrong_slot_used_for_consensus_operation"
Wrong_slot_used_for_consensus_operation
{| Wrong_slot_used_for_consensus_operation.kind := kind_value; |})
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.double_inclusion_of_consensus_operation"
"Double inclusion of consensus operation"
"Double inclusion of consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × operation_conflict) ⇒
let
'(kind_value,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing;
operation_conflict.Operation_conflict.new_operation :=
new_operation
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" conflicts with existing "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))
"%a operation %a conflicts with existing %a")
consensus_operation_kind_pp kind_value Operation_hash.pp
new_operation Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_consensus_operation" then
let '{|
Conflicting_consensus_operation.kind := kind_value;
Conflicting_consensus_operation.conflict := conflict
|} := cast Conflicting_consensus_operation payload in
Some (kind_value, conflict)
else None
end)
(fun (function_parameter :
consensus_operation_kind × operation_conflict) ⇒
let '(kind_value, conflict) := function_parameter in
Build_extensible "Conflicting_consensus_operation"
Conflicting_consensus_operation
{| Conflicting_consensus_operation.kind := kind_value;
Conflicting_consensus_operation.conflict := conflict; |}) in
Error_monad.register_error_kind Error_monad.Branch
"validate.consensus_operation_not_allowed"
"Consensus operation not allowed" "Consensus operation not allowed."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Validation of consensus operation if forbidden "
CamlinternalFormatBasics.End_of_format)
"Validation of consensus operation if forbidden ")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_not_allowed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Consensus_operation_not_allowed" unit tt).
End Consensus.
Module Voting.
Module Wrong_voting_period_index.
Record record : Set := Build {
expected : int32;
provided : int32;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_voting_period_index.
Definition Wrong_voting_period_index := Wrong_voting_period_index.record.
Module Wrong_voting_period_kind.
Record record : Set := Build {
current : Alpha_context.Voting_period.kind;
expected : list Alpha_context.Voting_period.kind;
}.
Definition with_current current (r : record) :=
Build current r.(expected).
Definition with_expected expected (r : record) :=
Build r.(current) expected.
End Wrong_voting_period_kind.
Definition Wrong_voting_period_kind := Wrong_voting_period_kind.record.
Module Proposals_contain_duplicate.
Record record : Set := Build {
proposal : Protocol_hash.t;
}.
Definition with_proposal proposal (r : record) :=
Build proposal.
End Proposals_contain_duplicate.
Definition Proposals_contain_duplicate := Proposals_contain_duplicate.record.
Module Already_proposed.
Record record : Set := Build {
proposal : Protocol_hash.t;
}.
Definition with_proposal proposal (r : record) :=
Build proposal.
End Already_proposed.
Definition Already_proposed := Already_proposed.record.
Module Too_many_proposals.
Record record : Set := Build {
previous_count : int;
operation_count : int;
}.
Definition with_previous_count previous_count (r : record) :=
Build previous_count r.(operation_count).
Definition with_operation_count operation_count (r : record) :=
Build r.(previous_count) operation_count.
End Too_many_proposals.
Definition Too_many_proposals := Too_many_proposals.record.
Module Ballot_for_wrong_proposal.
Record record : Set := Build {
current : Protocol_hash.t;
submitted : Protocol_hash.t;
}.
Definition with_current current (r : record) :=
Build current r.(submitted).
Definition with_submitted submitted (r : record) :=
Build r.(current) submitted.
End Ballot_for_wrong_proposal.
Definition Ballot_for_wrong_proposal := Ballot_for_wrong_proposal.record.
let '_ :=
Error_monad.register_error_kind Error_monad.Outdated
"validate.consensus_operation_for_old_level"
"Consensus operation for old level" "Consensus operation for old level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for old level (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for old level (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided"
Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_level" then
let '{|
Consensus_operation_for_old_level.kind := kind_value;
Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided
|} := cast Consensus_operation_for_old_level payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_level"
Consensus_operation_for_old_level
{| Consensus_operation_for_old_level.kind := kind_value;
Consensus_operation_for_old_level.expected := expected;
Consensus_operation_for_old_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.consensus_operation_for_future_level"
"Consensus operation for future level"
"Consensus operation for future level."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for future level (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for future level (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value
Alpha_context.Raw_level.pp expected Alpha_context.Raw_level.pp
provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected"
Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "provided"
Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_level" then
let '{|
Consensus_operation_for_future_level.kind := kind_value;
Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided
|} := cast Consensus_operation_for_future_level payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_level"
Consensus_operation_for_future_level
{| Consensus_operation_for_future_level.kind := kind_value;
Consensus_operation_for_future_level.expected := expected;
Consensus_operation_for_future_level.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.consensus_operation_for_old_round"
"Consensus operation for old round" "Consensus operation for old round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for old round (expected_min: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for old round (expected_min: %a, provided: %a).")
consensus_operation_kind_pp kind_value Alpha_context.Round.pp
expected Alpha_context.Round.pp provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected_min"
Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_old_round" then
let '{|
Consensus_operation_for_old_round.kind := kind_value;
Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided
|} := cast Consensus_operation_for_old_round payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_old_round"
Consensus_operation_for_old_round
{| Consensus_operation_for_old_round.kind := kind_value;
Consensus_operation_for_old_round.expected := expected;
Consensus_operation_for_old_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.consensus_operation_for_future_round"
"Consensus operation for future round"
"Consensus operation for future round."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for future round (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a for future round (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value Alpha_context.Round.pp
expected Alpha_context.Round.pp provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected_max"
Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_for_future_round" then
let '{|
Consensus_operation_for_future_round.kind := kind_value;
Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided
|} := cast Consensus_operation_for_future_round payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Alpha_context.Round.t ×
Alpha_context.Round.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Consensus_operation_for_future_round"
Consensus_operation_for_future_round
{| Consensus_operation_for_future_round.kind := kind_value;
Consensus_operation_for_future_round.expected := expected;
Consensus_operation_for_future_round.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.wrong_consensus_operation_branch"
"Wrong consensus operation branch"
"Trying to include an endorsement or preendorsement which points to the wrong block. It should be the predecessor for preendorsements and the grandfather for endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Block_hash.t × Block_hash.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" with wrong branch (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a with wrong branch (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value Block_hash.pp expected
Block_hash.pp provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected" Block_hash.encoding)
(Data_encoding.req None None "provided" Block_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_consensus_operation_branch" then
let '{|
Wrong_consensus_operation_branch.kind := kind_value;
Wrong_consensus_operation_branch.expected := expected;
Wrong_consensus_operation_branch.provided := provided
|} := cast Wrong_consensus_operation_branch payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Block_hash.t × Block_hash.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Wrong_consensus_operation_branch"
Wrong_consensus_operation_branch
{| Wrong_consensus_operation_branch.kind := kind_value;
Wrong_consensus_operation_branch.expected := expected;
Wrong_consensus_operation_branch.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.wrong_payload_hash_for_consensus_operation"
"Wrong payload hash for consensus operation"
"Wrong payload hash for consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × Block_payload_hash.t ×
Block_payload_hash.t) ⇒
let '(kind_value, expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" with wrong payload hash (expected: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format))))))
"%a with wrong payload hash (expected: %a, provided: %a).")
consensus_operation_kind_pp kind_value
Block_payload_hash.pp_short expected Block_payload_hash.pp_short
provided))
(Data_encoding.obj3
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "expected" Block_payload_hash.encoding)
(Data_encoding.req None None "provided" Block_payload_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_payload_hash_for_consensus_operation" then
let '{|
Wrong_payload_hash_for_consensus_operation.kind := kind_value;
Wrong_payload_hash_for_consensus_operation.expected :=
expected;
Wrong_payload_hash_for_consensus_operation.provided :=
provided
|} :=
cast Wrong_payload_hash_for_consensus_operation payload in
Some (kind_value, expected, provided)
else None
end)
(fun (function_parameter :
consensus_operation_kind × Block_payload_hash.t × Block_payload_hash.t)
⇒
let '(kind_value, expected, provided) := function_parameter in
Build_extensible "Wrong_payload_hash_for_consensus_operation"
Wrong_payload_hash_for_consensus_operation
{| Wrong_payload_hash_for_consensus_operation.kind := kind_value;
Wrong_payload_hash_for_consensus_operation.expected := expected;
Wrong_payload_hash_for_consensus_operation.provided := provided;
|}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.unexpected_preendorsement_in_block"
"Unexpected preendorsement in block"
"Unexpected preendorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected preendorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected preendorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_preendorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_preendorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.unexpected_endorsement_in_block"
"Unexpected endorsement in block" "Unexpected endorsement in block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unexpected endorsement in block."
CamlinternalFormatBasics.End_of_format)
"Unexpected endorsement in block."))) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_endorsement_in_block" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unexpected_endorsement_in_block" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.preendorsement_round_too_high" "Preendorsement round too high"
"Preendorsement round too high."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(block_round, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Preendorsement round too high (block_round: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ", provided: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))
"Preendorsement round too high (block_round: %a, provided: %a).")
Alpha_context.Round.pp block_round Alpha_context.Round.pp
provided))
(Data_encoding.obj2
(Data_encoding.req None None "block_round"
Alpha_context.Round.encoding)
(Data_encoding.req None None "provided" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Preendorsement_round_too_high" then
let '{|
Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided
|} := cast Preendorsement_round_too_high payload in
Some (block_round, provided)
else None
end)
(fun (function_parameter :
Alpha_context.Round.t × Alpha_context.Round.t) ⇒
let '(block_round, provided) := function_parameter in
Build_extensible "Preendorsement_round_too_high"
Preendorsement_round_too_high
{| Preendorsement_round_too_high.block_round := block_round;
Preendorsement_round_too_high.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.wrong_slot_for_consensus_operation"
"Wrong slot for consensus operation"
"Wrong slot used for a preendorsement or endorsement."
(Some
(fun (ppf : Format.formatter) ⇒
fun (kind_value : consensus_operation_kind) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong slot used for a "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Wrong slot used for a %a.") consensus_operation_kind_pp
kind_value))
(Data_encoding.obj1
(Data_encoding.req None None "kind" consensus_operation_kind_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_slot_used_for_consensus_operation" then
let '{|
Wrong_slot_used_for_consensus_operation.kind := kind_value
|} := cast Wrong_slot_used_for_consensus_operation payload in
Some kind_value
else None
end)
(fun (kind_value : consensus_operation_kind) ⇒
Build_extensible "Wrong_slot_used_for_consensus_operation"
Wrong_slot_used_for_consensus_operation
{| Wrong_slot_used_for_consensus_operation.kind := kind_value; |})
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.double_inclusion_of_consensus_operation"
"Double inclusion of consensus operation"
"Double inclusion of consensus operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
consensus_operation_kind × operation_conflict) ⇒
let
'(kind_value,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing;
operation_conflict.Operation_conflict.new_operation :=
new_operation
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" conflicts with existing "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)))))
"%a operation %a conflicts with existing %a")
consensus_operation_kind_pp kind_value Operation_hash.pp
new_operation Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "kind" consensus_operation_kind_encoding)
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_consensus_operation" then
let '{|
Conflicting_consensus_operation.kind := kind_value;
Conflicting_consensus_operation.conflict := conflict
|} := cast Conflicting_consensus_operation payload in
Some (kind_value, conflict)
else None
end)
(fun (function_parameter :
consensus_operation_kind × operation_conflict) ⇒
let '(kind_value, conflict) := function_parameter in
Build_extensible "Conflicting_consensus_operation"
Conflicting_consensus_operation
{| Conflicting_consensus_operation.kind := kind_value;
Conflicting_consensus_operation.conflict := conflict; |}) in
Error_monad.register_error_kind Error_monad.Branch
"validate.consensus_operation_not_allowed"
"Consensus operation not allowed" "Consensus operation not allowed."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Validation of consensus operation if forbidden "
CamlinternalFormatBasics.End_of_format)
"Validation of consensus operation if forbidden ")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Consensus_operation_not_allowed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Consensus_operation_not_allowed" unit tt).
End Consensus.
Module Voting.
Module Wrong_voting_period_index.
Record record : Set := Build {
expected : int32;
provided : int32;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Wrong_voting_period_index.
Definition Wrong_voting_period_index := Wrong_voting_period_index.record.
Module Wrong_voting_period_kind.
Record record : Set := Build {
current : Alpha_context.Voting_period.kind;
expected : list Alpha_context.Voting_period.kind;
}.
Definition with_current current (r : record) :=
Build current r.(expected).
Definition with_expected expected (r : record) :=
Build r.(current) expected.
End Wrong_voting_period_kind.
Definition Wrong_voting_period_kind := Wrong_voting_period_kind.record.
Module Proposals_contain_duplicate.
Record record : Set := Build {
proposal : Protocol_hash.t;
}.
Definition with_proposal proposal (r : record) :=
Build proposal.
End Proposals_contain_duplicate.
Definition Proposals_contain_duplicate := Proposals_contain_duplicate.record.
Module Already_proposed.
Record record : Set := Build {
proposal : Protocol_hash.t;
}.
Definition with_proposal proposal (r : record) :=
Build proposal.
End Already_proposed.
Definition Already_proposed := Already_proposed.record.
Module Too_many_proposals.
Record record : Set := Build {
previous_count : int;
operation_count : int;
}.
Definition with_previous_count previous_count (r : record) :=
Build previous_count r.(operation_count).
Definition with_operation_count operation_count (r : record) :=
Build r.(previous_count) operation_count.
End Too_many_proposals.
Definition Too_many_proposals := Too_many_proposals.record.
Module Ballot_for_wrong_proposal.
Record record : Set := Build {
current : Protocol_hash.t;
submitted : Protocol_hash.t;
}.
Definition with_current current (r : record) :=
Build current r.(submitted).
Definition with_submitted submitted (r : record) :=
Build r.(current) submitted.
End Ballot_for_wrong_proposal.
Definition Ballot_for_wrong_proposal := Ballot_for_wrong_proposal.record.
Init function; without side-effects in Coq
Definition init_module3 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.wrong_voting_period_index"
"Wrong voting period index"
"The voting operation contains a voting period index different from the current one."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int32 × int32) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The voting operation is meant for voting period "
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
", whereas the current period is "
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"The voting operation is meant for voting period %ld, whereas the current period is %ld.")
provided expected))
(Data_encoding.obj2
(Data_encoding.req None None "current_index" Data_encoding.int32_value)
(Data_encoding.req None None "provided_index"
Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_voting_period_index" then
let '{|
Wrong_voting_period_index.expected := expected;
Wrong_voting_period_index.provided := provided
|} := cast Wrong_voting_period_index payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : int32 × int32) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_voting_period_index" Wrong_voting_period_index
{| Wrong_voting_period_index.expected := expected;
Wrong_voting_period_index.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.wrong_voting_period_kind" "Wrong voting period kind"
"The voting operation is incompatible the current voting period kind."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Voting_period.kind ×
list Alpha_context.Voting_period.kind) ⇒
let '(current, expected) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The voting operation is only valid during a "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" voting period, but we are currently in a "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " period."
CamlinternalFormatBasics.End_of_format)))))
"The voting operation is only valid during a %a voting period, but we are currently in a %a period.")
(Format.pp_print_list
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal " or "
CamlinternalFormatBasics.End_of_format) " or ")))
Alpha_context.Voting_period.pp_kind) expected
Alpha_context.Voting_period.pp_kind current))
(Data_encoding.obj2
(Data_encoding.req None None "current"
Alpha_context.Voting_period.kind_encoding)
(Data_encoding.req None None "expected"
(Data_encoding.list_value None
Alpha_context.Voting_period.kind_encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_voting_period_kind" then
let '{|
Wrong_voting_period_kind.current := current;
Wrong_voting_period_kind.expected := expected
|} := cast Wrong_voting_period_kind payload in
Some (current, expected)
else None
end)
(fun (function_parameter :
Alpha_context.Voting_period.kind ×
list Alpha_context.Voting_period.kind) ⇒
let '(current, expected) := function_parameter in
Build_extensible "Wrong_voting_period_kind" Wrong_voting_period_kind
{| Wrong_voting_period_kind.current := current;
Wrong_voting_period_kind.expected := expected; |}) in
let description := "The delegate is not in the vote listings." in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.source_not_in_vote_listings"
"Source not in vote listings" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Source_not_in_vote_listings" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Source_not_in_vote_listings" unit tt) in
let description := "Proposal list cannot be empty." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.empty_proposals" "Empty proposals" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Empty_proposals" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Empty_proposals" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.proposals_contain_duplicate"
"Proposals contain duplicate"
"The list of proposals contains a duplicate element."
(Some
(fun (ppf : Format.formatter) ⇒
fun (proposal : Protocol_hash.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The list of proposals contains multiple occurrences of the proposal "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"The list of proposals contains multiple occurrences of the proposal %a.")
Protocol_hash.pp proposal))
(Data_encoding.obj1
(Data_encoding.req None None "proposal" Protocol_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proposals_contain_duplicate" then
let '{| Proposals_contain_duplicate.proposal := proposal |} :=
cast Proposals_contain_duplicate payload in
Some proposal
else None
end)
(fun (proposal : Protocol_hash.t) ⇒
Build_extensible "Proposals_contain_duplicate"
Proposals_contain_duplicate
{| Proposals_contain_duplicate.proposal := proposal; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.already_proposed" "Already proposed"
"The delegate has already submitted one of the operation's proposals."
(Some
(fun (ppf : Format.formatter) ⇒
fun (proposal : Protocol_hash.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The delegate has already submitted the proposal "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"The delegate has already submitted the proposal %a.")
Protocol_hash.pp proposal))
(Data_encoding.obj1
(Data_encoding.req None None "proposal" Protocol_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_proposed" then
let '{| Already_proposed.proposal := proposal |} :=
cast Already_proposed payload in
Some proposal
else None
end)
(fun (proposal : Protocol_hash.t) ⇒
Build_extensible "Already_proposed" Already_proposed
{| Already_proposed.proposal := proposal; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.conflict_too_many_proposals"
"Conflict too many proposals"
"The delegate exceeded the maximum number of allowed proposals due to, among others, previous Proposals operations in the current block/mempool."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(previous_count, operation_count) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The delegate cannot submit too many protocol proposals: it currently voted for "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" and is trying to vote for "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " more."
CamlinternalFormatBasics.End_of_format)))))
"The delegate cannot submit too many protocol proposals: it currently voted for %d and is trying to vote for %d more.")
previous_count operation_count))
(Data_encoding.obj2
(Data_encoding.req None None "previous_count" Data_encoding.int8)
(Data_encoding.req None None "operation_count" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_many_proposals" then
let '{|
Too_many_proposals.previous_count := previous_count;
Too_many_proposals.operation_count := operation_count
|} := cast Too_many_proposals payload in
Some (previous_count, operation_count)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(previous_count, operation_count) := function_parameter in
Build_extensible "Too_many_proposals" Too_many_proposals
{| Too_many_proposals.previous_count := previous_count;
Too_many_proposals.operation_count := operation_count; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.conflicting_proposals" "Conflicting proposals"
"The current block/mempool already contains a testnest dictator proposals operation, so it cannot have any other voting operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The current block/mempool already contains a conflicting operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"The current block/mempool already contains a conflicting operation %a.")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_proposals" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_proposals" operation_conflict conflict)
in
let description :=
"A testnet dictator cannot submit more than one proposal at a time." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.testnet_dictator_multiple_proposals"
"Testnet dictator multiple proposals" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Testnet_dictator_multiple_proposals" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Testnet_dictator_multiple_proposals" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.proposals_from_unregistered_delegate"
"Proposals from an unregistered delegate"
"Cannot submit proposals with an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot submit proposals with public key hash "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" (unregistered delegate)."
CamlinternalFormatBasics.End_of_format)))
"Cannot submit proposals with public key hash %a (unregistered delegate).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Proposals_from_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Proposals_from_unregistered_delegate"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.ballot_for_wrong_proposal"
"Ballot for wrong proposal"
"Ballot provided for a proposal that is not the current one."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Protocol_hash.t × Protocol_hash.t) ⇒
let '(current, submitted) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Ballot provided for proposal "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" whereas the current proposal is "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Ballot provided for proposal %a whereas the current proposal is %a.")
Protocol_hash.pp submitted Protocol_hash.pp current))
(Data_encoding.obj2
(Data_encoding.req None None "current_proposal" Protocol_hash.encoding)
(Data_encoding.req None None "ballot_proposal" Protocol_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Ballot_for_wrong_proposal" then
let '{|
Ballot_for_wrong_proposal.current := current;
Ballot_for_wrong_proposal.submitted := submitted
|} := cast Ballot_for_wrong_proposal payload in
Some (current, submitted)
else None
end)
(fun (function_parameter : Protocol_hash.t × Protocol_hash.t) ⇒
let '(current, submitted) := function_parameter in
Build_extensible "Ballot_for_wrong_proposal" Ballot_for_wrong_proposal
{| Ballot_for_wrong_proposal.current := current;
Ballot_for_wrong_proposal.submitted := submitted; |}) in
let description :=
"The delegate has already submitted a ballot for the current voting period."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.already_submitted_a_ballot"
"Already submitted a ballot" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_submitted_a_ballot" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Already_submitted_a_ballot" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.ballot_from_unregistered_delegate"
"Ballot from an unregistered delegate"
"Cannot cast a ballot for an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot cast a ballot for public key hash "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" (unregistered delegate)."
CamlinternalFormatBasics.End_of_format)))
"Cannot cast a ballot for public key hash %a (unregistered delegate).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Ballot_from_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Ballot_from_unregistered_delegate"
Signature.public_key_hash c_value) in
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.conflicting_ballot" "Conflicting ballot"
"The delegate has already submitted a ballot in a previously validated operation of the current block or mempool."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The delegate has already submitted a ballot in the previously validated operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" of the current block or mempool."
CamlinternalFormatBasics.End_of_format)))
"The delegate has already submitted a ballot in the previously validated operation %a of the current block or mempool.")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_ballot" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_ballot" operation_conflict conflict).
End Voting.
Module Anonymous.
Module Invalid_activation.
Record record : Set := Build {
pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t);
}.
Definition with_pkh pkh (r : record) :=
Build pkh.
End Invalid_activation.
Definition Invalid_activation := Invalid_activation.record.
Module Conflicting_activation.
Record record : Set := Build {
edpkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t);
conflict : operation_conflict;
}.
Definition with_edpkh edpkh (r : record) :=
Build edpkh r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(edpkh) conflict.
End Conflicting_activation.
Definition Conflicting_activation := Conflicting_activation.record.
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.wrong_voting_period_index"
"Wrong voting period index"
"The voting operation contains a voting period index different from the current one."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int32 × int32) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The voting operation is meant for voting period "
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
", whereas the current period is "
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"The voting operation is meant for voting period %ld, whereas the current period is %ld.")
provided expected))
(Data_encoding.obj2
(Data_encoding.req None None "current_index" Data_encoding.int32_value)
(Data_encoding.req None None "provided_index"
Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_voting_period_index" then
let '{|
Wrong_voting_period_index.expected := expected;
Wrong_voting_period_index.provided := provided
|} := cast Wrong_voting_period_index payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : int32 × int32) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Wrong_voting_period_index" Wrong_voting_period_index
{| Wrong_voting_period_index.expected := expected;
Wrong_voting_period_index.provided := provided; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.wrong_voting_period_kind" "Wrong voting period kind"
"The voting operation is incompatible the current voting period kind."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Alpha_context.Voting_period.kind ×
list Alpha_context.Voting_period.kind) ⇒
let '(current, expected) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The voting operation is only valid during a "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" voting period, but we are currently in a "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " period."
CamlinternalFormatBasics.End_of_format)))))
"The voting operation is only valid during a %a voting period, but we are currently in a %a period.")
(Format.pp_print_list
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal " or "
CamlinternalFormatBasics.End_of_format) " or ")))
Alpha_context.Voting_period.pp_kind) expected
Alpha_context.Voting_period.pp_kind current))
(Data_encoding.obj2
(Data_encoding.req None None "current"
Alpha_context.Voting_period.kind_encoding)
(Data_encoding.req None None "expected"
(Data_encoding.list_value None
Alpha_context.Voting_period.kind_encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Wrong_voting_period_kind" then
let '{|
Wrong_voting_period_kind.current := current;
Wrong_voting_period_kind.expected := expected
|} := cast Wrong_voting_period_kind payload in
Some (current, expected)
else None
end)
(fun (function_parameter :
Alpha_context.Voting_period.kind ×
list Alpha_context.Voting_period.kind) ⇒
let '(current, expected) := function_parameter in
Build_extensible "Wrong_voting_period_kind" Wrong_voting_period_kind
{| Wrong_voting_period_kind.current := current;
Wrong_voting_period_kind.expected := expected; |}) in
let description := "The delegate is not in the vote listings." in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.source_not_in_vote_listings"
"Source not in vote listings" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Source_not_in_vote_listings" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Source_not_in_vote_listings" unit tt) in
let description := "Proposal list cannot be empty." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.empty_proposals" "Empty proposals" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Empty_proposals" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Empty_proposals" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.proposals_contain_duplicate"
"Proposals contain duplicate"
"The list of proposals contains a duplicate element."
(Some
(fun (ppf : Format.formatter) ⇒
fun (proposal : Protocol_hash.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The list of proposals contains multiple occurrences of the proposal "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"The list of proposals contains multiple occurrences of the proposal %a.")
Protocol_hash.pp proposal))
(Data_encoding.obj1
(Data_encoding.req None None "proposal" Protocol_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Proposals_contain_duplicate" then
let '{| Proposals_contain_duplicate.proposal := proposal |} :=
cast Proposals_contain_duplicate payload in
Some proposal
else None
end)
(fun (proposal : Protocol_hash.t) ⇒
Build_extensible "Proposals_contain_duplicate"
Proposals_contain_duplicate
{| Proposals_contain_duplicate.proposal := proposal; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.already_proposed" "Already proposed"
"The delegate has already submitted one of the operation's proposals."
(Some
(fun (ppf : Format.formatter) ⇒
fun (proposal : Protocol_hash.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The delegate has already submitted the proposal "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"The delegate has already submitted the proposal %a.")
Protocol_hash.pp proposal))
(Data_encoding.obj1
(Data_encoding.req None None "proposal" Protocol_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_proposed" then
let '{| Already_proposed.proposal := proposal |} :=
cast Already_proposed payload in
Some proposal
else None
end)
(fun (proposal : Protocol_hash.t) ⇒
Build_extensible "Already_proposed" Already_proposed
{| Already_proposed.proposal := proposal; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.conflict_too_many_proposals"
"Conflict too many proposals"
"The delegate exceeded the maximum number of allowed proposals due to, among others, previous Proposals operations in the current block/mempool."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(previous_count, operation_count) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The delegate cannot submit too many protocol proposals: it currently voted for "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" and is trying to vote for "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal " more."
CamlinternalFormatBasics.End_of_format)))))
"The delegate cannot submit too many protocol proposals: it currently voted for %d and is trying to vote for %d more.")
previous_count operation_count))
(Data_encoding.obj2
(Data_encoding.req None None "previous_count" Data_encoding.int8)
(Data_encoding.req None None "operation_count" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_many_proposals" then
let '{|
Too_many_proposals.previous_count := previous_count;
Too_many_proposals.operation_count := operation_count
|} := cast Too_many_proposals payload in
Some (previous_count, operation_count)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(previous_count, operation_count) := function_parameter in
Build_extensible "Too_many_proposals" Too_many_proposals
{| Too_many_proposals.previous_count := previous_count;
Too_many_proposals.operation_count := operation_count; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.conflicting_proposals" "Conflicting proposals"
"The current block/mempool already contains a testnest dictator proposals operation, so it cannot have any other voting operation."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The current block/mempool already contains a conflicting operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"The current block/mempool already contains a conflicting operation %a.")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_proposals" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_proposals" operation_conflict conflict)
in
let description :=
"A testnet dictator cannot submit more than one proposal at a time." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.testnet_dictator_multiple_proposals"
"Testnet dictator multiple proposals" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Testnet_dictator_multiple_proposals" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Testnet_dictator_multiple_proposals" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.proposals_from_unregistered_delegate"
"Proposals from an unregistered delegate"
"Cannot submit proposals with an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot submit proposals with public key hash "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" (unregistered delegate)."
CamlinternalFormatBasics.End_of_format)))
"Cannot submit proposals with public key hash %a (unregistered delegate).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Proposals_from_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Proposals_from_unregistered_delegate"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.ballot_for_wrong_proposal"
"Ballot for wrong proposal"
"Ballot provided for a proposal that is not the current one."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : Protocol_hash.t × Protocol_hash.t) ⇒
let '(current, submitted) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Ballot provided for proposal "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" whereas the current proposal is "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Ballot provided for proposal %a whereas the current proposal is %a.")
Protocol_hash.pp submitted Protocol_hash.pp current))
(Data_encoding.obj2
(Data_encoding.req None None "current_proposal" Protocol_hash.encoding)
(Data_encoding.req None None "ballot_proposal" Protocol_hash.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Ballot_for_wrong_proposal" then
let '{|
Ballot_for_wrong_proposal.current := current;
Ballot_for_wrong_proposal.submitted := submitted
|} := cast Ballot_for_wrong_proposal payload in
Some (current, submitted)
else None
end)
(fun (function_parameter : Protocol_hash.t × Protocol_hash.t) ⇒
let '(current, submitted) := function_parameter in
Build_extensible "Ballot_for_wrong_proposal" Ballot_for_wrong_proposal
{| Ballot_for_wrong_proposal.current := current;
Ballot_for_wrong_proposal.submitted := submitted; |}) in
let description :=
"The delegate has already submitted a ballot for the current voting period."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.already_submitted_a_ballot"
"Already submitted a ballot" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_submitted_a_ballot" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Already_submitted_a_ballot" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"operation.ballot_from_unregistered_delegate"
"Ballot from an unregistered delegate"
"Cannot cast a ballot for an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot cast a ballot for public key hash "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" (unregistered delegate)."
CamlinternalFormatBasics.End_of_format)))
"Cannot cast a ballot for public key hash %a (unregistered delegate).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Ballot_from_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Ballot_from_unregistered_delegate"
Signature.public_key_hash c_value) in
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.conflicting_ballot" "Conflicting ballot"
"The delegate has already submitted a ballot in a previously validated operation of the current block or mempool."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The delegate has already submitted a ballot in the previously validated operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" of the current block or mempool."
CamlinternalFormatBasics.End_of_format)))
"The delegate has already submitted a ballot in the previously validated operation %a of the current block or mempool.")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_ballot" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_ballot" operation_conflict conflict).
End Voting.
Module Anonymous.
Module Invalid_activation.
Record record : Set := Build {
pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t);
}.
Definition with_pkh pkh (r : record) :=
Build pkh.
End Invalid_activation.
Definition Invalid_activation := Invalid_activation.record.
Module Conflicting_activation.
Record record : Set := Build {
edpkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t);
conflict : operation_conflict;
}.
Definition with_edpkh edpkh (r : record) :=
Build edpkh r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(edpkh) conflict.
End Conflicting_activation.
Definition Conflicting_activation := Conflicting_activation.record.
Init function; without side-effects in Coq
Definition init_module4 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.invalid_activation" "Invalid activation"
"The given key and secret do not correspond to any existing preallocated contract."
(Some
(fun (ppf : Format.formatter) ⇒
fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t))
⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid activation. The public key "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" and accompanying secret do not match any commitment."
CamlinternalFormatBasics.End_of_format)))
"Invalid activation. The public key %a and accompanying secret do not match any commitment.")
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
(Data_encoding.obj1
(Data_encoding.req None None "pkh"
Ed25519.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 "Invalid_activation" then
let '{| Invalid_activation.pkh := pkh |} :=
cast Invalid_activation payload in
Some pkh
else None
end)
(fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
Build_extensible "Invalid_activation" Invalid_activation
{| Invalid_activation.pkh := pkh; |}) in
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_activation"
"Account already activated in current validation_state"
"The account has already been activated by a previous operation in the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) ×
operation_conflict) ⇒
let
'(edpkh,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid activation: the account "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has already been activated in the current validation state by operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Invalid activation: the account %a has already been activated in the current validation state by operation %a.")
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) edpkh
Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "edpkh"
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_activation" then
let '{|
Conflicting_activation.edpkh := edpkh;
Conflicting_activation.conflict := conflict
|} := cast Conflicting_activation payload in
Some (edpkh, conflict)
else None
end)
(fun (function_parameter :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) ×
operation_conflict) ⇒
let '(edpkh, conflict) := function_parameter in
Build_extensible "Conflicting_activation" Conflicting_activation
{| Conflicting_activation.edpkh := edpkh;
Conflicting_activation.conflict := conflict; |}).
Inductive denunciation_kind : Set :=
| Preendorsement : denunciation_kind
| Endorsement : denunciation_kind
| Block : denunciation_kind.
Definition denunciation_kind_encoding
: Data_encoding.encoding denunciation_kind :=
Data_encoding.string_enum
[
("preendorsement", Preendorsement);
("endorsement", Endorsement);
("block", Block)
].
Definition pp_denunciation_kind
(fmt : Format.formatter) (function_parameter : denunciation_kind) : unit :=
match function_parameter with
| Preendorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "preendorsement"
CamlinternalFormatBasics.End_of_format) "preendorsement")
| Endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "endorsement"
CamlinternalFormatBasics.End_of_format) "endorsement")
| Block ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "block"
CamlinternalFormatBasics.End_of_format) "block")
end.
Module Invalid_double_baking_evidence.
Record record : Set := Build {
hash1 : Block_hash.t;
level1 : Alpha_context.Raw_level.t;
round1 : Alpha_context.Round.t;
hash2 : Block_hash.t;
level2 : Alpha_context.Raw_level.t;
round2 : Alpha_context.Round.t;
}.
Definition with_hash1 hash1 (r : record) :=
Build hash1 r.(level1) r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_level1 level1 (r : record) :=
Build r.(hash1) level1 r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_round1 round1 (r : record) :=
Build r.(hash1) r.(level1) round1 r.(hash2) r.(level2) r.(round2).
Definition with_hash2 hash2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) hash2 r.(level2) r.(round2).
Definition with_level2 level2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) level2 r.(round2).
Definition with_round2 round2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) r.(level2) round2.
End Invalid_double_baking_evidence.
Definition Invalid_double_baking_evidence :=
Invalid_double_baking_evidence.record.
Module Inconsistent_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
delegate1 : Signature.public_key_hash;
delegate2 : Signature.public_key_hash;
}.
Definition with_kind kind (r : record) :=
Build kind r.(delegate1) r.(delegate2).
Definition with_delegate1 delegate1 (r : record) :=
Build r.(kind) delegate1 r.(delegate2).
Definition with_delegate2 delegate2 (r : record) :=
Build r.(kind) r.(delegate1) delegate2.
End Inconsistent_denunciation.
Definition Inconsistent_denunciation := Inconsistent_denunciation.record.
Module Already_denounced.
Record record : Set := Build {
kind : denunciation_kind;
delegate : Signature.public_key_hash;
level : Alpha_context.Level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(delegate) r.(level).
Definition with_delegate delegate (r : record) :=
Build r.(kind) delegate r.(level).
Definition with_level level (r : record) :=
Build r.(kind) r.(delegate) level.
End Already_denounced.
Definition Already_denounced := Already_denounced.record.
Module Conflicting_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
conflict : operation_conflict;
}.
Definition with_kind kind (r : record) :=
Build kind r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(kind) conflict.
End Conflicting_denunciation.
Definition Conflicting_denunciation := Conflicting_denunciation.record.
Module Too_early_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
current : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(current).
Definition with_level level (r : record) :=
Build r.(kind) level r.(current).
Definition with_current current (r : record) :=
Build r.(kind) r.(level) current.
End Too_early_denunciation.
Definition Too_early_denunciation := Too_early_denunciation.record.
Module Outdated_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
last_cycle : Alpha_context.Cycle.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(last_cycle).
Definition with_level level (r : record) :=
Build r.(kind) level r.(last_cycle).
Definition with_last_cycle last_cycle (r : record) :=
Build r.(kind) r.(level) last_cycle.
End Outdated_denunciation.
Definition Outdated_denunciation := Outdated_denunciation.record.
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.invalid_activation" "Invalid activation"
"The given key and secret do not correspond to any existing preallocated contract."
(Some
(fun (ppf : Format.formatter) ⇒
fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t))
⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid activation. The public key "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" and accompanying secret do not match any commitment."
CamlinternalFormatBasics.End_of_format)))
"Invalid activation. The public key %a and accompanying secret do not match any commitment.")
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
(Data_encoding.obj1
(Data_encoding.req None None "pkh"
Ed25519.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 "Invalid_activation" then
let '{| Invalid_activation.pkh := pkh |} :=
cast Invalid_activation payload in
Some pkh
else None
end)
(fun (pkh : Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t)) ⇒
Build_extensible "Invalid_activation" Invalid_activation
{| Invalid_activation.pkh := pkh; |}) in
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_activation"
"Account already activated in current validation_state"
"The account has already been activated by a previous operation in the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) ×
operation_conflict) ⇒
let
'(edpkh,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid activation: the account "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has already been activated in the current validation state by operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Invalid activation: the account %a has already been activated in the current validation state by operation %a.")
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) edpkh
Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "edpkh"
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_activation" then
let '{|
Conflicting_activation.edpkh := edpkh;
Conflicting_activation.conflict := conflict
|} := cast Conflicting_activation payload in
Some (edpkh, conflict)
else None
end)
(fun (function_parameter :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) ×
operation_conflict) ⇒
let '(edpkh, conflict) := function_parameter in
Build_extensible "Conflicting_activation" Conflicting_activation
{| Conflicting_activation.edpkh := edpkh;
Conflicting_activation.conflict := conflict; |}).
Inductive denunciation_kind : Set :=
| Preendorsement : denunciation_kind
| Endorsement : denunciation_kind
| Block : denunciation_kind.
Definition denunciation_kind_encoding
: Data_encoding.encoding denunciation_kind :=
Data_encoding.string_enum
[
("preendorsement", Preendorsement);
("endorsement", Endorsement);
("block", Block)
].
Definition pp_denunciation_kind
(fmt : Format.formatter) (function_parameter : denunciation_kind) : unit :=
match function_parameter with
| Preendorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "preendorsement"
CamlinternalFormatBasics.End_of_format) "preendorsement")
| Endorsement ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "endorsement"
CamlinternalFormatBasics.End_of_format) "endorsement")
| Block ⇒
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "block"
CamlinternalFormatBasics.End_of_format) "block")
end.
Module Invalid_double_baking_evidence.
Record record : Set := Build {
hash1 : Block_hash.t;
level1 : Alpha_context.Raw_level.t;
round1 : Alpha_context.Round.t;
hash2 : Block_hash.t;
level2 : Alpha_context.Raw_level.t;
round2 : Alpha_context.Round.t;
}.
Definition with_hash1 hash1 (r : record) :=
Build hash1 r.(level1) r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_level1 level1 (r : record) :=
Build r.(hash1) level1 r.(round1) r.(hash2) r.(level2) r.(round2).
Definition with_round1 round1 (r : record) :=
Build r.(hash1) r.(level1) round1 r.(hash2) r.(level2) r.(round2).
Definition with_hash2 hash2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) hash2 r.(level2) r.(round2).
Definition with_level2 level2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) level2 r.(round2).
Definition with_round2 round2 (r : record) :=
Build r.(hash1) r.(level1) r.(round1) r.(hash2) r.(level2) round2.
End Invalid_double_baking_evidence.
Definition Invalid_double_baking_evidence :=
Invalid_double_baking_evidence.record.
Module Inconsistent_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
delegate1 : Signature.public_key_hash;
delegate2 : Signature.public_key_hash;
}.
Definition with_kind kind (r : record) :=
Build kind r.(delegate1) r.(delegate2).
Definition with_delegate1 delegate1 (r : record) :=
Build r.(kind) delegate1 r.(delegate2).
Definition with_delegate2 delegate2 (r : record) :=
Build r.(kind) r.(delegate1) delegate2.
End Inconsistent_denunciation.
Definition Inconsistent_denunciation := Inconsistent_denunciation.record.
Module Already_denounced.
Record record : Set := Build {
kind : denunciation_kind;
delegate : Signature.public_key_hash;
level : Alpha_context.Level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(delegate) r.(level).
Definition with_delegate delegate (r : record) :=
Build r.(kind) delegate r.(level).
Definition with_level level (r : record) :=
Build r.(kind) r.(delegate) level.
End Already_denounced.
Definition Already_denounced := Already_denounced.record.
Module Conflicting_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
conflict : operation_conflict;
}.
Definition with_kind kind (r : record) :=
Build kind r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(kind) conflict.
End Conflicting_denunciation.
Definition Conflicting_denunciation := Conflicting_denunciation.record.
Module Too_early_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
current : Alpha_context.Raw_level.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(current).
Definition with_level level (r : record) :=
Build r.(kind) level r.(current).
Definition with_current current (r : record) :=
Build r.(kind) r.(level) current.
End Too_early_denunciation.
Definition Too_early_denunciation := Too_early_denunciation.record.
Module Outdated_denunciation.
Record record : Set := Build {
kind : denunciation_kind;
level : Alpha_context.Raw_level.t;
last_cycle : Alpha_context.Cycle.t;
}.
Definition with_kind kind (r : record) :=
Build kind r.(level) r.(last_cycle).
Definition with_level level (r : record) :=
Build r.(kind) level r.(last_cycle).
Definition with_last_cycle last_cycle (r : record) :=
Build r.(kind) r.(level) last_cycle.
End Outdated_denunciation.
Definition Outdated_denunciation := Outdated_denunciation.record.
Init function; without side-effects in Coq
Definition init_module5 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.block.invalid_double_baking_evidence"
"Invalid double baking evidence"
"A double-baking evidence is inconsistent (two distinct levels)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t × Block_hash.t ×
Alpha_context.Raw_level.raw_level × Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid double-baking evidence (hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", levels/rounds: ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
") and ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
"," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
"))"
CamlinternalFormatBasics.End_of_format)))))))))))))
"Invalid double-baking evidence (hash: %a and %a, levels/rounds: (%ld,%ld) and (%ld,%ld))")
Block_hash.pp hash1 Block_hash.pp hash2
(Alpha_context.Raw_level.to_int32 level1)
(Alpha_context.Round.to_int32 round1)
(Alpha_context.Raw_level.to_int32 level2)
(Alpha_context.Round.to_int32 round2)))
(Data_encoding.obj6
(Data_encoding.req None None "hash1" Block_hash.encoding)
(Data_encoding.req None None "level1" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round1" Alpha_context.Round.encoding)
(Data_encoding.req None None "hash2" Block_hash.encoding)
(Data_encoding.req None None "level2" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round2" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_double_baking_evidence" then
let '{|
Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2
|} := cast Invalid_double_baking_evidence payload in
Some (hash1, level1, round1, hash2, level2, round2)
else None
end)
(fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t × Block_hash.t ×
Alpha_context.Raw_level.raw_level × Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Build_extensible "Invalid_double_baking_evidence"
Invalid_double_baking_evidence
{| Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.block.invalid_denunciation" "Invalid denunciation"
"A denunciation is malformed"
(Some
(fun (ppf : Format.formatter) ⇒
fun (kind_value : denunciation_kind) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Malformed double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " evidence"
CamlinternalFormatBasics.End_of_format)))
"Malformed double-%a evidence") pp_denunciation_kind
kind_value))
(Data_encoding.obj1
(Data_encoding.req None None "kind" denunciation_kind_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_denunciation" then
let kind_value := cast denunciation_kind payload in
Some kind_value
else None
end)
(fun (kind_value : denunciation_kind) ⇒
Build_extensible "Invalid_denunciation" denunciation_kind kind_value)
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.block.inconsistent_denunciation"
"Inconsistent denunciation"
"A denunciation operation is inconsistent (two distinct delegates)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Inconsistent double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" evidence (distinct delegate: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"Inconsistent double-%a evidence (distinct delegate: %a and %a)")
pp_denunciation_kind kind_value
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate1
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate2))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "delegate1"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "delegate2"
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 "Inconsistent_denunciation" then
let '{|
Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2
|} := cast Inconsistent_denunciation payload in
Some (kind_value, delegate1, delegate2)
else None
end)
(fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Build_extensible "Inconsistent_denunciation" Inconsistent_denunciation
{| Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.already_denounced" "Already denounced"
"The same denunciation has already been validated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Alpha_context.Level.t) ⇒
let '(kind_value, delegate, level) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " at level "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has already been denounced for a double "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))))
"Delegate %a at level %a has already been denounced for a double %a.")
pp_denunciation_kind kind_value
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate Alpha_context.Level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "denunciation_kind"
denunciation_kind_encoding)
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "level" Alpha_context.Level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_denounced" then
let '{|
Already_denounced.kind := kind_value;
Already_denounced.delegate := delegate;
Already_denounced.level := level
|} := cast Already_denounced payload in
Some (kind_value, delegate, level)
else None
end)
(fun (function_parameter :
denunciation_kind × Signature.public_key_hash × Alpha_context.Level.t)
⇒
let '(kind_value, delegate, level) := function_parameter in
Build_extensible "Already_denounced" Already_denounced
{| Already_denounced.kind := kind_value;
Already_denounced.delegate := delegate;
Already_denounced.level := level; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_denunciation"
"Conflicting denunciation in current validation state"
"The same denunciation has already been validated in the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : denunciation_kind × operation_conflict) ⇒
let
'(kind_value,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Double "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" evidence already exists in the current validation state as operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Double %a evidence already exists in the current validation state as operation %a.")
pp_denunciation_kind kind_value Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "denunciation_kind"
denunciation_kind_encoding)
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_denunciation" then
let '{|
Conflicting_denunciation.kind := kind_value;
Conflicting_denunciation.conflict := conflict
|} := cast Conflicting_denunciation payload in
Some (kind_value, conflict)
else None
end)
(fun (function_parameter : denunciation_kind × operation_conflict) ⇒
let '(kind_value, conflict) := function_parameter in
Build_extensible "Conflicting_denunciation" Conflicting_denunciation
{| Conflicting_denunciation.kind := kind_value;
Conflicting_denunciation.conflict := conflict; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.block.too_early_denunciation"
"Too early denunciation" "A denunciation is too far in the future"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" denunciation is too far in the future (current level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a denunciation is too far in the future (current level: %a, given level: %a)")
pp_denunciation_kind kind_value Alpha_context.Raw_level.pp
current Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "current"
Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_early_denunciation" then
let '{|
Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current
|} := cast Too_early_denunciation payload in
Some (kind_value, level, current)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Build_extensible "Too_early_denunciation" Too_early_denunciation
{| Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current; |}) in
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.block.outdated_denunciation" "Outdated denunciation"
"A denunciation is outdated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Cycle.t) ⇒
let '(kind_value, level, last_cycle) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" denunciation is outdated (last acceptable cycle: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a denunciation is outdated (last acceptable cycle: %a, given level: %a).")
pp_denunciation_kind kind_value Alpha_context.Cycle.pp last_cycle
Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "last" Alpha_context.Cycle.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Outdated_denunciation" then
let '{|
Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle
|} := cast Outdated_denunciation payload in
Some (kind_value, level, last_cycle)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t × Alpha_context.Cycle.t)
⇒
let '(kind_value, level, last_cycle) := function_parameter in
Build_extensible "Outdated_denunciation" Outdated_denunciation
{| Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle; |}).
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.block.invalid_double_baking_evidence"
"Invalid double baking evidence"
"A double-baking evidence is inconsistent (two distinct levels)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t × Block_hash.t ×
Alpha_context.Raw_level.raw_level × Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Invalid double-baking evidence (hash: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", levels/rounds: ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
") and ("
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal
"," % char
(CamlinternalFormatBasics.Int32
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
"))"
CamlinternalFormatBasics.End_of_format)))))))))))))
"Invalid double-baking evidence (hash: %a and %a, levels/rounds: (%ld,%ld) and (%ld,%ld))")
Block_hash.pp hash1 Block_hash.pp hash2
(Alpha_context.Raw_level.to_int32 level1)
(Alpha_context.Round.to_int32 round1)
(Alpha_context.Raw_level.to_int32 level2)
(Alpha_context.Round.to_int32 round2)))
(Data_encoding.obj6
(Data_encoding.req None None "hash1" Block_hash.encoding)
(Data_encoding.req None None "level1" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round1" Alpha_context.Round.encoding)
(Data_encoding.req None None "hash2" Block_hash.encoding)
(Data_encoding.req None None "level2" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "round2" Alpha_context.Round.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_double_baking_evidence" then
let '{|
Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2
|} := cast Invalid_double_baking_evidence payload in
Some (hash1, level1, round1, hash2, level2, round2)
else None
end)
(fun (function_parameter :
Block_hash.t × Alpha_context.Raw_level.raw_level ×
Alpha_context.Round.t × Block_hash.t ×
Alpha_context.Raw_level.raw_level × Alpha_context.Round.t) ⇒
let '(hash1, level1, round1, hash2, level2, round2) :=
function_parameter in
Build_extensible "Invalid_double_baking_evidence"
Invalid_double_baking_evidence
{| Invalid_double_baking_evidence.hash1 := hash1;
Invalid_double_baking_evidence.level1 := level1;
Invalid_double_baking_evidence.round1 := round1;
Invalid_double_baking_evidence.hash2 := hash2;
Invalid_double_baking_evidence.level2 := level2;
Invalid_double_baking_evidence.round2 := round2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.block.invalid_denunciation" "Invalid denunciation"
"A denunciation is malformed"
(Some
(fun (ppf : Format.formatter) ⇒
fun (kind_value : denunciation_kind) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Malformed double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " evidence"
CamlinternalFormatBasics.End_of_format)))
"Malformed double-%a evidence") pp_denunciation_kind
kind_value))
(Data_encoding.obj1
(Data_encoding.req None None "kind" denunciation_kind_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_denunciation" then
let kind_value := cast denunciation_kind payload in
Some kind_value
else None
end)
(fun (kind_value : denunciation_kind) ⇒
Build_extensible "Invalid_denunciation" denunciation_kind kind_value)
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.block.inconsistent_denunciation"
"Inconsistent denunciation"
"A denunciation operation is inconsistent (two distinct delegates)"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Inconsistent double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" evidence (distinct delegate: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"Inconsistent double-%a evidence (distinct delegate: %a and %a)")
pp_denunciation_kind kind_value
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate1
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp_short)
delegate2))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "delegate1"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "delegate2"
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 "Inconsistent_denunciation" then
let '{|
Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2
|} := cast Inconsistent_denunciation payload in
Some (kind_value, delegate1, delegate2)
else None
end)
(fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(kind_value, delegate1, delegate2) := function_parameter in
Build_extensible "Inconsistent_denunciation" Inconsistent_denunciation
{| Inconsistent_denunciation.kind := kind_value;
Inconsistent_denunciation.delegate1 := delegate1;
Inconsistent_denunciation.delegate2 := delegate2; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.already_denounced" "Already denounced"
"The same denunciation has already been validated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Signature.public_key_hash ×
Alpha_context.Level.t) ⇒
let '(kind_value, delegate, level) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " at level "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" has already been denounced for a double "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))))
"Delegate %a at level %a has already been denounced for a double %a.")
pp_denunciation_kind kind_value
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate Alpha_context.Level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "denunciation_kind"
denunciation_kind_encoding)
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "level" Alpha_context.Level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Already_denounced" then
let '{|
Already_denounced.kind := kind_value;
Already_denounced.delegate := delegate;
Already_denounced.level := level
|} := cast Already_denounced payload in
Some (kind_value, delegate, level)
else None
end)
(fun (function_parameter :
denunciation_kind × Signature.public_key_hash × Alpha_context.Level.t)
⇒
let '(kind_value, delegate, level) := function_parameter in
Build_extensible "Already_denounced" Already_denounced
{| Already_denounced.kind := kind_value;
Already_denounced.delegate := delegate;
Already_denounced.level := level; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_denunciation"
"Conflicting denunciation in current validation state"
"The same denunciation has already been validated in the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : denunciation_kind × operation_conflict) ⇒
let
'(kind_value,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Double "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" evidence already exists in the current validation state as operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Double %a evidence already exists in the current validation state as operation %a.")
pp_denunciation_kind kind_value Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "denunciation_kind"
denunciation_kind_encoding)
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_denunciation" then
let '{|
Conflicting_denunciation.kind := kind_value;
Conflicting_denunciation.conflict := conflict
|} := cast Conflicting_denunciation payload in
Some (kind_value, conflict)
else None
end)
(fun (function_parameter : denunciation_kind × operation_conflict) ⇒
let '(kind_value, conflict) := function_parameter in
Build_extensible "Conflicting_denunciation" Conflicting_denunciation
{| Conflicting_denunciation.kind := kind_value;
Conflicting_denunciation.conflict := conflict; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.block.too_early_denunciation"
"Too early denunciation" "A denunciation is too far in the future"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" denunciation is too far in the future (current level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal ")" % char
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a denunciation is too far in the future (current level: %a, given level: %a)")
pp_denunciation_kind kind_value Alpha_context.Raw_level.pp
current Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "current"
Alpha_context.Raw_level.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Too_early_denunciation" then
let '{|
Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current
|} := cast Too_early_denunciation payload in
Some (kind_value, level, current)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Raw_level.t) ⇒
let '(kind_value, level, current) := function_parameter in
Build_extensible "Too_early_denunciation" Too_early_denunciation
{| Too_early_denunciation.kind := kind_value;
Too_early_denunciation.level := level;
Too_early_denunciation.current := current; |}) in
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.block.outdated_denunciation" "Outdated denunciation"
"A denunciation is outdated."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t ×
Alpha_context.Cycle.t) ⇒
let '(kind_value, level, last_cycle) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "A double-"
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" denunciation is outdated (last acceptable cycle: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
", given level: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))))
"A double-%a denunciation is outdated (last acceptable cycle: %a, given level: %a).")
pp_denunciation_kind kind_value Alpha_context.Cycle.pp last_cycle
Alpha_context.Raw_level.pp level))
(Data_encoding.obj3
(Data_encoding.req None None "kind" denunciation_kind_encoding)
(Data_encoding.req None None "level" Alpha_context.Raw_level.encoding)
(Data_encoding.req None None "last" Alpha_context.Cycle.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Outdated_denunciation" then
let '{|
Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle
|} := cast Outdated_denunciation payload in
Some (kind_value, level, last_cycle)
else None
end)
(fun (function_parameter :
denunciation_kind × Alpha_context.Raw_level.t × Alpha_context.Cycle.t)
⇒
let '(kind_value, level, last_cycle) := function_parameter in
Build_extensible "Outdated_denunciation" Outdated_denunciation
{| Outdated_denunciation.kind := kind_value;
Outdated_denunciation.level := level;
Outdated_denunciation.last_cycle := last_cycle; |}).
Init function; without side-effects in Coq
Definition init_module6 : unit :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_nonce_revelation"
"Conflicting nonce revelation in the current validation state)."
"A revelation for the same nonce has already been validated for the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce revelation is conflicting with an existing revelation "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"This nonce revelation is conflicting with an existing revelation %a")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_nonce_revelation" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_nonce_revelation" operation_conflict
conflict).
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_nonce_revelation"
"Conflicting nonce revelation in the current validation state)."
"A revelation for the same nonce has already been validated for the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This nonce revelation is conflicting with an existing revelation "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"This nonce revelation is conflicting with an existing revelation %a")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_nonce_revelation" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_nonce_revelation" operation_conflict
conflict).
Init function; without side-effects in Coq
Definition init_module7 : unit :=
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_vdf_revelation"
"Conflicting vdf revelation in the current validation state)."
"A revelation for the same vdf has already been validated for the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This vdf revelation is conflicting with an existing revelation "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"This vdf revelation is conflicting with an existing revelation %a")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_vdf_revelation" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_vdf_revelation" operation_conflict
conflict).
Module Invalid_drain_delegate_inactive_key.
Record record : Set := Build {
delegate : Signature.public_key_hash;
consensus_key : Signature.public_key_hash;
active_consensus_key : Signature.public_key_hash;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(consensus_key) r.(active_consensus_key).
Definition with_consensus_key consensus_key (r : record) :=
Build r.(delegate) consensus_key r.(active_consensus_key).
Definition with_active_consensus_key active_consensus_key (r : record) :=
Build r.(delegate) r.(consensus_key) active_consensus_key.
End Invalid_drain_delegate_inactive_key.
Definition Invalid_drain_delegate_inactive_key :=
Invalid_drain_delegate_inactive_key.record.
Module Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.
Record record : Set := Build {
delegate : Signature.public_key_hash;
destination : Signature.public_key_hash;
min_amount : Alpha_context.Tez.t;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(destination) r.(min_amount).
Definition with_destination destination (r : record) :=
Build r.(delegate) destination r.(min_amount).
Definition with_min_amount min_amount (r : record) :=
Build r.(delegate) r.(destination) min_amount.
End Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.
Definition Invalid_drain_delegate_insufficient_funds_for_burn_or_fees :=
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.record.
Module Conflicting_drain_delegate.
Record record : Set := Build {
delegate : Signature.public_key_hash;
conflict : operation_conflict;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(delegate) conflict.
End Conflicting_drain_delegate.
Definition Conflicting_drain_delegate := Conflicting_drain_delegate.record.
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_vdf_revelation"
"Conflicting vdf revelation in the current validation state)."
"A revelation for the same vdf has already been validated for the current validation state."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : operation_conflict) ⇒
let
'Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|} := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This vdf revelation is conflicting with an existing revelation "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))
"This vdf revelation is conflicting with an existing revelation %a")
Operation_hash.pp existing))
(Data_encoding.obj1
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_vdf_revelation" then
let conflict := cast operation_conflict payload in
Some conflict
else None
end)
(fun (conflict : operation_conflict) ⇒
Build_extensible "Conflicting_vdf_revelation" operation_conflict
conflict).
Module Invalid_drain_delegate_inactive_key.
Record record : Set := Build {
delegate : Signature.public_key_hash;
consensus_key : Signature.public_key_hash;
active_consensus_key : Signature.public_key_hash;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(consensus_key) r.(active_consensus_key).
Definition with_consensus_key consensus_key (r : record) :=
Build r.(delegate) consensus_key r.(active_consensus_key).
Definition with_active_consensus_key active_consensus_key (r : record) :=
Build r.(delegate) r.(consensus_key) active_consensus_key.
End Invalid_drain_delegate_inactive_key.
Definition Invalid_drain_delegate_inactive_key :=
Invalid_drain_delegate_inactive_key.record.
Module Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.
Record record : Set := Build {
delegate : Signature.public_key_hash;
destination : Signature.public_key_hash;
min_amount : Alpha_context.Tez.t;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(destination) r.(min_amount).
Definition with_destination destination (r : record) :=
Build r.(delegate) destination r.(min_amount).
Definition with_min_amount min_amount (r : record) :=
Build r.(delegate) r.(destination) min_amount.
End Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.
Definition Invalid_drain_delegate_insufficient_funds_for_burn_or_fees :=
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.record.
Module Conflicting_drain_delegate.
Record record : Set := Build {
delegate : Signature.public_key_hash;
conflict : operation_conflict;
}.
Definition with_delegate delegate (r : record) :=
Build delegate r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(delegate) conflict.
End Conflicting_drain_delegate.
Definition Conflicting_drain_delegate := Conflicting_drain_delegate.record.
Init function; without side-effects in Coq
Definition init_module8 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.drain_delegate_key_on_unregistered_delegate"
"Drain delegate key on an unregistered delegate"
"Cannot drain an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot drain an unregistered delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Cannot drain an unregistered delegate %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Drain_delegate_on_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Drain_delegate_on_unregistered_delegate"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.inactive_key"
"Drain delegate with an inactive consensus key"
"Cannot drain with an inactive consensus key."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(delegate, consensus_key, active_consensus_key) :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Consensus key "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is not the active consensus key for delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
". The active consensus key is "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))))
"Consensus key %a is not the active consensus key for delegate %a. The active consensus key is %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
consensus_key
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
active_consensus_key))
(Data_encoding.obj3
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "consensus_key"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "active_consensus_key"
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 "Invalid_drain_delegate_inactive_key" then
let '{|
Invalid_drain_delegate_inactive_key.delegate := delegate;
Invalid_drain_delegate_inactive_key.consensus_key :=
consensus_key;
Invalid_drain_delegate_inactive_key.active_consensus_key :=
active_consensus_key
|} := cast Invalid_drain_delegate_inactive_key payload in
Some (delegate, consensus_key, active_consensus_key)
else None
end)
(fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(delegate, consensus_key, active_consensus_key) :=
function_parameter in
Build_extensible "Invalid_drain_delegate_inactive_key"
Invalid_drain_delegate_inactive_key
{| Invalid_drain_delegate_inactive_key.delegate := delegate;
Invalid_drain_delegate_inactive_key.consensus_key :=
consensus_key;
Invalid_drain_delegate_inactive_key.active_consensus_key :=
active_consensus_key; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.no_consensus_key"
"Drain a delegate without consensus key"
"Cannot drain a delegate without consensus key."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"There is no active consensus key for delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"There is no active consensus key for delegate %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Invalid_drain_delegate_no_consensus_key" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Invalid_drain_delegate_no_consensus_key"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.noop" "Invalid drain delegate: noop"
"Cannot drain a delegate to itself."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The destination of a drain operation cannot be the delegate itself ("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))
"The destination of a drain operation cannot be the delegate itself (%a).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Invalid_drain_delegate_noop" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Invalid_drain_delegate_noop"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.insufficient_funds_for_burn_or_fees"
"Drain delegate without enough balance for allocation burn or drain fees"
"Cannot drain without enough allocation burn and drain fees."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Alpha_context.Tez.t) ⇒
let '(delegate, destination, min_amount) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot drain delegate from "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " to "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
": not enough funds for the drain fees in the delegate account (minimum balance required: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))))
"Cannot drain delegate from %a to %a: not enough funds for the drain fees in the delegate account (minimum balance required: %a).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
destination Alpha_context.Tez.pp min_amount))
(Data_encoding.obj3
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "destination"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "min_amount" Alpha_context.Tez.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if
String.eqb tag
"Invalid_drain_delegate_insufficient_funds_for_burn_or_fees"
then
let '{|
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.delegate :=
delegate;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.destination
:= destination;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.min_amount
:= min_amount
|} :=
cast Invalid_drain_delegate_insufficient_funds_for_burn_or_fees
payload in
Some (delegate, destination, min_amount)
else None
end)
(fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Alpha_context.Tez.t) ⇒
let '(delegate, destination, min_amount) := function_parameter in
Build_extensible
"Invalid_drain_delegate_insufficient_funds_for_burn_or_fees"
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees
{|
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.delegate
:= delegate;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.destination
:= destination;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.min_amount
:= min_amount; |}) in
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_drain"
"Conflicting drain in the current validation state)."
"A manager operation or another drain operation is in conflict."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × operation_conflict) ⇒
let
'(delegate,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This drain operation conflicts with operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for the delegate "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"This drain operation conflicts with operation %a for the delegate %a")
Operation_hash.pp existing
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj2
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_drain_delegate" then
let '{|
Conflicting_drain_delegate.delegate := delegate;
Conflicting_drain_delegate.conflict := conflict
|} := cast Conflicting_drain_delegate payload in
Some (delegate, conflict)
else None
end)
(fun (function_parameter : Signature.public_key_hash × operation_conflict)
⇒
let '(delegate, conflict) := function_parameter in
Build_extensible "Conflicting_drain_delegate" Conflicting_drain_delegate
{| Conflicting_drain_delegate.delegate := delegate;
Conflicting_drain_delegate.conflict := conflict; |}).
End Anonymous.
Module Manager.
Module Manager_restriction.
Record record : Set := Build {
source : Signature.public_key_hash;
conflict : operation_conflict;
}.
Definition with_source source (r : record) :=
Build source r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(source) conflict.
End Manager_restriction.
Definition Manager_restriction := Manager_restriction.record.
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.drain_delegate_key_on_unregistered_delegate"
"Drain delegate key on an unregistered delegate"
"Cannot drain an unregistered delegate."
(Some
(fun (ppf : Format.formatter) ⇒
fun (c_value : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot drain an unregistered delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Cannot drain an unregistered delegate %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
c_value))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Drain_delegate_on_unregistered_delegate" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Drain_delegate_on_unregistered_delegate"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.inactive_key"
"Drain delegate with an inactive consensus key"
"Cannot drain with an inactive consensus key."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(delegate, consensus_key, active_consensus_key) :=
function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Consensus key "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" is not the active consensus key for delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
". The active consensus key is "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))))
"Consensus key %a is not the active consensus key for delegate %a. The active consensus key is %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
consensus_key
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
active_consensus_key))
(Data_encoding.obj3
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "consensus_key"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "active_consensus_key"
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 "Invalid_drain_delegate_inactive_key" then
let '{|
Invalid_drain_delegate_inactive_key.delegate := delegate;
Invalid_drain_delegate_inactive_key.consensus_key :=
consensus_key;
Invalid_drain_delegate_inactive_key.active_consensus_key :=
active_consensus_key
|} := cast Invalid_drain_delegate_inactive_key payload in
Some (delegate, consensus_key, active_consensus_key)
else None
end)
(fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Signature.public_key_hash) ⇒
let '(delegate, consensus_key, active_consensus_key) :=
function_parameter in
Build_extensible "Invalid_drain_delegate_inactive_key"
Invalid_drain_delegate_inactive_key
{| Invalid_drain_delegate_inactive_key.delegate := delegate;
Invalid_drain_delegate_inactive_key.consensus_key :=
consensus_key;
Invalid_drain_delegate_inactive_key.active_consensus_key :=
active_consensus_key; |}) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.no_consensus_key"
"Drain a delegate without consensus key"
"Cannot drain a delegate without consensus key."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"There is no active consensus key for delegate "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"There is no active consensus key for delegate %a.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Invalid_drain_delegate_no_consensus_key" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Invalid_drain_delegate_no_consensus_key"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.noop" "Invalid drain delegate: noop"
"Cannot drain a delegate to itself."
(Some
(fun (ppf : Format.formatter) ⇒
fun (delegate : Signature.public_key_hash) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"The destination of a drain operation cannot be the delegate itself ("
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))
"The destination of a drain operation cannot be the delegate itself (%a).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj1
(Data_encoding.req None None "delegate"
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 "Invalid_drain_delegate_noop" then
let c_value := cast Signature.public_key_hash payload in
Some c_value
else None
end)
(fun (c_value : Signature.public_key_hash) ⇒
Build_extensible "Invalid_drain_delegate_noop"
Signature.public_key_hash c_value) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"operation.invalid_drain.insufficient_funds_for_burn_or_fees"
"Drain delegate without enough balance for allocation burn or drain fees"
"Cannot drain without enough allocation burn and drain fees."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Alpha_context.Tez.t) ⇒
let '(delegate, destination, min_amount) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot drain delegate from "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal " to "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
": not enough funds for the drain fees in the delegate account (minimum balance required: "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal ")."
CamlinternalFormatBasics.End_of_format)))))))
"Cannot drain delegate from %a to %a: not enough funds for the drain fees in the delegate account (minimum balance required: %a).")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
destination Alpha_context.Tez.pp min_amount))
(Data_encoding.obj3
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "destination"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "min_amount" Alpha_context.Tez.encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if
String.eqb tag
"Invalid_drain_delegate_insufficient_funds_for_burn_or_fees"
then
let '{|
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.delegate :=
delegate;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.destination
:= destination;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.min_amount
:= min_amount
|} :=
cast Invalid_drain_delegate_insufficient_funds_for_burn_or_fees
payload in
Some (delegate, destination, min_amount)
else None
end)
(fun (function_parameter :
Signature.public_key_hash × Signature.public_key_hash ×
Alpha_context.Tez.t) ⇒
let '(delegate, destination, min_amount) := function_parameter in
Build_extensible
"Invalid_drain_delegate_insufficient_funds_for_burn_or_fees"
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees
{|
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.delegate
:= delegate;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.destination
:= destination;
Invalid_drain_delegate_insufficient_funds_for_burn_or_fees.min_amount
:= min_amount; |}) in
Error_monad.register_error_kind Error_monad.Branch
"validate.operation.conflicting_drain"
"Conflicting drain in the current validation state)."
"A manager operation or another drain operation is in conflict."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × operation_conflict) ⇒
let
'(delegate,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"This drain operation conflicts with operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" for the delegate "
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format))))
"This drain operation conflicts with operation %a for the delegate %a")
Operation_hash.pp existing
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
delegate))
(Data_encoding.obj2
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Conflicting_drain_delegate" then
let '{|
Conflicting_drain_delegate.delegate := delegate;
Conflicting_drain_delegate.conflict := conflict
|} := cast Conflicting_drain_delegate payload in
Some (delegate, conflict)
else None
end)
(fun (function_parameter : Signature.public_key_hash × operation_conflict)
⇒
let '(delegate, conflict) := function_parameter in
Build_extensible "Conflicting_drain_delegate" Conflicting_drain_delegate
{| Conflicting_drain_delegate.delegate := delegate;
Conflicting_drain_delegate.conflict := conflict; |}).
End Anonymous.
Module Manager.
Module Manager_restriction.
Record record : Set := Build {
source : Signature.public_key_hash;
conflict : operation_conflict;
}.
Definition with_source source (r : record) :=
Build source r.(conflict).
Definition with_conflict conflict (r : record) :=
Build r.(source) conflict.
End Manager_restriction.
Definition Manager_restriction := Manager_restriction.record.
Init function; without side-effects in Coq
Definition init_module9 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.manager_restriction" "Manager restriction"
"An operation with the same manager has already been validated in the current block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × operation_conflict) ⇒
let
'(source,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Manager "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" already has the operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" in the current block."
CamlinternalFormatBasics.End_of_format)))))
"Manager %a already has the operation %a in the current block.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
source Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "source"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Manager_restriction" then
let '{|
Manager_restriction.source := source;
Manager_restriction.conflict := conflict
|} := cast Manager_restriction payload in
Some (source, conflict)
else None
end)
(fun (function_parameter :
Signature.public_key_hash × operation_conflict) ⇒
let '(source, conflict) := function_parameter in
Build_extensible "Manager_restriction" Manager_restriction
{| Manager_restriction.source := source;
Manager_restriction.conflict := conflict; |}) in
let inconsistent_sources_description :=
"The operation batch includes operations from different sources." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.inconsistent_sources"
"Inconsistent sources in operation batch"
inconsistent_sources_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
inconsistent_sources_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_sources" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_sources" unit tt) in
let inconsistent_counters_description :=
"Inconsistent counters in operation. Counters of an operation must be successive."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.inconsistent_counters"
"Inconsistent counters in operation" inconsistent_counters_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
inconsistent_counters_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_counters" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_counters" unit tt) in
let incorrect_reveal_description :=
"Incorrect reveal operation position in batch: only allowed in first position."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.incorrect_reveal_position"
"Incorrect reveal position" incorrect_reveal_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
incorrect_reveal_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Incorrect_reveal_position" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Incorrect_reveal_position" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.insufficient_gas_for_manager"
"Not enough gas for initial manager cost"
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Gas limit is too low to cover the initial cost of manager operations: a minimum of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" gas units is required."
CamlinternalFormatBasics.End_of_format)))
"Gas limit is too low to cover the initial cost of manager operations: a minimum of %a gas units is required.")
Alpha_context.Gas.pp_cost_as_gas
Michelson_v1_gas.Cost_of.manager_operation) None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Insufficient_gas_for_manager" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Insufficient_gas_for_manager" unit tt) in
let gas_deserialize_description :=
"Gas limit was not high enough to deserialize the transaction parameters or origination script code or initial storage etc., making the operation impossible to parse within the provided gas bounds."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.gas_quota_exceeded_init_deserialize"
"Not enough gas for initial deserialization of script expressions"
gas_deserialize_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
gas_deserialize_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Gas_quota_exceeded_init_deserialize" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.tx_rollup_is_disabled" "Tx rollup is disabled"
"Cannot originate a tx rollup as it is disabled."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal"
CamlinternalFormatBasics.End_of_format)
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_feature_disabled" unit tt) in
let scoru_disabled_description :=
"Smart contract rollups will be enabled in a future proposal." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.sc_rollup_disabled"
"Smart contract rollups are disabled" scoru_disabled_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
scoru_disabled_description)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_feature_disabled" unit tt) in
let zkru_disabled_description :=
"ZK rollups will be enabled in a future proposal." in
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.zk_rollup_disabled" "ZK rollups are disabled"
zkru_disabled_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
zkru_disabled_description)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_feature_disabled" unit tt).
End Manager.
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
"validate.operation.manager_restriction" "Manager restriction"
"An operation with the same manager has already been validated in the current block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Signature.public_key_hash × operation_conflict) ⇒
let
'(source,
Operation_conflict {|
operation_conflict.Operation_conflict.existing := existing
|}) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Manager "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" already has the operation "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" in the current block."
CamlinternalFormatBasics.End_of_format)))))
"Manager %a already has the operation %a in the current block.")
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
source Operation_hash.pp existing))
(Data_encoding.obj2
(Data_encoding.req None None "source"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "conflict" operation_conflict_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Manager_restriction" then
let '{|
Manager_restriction.source := source;
Manager_restriction.conflict := conflict
|} := cast Manager_restriction payload in
Some (source, conflict)
else None
end)
(fun (function_parameter :
Signature.public_key_hash × operation_conflict) ⇒
let '(source, conflict) := function_parameter in
Build_extensible "Manager_restriction" Manager_restriction
{| Manager_restriction.source := source;
Manager_restriction.conflict := conflict; |}) in
let inconsistent_sources_description :=
"The operation batch includes operations from different sources." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.inconsistent_sources"
"Inconsistent sources in operation batch"
inconsistent_sources_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
inconsistent_sources_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_sources" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_sources" unit tt) in
let inconsistent_counters_description :=
"Inconsistent counters in operation. Counters of an operation must be successive."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.inconsistent_counters"
"Inconsistent counters in operation" inconsistent_counters_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
inconsistent_counters_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_counters" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Inconsistent_counters" unit tt) in
let incorrect_reveal_description :=
"Incorrect reveal operation position in batch: only allowed in first position."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.incorrect_reveal_position"
"Incorrect reveal position" incorrect_reveal_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
incorrect_reveal_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Incorrect_reveal_position" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Incorrect_reveal_position" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.insufficient_gas_for_manager"
"Not enough gas for initial manager cost"
(Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Gas limit is too low to cover the initial cost of manager operations: a minimum of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" gas units is required."
CamlinternalFormatBasics.End_of_format)))
"Gas limit is too low to cover the initial cost of manager operations: a minimum of %a gas units is required.")
Alpha_context.Gas.pp_cost_as_gas
Michelson_v1_gas.Cost_of.manager_operation) None Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Insufficient_gas_for_manager" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Insufficient_gas_for_manager" unit tt) in
let gas_deserialize_description :=
"Gas limit was not high enough to deserialize the transaction parameters or origination script code or initial storage etc., making the operation impossible to parse within the provided gas bounds."
in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.gas_quota_exceeded_init_deserialize"
"Not enough gas for initial deserialization of script expressions"
gas_deserialize_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
gas_deserialize_description)) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Gas_quota_exceeded_init_deserialize" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Gas_quota_exceeded_init_deserialize" unit tt) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.tx_rollup_is_disabled" "Tx rollup is disabled"
"Cannot originate a tx rollup as it is disabled."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal"
CamlinternalFormatBasics.End_of_format)
"Cannot apply a tx rollup operation as it is disabled. This feature will be enabled in a future proposal")))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Tx_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Tx_rollup_feature_disabled" unit tt) in
let scoru_disabled_description :=
"Smart contract rollups will be enabled in a future proposal." in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.sc_rollup_disabled"
"Smart contract rollups are disabled" scoru_disabled_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
scoru_disabled_description)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_feature_disabled" unit tt) in
let zkru_disabled_description :=
"ZK rollups will be enabled in a future proposal." in
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.zk_rollup_disabled" "ZK rollups are disabled"
zkru_disabled_description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
zkru_disabled_description)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Zk_rollup_feature_disabled" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Zk_rollup_feature_disabled" unit tt).
End Manager.
Init function; without side-effects in Coq
Definition init_module10 : unit :=
let description := "A failing_noop operation can never be validated." in
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.failing_noop_error" "Failing_noop error" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failing_noop_error" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Failing_noop_error" unit tt).
Module Block.
Module Not_enough_endorsements.
Record record : Set := Build {
required : int;
provided : int;
}.
Definition with_required required (r : record) :=
Build required r.(provided).
Definition with_provided provided (r : record) :=
Build r.(required) provided.
End Not_enough_endorsements.
Definition Not_enough_endorsements := Not_enough_endorsements.record.
Module Inconsistent_validation_passes_in_block.
Record record : Set := Build {
expected : int;
provided : int;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Inconsistent_validation_passes_in_block.
Definition Inconsistent_validation_passes_in_block :=
Inconsistent_validation_passes_in_block.record.
let description := "A failing_noop operation can never be validated." in
Error_monad.register_error_kind Error_monad.Permanent
"validate.operation.failing_noop_error" "Failing_noop error" description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Failing_noop_error" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Failing_noop_error" unit tt).
Module Block.
Module Not_enough_endorsements.
Record record : Set := Build {
required : int;
provided : int;
}.
Definition with_required required (r : record) :=
Build required r.(provided).
Definition with_provided provided (r : record) :=
Build r.(required) provided.
End Not_enough_endorsements.
Definition Not_enough_endorsements := Not_enough_endorsements.record.
Module Inconsistent_validation_passes_in_block.
Record record : Set := Build {
expected : int;
provided : int;
}.
Definition with_expected expected (r : record) :=
Build expected r.(provided).
Definition with_provided provided (r : record) :=
Build r.(expected) provided.
End Inconsistent_validation_passes_in_block.
Definition Inconsistent_validation_passes_in_block :=
Inconsistent_validation_passes_in_block.record.
Init function; without side-effects in Coq
Definition init_module11 : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.block.not_enough_endorsements" "Not enough endorsements"
"The block being validated does not include the required minimum number of endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong number of endorsements ("
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "), at least "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" are expected"
CamlinternalFormatBasics.End_of_format)))))
"Wrong number of endorsements (%i), at least %i are expected")
provided required))
(Data_encoding.obj2
(Data_encoding.req None None "required" Data_encoding.int31)
(Data_encoding.req None None "provided" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Not_enough_endorsements" then
let '{|
Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided
|} := cast Not_enough_endorsements payload in
Some (required, provided)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Build_extensible "Not_enough_endorsements" Not_enough_endorsements
{| Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided; |}) in
Error_monad.register_error_kind Error_monad.Permanent
"validate.block.inconsistent_validation_passes_in_block"
"Inconsistent validation passes in block"
"Validation of operation should be ordered by their validation passes in a block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Validation of operation should be ordered by their validation passes in a block. Got an operation with validation pass: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" while the last validated operation had the validation pass "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Validation of operation should be ordered by their validation passes in a block. Got an operation with validation pass: %d while the last validated operation had the validation pass %d.")
provided expected))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Data_encoding.int31)
(Data_encoding.req None None "provided" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_validation_passes_in_block" then
let '{|
Inconsistent_validation_passes_in_block.expected := expected;
Inconsistent_validation_passes_in_block.provided := provided
|} := cast Inconsistent_validation_passes_in_block payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Inconsistent_validation_passes_in_block"
Inconsistent_validation_passes_in_block
{| Inconsistent_validation_passes_in_block.expected := expected;
Inconsistent_validation_passes_in_block.provided := provided; |}).
End Block.
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"validate.block.not_enough_endorsements" "Not enough endorsements"
"The block being validated does not include the required minimum number of endorsements."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Wrong number of endorsements ("
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal "), at least "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_i
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" are expected"
CamlinternalFormatBasics.End_of_format)))))
"Wrong number of endorsements (%i), at least %i are expected")
provided required))
(Data_encoding.obj2
(Data_encoding.req None None "required" Data_encoding.int31)
(Data_encoding.req None None "provided" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Not_enough_endorsements" then
let '{|
Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided
|} := cast Not_enough_endorsements payload in
Some (required, provided)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(required, provided) := function_parameter in
Build_extensible "Not_enough_endorsements" Not_enough_endorsements
{| Not_enough_endorsements.required := required;
Not_enough_endorsements.provided := provided; |}) in
Error_monad.register_error_kind Error_monad.Permanent
"validate.block.inconsistent_validation_passes_in_block"
"Inconsistent validation passes in block"
"Validation of operation should be ordered by their validation passes in a block."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : int × int) ⇒
let '(expected, provided) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Validation of operation should be ordered by their validation passes in a block. Got an operation with validation pass: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" while the last validated operation had the validation pass "
(CamlinternalFormatBasics.Int
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Validation of operation should be ordered by their validation passes in a block. Got an operation with validation pass: %d while the last validated operation had the validation pass %d.")
provided expected))
(Data_encoding.obj2
(Data_encoding.req None None "expected" Data_encoding.int31)
(Data_encoding.req None None "provided" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Inconsistent_validation_passes_in_block" then
let '{|
Inconsistent_validation_passes_in_block.expected := expected;
Inconsistent_validation_passes_in_block.provided := provided
|} := cast Inconsistent_validation_passes_in_block payload in
Some (expected, provided)
else None
end)
(fun (function_parameter : int × int) ⇒
let '(expected, provided) := function_parameter in
Build_extensible "Inconsistent_validation_passes_in_block"
Inconsistent_validation_passes_in_block
{| Inconsistent_validation_passes_in_block.expected := expected;
Inconsistent_validation_passes_in_block.provided := provided; |}).
End Block.