🥖 Baking.v

Proofs

See code, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Baking.

Require TezosOfOCaml.Proto_alpha.Proofs.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Delegate_sampler.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Slot_repr.
Require TezosOfOCaml.Proto_alpha.Simulations.Baking.

Require Import FunctionalExtensionality.

[Baking.bonus_baking_reward] is valid.

Lemma bonus_baking_reward_is_valid
  (ctxt : Proto_alpha.Raw_context.t) (endorsing_power : int)
  : Raw_context.Valid.t ctxt →
    Pervasives.Int.Valid.t endorsing_power →
    endorsing_power ≥ Constants_storage.consensus_threshold ctxt →
    letP? reward :=
      Proto_alpha.Baking.bonus_baking_reward ctxt endorsing_power in
    Tez_repr.Valid.t reward.
Proof.
  intros H0 H1 H2.
  specialize
    (Constants_storage.baking_reward_bonus_per_slot_is_valid ctxt H0) as Hz.
  specialize
    (Constants_storage.consensus_threshold_is_valid ctxt H0) as Hw.
  unfold Proto_alpha.Baking.bonus_baking_reward.
  apply split_letP with (P:=(fun _ ⇒ True)).
  destruct (_ <i _); [reflexivity|]; exact I.
  intros.
  unfold Alpha_context.Tez.op_starquestion.
  step; step; [reflexivity|].
  step; [simpl; lia|].
  step; [reflexivity|].
  simpl; unfold "-i", Int64.of_int in *; simpl in ×.
  assert(Hx
    : normalize_int(
        endorsing_power - Alpha_context.Constants.consensus_threshold ctxt
      ) > 0)
    by lia.
  assert(Hy
    : (r ≤ max_int /i64 normalize_int (
         endorsing_power - Alpha_context.Constants.consensus_threshold ctxt)))
    by lia.
  clear - Hw Hx Hy Hz H0 H1 H2.
  rewrite Pervasives.normalize_identity in × by lia.
  unfold "*i64", "/i64" in ×.
  rewrite Int64.normalize_identity in × by nia.
  rewrite Int64.normalize_identity by nia.
  nia.
Qed.

[Baking.endorsing_rights_by_first_slot] is valid

Lemma endorsing_rights_is_valid
  (ctxt : Proto_alpha.Raw_context.t)
  (level : Level_repr.t)
  : Raw_context.Valid.t ctxt →
    Level_repr.Valid.t level →
    letP? '(ctxt, _) := Baking.endorsing_rights ctxt level in
    Raw_context.Valid.t ctxt.
Proof.
  intros.
  unfold Baking.endorsing_rights.
  eapply Error.split_letP; [apply Slot_repr.Range.create_is_valid|].
  intros; apply Slot_repr.Range.rev_fold_es_is_valid; trivial.
  intros [] **.
  eapply Error.split_letP;
    [apply Delegate_sampler.slot_owner_is_valid|]; trivial.
  intros [] **; trivial.
Qed.

[Baking.endorsing_rights_by_first_slot] is valid

Lemma endorsing_rights_by_first_slot_is_valid
  (ctxt : Proto_alpha.Raw_context.t)
  (endorsement_level : Level_repr.t)
  : Raw_context.Valid.t ctxt →
    Level_repr.Valid.t endorsement_level →
    letP? '(ctxt, _) := Baking.endorsing_rights_by_first_slot ctxt endorsement_level in
    Raw_context.Valid.t ctxt.
Proof.
  intros.
  unfold Baking.endorsing_rights_by_first_slot.
  specialize
    (Slot_repr.Range.create_is_valid
       0 (Alpha_context.Constants.consensus_committee_size ctxt)) as Hv.
  specialize
    (Slot_repr.Range.create_is_valid
       0 (Alpha_context.Constants.consensus_committee_size ctxt)) as Hie.
  destruct Alpha_context.Slot.Range.create as [[[]]|]; [|easy].
  with_strategy opaque [Alpha_context.Slot.Range.fold_es] simpl in ×.
  apply Error.split_letP
    with (P:=(fun '(ctxt, _) ⇒ Raw_context.Valid.t ctxt));
    [|intros [? []] ?; trivial].
  apply Slot_repr.Range.fold_es_is_valid; trivial.
  intros [? []] **.
  eapply split_letP; [apply Delegate_sampler.slot_owner_is_valid; trivial|].
  now intros []; step.
Qed.