Skip to main content

🪤 Stake_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.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_valuereturn? 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_balancereturn? (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
  | Nonereturn? ctxt
  | Some cycle_to_clearclear_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
  | trueget_staking_balance ctxt delegate
  | falsereturn? 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
  | Nonereturn? ctxt
  | Some delegateremove_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
  | Nonereturn? ctxt
  | Some delegateadd_stake ctxt delegate amount
  end.