Topology-Driven Verification

Learning objective: Generate ZK proof circuits automatically from Petri net topology, and verify execution on-chain.

Chapter 12 built ZK circuits by hand — defining the PetriTransitionCircuit step by step, wiring up MiMC hashes and delta computations manually. That was instructive, but nobody should write ZK circuits by hand for every new model. This chapter closes the loop: given a Petri net JSON model, go-pflow’s petrigen package generates the gnark circuits, the witness generator and their tests, and the compiled circuit can then be exported as a Solidity verifier. The topology becomes constant arrays in the circuit, so changing the model and regenerating gives a new proof system.

Along the way, graph connectivity turns out to carry strategic value as well as circuit structure. Once the modeler says which transitions are moves and which are goals, rate constants for the ODE can be read off the bipartite graph, with no training data and no manual tuning, and counting win-line connections reproduces the classic tic-tac-toe heuristic (center > corner > edge). The derived rates are the constants of petri-pilot’s ZK ODE circuit.

The Compilation Pipeline

The full path from model to verifiable computation:

┌─────────────────┐     ┌─────────────────┐     ┌─────────────────┐
│   JSON Model    │────▶│    petrigen     │────▶│  gnark Circuit  │
│  (Petri net)    │     │   (generator)   │     │   (Go code)     │
└─────────────────┘     └─────────────────┘     └─────────────────┘
                                                        │
                                                        ▼
                                               ┌─────────────────┐
                                               │ Groth16/PLONK   │
                                               │    Prover       │
                                               └─────────────────┘
                                                        │
                                                        ▼
                                               ┌─────────────────┐
                                               │ Solidity        │
                                               │ Verifier        │
                                               └─────────────────┘

The petrigen package in go-pflow reads a Petri net model and generates four files:

The topology encoding — which places each transition consumes from and produces to — becomes compile-time constant arrays in the generated code, and the selector trick from Chapter 12 (evaluating all transitions and using IsZero to select one) is wired up automatically. The Solidity verifier is a separate step: SolidityExporter in zkcompile/solidity.go compiles a circuit, runs a Groth16 setup on BN254 and calls gnark’s ExportSolidity.

Two limits of the generator follow from that encoding (context.go). Each arc moves exactly one token: the arc’s weight is not read, so petrigen is only faithful on nets whose arcs all have weight 1. And a read or inhibitor arc moves no tokens, which two lists of decremented and incremented places cannot express, so petrigen refuses such a model with an error rather than prove a net that consumes from the tested place. Contextual arcs sit outside the incidence matrix; Appendix E gives the boundary they mark.

A Complete Example: Order Workflow

Consider a simple order processing workflow:

[pending] --approve--> [approved] --ship--> [shipped]
     |
     +----cancel----> [cancelled]

Define it as JSON:

{
  "name": "order-workflow",
  "places": [
    {"id": "pending", "initial": 1},
    {"id": "approved"},
    {"id": "shipped"},
    {"id": "cancelled"}
  ],
  "transitions": [
    {"id": "approve"},
    {"id": "ship"},
    {"id": "cancel"}
  ],
  "arcs": [
    {"from": "pending", "to": "approve"},
    {"from": "approve", "to": "approved"},
    {"from": "approved", "to": "ship"},
    {"from": "ship", "to": "shipped"},
    {"from": "pending", "to": "cancel"},
    {"from": "cancel", "to": "cancelled"}
  ]
}

Generate the circuits:

gen, _ := petrigen.New(petrigen.Options{
    PackageName:  "main",
    OutputDir:    ".",
    IncludeTests: true,
})

files, _ := gen.Generate(&model)
for _, f := range files {
    fmt.Println("Generated:", f.Name)
}

Output:

Generated: petri_state.go
Generated: petri_circuits.go
Generated: petri_game.go
Generated: petri_circuits_test.go

The generated petri_state.go encodes the topology as constants (an excerpt, laid out from the template in templates.go; the file also holds the place and transition names, the initial marking, IsEnabled, Fire and the MiMC marking root):

const NumPlaces = 4
const NumTransitions = 3

