Proof: add delegatecall semantics to proof interpreter

[Th0rgal]

Summary

delegatecall exists as a first-class Expr in the CompilationModel and compiles to correct Yul, but has zero proof interpreter coverage. The interpreter feature matrix shows 0 proofs and 0 tests for delegatecall. This means proxy/upgradeable contracts compile but cannot be formally verified.

Previously tracked informally as gap #1420 in docs.

Current state

• Expr.delegatecall exists in Compiler/CompilationModel/Types.lean
• Yul codegen works in ExpressionCompile.lean
• Validation passes handle it
• --deny-proxy-upgradeability flag exists to block it when not wanted
• Proof interpreter: does not model delegatecall at all
• Foundry tests: basic smoke test only (ProxyUpgradeabilityMacroSmoke)

What delegatecall needs at the proof level

delegatecall has unique semantics that differ from call/staticcall:

• Executes callee's code in caller's storage context
• msg.sender and msg.value are preserved (not updated)
• Storage reads/writes affect the calling contract, not the target
• address(this) returns the caller's address, not the callee's

Proof model options

Option A: Context-switching oracle (minimal)

Model delegatecall as an oracle that can mutate the current contract's storage:

def delegatecallEffect (env : Env) (target : Address) (input : List Uint256) 
    (s : ContractState) : ContractResult Unit :=
  -- Oracle determines which storage slots change and to what values
  -- env.delegatecallOracle returns (success : Bool, storageChanges : List (Nat × Uint256))

This is the most pragmatic approach — it doesn't model the callee's code, but allows reasoning about what storage changes are possible.

Option B: Paired-contract simulation (full)

Model the callee as a function ContractState → ContractResult ContractState that operates on the caller's state. Requires the callee's spec to be available (connects to #1625 cross-contract specs).

Specific proof obligations

1. Storage context preservation: prove that delegatecall operates on the caller's storage, not a fresh state
2. msg.sender preservation: prove msg.sender is not updated during delegatecall
3. Revert rollback: prove that if delegatecall reverts, caller's storage is unchanged
4. Return data forwarding: prove returndatasize/returndatacopy reflect the callee's return

Definition of done

• Proof interpreter handles Expr.delegatecall (not just skips it)
• delegatecall has documented proof-level semantics (oracle-based or paired-contract)
• At least one theorem proven: delegatecall revert leaves caller storage unchanged
• At least one theorem proven: delegatecall preserves msg.sender
• Proxy smoke contract with initializer/reinitializer guards has proof coverage (not just compilation)
• Interpreter feature matrix updated: delegatecall row shows non-zero proof/test counts
• --trust-report accurately reflects what is proven vs assumed for delegatecall
• No new axioms beyond the delegatecall oracle interface assumption (if using Option A)

Related

• Connects to Specs: cross-contract invariant proofs via postcondition hypotheses + assume-guarantee interfaces #1625 (cross-contract specs) — Option B requires callee specs
• Related to --deny-proxy-upgradeability trust surface flag (already exists)
• EIP-1967 storage slot verification (future work, not in scope here)