spec: add dao::vote()

doc/src/spec/contract/dao/scheme.md

@@ -1,4 +1,4 @@
-# Contract
+# Scheme
 
 <!-- toc -->
 
@@ -8,6 +8,8 @@ Let $𝔽ₚ, ℙₚ, \t{DerivePubKey}$ be defined as in the section [Pallas and
 
 Let $\t{PedersenCommit}$ be defined as in the section [Homomorphic Pedersen Commitments](../../crypto-schemes.md#homomorphic-pedersen-commitments).
 
+Let $\t{MerklePos}, \t{MerklePath}, \t{MerkleRoot}$ be defined as in the section [Incremental Merkle Tree](../../crypto-schemes.md#incremental-merkle-tree).
+
 Let $\t{Params}_\t{DAO}, \t{Bulla}_\t{DAO}, \t{Params}_\t{Proposal}, \t{Bulla}_\t{Proposal}$ be defined as in [DAO Model](model.md).
 
 ## Mint
@@ -63,7 +65,7 @@ $$ \begin{aligned}
   𝐢 &∈ \t{ProposeInput}^*
 \end{aligned} $$
 
-Define the DAO propose input function params
+Define the DAO propose-input function params
 $$ \begin{aligned}
   \t{ProposeInput}.\cN &∈ 𝔽ₚ \\
   \t{ProposeInput}.V &∈ ℙₚ \\
@@ -76,7 +78,7 @@ $$ \begin{aligned}
 ```
 
 ```rust
-{{#include ../../../../../src/contract/dao/src/model.rs:dao-propose-input-params}}
+{{#include ../../../../../src/contract/dao/src/model.rs:dao-propose-params-input}}
 ```
 
 ### Contract Statement
@@ -90,27 +92,27 @@ seen merkle root in the DAO contract merkle roots DB.
 
 **Proposal bulla uniqueness** &emsp; whether $𝒫 $ already exists. If yes then fail.
 
-Let there be a prover auxiliary witness inputs:
+Let there be prover auxiliary witness inputs:
 $$ \begin{aligned}
   v &∈ 𝔽ₚ \\
   bᵥ &∈ 𝔽ᵥ \\
   b_τ &∈ 𝔽ₚ \\
   p &∈ \t{Params}_\t{Proposal} \\
-  p_d &∈ 𝔽ₚ \\
+  b_p &∈ 𝔽ₚ \\
   d &∈ \t{Params}_\t{DAO} \\
   b_d &∈ 𝔽ₚ \\
   (ψ, Π) &∈ \t{MerklePos} × \t{MerklePath} \\
 \end{aligned} $$
-Attach a proof $π_\t{𝒫 }$ such that the following relations hold:
+Attach a proof $π_𝒫 $ such that the following relations hold:
 
 **Governance token commit** &emsp; export the DAO token ID as an encrypted pedersen
-commit $T = \t{PedersenCommit}(d.τ, d.b_τ)$ where $T = ∑_{i ∈ 𝐢} Tᵢ$.
+commit $T = \t{PedersenCommit}(d.τ, b_τ)$ where $T = ∑_{i ∈ 𝐢} Tᵢ$.
 
-**DAO bulla integrity** &emsp; $ℬ  = \t{Bulla}_\t{DAO}(d, b_d)$
+**DAO bulla integrity** &emsp; $𝒟  = \t{Bulla}_\t{DAO}(d, b_d)$
 
-**DAO existence** &emsp; $R_\t{DAO} = \t{MerkleRoot}(ψ, Π, ℬ )$
+**DAO existence** &emsp; $R_\t{DAO} = \t{MerkleRoot}(ψ, Π, 𝒟 )$
 
-**Proposal bulla integrity** &emsp; $𝒫 = \t{Bulla}_\t{Proposal}(p, p_d)$
+**Proposal bulla integrity** &emsp; $𝒫 = \t{Bulla}_\t{Proposal}(p, b_p)$
 where $p.t₀ = t₀$.
 
 **Proposer limit threshold met** &emsp; check the proposer has supplied enough
@@ -132,21 +134,119 @@ previously seen merkle root in the money contract merkle roots DB.
 &emsp; Let there be a prover auxiliary witness inputs:
 $$ \begin{aligned}
   x_c &∈ 𝔽ₚ \\
-  x_σ &∈ 𝔽ₚ \\
   c &∈ \t{Params}_\t{Coin} \\
   bᵥ &∈ 𝔽ᵥ \\
   b_τ &∈ 𝔽ₚ \\
   (ψᵢ, Πᵢ) &∈ \t{MerklePos} × \t{MerklePath} \\
+  x_σ &∈ 𝔽ₚ \\
 \end{aligned} $$
 &emsp; Attach a proof $π_i$ such that the following relations hold:
 
-&emsp; **Nullifier integrity** &emsp; $\cN = \t{PoseidonHash}(x_c, C)$.
+&emsp; **Nullifier integrity** &emsp; $\cN = \t{PoseidonHash}(x_c, C)$
+
+&emsp; **Coin value commit** &emsp; $i.V = \t{PedersenCommit}(c.v, bᵥ)$.
+
+&emsp; **Token commit** &emsp; $T = \t{PoseidonHash}(c.τ, b_τ)$.
+
+&emsp; **Valid coin** &emsp; Check $c.P = \t{DerivePubKey}(x_c)$. Let $C = \t{Coin}(c)$. Check $i.R_\t{coin} = \t{MerkleRoot}(ψᵢ, Πᵢ, C)$.
+
+&emsp; **Proof of signature public key ownership** &emsp; $i.\t{PK}_σ = \t{DerivePubKey}(x_σ)$.
+
+## Vote
+
+### Function Params
+
+Define the DAO vote function params
+$$ \begin{aligned}
+  τ &∈ 𝔽ₚ \\
+  𝒫 &∈ \t{im}(\t{Bulla}_\t{Proposal}) \\
+  Y &∈ ℙₚ \\
+  \t{EncNote} &∈ ⟂ \\
+  𝐢 &∈ \t{VoteInput}^*
+\end{aligned} $$
+
+Define the DAO vote-input function params
+$$ \begin{aligned}
+  \t{VoteInput}.𝒩 &∈ 𝔽ₚ \\
+  \t{VoteInput}.V &∈ ℙₚ \\
+  \t{VoteInput}.R_\t{coin} &∈ 𝔽ₚ \\
+  \t{VoteInput}.\t{PK}_σ &∈ ℙₚ
+\end{aligned} $$
+
+```rust
+{{#include ../../../../../src/contract/dao/src/model.rs:dao-vote-params}}
+```
+
+```rust
+{{#include ../../../../../src/contract/dao/src/model.rs:dao-vote-params-input}}
+```
+
+### Contract Statement
+
+**Proposal bulla exists** &emsp; check $𝒫 $ exists in the DAO contract proposal
+bullas DB.
+
+Let there be prover auxiliary witness inputs:
+$$ \begin{aligned}
+  p &∈ \t{Params}_\t{Proposal} \\
+  b_p &∈ 𝔽ₚ \\
+  d &∈ \t{Params}_\t{DAO} \\
+  b_d &∈ 𝔽ₚ \\
+  o &∈ 𝔽ₚ \\
+  b_y &∈ 𝔽ᵥ \\
+  v &∈ 𝔽ₚ \\
+  bᵥ &∈ 𝔽ᵥ \\
+  b_τ &∈ 𝔽ₚ \\
+  t_\t{now} &∈ 𝔽ₚ
+\end{aligned} $$
+Attach a proof $π_\mathcal{V}$ such that the following relations hold:
+
+**Governance token commit** &emsp; export the DAO token ID as an encrypted pedersen
+commit $T = \t{PedersenCommit}(d.τ, b_τ)$ where $T = ∑_{i ∈ 𝐢} Tᵢ$.
+
+**DAO bulla integrity** &emsp; $𝒟 = \t{Bulla}_\t{DAO}(d, b_d)$
+
+**Proposal bulla integrity** &emsp; $𝒫 = \t{Bulla}_\t{Proposal}(p, b_p)$
+
+**Yes vote commit** &emsp; $Y = \t{PedersenCommit}(ov, b_y)$
+
+**Total vote value commit** &emsp; $V = \t{PedersenCommit}(v, bᵥ)$ where
+$V = ∑_{i ∈ 𝐢} i.V$ should also hold.
+
+**Vote option boolean** &emsp; enforce $o ∈ \{ 0, 1 \}$.
+
+**Proposal not expired** &emsp; let $t_\t{end} = ℕ₆₄2𝔽ₚ(p.t₀) + ℕ₆₄2𝔽ₚ(p.D)$,
+and then check $t_\t{now} < t_\t{end}$.
+
+For each input $i ∈ 𝐢$,
+
+&emsp; **Valid input merkle root** &emsp; check that $i.R_\t{coin}$ is the
+previously seen merkle root in the proposal snapshot merkle root.
+
+&emsp; **Unused nullifier (money)** &emsp; check that $\cN$ does not exist in the
+money contract nullifiers DB.
+
+&emsp; **Unused nullifier (proposal)** &emsp; check that $\cN$ does not exist in the
+DAO contract nullifiers DB for this specific proposal.
+
+Let there be prover auxiliary witness inputs:
+$$ \begin{aligned}
+  x_c &∈ 𝔽ₚ \\
+  c &∈ \t{Params}_\t{Coin} \\
+  bᵥ &∈ 𝔽ᵥ \\
+  b_τ &∈ 𝔽ₚ \\
+  (ψᵢ, Πᵢ) &∈ \t{MerklePos} × \t{MerklePath} \\
+  x_σ &∈ 𝔽ₚ \\
+\end{aligned} $$
+Attach a proof $πᵢ$ such that the following relations hold:
+
+&emsp; **Nullifier integrity** &emsp; $\cN = \t{PoseidonHash}(x_c, C)$
 
 &emsp; **Coin value commit** &emsp; $i.V = \t{PedersenCommit}(c.v, bᵥ)$.
 
 &emsp; **Token commit** &emsp; $T = \t{PoseidonHash}(c.τ, b_τ)$.
 
-&emsp; **Valid coin** &emsp; Check $c.P = \t{DerivePubKey}(x_c)$. Let $C = \t{Commit}(c)$. Check $i.R_\t{coin} = \t{MerkleRoot}(ψᵢ, Πᵢ, C)$.
+&emsp; **Valid coin** &emsp; Check $c.P = \t{DerivePubKey}(x_c)$. Let $C = \t{Coin}(c)$. Check $i.R_\t{coin} = \t{MerkleRoot}(ψᵢ, Πᵢ, C)$.
 
 &emsp; **Proof of signature public key ownership** &emsp; $i.\t{PK}_σ = \t{DerivePubKey}(x_σ)$.
 

src/contract/dao/src/model.rs

@@ -237,7 +237,7 @@ pub struct DaoProposeParams {
 // ANCHOR_END: dao-propose-params
 
 #[derive(Debug, Clone, SerialEncodable, SerialDecodable)]
-// ANCHOR: dao-propose-input-params
+// ANCHOR: dao-propose-params-input
 /// Input for a DAO proposal
 pub struct DaoProposeParamsInput {
     pub nullifier: Nullifier,
@@ -248,7 +248,7 @@ pub struct DaoProposeParamsInput {
     /// Public key used for signing
     pub signature_public: PublicKey,
 }
-// ANCHOR_END: dao-propose-input-params
+// ANCHOR_END: dao-propose-params-input
 
 /// State update for `Dao::Propose`
 #[derive(Debug, Clone, SerialEncodable, SerialDecodable)]
@@ -268,8 +268,9 @@ pub struct DaoProposalMetadata {
     pub snapshot_root: MerkleNode,
 }
 
-/// Parameters for `Dao::Vote`
 #[derive(Debug, Clone, SerialEncodable, SerialDecodable)]
+// ANCHOR: dao-vote-params
+/// Parameters for `Dao::Vote`
 pub struct DaoVoteParams {
     /// Token commitment for the vote inputs
     pub token_commit: pallas::Base,
@@ -282,9 +283,11 @@ pub struct DaoVoteParams {
     /// Inputs for the vote
     pub inputs: Vec<DaoVoteParamsInput>,
 }
+// ANCHOR_END: dao-vote-params
 
-/// Input for a DAO proposal vote
 #[derive(Debug, Clone, SerialEncodable, SerialDecodable)]
+// ANCHOR: dao-vote-params-input
+/// Input for a DAO proposal vote
 pub struct DaoVoteParamsInput {
     /// Revealed nullifier
     pub nullifier: Nullifier,
@@ -295,6 +298,8 @@ pub struct DaoVoteParamsInput {
     /// Public key used for signing
     pub signature_public: PublicKey,
 }
+// ANCHOR_END: dao-vote-params-input
+/// Input for a DAO proposal vote
 
 /// State update for `Dao::Vote`
 #[derive(Debug, Clone, SerialEncodable, SerialDecodable)]