Building ZK Poker: Four Petri Nets and a Branchless Circuit

stackedup.gg runs heads-up Texas Hold'em where every hand is provably fair. The deck shuffle is committed before play begins. At showdown, a Groth16 zero-knowledge proof verifies hand strength without revealing hole cards. No trust required.

The game logic itself is driven by four cooperating Petri nets — not a conventional state machine with switch statements, but declarative token dynamics. This post walks through how we built it.

Four Nets, One Game

A poker hand involves four distinct concerns: what phase we're in, what hand a player holds, what the bot should do, and where the chips are. Each gets its own Petri net.

Phase FSM — 7 states, 15 transitions. A statechart that encodes the legal phase progression: waiting → preflop → flop → turn → river → showdown → complete. Fold and all-in create shortcuts. Built with go-pflow's statemachine.Chart:

statemachine.NewChart("poker-phase").
    Region("phase").
    State("waiting").Initial().
    State("preflop").
    State("flop").
    State("turn").
    State("river").
    State("showdown").
    State("complete").
    EndRegion().
    When("deal").In("phase:waiting").GoTo("phase:preflop").
    When("deal_flop").In("phase:preflop").GoTo("phase:flop").
    When("fold").In("phase:preflop").GoTo("phase:complete").
    When("fold").In("phase:flop").GoTo("phase:complete").
    When("allin_resolve").In("phase:preflop").GoTo("phase:showdown").
    // ... remaining transitions
    Build()

The chart replaces if table.Phase == Preflop { ... } cascades with event-driven transitions. Illegal phase changes are structurally impossible.

Hand Classifier — 74 places, 235 transitions. The largest net. 52 card places (one per card), 13 rank aggregation places, 4 suit counters, and output places for pair, trips, quads, and straight flush. Card places use catalyst arcs — tokens flow through transitions but return to the source, preserving the input state while producing output signals.

The ODE solver runs this net and we read the output:

net := BuildHandNet(cards)
sol := solver.Solve(prob, solver.Tsit5(), solver.GameAIOptions())
final := sol.GetFinalState()

// Read output places
if final["straight_flush"] > 0.01 { return StraightFlush }
if final["four_kind"] > 0.01     { return Quads }
// ...

235 transitions encode every combinatorial pattern — 78 pair detectors (C(4,2) × 13 ranks), 52 trip detectors, 13 quad detectors, 40 straight flush patterns. No conditionals in the model. The topology is the evaluator.

Bot Decision — 10 places, 7 transitions. This is where it gets interesting. The house bot's strategy is a Petri net where input place token concentrations drive competing transitions:

Place("strength", 0).    // hand quality (0-20)
Place("weakness", 0).    // 12 - strength
Place("draws", 0).       // flush/straight outs
Place("pot_odds", 0).    // pot / (pot + toCall) × 10
Place("free", 0).        // 1.0 if no cost to act
Place("pressure", 0).    // chips at risk

Place("do_fold", 0).     // output
Place("do_check", 0).
Place("do_call", 0).
Place("do_raise", 0).

Seven transitions compete for tokens:

Notice raise_value takes two strength arcs — it fires proportionally to the square of hand strength. Strong hands raise much more aggressively than mediocre ones. This quadratic scaling emerges from the arc topology, not from a coded formula.

After ODE solving, the output place with the most tokens wins:

sol := solver.Solve(prob, solver.Tsit5(), solver.GameAIOptions())
final := sol.GetFinalState()

actions := map[string]float64{
    "fold":  final["do_fold"],
    "check": final["do_check"],
    "call":  final["do_call"],
    "raise": final["do_raise"],
}
// pick max, filter by legal actions

The bot's strategy is a topology, not an algorithm.

Chip Ledger — 4 places, 6 transitions. The simplest net, but it enforces the most critical invariant: player_0 + player_1 + pot == supply. Always. Chips cannot be created or destroyed — only moved between places via firing rules:

func chipFire(m chipMarking, t int, amount int64) (chipMarking, error) {
    arc := chipTopology[t]
    for _, p := range arc.Inputs {
        if m[p] < amount {
            return m, fmt.Errorf("insufficient tokens in %s: have %d, need %d",
                chipPlaceNames[p], m[p], amount)
        }
    }
    newM := m
    for _, p := range arc.Inputs  { newM[p] -= amount }
    for _, p := range arc.Outputs { newM[p] += amount }
    return newM, nil
}

Every chip movement — blinds, bets, pot awards — goes through this function. The conservation law is structural, not checked after the fact. Behind this sits a double-entry ledger and a SHA256-chained audit log for tamper evidence.

The Shuffle

Online poker's trust problem is the deck. We use commit-reveal with deterministic seeding:

Before play begins:

1. Server generates a random 32-byte serverSeed
2. Server publishes commitment = MiMC(serverSeed) — a hash the client stores
3. Client provides their own clientSeed

Each hand:

handKey = HMAC-SHA256(serverSeed, clientSeed || handNumber)
deck = Fisher-Yates shuffle seeded by handKey

Every card in every hand is deterministic given the two seeds and hand number. The server can't manipulate the deck after committing, because changing the seed would break the commitment.

After the session: Server reveals serverSeed. Client verifies MiMC(serverSeed) == commitment, then replays every shuffle independently. If any deck doesn't match what was dealt, the server cheated.

MiMC is used for the commitment because it's ZK-friendly — cheap to verify inside a circuit. HMAC-SHA256 handles the per-hand key derivation because it's fast and well-understood for this use.

The Branchless Circuit

At showdown, a player must prove their hole cards form the claimed hand rank — without revealing the cards. This is a Groth16 zero-knowledge proof compiled with gnark.

The constraint: ZK circuits can't branch. No if, no switch, no early returns. Every code path executes every time. The circuit evaluates all hand patterns simultaneously using arithmetic:

type ShowdownCircuit struct {
    // Public (12 values)
    Commitment     frontend.Variable    `gnark:",public"`
    CommunityRanks [5]frontend.Variable `gnark:",public"`
    CommunitySuits [5]frontend.Variable `gnark:",public"`
    ClaimedRank    frontend.Variable    `gnark:",public"`

    // Private (5 values — never revealed)
    HoleRanks [2]frontend.Variable
    HoleSuits [2]frontend.Variable
    Salt      frontend.Variable
}

The circuit does five things:

1. Verify commitment. MiMC(holeRank0, holeSuit0, holeRank1, holeSuit1, salt) == Commitment. This proves the player committed to these specific cards before the community cards were revealed.

2. Validate cards. Ranks must be in [2, 14], suits in [0, 3]. Checked via binary decomposition — a rank is valid if it decomposes into 4 bits that reconstruct to a value between 2 and 14.

3. No duplicates. For all 21 pairs among 7 cards: NOT(sameRank AND sameSuit). In circuit arithmetic:

sameRank := api.IsZero(api.Sub(allRanks[i], allRanks[j]))
sameSuit := api.IsZero(api.Sub(allSuits[i], allSuits[j]))
duplicate := api.Mul(sameRank, sameSuit) // AND = multiply
api.AssertIsEqual(duplicate, 0)

4. Classify hand. Count rank occurrences, detect pairs/trips/quads, check for straights and flushes — all branchlessly. The key trick is priority encoding with a running notClassified flag:

rank := frontend.Variable(0)
notClassified := frontend.Variable(1)

// Straight Flush (8) — checked first, highest priority
isSF := hasStraightFlush
rank = api.Add(rank, api.Mul(api.Mul(notClassified, isSF), 8))
notClassified = api.Mul(notClassified, api.Sub(1, isSF))

// Quads (7)
isQuads := api.Sub(1, api.IsZero(quadCount))
rank = api.Add(rank, api.Mul(api.Mul(notClassified, isQuads), 7))
notClassified = api.Mul(notClassified, api.Sub(1, isQuads))

// ... down through Pair (1) and High Card (0)

Once a hand type matches, notClassified drops to zero and all subsequent checks contribute nothing. No branches — just multiplication by zero.

5. Assert. computedRank == ClaimedRank. The proof succeeds only if the private hole cards, combined with the public community cards, actually form the claimed hand.

The compiled circuit runs in a 22MB WASM binary in the browser. Proof generation takes a few seconds on a modern machine; verification takes ~0.8ms.

Why Petri Nets?

We could have written all of this as conventional Go code — switch statements, if/else chains, explicit state tracking. It would work. But:

The phase FSM makes illegal transitions structurally impossible. We don't need to test that you can't go from waiting to showdown — the topology doesn't allow it.

The hand classifier encodes 235 combinatorial patterns without a single conditional. Adding a new pattern means adding transitions, not refactoring code paths.

The bot decision net lets us tune strategy by adjusting 7 transition rates — not rewriting logic. We can visualize the token dynamics to understand why the bot makes a given choice.

The chip ledger guarantees conservation structurally. There's no way to write a bug that creates chips from nothing, because the topology can't express it.

Each net is small enough to visualize, simulate, and reason about. Together they produce a complete poker game where the rules are topology, the strategy is dynamics, and the fairness is mathematics.

Try It

• stackedup.gg — play heads-up hold'em against the house
• pflow.xyz — visualize the poker nets
• ZK Hold'em post — hand ranking from topology
• Texas Hold'em Model post — the game state machine
• go-pflow — the Petri net library

All models are viewable at stackedup.gg/pflow — poker decision, hand classification, chip ledger, and phase flow.