Skip to main content

👥 Delegate_missed_endorsements_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.V7.
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
  | ParticipatedStake_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 bonuspay_block_producer ctxt block_producer bonus
    | Nonereturn? (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
  | Nonereturn? (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.