Skip to main content

👥 Delegate_services.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Require TezosOfOCaml.Proto_alpha.Storage.

Init function; without side-effects in Coq
Definition init_module1 : unit :=
  Error_monad.register_error_kind Error_monad.Temporary
    "delegate.not_registered" "Not a registered delegate"
    "The provided public key hash is not the address of a registered delegate."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "The provided public key hash ("
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    ") is not the address of a registered delegate. If you own this account and want to register it as a delegate, use a delegation operation to delegate the account to itself."
                    CamlinternalFormatBasics.End_of_format)))
              "The provided public key hash (%a) is not the address of a registered delegate. If you own this account and want to register it as a delegate, use a delegation operation to delegate the account to itself.")
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
    (Data_encoding.obj1
      (Data_encoding.req None None "pkh"
        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 "Not_registered" then
          let pkh := cast Signature.public_key_hash payload in
          Some pkh
        else None
      end)
    (fun (pkh : Signature.public_key_hash) ⇒
      Build_extensible "Not_registered" Signature.public_key_hash pkh).

Init function; without side-effects in Coq
Definition init_module2 : unit :=
  Error_monad.register_error_kind Error_monad.Temporary
    "delegate_service.balance_rpc_on_non_delegate"
    "Balance request for an unregistered delegate"
    "The account whose balance was requested is not a delegate."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "The implicit account ("
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    ") whose balance was requested is not a registered delegate. To get the balance of this account you can use the ../context/contracts/"
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal "/balance RPC."
                        CamlinternalFormatBasics.End_of_format)))))
              "The implicit account (%a) whose balance was requested is not a registered delegate. To get the balance of this account you can use the ../context/contracts/%a/balance RPC.")
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) pkh))
    (Data_encoding.obj1
      (Data_encoding.req None None "pkh"
        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 "Balance_rpc_non_delegate" then
          let pkh := cast Alpha_context.public_key_hash payload in
          Some pkh
        else None
      end)
    (fun (pkh : Signature.public_key_hash) ⇒
      Build_extensible "Balance_rpc_non_delegate" Signature.public_key_hash pkh).

Module info.
  Record record : Set := Build {
    full_balance : Alpha_context.Tez.t;
    current_frozen_deposits : Alpha_context.Tez.t;
    frozen_deposits : Alpha_context.Tez.t;
    staking_balance : Alpha_context.Tez.t;
    frozen_deposits_limit : option Alpha_context.Tez.t;
    delegated_contracts : list Alpha_context.Contract.t;
    delegated_balance : Alpha_context.Tez.t;
    deactivated : bool;
    grace_period : Alpha_context.Cycle.t;
    voting_info : Alpha_context.Vote.delegate_info;
    active_consensus_key : Signature.public_key_hash;
    pending_consensus_keys :
      list (Alpha_context.Cycle.t × Signature.public_key_hash);
  }.
  Definition with_full_balance full_balance (r : record) :=
    Build full_balance r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_current_frozen_deposits current_frozen_deposits
    (r : record) :=
    Build r.(full_balance) current_frozen_deposits r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_frozen_deposits frozen_deposits (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) frozen_deposits
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_staking_balance staking_balance (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      staking_balance r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_frozen_deposits_limit frozen_deposits_limit (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) frozen_deposits_limit r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_delegated_contracts delegated_contracts (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) delegated_contracts
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_delegated_balance delegated_balance (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      delegated_balance r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_deactivated deactivated (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) deactivated r.(grace_period) r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_grace_period grace_period (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) grace_period r.(voting_info)
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_voting_info voting_info (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) voting_info
      r.(active_consensus_key) r.(pending_consensus_keys).
  Definition with_active_consensus_key active_consensus_key (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      active_consensus_key r.(pending_consensus_keys).
  Definition with_pending_consensus_keys pending_consensus_keys (r : record) :=
    Build r.(full_balance) r.(current_frozen_deposits) r.(frozen_deposits)
      r.(staking_balance) r.(frozen_deposits_limit) r.(delegated_contracts)
      r.(delegated_balance) r.(deactivated) r.(grace_period) r.(voting_info)
      r.(active_consensus_key) pending_consensus_keys.
End info.
Definition info := info.record.

Definition info_encoding : Data_encoding.encoding info :=
  Data_encoding.conv
    (fun (function_parameter : info) ⇒
      let '{|
        info.full_balance := full_balance;
          info.current_frozen_deposits := current_frozen_deposits;
          info.frozen_deposits := frozen_deposits;
          info.staking_balance := staking_balance;
          info.frozen_deposits_limit := frozen_deposits_limit;
          info.delegated_contracts := delegated_contracts;
          info.delegated_balance := delegated_balance;
          info.deactivated := deactivated;
          info.grace_period := grace_period;
          info.voting_info := voting_info;
          info.active_consensus_key := active_consensus_key;
          info.pending_consensus_keys := pending_consensus_keys
          |} := function_parameter in
      ((full_balance, current_frozen_deposits, frozen_deposits, staking_balance,
        frozen_deposits_limit, delegated_contracts, delegated_balance,
        deactivated, grace_period),
        (voting_info, (active_consensus_key, pending_consensus_keys))))
    (fun (function_parameter :
      (Alpha_context.Tez.t × Alpha_context.Tez.t × Alpha_context.Tez.t ×
        Alpha_context.Tez.t × option Alpha_context.Tez.t ×
        list Alpha_context.Contract.t × Alpha_context.Tez.t × bool ×
        Alpha_context.Cycle.t) ×
        (Alpha_context.Vote.delegate_info ×
          (Signature.public_key_hash ×
            list (Alpha_context.Cycle.t × Signature.public_key_hash)))) ⇒
      let
        '((full_balance, current_frozen_deposits, frozen_deposits,
          staking_balance, frozen_deposits_limit, delegated_contracts,
          delegated_balance, deactivated, grace_period),
          (voting_info, (active_consensus_key, pending_consensus_keys))) :=
        function_parameter in
      {| info.full_balance := full_balance;
        info.current_frozen_deposits := current_frozen_deposits;
        info.frozen_deposits := frozen_deposits;
        info.staking_balance := staking_balance;
        info.frozen_deposits_limit := frozen_deposits_limit;
        info.delegated_contracts := delegated_contracts;
        info.delegated_balance := delegated_balance;
        info.deactivated := deactivated; info.grace_period := grace_period;
        info.voting_info := voting_info;
        info.active_consensus_key := active_consensus_key;
        info.pending_consensus_keys := pending_consensus_keys; |}) None
    (Data_encoding.merge_objs
      (Data_encoding.obj9
        (Data_encoding.req None None "full_balance" Alpha_context.Tez.encoding)
        (Data_encoding.req None None "current_frozen_deposits"
          Alpha_context.Tez.encoding)
        (Data_encoding.req None None "frozen_deposits"
          Alpha_context.Tez.encoding)
        (Data_encoding.req None None "staking_balance"
          Alpha_context.Tez.encoding)
        (Data_encoding.opt None None "frozen_deposits_limit"
          Alpha_context.Tez.encoding)
        (Data_encoding.req None None "delegated_contracts"
          (Data_encoding.list_value None Alpha_context.Contract.encoding))
        (Data_encoding.req None None "delegated_balance"
          Alpha_context.Tez.encoding)
        (Data_encoding.req None None "deactivated" Data_encoding.bool_value)
        (Data_encoding.req None None "grace_period" Alpha_context.Cycle.encoding))
      (Data_encoding.merge_objs Alpha_context.Vote.delegate_info_encoding
        (Data_encoding.obj2
          (Data_encoding.req None None "active_consensus_key"
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
          (Data_encoding.dft None None "pending_consensus_keys"
            (Data_encoding.list_value None
              (Data_encoding.obj2
                (Data_encoding.req None None "cycle"
                  Alpha_context.Cycle.encoding)
                (Data_encoding.req None None "pkh"
                  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))))
            nil)))).

Definition participation_info_encoding
  : Data_encoding.encoding Alpha_context.Delegate.participation_info :=
  Data_encoding.conv
    (fun (function_parameter : Alpha_context.Delegate.participation_info) ⇒
      let '{|
        Alpha_context.Delegate.participation_info.expected_cycle_activity :=
          expected_cycle_activity;
          Alpha_context.Delegate.participation_info.minimal_cycle_activity :=
            minimal_cycle_activity;
          Alpha_context.Delegate.participation_info.missed_slots := missed_slots;
          Alpha_context.Delegate.participation_info.missed_levels :=
            missed_levels;
          Alpha_context.Delegate.participation_info.remaining_allowed_missed_slots
            := remaining_allowed_missed_slots;
          Alpha_context.Delegate.participation_info.expected_endorsing_rewards
            := expected_endorsing_rewards
          |} := function_parameter in
      (expected_cycle_activity, minimal_cycle_activity, missed_slots,
        missed_levels, remaining_allowed_missed_slots,
        expected_endorsing_rewards))
    (fun (function_parameter :
      int × int × int × int × int × Alpha_context.Tez.t) ⇒
      let
        '(expected_cycle_activity, minimal_cycle_activity, missed_slots,
          missed_levels, remaining_allowed_missed_slots,
          expected_endorsing_rewards) := function_parameter in
      {|
        Alpha_context.Delegate.participation_info.expected_cycle_activity :=
          expected_cycle_activity;
        Alpha_context.Delegate.participation_info.minimal_cycle_activity :=
          minimal_cycle_activity;
        Alpha_context.Delegate.participation_info.missed_slots := missed_slots;
        Alpha_context.Delegate.participation_info.missed_levels :=
          missed_levels;
        Alpha_context.Delegate.participation_info.remaining_allowed_missed_slots
          := remaining_allowed_missed_slots;
        Alpha_context.Delegate.participation_info.expected_endorsing_rewards :=
          expected_endorsing_rewards; |}) None
    (Data_encoding.obj6
      (Data_encoding.req None None "expected_cycle_activity" Data_encoding.int31)
      (Data_encoding.req None None "minimal_cycle_activity" Data_encoding.int31)
      (Data_encoding.req None None "missed_slots" Data_encoding.int31)
      (Data_encoding.req None None "missed_levels" Data_encoding.int31)
      (Data_encoding.req None None "remaining_allowed_missed_slots"
        Data_encoding.int31)
      (Data_encoding.req None None "expected_endorsing_rewards"
        Alpha_context.Tez.encoding)).

