← Back to Petri-Pilot

Zero-Knowledge Proofs for Petri Nets

How gnark circuits prove that a state transition is valid — without revealing the state itself.

The Problem

When a Petri net fires a transition, the marking (token counts for every place) changes. In a multiplayer game or a blockchain, you want to prove that the transition was legal — that the input places had enough tokens and the output places received the right amount — without revealing the full game state to everyone.

This is exactly what zero-knowledge proofs (ZK proofs) do: they let a prover convince a verifier that a statement is true, without revealing why it's true.

What Gets Proven

Every ZK proof in this system proves one statement:

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

More precisely, the proof demonstrates:

  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 which transition fired. The actual token counts (the full game state) remain hidden.

Public inputs (verifier sees)

  • Pre-state root (hash)
  • Post-state root (hash)
  • Transition ID

Private inputs (prover knows)

  • Pre-marking (all token counts)
  • Post-marking (all token counts)

How It Works: The Circuit

A ZK proof is generated by an arithmetic circuit — a program built from additions and multiplications over a finite field. We use gnark, a Go library for writing these circuits.

The circuit for a Petri net transition has five steps:

1

Hash the pre-marking

Compute MiMC(pre[0], pre[1], ..., pre[N]) and assert it equals the public pre-state root. This binds the private marking to the public commitment.

2

Hash the post-marking

Same hash, same check. Now both states are committed.

3

Compute the delta

From the transition ID, look up the Petri net topology: which places lose tokens (inputs) and which gain tokens (outputs). Build a delta vector: delta[p] = outputs[p] - inputs[p].

4

Assert post = pre + delta

For every place, check that post[p] == pre[p] + delta[p]. This ensures the marking changed exactly as the topology dictates.

5

Assert enabledness

For every input place of the transition, check that pre[p] >= 1. This is done by decomposing pre[p] - 1 into bits — if the value were negative, it would wrap to a huge field element and the bit decomposition would fail.

In gnark code, the core constraint looks like this:

// For each transition in the topology... isThis := api.IsZero(api.Sub(c.Transition, t)) // Subtract from input places, add to output places deltas[p] = api.Sub(deltas[p], isThis) // inputs deltas[p] = api.Add(deltas[p], isThis) // outputs // Assert marking change matches topology expected := api.Add(c.PreMarking[p], deltas[p]) api.AssertIsEqual(c.PostMarking[p], expected)

Why MiMC?

The hash function MiMC (Minimal Multiplicative Complexity) is designed for ZK circuits. Unlike SHA-256 which needs thousands of boolean operations, MiMC is defined over the same finite field the circuit uses, making it extremely cheap in constraints.

Each state root is a MiMC hash of all token counts in the marking:

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

The verifier only sees the state root. To find the actual token counts, an attacker would need to invert the hash — computationally infeasible.

The Two Circuits

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

Transition Circuit

Proves a move is legal. The prover shows they know a valid marking where the transition fires and produces the next state. Used for every move.

Win Circuit

Proves a player has won. The win condition is already in the Petri net topology (win-detection transitions). The circuit just checks that the win_x or win_o place has a token.

Because the Petri net topology is the game rules, the ZK circuit doesn't need to know anything about tic-tac-toe specifically. It proves valid Petri net state transitions — the game logic lives in the net structure.

Key insight: The same circuit structure works for any Petri net. Change the topology constants and you get ZK proofs for a different game, workflow, or token standard — without writing a new circuit.

Beyond Games: Token Transfers

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

The gnark circuit proves the transfer is valid using a Merkle tree of account balances, so 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.

// TransferCircuit: prove balances[from] >= amount diff := api.Sub(c.BalanceFrom, c.Amount) api.ToBinary(diff, 64) // Fails if negative (insufficient balance) // Verify Merkle inclusion of balance in state tree leaf := MiMC(from, balanceFrom) // Walk 20-level Merkle proof to reach state root... api.AssertIsEqual(computedRoot, preStateRoot)

The Proof Pipeline

  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 using gnark
  4. Proof is returned as a compact byte string (~256 bytes) with public inputs
  5. Anyone can verify the proof in constant time using only the public inputs, without knowing the private marking
  6. On-chain verification is possible via an auto-generated Solidity verifier contract

Groth16 is the proving system used. It requires a one-time trusted setup per circuit but produces the smallest proofs (~128 bytes) and fastest verification. gnark handles the setup, proving, and Solidity export.

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 the state roots, verify the chain of proofs, and export Solidity calldata for on-chain verification.

Play ZK Tic-Tac-Toe →
← ODE Simulation & Prediction Thinking in Petri Nets →