Skip to main content

👥 Delegate_cycles.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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_missed_endorsements_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_sampler.
Require TezosOfOCaml.Proto_alpha.Delegate_slashed_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Misc.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.

Definition update_activity
  (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
  : M? (Raw_context.t × list Signature.public_key_hash) :=
  let preserved := Constants_storage.preserved_cycles ctxt in
  let? res := Cycle_repr.sub last_cycle preserved in
  match res with
  | Nonereturn? (ctxt, nil)
  | Some _unfrozen_cycle
    let? '(ctxt, deactivated) :=
      Stake_storage.fold_on_active_delegates_with_minimal_stake ctxt
        (Variant.Build "Sorted" unit tt) (ctxt, nil)
        (fun (delegate : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter :
              Raw_context.t × list Signature.public_key_hash) ⇒
              let '(ctxt, deactivated) := function_parameter in
              let? cycle :=
                Delegate_activation_storage.last_cycle_before_deactivation ctxt
                  delegate in
              if Cycle_repr.op_lteq cycle last_cycle then
                let ctxt := Stake_storage.set_inactive ctxt delegate in
                return? (ctxt, (cons delegate deactivated))
              else
                return? (ctxt, deactivated)) in
    return? (ctxt, deactivated)
  end.

Definition max_frozen_deposits_and_delegates_to_remove
  (ctxt : Raw_context.t) (from_cycle : Cycle_repr.cycle)
  (to_cycle : Cycle_repr.cycle)
  : M?
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
      Tez_repr.t ×
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t)) :=
  let frozen_deposits_percentage :=
    Constants_storage.frozen_deposits_percentage ctxt in
  let cycles := Cycle_repr.op_minusminusminusgt from_cycle to_cycle in
  let? cleared_cycle_delegates :=
    match Cycle_repr.pred from_cycle with
    | None
      return?
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
    | Some cleared_cycle
      let? cleared_cycle_delegates :=
        Stake_storage.find_selected_distribution ctxt cleared_cycle in
      match cleared_cycle_delegates with
      | None
        return?
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
      | Some delegates
        return?
          (List.fold_left
            (fun (set :
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
              ⇒
              fun (function_parameter : Signature.public_key_hash × Tez_repr.t)
                ⇒
                let '(d_value, _) := function_parameter in
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.add)
                  d_value set)
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
            delegates)
      end
    end in
  List.fold_left_es
    (fun (function_parameter :
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
        Tez_repr.t ×
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
      ⇒
      let '(maxima, delegates_to_remove) := function_parameter in
      fun (cycle : Cycle_repr.t) ⇒
        let? active_stakes := Stake_storage.get_selected_distribution ctxt cycle
          in
        return?
          (List.fold_left
            (fun (function_parameter :
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
                Tez_repr.t ×
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
              ⇒
              let '(maxima, delegates_to_remove) := function_parameter in
              fun (function_parameter : Signature.public_key_hash × Tez_repr.t)
                ⇒
                let '(delegate, stake) := function_parameter in
                let stake_to_be_deposited :=
                  Tez_repr.div_exn
                    (Tez_repr.mul_exn stake frozen_deposits_percentage) 100 in
                let maxima :=
                  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.update)
                    delegate
                    (fun (function_parameter : option Tez_repr.t) ⇒
                      match function_parameter with
                      | NoneSome stake_to_be_deposited
                      | Some maximum
                        Some (Tez_repr.max maximum stake_to_be_deposited)
                      end) maxima in
                let delegates_to_remove :=
                  Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.remove)
                    delegate delegates_to_remove in
                (maxima, delegates_to_remove)) (maxima, delegates_to_remove)
            active_stakes))
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty),
      cleared_cycle_delegates) cycles.

