👥 Delegate_cycles.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.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
| None ⇒ return? (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
| None ⇒ Some 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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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 cycle ⇒ return? 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.
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
| None ⇒ return? (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
| None ⇒ Some 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_starsthstar ⇒ op_starsthstar
| None ⇒ Receipt_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 cycle ⇒ return? 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.