Generate ZK circuits from Petri net model (circuit synthesis from .btw DSL)

[stackdump]

Problem

The project's thesis is that Petri nets are ZK containers — the net structure should define both the smart contract AND the ZK circuit. Currently:

• Solidity contracts are generated from the Petri net model (.btw → schema → codegen) ✅
• ZK circuits are hand-written in Go (prover/circuits.go) ❌

The two are connected only by convention (same field names). The Petri net model doesn't generate the circuit constraints.

Current State

The VoteCastCircuit in prover/circuits.go is a flat gnark constraint system:

type VoteCastCircuit struct {
    PollID, VoterRegistryRoot, Nullifier, VoteCommitment, MaxChoices  // public
    VoterSecret, VoteChoice, VoterWeight                              // private
    PathElements, PathIndices [20]frontend.Variable                    // Merkle proof
}

It manually encodes: Merkle membership proof, nullifier binding, vote range check, commitment binding. None of this is derived from the Petri net model.

Desired State

A .btw file should be the single source of truth for:

1. Solidity contract (already works via solidity.Generate)
2. Foundry tests (already works via solidity.GenerateTests)
3. ZK circuit (new: circuit.Generate from the same schema)
4. Witness builder (new: derive from arc structure)

The Petri net structure maps naturally to ZK constraints:

• Input arcs = state that must be proven to exist (Merkle membership)
• Output arcs = state transitions that the proof commits to
• Guards = constraint equations the circuit must enforce
• Places with tokens = committed state (hashed into Merkle trees)
• Transitions = the action being proven (each is a separate circuit)

Example

For a vote poll with choices [a, b], the Petri net has:

• vote:a transition: consumes from voterRegistry, produces at tally:a + nullifiers
• vote:b transition: consumes from voterRegistry, produces at tally:b + nullifiers

This should generate two circuits (or one parameterized circuit):

• Prove: "I have a leaf in voterRegistry (Merkle proof), I'm producing a nullifier (binding), and I'm incrementing tally:a (commitment)"
• The choice IS the transition selection — not a parameter inside a single circuit

Design Considerations

• Each transition in the net = one circuit (or one variant of a parameterized circuit)
• Arc weights map to constraint values
• Keyed arcs (map access) require Merkle proofs for the state tree
• Read arcs (input+output to same state) = state that's verified but not consumed
• The Merkle tree depth could be a schema parameter
• Should work with the existing gnark Groth16 backend

Related

• The editor now shows poll-specific Petri nets with per-choice transitions
• Go/JS/Solidity execution parity is tested (runtime matches generated contracts)
• The .btw DSL already has the arc/guard/state information needed for circuit synthesis