const (
    Pending   = 0
    Approved  = 1
    Shipped   = 2
    Cancelled = 3
)

const (
    Approve = 0
    Ship    = 1
    Cancel  = 2
)

var Topology = [NumTransitions]ArcDef{
    Approve: {Inputs: []int{0}, Outputs: []int{1}},
    Ship: {Inputs: []int{1}, Outputs: []int{2}},
    Cancel: {Inputs: []int{0}, Outputs: []int{3}},
}

This is the same pattern from Chapter 12, but generated automatically. The circuit’s Define() method iterates over Topology, computing deltas and enforcing the firing rule, and the developer does not edit circuit code.

go-pflow’s integration_test.go runs this pipeline end to end on the same workflow with a deliver step added (5 places, 4 transitions): it generates the four files, builds them, and runs the generated tests, which compile both circuits and check with gnark’s test harness that a proof succeeds for the first enabled transition. A second test does the same for a model with guards.

Proving a Transition

With the generated code, proving a valid state transition takes five steps. The listing below is a sketch against the generated API and gnark’s Groth16 backend, with errors ignored for brevity; the generated test performs the equivalent check through gnark’s test harness:

// 1. Compile the circuit
ccs, _ := frontend.Compile(ecc.BN254.ScalarField(),
    r1cs.NewBuilder, &PetriTransitionCircuit{})
fmt.Printf("Circuit has %d constraints\n", ccs.GetNbConstraints())

// 2. Trusted setup (one-time per circuit)
pk, vk, _ := groth16.Setup(ccs)

// 3. Fire a transition locally
game := NewPetriGame()
witness, _ := game.FireTransition(Approve)

// 4. Generate proof
assignment := witness.ToPetriTransitionAssignment()
w, _ := frontend.NewWitness(assignment, ecc.BN254.ScalarField())
proof, _ := groth16.Prove(ccs, pk, w)

// 5. Verify
publicWitness, _ := w.Public()
err := groth16.Verify(proof, vk, publicWitness)
// err == nil: proof valid

The verifier sees three public inputs — PreStateRoot, PostStateRoot, and Transition — and confirms the state changed correctly. The actual marking (which places have tokens) stays private.

We do not quote a constraint count or timings for this circuit: none of petrigen’s tests prints them, and the pipeline was not re-run for this chapter. Step 1 prints the count, which is dominated by the two MiMC hashes of the marking and so grows with the number of places. What does not depend on the run is the proof’s size: a Groth16 proof over BN254 is two G1 points and one G2 point, 128 bytes compressed, whatever the circuit, and verifying it costs a fixed number of pairings plus work proportional to the public inputs (three here).

Invalid Transitions Are Unprovable

What happens if someone tries to ship an order that hasn’t been approved?

game := NewPetriGame()  // Initial: pending=1
_, err := game.FireTransition(Ship)
// err: "transition ship failed: transition ship is not enabled"

The FireTransition function checks enabledness before generating a witness. But even if someone bypasses this check and constructs a malicious witness, the circuit’s bit decomposition will fail — PreMarking[Approved] is 0, and 0 - 1 wraps to a huge field element that can’t be decomposed into 8 bits, so no proof can be generated. Soundness comes from the circuit, not from the application code. Note what is tested: the generated TestPetriTransitionCircuit_InvalidTransition exercises only the application-level check, and the circuit-level claim follows from the enabledness constraint (api.ToBinary(diff, 8) in the template) rather than from a test that feeds the circuit a bad witness.

From Graph Connectivity to Rate Constants

Chapter 3 introduced mass-action kinetics with hand-tuned rate constants, and Chapter 6 ran the tic-tac-toe heatmaps with uniform rates. But where do rate constants come from?

For chemical reactions, rates encode physical properties — activation energies, temperature dependence, catalytic effects. You measure them in a lab. For games and workflows, there’s no lab. The rate constants encode strategic value, and that value can be derived from the graph itself.

The Algorithm

The rate auto-derivation algorithm operates on the bipartite directed graph of the Petri net:

