✅ Validate_errors.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.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.

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

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.

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.

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.

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.

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.

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; |}).

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

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.

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.

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.

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.

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.