Building ZK Poker: Four Petri Nets and a Branchless Circuit

Prerequisites: Texas Hold'em Model for the game as a net, and Zero-Knowledge Proofs for Petri Nets for the Groth16 setup.

stackedup.gg runs heads-up Texas Hold'em against a house seat. In a casino session the deck for every hand is fixed by a seed the server commits to before play, and at showdown the player's browser can generate a Groth16 proof that checks their claimed hand score against their committed hole cards without revealing them.

Four Petri nets sit in the stackedup-gg zk-poker package: a phase statechart, a hand classifier, a bot decision net and a chip ledger. They don't all carry the same weight. The phase net and the chip ledger are on every hand's path — the table cannot change phase or move a chip except by firing them. The hand classifier labels each hand at showdown, but the pot is decided by a conventional scorer. The decision net is a working, tested bot that does not currently sit in the house seat. Each section below says which. The stackedup-gg source is not in a public repository, so the file and test names below are pointers for whoever has it; the nets themselves are public in the model viewer.

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 (zk-poker/petri_phase.go):

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()

Table holds a PokerPhaseNet, and every phase change in game.go is an event sent to it (Deal, DealFlop, Fold, AllInResolve, …); the phase field is read back from the machine, never assigned. An event that isn't enabled in the current phase is refused — SendEvent returns false and the phase stays where it was. There is one deliberate escape hatch: Reset rebuilds the machine from its initial state if the hand isn't already in complete.

Hand Classifier — 73 places, 235 transitions. The largest net: 52 card places (one per card), 13 has_rank aggregation places, 4 suit counters, and 4 output places for pair, trips, quads and straight flush. Card places use catalyst arcs — each transition consumes a card token and returns it, so the inputs stay constant while the output places accumulate. The ODE solver runs the net and we read the outputs (abridged from EvaluateHand in zk-poker/petri_hand.go):

net := BuildHandNet(cards)
rates := handNetRates(net)
initial := handNetInitialState(net, cards)

prob := solver.NewProblem(net, initial, [2]float64{0, 1}, rates)
sol := solver.Solve(prob, solver.Tsit5(), solver.GameAIOptions())
final := sol.GetFinalState()

pairVal := final["pair"]
tripsVal := final["three_kind"]
quadsVal := final["four_kind"]
sfVal := final["straight_flush"]

if sfVal > 0.01 {
    return StraightFlush
}
if quadsVal > 0.01 {
    return Quads
}
// ...

The 235 transitions are 52 aggregation transitions (each card feeds its rank and suit counters) plus 183 pattern detectors — 78 pair detectors (C(4,2) × 13 ranks), 52 trip detectors (C(4,3) × 13), 13 quad detectors and 40 straight-flush patterns (10 runs × 4 suits). There are no conditionals in the net, but the read-out has some. Straight flush and quads come straight off an output place; trips and pair do too, once full house and two pair have been ruled out by rounding the pair and trip counts; flush and straight are read from the aggregation places — a suit counter above 4.5, or all five has_rank places of a straight pattern non-zero. The topology does the counting and a dozen lines of Go thresholds do the rest. TestPetriHandMatchesAlgorithmic in zk-poker/petri_hand_test.go checks the net against the conventional evaluator on nine seven-card hands, one per class (not re-run for this revision); nothing checks it exhaustively. At the table, game.go uses the net to label each hand's rank at showdown, while the pot goes to the higher ComputeHandScore — the conventional rank-plus-kickers scorer, which is also what the circuit below proves.

Bot Decision — 10 places, 7 transitions, 34 arcs. A poker strategy as a net: the game state sets token concentrations in six input places, and competing transitions route flux to four output places (abridged from BuildDecisionNet in zk-poker/petri_bot.go; the comments are ours, taken from computeInputs):

Place("strength", 0).    // hand quality (0-20)
Place("weakness", 0).    // max(0, 12 - strength)
Place("draws", 0).       // flush/straight outs
Place("pot_odds", 0).    // pot / (pot + toCall) × 10
Place("free", 0).        // 1.0 if nothing to call, else 0.01
Place("pressure", 0).    // min(toCall, 20)

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

