Problem summary

Any contract that inherits OpenZeppelin's Context (directly or through Ownable, ERC20, ERC721, etc.) relies on the internal function _msgSender() for access-control checks.
To verify that an authorised caller can execute a function without revert, we need to tell Certora that _msgSender() equals e.msg.sender.

Every attempt to add a CVL summary for _msgSender() fails with fatal errors, so the Prover cannot verify the positive (success) path – it can only prove that unauthorised callers revert.

Minimal reproduction

1. Solidity 0.8.29 contract PrizesWallet that inherits Ownable → Context.
2. CVL spec (essential parts):

methods {
  function game() external returns(address) envfree;
  function registerRoundEnd(uint256,address) external;
  function depositEth(uint256,address) external;

  // Any summary like the next line triggers an error
  // function Context._msgSender() internal with(env e) => e.msg.sender expect address;
}

rule gameCanDepositSuccess {
  env e; uint roundNum; address winner;
  require game() != 0;
  require e.msg.sender == game();
  require winner != 0;

  depositEth@withrevert(e, roundNum, winner);
  assert !lastReverted; // should pass, but always fails
}

3. Run with certoraRun (CLI 7.7.0, solc 0.8.29).
   *If the summary for _msgSender is omitted, the run finishes but the rule fails (lastReverted true).
   *If any summary is added, Certora terminates with compilation errors like:

Bad internal method returns: Cannot merge "Context._msgSender() returns (address)" and "Context._msgSender()" – different arities (1 vs 0)

or

Internal method `_msgSender()` is not declared in contract PrizesWallet, although it is defined in Context. Use the defining contract instead.

As a result _msgSender cannot be summarised and the positive path cannot be proved.

Approaches we tried

• Wildcard summary
  function _._msgSender() internal with(env e) => e.msg.sender;
  Rejected – wildcard entries cannot specify return types.

• Exact summary on defining contract
  function Context._msgSender() internal with(env e) => e.msg.sender expect address;
  Fails with "Bad internal method returns" – Certora detects an implementation with zero return values and cannot merge signatures.

• Exact summary on inheriting contract
  function PrizesWallet._msgSender() internal with(env e) => e.msg.sender expect address;
  Error: _msgSender not declared in PrizesWallet (it lives only in Context).

• DELETE summary then replacement summary
  Removes the method entirely; all calls revert, so success path remains unverifiable.

• Hooks, ghost variables, harness contract overriding _msgSender
  Solidity does not allow overriding non-virtual internal functions; hooks run after _msgSender already executed.

All attempts produce the same dead end.

Impact

Without the ability to summarise _msgSender, Certora cannot prove success scenarios for any contract that uses OpenZeppelin's Context pattern. That blocks verification of authorised-caller flows for most modern Solidity codebases.

Desired behaviour

Allow a CVL summary for an internal function inherited from another contract without running into signature/arity merge conflicts. Ideally, an entry such as

function Context._msgSender() internal with(env e) => e.msg.sender expect address;

should override or coexist with the implementation detected from bytecode so that success-path rules can be proved.