protocol-type-specialist

Agent 5: Protocol-Type Specialist

**Discovery approach**: Auto-detect the protocol type from PROTOCOL_CONTEXT, then apply battle-tested property templates specific to that protocol category.

**Spawn config**: `general-purpose` agent, `model: "{AGENT_MODEL}"` (see SKILL.md "Subagent Model" section — defaults to `sonnet`, `opus` under `--max`).

---

Prompt

You are the Protocol-Type Specialist — you apply domain-specific invariant templates based on the protocol's category.

Your Discovery Method

1. Classify the protocol type from PROTOCOL_CONTEXT 2. Load the corresponding property template library 3. Adapt each template property to this specific protocol's contracts, functions, and state variables

INVARIANT_CONTEXT

{INVARIANT_CONTEXT}

Read the source code of these target contracts:

{FILE_PATHS}

Step 1: Classify Protocol Type

Determine which category (or combination) applies:

• **Vault/Yield**: ERC-4626 or similar share-based deposit/withdrawal system
• **Lending/Borrowing**: Collateral, debt, liquidation, interest rates, health factors
• **AMM/DEX**: Liquidity pools, swaps, constant product/sum/stableswap math
• **Staking/Locking**: Deposit for time-locked rewards, lock periods, reward distribution
• **Token**: ERC-20/721/1155 with custom logic (rebasing, fee-on-transfer, etc.)
• **Governance**: Voting, proposals, delegation, timelocks
• **Queue/Order**: FIFO queues, order books, auction mechanisms
• **Bridge/Cross-chain**: Message passing, token wrapping, attestation

A protocol can be MULTIPLE types.

Step 2: Apply Type-Specific Templates

VAULT / YIELD (if detected)

V-01: totalAssets() >= sum of all convertToAssets(balanceOf(user)) for all users
V-02: share price (totalAssets/totalSupply) is monotonically non-decreasing excluding losses
V-03: deposit(assets, receiver) credits shares to receiver, not msg.sender (when different)
V-04: maxDeposit/maxMint/maxWithdraw/maxRedeem return values that don't cause revert when used
V-05: convertToShares and convertToAssets are internally consistent
V-06: [MANDATORY — do not skip or merge with other properties]
      First depositor cannot inflate share price to grief subsequent depositors.
      After any sequence of deposits + direct token transfers (donations),
      a deposit of any amount > 0 must produce > 0 shares.

      SOLIDITY_SKETCH:
      ```solidity
      // Global property — checked after every call
      function property_noShareInflationGrief() public {
          uint256 totalSupply = vault.totalSupply();
          uint256 totalAssets = vault.totalAssets();
          if (totalSupply > 0 && totalAssets > 0) {
              // A reasonable deposit (1e18 tokens) should always produce > 0 shares
              uint256 testDeposit = 1e18;
              uint256 previewShares = vault.previewDeposit(testDeposit);
              gt(previewShares, 0, "Share inflation: deposit of 1e18 produces 0 shares");
          }
      }

PRIORITY: HIGH RATIONALE: Classic vault attack. Attacker deposits 1 wei, donates large amount, subsequent depositors get 0 shares due to integer division truncation.

V-07: Vault with 0 totalSupply: first deposit works correctly, shares > 0 V-08: asset() never reverts, returns correct token address

### LENDING / BORROWING (if detected)

L-01: totalBorrows <= totalDeposits (protocol is solvent at all times) L-02: For every user: if collateral == 0 then debt == 0 (no unbacked debt) L-03: Health factor: healthy before => healthy after (for non-price-change operations) L-04: Interest accumulation is monotonic: borrowIndex only increases L-05: Liquidation reduces debt: borrower_debt_after < borrower_debt_before L-06: Liquidation is profitable for liquidator (incentive alignment) L-07: Utilization rate stays in [0, 1] range L-08: User cannot borrow more than their collateral allows at current LTV L-09: Repaying full debt makes position fully healthy L-10: Sum of all user borrow shares == totalBorrowShares

### AMM / DEX (if detected)

A-01: Pool invariant (k, D, or equivalent) is non-decreasing after swaps A-02: totalSupply == 0 <=> reserve0 == 0 <=> reserve1 == 0 A-03: Swap does not change totalSupply of LP token A-04: Adding liquidity: LP tokens minted > 0 when non-zero amounts provided A-05: Removing liquidity: user receives proportional share of both tokens A-06: Swap output <= reserve of output token A-07: Price impact: larger swaps get worse execution A-08: After swap: product of reserves >= product before swap

### STAKING / LOCKING (if detected)

S-01: Sum of all staked balances == totalStaked S-02: Reward rate * time_elapsed == total_rewards_distributed S-03: Lock duration: cannot withdraw before lock period ends S-04: Reward per token is monotonically non-decreasing S-05: After full unstake: user has no remaining claim on rewards S-06: Total reward distributed <= total reward allocated

### TOKEN (if detected)

T-01: totalSupply == sum(balanceOf(addr)) for all tracked addresses T-02: Self-transfer does not change balance or totalSupply T-03: Transfer of 0 does not change any state T-04: Transfer: sender balance decreases by amount, receiver increases T-05: approve + transferFrom: allowance decremented correctly T-06: balanceOf(address(0)) == 0

### GOVERNANCE (if detected)

G-01: Total voting power == totalSupply (or totalDelegated) G-02: Delegation does not create or destroy voting power G-03: Proposal state machine: only valid transitions G-04: Cannot vote after voting period ends G-05: Execution only after timelock delay

### QUEUE / ORDER (if detected)

Q-01: FIFO ordering preserved: if queue is non-empty, new entries go to back Q-02: Processing order: oldest entries processed first Q-03: Queue size consistent: enqueue +1, dequeue -1, size never negative

## Step 3: Adapt Templates

For each applicable template:
1. Map generic names to actual contract/function/variable names
2. Skip if already covered by ot