🪤 Stake_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.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_delegate_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Module Selected_distribution_for_cycle.
Module Cache_client.
Definition cached_value : Set :=
list (Signature.public_key_hash × Tez_repr.t).
Definition namespace_value : Cache_repr.namespace :=
Cache_repr.create_namespace "stake_distribution".
Definition cache_index : int := 1.
Definition value_of_identifier (ctxt : Raw_context.t) (identifier : string)
: M?
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value) :=
let cycle := Cycle_repr.of_string_exn identifier in
Storage.Stake.Selected_distribution_for_cycle.(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)
(stakes :
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value))
: M? Raw_context.t :=
let id := identifier_of_cycle cycle in
let? ctxt :=
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.init_value)
ctxt cycle stakes in
let size_value := 1 in
let? ctxt :=
Cache.(Cache_repr.INTERFACE.update) ctxt id (Some (stakes, size_value)) in
return? ctxt.
Definition get (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
: M?
Storage.Stake.Selected_distribution_for_cycle.(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.Stake.Selected_distribution_for_cycle.(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.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt cycle.
End Selected_distribution_for_cycle.
Definition get_staking_balance
: Raw_context.t → Signature.public_key_hash → M? Tez_repr.t :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.get).
Definition get_initialized_stake
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Tez_repr.t × Raw_context.t) :=
let? function_parameter :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.find)
ctxt delegate in
match function_parameter with
| Some staking_balance ⇒ return? (staking_balance, ctxt)
| None ⇒
let? ctxt := Frozen_deposits_storage.init_value ctxt delegate in
let balance := Tez_repr.zero in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.init_value)
ctxt delegate balance in
return? (balance, ctxt)
end.
Definition remove_stake
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(amount : Tez_repr.t) : M? Raw_context.t :=
let? '(staking_balance_before, ctxt) := get_initialized_stake ctxt delegate in
let? staking_balance :=
Tez_repr.op_minusquestion staking_balance_before amount in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.update)
ctxt delegate staking_balance in
let minimal_stake := Constants_storage.minimal_stake ctxt in
if Tez_repr.op_gteq staking_balance_before minimal_stake then
let? inactive := Delegate_activation_storage.is_inactive ctxt delegate in
if
(Pervasives.not inactive) &&
(Tez_repr.op_lt staking_balance minimal_stake)
then
let ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.remove)
ctxt delegate in
return? ctxt
else
return? ctxt
else
return? ctxt.
Definition add_stake
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(amount : Tez_repr.t) : M? Raw_context.t :=
let? '(staking_balance_before, ctxt) := get_initialized_stake ctxt delegate in
let? staking_balance := Tez_repr.op_plusquestion amount staking_balance_before
in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.update)
ctxt delegate staking_balance in
let minimal_stake := Constants_storage.minimal_stake ctxt in
if Tez_repr.op_gteq staking_balance minimal_stake then
let? inactive := Delegate_activation_storage.is_inactive ctxt delegate in
if
inactive || (Tez_repr.op_gteq staking_balance_before minimal_stake)
then
return? ctxt
else
let ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.add)
ctxt delegate tt in
return? ctxt
else
return? ctxt.
Definition set_inactive
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: Raw_context.t :=
let ctxt := Delegate_activation_storage.set_inactive ctxt delegate in
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.remove)
ctxt delegate.
Definition set_active
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? Raw_context.t :=
let? '(ctxt, inactive) := Delegate_activation_storage.set_active ctxt delegate
in
if Pervasives.not inactive then
return? ctxt
else
let? '(staking_balance, ctxt) := get_initialized_stake ctxt delegate in
let minimal_stake := Constants_storage.minimal_stake ctxt in
if Tez_repr.op_gteq staking_balance minimal_stake then
let ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.add)
ctxt delegate tt in
return? ctxt
else
return? ctxt.
Definition snapshot_value (ctxt : Raw_context.t) : M? Raw_context.t :=
let? index_value :=
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.get) ctxt in
let? ctxt :=
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.update) ctxt
(index_value +i 1) in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.snapshot_value)
ctxt index_value in
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.snapshot_value)
ctxt index_value.
Definition max_snapshot_index : Raw_context.t → M? int :=
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.get).
Definition set_selected_distribution_for_cycle
(ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
(stakes : list (Signature.public_key_hash × Tez_repr.t))
(total_stake : Tez_repr.t) : M? Raw_context.t :=
let stakes :=
List.sort
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(_, x_value) := function_parameter in
fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(_, y_value) := function_parameter in
Tez_repr.compare y_value x_value) stakes in
let? ctxt := Selected_distribution_for_cycle.init_value ctxt cycle stakes in
let ctxt :=
Storage.Stake.Total_active_stake.(Storage_sigs.Indexed_data_storage.add)
ctxt cycle total_stake in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.Snapshot).(Storage_sigs.Indexed_data_storage.clear)
ctxt in
let? ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.Snapshot).(Storage_sigs.Indexed_data_storage.clear)
ctxt in
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.update) ctxt 0.
Definition clear_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
: M? Raw_context.t :=
let? ctxt :=
Storage.Stake.Total_active_stake.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt cycle in
Selected_distribution_for_cycle.remove_existing ctxt cycle.
Definition fold {A : Set}
(ctxt : Raw_context.t)
(f_value : Signature.public_key_hash × Tez_repr.t → A → M? A)
(order : Variant.t) (init_value : A) : M? A :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.fold)
ctxt order init_value
(fun (delegate : Signature.public_key_hash) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (acc_value : A) ⇒
let? stake := get_staking_balance ctxt delegate in
f_value (delegate, stake) acc_value).
Definition fold_snapshot {A : Set}
(ctxt : Raw_context.t) (index_value : int)
(f_value : Signature.public_key_hash × Tez_repr.t → A → M? A)
(init_value : A) : M? A :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.fold_snapshot)
ctxt index_value (Variant.Build "Sorted" unit tt) init_value
(fun (delegate : Signature.public_key_hash) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (acc_value : A) ⇒
let? stake :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.Snapshot).(Storage_sigs.Indexed_data_storage.get)
ctxt (index_value, delegate) in
f_value (delegate, stake) acc_value).
Definition clear_at_cycle_end
(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 cycle_to_clear ⇒ clear_cycle ctxt cycle_to_clear
end.
Definition get (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? Tez_repr.t :=
let function_parameter :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.mem)
ctxt delegate in
match function_parameter with
| true ⇒ get_staking_balance ctxt delegate
| false ⇒ return? Tez_repr.zero
end.
Definition fold_on_active_delegates_with_minimal_stake {A : Set}
: Raw_context.t → Variant.t → A →
(Signature.public_key_hash → unit → A → M? A) → M? A :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.fold).
Definition get_selected_distribution
: Raw_context.t → Cycle_repr.cycle →
M?
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value) :=
Selected_distribution_for_cycle.get.
Definition find_selected_distribution
: Raw_context.t → Cycle_repr.t →
M?
(option
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value)) :=
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.find).
Definition prepare_stake_distribution (ctxt : Raw_context.t)
: M? Raw_context.t :=
let level := Level_storage.current ctxt in
let? stakes :=
Selected_distribution_for_cycle.get ctxt level.(Level_repr.t.cycle) in
let stake_distribution :=
List.fold_left
(fun (map :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t) ⇒
fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(pkh, stake) := function_parameter in
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
pkh stake map)
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty)
stakes in
return?
(Raw_context.init_stake_distribution_for_current_cycle ctxt
stake_distribution).
Definition get_total_active_stake
: Raw_context.t → Cycle_repr.t → M? Tez_repr.t :=
Storage.Stake.Total_active_stake.(Storage_sigs.Indexed_data_storage.get).
Definition remove_contract_stake
(ctxt : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
: M? Raw_context.t :=
let? function_parameter := Contract_delegate_storage.find ctxt contract in
match function_parameter with
| None ⇒ return? ctxt
| Some delegate ⇒ remove_stake ctxt delegate amount
end.
Definition add_contract_stake
(ctxt : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
: M? Raw_context.t :=
let? function_parameter := Contract_delegate_storage.find ctxt contract in
match function_parameter with
| None ⇒ return? ctxt
| Some delegate ⇒ add_stake ctxt delegate amount
end.
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_delegate_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_activation_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Module Selected_distribution_for_cycle.
Module Cache_client.
Definition cached_value : Set :=
list (Signature.public_key_hash × Tez_repr.t).
Definition namespace_value : Cache_repr.namespace :=
Cache_repr.create_namespace "stake_distribution".
Definition cache_index : int := 1.
Definition value_of_identifier (ctxt : Raw_context.t) (identifier : string)
: M?
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value) :=
let cycle := Cycle_repr.of_string_exn identifier in
Storage.Stake.Selected_distribution_for_cycle.(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)
(stakes :
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value))
: M? Raw_context.t :=
let id := identifier_of_cycle cycle in
let? ctxt :=
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.init_value)
ctxt cycle stakes in
let size_value := 1 in
let? ctxt :=
Cache.(Cache_repr.INTERFACE.update) ctxt id (Some (stakes, size_value)) in
return? ctxt.
Definition get (ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
: M?
Storage.Stake.Selected_distribution_for_cycle.(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.Stake.Selected_distribution_for_cycle.(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.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt cycle.
End Selected_distribution_for_cycle.
Definition get_staking_balance
: Raw_context.t → Signature.public_key_hash → M? Tez_repr.t :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.get).
Definition get_initialized_stake
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? (Tez_repr.t × Raw_context.t) :=
let? function_parameter :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.find)
ctxt delegate in
match function_parameter with
| Some staking_balance ⇒ return? (staking_balance, ctxt)
| None ⇒
let? ctxt := Frozen_deposits_storage.init_value ctxt delegate in
let balance := Tez_repr.zero in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.init_value)
ctxt delegate balance in
return? (balance, ctxt)
end.
Definition remove_stake
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(amount : Tez_repr.t) : M? Raw_context.t :=
let? '(staking_balance_before, ctxt) := get_initialized_stake ctxt delegate in
let? staking_balance :=
Tez_repr.op_minusquestion staking_balance_before amount in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.update)
ctxt delegate staking_balance in
let minimal_stake := Constants_storage.minimal_stake ctxt in
if Tez_repr.op_gteq staking_balance_before minimal_stake then
let? inactive := Delegate_activation_storage.is_inactive ctxt delegate in
if
(Pervasives.not inactive) &&
(Tez_repr.op_lt staking_balance minimal_stake)
then
let ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.remove)
ctxt delegate in
return? ctxt
else
return? ctxt
else
return? ctxt.
Definition add_stake
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
(amount : Tez_repr.t) : M? Raw_context.t :=
let? '(staking_balance_before, ctxt) := get_initialized_stake ctxt delegate in
let? staking_balance := Tez_repr.op_plusquestion amount staking_balance_before
in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.update)
ctxt delegate staking_balance in
let minimal_stake := Constants_storage.minimal_stake ctxt in
if Tez_repr.op_gteq staking_balance minimal_stake then
let? inactive := Delegate_activation_storage.is_inactive ctxt delegate in
if
inactive || (Tez_repr.op_gteq staking_balance_before minimal_stake)
then
return? ctxt
else
let ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.add)
ctxt delegate tt in
return? ctxt
else
return? ctxt.
Definition set_inactive
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: Raw_context.t :=
let ctxt := Delegate_activation_storage.set_inactive ctxt delegate in
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.remove)
ctxt delegate.
Definition set_active
(ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? Raw_context.t :=
let? '(ctxt, inactive) := Delegate_activation_storage.set_active ctxt delegate
in
if Pervasives.not inactive then
return? ctxt
else
let? '(staking_balance, ctxt) := get_initialized_stake ctxt delegate in
let minimal_stake := Constants_storage.minimal_stake ctxt in
if Tez_repr.op_gteq staking_balance minimal_stake then
let ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.add)
ctxt delegate tt in
return? ctxt
else
return? ctxt.
Definition snapshot_value (ctxt : Raw_context.t) : M? Raw_context.t :=
let? index_value :=
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.get) ctxt in
let? ctxt :=
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.update) ctxt
(index_value +i 1) in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.snapshot_value)
ctxt index_value in
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.snapshot_value)
ctxt index_value.
Definition max_snapshot_index : Raw_context.t → M? int :=
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.get).
Definition set_selected_distribution_for_cycle
(ctxt : Raw_context.t) (cycle : Cycle_repr.cycle)
(stakes : list (Signature.public_key_hash × Tez_repr.t))
(total_stake : Tez_repr.t) : M? Raw_context.t :=
let stakes :=
List.sort
(fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(_, x_value) := function_parameter in
fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(_, y_value) := function_parameter in
Tez_repr.compare y_value x_value) stakes in
let? ctxt := Selected_distribution_for_cycle.init_value ctxt cycle stakes in
let ctxt :=
Storage.Stake.Total_active_stake.(Storage_sigs.Indexed_data_storage.add)
ctxt cycle total_stake in
let? ctxt :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.Snapshot).(Storage_sigs.Indexed_data_storage.clear)
ctxt in
let? ctxt :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.Snapshot).(Storage_sigs.Indexed_data_storage.clear)
ctxt in
Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.update) ctxt 0.
Definition clear_cycle (ctxt : Raw_context.t) (cycle : Cycle_repr.t)
: M? Raw_context.t :=
let? ctxt :=
Storage.Stake.Total_active_stake.(Storage_sigs.Indexed_data_storage.remove_existing)
ctxt cycle in
Selected_distribution_for_cycle.remove_existing ctxt cycle.
Definition fold {A : Set}
(ctxt : Raw_context.t)
(f_value : Signature.public_key_hash × Tez_repr.t → A → M? A)
(order : Variant.t) (init_value : A) : M? A :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.fold)
ctxt order init_value
(fun (delegate : Signature.public_key_hash) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (acc_value : A) ⇒
let? stake := get_staking_balance ctxt delegate in
f_value (delegate, stake) acc_value).
Definition fold_snapshot {A : Set}
(ctxt : Raw_context.t) (index_value : int)
(f_value : Signature.public_key_hash × Tez_repr.t → A → M? A)
(init_value : A) : M? A :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.fold_snapshot)
ctxt index_value (Variant.Build "Sorted" unit tt) init_value
(fun (delegate : Signature.public_key_hash) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
fun (acc_value : A) ⇒
let? stake :=
Storage.Stake.Staking_balance.(Storage_sigs.Indexed_data_snapshotable_storage.Snapshot).(Storage_sigs.Indexed_data_storage.get)
ctxt (index_value, delegate) in
f_value (delegate, stake) acc_value).
Definition clear_at_cycle_end
(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 cycle_to_clear ⇒ clear_cycle ctxt cycle_to_clear
end.
Definition get (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
: M? Tez_repr.t :=
let function_parameter :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.mem)
ctxt delegate in
match function_parameter with
| true ⇒ get_staking_balance ctxt delegate
| false ⇒ return? Tez_repr.zero
end.
Definition fold_on_active_delegates_with_minimal_stake {A : Set}
: Raw_context.t → Variant.t → A →
(Signature.public_key_hash → unit → A → M? A) → M? A :=
Storage.Stake.Active_delegates_with_minimal_stake.(Storage_sigs.Indexed_data_snapshotable_storage.fold).
Definition get_selected_distribution
: Raw_context.t → Cycle_repr.cycle →
M?
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value) :=
Selected_distribution_for_cycle.get.
Definition find_selected_distribution
: Raw_context.t → Cycle_repr.t →
M?
(option
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.value)) :=
Storage.Stake.Selected_distribution_for_cycle.(Storage_sigs.Indexed_data_storage.find).
Definition prepare_stake_distribution (ctxt : Raw_context.t)
: M? Raw_context.t :=
let level := Level_storage.current ctxt in
let? stakes :=
Selected_distribution_for_cycle.get ctxt level.(Level_repr.t.cycle) in
let stake_distribution :=
List.fold_left
(fun (map :
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
Tez_repr.t) ⇒
fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
let '(pkh, stake) := function_parameter in
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
pkh stake map)
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty)
stakes in
return?
(Raw_context.init_stake_distribution_for_current_cycle ctxt
stake_distribution).
Definition get_total_active_stake
: Raw_context.t → Cycle_repr.t → M? Tez_repr.t :=
Storage.Stake.Total_active_stake.(Storage_sigs.Indexed_data_storage.get).
Definition remove_contract_stake
(ctxt : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
: M? Raw_context.t :=
let? function_parameter := Contract_delegate_storage.find ctxt contract in
match function_parameter with
| None ⇒ return? ctxt
| Some delegate ⇒ remove_stake ctxt delegate amount
end.
Definition add_contract_stake
(ctxt : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
: M? Raw_context.t :=
let? function_parameter := Contract_delegate_storage.find ctxt contract in
match function_parameter with
| None ⇒ return? ctxt
| Some delegate ⇒ add_stake ctxt delegate amount
end.