1. Identify candidate transitions (the moves a player can make) and target transitions (the goals — win conditions, completion states)
2. For each candidate, find its unique output places — places it produces that no other candidate produces
3. Count how many target transitions take those unique places as inputs
4. That count is the rate constant

The implementation is deriveRatesFromTopology in petri-pilot’s ZK ODE code generator, zk-ode/codegen/context.go. Candidates and targets are given as globs over transition names (x_play_*, x_win_*), so the move/goal split is the modeler’s input, not something the graph decides. Two details of the code: a count of 0 or 1 leaves the default rate of 1, and a rate written explicitly in the model is kept rather than derived.

Tic-Tac-Toe: Strategy from Topology

The ZK variant of the TTT Petri net from Chapter 6 (the one Chapter 12 compiles; 33 places and 35 transitions, against Chapter 6’s 30 and 34) is the model used here, services/tic-tac-toe.json in petri-pilot. Each play transition (like x_play_11) produces a piece at a position (like x11). Each win transition (like x_win_diag) requires three specific pieces as inputs.

Apply the algorithm to the center position:

x_play_11 outputs → {x11, o_turn, move_tokens}

Unique outputs (only x_play_11 produces x11):
  x11

Win transitions with x11 as input:
  x_win_row1  (middle row)    ✓
  x_win_col1  (center column) ✓
  x_win_diag  (main diagonal) ✓
  x_win_anti  (anti-diagonal) ✓

Rate for x_play_11 = 4  (center: 4 win lines)

Compare with a corner:

x_play_00 outputs → {x00, o_turn, move_tokens}

Unique outputs: x00

Win transitions with x00 as input:
  x_win_row0  ✓
  x_win_col0  ✓
  x_win_diag  ✓

Rate for x_play_00 = 3  (corner: 3 win lines)

And an edge:

x_play_01 outputs → {x01, o_turn, move_tokens}

Unique outputs: x01

Win transitions with x01 as input:
  x_win_row0  ✓
  x_win_col1  ✓

Rate for x_play_01 = 2  (edge: 2 win lines)

Counting connections ranks center above corner above edge, the classic opening heuristic, without game-tree search or training data. The generator’s cross-validation test, zk-ode/codegen/crossvalidate_test.go, loads the JSON model with play transitions of both players as candidates and win transitions of both as targets, and checks that every derived rate equals the hand-coded table in zk-ode/ttt_topology.go (center 4, corners 3, edges 2); it was not re-run for this chapter.

Filtering Shared Places

The algorithm has one non-obvious step: filtering shared output places. Without it, every candidate gets the same rate.

Every x_play_* transition produces three output places: the piece (e.g., x00), the opponent’s turn token (o_turn), and a move counter (move_tokens). The piece place is unique to that candidate — only x_play_00 produces x00. But o_turn and move_tokens are produced by all 9 x-play transitions identically.

The problem: o_turn is an input to every x_win_* transition (win detection happens on the opponent’s turn). If you include o_turn in the connectivity count, every candidate connects to all 8 win targets through it, giving every position rate=8. The heatmap collapses to a flat field — center, corner, and edge become indistinguishable.

The fix: exclude any output place produced by more than one candidate. A shared place carries no discriminative signal — it’s the DC component that shifts every candidate equally. Only places unique to a single candidate can distinguish one candidate from another. This is analogous to mean-centering features before computing distances: the shared component must be subtracted before differences become meaningful.

Graph Theory First

The rate auto-derivation is pure graph theory. It operates on a bipartite directed graph — nodes are candidates and targets, edges pass through output places — and computes degree centrality of candidates with respect to targets through unique edges. Nothing about the algorithm requires Petri net firing semantics, token counts, or conservation laws.

The algorithm is structurally similar to a single message-passing step in a graph neural network:

• GNN: node_embedding = aggregate(neighbor_features)
• Petri net: rate[candidate] = count(reachable_targets through unique_outputs)

The difference: GNNs learn the aggregation function from data. The Petri net version uses a fixed, interpretable aggregation (count of target connections). No training needed.

