🗳️ Voting_period_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.

[get_current] after [init] is valid, as long as the value used in the initialization is valid

Lemma get_current_is_valid
  (ctxt : Raw_context.t) (period : Voting_period_repr.t) :
  Voting_period_repr.Valid.t period →
  letP? ctxt' := Voting_period_storage.init_value ctxt period in
  letP? v := Voting_period_storage.get_current ctxt in
    Voting_period_repr.Valid.t v.
Proof.
  intros.
  unfold Voting_period_storage.init_value,
    Voting_period_storage.get_current.
  rewrite Storage.Eq.Votes.Current_period.eq.(
    Storage_sigs.Single_data_storage.Eq.init_value); simpl.
  rewrite Storage.Eq.Votes.Current_period.eq.(
    Storage_sigs.Single_data_storage.Eq.get); simpl.
  Storage_sigs.Single_data_storage.Op.unfold_all.
  destruct Storage.Eq.Votes.Current_period.parse eqn:?; easy.
Qed.