external-precondition-audit

name	external-precondition-audit
description	Trigger Pattern Any external module interaction detected in attack_surface.md - Inject Into Breadth agents (merged via M5 hierarchy)

EXTERNAL_PRECONDITION_AUDIT Skill

Trigger Pattern: Any external module interaction detected in attack_surface.md Inject Into: Breadth agents (merged via M5 hierarchy) Constraint: Interface-level inference only -- no production fetch required

For every external module the protocol interacts with:

1. Interface-Level Requirement Inference

From the use imports and function calls to external modules, infer what the external module requires:

External Function Called	Module::Function	Parameters Passed	Likely Preconditions (from signature + abort codes)	Our Protocol Validates?

Inference method: Read the function signature, type parameters, ability constraints, and abort conditions. Example: coin::withdraw<CoinType>(account: &signer, amount: u64) -> infer that account must have sufficient balance, CoinType must be initialized, amount must be > 0. Check abort codes in framework source if available.

Aptos-specific patterns:

• &signer parameters: does external module require the signer to own a specific resource?
• Generic type parameters <T>: does external module require T to be registered/initialized?
• Object<T> parameters: does external module validate object ownership or type?
• Abort conditions: enumerate all assert! / abort in external function that could revert our call

2. Return Value Consumption

External Call	Return Type	How Protocol Uses Return	Failure Mode if Return Unexpected

For each return value:

• What happens if it returns 0? What happens if it returns MAX_U64?
• What happens if the external call aborts?
• For Option<T> returns: does our protocol handle none correctly?
• For FungibleAsset returns: is metadata validated after receiving?
• For Object<T> returns: is the object type verified before use?
• For each external data structure received (Vec, array, Map, list): (a) What ordering/uniqueness does the consuming code assume? (b) Does the external contract's spec guarantee that ordering? (c) What happens if the assumption is violated (unsorted, duplicates, gaps)?

3. State Dependency Mapping

Protocol State	Depends on External State	External Module Upgradeable?	State Can Change Without Our Knowledge?

For each dependency:

• Upgrade risk: Aptos modules are upgradeable by default (compatible policy). Can the external module add new abort conditions to a function we call? Can it change return value semantics within compatible upgrade bounds?
• Immutability check: Is the external module published as immutable? If so, behavior is frozen.
• State mutation timing: Can external module state change between our module's read and use within the same transaction? (e.g., another instruction in a multi-instruction transaction modifies external state)
• Framework dependency: If depending on aptos_framework modules, are there governance-controlled parameters that could change? (e.g., transaction_fee, staking_config)

Instantiation Parameters

{CONTRACTS}           -- List of modules to analyze
{EXTERNAL_MODULES}    -- External modules identified during recon
{FRAMEWORK_DEPS}      -- aptos_framework / aptos_std / aptos_token dependencies

Output Schema

For each finding:

## Finding [EP-N]: Title

**Verdict**: CONFIRMED / PARTIAL / REFUTED / CONTESTED
**Step Execution**: S1,S2,S3 | X(reasons) | ?(uncertain)
**Rules Applied**: [R1:Y, R4:Y, R8:Y]
**Severity**: Critical/High/Medium/Low/Info
**Location**: module::function (source_file.move:LineN)

**External Dependency**: {module::function}
**Failure Mode**: {what breaks}

**Description**: What's wrong
**Impact**: What can happen (abort DoS, wrong state, fund loss)
**Evidence**: Code showing dependency and missing validation

Step Execution Checklist

Section	Required	Completed?
1. Interface-Level Requirement Inference	YES	Y/N/?
2. Return Value Consumption	YES	Y/N/?
3. State Dependency Mapping	YES	Y/N/?