Skip to main content
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.