# User State Transition Proof

The [user state transition](https://unirep.gitbook.io/unirep/protocol/glossary/user-state-transition) proof is used to process attestations from the latest epoch the user transitioned and then compute the latest [global state tree](https://unirep.gitbook.io/unirep/glossary/trees#global-state-tree) leaf.

The user state transition circuit checks that

1. The user has [registered](https://unirep.gitbook.io/unirep/protocol/glossary/users-and-attesters#user) and performed [user state transition](https://unirep.gitbook.io/unirep/protocol/glossary/user-state-transition) in the previous epoch.
2. The [user state tree](https://unirep.gitbook.io/unirep/glossary/trees#user-state-tree) is updated correctly by the attestations, and the same attestations are chained by hash functions.

   * For example, the original user state tree root is `r_1`, and the original user state tree leaf has 5 positive reputation

   ```
   user_state_tree_leaf = hash(5, 0, 0, 0, 0)
   ```

   * An incoming attestation has
     * `attester_id = 1`
     * `pos_rep = 3`
   * compute the hash of [reputation](https://unirep.gitbook.io/unirep/glossary/reputation#reputation)

   ```
   hash_reputation = hash(5 + 3, 0, 0, 0, 0)
   ```

   * compute the updated user state tree root `r_2` with user state tree leaf `hash(8, 0, 0, 0, 0)` in the leaf index `1`
   * compute the hash of [attestation](https://unirep.gitbook.io/unirep/glossary/reputation#attestation)

   ```
   hash_attestation = hash(1, 3, 0, 0, 0)
   ```

   * compute the hash chain

   ```
   hash_chain = hash(hash_attestation, hash_chain)
   ```
3. After all attestations of all epoch keys are processed, the circuit seals all hash chains and computes the [epoch tree](https://unirep.gitbook.io/unirep/glossary/trees#epoch-tree). (If the output epoch tree root mismatches others' epoch tree roots, then the user state transition proof is invalid because the user process attestations in a wrong way.)
4. Compute the updated global state tree leaf by

```typescript
hash(identity_commitment, updated_user_state_root)
```

Ideally, the user state transition proof should be in [one circuit](https://github.com/appliedzkp/UniRep/blob/5701dd3c060c332e8e83895c49e3a90b3fca3c49/circuits/userStateTransition.circom). But the circuit size is too big to generate a proof in a browser, we separate the proof into three different parts: **start transition proof**, **process attestations proof**, and **user state transition proof**.

The idea of chaining these three proofs but without revealing user's sensitive information is to use `blinded_user_state` and `blinded_hash_chain`

```typescript
const blinded_user_state = hash(
    identity_nullifier, 
    user_tree_root, 
    epoch, 
    from_epoch_key_nonce
)
const blinded_hash_chain = hash(
    identity_nullifier, 
    current_hash_chain, 
    epoch, 
    from_epoch_key_nonce
)
```

In the **start transition proof**, the circuit will compute the initial `blinded_user_state` and `blinded_hash_chain`, the `user_tree_root` is the latest transitioned user state tree and the `hash(identity_commitment, updated_user_state_root)` should be in a global state tree. The `current_hash_chain` is start with `0` as the definition of hash chain.

![How blinded user states and blinded hash chains are computed.](https://1939836936-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-Mb9Vp6gNlb57m_A4qKo%2Fuploads%2FoY9WGiK6LDTGMZEZOEhC%2F%E6%88%AA%E5%9C%96%202022-07-22%20%E4%B8%8B%E5%8D%881.27.59.png?alt=media\&token=27f74eb4-0f9f-4efb-9aea-915f2a354a8e)

After `blinded_user_state` and `blinded_hash_chain` are submitted, the user can take them as public inputs and start to **process attestations** according to the `user_tree_root` and `current_hash_chain`. When the attestations limit reaches (e.g. a `processAttestations` circuit can process only 10 attestations per proof) or all attestations to the epoch key are processed, the circuit will output another `blinded_user_state` and `blinded_hash_chain` to continue processing attestations.

![How hash chain is processed in process attestations proofs.](https://1939836936-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-Mb9Vp6gNlb57m_A4qKo%2Fuploads%2FxKPbDVFWpBlxiePhbBlv%2F%E6%88%AA%E5%9C%96%202022-07-23%20%E4%B8%8B%E5%8D%883.55.55.png?alt=media\&token=c48eeb82-7407-422f-9468-d7e2a187e17a)

![How user state tree is processed in process attestation proofs.](https://1939836936-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-Mb9Vp6gNlb57m_A4qKo%2Fuploads%2F5INo1XbdvuvzugRHkvJC%2F%E6%88%AA%E5%9C%96%202022-07-23%20%E4%B8%8B%E5%8D%884.06.07.png?alt=media\&token=5b0e903f-89f5-4175-a321-d995fe2f0a9e)

The `epoch_key_nonce` is used in the blinded user state and blinded hash chain to indicate the attestations of which epoch key is processed. In the final **`userStateTransition`** proof, it checks all epoch key with different `epoch_key_nonce` are processed and the hash chain result matches the [epoch tree](https://unirep.gitbook.io/unirep/glossary/trees#epoch-tree).

There are only one user state tree result after all attestations are processed, so in the final proof it only takes the initial `blinded_user_state` and the final one and computes the new global state tree leaf. On the other hand, there are `numEpochKeyNoncePerEpoch` hash chains after processing attestations, so the final circuit will take `numEpochKeyNoncePerEpoch` `blinded_hash_chain` to check the epoch tree root.

![How the final user state transition proof verifies hash chains and user states.](https://1939836936-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F-Mb9Vp6gNlb57m_A4qKo%2Fuploads%2FguuWN2vAUXmL7ZWhWDak%2F%E6%88%AA%E5%9C%96%202022-07-23%20%E4%B8%8B%E5%8D%8811.10.10.png?alt=media\&token=f247208a-60ca-4fb4-872c-969975c1db94)

The user state tree root is continuously updated: the output should be the input of another proof, so the `processAttestation` proof takes `blinded_user_state` as public input and output another `blinded_user_state`. The hash chain results might not be continuously. When all attestations of one epoch key is processed, the hash chain of the next epoch key should be `0` but not the previous hash chain. Therefore, `processAttestation` proof does not take `blinded_hash_chain` as input.

While verifying all of the proofs, there are the following things to check to make sure it follows the rules:

1. `startTransitionProof` takes a valid global state tree root as a public input.
2. `processAttestationsProof` takes `blinded_user_state` as public input and `blinded_hash_chain` as private input from either `startTransitionProof` or another `processAttestationsProof`.
3. `userStateTransitionProof` takes two `blinded_user_state`, one is from `startTransitionProof` and the other is from the latest `processAttestationsProof`.
4. `userStateTransitionProof` takes `numEpochKeyNoncePerEpoch` `blinded_hash_chain` from `processAttestationsProof`.

## 1. Start Transition proof

### Public inputs

* `GST_root`

### Public outputs

* `blinded_user_state`
* `blinded_hash_chain_result`

### Private inputs

* `epoch`
* `epoch_key_nonce`
* `user_tree_root`
* `identity_nullifier`
* `identity_trapdoor`
* `GST_path_elements`
* `GST_path_index`

### Contraints

#### 1. Check if user exists in the Global State Tree

Check if `hash(identity_commitment, UST_root)` is one of the leaves in the global state tree of root `GST_root`.

#### 2. Compute blinded public output

```typescript
const blinded_user_state = hash(
    identity_nullifier, 
    user_tree_root, 
    epoch, 
    from_epoch_key_nonce
)
const blinded_hash_chain = hash(
    identity_nullifier, 
    current_hash_chain, 
    epoch, 
    from_epoch_key_nonce
)
```

{% hint style="info" %}
See the whole circuit in [circuits/startTransition.circom](https://github.com/Unirep/Unirep/blob/main/packages/circuits/circuits/startTransition.circom)
{% endhint %}

## 2. Process attestations proof

### Public inputs

* `input_blinded_user_state`

### Public outputs

* `blinded_user_state`
* `blinded_hash_chain_result`

### Private inputs

* `epoch`
* `from_nonce`
* `to_nonce`
* `identity_nullifier`
* `intermediate_user_state_tree_roots`
* `old_pos_reps`
* `old_neg_reps`
* `old_graffities`
* `old_sign_ups`
* `path_elements`
* `attester_ids`
* `pos_reps`
* `neg_reps`
* `graffities`
* `overwrite_graffities`
* `sign_ups`
* `selectors`
* `hash_chain_starter`

### Contraints

#### 1. Verify blinded input user state

Check if

```typescript
const input_blinded_user_state = hash(
    identity_nullifier, 
    intermediate_user_state_tree_roots[0], 
    epoch, 
    from_nonce
)
```

#### 2. Verify attestation hash chain

Check if

```typescript
const current_hash_chain = hash(
    hash(
        attester_ids[i]
        pos_reps[i],
        neg_reps[i],
        graffities[i],
        sign_ups[i]
    ),
    prev_hash_chain
)
```

#### 3. Process attestations and update user state tree

Check `intermediate_user_state_tree_roots[i]` has leaves

```typescript
hash(
    old_pos_reps[i],
    old_neg_reps[i],
    old_graffities[i],
    old_sign_ups[i]
)
```

with index `attester_ids`.

And update the leaf by

```typescript
new_pos_reps[i] = pos_reps[i] + old_pos_reps[i]
new_neg_reps[i] = neg_reps[i] + old_neg_reps[i]
if (overwrite_graffities[i]) {
    new_graffities[i] = graffities[i]
} else {
    new_graffities[i] = old_graffities[i]
}
    
new_sign_ups[i] = sign_ups[i] || old_sign_ups[i]
```

And the new leaf

```typescript
hash(
    new_pos_reps[i],
    new_neg_reps[i],
    new_graffities[i],
    new_sign_ups[i]
)
```

Should be one of the leaves in `intermediate_user_state_tree_roots[i+1]` with index `attester_ids[i]`.

#### 4. Compute blinded public output

```typescript
const output_blinded_user_state = hash(
    identity_nullifier, 
    intermediate_user_state_tree_roots[n+1], 
    epoch, 
    to_nonce
)
const output_blinded_hash_chain = hash(
    identity_nullifier, 
    current_hash_chain, 
    epoch, 
    to_nonce
)
```

{% hint style="info" %}
See the whole circuit in [circuits/processAttestations.circom](https://github.com/Unirep/Unirep/blob/main/packages/circuits/circuits/processAttestations.circom)
{% endhint %}

## 3. User State Transition proof

### Public inputs

* `epoch`
* `GST_root`
* `blinded_hash_chain_results`
* `epoch_tree_root`

### Public outputs

* `new_GST_leaf`
* `epoch_key_nullifier`

### Private inputs

* `blinded_user_state`
* `intermediate_user_state_tree_roots`
* `start_epoch_key_nonce`
* `end_epoch_key_nonce`
* `identity_nullifier`
* `identity_trapdoor`
* `GST_path_elements`
* `GST_path_index`
* `epk_path_elements`
* `hash_chain_results`

### Contraints

#### 1. Check if user exists in the Global State Tree

Check if `hash(identity_commitment, UST_root)` is one of the leaves in the global state tree of root `GST_root`.

#### 2. Process the hashchain of the epoch key specified by nonce `n`

Get all blinded hash chains with nonce iterates from `0` to `n-1`

```typescript
const output_blinded_hash_chain = hash(
    identity_nullifier, 
    hash_chains[i], 
    epoch, 
    i
)
```

Seal all hash chains

```typescript
const sealed_hash_chain = hash(1, hash_chains[i])
```

Check the epoch tree root with `epoch_keys[i]` and `hash_chains[i]`.

#### 3. Check if blinded user state matches

Output two blinded user states with `start_epoch_key_nonce` and `end_epoch_key_nonce`.

```typescript
const output_blinded_user_state[0] = hash(
    identity_nullifier, 
    intermediate_user_state_tree_roots[0], 
    epoch, 
    start_epoch_key_nonce
)
const output_blinded_user_state[1] = hash(
    identity_nullifier, 
    intermediate_user_state_tree_roots[1], 
    epoch, 
    end_epoch_key_nonce
)
```

#### 4. Compute and output nullifiers and new GST leaf

```typescript
const new_GST_leaf = hash(
    id_commitment, 
    intermediate_user_state_tree_roots[1]
)
```

{% hint style="info" %}
See the whole circuit in [circuits/userStateTransition.circom](https://github.com/Unirep/Unirep/blob/main/packages/circuits/circuits/userStateTransition.circom)
{% endhint %}