🗳️ Vote_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.Vote_storage.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Proofs.Utils.

[has_recorded_ballot] after [record_ballot] returns [true]

Lemma has_recorded_ballot_eq_true (ctxt : Raw_context.t) (pkh : public_key_hash)
  (ballot : Vote_repr.ballot) :
  letP? ctxt' := Vote_storage.record_ballot ctxt pkh ballot in
  Vote_storage.has_recorded_ballot ctxt' pkh = true.
Proof.
  unfold Vote_storage.record_ballot.
  rewrite Storage.Eq.Votes.Ballots.eq.(
    Indexed_data_storage.Eq.init_value); simpl.
  Indexed_data_storage.Op.Unfold.all.
  destruct (Map.Make _).(S.mem) eqn:?; [easy|]; simpl.
  unfold Vote_storage.has_recorded_ballot.
  rewrite Storage.Eq.Votes.Ballots.eq.(
    Indexed_data_storage.Eq.mem); simpl.
  Storage.auto_parse_apply; simpl.
  Indexed_data_storage.Op.Unfold.all.
  rewrite Map.mem_add_eq; try easy.
  apply Storage.generic_Path_encoding_Valid.
Qed.

Assuming enough gas, [get_voting_power] and [get_voting_power_free] are equal

Lemma get_voting_power_free_get_voting_power_eq
  (ctxt : Raw_context.t) (owner : public_key_hash) :
  letP? ctxt' := Raw_context.consume_gas
     ctxt (Storage_costs.read_access 4 8) in
  let results :=
    (Vote_storage.get_voting_power ctxt owner,
     Vote_storage.get_voting_power_free ctxt' owner) in
  match results with
  | (Pervasives.Ok (_, power), Pervasives.Ok power') ⇒
      power = power'
  | (_, _) ⇒ True
  end.
Proof.
  destruct Raw_context.consume_gas eqn:?; [|easy]; simpl.
  unfold Vote_storage.get_voting_power. rewrite Heqt. simpl.
  unfold Vote_storage.get_voting_power_free.
  destruct (_.(Storage_sigs.Indexed_data_storage.find) t _) eqn:?;
    [|easy]; simpl.
  now destruct o.
Qed.

[recorded_proposal_count] after [record_proposal] returns [Pervasives.Ok]

Lemma recorded_proposal_count_for_delegate_is_ok
  (ctxt : Raw_context.t) (proposer : public_key_hash)
  (proposal : Protocol_hash.t) :
  letP? ctxt' := Vote_storage.record_proposal
    ctxt proposal proposer in
  Pervasives.is_ok (Vote_storage.recorded_proposal_count_for_delegate
    ctxt' proposer).
Proof.
  unfold Vote_storage.record_proposal.
  destruct Vote_storage.recorded_proposal_count_for_delegate
    eqn:?; [|easy]; simpl.
  unfold Vote_storage.recorded_proposal_count_for_delegate.
  rewrite Storage.Eq.Votes.Proposals_count.eq
      .(Indexed_data_storage.Eq.find),
    Storage.Eq.Votes.Proposals.eq
      .(Data_set_storage.Eq.add),
    Storage.Eq.Votes.Proposals_count.eq
      .(Indexed_data_storage.Eq.add); simpl.
  Indexed_data_storage.Op.Unfold.all.
  Data_set_storage.Op.unfold_all.
  Storage.auto_parse_apply.
  Indexed_data_storage.Op.Unfold.all.
  rewrite Map.find_add_eq_some; [easy|].
  simpl.
  apply Storage.generic_Path_encoding_Valid.
Qed.

Module Ballots.
  Module Valid.
    Import Vote_storage.ballots.

    Record t (x : Vote_storage.ballots) : Prop := {
      yay : Int32.Valid.t x.(yay);
      nay : Int32.Valid.t x.(nay);
      pass : Int32.Valid.t x.(pass);
    }.
  End Valid.
End Ballots.

Lemma ballots_encoding_is_valid :
  Data_encoding.Valid.t Ballots.Valid.t Vote_storage.ballots_encoding.
  Data_encoding.Valid.data_encoding_auto.
  intros [] []; simpl in *; repeat split; trivial; lia.
Qed.
#[global] Hint Resolve ballots_encoding_is_valid : Data_encoding_db.

Module Listings.
  Module Valid.
    Definition t (l : list (Signature.public_key_hash × int32)) : Prop :=
      List.Forall (fun '(_, rolls) ⇒ Int32.Valid.t rolls) l.
  End Valid.
End Listings.

Lemma listings_encoding_is_valid :
  Data_encoding.Valid.t Listings.Valid.t Vote_storage.listings_encoding.
  Data_encoding.Valid.data_encoding_auto.
  apply List.Forall_impl; intros []; lia.
Qed.
#[global] Hint Resolve listings_encoding_is_valid : Data_encoding_db.