This post extends the tic-tac-toe Petri net model with zero-knowledge proofs. With gnark, a player proves that a move took one committed state to the next by a legal firing, and the verifier checks that proof against two hashes rather than against the board. What the proof hides is a good deal narrower than the first version of this post said; What the proof hides below says how much.
Prerequisite: the base model. For the proof system in general, read Zero-Knowledge Proofs for Petri Nets or Chapter 12 of the book.
The plain tic-tac-toe net runs on sim.pflow.xyz; the browser demo that proved each move has been retired. The circuits quoted below are from zk-tictactoe/ in the petri-pilot repository, which is not public. The Petri-net circuit is also what go-pflow's generator emits from a template (zkcompile/petrigen/templates.go), and proving goes through go-pflow's Groth16 wrapper (prover/prover.go), so the shape can be checked in public code even where the tic-tac-toe instance can't.
The code carries two versions of the move proof. MoveCircuit (circuits.go) works on the board — nine cells holding 0 for empty, 1 for X, 2 for O. PetriTransitionCircuit (petri_circuits.go) works on the full marking of a 33-place, 35-transition net: nine cell places p00–p22, nine x and nine o piece places, and x_turn, o_turn, win_x, win_o, can_reset, game_active. That net is a variant of the base post's model — two turn places instead of Next, and the piece places doing the job of the history places. Each move circuit has a matching win circuit.
The board circuit, as written in circuits.go:
type MoveCircuit struct {
// Public
PreStateRoot frontend.Variable `gnark:",public"`
PostStateRoot frontend.Variable `gnark:",public"`
Position frontend.Variable `gnark:",public"`
Player frontend.Variable `gnark:",public"`
// Private
Board [9]frontend.Variable
TurnCount frontend.Variable
}
Its Define checks, in order, that the MiMC hash of Board equals PreStateRoot; that the cell at Position is 0, found by a linear scan of nine IsZero selectors; that Player equals 1 plus the low bit of TurnCount; that the post-board is the pre-board with Player written at Position; and that the post-board hashes to PostStateRoot.
The Petri-net circuit has the same outline with the marking in place of the board: public PreStateRoot, PostStateRoot and Transition, private PreMarking and PostMarking over all 33 places. It hashes both markings, builds the selected transition's delta by multiplexing over all 35 transitions (isThis := api.IsZero(api.Sub(c.Transition, t))), asserts post[p] == pre[p] + delta[p] for every place, and proves enabledness by decomposing pre[p] − isInput into eight bits, which has no solution when an input place is empty. The five steps are walked through with the code in Zero-Knowledge Proofs for Petri Nets.
The two circuits differ in one place that matters. In MoveCircuit, TurnCount is a private input and is not part of the hashed board, so no constraint ties it to the committed state — a prover can pick whichever parity lets Player pass. TestMoveCircuit_WrongTurn fails because it hands the circuit an honest TurnCount of 1 with X moving; the same witness with TurnCount set to 0 would, as far as we can read the constraints, prove. We have not run that witness. A verifier that follows every public move can track the turn itself, but the circuit isn't doing it. In the Petri-net circuit the turn is a token in x_turn or o_turn, inside the hashed marking, and every x_play_* transition consumes x_turn, so a move out of turn fails the enabledness check like any other empty input. TestPetriTransitionCircuit_WrongTurn builds such a witness and asserts that proving fails. When the rule is in the marking the structure enforces it; when it sits beside the marking, the prover's good faith does.
Both circuits make the move public — Position and Player in one, the Transition index in the other — so the verifier learns which cell was taken on every turn. From the known empty board, anyone who sees every move can rebuild the board, so the private board or marking is private only from a verifier who has missed part of the transcript. The state root is also an unsalted MiMC hash, and tic-tac-toe has few reachable states, so a root can be matched by hashing candidate boards and comparing. What the proof does give is that each published root follows from the previous one by a legal move, checked without the verifier holding the board or re-running the rules — which is the property an on-chain verifier would need. Hiding the move itself would take a circuit that proves some enabled transition fired without naming it; nothing in the repository does that.
WinCircuit hashes the board against a public StateRoot and checks all eight lines for three cells equal to the public Winner, asserting that the count of matching lines is nonzero. PetriWinCircuit doesn't look at lines. Win detection is already in the net — each x_win_* or o_win_* transition consumes three piece tokens and game_active and puts a token in win_x or win_o — so the circuit only checks that the named win place holds a token and that the name is place 29 or 30. TestPetriTransitionCircuit_FullGameXWins plays X to a left-column win (cells 0, 1, 3, 4, 6, alternating) and asserts a proof for every move and for the x_win_col0 firing; TestPetriWinCircuit_NoWinnerFails asserts that a win claimed for X after two moves does not prove. These run on gnark's test prover in petri_circuits_test.go, and none of them was re-run for this revision.
No test records one. service.go logs the count when it compiles MoveCircuit and WinCircuit, but nothing keeps the number. An estimate can be read off the code: by Chapter 12's reading of gnark v0.14.0 (the version petri-pilot pins), BN254 MiMC costs 330 constraints per absorbed element — 110 rounds of x⁵ at three multiplications each. The two hashes alone are then 2 × 9 × 330 = 5,940 constraints for the board circuit and 2 × 33 × 330 = 21,780 for the Petri-net circuit, with the selectors and range checks on top. The first version of this post said a move took about 100 constraints, which is off by more than an order of magnitude for either circuit. Proving and verification times have not been benchmarked. The proof itself is Groth16 on BN254 — two G1 points and one G2 point, about 128 bytes compressed — and its verification cost depends on the number of public inputs, not on the size of the circuit.
The first version of this post argued that Petri nets suit circuits because both are local: a transition reads only its input places, a constraint only its witness variables. The circuit doesn't work that way. It multiplexes over every transition, range-checks every place and hashes the whole marking, so its cost grows with the size of the net, not with the arity of the move — the same thing we found in the arkworks circuit, which pads every step to the widest transition (Structuralism, Not Objects). What the net buys is genericity and enforcement. The game is the Topology constant in petri_state.go, and the same Define proves moves for any net whose arcs have weight 1 and which has no guards — go-pflow's generator adds a guard block when the model has one. And, as the turn check shows, a rule the net carries as a token is a rule the circuit enforces without anyone writing a constraint for it.
A game, sketched rather than copied from code:
Initial: root_0 = MiMC(initial marking)
Move n:
1. Mover fires a transition locally and computes the new marking
2. root_n = MiMC(new marking)
3. Groth16 proof over public (root_{n-1}, root_n, transition)
4. Opponent verifies the proof
5. If valid, accept root_n; otherwise reject the move
6. Once a win transition fires, a PetriWinCircuit proof shows the win place is marked
The same circuit shape with a balance guard proves a token transfer (Zero-Knowledge Proofs for Petri Nets), and ZK Polls proves voter eligibility over a small net. The other uses the first version of this post listed — supply chains, access control, financial audits — have no circuit behind them yet.
Revised 2026-11-13 against zk-tictactoe/ in petri-pilot (not public), go-pflow's zkcompile/petrigen and prover, and Chapter 12 of the book. Nothing was re-run.
MoveCircuit with a private Position and a ten-entry marking. No circuit in the code has that shape; the real MoveCircuit is quoted above, and the 33-place Petri-net circuit is described alongside it.prev_marking[pos] * 1 == 1 and so on) is not in the code, and "~100 constraints" understates the two hashes alone by more than fifty times.TurnCount is not committed, so its turn check binds only an honest prover. The Petri-net circuit enforces turns through the marking.Related: Tic-Tac-Toe Model · Zero-Knowledge Proofs for Petri Nets · ZK Hold'em · Bitwrap: Petri Nets as ZK Containers · gnark documentation