🗳️ Vote_storage.v

Proofs

The function [get_delegate_proposal_count] is valid.

Lemma get_delegate_proposal_count_is_valid ctxt proposer :
  Raw_context.Valid.on
    (fun sim_ctxt : Raw_context.t ⇒
      Raw_context.Indexed_data_storage.value_exists
        (fun count ⇒
          count ≤ Constants_repr.max_proposals_per_delegate)
        proposer
        sim_ctxt
          .(Raw_context.Vote_Proposals_count)
    )
    ctxt →
  letP ? nb := Vote_storage.get_delegate_proposal_count ctxt proposer in
  nb ≤ Constants_repr.max_proposals_per_delegate.
Proof.
  intros H_ctxt_valid.
  unfold Vote_storage.get_delegate_proposal_count.
  Raw_context.Valid.destruct_rewrite H_ctxt_valid.
  rewrite_db storage_db. cbn in ×.
  unfold op_gtpipeeqquestion; cbn.
  match goal with
  | |- context [match ?e with _ ⇒ _ end] ⇒
      match type of H_sim_ctxt_domain with
      | context [match ?e' with _ ⇒ _ end] ⇒
          change e with e'
      end
  end.
  now step.
Qed.

The function [set_delegate_proposal_count] is valid.

The function [add_proposal] is valid.

The function [get_proposals] is valid.

The function [clear_proposals] is valid.

Lemma clear_proposals_is_valid ctxt :
  Raw_context.Valid.t ctxt →
  letP ? ctxt := Vote_storage.clear_proposals ctxt in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

Module ballots.
  Module Valid.
    Import Proto_alpha.Vote_storage.ballots.

Validity predicate for the type [ballots].

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

The function [ballots_zero] is valid.

Lemma ballots_zero_is_valid :
ballots.Valid.t Vote_storage.ballots_zero.
Proof.
constructor; simpl; lia.
Qed.

The encoding [ballots_encoding] is valid.

Lemma ballots_encoding_is_valid :
Data_encoding.Valid.t ballots.Valid.t Vote_storage.ballots_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve ballots_encoding_is_valid : Data_encoding_db.

The function [equal_ballots] is valid.

The function [record_ballot] is valid.

[has_recorded_ballot] after [record_ballot] returns [true]

The function [get_ballots] is valid.

The function [get_ballot_list] is valid.

The function [clear_ballots] is valid.

Validity predicate for listings.

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

The encoding [listings_encoding] is valid.

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

The function [update_listings] is valid.

Validity predicate for [delegate_info].

  Module Valid.
    Import Proto_alpha.Vote_storage.delegate_info.

    Record t (x : Vote_storage.delegate_info) : Prop := {
      voting_power : Option.Forall Int64.Valid.t x.(voting_power);
      remaining_proposals : Pervasives.Int31.Valid.t x.(remaining_proposals);
    }.
  End Valid.
End delegate_info.

The encoding [delegate_info_encoding] is valid.

Lemma delegate_info_encoding_is_valid :
  Data_encoding.Valid.t delegate_info.Valid.t
    Vote_storage.delegate_info_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  sauto l: on.
Qed.
#[global] Hint Resolve delegate_info_encoding_is_valid : Data_encoding_db.

The function [get_listings] is valid.