Skip to content

Commit

Permalink
spec: move rest of invariants to their relevant sections
Browse files Browse the repository at this point in the history
  • Loading branch information
@redshiftzero @cronokirby
redshiftzero authored and cronokirby committed Mar 14, 2024
1 parent cd8b12b commit b0a8a66
Show file tree
Hide file tree
Showing 5 changed files with 145 additions and 117 deletions.
22 changes: 21 additions & 1 deletion docs/protocol/src/dex/action/swap.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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:

Expand Down
62 changes: 55 additions & 7 deletions docs/protocol/src/dex/action/swap_claim.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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:

Expand All @@ -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:

Expand All @@ -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).
Expand All @@ -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.:
Expand All @@ -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:

Expand Down
43 changes: 41 additions & 2 deletions docs/protocol/src/governance/action/delegator_vote.md
View file
Original file line number Diff line number Diff line change
@@ -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:

Expand Down
24 changes: 23 additions & 1 deletion docs/protocol/src/stake/action/undelegate_claim.md
View file
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
111 changes: 5 additions & 106 deletions docs/protocol/src/transactions/invariants.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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)

0 comments on commit b0a8a66

Please sign in to comment.