Module S.
  Definition raw_path : RPC_path.path Updater.rpc_context Updater.rpc_context :=
    RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "delegates".

  Module list_query.
    Record record : Set := Build {
      active : bool;
      inactive : bool;
      with_minimal_stake : bool;
      without_minimal_stake : bool;
    }.
    Definition with_active active (r : record) :=
      Build active r.(inactive) r.(with_minimal_stake)
        r.(without_minimal_stake).
    Definition with_inactive inactive (r : record) :=
      Build r.(active) inactive r.(with_minimal_stake)
        r.(without_minimal_stake).
    Definition with_with_minimal_stake with_minimal_stake (r : record) :=
      Build r.(active) r.(inactive) with_minimal_stake
        r.(without_minimal_stake).
    Definition with_without_minimal_stake without_minimal_stake (r : record) :=
      Build r.(active) r.(inactive) r.(with_minimal_stake)
        without_minimal_stake.
  End list_query.
  Definition list_query := list_query.record.

  Definition list_query_value : RPC_query.t list_query :=
    RPC_query.seal
      (RPC_query.op_pipeplus
        (RPC_query.op_pipeplus
          (RPC_query.op_pipeplus
            (RPC_query.op_pipeplus
              (RPC_query.query_value
                (fun (active : bool) ⇒
                  fun (inactive : bool) ⇒
                    fun (with_minimal_stake : bool) ⇒
                      fun (without_minimal_stake : bool) ⇒
                        {| list_query.active := active;
                          list_query.inactive := inactive;
                          list_query.with_minimal_stake := with_minimal_stake;
                          list_query.without_minimal_stake :=
                            without_minimal_stake; |}))
              (RPC_query.flag None "active"
                (fun (t_value : list_query) ⇒ t_value.(list_query.active))))
            (RPC_query.flag None "inactive"
              (fun (t_value : list_query) ⇒ t_value.(list_query.inactive))))
          (RPC_query.flag None "with_minimal_stake"
            (fun (t_value : list_query) ⇒
              t_value.(list_query.with_minimal_stake))))
        (RPC_query.flag None "without_minimal_stake"
          (fun (t_value : list_query) ⇒
            t_value.(list_query.without_minimal_stake)))).

  Definition list_delegate
    : RPC_service.service Updater.rpc_context Updater.rpc_context list_query
      unit (list Signature.public_key_hash) :=
    RPC_service.get_service
      (Some
        "Lists all registered delegates by default. The arguments `active`, `inactive`, `with_minimal_stake`, and `without_minimal_stake` allow to enumerate only the delegates that are active, inactive, have at least a minimal stake to participate in consensus and in governance, or do not have such a minimal stake, respectively. Note, setting these arguments to false has no effect.")
      list_query_value
      (Data_encoding.list_value None
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      raw_path.

  Definition path
    : RPC_path.path Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) :=
    RPC_path.op_divcolon raw_path
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg).

  Definition info_value
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit info :=
    RPC_service.get_service (Some "Everything about a delegate.")
      RPC_query.empty info_encoding path.

  Definition full_balance
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Tez.t :=
    RPC_service.get_service
      (Some
        "Returns the full balance (in mutez) of a given delegate, including the frozen deposits and the frozen bonds. It does not include its delegated balance.")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div path "full_balance").

  Definition current_frozen_deposits
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Tez.t :=
    RPC_service.get_service
      (Some "Returns the current amount of the frozen deposits (in mutez).")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div path "current_frozen_deposits").

  Definition frozen_deposits
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Tez.t :=
    RPC_service.get_service
      (Some
        "Returns the initial amount (that is, at the beginning of a cycle) of the frozen deposits (in mutez). This amount is the same as the current amount of the frozen deposits, unless the delegate has been punished.")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div path "frozen_deposits").

  Definition staking_balance
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Tez.t :=
    RPC_service.get_service
      (Some
        "Returns the total amount of tokens (in mutez) delegated to a given delegate. This includes the balances of all the contracts that delegate to it, but also the balance of the delegate itself, its frozen deposits, and its frozen bonds.")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div path "staking_balance").

  Definition frozen_deposits_limit
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      (option Alpha_context.Tez.t) :=
    RPC_service.get_service
      (Some
        "Returns the frozen deposits limit for the given delegate or none if no limit is set.")
      RPC_query.empty (Data_encoding.option_value Alpha_context.Tez.encoding)
      (RPC_path.op_div path "frozen_deposits_limit").

  Definition delegated_contracts
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      (list Alpha_context.Contract.t) :=
    RPC_service.get_service
      (Some "Returns the list of contracts that delegate to a given delegate.")
      RPC_query.empty
      (Data_encoding.list_value None Alpha_context.Contract.encoding)
      (RPC_path.op_div path "delegated_contracts").

  Definition delegated_balance
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Tez.t :=
    RPC_service.get_service
      (Some
        "Returns the sum (in mutez) of all balances of all the contracts that delegate to a given delegate. This excludes the delegate's own balance, its frozen deposits and its frozen bonds.")
      RPC_query.empty Alpha_context.Tez.encoding
      (RPC_path.op_div path "delegated_balance").

  Definition deactivated
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit bool :=
    RPC_service.get_service
      (Some
        "Tells whether the delegate is currently tagged as deactivated or not.")
      RPC_query.empty Data_encoding.bool_value
      (RPC_path.op_div path "deactivated").

  Definition grace_period
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Cycle.t :=
    RPC_service.get_service
      (Some
        "Returns the cycle by the end of which the delegate might be deactivated if she fails to execute any delegate action. A deactivated delegate might be reactivated (without loosing any stake) by simply re-registering as a delegate. For deactivated delegates, this value contains the cycle at which they were deactivated.")
      RPC_query.empty Alpha_context.Cycle.encoding
      (RPC_path.op_div path "grace_period").

  Definition voting_power
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit int64 :=
    RPC_service.get_service
      (Some "The voting power in the vote listings for a given delegate.")
      RPC_query.empty Data_encoding.int64_value
      (RPC_path.op_div path "voting_power").

  Definition voting_info
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Vote.delegate_info :=
    RPC_service.get_service
      (Some
        "Returns the delegate info (e.g. voting power) found in the listings of the current voting period.")
      RPC_query.empty Alpha_context.Vote.delegate_info_encoding
      (RPC_path.op_div path "voting_info").

  Definition consensus_key
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      (Signature.public_key_hash ×
        list (Alpha_context.Cycle.t × Signature.public_key_hash)) :=
    RPC_service.get_service
      (Some
        "The active consensus key for a given delegate and the pending consensus keys.")
      RPC_query.empty
      (Data_encoding.obj2
        (Data_encoding.req None None "active"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
        (Data_encoding.dft None None "pendings"
          (Data_encoding.list_value None
            (Data_encoding.obj2
              (Data_encoding.req None None "cycle" Alpha_context.Cycle.encoding)
              (Data_encoding.req None None "pkh"
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))))
          nil)) (RPC_path.op_div path "consensus_key").

  Definition participation
    : RPC_service.service Updater.rpc_context
      (Updater.rpc_context × Signature.public_key_hash) unit unit
      Alpha_context.Delegate.participation_info :=
    RPC_service.get_service
      (Some
        "Returns cycle and level participation information. In particular this indicates, in the field 'expected_cycle_activity', the number of slots the delegate is expected to have in the cycle based on its active stake. The field 'minimal_cycle_activity' indicates the minimal endorsing slots in the cycle required to get endorsing rewards. It is computed based on 'expected_cycle_activity. The fields 'missed_slots' and 'missed_levels' indicate the number of missed endorsing slots and missed levels (for endorsing) in the cycle so far. 'missed_slots' indicates the number of missed endorsing slots in the cycle so far. The field 'remaining_allowed_missed_slots' indicates the remaining amount of endorsing slots that can be missed in the cycle before forfeiting the rewards. Finally, 'expected_endorsing_rewards' indicates the endorsing rewards that will be distributed at the end of the cycle if activity at that point will be greater than the minimal required; if the activity is already known to be below the required minimum, then the rewards are zero.")
      RPC_query.empty participation_info_encoding
      (RPC_path.op_div path "participation").
