👥 Delegate_slashed_deposits_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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
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 already_slashed_for_double_endorsing
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t) : M? bool :=
  let? function_parameter :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  match function_parameter with
  | None ⇒ Error_monad.return_false
  | Some slashed ⇒ return? slashed.(Storage.slashed_level.for_double_endorsing)
  end.

Definition already_slashed_for_double_baking
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t) : M? bool :=
  let? function_parameter :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  match function_parameter with
  | None ⇒ Error_monad.return_false
  | Some slashed ⇒ return? slashed.(Storage.slashed_level.for_double_baking)
  end.

Definition punish_double_endorsing
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t)
  : M? (Raw_context.t × Tez_repr.t × Receipt_repr.balance_updates) :=
  let? slashed :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  let? updated_slashed :=
    match slashed with
    | None ⇒
      return?
        {| Storage.slashed_level.for_double_endorsing := true;
          Storage.slashed_level.for_double_baking := false; |}
    | Some slashed ⇒
      if
        Compare.Bool.(Compare.S.op_eq)
          slashed.(Storage.slashed_level.for_double_endorsing) false
      then
        return? (Storage.slashed_level.with_for_double_endorsing true slashed)
      else
        Error_monad.error_value (Build_extensible "Asserted" unit tt)
    end in
  let delegate_contract := Contract_repr.Implicit delegate in
  let? frozen_deposits := Frozen_deposits_storage.get ctxt delegate_contract in
  let slashing_ratio :=
    Constants_storage.ratio_of_frozen_deposits_slashed_per_double_endorsement
      ctxt in
  let punish_value :=
    Tez_repr.div_exn
      (Tez_repr.mul_exn frozen_deposits.(Storage.deposits.initial_amount)
        slashing_ratio.(Ratio_repr.t.numerator))
      slashing_ratio.(Ratio_repr.t.denominator) in
  let amount_to_burn :=
    Tez_repr.min frozen_deposits.(Storage.deposits.current_amount) punish_value
    in
  let? '(ctxt, balance_updates) :=
    Token.transfer None ctxt
      (Token.Source_container (Token.Frozen_deposits delegate))
      (Token.Sink_infinite Token.Double_signing_punishments) amount_to_burn in
  let? ctxt := Stake_storage.remove_stake ctxt delegate amount_to_burn in
  let ctxt :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.add)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
      updated_slashed in
  return? (ctxt, amount_to_burn, balance_updates).

Definition punish_double_baking
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (level : Level_repr.t)
  : M? (Raw_context.t × Tez_repr.t × Receipt_repr.balance_updates) :=
  let? slashed :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.find)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
    in
  let? updated_slashed :=
    match slashed with
    | None ⇒
      return?
        {| Storage.slashed_level.for_double_endorsing := false;
          Storage.slashed_level.for_double_baking := true; |}
    | Some slashed ⇒
      if
        Compare.Bool.(Compare.S.op_eq)
          slashed.(Storage.slashed_level.for_double_baking) false
      then
        return? (Storage.slashed_level.with_for_double_baking true slashed)
      else
        Error_monad.error_value (Build_extensible "Asserted" unit tt)
    end in
  let delegate_contract := Contract_repr.Implicit delegate in
  let? frozen_deposits := Frozen_deposits_storage.get ctxt delegate_contract in
  let slashing_for_one_block := Constants_storage.double_baking_punishment ctxt
    in
  let amount_to_burn :=
    Tez_repr.min frozen_deposits.(Storage.deposits.current_amount)
      slashing_for_one_block in
  let? '(ctxt, balance_updates) :=
    Token.transfer None ctxt
      (Token.Source_container (Token.Frozen_deposits delegate))
      (Token.Sink_infinite Token.Double_signing_punishments) amount_to_burn in
  let? ctxt := Stake_storage.remove_stake ctxt delegate amount_to_burn in
  let ctxt :=
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.add)
      (ctxt, level.(Level_repr.t.cycle)) (level.(Level_repr.t.level), delegate)
      updated_slashed in
  return? (ctxt, amount_to_burn, balance_updates).

Definition clear_outdated_slashed_deposits
  (ctxt : Raw_context.t) (new_cycle : Cycle_repr.cycle) : M? Raw_context.t :=
  let max_slashable_period := Constants_storage.max_slashing_period ctxt in
  let? res := Cycle_repr.sub new_cycle max_slashable_period in
  match res with
  | None ⇒ return? ctxt
  | Some outdated_cycle ⇒
    Storage.Slashed_deposits.(Storage_sigs.Indexed_data_storage.clear)
      (ctxt, outdated_cycle)
  end.