Skip to main content

👥 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.
The function [record_endorsing_participation] is valid.
The function [record_baking_activity_and_pay_rewards_and_fees] is valid.
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].
The function [participation_info_value] is valid.