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