🗳️ Voting_services.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Voting_services.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.
Require TezosOfOCaml.Environment.V8.Proofs.Protocol_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Vote_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.

Module S.
  Lemma ballots_is_valid :
    RPC_service.Valid.t
      (fun _ ⇒ True) (fun _ ⇒ True) Vote_storage.ballots.Valid.t
      Voting_services.S.ballots.
  Proof.
    RPC_service.rpc_auto.
  Qed.

  Lemma ballot_list_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Voting_services.S.ballot_list.
  Proof.
    RPC_service.rpc_auto.
    intros x [].
    hauto l: on use: List.Forall_forall.
  Qed.

  Lemma current_period_is_valid :
    RPC_service.Valid.t
      (fun _ ⇒ True) (fun _ ⇒ True) Voting_period_repr.Info.Valid.t
      Voting_services.S.current_period.
  Proof.
    RPC_service.rpc_auto.
  Qed.

  Lemma successor_period_is_valid :
    RPC_service.Valid.t
      (fun _ ⇒ True) (fun _ ⇒ True) Voting_period_repr.Info.Valid.t
      Voting_services.S.successor_period.
  Proof.
    RPC_service.rpc_auto.
  Qed.

  Lemma current_quorum_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Int32.Valid.t
      Voting_services.S.current_quorum.
  Proof.
    RPC_service.rpc_auto.
  Qed.

  Lemma listings_is_valid :
    RPC_service.Valid.t
      (fun _ ⇒ True) (fun _ ⇒ True) Vote_storage.Listings.Valid.t
      Voting_services.S.listings.
  Proof.
    RPC_service.rpc_auto.
  Qed.

  Lemma proposals_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Voting_services.S.proposals.
  Proof.
    RPC_service.rpc_auto.
    { eapply Protocol_hash.Map_encoding_is_valid.
      apply Data_encoding.Valid.int64_value.
    }
    { Data_encoding.Valid.data_encoding_auto. }
  Qed.

  Lemma current_proposal_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) (fun _ ⇒ True)
      Voting_services.S.current_proposal.
  Proof.
    RPC_service.rpc_auto.
  Qed.

  Lemma total_voting_power_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True) Int32.Valid.t
      Voting_services.S.total_voting_power.
  Proof.
    RPC_service.rpc_auto.
    intros; lia.
  Qed.
End S.