Overview
zkStark-aMACI is a Starknet implementation of the anonymous MACI protocol (aMACI). It expresses aMACI's protocol state transitions and cryptographic checks as Cairo programs, proves the correctness of those program executions with zkSTARK proofs, and lets Starknet contracts consume verified facts to advance the round state.
This document discusses two parts of the system:
- Circuit layer: what each Cairo program proves, how the public output binds state, and why the on-chain contract only needs to consume facts.
- aMACI round flow implementation: how one aMACI round runs from signup to tally, and what the voter, operator, and contract each do.
The current implementation is designed based on Starknet's native execution environment. Protocol state transitions and cryptographic relations are expressed as Cairo programs, and proofs are generated by a zkSTARK proving system. In the Atlantic flow, Atlantic generates and submits proofs, the Integrity verifier performs on-chain verification, and the aMACI contract consumes registered facts to advance the round state.
The privacy boundary should be stated upfront: in the aMACI protocol model, the Operator decrypts and processes messages, so the Operator can see plaintext votes. The privacy goal of the current implementation is mainly to prevent on-chain and public observers from learning plaintext votes, while using proofs to constrain accepted state transitions to follow the circuit rules. When Atlantic is used, the witness enters Atlantic's execution environment. If that is not acceptable in production, the system should switch to a self-hosted prover.
Part 1: Cairo Circuits and the Proving System
1. What "circuit" means here
A "circuit" is a Cairo program whose execution can be validated.

Each Cairo program takes a witness and public inputs, recomputes the relevant cryptographic relations, and finally emits public output. The proof attests that:
For a given Cairo program and public output, there exists a witness such that the program executes successfully and produces that public output.
2. Fixed parameters
The current full E2E flow uses the 2-1-1-3 parameter size:
3. Four groups of circuits
The verifiable execution of the current aMACI round is supported by four Cairo circuit groups:

These four circuit groups prove state transitions for different phases of the round, and together maintain three types of on-chain commitments:
- deactivateCommitment
- stateCommitment
- tallyCommitment
The on-chain contract does not see the witness and does not re-execute private computation. It only consumes verified facts and checks that the commitments in the proof's public output form a valid transition from the current on-chain state.
ProcessDeactivate circuit
processDeactivate proves that a batch of deactivation messages has been processed correctly according to the protocol rules. The current batch size is 3 deactivation messages.
For each message, the circuit verifies that:
- the ECDH shared key derived from the message public key and the coordinator private key is correct;
- the encrypted deactivate command is decrypted correctly;
- the STARK ECDSA signature over the command by the old
StateLeaf.pubKeyis valid; pollIdandstateIndexin the command are valid;- the old key is still active at the time of processing;
- updates to
ActiveStateTreeandDeactivateTreeare correct.
The public output of this circuit binds the new deactivateCommitment, which the contract uses to advance the deactivation phase state.
AddNewKey circuit
addNewKey proves that a user can register a new key using an old key that has already been deactivated.
It does not prove something like "a regular new user was added on-chain." Instead, it proves that all of the following relations hold:
The prover knows the private key of an old key that has been deactivated;
that old key has not already been used to rotate to a new key in the current poll;
the new public key is correctly bound to the deactivation credential of the old key,
but the public data cannot directly link the old key and the new key.
The circuit mainly checks that:
nullifier = H(oldPrivKey, pollId, domain), preventing the same old key from rotating more than once;- the shared key derived from the old private key and the coordinator public key corresponds to
deactivateSharedKeyHashinDeactivateTree; d1/d2is a valid rerandomization ofc1/c2;- the Merkle inclusion path for
DeactivateTreeis correct; - the new public key is bound to the public output.
The public output of this circuit binds the nullifier, the new public key, and the new stateCommitment, allowing the contract to complete new key registration.
ProcessMessages circuit
processMessages proves that a batch of vote messages has been processed correctly according to the protocol rules. The current batch size is 3 vote messages, processed in reverse order of the message queue.
For each message, the circuit verifies that:
- the ECDH shared key derived from the message public key and the coordinator private key is correct;
- the encrypted vote command is decrypted correctly;
- the STARK ECDSA signature over the command by the current
StateLeaf.pubKeyis valid; - the
StateLeafatstateIndexexists; - the current key has not been deactivated;
pollId,nonce, andvoteOptionIndexare valid;- updates to
VoteOptionTreeandStateTreeare correct.
Each vote command updates only one voteOptionIndex. If a message comes from an old key that has already been deactivated, it is treated as an invalid message and does not change the final voting state.
The public output of this circuit binds the new stateCommitment and the message hash chain boundaries, allowing the contract to advance vote message processing.
Tally circuit
tally proves that the final tally results are correctly accumulated from the StateTree after processMessages.
The Tally circuit verifies that:
stateCommitmentequals the finalprocessMessages.newStateCommitment;- each
StateLeaf.voteOptionRootmatches the input vote option array; - the current batch is correctly accumulated into
currentResults; newTallyCommitment = H(H(newResults), salt)is correct.
The public output of this circuit binds the new tallyCommitment. Plaintext results are not stored on-chain; only tallyCommitment is stored. The Operator can publish the raw results and salt, and anyone can verify whether they match the on-chain commitment.
Part 2: aMACI Round Flow Implementation
1. Core state objects
2. E2E round lifecycle

