Ceaser Protocol -- Smart Contracts

Privacy-preserving ETH/ERC20 wrapper on Base L2 using Noir/UltraHonk zero-knowledge proofs. This repository contains the audited smart contracts and formal verification suite.

Formal Verification

All smart contracts in this repository have been formally verified using the Certora Prover. Certora uses SMT solvers to mathematically prove that specified properties hold for all possible inputs and states -- not just tested cases.

79 rules verified across 7 specification files.

Specification	Rules	Properties	Report
zkWrapper	44	Fund conservation, nullifier uniqueness, fee correctness, access control, pause safety, input validation, who-changes-X access proofs	View
Merkle Tree	12	Root permanence, leaf index monotonicity, insert correctness, zero root safety	View
Rate Limiter	9	Per-block limits, per-address limits, exact increment accounting, constant validation	View
Denomination	6	Exact 6-value validation, biconditional completeness	View
Ghost Invariants	5	Sstore hook tracking, nullifier/root/leaf/flow sum invariants	View
Liveness	7	Reachability proofs (satisfy) for all core operations	View
Reentrancy	2	CALL opcode hook, nullifier integrity under external calls	View

Verification Methodology

The verification suite employs techniques used by leading DeFi protocols (Aave V3, Compound, OpenZeppelin):

• Parametric rules: Properties proven for all possible function selectors, not just specific functions
• Ghost variables with Sstore hooks: Track cumulative state transitions (nullifier spends, root additions, fund flow) across transactions
• Persistent ghosts: Survive external calls (recipient.call, fee transfers) without being havoced by the prover
• Delta-based sum invariants: Capture ghost values before each function call, assert on the delta to handle initial state setup
• Liveness proofs (satisfy): Prove operations CAN succeed -- guards against accidentally making operations unreachable
• CALL opcode hooks: Bytecode-level external call detection for reentrancy analysis
• Who-changes-X access proofs: Prove that only authorized functions can modify specific state variables
• Filtered parametric rules: Exclude view functions for performance and sanity compliance
• Definition blocks: Reusable boolean predicates for function classification

Scope

In scope (verified by Certora):

• Fund accounting: ETH/ERC20 amounts tracked correctly through shield/unshield
• Double-spend prevention: Nullifiers transition false-to-true and never revert
• Fee arithmetic: 0.25% split (0.24% treasury + 0.01% relayer) mathematically correct
• Merkle root permanence: Once valid, a root stays valid forever
• Rate limiting: Global per-block and per-address per-hour limits enforced
• Access control: Admin functions restricted to contract owner
• Pause mechanism: All state-changing operations blocked when paused
• State mutation boundaries: Only authorized functions modify each state variable

Out of scope (verified independently):

• ZK proof soundness (Noir/Aztec circuit tests)
• Poseidon hash collision resistance (cryptographic assumption)
• UltraHonk verifier correctness (Barretenberg)

Contract Architecture

contracts/solidity/
  core/
    zkWrapper.sol                    Main privacy contract (shield, unshield, transfer)
  components/
    MerkleTreeComponent.sol          24-level Poseidon Merkle tree
    RateLimiterComponent.sol         Per-address + global rate limiting
  libraries/
    DenominationLib.sol              Fixed denomination validation
    PoseidonT3.sol                   Poseidon hash (2 inputs)
    PoseidonT3Wrapper.sol            Wrapper for Merkle tree
    PoseidonT4.sol                   Poseidon hash (4 inputs)
    PoseidonT4Wrapper.sol            Wrapper for commitment computation
  interfaces/
    IPoseidon.sol                    Poseidon interface
    IVerifier.sol                    HonkVerifier interface
    IzkWrapper.sol                   Main contract interface
  verifiers/
    ShieldVerifier.sol               Auto-generated UltraHonk verifier
    TransferVerifier.sol             Auto-generated UltraHonk verifier
    BurnVerifier.sol                 Auto-generated UltraHonk verifier (unshield)

Key Parameters

Parameter	Value
Merkle tree depth	24 levels
Max capacity	16,777,216 notes
Protocol fee	0.25% (25 bps)
Treasury share	0.24% (24 bps)
Relayer share	0.01% (1 bps)
Valid denominations	0.001, 0.01, 0.1, 1, 10, 100 (ETH units)
Shield rate limit (per block)	1,000 ETH
Unshield rate limit (per block)	100 ETH
Per-address rate limit	50 ETH/hour (shield + unshield)
Solidity compiler	0.8.27 (optimizer: 1 run)

Running Verification

Prerequisites

• Docker
• Certora API key (free at certora.com)

Quick Start

# Build the verification container
docker build -t ceaser-certora certora/

# Run all 7 specification files
docker run --rm \
  -e CERTORAKEY="$CERTORAKEY" \
  -v $(pwd):/project \
  ceaser-certora

# Run a single specification
docker run --rm \
  -e CERTORAKEY="$CERTORAKEY" \
  -v $(pwd):/project \
  ceaser-certora confs/ghosts.conf

# Compile-only check (no API key needed)
docker run --rm \
  -v $(pwd):/project \
  --entrypoint certora-run \
  ceaser-certora --compilation_steps_only

Without Docker

pip install certora-cli solc-select
solc-select install 0.8.27 && solc-select use 0.8.27
npm install
export CERTORAKEY="your_key"
certoraRun certora/confs/zkWrapper.conf

See certora/README.md for detailed specification documentation.

License

MIT