From e2787149e5b867d9feb1b1703ebe3a4be8db8453 Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Mon, 11 Mar 2024 14:40:35 -0400 Subject: [PATCH 1/8] WIP --- docs/protocol/src/SUMMARY.md | 1 + docs/protocol/src/transactions/invariants.md | 62 ++++++++++++++++++++ 2 files changed, 63 insertions(+) create mode 100644 docs/protocol/src/transactions/invariants.md diff --git a/docs/protocol/src/SUMMARY.md b/docs/protocol/src/SUMMARY.md index a3929f4448..1a4736043a 100644 --- a/docs/protocol/src/SUMMARY.md +++ b/docs/protocol/src/SUMMARY.md @@ -49,6 +49,7 @@ - [Assets and Values](./assets.md) - [Transaction Model](./transactions.md) - [Transaction Signing](./transactions/signing.md) + - [Action Invariants](./transactions/invariants.md) - [Action Reference](./transactions/actions.md) - [Multi-Asset Shielded Pool](./shielded_pool.md) - [Note Plaintexts](./shielded_pool/note_plaintexts.md) diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md new file mode 100644 index 0000000000..5c0cb0743d --- /dev/null +++ b/docs/protocol/src/transactions/invariants.md @@ -0,0 +1,62 @@ + +# System-Level + +#### Invariants + +1. Value cannot be created or destroyed after genesis or via IBC. Value cannot be created by the DEX. +1.1. Each action may create or destroy value, but commits to this imbalance, which when summed over a transaction, will not violate this rule. +2. Individual actions are bound to the transaction they belong to. + +#### Justification + +1.1. We check that the summed balance commitment of a transaction commits to 0. + +## Action-Level + +### Community Pool Output + +#### Global Violations + +### Spend + +#### Local Invariants + +1. You must have spend authority over the note to spend +2. You can't spend a positioned note twice. +2.1. Each positioned note has exactly one valid nullifier for it. +2.2. No two spends on the ledger, even in the same transaction, can have the same nullifier. +3. You can't spend a note that has not been created, unless the amount of that note is 0. + +#### Local Justification + +1. We verify the auth_sig using the randomized verification key, which must not be 0, provided on the spend body, even if the amount of the note is 0. A note's transmission key binds the authority. +2.1. A note's transmission key binds to the nullifier key, and all components of a positioned note, along with this key are hashed to derive the nullifier, in circuit. +2.2. This is in check_stateful, and an external check about the integrity of each transaction. + +#### Global Justification + +1.1. This action destroys the value of the note spent, and is reflected in the balance. We do not create value, because of 3. + +### Delegator Votes + +#### Local Invariants + +Privacy note: Value of staked note used for voting is revealed during a delegator vote. + +1. Available voting power for a proposal = total delegated stake to active validators when the proposal was created +1.1 Voting power must have been present before the proposal was created. +1.2 You can't vote with a note that was spent prior to proposal start. +1.3 That staked note must correspond to a validator that was in the active set when the +proposal being voted on was created. +2. You can't use the same voting power twice on a proposal. +3. You can't vote on a proposal that is not votable, i.e. it has not been withdrawn or voting has finished. +4. All invariants with regards to spending a note apply to voting with it. + +#### Local Justification + +1.1 The circuit checks the age of the staked note, and the stateful check verifies that the claimed position matches that of the proposal. +1.2 We check that the note was spent only after the block of the proposal. +1.3 The stateful check for the exchange rate makes sure the validator was active at that time. +2. We maintain a nullifier set for delegator votes and check for duplicate nullifiers in the stateful checks. +3. The stateful check looks up the proposal ID and ensures it is votable. +4. c.f. justification for spend circuit From 236582a7c39d908b65553f003052a8c4149fcf7f Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Mon, 4 Mar 2024 18:00:34 -0500 Subject: [PATCH 2/8] spec: output invariants --- docs/protocol/src/transactions/invariants.md | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md index 5c0cb0743d..67f7c5ab38 100644 --- a/docs/protocol/src/transactions/invariants.md +++ b/docs/protocol/src/transactions/invariants.md @@ -1,5 +1,5 @@ -# System-Level +# System-Level #### Invariants @@ -13,9 +13,22 @@ ## Action-Level -### Community Pool Output +### Output -#### Global Violations +#### Local Invariants + +1. The created output note is spendable by the recipient if its nullifier has not been revealed. +1.1 The output note is bound to the recipient. +1.2 The output note can be spent only by the recipient. + +#### Local Justification + +1.1 The note commitment binds the note to the typed value and the address of the recipient. +1.2 Each note has a unique note commitment if the note blinding factor is unique for duplicate (recipient, typed value) pairs. Duplicate note commitments are allowed on chain since they commit to the same (recipient, typed value) pair. + +#### Global Justification + +1.1 This action contributes the value of the output note, which is summed as part of the transaction value balance. Value is not created due to system level invariant 1, which ensures that transactions contribute a 0 value balance. ### Spend From 57486a321bed08b6546ca7c04913e7e5f7b83075 Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Thu, 7 Mar 2024 22:55:42 -0500 Subject: [PATCH 3/8] spec: start of swap claim and swap section --- docs/protocol/src/transactions/invariants.md | 48 ++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md index 67f7c5ab38..6f9a446d2a 100644 --- a/docs/protocol/src/transactions/invariants.md +++ b/docs/protocol/src/transactions/invariants.md @@ -45,6 +45,7 @@ 1. We verify the auth_sig using the randomized verification key, which must not be 0, provided on the spend body, even if the amount of the note is 0. A note's transmission key binds the authority. 2.1. A note's transmission key binds to the nullifier key, and all components of a positioned note, along with this key are hashed to derive the nullifier, in circuit. 2.2. This is in check_stateful, and an external check about the integrity of each transaction. +3. The circuit verifies for non-zero amounts that there is a valid Merkle authentication path to the note in the global state commitment tree. #### Global Justification @@ -73,3 +74,50 @@ proposal being voted on was created. 2. We maintain a nullifier set for delegator votes and check for duplicate nullifiers in the stateful checks. 3. The stateful check looks up the proposal ID and ensures it is votable. 4. c.f. justification for spend circuit + +### Swap + +#### Local Invariants + +#### Local Justification + +#### Global Justification + +1.1 This action destroys the value of the two input notes (one per asset) consumed, and is reflected in the balance. We do not create value, because of 3. +1.2 TK (fee commitment) + +### SwapClaim + +#### Local Invariants + +1. You cannot mint swap outputs to a different address than what was specified during the initial swap. +2. You cannot mint swap outputs to different assets than those specified in the original swap. +3. You cannot mint swap outputs to different amounts than those specified by the batch swap output data. +3.1. You can only claim your contribution to the batch swap outputs. +3.2 You can only claim the outputs using the batch swap output data for the block in which the swap was executed. +4. You can only claim swap outputs for swaps that occurred. +5. You can only claim swap outputs once. +5.1. Each positioned swap has exactly one valid nullifier for it. +5.2. No two swaps can have the same nullifier. + +#### Local Justification + +1. The Swap commits to the claim address. The SwapClaim circuit enforces that the same address used to derive the swap commitment is that used to derive the note commitments for the two output notes. +2. The SwapClaim circuit checks that the trading pair on the original Swap is the same as that on the batch swap output data. + +TODO: What happens if we swap the order of asset IDs? There is a canonical ordering OOC for a TradingPair that is not checked in-circuit. + +3.1 The output amounts of each note is checked in-circuit to be only due to that user's contribution of the batch swap output data. +3.2 The circuit checks the block height of the swap matches that of the batch swap output data. The ActionHandler for the SwapClaim checks that the batch swap output data provided by the SwapClaim matches that saved on-chain for that output height and trading pair. + +4. The SwapClaim circuit verifies that there is a valid Merkle authentication path to the swap in the global state commitment tree. + +5.1. A swap's transmission key binds to the nullifier key, and all components of a positioned swap, along with this key are hashed to derive the nullifier, in circuit. + +TODO: The binding of the transmission key to the nullifier key is not currently checked in circuit + +5.2. In the ActionHandler for check_stateful we check that the nullifier is unspent. + +#### Global Justification + +TK \ No newline at end of file From 6f8fb4947e63d8d5fd484b0a5a0ba1bb34a69830 Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Mon, 11 Mar 2024 13:37:54 -0400 Subject: [PATCH 4/8] spec: more Swap/SwapClaim invariants --- docs/protocol/src/transactions/invariants.md | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md index 6f9a446d2a..3c385c1fd2 100644 --- a/docs/protocol/src/transactions/invariants.md +++ b/docs/protocol/src/transactions/invariants.md @@ -49,7 +49,7 @@ #### Global Justification -1.1. This action destroys the value of the note spent, and is reflected in the balance. We do not create value, because of 3. +1.1. This action destroys the value of the note spent, and is reflected in the balance by adding the value to the transaction value balance. We do not create value, because of 3. ### Delegator Votes @@ -79,12 +79,17 @@ proposal being voted on was created. #### Local Invariants +1. The swap binds to the specific trading pair. +2. The swap binds to a specific claim address. + #### Local Justification +1. The swap commitment includes as inputs the trading pair of the two assets. +2. The swap commitment includes as inputs each component of the claim address. + #### Global Justification -1.1 This action destroys the value of the two input notes (one per asset) consumed, and is reflected in the balance. We do not create value, because of 3. -1.2 TK (fee commitment) +1.1 This action consumes the value of the two input notes (one per asset) consumed and the value of the pre-paid fee to be used by the SwapClaim, and is reflected in the balance by subtracting the value from the transaction value balance. We do not create value, because of 3. ### SwapClaim @@ -114,10 +119,10 @@ TODO: What happens if we swap the order of asset IDs? There is a canonical order 5.1. A swap's transmission key binds to the nullifier key, and all components of a positioned swap, along with this key are hashed to derive the nullifier, in circuit. -TODO: The binding of the transmission key to the nullifier key is not currently checked in circuit +TODO: The binding of the transmission key to the nullifier key is not currently checked in circuit. Issue: https://github.com/penumbra-zone/penumbra/issues/3978 5.2. In the ActionHandler for check_stateful we check that the nullifier is unspent. #### Global Justification -TK \ No newline at end of file +1.1 This action mints the swap's output notes, and is reflected in the balance by adding the value from the transaction value balance. We do not create value, because of 3. From 04377032d9b33e934814996b9ff9b835c31409e0 Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Mon, 11 Mar 2024 14:33:26 -0400 Subject: [PATCH 5/8] spec: UndelegateClaim --- docs/protocol/src/transactions/invariants.md | 22 +++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md index 3c385c1fd2..ff63a6f458 100644 --- a/docs/protocol/src/transactions/invariants.md +++ b/docs/protocol/src/transactions/invariants.md @@ -110,8 +110,6 @@ proposal being voted on was created. 1. The Swap commits to the claim address. The SwapClaim circuit enforces that the same address used to derive the swap commitment is that used to derive the note commitments for the two output notes. 2. The SwapClaim circuit checks that the trading pair on the original Swap is the same as that on the batch swap output data. -TODO: What happens if we swap the order of asset IDs? There is a canonical ordering OOC for a TradingPair that is not checked in-circuit. - 3.1 The output amounts of each note is checked in-circuit to be only due to that user's contribution of the batch swap output data. 3.2 The circuit checks the block height of the swap matches that of the batch swap output data. The ActionHandler for the SwapClaim checks that the batch swap output data provided by the SwapClaim matches that saved on-chain for that output height and trading pair. @@ -119,10 +117,24 @@ TODO: What happens if we swap the order of asset IDs? There is a canonical order 5.1. A swap's transmission key binds to the nullifier key, and all components of a positioned swap, along with this key are hashed to derive the nullifier, in circuit. -TODO: The binding of the transmission key to the nullifier key is not currently checked in circuit. Issue: https://github.com/penumbra-zone/penumbra/issues/3978 - -5.2. In the ActionHandler for check_stateful we check that the nullifier is unspent. +5.2. In the `ActionHandler` for `check_stateful` we check that the nullifier is unspent. #### Global Justification 1.1 This action mints the swap's output notes, and is reflected in the balance by adding the value from the transaction value balance. We do not create value, because of 3. + +### UndelegateClaim + +#### Local Invariants + +1. You cannot claim undelegations that have not finishing unbonding. +2. Slashing penalties must be applied when unbonding. + +#### Local Justification + +1. In the `ActionHandler` for `check_stateful` we check that the undelegations have finished unbonding. +2. The `ConvertCircuit` verifies that the conversion from the unbonding token to the staking token was done using the correct conversion rate calculated from the penalty. We check in the `ActionHandler` for `check_stateful` that the _correct_ penalty was used. + +#### Global Justification + +1.1. This action consumes the amount of the unbonding tokens and contributes the unbonded amount of the staking tokens to the transaction's value balance. We do not create value, because of 3. From c933d9912ea0af765623b94bb987bbc0f45453d9 Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Mon, 11 Mar 2024 14:37:16 -0400 Subject: [PATCH 6/8] spec: clean up formatting of invariants section --- docs/protocol/src/transactions/invariants.md | 33 ++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md index ff63a6f458..e910a2ebba 100644 --- a/docs/protocol/src/transactions/invariants.md +++ b/docs/protocol/src/transactions/invariants.md @@ -4,7 +4,9 @@ #### Invariants 1. Value cannot be created or destroyed after genesis or via IBC. Value cannot be created by the DEX. + 1.1. Each action may create or destroy value, but commits to this imbalance, which when summed over a transaction, will not violate this rule. + 2. Individual actions are bound to the transaction they belong to. #### Justification @@ -18,12 +20,15 @@ #### Local Invariants 1. The created output note is spendable by the recipient if its nullifier has not been revealed. + 1.1 The output note is bound to the recipient. + 1.2 The output note can be spent only by the recipient. #### Local Justification 1.1 The note commitment binds the note to the typed value and the address of the recipient. + 1.2 Each note has a unique note commitment if the note blinding factor is unique for duplicate (recipient, typed value) pairs. Duplicate note commitments are allowed on chain since they commit to the same (recipient, typed value) pair. #### Global Justification @@ -35,16 +40,23 @@ #### Local Invariants 1. You must have spend authority over the note to spend + 2. You can't spend a positioned note twice. + 2.1. Each positioned note has exactly one valid nullifier for it. + 2.2. No two spends on the ledger, even in the same transaction, can have the same nullifier. + 3. You can't spend a note that has not been created, unless the amount of that note is 0. #### Local Justification 1. We verify the auth_sig using the randomized verification key, which must not be 0, provided on the spend body, even if the amount of the note is 0. A note's transmission key binds the authority. + 2.1. A note's transmission key binds to the nullifier key, and all components of a positioned note, along with this key are hashed to derive the nullifier, in circuit. + 2.2. This is in check_stateful, and an external check about the integrity of each transaction. + 3. The circuit verifies for non-zero amounts that there is a valid Merkle authentication path to the note in the global state commitment tree. #### Global Justification @@ -58,21 +70,32 @@ Privacy note: Value of staked note used for voting is revealed during a delegator vote. 1. Available voting power for a proposal = total delegated stake to active validators when the proposal was created + 1.1 Voting power must have been present before the proposal was created. + 1.2 You can't vote with a note that was spent prior to proposal start. + 1.3 That staked note must correspond to a validator that was in the active set when the proposal being voted on was created. + 2. You can't use the same voting power twice on a proposal. + 3. You can't vote on a proposal that is not votable, i.e. it has not been withdrawn or voting has finished. + 4. All invariants with regards to spending a note apply to voting with it. #### Local Justification 1.1 The circuit checks the age of the staked note, and the stateful check verifies that the claimed position matches that of the proposal. + 1.2 We check that the note was spent only after the block of the proposal. + 1.3 The stateful check for the exchange rate makes sure the validator was active at that time. + 2. We maintain a nullifier set for delegator votes and check for duplicate nullifiers in the stateful checks. + 3. The stateful check looks up the proposal ID and ensures it is votable. + 4. c.f. justification for spend circuit ### Swap @@ -96,21 +119,31 @@ proposal being voted on was created. #### Local Invariants 1. You cannot mint swap outputs to a different address than what was specified during the initial swap. + 2. You cannot mint swap outputs to different assets than those specified in the original swap. + 3. You cannot mint swap outputs to different amounts than those specified by the batch swap output data. + 3.1. You can only claim your contribution to the batch swap outputs. + 3.2 You can only claim the outputs using the batch swap output data for the block in which the swap was executed. + 4. You can only claim swap outputs for swaps that occurred. + 5. You can only claim swap outputs once. + 5.1. Each positioned swap has exactly one valid nullifier for it. + 5.2. No two swaps can have the same nullifier. #### Local Justification 1. The Swap commits to the claim address. The SwapClaim circuit enforces that the same address used to derive the swap commitment is that used to derive the note commitments for the two output notes. + 2. The SwapClaim circuit checks that the trading pair on the original Swap is the same as that on the batch swap output data. 3.1 The output amounts of each note is checked in-circuit to be only due to that user's contribution of the batch swap output data. + 3.2 The circuit checks the block height of the swap matches that of the batch swap output data. The ActionHandler for the SwapClaim checks that the batch swap output data provided by the SwapClaim matches that saved on-chain for that output height and trading pair. 4. The SwapClaim circuit verifies that there is a valid Merkle authentication path to the swap in the global state commitment tree. From 01c4be740760015fcea79f5c18a0c3c799023e8b Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Wed, 13 Mar 2024 15:15:24 -0400 Subject: [PATCH 7/8] spec: move output, spend invariants to shielded pool section --- .../src/shielded_pool/action/output.md | 24 ++++++++++ .../src/shielded_pool/action/spend.md | 44 ++++++++++++++--- docs/protocol/src/transactions/invariants.md | 48 +------------------ 3 files changed, 63 insertions(+), 53 deletions(-) diff --git a/docs/protocol/src/shielded_pool/action/output.md b/docs/protocol/src/shielded_pool/action/output.md index 604ca89c0c..86104dced0 100644 --- a/docs/protocol/src/shielded_pool/action/output.md +++ b/docs/protocol/src/shielded_pool/action/output.md @@ -2,6 +2,30 @@ Each output contains an OutputBody and a zk-SNARK output proof. +## Invariants + +The invariants that the Output upholds are described below. + +#### Local Invariants + +1. The created output note is spendable by the recipient if its nullifier has not been revealed. + +1.1 The output note is bound to the recipient. + +1.2 The output note can be spent only by the recipient. + +#### Local Justification + +1.1 The note commitment binds the note to the typed value and the address of the recipient. + +1.2 Each note has a unique note commitment if the note blinding factor is unique for duplicate (recipient, typed value) pairs. Duplicate note commitments are allowed on chain since they commit to the same (recipient, typed value) pair. + +#### Global Justification + +1.1 This action contributes the value of the output note, which is summed as part of the transaction value balance. Value is not created due to [system level invariant 1](../../transactions/invariants.md), which ensures that transactions contribute a 0 value balance. + +## Note Decryption Checks + Clients using the ephemeral public key $epk$ provided in an output body to decrypt a note payload MUST check: $epk = [esk] B_d$ diff --git a/docs/protocol/src/shielded_pool/action/spend.md b/docs/protocol/src/shielded_pool/action/spend.md index 0e0145a3bd..499d8e8941 100644 --- a/docs/protocol/src/shielded_pool/action/spend.md +++ b/docs/protocol/src/shielded_pool/action/spend.md @@ -2,6 +2,38 @@ Each spend contains an SpendBody and a zk-SNARK spend proof. +## Invariants + +The invariants that the Spend upholds are described below. + +#### Local Invariants + +1. You must have spend authority over the note to spend + +2. You can't spend a positioned note twice. + + 2.1. Each positioned note has exactly one valid nullifier for it. + + 2.2. No two spends on the ledger, even in the same transaction, can have the same nullifier. + +3. You can't spend a note that has not been created, unless the amount of that note is 0. + +#### Local Justification + +1. We verify the auth_sig using the randomized verification key, which must not be 0, provided on the spend body, even if the amount of the note is 0. A note's transmission key binds the authority. + +2. The following checks prevent spending a positioned note twice: + + 2.1. A note's transmission key binds to the nullifier key in circuit as described in the [Diversified Address Integrity](#diversified-address-integrity) section, and all components of a positioned note, along with this key are hashed to derive the nullifier in circuit as described below in the [Nullifier Integrity](#nullifier-integrity) section. + + 2.2. This is in the `ActionHandler` implementation on `check_stateful`, and an external check about the integrity of each transaction. + +3. The circuit verifies for non-zero amounts that there is a valid [Merkle authentication path](#merkle-auth-path-verification) to the note in the global state commitment tree. + +#### Global Justification + +1.1. This action destroys the value of the note spent, and is reflected in the balance by adding the value to the transaction value balance. Value is not created due to [system level invariant 1](../../transactions/invariants.md), which ensures that transactions contribute a 0 value balance. We do not create value, because of 3. + ## Spend zk-SNARK Statements The spend proof demonstrates the properties enumerated below for the following private witnesses known by the prover: @@ -24,7 +56,7 @@ And the corresponding public inputs: * Nullifier $nf \isin F_q$ of the note to be spent * Randomized verification key $rk \isin \mathbb G$ -### Note Commitment Integrity +### [Note Commitment Integrity](#note-commitment-integrity) The zk-SNARK certifies that the note commitment $cm$ was derived as: @@ -42,7 +74,7 @@ $cv = [v] G_v + [\widetilde{v}] G_{\widetilde{v}}$ where $G_{\widetilde{v}}$ is a constant generator and $G_v$ is an asset-specific generator point derived in-circuit as described in [Value Commitments](../../protocol/value_commitments.md). -### Nullifier Integrity +### [Nullifier Integrity](#nullifier-integrity) The zk-SNARK certifies that the revealed nullifier $nf$ was derived as: @@ -54,7 +86,7 @@ using the witnessed values above and where `ds` is a constant domain separator: as described in [Nullifiers](../notes/nullifiers.md). -### Diversified address Integrity +### [Diversified address Integrity](#diversified-address-integrity) The zk-SNARK certifies that the diversified address $pk_d$ associated with the note being spent was derived as: @@ -74,9 +106,9 @@ $rk = ak + [\alpha]B_{SpendAuth}$ where $B_{SpendAuth}$ is the conventional `decaf377` basepoint as described in [The Decaf377 Group](../../crypto/decaf377.md). -### Merkle auth path verification +### [Merkle auth path verification](#merkle-auth-path-verification) -The zk-SNARK certifies that for non-zero values[^1] $v \ne 0$, the witnessed Merkle authentication path is a valid Merkle path to the provided public anchor. Only for notes with non-zero values $v \ne 0$, the note is unrooted from the state commitment tree to allow for these "dummy" spends to pass stateless verification. Dummy spends may be added for metadata resistance (e.g. to ensure there are two spends and two outputs in each transaction). +The zk-SNARK certifies that for non-zero values $v \ne 0$, the witnessed Merkle authentication path is a valid Merkle path to the provided public anchor. Only for notes with non-zero values $v \ne 0$, the note is unrooted from the state commitment tree to allow for these "dummy" spends to pass stateless verification. Dummy spends may be added for metadata resistance (e.g. to ensure there are two spends and two outputs in each transaction). ### Diversified Base is not Identity @@ -85,5 +117,3 @@ The zk-SNARK certifies that the diversified basepoint $B_d$ associated with the ### The spend authorization key is not Identity The zk-SNARK certifies that the spend authorization key $ak$ is not identity. - -[^1]: Note that [issue 2135](https://github.com/penumbra-zone/penumbra/issues/2135) tracks a bug where dummy spends fail to verify due to the merkle paths. diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md index e910a2ebba..b8e4ff139e 100644 --- a/docs/protocol/src/transactions/invariants.md +++ b/docs/protocol/src/transactions/invariants.md @@ -15,53 +15,9 @@ ## Action-Level -### Output +* [Output Invariants](../shielded_pool/action/output.md) -#### Local Invariants - -1. The created output note is spendable by the recipient if its nullifier has not been revealed. - -1.1 The output note is bound to the recipient. - -1.2 The output note can be spent only by the recipient. - -#### Local Justification - -1.1 The note commitment binds the note to the typed value and the address of the recipient. - -1.2 Each note has a unique note commitment if the note blinding factor is unique for duplicate (recipient, typed value) pairs. Duplicate note commitments are allowed on chain since they commit to the same (recipient, typed value) pair. - -#### Global Justification - -1.1 This action contributes the value of the output note, which is summed as part of the transaction value balance. Value is not created due to system level invariant 1, which ensures that transactions contribute a 0 value balance. - -### Spend - -#### Local Invariants - -1. You must have spend authority over the note to spend - -2. You can't spend a positioned note twice. - -2.1. Each positioned note has exactly one valid nullifier for it. - -2.2. No two spends on the ledger, even in the same transaction, can have the same nullifier. - -3. You can't spend a note that has not been created, unless the amount of that note is 0. - -#### Local Justification - -1. We verify the auth_sig using the randomized verification key, which must not be 0, provided on the spend body, even if the amount of the note is 0. A note's transmission key binds the authority. - -2.1. A note's transmission key binds to the nullifier key, and all components of a positioned note, along with this key are hashed to derive the nullifier, in circuit. - -2.2. This is in check_stateful, and an external check about the integrity of each transaction. - -3. The circuit verifies for non-zero amounts that there is a valid Merkle authentication path to the note in the global state commitment tree. - -#### Global Justification - -1.1. This action destroys the value of the note spent, and is reflected in the balance by adding the value to the transaction value balance. We do not create value, because of 3. +* [Spend Invariants](../shielded_pool/action/spend.md) ### Delegator Votes From 933a6f01f31f1afad2e53d328373a9a6b4f28151 Mon Sep 17 00:00:00 2001 From: redshiftzero Date: Wed, 13 Mar 2024 15:39:00 -0400 Subject: [PATCH 8/8] spec: move rest of invariants to their relevant sections --- docs/protocol/src/dex/action/swap.md | 22 +++- docs/protocol/src/dex/action/swap_claim.md | 62 ++++++++-- .../src/governance/action/delegator_vote.md | 43 ++++++- .../src/stake/action/undelegate_claim.md | 24 +++- docs/protocol/src/transactions/invariants.md | 111 +----------------- 5 files changed, 145 insertions(+), 117 deletions(-) diff --git a/docs/protocol/src/dex/action/swap.md b/docs/protocol/src/dex/action/swap.md index f9289416c3..36842c5720 100644 --- a/docs/protocol/src/dex/action/swap.md +++ b/docs/protocol/src/dex/action/swap.md @@ -2,6 +2,26 @@ Each swap contains a SwapBody and a zk-SNARK swap proof. +## Invariants + +The invariants that the Swap upholds are described below. + +#### Local Invariants + +1. The swap binds to the specific trading pair. + +2. The swap binds to a specific claim address. + +#### Local Justification + +1. The swap commitment includes as inputs the trading pair of the two assets, demonstrated in circuit by the [Swap Commitment Integrity](#swap-commitment-integrity) check. + +2. The swap commitment includes as inputs each component of the claim address, demonstrated in circuit by the [Swap Commitment Integrity](#swap-commitment-integrity) check. + +#### Global Justification + +1.1 This action consumes the value of the two input notes (one per asset) consumed and the value of the pre-paid fee to be used by the SwapClaim, and is reflected in the balance by subtracting the value from the transaction value balance. Value is not created due to [system level invariant 1](../../transactions/invariants.md), which ensures that transactions contribute a 0 value balance. + ## Swap zk-SNARK Statements The swap proof demonstrates the properties enumerated below for the private witnesses known by the prover: @@ -23,7 +43,7 @@ And the corresponding public inputs: * Fee commitment $cv_f \isin G$ to the value of the fee * Swap commitment $scm \isin \mathbb F_q$ -### Swap Commitment Integrity +### [Swap Commitment Integrity](#swap-commitment-integrity) The zk-SNARK certifies that the public input swap commitment $scm$ was derived as: diff --git a/docs/protocol/src/dex/action/swap_claim.md b/docs/protocol/src/dex/action/swap_claim.md index d3b4650a87..ef70aec4e8 100644 --- a/docs/protocol/src/dex/action/swap_claim.md +++ b/docs/protocol/src/dex/action/swap_claim.md @@ -2,6 +2,54 @@ Each swap claim contains a SwapClaimBody and a zk-SNARK swap claim proof. +## Invariants + +The invariants that the SwapClaim upholds are described below. + +#### Local Invariants + +1. You cannot mint swap outputs to a different address than what was specified during the initial swap. + +2. You cannot mint swap outputs to different assets than those specified in the original swap. + +3. You cannot mint swap outputs to different amounts than those specified by the batch swap output data. + + 3.1. You can only claim your contribution to the batch swap outputs. + + 3.2. You can only claim the outputs using the batch swap output data for the block in which the swap was executed. + +4. You can only claim swap outputs for swaps that occurred. + +5. You can only claim swap outputs once. + + 5.1. Each positioned swap has exactly one valid nullifier for it. + + 5.2. No two swaps can have the same nullifier. + +#### Local Justification + +1. The Swap commits to the claim address. The SwapClaim circuit enforces that the same address used to derive the swap commitment is that used to derive the note commitments for the two output notes via the [Swap Commitment Integrity](#swap-commitment-integrity) and [Output Note Commitment Integrity](#output-note-commitment-integrity) checks. + +2. The SwapClaim circuit checks that the trading pair on the original Swap is the same as that on the batch swap output data via the [Trading Pair Consistency Check](#trading-pair-consistency-check). + +3. You cannot mint outputs to different amounts via: + + 3.1. The output amounts of each note is checked in-circuit to be only due to that user's contribution of the batch swap output data via the [Output Amounts Integrity](#output-amounts-integrity) check. + + 3.2. The circuit checks the block height of the swap matches that of the batch swap output data via the [Height Consistency Check](#height-consistency-check). The `ActionHandler` for the SwapClaim checks that the batch swap output data provided by the SwapClaim matches that saved on-chain for that output height and trading pair. + +4. The SwapClaim circuit verifies that there is a valid [Merkle authentication path](#merkle-auth-path-verification) to the swap in the global state commitment tree. + +5. You can only claim swap outputs once via: + + 5.1. A swap's transmission key binds to the nullifier key as described in the [Diversified Address Integrity](#diversified-address-integrity) section, and all components of a positioned swap, along with this key, are hashed to derive the nullifier, in circuit as described below in the [Nullifier Integrity](#nullifier-integrity) section. + + 5.2. In the `ActionHandler` for `check_stateful` we check that the nullifier is unspent. + +#### Global Justification + +1.1. This action mints the swap's output notes, and is reflected in the balance by adding the value from the transaction value balance. Value is not created due to [system level invariant 1](../../transactions/invariants.md), which ensures that transactions contribute a 0 value balance. + ## SwapClaim zk-SNARK Statements The swap claim proof demonstrates the properties enumerated below for the private witnesses known by the prover: @@ -36,7 +84,7 @@ And the corresponding public inputs: * Note commitment of the first output note $cm_1 \isin \mathbb F_q$ * Note commitment of the second output note $cm_2 \isin \mathbb F_q$ -### Swap Commitment Integrity +### [Swap Commitment Integrity](#swap-commitment-integrity) The zk-SNARK certifies that the witnessed swap commitment $scm$ was derived as: @@ -48,11 +96,11 @@ using the above witnessed values and where `ds` is a constant domain separator: `ds = from_le_bytes(BLAKE2b-512(b"penumbra.swap")) mod q` -### Merkle auth path verification +### [Merkle auth path verification](#merkle-auth-path-verification) The zk-SNARK certifies that the witnessed Merkle authentication path is a valid Merkle path of the swap commitment to the provided public anchor. -### Nullifier Integrity +### [Nullifier Integrity](#nullifier-integrity) The zk-SNARK certifies that the nullifier $nf$ was derived as: @@ -69,7 +117,7 @@ as described in [Nullifiers](../notes/nullifiers.md). The zk-SNARK certifies that the public claim fee is equal to the value witnessed as part of the swap plaintext. -### Height Consistency Check +### [Height Consistency Check](#height-consistency-check) The zk-SNARK certifies that the swap commitment's height is equal to the height of the batch swap output data (the clearing price height). @@ -81,7 +129,7 @@ $h = h_e + h_b$ where $h, h_e$ are provided on the batch swap output data as a public input. -### Trading Pair Consistency Check +### [Trading Pair Consistency Check](#trading-pair-consistency-check) The zk-SNARK certifies that the trading pair included in the swap plaintext corresponds to the trading pair included on the batch swap output data, i.e.: @@ -90,13 +138,13 @@ $ID_1 = ID_{pi1}$ $ID_2 = ID_{pi2}$ -### Output amounts integrity +### [Output Amounts Integrity](#output-amounts-integrity) The zk-SNARK certifies that the claimed output amounts $\Lambda_{1i}, \Lambda_{2i}$ were computed correctly following the pro-rata output calculation performed using the correct batch swap output data. -### Output Note Commitment Integrity +### [Output Note Commitment Integrity](#output-note-commitment-integrity) The zk-SNARK certifies that the note commitments $cm_1$ and $cm_2$ were derived as: diff --git a/docs/protocol/src/governance/action/delegator_vote.md b/docs/protocol/src/governance/action/delegator_vote.md index 3755b6d676..16e81cab1d 100644 --- a/docs/protocol/src/governance/action/delegator_vote.md +++ b/docs/protocol/src/governance/action/delegator_vote.md @@ -1,8 +1,47 @@ -# Delegator Vote Descriptions +# DelegatorVote Descriptions Each delegator vote contains an DelegatorVoteBody and a zk-SNARK delegator vote proof. -## Delegator Vote zk-SNARK Statements +## Invariants + +The invariants that the DelegatorVote upholds are described below. + +#### Local Invariants + +Privacy note: Value of staked note used for voting is revealed during a delegator vote. + +1. Available voting power for a proposal = total delegated stake to active validators when the proposal was created + + 1.1 Voting power must have been present before the proposal was created. + + 1.2 You can't vote with a note that was spent prior to proposal start. + + 1.3 That staked note must correspond to a validator that was in the active set when the +proposal being voted on was created. + +2. You can't use the same voting power twice on a proposal. + +3. You can't vote on a proposal that is not votable, i.e. it has not been withdrawn or voting has finished. + +4. All invariants with regards to spending a note apply to voting with it. + +#### Local Justification + +1. We check the available voting power for a proposal equals the total delegated stake to active validators when the proposal was created via: + + 1.1 The circuit checks the age of the staked note, and the stateful check verifies that the claimed position matches that of the proposal. + + 1.2 We check that the note was spent only after the block of the proposal. + + 1.3 The stateful check for the exchange rate makes sure the validator was active at that time. + +2. We maintain a nullifier set for delegator votes and check for duplicate nullifiers in the stateful checks. + +3. The stateful check looks up the proposal ID and ensures it is votable. + +4. c.f. justification for spend circuit [here](../../shielded_pool/action/spend.md) + +## DelegatorVote zk-SNARK Statements The delegator vote proof demonstrates the properties enumerated below for the following private witnesses known by the prover: diff --git a/docs/protocol/src/stake/action/undelegate_claim.md b/docs/protocol/src/stake/action/undelegate_claim.md index 38dfa7a37e..d5669358d0 100644 --- a/docs/protocol/src/stake/action/undelegate_claim.md +++ b/docs/protocol/src/stake/action/undelegate_claim.md @@ -1,6 +1,28 @@ # Undelegate Claim Descriptions -Each undelegate claim contains a UndelegateClaimBody and a zk-SNARK undelegate claim proof. The undelegate claim proof is implemented as an instance of a generic convert circuit which converts a private amount of one input asset into a target asset, given a public conversion rate. +Each undelegate claim contains a UndelegateClaimBody and a zk-SNARK undelegate claim proof. + +# Invariants + +#### Local Invariants + +1. You cannot claim undelegations that have not finishing unbonding. + +2. Slashing penalties must be applied when unbonding. + +#### Local Justification + +1. In the `ActionHandler` for `check_stateful` we check that the undelegations have finished unbonding. + +2. The `ConvertCircuit` verifies that the conversion from the unbonding token to the staking token was done using the correct conversion rate calculated from the penalty. We check in the `ActionHandler` for `check_stateful` that the _correct_ penalty rate was used. + +#### Global Justification + +1.1. This action consumes the amount of the unbonding tokens and contributes the unbonded amount of the staking tokens to the transaction's value balance. Value is not created due to [system level invariant 1](../../transactions/invariants.md), which ensures that transactions contribute a 0 value balance. + +# zk-SNARK Statements + +The undelegate claim proof is implemented as an instance of a generic convert circuit which converts a private amount of one input asset into a target asset, given a public conversion rate. First we describe the convert circuit, and then the undelegate claim proof. diff --git a/docs/protocol/src/transactions/invariants.md b/docs/protocol/src/transactions/invariants.md index b8e4ff139e..b3a878f65a 100644 --- a/docs/protocol/src/transactions/invariants.md +++ b/docs/protocol/src/transactions/invariants.md @@ -5,7 +5,7 @@ 1. Value cannot be created or destroyed after genesis or via IBC. Value cannot be created by the DEX. -1.1. Each action may create or destroy value, but commits to this imbalance, which when summed over a transaction, will not violate this rule. + 1.1. Each action may create or destroy value, but commits to this imbalance, which when summed over a transaction, will not violate this rule. 2. Individual actions are bound to the transaction they belong to. @@ -19,111 +19,10 @@ * [Spend Invariants](../shielded_pool/action/spend.md) -### Delegator Votes +* [DelegatorVote Invariants](../governance/action/delegator_vote.md) -#### Local Invariants +* [Swap Invariants](../dex/action/swap.md) -Privacy note: Value of staked note used for voting is revealed during a delegator vote. +* [SwapClaim Invariants](../dex/action/swap_claim.md) -1. Available voting power for a proposal = total delegated stake to active validators when the proposal was created - -1.1 Voting power must have been present before the proposal was created. - -1.2 You can't vote with a note that was spent prior to proposal start. - -1.3 That staked note must correspond to a validator that was in the active set when the -proposal being voted on was created. - -2. You can't use the same voting power twice on a proposal. - -3. You can't vote on a proposal that is not votable, i.e. it has not been withdrawn or voting has finished. - -4. All invariants with regards to spending a note apply to voting with it. - -#### Local Justification - -1.1 The circuit checks the age of the staked note, and the stateful check verifies that the claimed position matches that of the proposal. - -1.2 We check that the note was spent only after the block of the proposal. - -1.3 The stateful check for the exchange rate makes sure the validator was active at that time. - -2. We maintain a nullifier set for delegator votes and check for duplicate nullifiers in the stateful checks. - -3. The stateful check looks up the proposal ID and ensures it is votable. - -4. c.f. justification for spend circuit - -### Swap - -#### Local Invariants - -1. The swap binds to the specific trading pair. -2. The swap binds to a specific claim address. - -#### Local Justification - -1. The swap commitment includes as inputs the trading pair of the two assets. -2. The swap commitment includes as inputs each component of the claim address. - -#### Global Justification - -1.1 This action consumes the value of the two input notes (one per asset) consumed and the value of the pre-paid fee to be used by the SwapClaim, and is reflected in the balance by subtracting the value from the transaction value balance. We do not create value, because of 3. - -### SwapClaim - -#### Local Invariants - -1. You cannot mint swap outputs to a different address than what was specified during the initial swap. - -2. You cannot mint swap outputs to different assets than those specified in the original swap. - -3. You cannot mint swap outputs to different amounts than those specified by the batch swap output data. - -3.1. You can only claim your contribution to the batch swap outputs. - -3.2 You can only claim the outputs using the batch swap output data for the block in which the swap was executed. - -4. You can only claim swap outputs for swaps that occurred. - -5. You can only claim swap outputs once. - -5.1. Each positioned swap has exactly one valid nullifier for it. - -5.2. No two swaps can have the same nullifier. - -#### Local Justification - -1. The Swap commits to the claim address. The SwapClaim circuit enforces that the same address used to derive the swap commitment is that used to derive the note commitments for the two output notes. - -2. The SwapClaim circuit checks that the trading pair on the original Swap is the same as that on the batch swap output data. - -3.1 The output amounts of each note is checked in-circuit to be only due to that user's contribution of the batch swap output data. - -3.2 The circuit checks the block height of the swap matches that of the batch swap output data. The ActionHandler for the SwapClaim checks that the batch swap output data provided by the SwapClaim matches that saved on-chain for that output height and trading pair. - -4. The SwapClaim circuit verifies that there is a valid Merkle authentication path to the swap in the global state commitment tree. - -5.1. A swap's transmission key binds to the nullifier key, and all components of a positioned swap, along with this key are hashed to derive the nullifier, in circuit. - -5.2. In the `ActionHandler` for `check_stateful` we check that the nullifier is unspent. - -#### Global Justification - -1.1 This action mints the swap's output notes, and is reflected in the balance by adding the value from the transaction value balance. We do not create value, because of 3. - -### UndelegateClaim - -#### Local Invariants - -1. You cannot claim undelegations that have not finishing unbonding. -2. Slashing penalties must be applied when unbonding. - -#### Local Justification - -1. In the `ActionHandler` for `check_stateful` we check that the undelegations have finished unbonding. -2. The `ConvertCircuit` verifies that the conversion from the unbonding token to the staking token was done using the correct conversion rate calculated from the penalty. We check in the `ActionHandler` for `check_stateful` that the _correct_ penalty was used. - -#### Global Justification - -1.1. This action consumes the amount of the unbonding tokens and contributes the unbonded amount of the staking tokens to the transaction's value balance. We do not create value, because of 3. +* [UndelegateClaim Invariants](../stake/action/undelegate_claim.md)