Choice Semantics

CHOICE_SEMANTICS Skill (DAML)

Trigger Pattern: Always required for DAML audits Inject Into: Breadth agents, depth-state-trace, depth-edge-case Finding prefix: [DML-CHS-N] Rules referenced: R8, R10, R12, R14

In DAML a "write" is a choice that archives a contract and creates a successor. The consume-mode of a choice determines whether the contract survives the exercise: a consuming choice (the default) archives the contract on the first exercise; a nonconsuming choice leaves it active. Misusing consume-mode is the DAML analog of double-spend: a value-moving choice marked nonconsuming can be exercised repeatedly on the same contract. Pre/postconsuming ordering bugs (self-fetch after archive), value-conservation gaps across split/merge/transfer, accumulator/cap drift across transactions, and cancel/abort paths that leave consequences un-unwound round out this class.

1. Consume-Mode Inventory

For EVERY choice, record its consume-mode and whether the action should be one-shot:

Critical patterns to flag:

• A nonconsuming choice that transfers, mints, splits, or withdraws value → exercisable repeatedly on the same active contract ([ELEVATE:NONCONSUMING_REPLAY], double-spend).
• A consuming choice intended to be repeatable that archives the contract and strands its peers.

DAML note: A consuming choice archives the contract; a SECOND exerciseCmd on the same ContractId MUST fail with CONTRACT_NOT_FOUND. That failure REFUTES a double-spend claim for a consuming choice. Double-spend is only reachable when the value-mover is nonconsuming (or recreates an equivalent contract).

2. Pre/Postconsuming Ordering Trace

preconsuming archives BEFORE the body runs; postconsuming archives AFTER. A body that fetches self (or this via key) behaves differently across the two.

Attack: A preconsuming choice that fetches its own contract by key in the body gets NO_SUCH_KEY/CONTRACT_NOT_FOUND because the archive already happened — either a brick (liveness) or, if guarded by a lookupByKey, a silent wrong branch. A postconsuming choice that re-exercises a sibling assuming self is gone may double-act.

3. Successor-State Completeness

Each value-moving choice should produce successor contracts that conserve value and carry forward every invariant field.

Check for:

• Split/merge where the sum of outputs ≠ input (value created or burned; rounding direction favors the caller) — R14 cross-variable conservation.
• A successor that drops a locked, owner, or maintainer field present in the predecessor (metadata/lock erase).
• An accumulator/cap field (totalIssued, mintedSoFar) that is NOT updated on the create path, so the cap is never enforced across transactions ([ELEVATE:VALUE_CONSERVATION], R14).

4. Cancel / Abort Unwind

A choice that allocates or locks resources must unwind them on the cancel/abort/reject path.

Attack: A Propose/Reserve choice creates a child contract or locks an asset; the Cancel/Reject choice archives the proposal but leaves the child/locked asset active. The reserved value is stranded or double-counted. Verify the cancel path archives every contract the success path created.

Finding Template

**ID**: [DML-CHS-N]
**Severity**: [Critical if double-spend/value-creation, High if conservation/lock-erase, Medium if liveness-only]
**Step Execution**: ✓1,2,3,4 | ✗(reasons) | ?(uncertain)
**Rules Applied**: [R8:✓/✗, R10:✓/✗, R12:✓/✗, R14:✓/✗]
**Location**: {Module}.daml:LineN (template X, choice Y)
**Title**: {Choice} nonconsuming value-mover / value-conservation gap allows {double-spend / value inflation}
**Description**: [Consume-mode or conservation gap with the exact in/out amounts and the field or successor that breaks]
**Impact**: [Repeated exercise on same contract / value created or destroyed / stranded locked asset / cap unenforced]
**PoC steer**: exercise the same `ContractId` twice (nonconsuming double-spend), or assert `out1.amt + out2.amt /= in.amt`, or `query@T` a stranded child after cancel.

Step Execution Checklist (MANDATORY)