> ## Documentation Index
> Fetch the complete documentation index at: https://docs.useabyss.com/llms.txt
> Use this file to discover all available pages before exploring further.

> Details how the ZK circuit is constructed to prevent forgery, inflation, and correlation, and why invalid state transitions are cryptographically impossible.

# Circuit Constraints and Soundness

The security of Abyss does not rely on application logic alone. It relies on the **soundness of the zero-knowledge circuit**. The circuit is the final arbiter of correctness. If a condition is not enforced inside the circuit, it is not enforced at all.

Abyss therefore treats the circuit as a formal specification of the protocol’s rules.

***

#### VII.2.1 Constraint Encoding Philosophy

All protocol invariants are encoded as **algebraic constraints** over a finite field. There are no implicit assumptions and no “off-circuit” checks relied upon for safety. This includes:

* Balance conservation
* Nullifier uniqueness
* Commitment membership
* Withdrawal bounds

If a prover cannot satisfy the constraints simultaneously, proof generation is computationally infeasible.

***

#### VII.2.2 Membership Constraints

Merkle inclusion is enforced inside the circuit by recomputing the root from the supplied path:

```
computed_root :=
  MerkleHash(leaf = commitment, path = merkle_path)

require(
  computed_root == merkle_root
)
```

This ensures the commitment existed in a valid pool state. The circuit does not assume a specific leaf index, preserving anonymity.

***

#### VII.2.3 Nullifier Correctness

Nullifiers are derived deterministically:

```
nullifier == H(secret_key || withdrawal_index)
```

This constraint guarantees that:

* Each withdrawal index maps to exactly one nullifier
* The prover cannot fabricate a nullifier unrelated to the secret
* Reuse of an index is detectable on-chain

Soundness here ensures **single-use authorization without identity**.

***

#### VII.2.4 Balance Conservation

The most critical constraint is balance conservation:

```
previous_withdrawals_sum + withdrawal_amount ≤ deposit_amount
```

This is enforced arithmetically inside the circuit. There is no on-chain balance to manipulate. The prover must supply a consistent internal accounting state that satisfies this inequality.

Any attempt to inflate balance or over-withdraw causes the circuit to fail.

***

#### VII.2.5 Non-Malleability and Binding

Commitments are binding by construction. Given:

```
commitment = H(secret_key || deposit_nonce || deposit_amount)
```

The prover cannot:

* Change the deposit amount
* Substitute a different secret
* Rebind the commitment to a new value

Collision resistance of `H` is a required assumption.

***

#### VII.2.6 Soundness Guarantees

Under standard ZK-SNARK assumptions:

* Forging a withdrawal without a valid deposit is infeasible
* Withdrawing more than deposited is infeasible
* Spending the same authorization twice is infeasible

These guarantees hold even if the adversary controls transaction ordering, mempool visibility, or attempts adaptive attacks.

***

#### VII.2.7 Failure Modes

The only failure modes are:

* Invalid witness data
* Stale Merkle root
* Reused nullifier

All failures result in proof verification failure and transaction revert. There is no partial execution state.

***