Skip to main content

🗳️ Vote_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Stake_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_costs.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Vote_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.

Definition get_delegate_proposal_count
  (ctxt : Raw_context.t) (proposer : Signature.public_key_hash) : M? int :=
  Error_monad.op_gtpipeeqquestion
    (Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.find) ctxt
      proposer) (fun x_1Option.value_value x_1 0).

Definition set_delegate_proposal_count
  (ctxt : Raw_context.t) (proposer : Signature.public_key_hash) (count : int)
  : Raw_context.t :=
  Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.add) ctxt
    proposer count.

Definition has_proposed
  (ctxt : Raw_context.t) (proposer : Signature.public_key_hash)
  (proposal : Protocol_hash.t) : bool :=
  Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.mem) ctxt
    (proposal, proposer).

Definition add_proposal
  (ctxt : Raw_context.t) (proposer : Signature.public_key_hash)
  (proposal : Protocol_hash.t) : Raw_context.t :=
  Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.add) ctxt
    (proposal, proposer).

Definition get_proposals (ctxt : Raw_context.t)
  : M? (Protocol_hash.Map.(S.INDEXES_MAP.t) int64) :=
  Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.fold) ctxt
    (Variant.Build "Sorted" unit tt) Protocol_hash.Map.(S.INDEXES_MAP.empty)
    (fun (function_parameter : Protocol_hash.t × Signature.public_key_hash) ⇒
      let '(proposal, delegate) := function_parameter in
      fun (acc_value : Protocol_hash.Map.(S.INDEXES_MAP.t) int64) ⇒
        let? weight :=
          Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
            delegate in
        let previous :=
          match Protocol_hash.Map.(S.INDEXES_MAP.find) proposal acc_value with
          | None ⇒ 0
          | Some x_valuex_value
          end in
        return?
          (Protocol_hash.Map.(S.INDEXES_MAP.add) proposal (weight +i64 previous)
            acc_value)).

Definition clear_proposals (ctxt : Raw_context.t) : M? Raw_context.t :=
  let? ctxt :=
    Storage.Vote.Proposals_count.(Storage_sigs.Indexed_data_storage.clear) ctxt
    in
  Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.clear) ctxt.

Module ballots.
  Record record : Set := Build {
    yay : int64;
    nay : int64;
    pass : int64;
  }.
  Definition with_yay yay (r : record) :=
    Build yay r.(nay) r.(pass).
  Definition with_nay nay (r : record) :=
    Build r.(yay) nay r.(pass).
  Definition with_pass pass (r : record) :=
    Build r.(yay) r.(nay) pass.
End ballots.
Definition ballots := ballots.record.

Definition ballots_zero : ballots :=
  {| ballots.yay := 0; ballots.nay := 0; ballots.pass := 0; |}.

Definition ballots_encoding : Data_encoding.encoding ballots :=
  Data_encoding.conv
    (fun (function_parameter : ballots) ⇒
      let '{| ballots.yay := yay; ballots.nay := nay; ballots.pass := pass |} :=
        function_parameter in
      (yay, nay, pass))
    (fun (function_parameter : int64 × int64 × int64) ⇒
      let '(yay, nay, pass) := function_parameter in
      {| ballots.yay := yay; ballots.nay := nay; ballots.pass := pass; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None None "yay" Data_encoding.int64_value)
      (Data_encoding.req None None "nay" Data_encoding.int64_value)
      (Data_encoding.req None None "pass" Data_encoding.int64_value)).

Definition equal_ballots (b1 : ballots) (b2 : ballots) : bool :=
  (Int64.equal b1.(ballots.yay) b2.(ballots.yay)) &&
  ((Int64.equal b1.(ballots.nay) b2.(ballots.nay)) &&
  (Int64.equal b1.(ballots.pass) b2.(ballots.pass))).

Definition pp_ballots (ppf : Format.formatter) (b_value : ballots) : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal "{ yay = "
        (CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
          CamlinternalFormatBasics.No_padding
          CamlinternalFormatBasics.No_precision
          (CamlinternalFormatBasics.String_literal "; nay = "
            (CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
              CamlinternalFormatBasics.No_padding
              CamlinternalFormatBasics.No_precision
              (CamlinternalFormatBasics.String_literal "; pass = "
                (CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  (CamlinternalFormatBasics.String_literal " }"
                    CamlinternalFormatBasics.End_of_format)))))))
      "{ yay = %Ld; nay = %Ld; pass = %Ld }") b_value.(ballots.yay)
    b_value.(ballots.nay) b_value.(ballots.pass).

