linked_contracts bindings are declarative only: bound calls still elaborate to the adversary oracle, callee bodies never run

Found while translating the Pareto Credit Vault (IdleCDOEpochVariant ↔ IdleCreditVault) into verity_contract sources on top of #2413 (c907fef0).

What the design note promises

docs/PARETO_MODEL_SUPPORT.md, Feature 2: "A bound call is a CALL-shaped hop in Verity.MultiContract.MultiWorld ... run the callee body against the callee account; success commits callee storage and journals the caller; revert restores the pre-call world and bubbles."

What the macro generates

linked_contracts bindings are parsed, validated (duplicate names, unknown interface/callee) and stored on the parsed contract, but no code path consumes them afterwards (grep -n linkedContracts Verity/Macro/Translate.lean shows only the parse/merge sites). The executable definition of a bound call is the same adversary-oracle stub as an unbound interface call:

import Contracts.Smoke.ModeledCall
open Contracts.Smoke
#print ModeledCaller.record
-- def Contracts.Smoke.ModeledCaller.record : Verity.Address → Verity.Contract Verity.Uint256 :=
-- fun token => do
--   let v ← Contracts.externalStaticCallContractWordsTo "ICallee.get" token [].flatten
--   Verity.setStorage ModeledCaller.last v
--   pure v
#print ModeledCaller.ping
-- ModeledCaller.ping : Contracts.ExecutableCallContext → Verity.Address → Verity.Uint256 → Verity.Contract Unit

ModeledCallee.get's body is never executed by the caller; hopContract/hopContractView exist in Verity/Core/Model/ModeledCall.lean but nothing generated uses them. The smoke test Contracts/Smoke/ModeledCall.lean builds the CallFrame by hand.

Why it matters

For Pareto, ~40 vault→strategy calls and ~12 strategy→vault reads must execute the modeled bodies in one evolving world (rollback lemmas such as "the late safeTransferFrom failure in finalizeDefaultRecovery restores the CDO skim" are statements about the composed execution). With the current plane, every cross-contract lemma has to be written against a hand-written combined-world model outside the macro. Bindings also cannot be cyclic (the callee must be declared first), so the vault↔strategy pair can only be bound in one direction.

Ask

Either wire the executable plane of a bound call to the callee body (a MultiWorld-aware executable, or a same-ContractState namespaced hop via StorageKey.contractSlot), or state explicitly in docs/PARETO_MODEL_SUPPORT.md and TRUST_ASSUMPTIONS.md §6b that linked_contracts is declarative only and that modeled-callee semantics require manual hopContract composition.

Closure-side tracking: audit/VERITY-GAPS.md G1/G15 in lfglabs-dev/pareto-credit-vault-proof-closure.

Start with docs/PARETO_MODEL_SUPPORT.md Feature 2 and inspect Verity/Macro/Translate.lean, especially the linkedContracts parse/merge sites, then compare the generated calls with Verity/Core/Model/ModeledCall.lean and Contracts/Smoke/ModeledCall.lean. Done means bound calls either execute modeled callee bodies with the required evolving-world and rollback semantics, or the declarative-only limitation is documented in the named trust documents.