Seven transitions compete for tokens:

raise_value takes two input arcs from strength. go-pflow's mass-action rate multiplies the transition rate by the input marking once per input arc entry, with arc weight scaling consumption only (solver/ode.go), so this transition's flux goes as strength² while the other six are bilinear — strong hands raise disproportionately more than mediocre ones. A single arc of weight 2 would not do it; the squaring comes from the two arc entries.

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

That map is a sketch of Decide, which does the same thing by iterating the output places. Where this bot plays is the qualification. The house seat in a casino session is NewODEBot() (casino.go), and despite its name ODEBot is a hand-written heuristic — Chen-score bands preflop, an equity table and pot odds postflop, randomized bluffs — with no net in it. The decision net runs as PetriBot in the Go tests (zk-poker/petri_bot_test.go: structure counts, expected actions on fixed preflop and postflop spots, never folding aces, deterministic output, and a printed side-by-side against the Chen and ODE bots that reports agreement without asserting any) and, through a JS port in frontends/zk-poker/petri-bot.js, as the analysis panel in training mode. That port currently returns NaN strength for a suited A-K hole; the repo's TODO tracks it.

Chip Ledger — 4 places, 6 transitions. The smallest net, and the one carrying the invariant that matters most: player_0 + player_1 + pot == supply. Chips move between places only by firing (zk-poker/petri_ledger.go):

func chipFire(m chipMarking, t int, amount int64) (chipMarking, error) {
    if t < 0 || t >= chipNumTransitions {
        return m, fmt.Errorf("invalid transition: %d", t)
    }
    if amount <= 0 {
        return m, fmt.Errorf("amount must be positive: %d", amount)
    }
    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
}

Table owns a PokerChipNet, and blinds, calls, raises, all-ins and pot awards in game.go all go through its Bet and Win, which call this function. Every transition in the topology preserves the sum — mint adds to supply and one player together, bet and win move chips between a player and the pot — so the law holds per firing rather than being checked after the fact. What the net refuses is an overdraft: chipFire returns an error when an input place is short. The callers in game.go currently discard that error, so a refused bet is a silent no-op rather than a halted hand. Behind the net sits a double-entry chip ledger in SQLite (ledger.go) and a SHA-256 hash-chained audit log (audit.go), which the server will re-verify on request at /api/zkpoker/audit/verify.

The Shuffle

The deck is online poker's trust problem. Casino sessions use commit-reveal with deterministic seeding (zk-poker/fair_shuffle.go); outside a casino session, Table.StartHand shuffles with crypto/rand and there is no seed commitment.

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 (optional — if the client never sends one, the key below derives from the server seed and hand number alone)

Each hand:

handKey = HMAC-SHA256(serverSeed, clientSeed || handNumber)
deck    = Fisher-Yates, i = 51..1, swapping i with SHA-256(handKey || i) mod (i+1)

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

On reveal: when the client sends casino_reveal_seed, the server returns serverSeed with the commitment and the number of hands played. Anyone holding the seeds and hand numbers can check MiMC(serverSeed) == commitment and recompute every deck; zk-poker/fair_shuffle_test.go does that server-side (same seeds give the same deck, hand number and client seed change it, no duplicates, the commitment recomputes). The browser client displays the commitment and the revealed seed but does not yet replay the decks itself — that check is left to the player.

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 proves that their hole cards, with the board, produce the claimed hand score — rank and kickers — without revealing the cards. This is a Groth16 zero-knowledge proof compiled with gnark (zk-poker/showdown_circuit.go).

The constraint is that a circuit can't branch on a private value. No if, no switch, no early returns on the witness — every path executes every time, so the circuit evaluates all hand patterns at once using arithmetic:

// ClaimedScore encodes hand rank + kickers as: handRank * 15^5 + k1 * 15^4 + ... + k5
type ShowdownCircuit struct {
    // Public (12 variables)
    Commitment     frontend.Variable    `gnark:",public"`
    CommunityRanks [5]frontend.Variable `gnark:",public"`
    CommunitySuits [5]frontend.Variable `gnark:",public"`
    ClaimedScore   frontend.Variable    `gnark:",public"`

    // Private (5 variables)
    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] and suits in [0, 3], each checked as two bounds by binary decomposition: rank − 2 and 14 − rank must both fit in 4 bits, suit and 3 − suit in 2 bits.

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)
api.AssertIsEqual(duplicate, 0)