Definition has_recorded_ballot
  : Raw_context.t Signature.public_key_hash bool :=
  Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.mem).

Definition record_ballot
  : Raw_context.t Signature.public_key_hash Vote_repr.ballot
  M? Raw_context.t :=
  Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.init_value).

Definition get_ballots (ctxt : Raw_context.t) : M? ballots :=
  Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.fold) ctxt
    (Variant.Build "Sorted" unit tt) ballots_zero
    (fun (delegate : Signature.public_key_hash) ⇒
      fun (ballot : Vote_repr.ballot) ⇒
        fun (ballots : ballots) ⇒
          let? weight :=
            Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.get) ctxt
              delegate in
          let count := Int64.add weight in
          match ballot with
          | Vote_repr.Yay
            return? (ballots.with_yay (count ballots.(ballots.yay)) ballots)
          | Vote_repr.Nay
            return? (ballots.with_nay (count ballots.(ballots.nay)) ballots)
          | Vote_repr.Pass
            return? (ballots.with_pass (count ballots.(ballots.pass)) ballots)
          end).

Definition get_ballot_list
  : Raw_context.t M? (list (Signature.public_key_hash × Vote_repr.ballot)) :=
  Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.bindings).

Definition clear_ballots : Raw_context.t M? Raw_context.t :=
  Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.clear).

Definition listings_encoding
  : Data_encoding.encoding (list (Signature.public_key_hash × int64)) :=
  Data_encoding.list_value None
    (Data_encoding.obj2
      (Data_encoding.req None None "pkh"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
      (Data_encoding.req None None "voting_power" Data_encoding.int64_value)).

Definition update_listings (ctxt : Raw_context.t) : M? Raw_context.t :=
  let? ctxt :=
    Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.clear) ctxt in
  let? '(ctxt, total) :=
    Stake_storage.fold ctxt
      (fun (function_parameter : Signature.public_key_hash × Tez_repr.t) ⇒
        let '(delegate, stake) := function_parameter in
        fun (function_parameter : Raw_context.t × int64) ⇒
          let '(ctxt, total) := function_parameter in
          let weight := Tez_repr.to_mutez stake in
          let? ctxt :=
            Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.init_value)
              ctxt delegate weight in
          return? (ctxt, (total +i64 weight))) (Variant.Build "Sorted" unit tt)
      (ctxt, 0) in
  let ctxt :=
    Storage.Vote.Voting_power_in_listings.(Storage_sigs.Single_data_storage.add)
      ctxt total in
  return? ctxt.

Module delegate_info.
  Record record : Set := Build {
    voting_power : option Int64.t;
    current_ballot : option Vote_repr.ballot;
    current_proposals : list Protocol_hash.t;
    remaining_proposals : int;
  }.
  Definition with_voting_power voting_power (r : record) :=
    Build voting_power r.(current_ballot) r.(current_proposals)
      r.(remaining_proposals).
  Definition with_current_ballot current_ballot (r : record) :=
    Build r.(voting_power) current_ballot r.(current_proposals)
      r.(remaining_proposals).
  Definition with_current_proposals current_proposals (r : record) :=
    Build r.(voting_power) r.(current_ballot) current_proposals
      r.(remaining_proposals).
  Definition with_remaining_proposals remaining_proposals (r : record) :=
    Build r.(voting_power) r.(current_ballot) r.(current_proposals)
      remaining_proposals.
End delegate_info.
Definition delegate_info := delegate_info.record.

