Zero-Knowledge Proofs for Petri Nets

The ZK Tic-Tac-Toe post showed how to add privacy to a game. This post goes deeper into the proof system itself: how any Petri net—not just tic-tac-toe—can be proven valid in zero knowledge.

The key insight: the circuit doesn't know anything about the application. It proves valid Petri net transitions. The game logic, workflow rules, or token transfer semantics live entirely in the net topology.

For an interactive introduction: Zero-Knowledge Proofs for Petri Nets

The Statement Being Proven

Every ZK proof in this system proves one statement:

"I know a valid marking that, when transition T fires, produces the claimed next state."

More precisely:

1. The pre-state root (a hash) matches a specific private marking
2. The post-state root matches a specific private marking
3. The chosen transition was enabled—all input places had sufficient tokens
4. The marking change is correct—post = pre + delta, where delta comes from the net topology

The verifier sees only the two state roots and the transition ID. The actual token counts remain hidden.

Public vs Private

The state roots are commitments. They bind the prover to a specific marking without revealing it.

The Circuit in Five Steps

The gnark circuit for a Petri net transition has five steps. Each step adds constraints that the prover must satisfy.

Step 1: Hash the Pre-Marking

Compute the MiMC hash of every place's token count and assert it equals the public pre-state root:

preRoot := petriMimcHash(api, c.PreMarking[:])
api.AssertIsEqual(preRoot, c.PreStateRoot)

This binds the private marking to the public commitment. The prover can't lie about what state they started from—the hash locks them in.

Step 2: Hash the Post-Marking

Same check for the post-state:

postRoot := petriMimcHash(api, c.PostMarking[:])
api.AssertIsEqual(postRoot, c.PostStateRoot)

Now both states are committed.

Step 3: Compute the Delta

From the transition ID, look up the Petri net topology to build a delta vector. For each transition in the net, conditionally apply its effect:

for t := 0; t < NumTransitions; t++ {
    isThis := api.IsZero(api.Sub(c.Transition, t))

    for _, p := range Topology[t].Inputs {
        deltas[p] = api.Sub(deltas[p], isThis)
    }
    for _, p := range Topology[t].Outputs {
        deltas[p] = api.Add(deltas[p], isThis)
    }
}

The isThis variable is 1 for the selected transition and 0 for all others. This multiplexes over all transitions without branching—arithmetic circuits can't branch, so we compute all possibilities and select.

Step 4: Assert Marking Change

For every place, check that the post-marking equals the pre-marking plus the delta:

for p := 0; p < NumPlaces; p++ {
    expected := api.Add(c.PreMarking[p], deltas[p])
    api.AssertIsEqual(c.PostMarking[p], expected)
}

This ensures the marking changed exactly as the topology dictates. No extra tokens appeared. No tokens vanished. The transition fired correctly.

Step 5: Assert Enabledness

For every input place of the selected transition, the pre-marking must have at least one token:

diff := api.Sub(c.PreMarking[p], isInput)
api.ToBinary(diff, 8)

The trick: ToBinary decomposes a value into bits. If the value were negative (insufficient tokens), it would wrap to a huge field element and the bit decomposition would fail—the proof can't be generated.

This is a standard gnark pattern for range checks: decompose into bits to prove non-negativity.

Why MiMC?

The hash function matters. SHA-256 needs thousands of boolean operations inside a circuit. MiMC (Minimal Multiplicative Complexity) is designed for arithmetic circuits—it's defined over the same finite field the circuit uses.

func petriMimcHash(api frontend.API, values []frontend.Variable) frontend.Variable {
    h, _ := mimc.NewMiMC(api)
    for _, v := range values {
        h.Write(v)
    }
    return h.Sum()
}

MiMC costs roughly 300 constraints per hash, compared to ~25,000 for SHA-256. For a circuit that hashes the marking twice (pre and post), this difference is significant.

The state root is:

stateRoot = MiMC(marking[0], marking[1], ..., marking[N])

To find the actual token counts from a state root, an attacker would need to invert MiMC—computationally infeasible.

Two Circuits for Tic-Tac-Toe

The ZK Tic-Tac-Toe implementation uses two circuits, both encoding the full 33-place Petri net:

PetriTransitionCircuit proves a move is legal. It's the general circuit described above—works for any transition in the net. Used for every move.

PetriWinCircuit proves a player has won. The win condition is already in the Petri net topology (win-detection transitions fire when three cells align). The circuit checks that the win_x or win_o place has a token:

func (c *PetriWinCircuit) Define(api frontend.API) error {
    root := petriMimcHash(api, c.Marking[:])
    api.AssertIsEqual(root, c.StateRoot)

    winTokens := frontend.Variable(0)
    for p := 0; p < NumPlaces; p++ {
        isWinnerPlace := api.IsZero(api.Sub(c.Winner, p))
        winTokens = api.Add(winTokens, api.Mul(c.Marking[p], isWinnerPlace))
    }
    api.ToBinary(api.Sub(winTokens, 1), 8) // >= 1 token
    return nil
}

