Support external calls with return values (staticcall/call) in EDSL

[Th0rgal]

Summary

The EDSL needs a way to express side-effecting external contract calls that return values. Currently externalCall is a pure function (stub returns 0) — it captures the call in the IR model but the executable path cannot use the return value.

Use cases in Morpho Blue

1. Oracle price query: IOracle(marketParams.oracle).price() → returns uint256 collateralPrice

   • Used by _isHealthy() for health checks in borrow, withdrawCollateral, liquidate
   • This is the single biggest semantic gap: without it, health checks cannot be expressed

2. IRM borrow rate: IIrm(marketParams.irm).borrowRate(marketParams, market[id]) → returns uint256 borrowRate

   • Used by _accrueInterest() for interest computation
   • Currently modeled as externalCall "borrowRate" [...] which captures the call but returns 0

3. ERC20 transfers: IERC20(token).safeTransferFrom(sender, recipient, amount)

   • Every function that moves tokens needs this
   • Requires call with calldata encoding and return value checking

Proposed EDSL syntax

-- staticcall: read-only external call returning a value
let price <- staticCall oracle "price" []

-- call: state-modifying external call
call token "transfer" [receiver, amount]

-- call with return value check (safeTransfer pattern)
let success <- call token "transfer" [receiver, amount]
require (success != 0) "transfer failed"

Layer 2 proof model

External calls should be modeled with callee-assumption hypotheses:

• The theorem states "assuming the oracle returns price P, the contract state transitions correctly"
• The proof doesn't need to verify the callee's behavior, only the caller's response to it

Impact

Without this feature, morpho-verity cannot express:

• Health checks (borrow, withdrawCollateral, liquidate) — critical security invariants
• Token transfers — full functional parity
• IRM calls with actual return values

Related

• Specs: cross-contract invariant proofs via postcondition hypotheses + assume-guarantee interfaces #1625 (cross-contract invariant proofs) — broader scope
• Proof: add delegatecall semantics to proof interpreter #1627 (delegatecall semantics) — related low-level call support