Definition pp_delegate_info
  (ppf : Format.formatter) (info_value : delegate_info) : unit :=
  match info_value.(delegate_info.voting_power) with
  | None
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Voting power: none"
          CamlinternalFormatBasics.End_of_format) "Voting power: none")
  | Some p_value
    let '_ :=
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Voting power: "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format)) "Voting power: %a")
        Tez_repr.pp (Tez_repr.of_mutez_exn p_value) in
    let '_ :=
      match info_value.(delegate_info.current_ballot) with
      | Nonett
      | Some ballot
        Format.fprintf ppf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@," 0 0)
              (CamlinternalFormatBasics.String_literal "Current ballot: "
                (CamlinternalFormatBasics.Alpha
                  CamlinternalFormatBasics.End_of_format)))
            "@,Current ballot: %a") Vote_repr.pp_ballot ballot
      end in
    match info_value.(delegate_info.current_proposals) with
    | []
      if info_value.(delegate_info.remaining_proposals) i 0 then
        Format.fprintf ppf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@," 0 0)
              (CamlinternalFormatBasics.String_literal "Remaining proposals: "
                (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  CamlinternalFormatBasics.End_of_format)))
            "@,Remaining proposals: %d")
          info_value.(delegate_info.remaining_proposals)
      else
        tt
    | proposals
      let '_ :=
        Format.fprintf ppf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@," 0 0)
              (CamlinternalFormatBasics.Formatting_gen
                (CamlinternalFormatBasics.Open_box
                  (CamlinternalFormatBasics.Format
                    (CamlinternalFormatBasics.String_literal "<v 2>"
                      CamlinternalFormatBasics.End_of_format) "<v 2>"))
                (CamlinternalFormatBasics.String_literal "Current proposals:"
                  CamlinternalFormatBasics.End_of_format)))
            "@,@[<v 2>Current proposals:") in
      let '_ :=
        List.iter
          (fun (p_value : Protocol_hash.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.Formatting_lit
                  (CamlinternalFormatBasics.Break "@," 0 0)
                  (CamlinternalFormatBasics.String_literal "- "
                    (CamlinternalFormatBasics.Alpha
                      CamlinternalFormatBasics.End_of_format))) "@,- %a")
              Protocol_hash.pp p_value) proposals in
      let '_ :=
        Format.fprintf ppf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.Formatting_lit
              CamlinternalFormatBasics.Close_box
              CamlinternalFormatBasics.End_of_format) "@]") in
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Formatting_lit
            (CamlinternalFormatBasics.Break "@," 0 0)
            (CamlinternalFormatBasics.String_literal "Remaining proposals: "
              (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.No_precision
                CamlinternalFormatBasics.End_of_format)))
          "@,Remaining proposals: %d")
        info_value.(delegate_info.remaining_proposals)
    end
  end.

Definition delegate_info_encoding : Data_encoding.encoding delegate_info :=
  Data_encoding.conv
    (fun (function_parameter : delegate_info) ⇒
      let '{|
        delegate_info.voting_power := voting_power;
          delegate_info.current_ballot := current_ballot;
          delegate_info.current_proposals := current_proposals;
          delegate_info.remaining_proposals := remaining_proposals
          |} := function_parameter in
      (voting_power, current_ballot, current_proposals, remaining_proposals))
    (fun (function_parameter :
      option Int64.t × option Vote_repr.ballot × list Protocol_hash.t × int) ⇒
      let
        '(voting_power, current_ballot, current_proposals, remaining_proposals) :=
        function_parameter in
      {| delegate_info.voting_power := voting_power;
        delegate_info.current_ballot := current_ballot;
        delegate_info.current_proposals := current_proposals;
        delegate_info.remaining_proposals := remaining_proposals; |}) None
    (Data_encoding.obj4
      (Data_encoding.opt None None "voting_power" Data_encoding.int64_value)
      (Data_encoding.opt None None "current_ballot" Vote_repr.ballot_encoding)
      (Data_encoding.dft None None "current_proposals"
        (Data_encoding.list_value None Protocol_hash.encoding) nil)
      (Data_encoding.dft None None "remaining_proposals" Data_encoding.int31 0)).

Definition in_listings : Raw_context.t Signature.public_key_hash bool :=
  Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.mem).

Definition get_listings
  : Raw_context.t M? (list (Signature.public_key_hash × int64)) :=
  Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.bindings).

