🥖 Baking.v

Proofs

[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.