| name | locking-semantics |
| description | Trigger Pattern Always required for DAML audits (self-skips if no lock pattern present) - Inject Into Breadth agents, depth-state-trace, depth-edge-case |
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:
| Template | Lock Mechanism | Lock Field/Wrapper | Set By (choice) | Cleared By (choice) | Asset Protected |
|---|
{T} | bool field / time field / Locked wrapper | {locked / lockedUntil} | {choice} | {choice} | {asset field} |
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:
| Template.Choice | Moves/Splits/Merges/Archives Asset? | Reads Lock Field? | Lock Check Expr | Bypassable? |
|---|
{T.C} | YES/NO | YES/NO | assertMsg "locked" (not locked) / NONE | [DML-LK-N] if moves while locked |
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.
| Template.Choice | Recreates Asset Successor? | Carries locked Forward? | Erase Risk? |
|---|
{T.C} | YES/NO | YES/NO | [DML-LK-N] if successor unlocked |
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.
| Lock Choice | Unlock Choice | Value Locked | Value Returned On Unlock | Conserved? | Finding? |
|---|
{choice} | {choice} | {amount} | {amount} | YES/NO | [DML-LK-N] if mismatch |
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)
| Section | Required | Completed? | Notes |
|---|
| 1. Lock-State Inventory | IF lock pattern present | ✓/✗(N/A)/? | Every lock field/wrapper and protected asset |
| 2. Lock-Honoring Audit | IF lockable template present | ✓/✗(N/A)/? | Every value-moving choice reads the lock |
| 3. Lock-Erase Audit | IF lockable template present | ✓/✗(N/A)/? | Every successor carries lock forward |
| 4. Value-Conservation Across Lock/Unlock | IF lock+unlock cycle present | ✓/✗(N/A)/? | Lock/unlock value parity, no double-count |
