🗳️ Voting_period_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_generated.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_generated.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.
The function [blocks_per_voting_period] is valid.
Lemma blocks_per_voting_period_is_valid ctxt :
Raw_context.Valid.t ctxt →
Int32.Valid.t (Voting_period_storage.blocks_per_voting_period ctxt).
Proof.
intros.
unfold Voting_period_storage.blocks_per_voting_period; simpl.
lia.
Qed.
Raw_context.Valid.t ctxt →
Int32.Valid.t (Voting_period_storage.blocks_per_voting_period ctxt).
Proof.
intros.
unfold Voting_period_storage.blocks_per_voting_period; simpl.
lia.
Qed.
The function [set_current] is valid.
Lemma set_current_is_valid ctxt period :
Raw_context.Valid.t ctxt →
Voting_period_repr.Valid.t period →
letP? ctxt := Voting_period_storage.set_current ctxt period in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Voting_period_repr.Valid.t period →
letP? ctxt := Voting_period_storage.set_current ctxt period in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_current] is valid.
Lemma get_current_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? v := Voting_period_storage.get_current ctxt in
Voting_period_repr.Valid.t v.
Proof.
intros H.
Raw_context.Valid.destruct_rewrite H.
unfold Voting_period_storage.get_current.
rewrite Storage_generated.Vote.Current_period.get.
unfold Storage_generated.Vote.Current_period.Helpers.get.
destruct H_sim_ctxt, config, standalone, Vote.
now step.
Qed.
Raw_context.Valid.t ctxt →
letP? v := Voting_period_storage.get_current ctxt in
Voting_period_repr.Valid.t v.
Proof.
intros H.
Raw_context.Valid.destruct_rewrite H.
unfold Voting_period_storage.get_current.
rewrite Storage_generated.Vote.Current_period.get.
unfold Storage_generated.Vote.Current_period.Helpers.get.
destruct H_sim_ctxt, config, standalone, Vote.
now step.
Qed.
The function [init_value] is valid.
Lemma init_value_is_valid ctxt period :
Raw_context.Valid.t ctxt →
Voting_period_repr.Valid.t period →
letP? ctxt := Voting_period_storage.init_value ctxt period in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Voting_period_repr.Valid.t period →
letP? ctxt := Voting_period_storage.init_value ctxt period in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [init_first_period] is valid.
Lemma init_first_period_is_valid ctxt start_position :
Raw_context.Valid.t ctxt →
Int32.Valid.t start_position →
letP? ctxt := Voting_period_storage.init_first_period ctxt start_position in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Int32.Valid.t start_position →
letP? ctxt := Voting_period_storage.init_first_period ctxt start_position in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [common] is valid.
Lemma common_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? '(ctxt, period, position) := Voting_period_storage.common ctxt in
Raw_context.Valid.t ctxt ∧
Voting_period_repr.Valid.t period ∧
Int32.Valid.t position.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? '(ctxt, period, position) := Voting_period_storage.common ctxt in
Raw_context.Valid.t ctxt ∧
Voting_period_repr.Valid.t period ∧
Int32.Valid.t position.
Proof.
Admitted.
The function [reset] is valid.
Lemma reset_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? ctxt := Voting_period_storage.reset ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Voting_period_storage.reset ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [succ] is valid.
Lemma succ_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? ctxt := Voting_period_storage.succ ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Voting_period_storage.succ ctxt in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get_current_kind] is valid.
Lemma get_current_kind_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? kind := Voting_period_storage.get_current_kind ctxt in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? kind := Voting_period_storage.get_current_kind ctxt in
True.
Proof.
Admitted.
The function [get_current_info] is valid.
Lemma get_current_info_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? info :=
Voting_period_storage.get_current_info ctxt in
Voting_period_repr.Info.Valid.t info.
Proof.
intros.
unfold Voting_period_storage.get_current_info.
eapply Error.split_letP; [now apply get_current_is_valid|].
intros; simpl.
constructor; simpl; trivial;
try apply Voting_period_repr.position_since_is_valid;
try apply Voting_period_repr.remaining_blocks_is_valid.
Qed.
Raw_context.Valid.t ctxt →
letP? info :=
Voting_period_storage.get_current_info ctxt in
Voting_period_repr.Info.Valid.t info.
Proof.
intros.
unfold Voting_period_storage.get_current_info.
eapply Error.split_letP; [now apply get_current_is_valid|].
intros; simpl.
constructor; simpl; trivial;
try apply Voting_period_repr.position_since_is_valid;
try apply Voting_period_repr.remaining_blocks_is_valid.
Qed.
The function [get_current_remaining] is valid.
Lemma get_current_remaining_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? remaining := Voting_period_storage.get_current_remaining ctxt in
Int32.Valid.t remaining.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? remaining := Voting_period_storage.get_current_remaining ctxt in
Int32.Valid.t remaining.
Proof.
Admitted.
The function [is_last_block] is valid.
Lemma is_last_block_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? _ := Voting_period_storage.is_last_block ctxt in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? _ := Voting_period_storage.is_last_block ctxt in
True.
Proof.
Admitted.
The function [blocks_before_activation] is valid.
Lemma blocks_before_activation_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? blocks := Voting_period_storage.blocks_before_activation ctxt in
Option.Forall Int32.Valid.t blocks.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? blocks := Voting_period_storage.blocks_before_activation ctxt in
Option.Forall Int32.Valid.t blocks.
Proof.
Admitted.
The function [get_rpc_current_info] is valid.
Lemma get_rpc_current_info_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? info :=
Voting_period_storage.get_rpc_current_info ctxt in
Voting_period_repr.Info.Valid.t info.
Proof.
intros H.
Raw_context.Valid.destruct_rewrite H.
unfold Voting_period_storage.get_rpc_current_info.
eapply Error.split_letP; [now apply get_current_info_is_valid|].
intros.
step.
{ rewrite Storage_generated.Vote.Pred_period_kind.get.
destruct H_sim_ctxt, config, standalone, Vote.
unfold Storage_generated.Vote.Pred_period_kind.Helpers.get.
step; simpl; [|congruence].
constructor; simpl;
try apply Voting_period_repr.position_since_is_valid;
try apply Voting_period_repr.remaining_blocks_is_valid.
constructor; simpl; lia.
}
{ easy. }
Qed.
Raw_context.Valid.t ctxt →
letP? info :=
Voting_period_storage.get_rpc_current_info ctxt in
Voting_period_repr.Info.Valid.t info.
Proof.
intros H.
Raw_context.Valid.destruct_rewrite H.
unfold Voting_period_storage.get_rpc_current_info.
eapply Error.split_letP; [now apply get_current_info_is_valid|].
intros.
step.
{ rewrite Storage_generated.Vote.Pred_period_kind.get.
destruct H_sim_ctxt, config, standalone, Vote.
unfold Storage_generated.Vote.Pred_period_kind.Helpers.get.
step; simpl; [|congruence].
constructor; simpl;
try apply Voting_period_repr.position_since_is_valid;
try apply Voting_period_repr.remaining_blocks_is_valid.
constructor; simpl; lia.
}
{ easy. }
Qed.
The function [get_rpc_succ_info] is valid.
Lemma get_rpc_succ_info_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? info := Voting_period_storage.get_rpc_succ_info ctxt in
Voting_period_repr.Info.Valid.t info.
Proof.
Admitted.
Module Testnet_dictator.
Raw_context.Valid.t ctxt →
letP? info := Voting_period_storage.get_rpc_succ_info ctxt in
Voting_period_repr.Info.Valid.t info.
Proof.
Admitted.
Module Testnet_dictator.
The function [overwrite_current_kind] is valid.