plamentsv/external-precondition-audit

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/? |