1. Signup
The user registers an initial public key, and the contract inserts the corresponding StateLeaf into StateTree.
Signup only establishes the initial identity. At this point, the user has not yet obtained a new unlinkable key through deactivate / addNewKey.
2. Deactivate
The old key sends an encrypted deactivation message. The message contains a deactivate command and is signed by the old key.
This phase is performed by the voter:
Voter:
Generate deactivate command
Encrypt command with an ephemeral message key
Sign command with old key
Publish deactivation message
3. ProcessDeactivate
The Operator collects deactivation messages, constructs the witness, and submits a processDeactivate proof generation task.
This phase is performed by the Operator:
Operator:
Decrypt deactivation message
Check signature and state
Update ActiveStateTree
Write into DeactivateTree
Generate proof input
Submit to Atlantic
After Integrity verifies the proof and registers the fact, the aMACI contract consumes that fact and advances deactivateCommitment.
4. AddNewKey
The user registers a new key using the deactivation credential of the old key.
This phase is performed by the voter:
Voter:
Use oldPrivKey to prove ownership of a corresponding deactivate leaf
Generate nullifier to prevent repeated key rotation
Rerandomize c1/c2 into d1/d2
Bind newPubKey
Generate addNewKey proof input
After Integrity verifies the proof and registers the fact, the aMACI contract consumes that fact:
consume nullifier
register newPubKey
keys_added += 1
5. Vote
The currently valid key sends an encrypted vote command.
Key fields in the vote command:
Message encryption uses an ephemeral message public key. The Operator computes the ECDH shared key from the coordinator private key and the message public key, then decrypts the command.
6. ProcessMessages
The Operator collects vote messages, constructs the witness, and submits a processMessages proof generation task.
This phase updates StateTree:
Read StateLeaf[stateIndex]
Check active/deactivate status
Check command signature, pollId, and nonce
Update the user's VoteOptionTree
Derive the new voteOptionRoot
Write back StateLeaf
Update StateTree root
After Integrity verifies the proof and registers the fact, the aMACI contract consumes that fact and advances stateCommitment and the message batch counter.
7. Tally
The Operator reads each user's voteOptionRoot from the final StateTree, accumulates the results batch by batch, and submits tally proof generation tasks.
After Integrity verifies the proof and registers the fact, the aMACI contract consumes that fact and advances tallyCommitment. The final raw results are not stored directly on-chain. The Operator can publish the raw results and salt, and anyone can verify:
H(H(results), salt) == tallyCommitment
This confirms whether the published results correspond to the on-chain commitment.
3. aMACI round proof flow and on-chain consumption
The four circuit groups, ProcessDeactivate, AddNewKey, ProcessMessages, and Tally, together with their respective witnesses and public inputs, are submitted to Atlantic according to the round phase. In this flow, Atlantic is responsible for proof generation and submission: it runs the corresponding Cairo program, generates the STARK proof for that phase, and submits the proof to the Integrity verifier contract.
The Integrity verifier contract performs on-chain proof verification. Once verification succeeds, the corresponding fact is registered in the FactRegistry. In the current Atlantic flow, the fact is bound to the metadata wrapper output; the aMACI contract then checks the application-level Cairo program hash and the application-level public output from that metadata output.
When handling an on-chain submission, the aMACI contract does not re-execute the circuit and does not read the witness. It only consumes a fact that has already been registered in the FactRegistry and satisfies the required security bits. It then uses the public output to check that the current commitment matches the on-chain state and that the next commitment can be written back, thereby advancing the deactivate, state, or tally state.

Summary
The current implementation uses Starknet-native cryptographic primitives and constrains aMACI's protocol state transitions and cryptographic checks inside Cairo programs:
- STARK ECDSA signatures;
- ECDH shared key;
- ElGamal-style decrypt / rerandomize;
- Poseidon stream decryption;
- nullifier;
- Merkle path;
- message hash chain;
- state / deactivate / tally commitment chain.
The current system has two security layers that should be kept separate:
Proving-system layer: zkSTARK proving system
Protocol-cryptography layer: STARK curve ECDSA / ECDH / ElGamal-style encryption
The zkSTARK proving system does not rely on elliptic-curve pairings and does not require a trusted setup. Its security mainly relies on hash functions and algebraic consistency checks, so the proving-system layer is generally considered to have a post-quantum-friendly security foundation.
However, the aMACI protocol itself still uses signatures, ECDH, and ElGamal-style encryption over the Starknet STARK curve. These rely on the elliptic-curve discrete logarithm assumption and are not secure against sufficiently powerful quantum attacks.
Therefore, in the current implementation, the zkSTARK proving system verifies aMACI's protocol state transitions and cryptographic checks:
- the proving-system layer has a post-quantum-friendly security foundation;
- the protocol's identity, signature, encryption, and key-agreement mechanisms still rely on non-post-quantum elliptic-curve cryptography and are not post-quantum secure.