# Formal spec of circom-rln

## Utils

utils.circom is a set of templates/gadgets that the RLN circuit uses.

These are:

- MerkleTreeInclusionProof - Merkle tree inclusion check, used like set membership check;
- RangeCheck - used for range check.

Their description is given below.

### MerkleTreeInclusionProof

**MerkleTreeInclusionProof(DEPTH)** template used for verification of inclusion in full binary incremental merkle tree. The implementation is a fork of https://github.com/privacy-scaling-explorations/incrementalquintree, and changed to *binary* tree and refactored to *Circom 2.1.0*.

**Parameters**:

**DEPTH**- depth of the Merkle Tree.

**Inputs**:

- \(leaf\) - \(Poseidon(elem)\), where \(elem\) is the element that's checked for inclusion;
- \(pathIndex[DEPTH]\) - array of length = \(DEPTH\), consists of \(0 | 1\), represents Merkle proof path. Basically, it says how to calculate Poseidon hash, e.g. for two inputs \(input1\), \(input2\), if the \(pathIndex[i] = 0\) it shoud be calculated as \(Poseidon(input1, input2)\), otherwise \(Poseidon(input2, input1)\);
- \(pathElements[DEPTH]\) - array of length = \(DEPTH\), represents elements of the Merkle proof.

**Outputs**:

- \(root\) - Root of the merkle tree.

**Templates used**:

- mux1.circom from circomlib;
- poseidon.circom from circomlib.

### RangeCheck

**RangeCheck(LIMIT_BIT_SIZE)** template used for range check.

**Parameters**:

- \(LIMIT\_BIT\_SIZE\) - maximum bit size of numbers that are used in range check, f.e. for the \(LIMIT\_BIT\_SIZE = 16\), input numbers allowed to be in the interval \([0, 65536)\).

**Inputs**:

- \(messageId\) - denotes counter value, that'll be described further;
- \(limit\) - maximum value.

**Templates used**:

- LessThan(n) from circomlib;
- Num2Bits(n) from circomlib.

**Logic/Constraints**:
Checked that \(0 \le messageId < limit\).

## RLN

rln.circom is a template that's used for RLN protocol.

**Parameters**:

- \(DEPTH\) - depth of a Merkle Tree. Described here;
- \(LIMIT\_BIT\_SIZE\) - maximum bit size of numbers that are used in range check. Described here.

**Private inputs**:

- \(identitySecret\) - randomly generated number in \(\mathbb{F_p}\), used as a private key;
- \(userMessageLimit\) - message limit of the user;
- \(messageId\) - id of the message;
- \(pathElements[DEPTH]\) - pathElements[DEPTH], described here;
- \(identityPathIndex[DEPTH]\) - pathIndex[DEPTH], described here.

**Public inputs**:

- \(x\) - \(Hash(signal)\), where \(signal\) is for example message, that was sent by user;
- \(externalNullifier\) - \(Hash(epoch, rln_identifier)\).

**Outputs**:

- \(y\) - calculated first-degree linear polynomial \((y = kx + b)\);
- \(root\) - root of the Merkle Tree;
- \(nullifier\) - internal nullifier/pseudonym of the user in anonyomus environment.

**Logic/Constraints**:

- Merkle tree membership check:
- \(identityCommitment = Poseidon(identitySecret)\) calculation;
- \(rateCommitment = Poseidon(identityCommitment, userMessageLimit)\) calculation;
- Merkle tree inclusion check for the \(rateCommitment\).

- Range check:
- Range check that \(0 \le messageId < limit\).

- Polynomial share calculation:
- \(a_1 = Poseidon(identitySecret, externalNullifier, messageId)\);
- \(y = identitySecret + a_1 * x\).

- Output of calculated \(root\), \(y = share\) and \(nullifier = Poseidon(a_1)\) values.

### Withdrawal

withdraw.circom is a circuit that's used for the withdrawal/slashing and is needed to prevent frontrun while withdrawing the stake from the smart-contract/registry.

**Private inputs**:

- \(identitySecret\) - randomly generated number in \(\mathbb{F_p}\), used as private key.

**Public inputs**:

- \(address\) - \(\mathbb{F_p}\) scalar field element; denotes ETH address that'll receive stake.

**Outputs**:

- \(identityCommitment = Poseidon(identitySecret)\).