Skip to main content

🗳️ Voting_period_storage.v

Proofs

See code, Gitlab , OCaml

The function [blocks_per_voting_period] is valid.
The function [set_current] is valid.
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.

The function [init_value] is valid.
The function [init_first_period] is valid.
The function [common] is valid.
The function [reset] is valid.
The function [succ] is valid.
The function [get_current_kind] is valid.
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.

The function [get_current_remaining] is valid.
The function [is_last_block] is valid.
The function [blocks_before_activation] is valid.
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.

The function [get_rpc_succ_info] is valid.
The function [overwrite_current_kind] is valid.