Skip to main content

🗳️ Vote_storage.v

Proofs

See code, Gitlab , OCaml

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.
Lemma get_proposals_is_valid ctxt :
  Raw_context.Valid.t ctxt
  letP? _ := Vote_storage.get_proposals ctxt in
  True.
Proof.
Admitted.

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.
The function [get_delegate_info] is valid.
The function [get_voting_power_free] is valid.
The function [get_voting_power] is valid.
Assuming enough gas, [get_voting_power] and [get_voting_power_free] are equal
Lemma get_voting_power_free_get_voting_power_eq ctxt owner :
  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.
Admitted.

The function [get_total_voting_power_free] is valid.
The function [get_total_voting_power] is valid.
The function [get_current_quorum] is valid.
The function [get_participation_ema] is valid.
The function [set_participation_ema] is valid.
The function [get_current_proposal] is valid.
The function [find_current_proposal] is valid.
The function [init_current_proposal] is valid.
The function [clear_current_proposal] is valid.
The function [init_value] is valid.