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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Require TezosOfOCaml.Proto_alpha.Storage.

Init function; without side-effects in Coq
Definition init_module : 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_power : int64;
  }.
  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_power).
  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_power).
  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_power).
  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_power).
  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_power).
  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_power).
  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_power).
  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_power).
  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_power).
  Definition with_voting_power voting_power (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_power.
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_power := voting_power
          |} := function_parameter in
      (full_balance, current_frozen_deposits, frozen_deposits, staking_balance,
        frozen_deposits_limit, delegated_contracts, delegated_balance,
        deactivated, grace_period, voting_power))
    (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 × int64) ⇒
      let
        '(full_balance, current_frozen_deposits, frozen_deposits,
          staking_balance, frozen_deposits_limit, delegated_contracts,
          delegated_balance, deactivated, grace_period, voting_power) :=
        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_power := voting_power; |}) None
    (Data_encoding.obj10
      (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.req None None "voting_power" Data_encoding.int64_value)).

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. 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.")
      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 and its frozen deposits.")
      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 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 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 : Signature.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 : Signature.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 tokens_per_roll := Alpha_context.Constants.tokens_per_roll 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 : Signature.public_key_hash) ⇒
                  let? staking_balance :=
                    Alpha_context.Delegate.staking_balance ctxt pkh in
                  return?
                    (Alpha_context.Tez.op_gteq staking_balance tokens_per_roll))
                delegates
            | {|
              S.list_query.with_minimal_stake := false;
                S.list_query.without_minimal_stake := true
                |} ⇒
              List.filter_es
                (fun (pkh : Signature.public_key_hash) ⇒
                  let? staking_balance :=
                    Alpha_context.Delegate.staking_balance ctxt pkh in
                  return?
                    (Alpha_context.Tez.op_lt staking_balance tokens_per_roll))
                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? '_ := Alpha_context.Delegate.check_delegate 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_power :=
                Alpha_context.Vote.get_voting_power_free 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_power := voting_power; |}) 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)
                  (Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate ctxt pkh in
              Error_monad.op_gtpipeeq
                (Alpha_context.Delegate.delegated_contracts ctxt pkh)
                Error_monad.ok) 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? '_ := Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate 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? '_ := Alpha_context.Delegate.check_delegate ctxt pkh in
              Alpha_context.Vote.get_voting_power_free ctxt pkh) 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? '_ := Alpha_context.Delegate.check_delegate ctxt pkh in
            Alpha_context.Delegate.delegate_participation_info 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 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.