Locking Semantics

LOCKING_SEMANTICS Skill (DAML)

Trigger Pattern: Always required for DAML audits — self-skip if no lock pattern present Inject Into: Breadth agents, depth-state-trace, depth-edge-case Finding prefix: [DML-LK-N] Rules referenced: R8, R10, R14

DAML has no native lock primitive; locking is emulated by a template field (locked : Bool, lockedUntil : Time, a held lock contract, or a separate Locked template wrapping the asset). The invariant is: while locked, the asset MUST NOT be split, merged, transferred, or archived through any path; and the value MUST be conserved across the lock→unlock cycle. The two high-yield bugs are lock-bypass (a choice that moves the asset ignores the lock field) and lock-erase (a choice recreates the asset successor dropping the locked field). If no template carries a lock field / lock wrapper, this skill self-skips.

1. Lock-State Inventory

Identify every lock mechanism and the asset it protects:

DAML note: A lock encoded as a plain Bool/Time field on the asset template is only honored if EVERY value-moving choice reads it. A lock encoded as a separate wrapper template is only honored if the underlying asset cannot be exercised directly while wrapped.

2. Lock-Honoring Audit (lock-bypass)

For EVERY value-moving choice on a lockable template, verify it checks the lock:

Attack: A Transfer/Split choice does not read locked, so a locked asset can still be moved ([ELEVATE:LOCK_BYPASS]). For wrapper-based locks: verify the underlying asset's own choices are not directly exercisable while wrapped (e.g., the wrapper holds the only ContractId and the asset's signatories prevent independent exercise).

Check for:

• ANY value-moving choice with zero lock check on a lockable template.
• A time-lock (lockedUntil) compared with the wrong relation (>= vs >) or against a caller-supplied time instead of getTime.

3. Lock-Erase Audit

A choice that recreates the asset successor must carry the lock field forward.

Attack: A consuming choice (e.g., a metadata update or partial action) archives the locked asset and creates a successor with locked = False (or omits the field, defaulting unlocked). The lock is silently erased and the asset is now freely movable. Verify every successor of a locked contract preserves the lock state.

4. Value-Conservation Across Lock/Unlock

The lock→unlock cycle must conserve the protected value and not double-count it.

Check for (R14):

• Unlock returns MORE than was locked (value inflation) or LESS (value loss).
• The locked asset is counted both in a Locked wrapper AND still in the original holder's balance (double-count).
• A unlock path reachable without the corresponding lock (mint-on-unlock), or a lock with no unlock (permanent loss / brick).

Finding Template

**ID**: [DML-LK-N]
**Severity**: [Critical if locked value moved/inflated, High if lock erased, Medium if liveness/double-count]
**Step Execution**: ✓1,2,3,4 | ✗(reasons) | ?(uncertain)
**Rules Applied**: [R8:✓/✗, R10:✓/✗, R14:✓/✗]
**Location**: {Module}.daml:LineN (template X, choice Y)
**Title**: {Choice} ignores lock / erases lock on successor allows moving locked {asset}
**Description**: [The lock mechanism, the choice that bypasses or erases it, and the value path that breaks the invariant]
**Impact**: [Locked asset moved despite lock / lock silently cleared / value inflated or double-counted across lock cycle]
**PoC steer**: lock the asset, then `submit owner (exerciseCmd cid Transfer ...)` and assert it SUCCEEDS (bypass); or update-then-`query@T` the successor and assert `locked == False` (erase); or assert unlock value /= locked value (conservation).

Step Execution Checklist (MANDATORY)