Flat Transaction Constraint

Protocol Design
,
1

One decision we made for the current transaction layer is to forbid transaction nesting. This post is about what that is, the solutions I saw, and related topics. Another issue is forbidding cross-controller transactions, a topic for another post.

This continues a series of posts I started on AVM ISA: What we’re currently building and why at 12/11/25 that somehow shares some of my current thoughts. As a result, I assume the reader has some familiarity with the current instruction set and has read ideas about the interpreter, or can infer how it’s implemented; if not, read the Interpreter spec in progress.

The AVM TxInstruction set includes beginTx, commitTx, and abortTx
operations. The interpreter uses a single Maybe TxId field in state to track
the active transaction. I call this the tx overlay layer. This design implicitly prevents nested transactions but
does not enforce the constraint explicitly. That is, the check is done at
runtime, not at compile time. What good is that?

The TxInstruction set

data TxInstruction : Safety → ISA where
  beginTx : TxInstruction Safe TxId
  commitTx : TxId → TxInstruction Safe Bool      -- May fail if conflicts
  abortTx : TxId → TxInstruction Safe ⊤

How to prevent nested tx calls.

As part of interpreting tx operation, when beginTx executes while a transaction is already active (state tx overlay), the interpreter silently overwrites the existing transaction state, this is how we are doing:

executeTx beginTx st =
  let txid = freshTxId (getFreshIdCounter st)
      st' = record st { tx = just txid
                       ; txLog = []
                       ; creates = []
                       ; destroys = []
                       ; observed = []
                       }

This creates three issues:

  1. The outer transaction’s txLog, creates, destroys, and observed are
    lost
  2. The outer transaction ID becomes orphaned—it cannot be committed or aborted
  3. No error is reported to the program (although we could squeeze in a logger call).

Don’t expect nested transactions, it just complicates semantics

Supporting nested transactions requires answering several design questions with
no canonical solution:

  • Abort semantics: Should an inner abort roll back only its changes or cascade to
    the outer transaction? Should an outer abort invalidate committed inner
    transactions?

  • Isolation: Can inner transactions observe uncommitted outer changes? If an inner
    transaction commits but the outer aborts, should the inner changes persist?

  • Commit dependencies: Are inner commits provisional until outer commit (savepoint
    model) or immediately durable (autonomous transaction model)?

  • How do read sets and version tracking interact across
    nesting levels? Do inner transactions extend or partition the outer read set?

Different transaction systems make different choices here. The AVM currently
avoids this complexity by maintaining a single active transaction at a time.

Solutions?

  • Option 1: Explicit runtime check rejecting nesting

Modify executeTx beginTx to reject nesting:

executeTx beginTx st with State.tx st
... | just oldTxId = failure (err-nested-tx-not-supported oldTxId)
... | nothing = -- current implementation

And consistently, add a new error constructor to TxError:

data TxError : Set where
  -- existing constructors
  ErrNestedTxNotSupported : TxId → TxError

Good thing: Clear error feedback. Documents the constraint explicitly.
Disadvantages: Runtime error only, not compile-time prevention.

  • Option 2: Static prevention via indexed types. type-driven solution.

Use type-level transaction state to prevent nesting statically:

data TxState : Set where
  NoTx : TxState
  InTx : TxId → TxState

data TxInstruction : TxState → TxState → Set → Set where
  beginTx  : TxInstruction NoTx (InTx ?txid) TxId
  commitTx : TxId → TxInstruction (InTx txid) NoTx Bool
  abortTx  : TxId → TxInstruction (InTx txid) NoTx ⊤

Programs that nest transactions would fail to type-check.

Advantages: Compile-time guarantee. Self-documenting in the type system. Enables
richer static analysis.
Disadvantages: Requires refactoring the instruction type, interpreter, and all
existing programs. Increases type complexity. May not compose cleanly with other
instruction families.

  • Option 3: Structured transaction combinator. Also neat.

Replace raw transaction instructions with a bracketing combinator as the primary
interface:

withTx : AVMProgram A → AVMProgram A
withTx prog =
  beginTx >>= λ txid →
  prog >>= λ result →
  commitTx txid >>= λ ok →
    if ok then ret result else abortTx txid >> ret result

Advantages: Ensures proper bracketing. Prevents forgetting to commit or abort.
Disadvantages: Requires interpreting nested withTx as sequential, autonomous transactions, which contradicts standard ACID semantics, where an outer abort should roll back inner commits.

So what do we do?

Use option 1 unless someone tells me otherwise. The runtime check is minimally invasive and provides clear feedback.
If nested transactions become necessary later, the error check can be replaced with a full implementation after resolving the semantic questions above, which I think are not trivial; prove me wrong.