Definition get_delegate_info
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? delegate_info :=
  let? voting_power :=
    Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt delegate
    in
  match voting_power with
  | None
    return?
      {| delegate_info.voting_power := voting_power;
        delegate_info.current_ballot := None;
        delegate_info.current_proposals := nil;
        delegate_info.remaining_proposals := 0; |}
  | Some _
    let? period := Voting_period_storage.get_current_kind ctxt in
    let? current_ballot :=
      match period with
      | (Voting_period_repr.Exploration | Voting_period_repr.Promotion) ⇒
        Storage.Vote.Ballots.(Storage_sigs.Indexed_data_storage.find) ctxt
          delegate
      |
        (Voting_period_repr.Proposal | Voting_period_repr.Cooldown |
        Voting_period_repr.Adoption) ⇒ return? None
      end in
    let? current_proposals :=
      match period with
      |
        (Voting_period_repr.Exploration | Voting_period_repr.Promotion |
        Voting_period_repr.Cooldown | Voting_period_repr.Adoption) ⇒
        return? nil
      | Voting_period_repr.Proposal
        Storage.Vote.Proposals.(Storage_sigs.Data_set_storage.fold) ctxt
          (Variant.Build "Undefined" unit tt) nil
          (fun (function_parameter :
            Protocol_hash.t × Signature.public_key_hash) ⇒
            let '(h_value, d_value) := function_parameter in
            fun (acc_value : list Protocol_hash.t) ⇒
              if
                Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
                  d_value delegate
              then
                return? (cons h_value acc_value)
              else
                return? acc_value)
      end in
    let remaining_proposals :=
      match period with
      | Voting_period_repr.Proposal
        Constants_repr.max_proposals_per_delegate -i
        (List.length current_proposals)
      | _ ⇒ 0
      end in
    return?
      {| delegate_info.voting_power := voting_power;
        delegate_info.current_ballot := current_ballot;
        delegate_info.current_proposals := current_proposals;
        delegate_info.remaining_proposals := remaining_proposals; |}
  end.

Definition get_voting_power_free
  (ctxt : Raw_context.t) (owner : Signature.public_key_hash) : M? int64 :=
  Error_monad.op_gtpipeeqquestion
    (Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt owner)
    (fun x_1Option.value_value x_1 0).

Definition get_voting_power
  (ctxt : Raw_context.t) (owner : Signature.public_key_hash)
  : M? (Raw_context.t × int64) :=
  let? ctxt := Raw_context.consume_gas ctxt (Storage_costs.read_access 4 8) in
  let? function_parameter :=
    Storage.Vote.Listings.(Storage_sigs.Indexed_data_storage.find) ctxt owner in
  match function_parameter with
  | Nonereturn? (ctxt, 0)
  | Some powerreturn? (ctxt, power)
  end.

Definition get_total_voting_power_free : Raw_context.t M? int64 :=
  Storage.Vote.Voting_power_in_listings.(Storage_sigs.Single_data_storage.get).

Definition get_total_voting_power (ctxt : Raw_context.t)
  : M? (Raw_context.t × int64) :=
  let? ctxt := Raw_context.consume_gas ctxt (Storage_costs.read_access 2 8) in
  let? total_voting_power := get_total_voting_power_free ctxt in
  return? (ctxt, total_voting_power).

Definition get_current_quorum (ctxt : Raw_context.t) : M? int32 :=
  let? participation_ema :=
    Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.get) ctxt
    in
  let quorum_min := Constants_storage.quorum_min ctxt in
  let quorum_max := Constants_storage.quorum_max ctxt in
  let quorum_diff := quorum_max -i32 quorum_min in
  return? (quorum_min +i32 ((participation_ema ×i32 quorum_diff) /i32 10000)).

Definition get_participation_ema : Raw_context.t M? int32 :=
  Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.get).

Definition set_participation_ema : Raw_context.t int32 M? Raw_context.t :=
  Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.update).

Definition current_proposal_exists : Raw_context.t bool :=
  Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.mem).

Definition get_current_proposal : Raw_context.t M? Protocol_hash.t :=
  Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.get).

Definition find_current_proposal
  : Raw_context.t M? (option Protocol_hash.t) :=
  Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.find).

Definition init_current_proposal
  : Raw_context.t Protocol_hash.t M? Raw_context.t :=
  Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.init_value).

Definition clear_current_proposal : Raw_context.t Raw_context.t :=
  Storage.Vote.Current_proposal.(Storage_sigs.Single_data_storage.remove).

Definition init_value (ctxt : Raw_context.t) (start_position : Int32.t)
  : M? Raw_context.t :=
  let participation_ema := Constants_storage.quorum_max ctxt in
  let? ctxt :=
    Storage.Vote.Participation_ema.(Storage_sigs.Single_data_storage.init_value)
      ctxt participation_ema in
  Voting_period_storage.init_first_period ctxt start_position.