The Token Language

At the heart of go-pflow is a language for defining and executing token models. Four terms generate the entire structure.

The Four Terms

These are the generators of a free symmetric monoidal category. Every token model — ERC-20 tokens, game boards, workflow engines — is a composition of morphisms built from these four terms. The DSL is a text syntax for writing morphisms.

S-Expression Syntax

(schema ERC-20
  (version v1.0.0)

  (state totalSupply :type uint256)
  (state balances :type map[address]uint256 :exported)
  (state allowances :type map[address]map[address]uint256)

  (action transfer :guard {balances[from] >= amount && to != address(0)})
  (action approve)
  (action mint :guard {to != address(0)})
  (action burn :guard {balances[from] >= amount})

  (arc balances -> transfer :keys (from))
  (arc transfer -> balances :keys (to))
  (arc mint -> totalSupply)
  (arc totalSupply -> burn)

  (constraint conservation {sum(balances) == totalSupply}))

Each form declares structure. The parser builds an AST, the interpreter converts it to an executable schema with validated references. The same text that documents the model runs it.

Memory Model: Tokens vs Data

The language distinguishes two kinds of state:

TokenState

Integer counters. Classic Petri net semantics — firing consumes from input places, produces to output places. Tokens are fungible; we track counts, not individuals.

type Snapshot struct {
    Tokens map[string]int  // TokenState
    Data   map[string]any  // DataState
}

DataState

Typed containers — maps, records, scalar values. Arc keys specify access paths: (arc balances -> transfer :keys (from)) binds from to the map key. Data arcs read and write; they don't consume.

The combination handles both control flow (tokens) and data transformations (balances, permissions, structured state).

Guards and Invariants

Guards and invariants split into right and left context:

Guards are right context — predicates on the current marking, recomputed each step. An action fires only when its guard is true:

balances[from] >= amount && to != address(0)

Guards support comparison, logical operators, indexing (balances[key], allowances[owner][spender]), field access, and function calls (sum, count, address(0)). Short-circuit evaluation.

Invariants are left context — conservation laws that must hold across all transitions:

(constraint conservation {sum(balances) == totalSupply})

Guards ask "can we fire?" Invariants ask "did we break a conservation law?" The core-observer boundary runs between them: invariants enforce the reversible core's P-invariants, guards enforce the irreversible observer's predicates.

Execution Pipeline

From source to running model: lexer → parser → AST → executable schema. Each action execution follows the zipper step: check guard (right context), process input arcs (consume/bind), process output arcs (produce/update), check invariants (left context), commit snapshot.

If the guard fails, the action is blocked. If an invariant fails, the action rolls back. The marking updates, the left context grows, the right context recomputes. One step to the right.

From Prototype to Production

The S-expression syntax above is the prototype in go-pflow. Bitwrap is the production language — a .btw syntax that compiles to Solidity smart contracts, ZK circuits, and Foundry test suites:

schema ERC20 {
  register ASSETS.AVAILABLE map[address]uint256 observable
  register ASSETS.TOTAL_SUPPLY uint256

  fn(transfer) {
    var from address
    var to address
    var amount amount

    require(ASSETS.AVAILABLE[from] >= amount && amount > 0)

    ASSETS.AVAILABLE[from] -|amount|> transfer
    transfer -|amount|> ASSETS.AVAILABLE[to]
  }
}

The arc syntax -|amount|> is a morphism in the free SMC written as text. register declares objects. fn declares morphisms. require is the right context. The compiler generates Solidity (the universe — on-chain state), ZK proofs (the left context — compressed witness of valid past transitions), and tests.

The compilation pipeline is the pflow square: parse the net (N), build the SMC (F), extract the universe (U), equip execution context (Exec). Bitwrap closes that loop — a categorical language where programs are morphisms, compilation enforces the structure, and you get verified contracts out the other end.

Try It

The prototype is in go-pflow. The production compiler is at bitwrap.io. For visual exploration, pflow.xyz provides a browser-based editor with ODE analysis.

Related: The Pflow Square · Symmetric Monoidal Categories · The Zipper Whose Hole Is a Universe · Earned Compression · Bitwrap Capstone

This topic is covered in depth in Chapter 4: The Token Language of Petri Nets as a Universal Abstraction.