Atomic-tx invariant

The load-bearing safety property of the SDK:

gate_payment + SPL transferChecked + emit_feedback MUST execute as one Solana transaction. Splitting them silently corrupts state when a Token-2022 mint's TransferHook extension reverts the transfer.

Background writeup: docs/proofs/transfer-hook-atomicity.md. The proof is structured as five layers; all five must hold.

The corruption vector

gate_payment_strict mutates state on Allow:

• PolicyAccount.spending_today_used, spending_today_anchor, spending_week_used, spending_week_anchor
• VelocityLedger.cumulative_amount, last_commit_slot, window_start_slot

If a downstream SPL transfer reverts after that mutation — and the two instructions are in different Solana transactions — the gate's state is durable while no money has moved. Subsequent gate_payment calls read the inflated counters and may Deny a legitimate payment. In the inverse, counters can drift such that velocity caps appear hit when nothing real has happened.

A Token-2022 TransferHook extension is the canonical instance of this fault model. The hook program runs synchronously inside the SPL transferChecked execution; if it returns Err, the transfer aborts. The specifics — compliance check, allowlist denial, freeze on suspicious counterparty — are domain-specific. From the runtime's perspective, a TransferHook revert is indistinguishable from any other inner-ix revert (NonTransferable mint, DefaultAccountState=Frozen, MissingRequiredSignature, out-of-funds). The atomicity guarantee is mint-extension-agnostic.

Five layers of proof

A — SDK type + runtime guards

export interface AtomicityEnforced {
  readonly atomicityEnforced: true;     // literal true, not boolean
}

export class AtomicityNotEnforcedError extends Error {
  constructor(siteName: string) {
    super(`[${siteName}] atomicityEnforced=true is required …`);
    this.name = "AtomicityNotEnforcedError";
  }
}

export function assertAtomicityEnforced(
  cfg: { atomicityEnforced?: unknown },
  siteName: string,
): void {
  if ((cfg as any).atomicityEnforced !== true) {
    throw new AtomicityNotEnforcedError(siteName);
  }
}

Compile-time: composeAtomicSettleTx({ …, atomicityEnforced: false }) is a TS error. Runtime: composeAtomicSettleTx({ …, atomicityEnforced: 1 } as any) throws AtomicityNotEnforcedError("composeAtomicSettleTx"). Both layers required: skipping either re-opens the corruption vector.

A.3 — Composer structure

composeAtomicSettleTx returns:

interface ComposedAtomicSettle {
  readonly tx: Transaction;
  readonly instructions: ReadonlyArray<TransactionInstruction>;  // exactly 3
  readonly accounts: { … };
}

The three instructions, in order:

1. gate_payment_strict — Err on Deny / RequireValidation. Reverts the whole bundle if the gate denies.
2. SPL transferChecked (legacy Token or Token-2022 — tokenProgram arg switches).
3. emit_feedback — PDA-signed CPI into Quantu via TrustGate.

Five test cases pin this contract — including a Token-2022 program-id propagation case that ensures the SPL ix uses TOKEN_2022_PROGRAM_ID when the caller passes it.

B+C — Localnet runtime proofs

The Anchor TS test tests/atomic-tx-invariant.spec.ts splits into two describe blocks:

• B. single-tx atomic revert. Builds the bundled tx with an intentionally-failing System.transfer (source keypair never signs → guaranteed MissingRequiredSignature) and asserts the entire bundle reverts; PolicyAccount + VelocityLedger remain in their pre-tx state.
• C. split-tx anti-pattern corrupts state. Splits the same flow into two transactions. Tx 1 commits the gate's velocity update. Tx 2 reverts on the failing transfer. The ledger now reflects a payment that never moved — the corruption vector that B prevents.

Why System.transfer instead of TransferHook

The localnet tests deliberately use a System.transfer with a never-signed source as the failing inner instruction. This:

1. Exercises the same Solana atomicity semantics a TransferHook revert would — the runtime aborts the bundle, all child mutations roll back.
2. Requires no Token-2022 mint setup or custom hook program on the localnet validator, keeping the test focused on the property under proof rather than mint-init plumbing.
3. Documents the corruption vector at the layer where it actually matters: any failing inner ix corrupts split-tx state. TransferHook is one specific failure mode, not the property itself.

The Token-2022 angle is fully covered at the SDK layer in composeAtomicSettleTx test cases.

On-chain Kani anchor

The strict handler's contract is pinned by Kani gate_payment_strict_correctness:

• strict_returns_ok_iff_allow — Ok(()) ⇔ Allow. 131 sub-checks.
• gate_decision_is_one_of_three_disjoint_variants — three arms pairwise disjoint; a fourth variant cannot silently slip past. 127 sub-checks.

Combined: 258 sub-checks, ~0.9 s. Sub-check 0 failed. If a future change re-routes the Deny arm to an Ok return, both proofs fail loud.

The on-chain anchor + the SDK guards together close the corruption vector at three layers: compile, runtime, and on-chain.

Reproduce

git clone https://github.com/agenttrust-labs/agenttrust && cd agenttrust
pnpm install

# A — SDK layers
cd trustgate/sdk
pnpm test                      # 6 atomicity-specific cases + 50 others

# B + C — localnet
cd ../..
anchor build
anchor test --provider.cluster localnet --validator legacy --skip-build

# On-chain anchor (Kani)
cd programs/policy-vault
cargo kani --harness strict_returns_ok_iff_allow
cargo kani --harness gate_decision_is_one_of_three_disjoint_variants

Read next