End S.

Definition check_delegate_registered
  (ctxt : Alpha_context.context) (pkh : Alpha_context.public_key_hash)
  : M? unit :=
  let function_parameter := Alpha_context.Delegate.registered ctxt pkh in
  match function_parameter with
  | trueError_monad.return_unit
  | false
    Error_monad.fail
      (Build_extensible "Not_registered" Alpha_context.public_key_hash pkh)
  end.

Definition register (function_parameter : unit) : unit :=
  let '_ := function_parameter in
  let '_ :=
    Services_registration.register0 true S.list_delegate
      (fun (ctxt : Alpha_context.t) ⇒
        fun (q_value : S.list_query) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            let? delegates := Alpha_context.Delegate.list_value ctxt in
            let? delegates :=
              match q_value with
              | {|
                S.list_query.active := true;
                  S.list_query.inactive := false
                  |} ⇒
                List.filter_es
                  (fun (pkh : Alpha_context.public_key_hash) ⇒
                    Error_monad.op_gtpipeeqquestion
                      (Alpha_context.Delegate.deactivated ctxt pkh)
                      Pervasives.not) delegates
              | {|
                S.list_query.active := false;
                  S.list_query.inactive := true
                  |} ⇒
                List.filter_es
                  (fun (pkh : Alpha_context.public_key_hash) ⇒
                    Alpha_context.Delegate.deactivated ctxt pkh) delegates
              |
                ({|
                S.list_query.active := false;
                  S.list_query.inactive := false
                  |} | {|
                S.list_query.active := true;
                  S.list_query.inactive := true
                  |}) ⇒ return? delegates
              end in
            let minimal_stake := Alpha_context.Constants.minimal_stake ctxt in
            match q_value with
            | {|
              S.list_query.with_minimal_stake := true;
                S.list_query.without_minimal_stake := false
                |} ⇒
              List.filter_es
                (fun (pkh : Alpha_context.public_key_hash) ⇒
                  let? staking_balance :=
                    Alpha_context.Delegate.staking_balance ctxt pkh in
                  return?
                    (Alpha_context.Tez.op_gteq staking_balance minimal_stake))
                delegates
            | {|
              S.list_query.with_minimal_stake := false;
                S.list_query.without_minimal_stake := true
                |} ⇒
              List.filter_es
                (fun (pkh : Alpha_context.public_key_hash) ⇒
                  let? staking_balance :=
                    Alpha_context.Delegate.staking_balance ctxt pkh in
                  return?
                    (Alpha_context.Tez.op_lt staking_balance minimal_stake))
                delegates
            |
              ({|
              S.list_query.with_minimal_stake := true;
                S.list_query.without_minimal_stake := true
                |} | {|
              S.list_query.with_minimal_stake := false;
                S.list_query.without_minimal_stake := false
                |}) ⇒ return? delegates
            end) in
  let '_ :=
    Services_registration.register1 false S.info_value
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              let? full_balance := Alpha_context.Delegate.full_balance ctxt pkh
                in
              let? frozen_deposits :=
                Alpha_context.Delegate.frozen_deposits ctxt pkh in
              let? staking_balance :=
                Alpha_context.Delegate.staking_balance ctxt pkh in
              let? frozen_deposits_limit :=
                Alpha_context.Delegate.frozen_deposits_limit ctxt pkh in
              let? delegated_contracts :=
                Alpha_context.Delegate.delegated_contracts ctxt pkh in
              let? delegated_balance :=
                Alpha_context.Delegate.delegated_balance ctxt pkh in
              let? deactivated := Alpha_context.Delegate.deactivated ctxt pkh in
              let? grace_period :=
                Alpha_context.Delegate.last_cycle_before_deactivation ctxt pkh
                in
              let? voting_info := Alpha_context.Vote.get_delegate_info ctxt pkh
                in
              let? consensus_key :=
                Alpha_context.Delegate.Consensus_key.active_pubkey ctxt pkh in
              let? pendings :=
                Alpha_context.Delegate.Consensus_key.pending_updates ctxt pkh in
              return?
                {| info.full_balance := full_balance;
                  info.current_frozen_deposits :=
                    frozen_deposits.(Storage.deposits.current_amount);
                  info.frozen_deposits :=
                    frozen_deposits.(Storage.deposits.initial_amount);
                  info.staking_balance := staking_balance;
                  info.frozen_deposits_limit := frozen_deposits_limit;
                  info.delegated_contracts := delegated_contracts;
                  info.delegated_balance := delegated_balance;
                  info.deactivated := deactivated;
                  info.grace_period := grace_period;
                  info.voting_info := voting_info;
                  info.active_consensus_key :=
                    consensus_key.(Raw_context.consensus_pk.consensus_pkh);
                  info.pending_consensus_keys := pendings; |}) in
  let '_ :=
    Services_registration.register1 false S.full_balance
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ :=
                Error_monad.trace_value
                  (Build_extensible "Balance_rpc_non_delegate"
                    Signature.public_key_hash pkh)
                  (check_delegate_registered ctxt pkh) in
              Alpha_context.Delegate.full_balance ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.current_frozen_deposits
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              let? deposits := Alpha_context.Delegate.frozen_deposits ctxt pkh
                in
              return? deposits.(Storage.deposits.current_amount)) in
  let '_ :=
    Services_registration.register1 false S.frozen_deposits
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              let? deposits := Alpha_context.Delegate.frozen_deposits ctxt pkh
                in
              return? deposits.(Storage.deposits.initial_amount)) in
  let '_ :=
    Services_registration.register1 false S.staking_balance
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Delegate.staking_balance ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.frozen_deposits_limit
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Delegate.frozen_deposits_limit ctxt pkh) in
  let '_ :=
    Services_registration.register1 true S.delegated_contracts
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Delegate.delegated_contracts ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.delegated_balance
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Delegate.delegated_balance ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.deactivated
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Delegate.deactivated ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.grace_period
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Delegate.last_cycle_before_deactivation ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.voting_power
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Vote.get_voting_power_free ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.voting_info
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '_ := check_delegate_registered ctxt pkh in
              Alpha_context.Vote.get_delegate_info ctxt pkh) in
  let '_ :=
    Services_registration.register1 false S.consensus_key
      (fun (ctxt : Alpha_context.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? pk :=
                Alpha_context.Delegate.Consensus_key.active_pubkey ctxt pkh in
              let? pendings :=
                Alpha_context.Delegate.Consensus_key.pending_updates ctxt pkh in
              return? (pk.(Raw_context.consensus_pk.consensus_pkh), pendings))
    in
  Services_registration.register1 false S.participation
    (fun (ctxt : Alpha_context.t) ⇒
      fun (pkh : Signature.public_key_hash) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            let? '_ := check_delegate_registered ctxt pkh in
            Alpha_context.Delegate.participation_info_value ctxt pkh).

Definition list_value {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (op_staroptstar : option bool)
  : option bool option bool option bool unit
  Error_monad.shell_tzresult (list Signature.public_key_hash) :=
  let active :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | Nonetrue
    end in
  fun (op_staroptstar : option bool) ⇒
    let inactive :=
      match op_staroptstar with
      | Some op_starsthstarop_starsthstar
      | Nonefalse
      end in
    fun (op_staroptstar : option bool) ⇒
      let with_minimal_stake :=
        match op_staroptstar with
        | Some op_starsthstarop_starsthstar
        | Nonetrue
        end in
      fun (op_staroptstar : option bool) ⇒
        let without_minimal_stake :=
          match op_staroptstar with
          | Some op_starsthstarop_starsthstar
          | Nonefalse
          end in
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          RPC_context.make_call0 S.list_delegate ctxt block
            {| S.list_query.active := active; S.list_query.inactive := inactive;
              S.list_query.with_minimal_stake := with_minimal_stake;
              S.list_query.without_minimal_stake := without_minimal_stake; |} tt.

Definition info_value {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult info :=
  RPC_context.make_call1 S.info_value ctxt block pkh tt tt.

Definition full_balance {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.full_balance ctxt block pkh tt tt.

Definition current_frozen_deposits {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.current_frozen_deposits ctxt block pkh tt tt.

Definition frozen_deposits {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.frozen_deposits ctxt block pkh tt tt.

Definition staking_balance {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.staking_balance ctxt block pkh tt tt.

Definition frozen_deposits_limit {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult (option Alpha_context.Tez.t) :=
  RPC_context.make_call1 S.frozen_deposits_limit ctxt block pkh tt tt.

Definition delegated_contracts {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult (list Alpha_context.Contract.t) :=
  RPC_context.make_call1 S.delegated_contracts ctxt block pkh tt tt.

Definition delegated_balance {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Tez.t :=
  RPC_context.make_call1 S.delegated_balance ctxt block pkh tt tt.

Definition deactivated {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult bool :=
  RPC_context.make_call1 S.deactivated ctxt block pkh tt tt.

Definition grace_period {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Cycle.t :=
  RPC_context.make_call1 S.grace_period ctxt block pkh tt tt.

Definition voting_power {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult int64 :=
  RPC_context.make_call1 S.voting_power ctxt block pkh tt tt.

Definition voting_info {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Vote.delegate_info :=
  RPC_context.make_call1 S.voting_info ctxt block pkh tt tt.

Definition consensus_key {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult
    (Signature.public_key_hash ×
      list (Alpha_context.Cycle.t × Signature.public_key_hash)) :=
  RPC_context.make_call1 S.consensus_key ctxt block pkh tt tt.

Definition participation {A : Set}
  (ctxt : RPC_context.simple A) (block : A) (pkh : Signature.public_key_hash)
  : Error_monad.shell_tzresult Alpha_context.Delegate.participation_info :=
  RPC_context.make_call1 S.participation ctxt block pkh tt tt.