Because the game logic lives in the net topology, the circuit doesn't know anything about tic-tac-toe. Change the topology constants and you get ZK proofs for a different game.

Beyond Games: Token Transfers

The arcnet project uses the same pattern for blockchain token transfers. An ERC-20 transfer is a Petri net transition:

• balances[from] is an input place (tokens consumed)
• balances[to] is an output place (tokens produced)
• The guard balances[from] >= amount is the enabledness check

The circuit proves the transfer is valid using a Merkle tree for account balances:

func (c *TransferCircuit) Define(api frontend.API) error {
    // Guard: balance >= amount
    diff := api.Sub(c.BalanceFrom, c.Amount)
    api.ToBinary(diff, 64)

    // Verify Merkle inclusion
    leaf := mimcHash(api, c.From, c.BalanceFrom)
    current := leaf
    for i := 0; i < 20; i++ {
        api.AssertIsBoolean(c.PathIndices[i])
        left := api.Select(c.PathIndices[i], c.PathElements[i], current)
        right := api.Select(c.PathIndices[i], current, c.PathElements[i])
        current = mimcHash(api, left, right)
    }
    api.AssertIsEqual(current, c.PreStateRoot)
    return nil
}

The 20-level Merkle proof means the full state doesn't need to live on-chain. Only state roots are published. The bridge contract verifies the proof and updates the root.

Same circuit structure. Different topology.

The Proof Pipeline

A complete proof cycle:

1. Player makes a move in the browser (fires a Petri net transition)
2. Frontend computes the new marking and MiMC state root client-side
3. Prover service receives the witness (pre/post markings + transition ID) and generates a Groth16 proof
4. Proof is returned as a compact byte string (~128 bytes) with public inputs
5. Anyone can verify the proof in constant time using only the public inputs
6. On-chain verification is possible via an auto-generated Solidity verifier contract

Why Groth16?

Groth16 is the proving system used by gnark. It requires a one-time trusted setup per circuit but produces:

• Smallest proofs: ~128 bytes (2 G1 points + 1 G2 point)
• Fastest verification: ~2ms, constant regardless of circuit size
• Solidity export: gnark generates a ready-to-deploy verifier contract

The trusted setup is performed once when the circuit is compiled. The resulting proving and verification keys are reused for every proof.

For our use case—small circuits with many proofs—Groth16's compact proofs and fast verification dominate.

Constraint Counts

The circuit size determines proving time. For the tic-tac-toe Petri net (33 places, 35 transitions):

Proof generation takes ~100ms on commodity hardware. Verification takes ~2ms. The circuit compiles once; proofs are generated per-move.

The Topology Is the Circuit

The most important property of this approach: the Petri net topology is baked into the circuit as constants. The Topology array maps each transition to its input and output places:

var Topology = [NumTransitions]struct {
    Inputs  []int
    Outputs []int
}{
    {Inputs: []int{0, 1}, Outputs: []int{2}},    // bind
    {Inputs: []int{2}, Outputs: []int{0, 1}},     // unbind
    {Inputs: []int{2}, Outputs: []int{3, 1}},     // catalyze
    // ...
}

This means:

1. No application-specific logic in the circuit. The same Define() method works for any net.
2. Topology changes require recompilation. Adding a place or transition means a new trusted setup.
3. The circuit is auditable. Anyone can inspect the topology to verify it matches the claimed rules.

The Petri net is the specification. The circuit is the verifier. The proof is the attestation that the specification was followed.

What ZK Doesn't Hide

A common misconception: ZK doesn't make the transition ID private. The verifier sees which transition fired. What's hidden is the state—the full marking of every place.

In tic-tac-toe, the opponent knows a move was made (transition X_center, say) but doesn't see the full board state. In a token transfer, the network knows a transfer happened but doesn't see individual balances.

For applications where even the transition must be hidden, an additional layer of indirection is needed—proving that some valid transition fired without revealing which one. This is possible but increases circuit complexity significantly.

Try It

Play the ZK Tic-Tac-Toe demo to see proofs generated in real time. Each move fires a Petri net transition, generates a gnark proof, and displays the proof structure. You can inspect state roots, verify the chain of proofs, and export Solidity calldata for on-chain verification.

For the interactive explainer: Zero-Knowledge Proofs for Petri Nets

Key Concepts

Conclusion

A Petri net is already a formal specification of valid state transitions. A ZK circuit turns that specification into a cryptographic proof system. The prover demonstrates they followed the rules; the verifier confirms it without seeing the state.

The circuit doesn't encode tic-tac-toe, or token transfers, or workflow rules. It encodes Petri net semantics: hash the marking, compute the delta from topology, assert the change, check enabledness. The application logic is in the net. The privacy is in the proof.

One circuit structure. Any Petri net. Provably correct, privately verified.

For gnark documentation: docs.gnark.consensys.io

For the base game model: Tic-Tac-Toe Model

For the arcnet bridge: github.com/pflow-xyz/arcnet