메뉴
Trigger Pattern Always required for DAML audits - Inject Into Breadth agents, depth-state-trace, depth-edge-case
기본적으로 소스를 먼저 확인하는 Prompt가 선택됩니다. 직접 명령으로 전환하거나 로컬 사본을 다운로드할 수도 있습니다.
설치 여부를 결정하기 전에 SKILL.md와 SkillsMP에 표시된 보조 파일을 읽어 보세요.
SOC 직업 분류 기준
Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.
직접 명령은 검토 Prompt를 거치지 않습니다. 실행하기 전에 소스를 확인하세요.
npx skills add https://github.com/PlamenTSV/plamen --skill choice-semantics명령은 한 줄로 유지됩니다. 복사하기 전에 가로로 스크롤해 전체 내용을 확인하세요.
로컬 사본을 원하시나요? SkillsMP에서 현재 제공할 수 있는 파일을 다운로드하세요.
SKILL.md 표시 중
Trigger Pattern Always (run during recon TASK 0, not breadth) - Inject Into Recon agent only (meta_buffer.md enrichment)
Trigger Pattern Always (run during recon TASK 0, not breadth) - Inject Into Recon agent only (meta_buffer.md enrichment)
Trigger STABLESWAP_FORK flag (fork-ancestry detects Curve/StableSwap parent via get_d/get_y/ramp_a/StableSwap patterns) - Agent Type general-purpose (standalone niche agent, 1 budget slot)
| name | choice-semantics |
| description | Trigger Pattern Always required for DAML audits - Inject Into Breadth agents, depth-state-trace, depth-edge-case |
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.
For EVERY choice, record its consume-mode and whether the action should be one-shot:
| Template.Choice | Consume-Mode | Moves Value / Mutates State? | Should Be One-Shot? | Mismatch? |
|---|---|---|---|---|
{T.C} | consuming/nonconsuming/preconsuming/postconsuming | YES/NO | YES/NO | [DML-CHS-N] if nonconsuming + should-be-one-shot |
Critical patterns to flag:
nonconsuming choice that transfers, mints, splits, or withdraws value → exercisable repeatedly on the same active contract (, double-spend).[ELEVATE:NONCONSUMING_REPLAY]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).
preconsuming archives BEFORE the body runs; postconsuming archives AFTER. A body that fetches self (or this via key) behaves differently across the two.
| Template.Choice | Consume-Mode | Body Self-Fetch / Self-Exercise? | Reads Pre-Archive State? | Finding? |
|---|---|---|---|---|
{T.C} | pre/postconsuming | YES/NO | YES/NO | [DML-CHS-N] if ordering-dependent |
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.
Each value-moving choice should produce successor contracts that conserve value and carry forward every invariant field.
| Template.Choice | Inputs (contracts/amounts) | Outputs Created | Conservation Check | Fields Carried Forward | Gap? |
|---|---|---|---|---|---|
{T.C} | {in} | {out} | out1.amt + out2.amt == in.amt? | owner/lock/maintainer | [DML-CHS-N] if value created/destroyed or field dropped |
Check for:
locked, owner, or maintainer field present in the predecessor (metadata/lock erase).totalIssued, mintedSoFar) that is NOT updated on the create path, so the cap is never enforced across transactions ([ELEVATE:VALUE_CONSERVATION], R14).A choice that allocates or locks resources must unwind them on the cancel/abort/reject path.
| Template.Choice | Allocates/Locks On Success | Cancel/Reject Choice Exists? | Unwinds Allocation? | Finding? |
|---|---|---|---|---|
{T.C} | {child created / asset locked} | YES/NO | YES/NO | [DML-CHS-N] if no unwind |
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.
**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.
| Section | Required | Completed? | Notes |
|---|---|---|---|
| 1. Consume-Mode Inventory | YES | ✓/✗/? | Every choice, value-movers especially |
| 2. Pre/Postconsuming Ordering Trace | IF pre/postconsuming present | ✓/✗(N/A)/? | Every self-fetch/self-exercise |
| 3. Successor-State Completeness | YES | ✓/✗/? | Every split/merge/transfer + accumulator |
| 4. Cancel / Abort Unwind | IF allocate/lock-then-cancel pattern | ✓/✗(N/A)/? | Every reserve/propose with a cancel path |