🧑⚖️ Amendment.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Vote_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Vote_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Amendment.
The function [select_winning_proposal] is valid
Lemma select_winning_proposal_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? _ := Amendment.select_winning_proposal ctxt in
True.
Proof.
intros H.
unfold Amendment.select_winning_proposal.
eapply Error.split_letP. {
now apply Vote_storage.get_proposals_is_valid.
}
intros.
step; [|easy].
do 2 step; [easy|].
step; [|easy].
eapply Error.split_letP. {
now apply Vote_storage.get_total_voting_power_free_is_valid.
}
intros.
now step.
Qed.
Raw_context.Valid.t ctxt →
letP? _ := Amendment.select_winning_proposal ctxt in
True.
Proof.
intros H.
unfold Amendment.select_winning_proposal.
eapply Error.split_letP. {
now apply Vote_storage.get_proposals_is_valid.
}
intros.
step; [|easy].
do 2 step; [easy|].
step; [|easy].
eapply Error.split_letP. {
now apply Vote_storage.get_total_voting_power_free_is_valid.
}
intros.
now step.
Qed.
The function [approval_and_participation_ema_is_valid] is valid
Lemma approval_and_participation_ema_is_valid
ballots maximum_vote participation_ema expected_quorum :
Vote_storage.ballots.Valid.t ballots →
Int64.Valid.t maximum_vote →
Int32.Valid.t participation_ema →
Int32.Valid.t expected_quorum →
let '(_, i) :=
Amendment.approval_and_participation_ema ballots maximum_vote
participation_ema expected_quorum in
Int32.Valid.t i.
Proof.
intros.
simpl.
unfold Z.of_int64, Z.of_int.
unfold Z.to_int32.
lia.
Qed.
ballots maximum_vote participation_ema expected_quorum :
Vote_storage.ballots.Valid.t ballots →
Int64.Valid.t maximum_vote →
Int32.Valid.t participation_ema →
Int32.Valid.t expected_quorum →
let '(_, i) :=
Amendment.approval_and_participation_ema ballots maximum_vote
participation_ema expected_quorum in
Int32.Valid.t i.
Proof.
intros.
simpl.
unfold Z.of_int64, Z.of_int.
unfold Z.to_int32.
lia.
Qed.
The function [get_approval_and_update_participation_ema] is valid
Lemma get_approval_and_update_participation_ema_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? '(ctxt', _) :=
Amendment.get_approval_and_update_participation_ema ctxt in
Raw_context.Valid.t ctxt'.
Proof.
intros H.
unfold Amendment.get_approval_and_update_participation_ema.
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_ballots_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_total_voting_power_free_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_participation_ema_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_current_quorum_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.clear_ballots_is_valid.
}
step.
eapply Error.split_letP.
{ pose proof
(approval_and_participation_ema_is_valid x x0 x1 x2)
as H_approval'.
repeat match goal with
| H_approval' : ?T → _,
H : ?T |- _ ⇒
specialize (H_approval' H)
end.
apply Vote_storage.set_participation_ema_is_valid; [easy|].
hauto lq:on.
}
{ hauto lq:on. }
Qed.
Raw_context.Valid.t ctxt →
letP? '(ctxt', _) :=
Amendment.get_approval_and_update_participation_ema ctxt in
Raw_context.Valid.t ctxt'.
Proof.
intros H.
unfold Amendment.get_approval_and_update_participation_ema.
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_ballots_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_total_voting_power_free_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_participation_ema_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_current_quorum_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.clear_ballots_is_valid.
}
step.
eapply Error.split_letP.
{ pose proof
(approval_and_participation_ema_is_valid x x0 x1 x2)
as H_approval'.
repeat match goal with
| H_approval' : ?T → _,
H : ?T |- _ ⇒
specialize (H_approval' H)
end.
apply Vote_storage.set_participation_ema_is_valid; [easy|].
hauto lq:on.
}
{ hauto lq:on. }
Qed.
The function [start_new_voting_period] is valid
Lemma start_new_voting_period_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? ctxt' :=
Amendment.start_new_voting_period ctxt in
Raw_context.Valid.t ctxt'.
Proof.
intros. unfold Amendment.start_new_voting_period.
eapply Error.split_letP; [|intros]. {
now apply Voting_period_storage.get_current_kind_is_valid.
}
step.
{ eapply Error.split_letP.
{ eapply Error.split_letP; [|intros]. {
now apply select_winning_proposal_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.clear_proposals_is_valid.
}
step.
{ eapply Error.split_letP; [|intros]. {
now apply Vote_storage.init_current_proposal_is_valid.
}
now apply Voting_period_storage.succ_is_valid.
}
{ now apply Voting_period_storage.reset_is_valid. }
}
{ intros.
now apply Vote_storage.update_listings_is_valid.
}
}
{ eapply Error.split_letP.
{ eapply Error.split_letP.
{ now apply get_approval_and_update_participation_ema_is_valid. }
{ intro. cbn. intros. step. step.
{ now apply Voting_period_storage.succ_is_valid. }
{ apply Voting_period_storage.reset_is_valid.
now apply Vote_storage.clear_current_proposal_is_valid.
}
}
}
{ intros.
now eapply Vote_storage.update_listings_is_valid.
}
}
{ eapply Error.split_letP; [|intros]. {
now apply Voting_period_storage.succ_is_valid.
}
now apply Vote_storage.update_listings_is_valid.
}
{ eapply Error.split_letP.
{ eapply Error.split_letP; [|intros]. {
now apply get_approval_and_update_participation_ema_is_valid.
}
do 2 step.
{ now apply Voting_period_storage.succ_is_valid. }
{ unfold Error_monad.op_gtgteq.
apply Voting_period_storage.reset_is_valid.
now apply Vote_storage.clear_current_proposal_is_valid.
}
}
{ intros.
now apply Vote_storage.update_listings_is_valid.
}
}
{ eapply Error.split_letP.
{ eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_current_proposal_is_valid.
}
eapply Error.split_letP.
{ apply Voting_period_storage.common_is_valid.
apply Vote_storage.clear_current_proposal_is_valid.
now apply Raw_context.activate_is_valid.
}
{ intros.
do 2 step.
apply Voting_period_storage.set_current_is_valid; [easy|].
now apply Voting_period_repr.raw_reset_is_valid.
}
}
{ intros.
now apply Vote_storage.update_listings_is_valid.
}
}
Qed.
Raw_context.Valid.t ctxt →
letP? ctxt' :=
Amendment.start_new_voting_period ctxt in
Raw_context.Valid.t ctxt'.
Proof.
intros. unfold Amendment.start_new_voting_period.
eapply Error.split_letP; [|intros]. {
now apply Voting_period_storage.get_current_kind_is_valid.
}
step.
{ eapply Error.split_letP.
{ eapply Error.split_letP; [|intros]. {
now apply select_winning_proposal_is_valid.
}
eapply Error.split_letP; [|intros]. {
now apply Vote_storage.clear_proposals_is_valid.
}
step.
{ eapply Error.split_letP; [|intros]. {
now apply Vote_storage.init_current_proposal_is_valid.
}
now apply Voting_period_storage.succ_is_valid.
}
{ now apply Voting_period_storage.reset_is_valid. }
}
{ intros.
now apply Vote_storage.update_listings_is_valid.
}
}
{ eapply Error.split_letP.
{ eapply Error.split_letP.
{ now apply get_approval_and_update_participation_ema_is_valid. }
{ intro. cbn. intros. step. step.
{ now apply Voting_period_storage.succ_is_valid. }
{ apply Voting_period_storage.reset_is_valid.
now apply Vote_storage.clear_current_proposal_is_valid.
}
}
}
{ intros.
now eapply Vote_storage.update_listings_is_valid.
}
}
{ eapply Error.split_letP; [|intros]. {
now apply Voting_period_storage.succ_is_valid.
}
now apply Vote_storage.update_listings_is_valid.
}
{ eapply Error.split_letP.
{ eapply Error.split_letP; [|intros]. {
now apply get_approval_and_update_participation_ema_is_valid.
}
do 2 step.
{ now apply Voting_period_storage.succ_is_valid. }
{ unfold Error_monad.op_gtgteq.
apply Voting_period_storage.reset_is_valid.
now apply Vote_storage.clear_current_proposal_is_valid.
}
}
{ intros.
now apply Vote_storage.update_listings_is_valid.
}
}
{ eapply Error.split_letP.
{ eapply Error.split_letP; [|intros]. {
now apply Vote_storage.get_current_proposal_is_valid.
}
eapply Error.split_letP.
{ apply Voting_period_storage.common_is_valid.
apply Vote_storage.clear_current_proposal_is_valid.
now apply Raw_context.activate_is_valid.
}
{ intros.
do 2 step.
apply Voting_period_storage.set_current_is_valid; [easy|].
now apply Voting_period_repr.raw_reset_is_valid.
}
}
{ intros.
now apply Vote_storage.update_listings_is_valid.
}
}
Qed.
The function [may_start_new_voting_period] is valid
Lemma may_start_new_voting_period_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? ctxt' :=
Amendment.may_start_new_voting_period ctxt in
Raw_context.Valid.t ctxt'.
Proof.
intros H.
eapply Error.split_letP; [|intros]. {
now apply Voting_period_storage.is_last_block_is_valid.
}
step.
{ now apply start_new_voting_period_is_valid. }
{ easy. }
Qed.
(* @TODO remove Proofs/Apply_results.v from blacklist *)
Raw_context.Valid.t ctxt →
letP? ctxt' :=
Amendment.may_start_new_voting_period ctxt in
Raw_context.Valid.t ctxt'.
Proof.
intros H.
eapply Error.split_letP; [|intros]. {
now apply Voting_period_storage.is_last_block_is_valid.
}
step.
{ now apply start_new_voting_period_is_valid. }
{ easy. }
Qed.
(* @TODO remove Proofs/Apply_results.v from blacklist *)
The function [apply_proposals] is valid
Lemma apply_proposals_is_valid ctxt chain_id contents :
Raw_context.Valid.t ctxt →
letP? '(ctxt', contents') :=
Amendment.apply_proposals ctxt chain_id contents in
Raw_context.Valid.t ctxt'.
Proof.
Admitted.
(* @TODO remove Proofs/Apply_results.v from blacklist *)
Raw_context.Valid.t ctxt →
letP? '(ctxt', contents') :=
Amendment.apply_proposals ctxt chain_id contents in
Raw_context.Valid.t ctxt'.
Proof.
Admitted.
(* @TODO remove Proofs/Apply_results.v from blacklist *)
The function [apply_ballot] is valid
Lemma apply_ballot_is_valid ctxt contents :
Raw_context.Valid.t ctxt →
letP? '(ctxt', contents') :=
Amendment.apply_ballot ctxt contents in
Raw_context.Valid.t ctxt'.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt', contents') :=
Amendment.apply_ballot ctxt contents in
Raw_context.Valid.t ctxt'.
Proof.
Admitted.