Interface-typed storage fields are rejected (design note promises them); no address-to-interface cast for storage-held callees

[Th0rgal]

docs/PARETO_MODEL_SUPPORT.md (Feature 2) says the linked_contracts name "may also match an interface-typed storage field or parameter". Interface-typed storage fields are rejected:

verity_contract IfaceField where
  storage
    strategy : IStrategy := slot 0
  interfaces
    interface IStrategy where
      function getApr() view returns (Uint256)
    end
  function read () : Uint256 := do
    let v ← strategy.getApr
    return v
-- error: unsupported type 'IStrategy'; expected a built-in type or a user-defined enum, struct, newtype, or inductive type

There is also no way to attach an interface to an address read from storage (interfaceNameOfTerm? only propagates from parameters/locals that already carry one), so every Solidity IdleCreditVault(strategy).f(...) on a storage-held address needs a thin internal helper with an interface-typed parameter:

function internal _strategyGetApr (_s : IIdleCreditVault) : Uint256 := do
  let apr ← _s.getApr
  return apr
function internal _getStrategyApr () : Uint256 := do
  let _strategy ← getStorageAddr strategy
  let apr ← _strategyGetApr _strategy
  return apr

Pareto needs ~35 such wrappers (vault→strategy, vault→tranche tokens, strategy→vault, both→underlying token), which is the single largest source of noise in the translation.

Ask: accept field : IFace := slot n as an address field tagged with the interface (and let linked_contracts bind it), or provide a cast form such as let s : IFace := addr / (IFace addr) for locals.

Closure-side tracking: audit/VERITY-GAPS.md G5.