4. Score the hand. Count rank occurrences, detect pairs/trips/quads, check for straights and flushes — all branchlessly. The rank comes from priority encoding with a running notClassified flag:

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

isSF := hasStraightFlush
handRank = api.Add(handRank, api.Mul(api.Mul(notClassified, isSF), 8))
notClassified = api.Mul(notClassified, api.Sub(1, isSF))

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

// ... down through Pair (1); High Card is what's left (0)

Once a hand type matches, notClassified drops to zero and every later check contributes nothing — multiplication by zero instead of a branch. The kickers are selected the same way: a kicker vector is computed for every hand type, and exclusive flags mux in the one that applies. Rank and five kickers fold into a single integer, handRank·15⁵ + k₁·15⁴ + … + k₅, so two hands compare as two numbers.

5. Assert. computedScore == ClaimedScore. The proof succeeds only if the private hole cards, combined with the public community cards, produce exactly the claimed score.

zk-poker/showdown_test.go proves one hand of each class plus the wheel, and checks that a wrong claim, a wrong salt and a duplicated card each make the prover fail (not re-run for this revision). The prover is compiled to WebAssembly (zkpoker.wasm, loaded by frontends/zk-poker/game.js), so the proof is generated in the player's browser; if it doesn't load, the server resolves the hand without a proof. We have not recorded the binary's size, the constraint count (TestShowdownCircuit_Compiles logs it, but nothing pins it), or proof and verification times for this circuit.

What the nets carry

We could have written all four as conventional Go, and two of them partly are. The phase net and the chip ledger earn their place directly: illegal phase events and overdrafts are refused by the structure instead of by checks scattered through game.go, and conservation is a property of the topology that holds on every firing. The hand classifier is half of an evaluator — the net counts, a few thresholds in Go read the counts — and its correctness rests on a nine-hand agreement test against the conventional evaluator, which still decides the pot. The decision net shows what a strategy looks like as seven rates and one squared arc, and the training panel lets you watch its token dynamics, but the house doesn't play it. Each net is small enough to open in the viewer and read.

All five poker models — poker-flow, poker-hand, poker-preflop, poker-decision and poker-chips — open in the viewer at stackedup.gg/pflow. Play against the house at stackedup.gg; the Petri net library is go-pflow.

What Changed

For readers of the August version (revised 2026-10-19 against the stackedup-gg source):

1. Place count. The hand classifier has 73 places, not 74 — 52 + 13 + 4 + 4. The comment in BuildHandNet still promises a fifth has_hand output that the builder never creates, and the figure above still says 74; the structure test's own comment counts 73.
2. The 235 transitions. The four detector families sum to 183; the other 52 are card-aggregation transitions. And "the topology is the evaluator" was too strong: flush, straight, full house and two pair are decided by Go thresholds on the net's counts.
3. The house bot. The post said the house's strategy is the decision net. The casino seat plays ODEBot, a hand-written heuristic; the decision net runs in tests and in the training panel.
4. The circuit proves a score. The public input is ClaimedScore (rank plus five kickers in base 15), not ClaimedRank, and rank validity is two 4-bit bounds rather than a single decomposition.
5. Shuffle scope. Commit-reveal covers casino sessions only, the client seed is optional, and the browser does not replay the decks itself.
6. Unsourced numbers removed. "22 MB WASM" and "~0.8 ms verification" had no measurement behind them for this circuit; they match figures quoted elsewhere on this blog for other circuits (bitwrap's prover, and the per-transition proofs in ZK Hold'em).
7. Chip conservation. "No way to write a bug that creates chips" became what the code shows: the sum is preserved per firing, overdrafts are refused, and the callers currently drop the refusal.

Related: ZK Hold'em · Texas Hold'em Model · Zero-Knowledge Proofs for Petri Nets