🗳️ Voting_period_storage.v

Proofs

See code, Gitlab , OCaml

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

The function [overwrite_current_kind] is valid.

  Lemma overwrite_current_kind_is_valid ctxt chain_id kind_value :
    Raw_context.Valid.t ctxt →
    letP? ctxt :=
      Voting_period_storage.Testnet_dictator.overwrite_current_kind
        ctxt chain_id kind_value in
    Raw_context.Valid.t ctxt.
  Proof.
  Admitted.
End Testnet_dictator.