👥 Delegate_sampler.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.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Module Delegate_sampler_state.
Module Cache_client.
Definition cached_value : Set := Sampler.t Delegate_consensus_key.pk.
Definition namespace_value : Cache_repr.namespace :=
Cache_repr.create_namespace "sampler_state".
Definition cache_index : int := 2.
Definition value_of_identifier (ctxt : Raw_context.t) (identifier : string)
: M?
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value) :=
let cycle := Cycle_repr.of_string_exn identifier in
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.get)
ctxt cycle.
(* Cache_client *)
Definition module :=
{|
Cache_repr.CLIENT.namespace_value := namespace_value;
Cache_repr.CLIENT.cache_index := cache_index;
Cache_repr.CLIENT.value_of_identifier := value_of_identifier
|}.
End Cache_client.
Definition Cache_client := Cache_client.module.
Axiom Cache : Cache_repr.INTERFACE (cached_value := Cache_client.cached_value).
Definition identifier_of_cycle (cycle : Cycle_repr.cycle) : string :=
Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") Cycle_repr.pp cycle.
Definition init_value
(ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
(sampler_state :
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value))
: M? Raw_context.t :=
let id := identifier_of_cycle cycle in
let? ctxt :=
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.init_value)
ctxt cycle sampler_state in
let size_value := 1 in
let? ctxt :=
Cache.(Cache_repr.INTERFACE.update) ctxt id
(Some (sampler_state, size_value)) in
return? ctxt.
Definition get (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
: M?
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value) :=
let id := identifier_of_cycle cycle in
let? function_parameter := Cache.(Cache_repr.INTERFACE.find) ctxt id in
match function_parameter with
| None ⇒
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.get)
ctxt cycle
| Some v_value ⇒ return? v_value
end.
Definition remove_existing (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
: M? Raw_context.t :=
let id := identifier_of_cycle cycle in
let? ctxt := Cache.(Cache_repr.INTERFACE.update) ctxt id None in
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt cycle.
End Delegate_sampler_state.
Module Random.
Definition init_random_state
(seed_value : Seed_repr.seed) (level : Level_repr.t) (index_value : int)
: bytes × int :=
((Raw_hashes.blake2b
(Data_encoding.Binary.to_bytes_exn None
(Data_encoding.tup3 Seed_repr.seed_encoding Data_encoding.int32_value
Data_encoding.int32_value)
(seed_value, level.(Level_repr.t.cycle_position),
(Int32.of_int index_value)))), 0).
#[bypass_check(guard)]
Definition take_int64 (bound : int64) (state_value : bytes × int)
: int64 × (bytes × int) :=
let drop_if_over := Int64.max_int -i64 (Int64.rem Int64.max_int bound) in
let fix loop (function_parameter : bytes × int) {struct function_parameter}
: int64 × (bytes × int) :=
let '(bytes_value, n_value) := function_parameter in
let consumed_bytes := 8 in
let state_size := Bytes.length bytes_value in
if n_value >i (state_size -i consumed_bytes) then
loop ((Raw_hashes.blake2b bytes_value), 0)
else
let r_value := TzEndian.get_int64 bytes_value n_value in
let r_value :=
if r_value =i64 Int64.min_int then
0
else
Int64.abs r_value in
if r_value ≥i64 drop_if_over then
loop (bytes_value, (n_value +i consumed_bytes))
else
let v_value := Int64.rem r_value bound in
(v_value, (bytes_value, (n_value +i consumed_bytes))) in
loop state_value.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_consensus_key.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sampler.
Require TezosOfOCaml.Proto_alpha.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Module Delegate_sampler_state.
Module Cache_client.
Definition cached_value : Set := Sampler.t Delegate_consensus_key.pk.
Definition namespace_value : Cache_repr.namespace :=
Cache_repr.create_namespace "sampler_state".
Definition cache_index : int := 2.
Definition value_of_identifier (ctxt : Raw_context.t) (identifier : string)
: M?
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value) :=
let cycle := Cycle_repr.of_string_exn identifier in
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.get)
ctxt cycle.
(* Cache_client *)
Definition module :=
{|
Cache_repr.CLIENT.namespace_value := namespace_value;
Cache_repr.CLIENT.cache_index := cache_index;
Cache_repr.CLIENT.value_of_identifier := value_of_identifier
|}.
End Cache_client.
Definition Cache_client := Cache_client.module.
Axiom Cache : Cache_repr.INTERFACE (cached_value := Cache_client.cached_value).
Definition identifier_of_cycle (cycle : Cycle_repr.cycle) : string :=
Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") Cycle_repr.pp cycle.
Definition init_value
(ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
(sampler_state :
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value))
: M? Raw_context.t :=
let id := identifier_of_cycle cycle in
let? ctxt :=
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.init_value)
ctxt cycle sampler_state in
let size_value := 1 in
let? ctxt :=
Cache.(Cache_repr.INTERFACE.update) ctxt id
(Some (sampler_state, size_value)) in
return? ctxt.
Definition get (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
: M?
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value) :=
let id := identifier_of_cycle cycle in
let? function_parameter := Cache.(Cache_repr.INTERFACE.find) ctxt id in
match function_parameter with
| None ⇒
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.get)
ctxt cycle
| Some v_value ⇒ return? v_value
end.
Definition remove_existing (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
: M? Raw_context.t :=
let id := identifier_of_cycle cycle in
let? ctxt := Cache.(Cache_repr.INTERFACE.update) ctxt id None in
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt cycle.
End Delegate_sampler_state.
Module Random.
Definition init_random_state
(seed_value : Seed_repr.seed) (level : Level_repr.t) (index_value : int)
: bytes × int :=
((Raw_hashes.blake2b
(Data_encoding.Binary.to_bytes_exn None
(Data_encoding.tup3 Seed_repr.seed_encoding Data_encoding.int32_value
Data_encoding.int32_value)
(seed_value, level.(Level_repr.t.cycle_position),
(Int32.of_int index_value)))), 0).
#[bypass_check(guard)]
Definition take_int64 (bound : int64) (state_value : bytes × int)
: int64 × (bytes × int) :=
let drop_if_over := Int64.max_int -i64 (Int64.rem Int64.max_int bound) in
let fix loop (function_parameter : bytes × int) {struct function_parameter}
: int64 × (bytes × int) :=
let '(bytes_value, n_value) := function_parameter in
let consumed_bytes := 8 in
let state_size := Bytes.length bytes_value in
if n_value >i (state_size -i consumed_bytes) then
loop ((Raw_hashes.blake2b bytes_value), 0)
else
let r_value := TzEndian.get_int64 bytes_value n_value in
let r_value :=
if r_value =i64 Int64.min_int then
0
else
Int64.abs r_value in
if r_value ≥i64 drop_if_over then
loop (bytes_value, (n_value +i consumed_bytes))
else
let v_value := Int64.rem r_value bound in
(v_value, (bytes_value, (n_value +i consumed_bytes))) in
loop state_value.
[sampler_for_cycle ctxt cycle] reads the sampler for [cycle] from
[ctxt] if it has been previously inited. Otherwise it initializes
the sampler and caches it in [ctxt] with
[Raw_context.set_sampler_for_cycle].
Definition sampler_for_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
: M? (Raw_context.t × Seed_repr.seed × Sampler.t Raw_context.consensus_pk) :=
let read (ctxt : Raw_context.t)
: M?
(Seed_repr.seed ×
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value)) :=
let? seed_value := Seed_storage.for_cycle ctxt cycle in
let? state_value := Delegate_sampler_state.get ctxt cycle in
return? (seed_value, state_value) in
Raw_context.sampler_for_cycle read ctxt cycle.
Definition owner
(c_value : Raw_context.t) (level : Level_repr.t) (offset : int)
: M? (Raw_context.t × Raw_context.consensus_pk) :=
let cycle := level.(Level_repr.t.cycle) in
let? '(c_value, seed_value, state_value) := sampler_for_cycle c_value cycle
in
let sample (int_bound : int) (mass_bound : int64) : int × int64 :=
let state_value := init_random_state seed_value level offset in
let '(i_value, state_value) :=
take_int64 (Int64.of_int int_bound) state_value in
let '(elt_value, _) := take_int64 mass_bound state_value in
((Int64.to_int i_value), elt_value) in
let? pk := Sampler.sample state_value sample in
return? (c_value, pk).
End Random.
Definition slot_owner
(c_value : Raw_context.t) (level : Level_repr.t) (slot : Slot_repr.t)
: M? (Raw_context.t × Raw_context.consensus_pk) :=
Random.owner c_value level (Slot_repr.to_int slot).
Definition baking_rights_owner
(c_value : Raw_context.t) (level : Level_repr.t) (round : Round_repr.t)
: M? (Raw_context.t × Slot_repr.t × Raw_context.consensus_pk) :=
let? round := Round_repr.to_int round in
let consensus_committee_size :=
Constants_storage.consensus_committee_size c_value in
let? slot := Slot_repr.of_int (Pervasives._mod round consensus_committee_size)
in
let? '(ctxt, pk) := slot_owner c_value level slot in
return? (ctxt, slot, pk).
Definition get_stakes_for_selected_index
(ctxt : Raw_context.t) (index_value : int)
: M? (list (Signature.public_key_hash × Tez_repr.t) × Tez_repr.t) :=
Stake_storage.fold_snapshot ctxt index_value
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(delegate, staking_balance) := function_parameter in
fun (function_parameter :
list (Signature.public_key_hash × Tez_repr.t) × Tez_repr.t) ⇒
let '(acc_value, total_stake) := function_parameter in
let delegate_contract := Contract_repr.Implicit delegate in
let? frozen_deposits_limit :=
Delegate_storage.frozen_deposits_limit ctxt delegate in
let? balance_and_frozen_bonds :=
Contract_storage.get_balance_and_frozen_bonds ctxt delegate_contract
in
let? frozen_deposits :=
Frozen_deposits_storage.get ctxt delegate_contract in
let? total_balance :=
Tez_repr.op_plusquestion balance_and_frozen_bonds
frozen_deposits.(Storage.deposits.current_amount) in
let? stake_for_cycle :=
let frozen_deposits_percentage :=
Int64.of_int (Constants_storage.frozen_deposits_percentage ctxt) in
let max_mutez := Tez_repr.of_mutez_exn Int64.max_int in
let frozen_deposits_limit :=
match frozen_deposits_limit with
| Some fdp ⇒ fdp
| None ⇒ max_mutez
end in
let aux := Tez_repr.min total_balance frozen_deposits_limit in
let? overflow_bound := Tez_repr.op_divquestion max_mutez 100 in
if Tez_repr.op_lteq aux overflow_bound then
let? aux := Tez_repr.op_starquestion aux 100 in
let? v_value :=
Tez_repr.op_divquestion aux frozen_deposits_percentage in
return? (Tez_repr.min v_value staking_balance)
else
let? sbal := Tez_repr.op_divquestion staking_balance 100 in
let? a_value :=
Tez_repr.op_divquestion aux frozen_deposits_percentage in
if Tez_repr.op_lteq sbal a_value then
return? staking_balance
else
let? r_value :=
Tez_repr.op_divquestion max_mutez frozen_deposits_percentage in
return? r_value in
let? total_stake := Tez_repr.op_plusquestion total_stake stake_for_cycle
in
return? ((cons (delegate, stake_for_cycle) acc_value), total_stake))
(nil, Tez_repr.zero).
Definition compute_snapshot_index_for_seed {A : Set}
(max_snapshot_index : int) (seed_value : Seed_repr.seed)
: Pervasives.result int A :=
let rd :=
Seed_repr.initialize_new seed_value [ Bytes.of_string "stake_snapshot" ] in
let seq := Seed_repr.sequence_value rd 0 in
return?
(Int32.to_int
(Pervasives.fst
(Seed_repr.take_int32 seq (Int32.of_int max_snapshot_index)))).
Definition compute_snapshot_index
(ctxt : Raw_context.t) (cycle : Cycle_repr.t) (max_snapshot_index : int)
: M? int :=
let? seed_value := Seed_storage.for_cycle ctxt cycle in
compute_snapshot_index_for_seed max_snapshot_index seed_value.
Definition select_distribution_for_cycle
(ctxt : Raw_context.t) (cycle : Cycle_repr.t) : M? Raw_context.t :=
let? max_snapshot_index := Stake_storage.max_snapshot_index ctxt in
let? seed_value := Seed_storage.raw_for_cycle ctxt cycle in
let? selected_index :=
compute_snapshot_index_for_seed max_snapshot_index seed_value in
let? '(stakes, total_stake) :=
get_stakes_for_selected_index ctxt selected_index in
let? ctxt :=
Stake_storage.set_selected_distribution_for_cycle ctxt cycle stakes
total_stake in
let? stakes_pk :=
List.fold_left_es
(fun (acc_value : list (Delegate_consensus_key.pk × Sampler.mass)) ⇒
fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(pkh, stake) := function_parameter in
let? pk :=
Delegate_consensus_key.active_pubkey_for_cycle ctxt pkh cycle in
return? (cons (pk, (Tez_repr.to_mutez stake)) acc_value)) nil stakes
in
let state_value := Sampler.create stakes_pk in
let? ctxt := Delegate_sampler_state.init_value ctxt cycle state_value in
Raw_context.init_sampler_for_cycle ctxt cycle seed_value state_value.
Definition select_new_distribution_at_cycle_end
(ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : M? Raw_context.t :=
let preserved := Constants_storage.preserved_cycles ctxt in
let? for_cycle := Cycle_repr.add new_cycle preserved in
select_distribution_for_cycle ctxt for_cycle.
Definition clear_outdated_sampling_data
(ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : M? Raw_context.t :=
let max_slashing_period := Constants_storage.max_slashing_period ctxt in
let? res := Cycle_repr.sub new_cycle max_slashing_period in
match res with
| None ⇒ return? ctxt
| Some outdated_cycle ⇒
let? ctxt := Delegate_sampler_state.remove_existing ctxt outdated_cycle in
Seed_storage.remove_for_cycle ctxt outdated_cycle
end.
: M? (Raw_context.t × Seed_repr.seed × Sampler.t Raw_context.consensus_pk) :=
let read (ctxt : Raw_context.t)
: M?
(Seed_repr.seed ×
Storage.Delegate_sampler_state.(Storage_sigs.Indexed_data_storage.value)) :=
let? seed_value := Seed_storage.for_cycle ctxt cycle in
let? state_value := Delegate_sampler_state.get ctxt cycle in
return? (seed_value, state_value) in
Raw_context.sampler_for_cycle read ctxt cycle.
Definition owner
(c_value : Raw_context.t) (level : Level_repr.t) (offset : int)
: M? (Raw_context.t × Raw_context.consensus_pk) :=
let cycle := level.(Level_repr.t.cycle) in
let? '(c_value, seed_value, state_value) := sampler_for_cycle c_value cycle
in
let sample (int_bound : int) (mass_bound : int64) : int × int64 :=
let state_value := init_random_state seed_value level offset in
let '(i_value, state_value) :=
take_int64 (Int64.of_int int_bound) state_value in
let '(elt_value, _) := take_int64 mass_bound state_value in
((Int64.to_int i_value), elt_value) in
let? pk := Sampler.sample state_value sample in
return? (c_value, pk).
End Random.
Definition slot_owner
(c_value : Raw_context.t) (level : Level_repr.t) (slot : Slot_repr.t)
: M? (Raw_context.t × Raw_context.consensus_pk) :=
Random.owner c_value level (Slot_repr.to_int slot).
Definition baking_rights_owner
(c_value : Raw_context.t) (level : Level_repr.t) (round : Round_repr.t)
: M? (Raw_context.t × Slot_repr.t × Raw_context.consensus_pk) :=
let? round := Round_repr.to_int round in
let consensus_committee_size :=
Constants_storage.consensus_committee_size c_value in
let? slot := Slot_repr.of_int (Pervasives._mod round consensus_committee_size)
in
let? '(ctxt, pk) := slot_owner c_value level slot in
return? (ctxt, slot, pk).
Definition get_stakes_for_selected_index
(ctxt : Raw_context.t) (index_value : int)
: M? (list (Signature.public_key_hash × Tez_repr.t) × Tez_repr.t) :=
Stake_storage.fold_snapshot ctxt index_value
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(delegate, staking_balance) := function_parameter in
fun (function_parameter :
list (Signature.public_key_hash × Tez_repr.t) × Tez_repr.t) ⇒
let '(acc_value, total_stake) := function_parameter in
let delegate_contract := Contract_repr.Implicit delegate in
let? frozen_deposits_limit :=
Delegate_storage.frozen_deposits_limit ctxt delegate in
let? balance_and_frozen_bonds :=
Contract_storage.get_balance_and_frozen_bonds ctxt delegate_contract
in
let? frozen_deposits :=
Frozen_deposits_storage.get ctxt delegate_contract in
let? total_balance :=
Tez_repr.op_plusquestion balance_and_frozen_bonds
frozen_deposits.(Storage.deposits.current_amount) in
let? stake_for_cycle :=
let frozen_deposits_percentage :=
Int64.of_int (Constants_storage.frozen_deposits_percentage ctxt) in
let max_mutez := Tez_repr.of_mutez_exn Int64.max_int in
let frozen_deposits_limit :=
match frozen_deposits_limit with
| Some fdp ⇒ fdp
| None ⇒ max_mutez
end in
let aux := Tez_repr.min total_balance frozen_deposits_limit in
let? overflow_bound := Tez_repr.op_divquestion max_mutez 100 in
if Tez_repr.op_lteq aux overflow_bound then
let? aux := Tez_repr.op_starquestion aux 100 in
let? v_value :=
Tez_repr.op_divquestion aux frozen_deposits_percentage in
return? (Tez_repr.min v_value staking_balance)
else
let? sbal := Tez_repr.op_divquestion staking_balance 100 in
let? a_value :=
Tez_repr.op_divquestion aux frozen_deposits_percentage in
if Tez_repr.op_lteq sbal a_value then
return? staking_balance
else
let? r_value :=
Tez_repr.op_divquestion max_mutez frozen_deposits_percentage in
return? r_value in
let? total_stake := Tez_repr.op_plusquestion total_stake stake_for_cycle
in
return? ((cons (delegate, stake_for_cycle) acc_value), total_stake))
(nil, Tez_repr.zero).
Definition compute_snapshot_index_for_seed {A : Set}
(max_snapshot_index : int) (seed_value : Seed_repr.seed)
: Pervasives.result int A :=
let rd :=
Seed_repr.initialize_new seed_value [ Bytes.of_string "stake_snapshot" ] in
let seq := Seed_repr.sequence_value rd 0 in
return?
(Int32.to_int
(Pervasives.fst
(Seed_repr.take_int32 seq (Int32.of_int max_snapshot_index)))).
Definition compute_snapshot_index
(ctxt : Raw_context.t) (cycle : Cycle_repr.t) (max_snapshot_index : int)
: M? int :=
let? seed_value := Seed_storage.for_cycle ctxt cycle in
compute_snapshot_index_for_seed max_snapshot_index seed_value.
Definition select_distribution_for_cycle
(ctxt : Raw_context.t) (cycle : Cycle_repr.t) : M? Raw_context.t :=
let? max_snapshot_index := Stake_storage.max_snapshot_index ctxt in
let? seed_value := Seed_storage.raw_for_cycle ctxt cycle in
let? selected_index :=
compute_snapshot_index_for_seed max_snapshot_index seed_value in
let? '(stakes, total_stake) :=
get_stakes_for_selected_index ctxt selected_index in
let? ctxt :=
Stake_storage.set_selected_distribution_for_cycle ctxt cycle stakes
total_stake in
let? stakes_pk :=
List.fold_left_es
(fun (acc_value : list (Delegate_consensus_key.pk × Sampler.mass)) ⇒
fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(pkh, stake) := function_parameter in
let? pk :=
Delegate_consensus_key.active_pubkey_for_cycle ctxt pkh cycle in
return? (cons (pk, (Tez_repr.to_mutez stake)) acc_value)) nil stakes
in
let state_value := Sampler.create stakes_pk in
let? ctxt := Delegate_sampler_state.init_value ctxt cycle state_value in
Raw_context.init_sampler_for_cycle ctxt cycle seed_value state_value.
Definition select_new_distribution_at_cycle_end
(ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : M? Raw_context.t :=
let preserved := Constants_storage.preserved_cycles ctxt in
let? for_cycle := Cycle_repr.add new_cycle preserved in
select_distribution_for_cycle ctxt for_cycle.
Definition clear_outdated_sampling_data
(ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : M? Raw_context.t :=
let max_slashing_period := Constants_storage.max_slashing_period ctxt in
let? res := Cycle_repr.sub new_cycle max_slashing_period in
match res with
| None ⇒ return? ctxt
| Some outdated_cycle ⇒
let? ctxt := Delegate_sampler_state.remove_existing ctxt outdated_cycle in
Seed_storage.remove_for_cycle ctxt outdated_cycle
end.