What the Petri net formalism adds sits above the rate derivation. Firing semantics make transitions consume and produce tokens atomically, which gives state machines that graph connectivity alone cannot express. The mass-action rate law, $v[t]=k[t]\times \prod M[\text{inputs}[t]]$ (first power in every input place, as in go-pflow’s solver), couples the topology-derived constants to the current marking. P-invariants constrain the state space in ways centrality cannot. And the pre- and post-place lists of each transition, which are the incidence matrix with unit weights, define the gnark circuit’s constraints. The rate derivation says how much each candidate matters; the net’s semantics say what happens when one fires.

Poker Hand Ranking: Integer Reduction

The tic-tac-toe example derives strategic value from outgoing connectivity — more connections to win transitions means higher value. But the same mechanism works in reverse. In poker, we want to rank hand categories by rarity. Rare hands should have high value; common hands, low.

The construction encodes combinatorial frequency as structural outflow. The analysis net is build_hand_analysis_net in pflow-rs’s zk_holdem.rs example; each hand category gets:

• A source place src_H (1 token) — constant inflow via catalytic arc
• A value place val_H (0 tokens) — accumulation target
• A play transition play_H — moves tokens from source to value, returning the source token
• N drain transitions — consume tokens from val_H at a rate proportional to hand frequency

The drain counts are chosen by hand to rise with the 5-card combination counts. The source comment calls them log-scaled, but they are not a fixed log or power transform of the counts: one pair to two pair is a factor of 8.9 in combinations and 1.5 in drains.

The full net has 18 places and 113 transitions (9 play + 104 drain).

At equilibrium under mass-action kinetics, inflow equals outflow for each value place:

$$\text{rate}\times [sr{c}_H]=\text{num\_drains}\times \text{rate}\times [va{l}_H]$$

Since src_H is catalytic (always 1) and rates are uniform:

$$va{l}_H=\frac{1}{\text{num\_drains}}$$

Rare hands have fewer drains, accumulate more tokens, and produce higher equilibrium values. Common hands drain fast, accumulate little, and score low. Each accumulator is its own decoupled linear ODE, so this equilibrium is exact and needs no solver. The example runs Tsit5 to equilibrium anyway (hand_integer_reduction) and divides every value by the smallest, High Card’s $1/32$, which gives $32/\text{num\_drains}$. The values below are that closed form, derived rather than re-run:

Straight Flush:  32.0  (1 drain)
Four of a Kind:  16.0  (2 drains)
Full House:       8.0  (4 drains)
Flush:            6.4  (5 drains)
Straight:         4.0  (8 drains)
Three of a Kind:  2.7  (12 drains)
Two Pair:         2.0  (16 drains)
One Pair:         1.3  (24 drains)
High Card:        1.0  (32 drains)

The poker ordering comes out of the ODE because it went in with the drain counts. The frequency table is the poker knowledge, and what the net adds is a mechanical, inspectable path from that table to the values. Nothing in the net counts poker hands, which is the difference from tic-tac-toe, where the win-line counts are read off the game’s own transitions.

TTT vs. Poker: Same Mechanism, Inverted Reading

In tic-tac-toe, more connections to win transitions means higher strategic value: in Chapter 6’s ODE heatmap the center scores highest because it feeds the most win lines.

In poker, fewer drain connections means higher hand value. The raw concentration of val_H rises as the drain count falls, so the straight flush, with one sink, holds the most.

Both cases read a ranking back from token flow, exactly as $1/\text{num\_drains}$ for poker and approximately (within a few percent, per Chapter 6) as 4 : 3 : 2 for tic-tac-toe. In both, differential outflow creates differential accumulation.

This bears on the modeling-scope boundary of Chapter 15, where 52 detection transitions produced a score that nothing in the net read. Here the drain transitions take part in the dynamics: they are what makes each value place settle where it does. The scoring is still a design choice, moved from the multipliers into the drain counts, but it is now in a form the net computes with rather than one it merely stores.

The next chapter completes the pipeline: compiling guards and state invariants into ZK circuits, committing state with Merkle trees, and verifying proofs on-chain via smart contracts.