Definition freeze_deposits (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t Cycle_repr.cycle
  list
    (Receipt_repr.balance × Receipt_repr.balance_update ×
      Receipt_repr.update_origin)
  M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (ctxt : Raw_context.t) ⇒
    fun (new_cycle : Cycle_repr.cycle) ⇒
      fun (balance_updates :
        list
          (Receipt_repr.balance × Receipt_repr.balance_update ×
            Receipt_repr.update_origin)) ⇒
        let max_slashable_period := Constants_storage.max_slashing_period ctxt
          in
        let? res := Cycle_repr.sub new_cycle (max_slashable_period -i 1) in
        let? from_cycle :=
          match res with
          | None
            let? first_level_of_protocol :=
              Storage.Tenderbake.First_level_of_protocol.(Storage_sigs.Single_data_storage.get)
                ctxt in
            let cycle_eras := Raw_context.cycle_eras ctxt in
            let? level :=
              Level_repr.level_from_raw cycle_eras first_level_of_protocol in
            return? level.(Level_repr.t.cycle)
          | Some cyclereturn? cycle
          end in
        let preserved_cycles := Constants_storage.preserved_cycles ctxt in
        let? to_cycle := Cycle_repr.add new_cycle preserved_cycles in
        let? '(maxima, delegates_to_remove) :=
          max_frozen_deposits_and_delegates_to_remove ctxt from_cycle to_cycle
          in
        let? '(ctxt, balance_updates) :=
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.fold_es)
            (fun (delegate : Signature.public_key_hash) ⇒
              fun (maximum_stake_to_be_deposited : Tez_repr.t) ⇒
                fun (function_parameter :
                  Raw_context.t ×
                    list
                      (Receipt_repr.balance × Receipt_repr.balance_update ×
                        Receipt_repr.update_origin)) ⇒
                  let '(ctxt, balance_updates) := function_parameter in
                  let delegate_contract := Contract_repr.Implicit delegate in
                  let? ctxt :=
                    Frozen_deposits_storage.update_initial_amount ctxt
                      delegate_contract maximum_stake_to_be_deposited in
                  let? deposits :=
                    Frozen_deposits_storage.get ctxt delegate_contract in
                  let current_amount :=
                    deposits.(Storage.deposits.current_amount) in
                  if
                    Tez_repr.op_gt current_amount maximum_stake_to_be_deposited
                  then
                    let? to_reimburse :=
                      Tez_repr.op_minusquestion current_amount
                        maximum_stake_to_be_deposited in
                    let? '(ctxt, bupds) :=
                      Token.transfer (Some origin) ctxt
                        (Token.Source_container (Token.Frozen_deposits delegate))
                        (Token.Sink_container (Token.Delegate_balance delegate))
                        to_reimburse in
                    return? (ctxt, (Pervasives.op_at bupds balance_updates))
                  else
                    if
                      Tez_repr.op_lt current_amount
                        maximum_stake_to_be_deposited
                    then
                      let? desired_to_freeze :=
                        Tez_repr.op_minusquestion maximum_stake_to_be_deposited
                          current_amount in
                      let? balance :=
                        Delegate_storage.spendable_balance ctxt delegate in
                      let to_freeze := Tez_repr.min balance desired_to_freeze in
                      let? '(ctxt, bupds) :=
                        Token.transfer (Some origin) ctxt
                          (Token.Source_container
                            (Token.Delegate_balance delegate))
                          (Token.Sink_container (Token.Frozen_deposits delegate))
                          to_freeze in
                      return? (ctxt, (Pervasives.op_at bupds balance_updates))
                    else
                      return? (ctxt, balance_updates)) maxima
            (ctxt, balance_updates) in
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.fold_es)
          (fun (delegate : Signature.public_key_hash) ⇒
            fun (function_parameter :
              Raw_context.t ×
                list
                  (Receipt_repr.balance × Receipt_repr.balance_update ×
                    Receipt_repr.update_origin)) ⇒
              let '(ctxt, balance_updates) := function_parameter in
              let delegate_contract := Contract_repr.Implicit delegate in
              let? ctxt :=
                Frozen_deposits_storage.update_initial_amount ctxt
                  delegate_contract Tez_repr.zero in
              let? frozen_deposits :=
                Frozen_deposits_storage.get ctxt delegate_contract in
              if
                Tez_repr.op_gt frozen_deposits.(Storage.deposits.current_amount)
                  Tez_repr.zero
              then
                let? '(ctxt, bupds) :=
                  Token.transfer (Some origin) ctxt
                    (Token.Source_container (Token.Frozen_deposits delegate))
                    (Token.Sink_container (Token.Delegate_balance delegate))
                    frozen_deposits.(Storage.deposits.current_amount) in
                return? (ctxt, (Pervasives.op_at bupds balance_updates))
              else
                return? (ctxt, balance_updates)) delegates_to_remove
          (ctxt, balance_updates).

Definition delegate_has_revealed_nonces
  (delegate : Signature.public_key_hash)
  (unrevelead_nonces_set :
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
  : bool :=
  Pervasives.not
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.mem)
      delegate unrevelead_nonces_set).

