👥 Delegate_missed_endorsements_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Delegate_missed_endorsements_storage.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.

The function [expected_slots_for_given_active_stake] is valid.

Lemma expected_slots_for_given_active_stake_is_valid
  ctxt total_active_stake active_stake :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t total_active_stake →
  Tez_repr.Valid.t active_stake →
  Pervasives.Int.Valid.t (
    Delegate_missed_endorsements_storage.expected_slots_for_given_active_stake
      ctxt total_active_stake active_stake
  ).
Proof.
Admitted.

The function [record_endorsing_participation] is valid.

Lemma record_endorsing_participation_is_valid
  ctxt delegate participation endorsing_power:
  Raw_context.Valid.t ctxt →
  Pervasives.Int.Valid.t endorsing_power →
  letP? ctxt :=
    Delegate_missed_endorsements_storage.record_endorsing_participation
      ctxt delegate participation endorsing_power in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [record_baking_activity_and_pay_rewards_and_fees] is valid.

Lemma record_baking_activity_and_pay_rewards_and_fees_is_valid
  ctxt payload_producer block_producer baking_reward reward_bonus :
  Raw_context.Valid.t ctxt →
  Tez_repr.Valid.t baking_reward →
  Option.Forall Tez_repr.Valid.t reward_bonus →
  letP? '(ctxt, udpates) :=
    Delegate_missed_endorsements_storage.record_baking_activity_and_pay_rewards_and_fees
      ctxt payload_producer block_producer baking_reward reward_bonus in
  Raw_context.Valid.t ctxt ∧
  Receipt_repr.balance_updates.Valid.t udpates.
Proof.
Admitted.

The function [check_and_reset_delegate_participation] is valid.

Lemma check_and_reset_delegate_participation_is_valid ctxt delegate:
  Raw_context.Valid.t ctxt →
  letP? '(ctxt, _) :=
    Delegate_missed_endorsements_storage.check_and_reset_delegate_participation
      ctxt delegate in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

Module participation_info.
  Module Valid.
    Import Proto_alpha.Delegate_missed_endorsements_storage.participation_info.

Validity predicate for [participation_info].

    Record t (x : Delegate_missed_endorsements_storage.participation_info) :
      Prop := {
      expected_cycle_activity :
        Pervasives.Int.Valid.t x.(expected_cycle_activity);
      minimal_cycle_activity :
        Pervasives.Int.Valid.t x.(minimal_cycle_activity);
      missed_slots :
        Pervasives.Int.Valid.t x.(missed_slots);
      missed_levels :
        Pervasives.Int.Valid.t x.(missed_levels);
      remaining_allowed_missed_slots :
        Pervasives.Int.Valid.t x.(remaining_allowed_missed_slots);
      expected_endorsing_rewards :
        Tez_repr.Valid.t x.(expected_endorsing_rewards);
    }.
  End Valid.
End participation_info.

The function [participation_info_value] is valid.

Lemma participation_info_value_is_valid ctxt delegate :
  Raw_context.Valid.t ctxt →
  letP? info :=
    Delegate_missed_endorsements_storage.participation_info_value
      ctxt delegate in
  participation_info.Valid.t info.
Proof.
Admitted.