Verifiable Computation from Petri Nets

How Scores Work

Base rates come from graph topology. Tactical adjustments are hand-tuned heuristics bolted on top. This is an ODE-derived heuristic, not game-theoretic optimality — tic-tac-toe was solved by minimax in the 1950s.

1. The board is a Petri net with 33 places and 35 transitions. Each cell has three places (empty, X, O) plus six control places for turns, wins, game state, and move counting.
2. Mass-action kinetics derive base rates from topology: rate = k * ∏ inputs. Rate constants are the number of win lines through each position — center k=4, corners k=3, edges k=2.
3. The base rates alone don't detect immediate wins or threats. Tactical patches are added: +10.0 for completing 3-in-a-row, −1.5 for leaving the opponent an unblocked threat. These are hand-tuned constants, not emergent properties.
4. What the ZK proof guarantees: the computation was performed correctly. Not that the strategy is optimal in the game-theoretic sense — only that the ODE + heuristic scores were computed honestly.

Building the Heatmap Circuit

A 176,891-constraint Groth16 circuit (gnark/BN254) that proves one ODE integration step + tactical scoring. The circuit is a direct translation of the Petri net topology — both are computational models, just at different abstraction levels.

Board Representation: 32 Places

The Petri net encodes the full game state as a marking vector:

Places 0-8:    P00..P22   empty cell tokens (1 = available, 0 = taken)
Places 9-17:   X00..X22   X pieces (1 = X placed here)
Places 18-26:  O00..O22   O pieces (1 = O placed here)
Place 27:      XTurn      (1 = X's turn)
Place 28:      OTurn      (1 = O's turn)
Places 29-30:  WinX, WinO (accumulators)
Place 31:      GameActive (1 = game in progress)

34 Transitions

18 play transitions (9 for X, 9 for O) plus 16 win-detection transitions (8 win patterns per player). Play transitions consume the empty-cell token and a turn token, producing a piece token and the opponent's turn:

X plays center: P11 + XTurn → X11 + OTurn    (k=4)
X plays corner: P00 + XTurn → X00 + OTurn    (k=3)
X plays edge:   P01 + XTurn → X01 + OTurn    (k=2)

Five Circuit Stages

The circuit verifies computation in five stages, all within a single Groth16 proof:

1. Pre-state root check: MiMC hash of the 32-element marking vector must match the public PreStateRoot.
2. Tsit5 ODE integration: A 7-stage Runge-Kutta method computes transition rates from the marking via mass-action kinetics, then integrates one step. Each rate is k * ∏(input tokens) computed with fixed-point multiplication at 10¹⁸ scale.
3. Post-state root check: MiMC hash of the post-integration marking must match PostStateRoot.
4. Tactical heatmap scoring: For each of the 9 cells, the circuit evaluates win detection (does placing here complete 3-in-a-row?) and block detection (does this leave the opponent an unblocked threat?), then computes the final score.
5. Score assertion: Each computed score must match the corresponding public HeatmapScores[i] input.

Tactical Scoring Formula

For each empty cell i:

win_flag[i]   = any win line completable by placing here?   (0 or 1)
block_flag[i] = opponent has unblocked threat after move?   (0 or 1)

score[i] = base_rate[i]
         + 10.0 * win_flag[i]
         -  1.5 * block_flag[i] * (1 - win_flag[i])
         *  cell_empty[i]           // zero out occupied cells

The +10.0 bonus dominates any base rate, so winning moves are always preferred. The −1.5 penalty only applies when a win isn't available, incentivizing defensive play. The (1 - win_flag) term ensures a simultaneous win-and-block still gets the full bonus.

Fixed-Point Arithmetic in ZK

All arithmetic uses 10¹⁸ fixed-point scaling over the BN254 scalar field (254-bit prime). Multiplication uses a gnark hint to compute quotient and remainder outside the circuit, then verifies a * b == q * SCALE + r with a range check on r inside the circuit. This avoids expensive in-circuit division while maintaining soundness.

Public Inputs (12 total)

 0  PreStateRoot    MiMC hash of board before ODE step
 1  PostStateRoot   MiMC hash of board after ODE step
 2  StepSize        ODE integration step (fixed-point)
3-11 HeatmapScores  Strategic score for each cell position

On-Chain Proof Chain

Each proof advances the contract's state root, enabling multi-move verification on Base Sepolia.

ZkOde.sol
  └ currentStateRoot: tracks the chain of board states
  └ stepCount: number of verified moves
  └ enforceOptimal: requires highest-scoring move

Architecture:
  ZkOde → IVerifier(Adapter) → Groth16Verifier (gnark BN254)
                                    177k constraints, 12 inputs

After each verified proof, currentStateRoot advances to the MiMC hash of the discrete post-move board (the piece actually placed), not the ODE post-state. This lets proofs chain across multiple moves — each proof's pre-state root must match the contract's current root.

Contract Enforcement

The contract checks that the submitted move has the highest ODE-derived score. "Optimal" here means "consistent with the heuristic" — not game-theoretically optimal.

// Enforce highest-scoring move per ODE heuristic
if (enforceOptimal) {
    uint256 chosenRate = publicInputs[3 + chosenTransition];
    for (uint256 t = 0; t < numTransitions; t++) {
        uint256 rate = publicInputs[3 + t];
        if (rate > chosenRate) {
            revert NotOptimalPlay(
                chosenTransition, chosenRate, t, rate
            );
        }
    }
}

The contract never re-runs the ODE or the heatmap evaluation. It trusts the Groth16 proof that the scores were computed correctly, then checks that the player picked the highest-scoring cell. The enforcement is sound relative to the heuristic — it guarantees consistency, not game-theoretic optimality. Verification costs ~275k gas regardless of circuit complexity.