👥 Delegate_missed_endorsements_storage.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.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
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 expected_slots_for_given_active_stake
(ctxt : Raw_context.t) (total_active_stake : Tez_repr.t)
(active_stake : Tez_repr.t) : int :=
let blocks_per_cycle := Int32.to_int (Constants_storage.blocks_per_cycle ctxt)
in
let consensus_committee_size :=
Constants_storage.consensus_committee_size ctxt in
let number_of_endorsements_per_cycle :=
blocks_per_cycle ×i consensus_committee_size in
Z.to_int
(((Z.of_int64 (Tez_repr.to_mutez active_stake)) ×Z
(Z.of_int number_of_endorsements_per_cycle)) /Z
(Z.of_int64 (Tez_repr.to_mutez total_active_stake))).
Inductive level_participation : Set :=
| Participated : level_participation
| Didn't_participate : level_participation.
Definition record_endorsing_participation
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(participation : level_participation) (endorsing_power : int)
: M? Raw_context.t :=
match participation with
| Participated ⇒ Stake_storage.set_active ctxt delegate
| Didn't_participate ⇒
let contract := Contract_repr.Implicit delegate in
let? function_parameter :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
ctxt contract in
match function_parameter with
|
Some {|
Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := missed_levels
|} ⇒
let remaining_slots := remaining_slots -i endorsing_power in
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.update)
ctxt contract
{| Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := missed_levels +i 1;
|}
| None ⇒
let level := Level_storage.current ctxt in
let? stake_distribution :=
Raw_context.stake_distribution_for_current_cycle ctxt in
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find)
delegate stake_distribution with
| None ⇒
if level.(Level_repr.t.cycle_position) =i32 0 then
return? ctxt
else
Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some active_stake ⇒
let? total_active_stake :=
Stake_storage.get_total_active_stake ctxt level.(Level_repr.t.cycle)
in
let expected_slots :=
expected_slots_for_given_active_stake ctxt total_active_stake
active_stake in
let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} := Constants_storage.minimal_participation_ratio ctxt in
let minimal_activity := (expected_slots ×i numerator) /i denominator in
let maximal_inactivity := expected_slots -i minimal_activity in
let remaining_slots := maximal_inactivity -i endorsing_power in
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.init_value)
ctxt contract
{|
Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := 1; |}
end
end
end.
Definition record_baking_activity_and_pay_rewards_and_fees
(ctxt : Raw_context.t) (payload_producer : Signature.public_key_hash)
(block_producer : Signature.public_key_hash) (baking_reward : Tez_repr.t)
(reward_bonus : option Tez_repr.t)
: M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let? ctxt := Stake_storage.set_active ctxt payload_producer in
let? ctxt :=
if
Pervasives.not
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
payload_producer block_producer)
then
Stake_storage.set_active ctxt block_producer
else
return? ctxt in
let pay_payload_producer
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Raw_context.t × Receipt_repr.balance_updates) :=
let contract := Contract_repr.Implicit delegate in
let? '(ctxt, block_fees) := Token.balance ctxt Token.Block_fees in
Token.transfer_n None ctxt
[
((Token.Source_container Token.Block_fees), block_fees);
((Token.Source_infinite Token.Baking_rewards), baking_reward)
] (Token.Sink_container (Token.Contract contract)) in
let pay_block_producer
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(bonus : Tez_repr.t) : M? (Raw_context.t × Receipt_repr.balance_updates) :=
let contract := Contract_repr.Implicit delegate in
Token.transfer None ctxt (Token.Source_infinite Token.Baking_bonuses)
(Token.Sink_container (Token.Contract contract)) bonus in
let? '(ctxt, balance_updates_payload_producer) :=
pay_payload_producer ctxt payload_producer in
let? '(ctxt, balance_updates_block_producer) :=
match reward_bonus with
| Some bonus ⇒ pay_block_producer ctxt block_producer bonus
| None ⇒ return? (ctxt, nil)
end in
return?
(ctxt,
(Pervasives.op_at balance_updates_payload_producer
balance_updates_block_producer)).
Definition check_and_reset_delegate_participation
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Raw_context.t × bool) :=
let contract := Contract_repr.Implicit delegate in
let? missed :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
ctxt contract in
match missed with
| None ⇒ return? (ctxt, true)
| Some missed_endorsements ⇒
let ctxt :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.remove)
ctxt contract in
return?
(ctxt,
(missed_endorsements.(Storage.missed_endorsements_info.remaining_slots)
≥i 0))
end.
Module participation_info.
Record record : Set := Build {
expected_cycle_activity : int;
minimal_cycle_activity : int;
missed_slots : int;
missed_levels : int;
remaining_allowed_missed_slots : int;
expected_endorsing_rewards : Tez_repr.t;
}.
Definition with_expected_cycle_activity expected_cycle_activity
(r : record) :=
Build expected_cycle_activity r.(minimal_cycle_activity) r.(missed_slots)
r.(missed_levels) r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_minimal_cycle_activity minimal_cycle_activity (r : record) :=
Build r.(expected_cycle_activity) minimal_cycle_activity r.(missed_slots)
r.(missed_levels) r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_missed_slots missed_slots (r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity) missed_slots
r.(missed_levels) r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_missed_levels missed_levels (r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
r.(missed_slots) missed_levels r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_remaining_allowed_missed_slots remaining_allowed_missed_slots
(r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
r.(missed_slots) r.(missed_levels) remaining_allowed_missed_slots
r.(expected_endorsing_rewards).
Definition with_expected_endorsing_rewards expected_endorsing_rewards
(r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
r.(missed_slots) r.(missed_levels) r.(remaining_allowed_missed_slots)
expected_endorsing_rewards.
End participation_info.
Definition participation_info := participation_info.record.
Definition participation_info_value
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? participation_info :=
let level := Level_storage.current ctxt in
let? stake_distribution :=
Stake_storage.get_selected_distribution ctxt level.(Level_repr.t.cycle) in
match
List.assoc_opt Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
delegate stake_distribution with
| None ⇒
return?
{| participation_info.expected_cycle_activity := 0;
participation_info.minimal_cycle_activity := 0;
participation_info.missed_slots := 0;
participation_info.missed_levels := 0;
participation_info.remaining_allowed_missed_slots := 0;
participation_info.expected_endorsing_rewards := Tez_repr.zero; |}
| Some active_stake ⇒
let? total_active_stake :=
Stake_storage.get_total_active_stake ctxt level.(Level_repr.t.cycle) in
let expected_cycle_activity :=
expected_slots_for_given_active_stake ctxt total_active_stake active_stake
in
let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} := Constants_storage.minimal_participation_ratio ctxt in
let endorsing_reward_per_slot :=
Constants_storage.endorsing_reward_per_slot ctxt in
let minimal_cycle_activity :=
(expected_cycle_activity ×i numerator) /i denominator in
let maximal_cycle_inactivity :=
expected_cycle_activity -i minimal_cycle_activity in
let expected_endorsing_rewards :=
Tez_repr.mul_exn endorsing_reward_per_slot expected_cycle_activity in
let contract := Contract_repr.Implicit delegate in
let? missed_endorsements :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
ctxt contract in
let '(missed_slots, missed_levels, remaining_allowed_missed_slots) :=
match missed_endorsements with
| None ⇒ (0, 0, maximal_cycle_inactivity)
|
Some {|
Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := missed_levels
|} ⇒
((maximal_cycle_inactivity -i remaining_slots), missed_levels,
(Compare.Int.max 0 remaining_slots))
end in
let expected_endorsing_rewards :=
match
(missed_endorsements,
match missed_endorsements with
| Some r_value ⇒
r_value.(Storage.missed_endorsements_info.remaining_slots) <i 0
| _ ⇒ false
end) with
| (Some r_value, true) ⇒ Tez_repr.zero
| (_, _) ⇒ expected_endorsing_rewards
end in
return?
{| participation_info.expected_cycle_activity := expected_cycle_activity;
participation_info.minimal_cycle_activity := minimal_cycle_activity;
participation_info.missed_slots := missed_slots;
participation_info.missed_levels := missed_levels;
participation_info.remaining_allowed_missed_slots :=
remaining_allowed_missed_slots;
participation_info.expected_endorsing_rewards :=
expected_endorsing_rewards; |}
end.
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.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Ratio_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
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 expected_slots_for_given_active_stake
(ctxt : Raw_context.t) (total_active_stake : Tez_repr.t)
(active_stake : Tez_repr.t) : int :=
let blocks_per_cycle := Int32.to_int (Constants_storage.blocks_per_cycle ctxt)
in
let consensus_committee_size :=
Constants_storage.consensus_committee_size ctxt in
let number_of_endorsements_per_cycle :=
blocks_per_cycle ×i consensus_committee_size in
Z.to_int
(((Z.of_int64 (Tez_repr.to_mutez active_stake)) ×Z
(Z.of_int number_of_endorsements_per_cycle)) /Z
(Z.of_int64 (Tez_repr.to_mutez total_active_stake))).
Inductive level_participation : Set :=
| Participated : level_participation
| Didn't_participate : level_participation.
Definition record_endorsing_participation
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(participation : level_participation) (endorsing_power : int)
: M? Raw_context.t :=
match participation with
| Participated ⇒ Stake_storage.set_active ctxt delegate
| Didn't_participate ⇒
let contract := Contract_repr.Implicit delegate in
let? function_parameter :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
ctxt contract in
match function_parameter with
|
Some {|
Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := missed_levels
|} ⇒
let remaining_slots := remaining_slots -i endorsing_power in
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.update)
ctxt contract
{| Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := missed_levels +i 1;
|}
| None ⇒
let level := Level_storage.current ctxt in
let? stake_distribution :=
Raw_context.stake_distribution_for_current_cycle ctxt in
match
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find)
delegate stake_distribution with
| None ⇒
if level.(Level_repr.t.cycle_position) =i32 0 then
return? ctxt
else
Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some active_stake ⇒
let? total_active_stake :=
Stake_storage.get_total_active_stake ctxt level.(Level_repr.t.cycle)
in
let expected_slots :=
expected_slots_for_given_active_stake ctxt total_active_stake
active_stake in
let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} := Constants_storage.minimal_participation_ratio ctxt in
let minimal_activity := (expected_slots ×i numerator) /i denominator in
let maximal_inactivity := expected_slots -i minimal_activity in
let remaining_slots := maximal_inactivity -i endorsing_power in
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.init_value)
ctxt contract
{|
Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := 1; |}
end
end
end.
Definition record_baking_activity_and_pay_rewards_and_fees
(ctxt : Raw_context.t) (payload_producer : Signature.public_key_hash)
(block_producer : Signature.public_key_hash) (baking_reward : Tez_repr.t)
(reward_bonus : option Tez_repr.t)
: M?
(Raw_context.t ×
list
(Receipt_repr.balance × Receipt_repr.balance_update ×
Receipt_repr.update_origin)) :=
let? ctxt := Stake_storage.set_active ctxt payload_producer in
let? ctxt :=
if
Pervasives.not
(Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
payload_producer block_producer)
then
Stake_storage.set_active ctxt block_producer
else
return? ctxt in
let pay_payload_producer
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Raw_context.t × Receipt_repr.balance_updates) :=
let contract := Contract_repr.Implicit delegate in
let? '(ctxt, block_fees) := Token.balance ctxt Token.Block_fees in
Token.transfer_n None ctxt
[
((Token.Source_container Token.Block_fees), block_fees);
((Token.Source_infinite Token.Baking_rewards), baking_reward)
] (Token.Sink_container (Token.Contract contract)) in
let pay_block_producer
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(bonus : Tez_repr.t) : M? (Raw_context.t × Receipt_repr.balance_updates) :=
let contract := Contract_repr.Implicit delegate in
Token.transfer None ctxt (Token.Source_infinite Token.Baking_bonuses)
(Token.Sink_container (Token.Contract contract)) bonus in
let? '(ctxt, balance_updates_payload_producer) :=
pay_payload_producer ctxt payload_producer in
let? '(ctxt, balance_updates_block_producer) :=
match reward_bonus with
| Some bonus ⇒ pay_block_producer ctxt block_producer bonus
| None ⇒ return? (ctxt, nil)
end in
return?
(ctxt,
(Pervasives.op_at balance_updates_payload_producer
balance_updates_block_producer)).
Definition check_and_reset_delegate_participation
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Raw_context.t × bool) :=
let contract := Contract_repr.Implicit delegate in
let? missed :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
ctxt contract in
match missed with
| None ⇒ return? (ctxt, true)
| Some missed_endorsements ⇒
let ctxt :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.remove)
ctxt contract in
return?
(ctxt,
(missed_endorsements.(Storage.missed_endorsements_info.remaining_slots)
≥i 0))
end.
Module participation_info.
Record record : Set := Build {
expected_cycle_activity : int;
minimal_cycle_activity : int;
missed_slots : int;
missed_levels : int;
remaining_allowed_missed_slots : int;
expected_endorsing_rewards : Tez_repr.t;
}.
Definition with_expected_cycle_activity expected_cycle_activity
(r : record) :=
Build expected_cycle_activity r.(minimal_cycle_activity) r.(missed_slots)
r.(missed_levels) r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_minimal_cycle_activity minimal_cycle_activity (r : record) :=
Build r.(expected_cycle_activity) minimal_cycle_activity r.(missed_slots)
r.(missed_levels) r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_missed_slots missed_slots (r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity) missed_slots
r.(missed_levels) r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_missed_levels missed_levels (r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
r.(missed_slots) missed_levels r.(remaining_allowed_missed_slots)
r.(expected_endorsing_rewards).
Definition with_remaining_allowed_missed_slots remaining_allowed_missed_slots
(r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
r.(missed_slots) r.(missed_levels) remaining_allowed_missed_slots
r.(expected_endorsing_rewards).
Definition with_expected_endorsing_rewards expected_endorsing_rewards
(r : record) :=
Build r.(expected_cycle_activity) r.(minimal_cycle_activity)
r.(missed_slots) r.(missed_levels) r.(remaining_allowed_missed_slots)
expected_endorsing_rewards.
End participation_info.
Definition participation_info := participation_info.record.
Definition participation_info_value
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? participation_info :=
let level := Level_storage.current ctxt in
let? stake_distribution :=
Stake_storage.get_selected_distribution ctxt level.(Level_repr.t.cycle) in
match
List.assoc_opt Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
delegate stake_distribution with
| None ⇒
return?
{| participation_info.expected_cycle_activity := 0;
participation_info.minimal_cycle_activity := 0;
participation_info.missed_slots := 0;
participation_info.missed_levels := 0;
participation_info.remaining_allowed_missed_slots := 0;
participation_info.expected_endorsing_rewards := Tez_repr.zero; |}
| Some active_stake ⇒
let? total_active_stake :=
Stake_storage.get_total_active_stake ctxt level.(Level_repr.t.cycle) in
let expected_cycle_activity :=
expected_slots_for_given_active_stake ctxt total_active_stake active_stake
in
let '{|
Ratio_repr.t.numerator := numerator;
Ratio_repr.t.denominator := denominator
|} := Constants_storage.minimal_participation_ratio ctxt in
let endorsing_reward_per_slot :=
Constants_storage.endorsing_reward_per_slot ctxt in
let minimal_cycle_activity :=
(expected_cycle_activity ×i numerator) /i denominator in
let maximal_cycle_inactivity :=
expected_cycle_activity -i minimal_cycle_activity in
let expected_endorsing_rewards :=
Tez_repr.mul_exn endorsing_reward_per_slot expected_cycle_activity in
let contract := Contract_repr.Implicit delegate in
let? missed_endorsements :=
Storage.Contract.Missed_endorsements.(Storage_sigs.Indexed_data_storage.find)
ctxt contract in
let '(missed_slots, missed_levels, remaining_allowed_missed_slots) :=
match missed_endorsements with
| None ⇒ (0, 0, maximal_cycle_inactivity)
|
Some {|
Storage.missed_endorsements_info.remaining_slots := remaining_slots;
Storage.missed_endorsements_info.missed_levels := missed_levels
|} ⇒
((maximal_cycle_inactivity -i remaining_slots), missed_levels,
(Compare.Int.max 0 remaining_slots))
end in
let expected_endorsing_rewards :=
match
(missed_endorsements,
match missed_endorsements with
| Some r_value ⇒
r_value.(Storage.missed_endorsements_info.remaining_slots) <i 0
| _ ⇒ false
end) with
| (Some r_value, true) ⇒ Tez_repr.zero
| (_, _) ⇒ expected_endorsing_rewards
end in
return?
{| participation_info.expected_cycle_activity := expected_cycle_activity;
participation_info.minimal_cycle_activity := minimal_cycle_activity;
participation_info.missed_slots := missed_slots;
participation_info.missed_levels := missed_levels;
participation_info.remaining_allowed_missed_slots :=
remaining_allowed_missed_slots;
participation_info.expected_endorsing_rewards :=
expected_endorsing_rewards; |}
end.