Support internal function composition in verity_contract macro

[Th0rgal]

Summary

The verity_contract macro treats each function as an independent selector — there is no way to call one function from another. Morpho Blue's Solidity uses _accrueInterest(marketParams, id) as a shared internal called from 7 external functions (supply, withdraw, borrow, repay, setFee, withdrawCollateral, liquidate).

Current workaround

Each EDSL function assumes interest has already been accrued. This creates a semantic gap vs Solidity where supply() atomically accrues interest then supplies.

The only alternative is inlining _accrueInterest into all 7 functions (~20 lines each), which is error-prone and bloats the EDSL.

Proposed solution

Allow verity_contract to define internal functions that can be called from other functions:

verity_contract MyContract where
  storage ...

  internal function _accrueInterest (marketParams : ..., id : Uint256) : Unit := do
    ...

  function supply (...) : Unit := do
    _accrueInterest marketParams id
    ...

The macro would inline the internal function body at each call site for IR generation. For the executable Contract monad path, it would generate a regular Lean function call.

Impact

• morpho-verity: 7 functions currently omit _accrueInterest call, creating the largest semantic gap vs Solidity
• General: Any contract with shared internal logic (modifiers, health checks, etc.)

Related

• Extend verity_contract macro: struct-typed packed storage, internal functions, mutable locals #1003 (closed) listed this as "Batch 1" but was closed before implementation
• The internalCall expression exists in the macro but has no Layer 2 proof semantics