Definition distribute_endorsing_rewards
  (ctxt : Raw_context.t) (last_cycle : Cycle_repr.t)
  (unrevealed_nonces : list Storage.Seed.unrevealed_nonce)
  : M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let endorsing_reward_per_slot :=
    Constants_storage.endorsing_reward_per_slot ctxt in
  let unrevealed_nonces_set :=
    List.fold_left
      (fun (set :
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.t))
        ⇒
        fun (function_parameter : Storage.Seed.unrevealed_nonce) ⇒
          let '{|
            Storage.Cycle.unrevealed_nonce.nonce_hash := _;
              Storage.Cycle.unrevealed_nonce.delegate := delegate
              |} := function_parameter in
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.add)
            delegate set)
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH._Set).(S.INDEXES_SET.empty)
      unrevealed_nonces in
  let? total_active_stake :=
    Stake_storage.get_total_active_stake ctxt last_cycle in
  let? delegates := Stake_storage.get_selected_distribution ctxt last_cycle in
  List.fold_left_es
    (fun (function_parameter :
      Raw_context.t ×
        list
          (Receipt_repr.balance × Receipt_repr.balance_update ×
            Receipt_repr.update_origin)) ⇒
      let '(ctxt, balance_updates) := function_parameter in
      fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
        let '(delegate, active_stake) := function_parameter in
        let delegate_contract := Contract_repr.Implicit delegate in
        let? '(ctxt, sufficient_participation) :=
          Delegate_missed_endorsements_storage.check_and_reset_delegate_participation
            ctxt delegate in
        let has_revealed_nonces :=
          delegate_has_revealed_nonces delegate unrevealed_nonces_set in
        let expected_slots :=
          Delegate_missed_endorsements_storage.expected_slots_for_given_active_stake
            ctxt total_active_stake active_stake in
        let rewards := Tez_repr.mul_exn endorsing_reward_per_slot expected_slots
          in
        if sufficient_participation && has_revealed_nonces then
          let? '(ctxt, payed_rewards_receipts) :=
            Token.transfer None ctxt
              (Token.Source_infinite Token.Endorsing_rewards)
              (Token.Sink_container (Token.Contract delegate_contract)) rewards
            in
          return?
            (ctxt, (Pervasives.op_at payed_rewards_receipts balance_updates))
        else
          let? '(ctxt, payed_rewards_receipts) :=
            Token.transfer None ctxt
              (Token.Source_infinite Token.Endorsing_rewards)
              (Token.Sink_infinite
                (Token.Lost_endorsing_rewards delegate
                  (Pervasives.not sufficient_participation)
                  (Pervasives.not has_revealed_nonces))) rewards in
          return?
            (ctxt, (Pervasives.op_at payed_rewards_receipts balance_updates)))
    (ctxt, nil) delegates.

Definition cycle_end (ctxt : Raw_context.t) (last_cycle : Cycle_repr.t)
  : M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin) × list Signature.public_key_hash) :=
  let? '(ctxt, unrevealed_nonces) := Seed_storage.cycle_end ctxt last_cycle in
  let? new_cycle := Cycle_repr.add last_cycle 1 in
  let? ctxt :=
    Delegate_sampler.select_new_distribution_at_cycle_end ctxt new_cycle in
  let? ctxt := Delegate_consensus_key.activate ctxt new_cycle in
  let? ctxt :=
    Delegate_slashed_deposits_storage.clear_outdated_slashed_deposits ctxt
      new_cycle in
  let? '(ctxt, balance_updates) :=
    distribute_endorsing_rewards ctxt last_cycle unrevealed_nonces in
  let? '(ctxt, balance_updates) :=
    freeze_deposits None ctxt new_cycle balance_updates in
  let? ctxt := Stake_storage.clear_at_cycle_end ctxt new_cycle in
  let? ctxt := Delegate_sampler.clear_outdated_sampling_data ctxt new_cycle in
  let? '(ctxt, deactivated_delagates) := update_activity ctxt last_cycle in
  return? (ctxt, balance_updates, deactivated_delagates).

Definition init_first_cycles
  (ctxt : Raw_context.t) (origin : Receipt_repr.update_origin)
  : M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let preserved := Constants_storage.preserved_cycles ctxt in
  let? ctxt :=
    List.fold_left_es
      (fun (ctxt : Raw_context.t) ⇒
        fun (c_value : int) ⇒
          let cycle := Cycle_repr.of_int32_exn (Int32.of_int c_value) in
          let? ctxt := Stake_storage.snapshot_value ctxt in
          Delegate_sampler.select_distribution_for_cycle ctxt cycle) ctxt
      (Misc.op_minusminusgt 0 preserved) in
  let cycle := (Raw_context.current_level ctxt).(Level_repr.t.cycle) in
  freeze_deposits (Some origin) ctxt cycle nil.