Field note
Petri Nets: A Small Machine for Resources That Must Not Duplicate
A Petri net is a diagram with two kinds of node. Places hold tokens. Transitions move tokens by consuming a required input marking and producing an output marking. A transition cannot fire unless every required token is present.
That is already close to a private value system. A committed resource is a token. An Action is a transition. The nullifier proves that an input token was consumed once, while the new commitments describe the output marking. The proof does not narrate what happened; it certifies that one legal transition took the old resources to the new ones.
The offer as the smallest useful net
PayMoney's FiatOfferV1 has two live states, Open and Claimed. One transition moves between them:
- Claim consumes
Openand createsClaimed.
The other three are terminal — they consume a live offer and create no successor:
- Cancel consumes
Openand returns the escrow to the maker. - Solve consumes
Claimedand releases the escrowed asset to the taker and collector. - Expire consumes
Claimed, after its epoch budget, and returns the asset to the maker.
The terminal results are not extra state tokens. The offer is gone. That distinction matters: there is no Settled, Failed, or Reclaimed object waiting to be interpreted later.
Two safety properties follow from the shape of the net. Because every terminal transition requires the one escrow token, two outcomes cannot both consume it. Because Cancel also requires Open, the maker cannot cancel after a taker has claimed. These are structural facts about the transition set, not branch order in an application service.
Why “open” Petri nets matter
An open Petri net marks explicit input and output boundaries. Two nets compose by gluing an output boundary of one to an input boundary of another. This provides a clean picture of the vault's L1 edge: deposits enter through an input leg, withdrawals leave through an output leg, and private resource transitions live inside.
Solver composition has the same shape. Compatible intents can be glued at matching boundaries, while the composed proof still accounts for every input and output. The composition rule is not “run two scripts and hope their bookkeeping agrees”; it is a mathematical operation on the boundaries.
Nets within nets
Object Petri nets allow tokens to carry their own transition systems. That captures the vault/kind split. The Compliance-AIR is the system net: it understands opaque resources, uniqueness, membership, authority coverage, and completeness. A kind such as FungibleV1 or FiatOfferV1 is an object net: it supplies the meaning and conservation rule for its resources.
The synchronization point is the authorization signal. An owner policy validates who may consume a resource; the resource logic validates what that consumption may do. The universal layer never has to learn what PLN, an offer, or a final bank status means.
This is why Petri nets are more than a visual metaphor here. They explain which transitions exist, how resources compose, and why “invalid states are unprovable” can be implemented as the absence of a transition rather than as another runtime error branch.