ZK Tic-Tac-Toe Model

This post extends the tic-tac-toe Petri net model with zero-knowledge proofs. Using gnark, we can cryptographically verify that a move is valid without revealing the player's strategy or the complete game state.

Try the interactive demo at pilot.pflow.xyz/zk-tic-tac-toe.

The Problem

In the basic tic-tac-toe model, all state is visible. Both players see:

• Current board position
• Whose turn it is
• All previous moves

But what if we want private strategy? Or verifiable computation where a third party confirms moves are legal without seeing the game? Zero-knowledge proofs make this possible.

What ZK Proves

A zero-knowledge proof for tic-tac-toe demonstrates:

1. Valid transition: The move corresponds to a legal Petri net transition
2. Correct preconditions: Required input places have tokens
3. Turn compliance: It's actually this player's turn
4. No tampering: The state hash matches the previous state

All without revealing:

• Which specific move was made
• The current board configuration
• The player's strategy

From Petri Net to Circuit

The gnark circuit encodes the Petri net's transition rules as arithmetic constraints:

// Simplified circuit structure
type MoveCircuit struct {
    // Public inputs
    PrevStateHash frontend.Variable `gnark:",public"`
    NewStateHash  frontend.Variable `gnark:",public"`
    PlayerTurn    frontend.Variable `gnark:",public"`

    // Private witness
    Position      frontend.Variable // Which cell (0-8)
    PrevMarking   [10]frontend.Variable // Previous token state
    NewMarking    [10]frontend.Variable // New token state
}

The circuit enforces:

1. Position ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8}
2. PrevMarking[Position] == 1 (cell was empty)
3. NewMarking[Position] == 0 (cell now claimed)
4. Turn token moved correctly
5. Hash(PrevMarking) == PrevStateHash
6. Hash(NewMarking) == NewStateHash

Circuit Constraints

Each Petri net rule becomes an R1CS constraint:

The total circuit has ~100 constraints for a single move verification.

Proof Generation

When a player makes a move:

1. Compute new marking (fire transition locally)
2. Hash the new state
3. Generate ZK proof with gnark
4. Send: (prev_hash, new_hash, player_turn, proof)

The verifier checks the proof without seeing the actual move:

1. Verify proof against public inputs
2. If valid: accept new_hash as canonical state
3. If invalid: reject (cheating detected)

Why ZK for Petri Nets?

Petri nets and ZK circuits share a key property: local verification. A transition fires based only on its input places, not global state. This maps directly to R1CS constraints.

Benefits of the combination:

Game Protocol

A complete ZK tic-tac-toe game works as:

Initial: state_hash = hash(empty_board)

Round n:
  1. Current player generates move locally
  2. Computes new_state_hash
  3. Generates ZK proof: (old_hash, new_hash, proof)
  4. Opponent verifies proof
  5. If valid: state_hash = new_hash
  6. Continue until win/draw detected

Win detection can be a separate ZK proof that demonstrates three-in-a-row without revealing the full board.

Performance

Gnark proof generation for a single move:

The bottleneck is proof generation, but 100ms is acceptable for turn-based games.

Applications Beyond Games

The Petri net + ZK pattern applies to:

• Voting systems: Prove valid vote without revealing choice
• Supply chains: Verify state transitions without exposing inventory
• Access control: Prove permission without revealing identity
• Financial audits: Verify transactions without exposing amounts

Any system modeled as a Petri net can gain privacy through ZK circuits.

Model Structure

The ZK version adds cryptographic machinery to the base model:

Standard Petri Net:
  Places: P00-P22 (cells), Next (turn), _X*, _O* (history)
  Transitions: X00-X22, O00-O22

ZK Extension:
  Circuit: MoveCircuit (gnark R1CS)
  Public: state_hash, player_turn
  Private: position, prev_marking, new_marking

Proof System: Groth16 (gnark default)

Key Concepts Demonstrated

Conclusion

Zero-knowledge proofs extend Petri nets from verifiable to privately verifiable. The same structural properties that make Petri nets analyzable—locality, composability, determinism—make them natural targets for ZK circuits.

The combination enables a new class of applications: systems where we can prove correct behavior without revealing what that behavior was. The Petri net provides the model; the ZK circuit provides the privacy.

For the base tic-tac-toe model: Tic-Tac-Toe Model

For gnark documentation: gnark.io