Called Contract and Executing Contract Example

CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "CalledContractAndExecutingContract.sol:Primary",
+        "CalledContractAndExecutingContract.sol:Secondary",
+        "CalledContractAndExecutingContract.sol:Tertiary"
+    ],
+    "link": [
+        "Primary:secondary=Secondary",
+        "Primary:tertiary=Tertiary"
+    ],
+    "verify": "Primary:CalledContractAndExecutingContract.spec"
+}

CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.sol

@@ -0,0 +1,103 @@
+// There are two contracts `Primary` and `Secondary` and a library `Library`.
+// Each has a `calleeInternal` and a `calleeExternal` function (these are
+// summarized in CalledContractAndExecutingContract.spec).  There are else several unsummarized `call...`
+// entry points; each is used in a rule in `CalledContractAndExecutingContract.spec`.
+
+contract Primary {
+
+    Secondary secondary;
+    Tertiary tertiary;
+
+    // callee functions are summarized
+
+    function calleeInternal() internal { }
+    function calleeExternal() external { }
+
+    // call functions are unsummarized; each corresponds to an example
+
+    function callPrimaryInternal() external {
+        calleeInternal();
+    }
+
+    function callSecondaryInternal() external {
+        secondary.callSecondaryInternal();
+    }
+
+    function callPrimaryExternal() external {
+        this.calleeExternal();
+    }
+
+    function callSecondaryExternal() external {
+        secondary.calleeExternal();
+    }
+
+    function callPrimaryExternalFromSecondary() external {
+        secondary.callPrimaryExternal(this);
+    }
+
+    function callLibraryInternalFromPrimary() external {
+        Library.calleeInternal();
+    }
+
+    function callLibraryExternalFromPrimary() external {
+        Library.calleeExternal();
+    }
+
+    function callLibraryInternalFromSecondary() external {
+        secondary.callLibraryInternal();
+    }
+
+    function callLibraryExternalFromSecondary() external {
+        secondary.callLibraryExternal();
+    }
+
+    function callTertiaryThroughSecondary() external {
+        secondary.callTertiaryExternal(tertiary);
+    }
+
+    function callSecondaryExternalViaDelegate() external {
+        address(secondary).delegatecall(abi.encodeWithSignature("calleeExternal()"));
+    }
+}
+
+
+contract Secondary {
+    // the `callee` methods are summarized
+
+    function calleeExternal() external { }
+    function calleeInternal() internal { }
+
+    // the `call` methods are used to dispatch to the callee methods
+
+    function callPrimaryExternal(Primary receiver) external {
+        receiver.calleeExternal();
+    }
+
+    function callSecondaryInternal() external {
+        calleeInternal();
+    }
+
+    function callLibraryInternal() external {
+        Library.calleeInternal();
+    }
+
+    function callLibraryExternal() external {
+        Library.calleeExternal();
+    }
+
+    function callTertiaryExternal(Tertiary receiver) external {
+        receiver.calleeExternal();
+    }
+}
+
+library Library {
+    function calleeExternal() external { }
+    function calleeInternal() internal { }
+}
+
+contract Tertiary {
+    // the `callee` methods are summarized
+
+    function calleeExternal() external { }
+    function calleeInternal() internal { }
+}

CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec

@@ -0,0 +1,136 @@
+// There are two contracts `Primary` and `Secondary` and a library `Library`,
+// each having a (summarized) `calleeInternal` and a `calleeExternal` method.
+// The contracts also have several `call` methods that call the different callee
+// methods from different callers.
+//
+// The summaries for all the `callee` methods save several values in ghosts:
+// * `calledContract` in the `called` ghost.
+// * `executingContract` in the `executing` ghost.
+// * `e.msg.sender` in the `sender` ghost.
+// the rules then check that all ghosts are updated correctly.
+// All assertions should pass.
+
+
+using Primary   as primary;
+using Secondary as secondary;
+using Tertiary  as tertiary;
+
+methods {
+    function _.calleeInternal() internal with (env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void;
+    function _.calleeExternal() external with (env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void ALL;
+}
+
+ghost address called;
+ghost address executing;
+ghost address sender;
+
+function saveContracts(address _called, address _executing, address _sender) {
+    called = _called;
+    executing = _executing;
+    sender = _sender;
+}
+
+rule primaryInternal(env e) {
+    callPrimaryInternal(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+
+rule secondaryInternal(env e) {
+    callSecondaryInternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == primary;
+}
+
+rule primaryExternal(env e) {
+    callPrimaryExternal(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == primary;
+}
+
+rule secondaryExternal(env e) {
+    callSecondaryExternal(e);
+    assert called == secondary;
+    assert executing == primary;
+    assert sender == primary;
+}
+
+rule primaryExternalFromSecondary(env e) {
+    callPrimaryExternalFromSecondary(e);
+    assert called == primary;
+    assert executing == secondary;
+    assert sender == secondary;
+}
+
+rule libraryInternalFromPrimary(env e) {
+    callLibraryInternalFromPrimary(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+
+rule libraryExternalFromPrimary(env e) {
+    callLibraryExternalFromPrimary(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+
+rule libraryInternalFromSecondary(env e) {
+    callLibraryInternalFromSecondary(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == primary;
+}
+
+rule libraryExternalFromSecondary(env e) {
+    callLibraryExternalFromSecondary(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == primary;
+}
+
+rule secondaryToPrimaryFromSpec(env e) {
+    secondary.callPrimaryExternal(e,primary);
+    assert called == primary;
+    assert executing == secondary;
+    assert sender == secondary;
+}
+
+rule secondaryToSecondaryFromSpec(env e) {
+    secondary.callSecondaryInternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == e.msg.sender;
+}
+
+rule secondaryToLibraryInternalFromSpec(env e) {
+    secondary.callLibraryInternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == e.msg.sender;
+}
+
+rule secondaryToLibraryExternalFromSpec(env e) {
+    secondary.callLibraryExternal(e);
+    assert called == secondary;
+    assert executing == secondary;
+    assert sender == e.msg.sender;
+}
+
+rule tertiaryThroughSecondary(env e) {
+    callTertiaryThroughSecondary(e);
+    assert called == tertiary;
+    assert executing == secondary;
+    assert sender == secondary;
+}
+
+rule secondaryExternalViaDelegateFromPrimary(env e) {
+    callSecondaryExternalViaDelegate(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}

CVLByExample/Summarization/CalledContractAndExecutingContract/README.md

@@ -0,0 +1,109 @@
+# Using `calledContract` and `executingContract` in Summaries
+
+This directory demonstrates how to use two CVL keywords—`calledContract` and `executingContract`—to track function call details within a summary context. The repository contains:
+
+1. A Solidity file, **`CalledContractAndExecutingContract.sol`**, which defines contracts **`Primary`**, **`Secondary`**, and **`Tertiary`**, as well as a **`Library`**.  
+2. A CVL spec file, **`CalledContractAndExecutingContract.spec`**, which verifies rules about contract function calls and how the two new keywords behave under different call types.
+
+## 1. Solidity File Overview
+
+The file **`CalledContractAndExecutingContract.sol`** declares three contracts (`Primary`, `Secondary`, `Tertiary`) and one library (`Library`). Each contract has two “callee” functions:
+
+- `calleeInternal()` – an internal function  
+- `calleeExternal()` – an external function  
+
+In addition, `Primary` and `Secondary` implement various "call" functions that invoke these callee functions in different ways:
+
+1. **Calls within the same contract** (e.g., `Primary` calling its own internal method).  
+2. **Calls to another contract** (e.g., `Primary` calling an external method on `Secondary`).  
+3. **Calls from one contract to another that in turn calls back** (e.g., `Secondary` calling `Primary` again).  
+4. **Library calls**, both internal and external (e.g., `Library.calleeInternal()` from within `Primary` or `Secondary`).  
+5. **Delegate calls**, where `Primary` uses `delegatecall` to call `Secondary`'s external function, ensuring the code runs in `Secondary` but uses `Primary`'s storage context.  
+
+These different invocation patterns let us test when and how `calledContract` and `executingContract` diverge.
+
+## 2. CVL Specification Overview
+
+The **`CalledContractAndExecutingContract.spec`** file does two key things:
+
+1. **Summaries**: Inside the `methods` block, it summarizes every `calleeInternal` and `calleeExternal` function (for all contracts and the library) by calling a helper function, `saveContracts`, which writes into ghost variables `called`, `executing`, and `sender`.
+2. **Rules**: A series of rules each perform a high-level call (e.g., `callPrimaryInternal`, `callSecondaryExternal`, etc.) from the `Primary` contract, and then assert that the ghost variables hold the correct addresses for the **called contract**, the **executing contract**, and the **sender**.  
+
+### 2.1 Summaries (Using `calledContract` and `executingContract`)
+
+In the `methods` block, the specification shows how to attach a summary to an internal or external function:
+
+```solidity
+methods {
+    function _.calleeInternal() internal with (env e)
+        => saveContracts(calledContract, executingContract, e.msg.sender)
+        expect void;
+
+    function _.calleeExternal() external with (env e)
+        => saveContracts(calledContract, executingContract, e.msg.sender)
+        expect void ALL;
+}
+```
+
+Here:
+- **`calledContract`** is the address of the contract on which the summarized function was called.
+- **`executingContract`** is the address of the contract that is actually running the function code.  
+- **`e.msg.sender`** is the caller’s address as specified in the test environment.
+
+These three values are passed to `saveContracts`, which stores them in ghost variables `called`, `executing`, and `sender`:
+
+```solidity
+ghost address called;
+ghost address executing;
+ghost address sender;
+
+function saveContracts(address _called, address _executing, address _sender) {
+    called = _called;
+    executing = _executing;
+    sender = _sender;
+}
+```
+
+By capturing these addresses as ghost variables, we can write rules that check whether the correct caller/callee relationship is preserved.
+
+### 2.2 Rules
+
+Each rule (e.g., `rule primaryInternal(env e)`) performs a specific contract call (like `callPrimaryInternal`) and then checks the ghost variables. For instance:
+
+```solidity
+rule primaryInternal(env e) {
+    callPrimaryInternal(e);
+    assert called == primary;
+    assert executing == primary;
+    assert sender == e.msg.sender;
+}
+```
+
+- We make a call to `callPrimaryInternal`.
+- Internally, this triggers `calleeInternal` on the same contract (`Primary`), setting `called = primary`, `executing = primary`, and `sender = e.msg.sender`.
+- The rule then **asserts** that these ghost variables match the expected values.
+
+By comparing `called`, `executing`, and `sender` in each rule, we ensure that **internal calls**, **external calls**, **delegate calls**, and **library calls** update the ghosts consistently with how the EVM actually routes the call.
+
+## 3. Behavior of `calledContract` and `executingContract`
+
+### `calledContract`
+- Represents the address of the contract on which the summarized method was called, or more precisely in whose context it runs. It is essentially `address(this)` in the context of the original call you are summarizing.
+- For **internal calls**, and non-delegate **external calls** `calledContract` is the same as the contract containing the function.
+- For **library calls** and **delegate calls**, `calledContract` is the contract *initiating* the code execution (since libraries and delegate calls run in the caller’s context).
+
+### `executingContract`
+- Represents the address of the contract that *initiated the call*.
+- For **internal** and **delegate** calls, this will be the same as `calledContract`.
+- For **external** calls, it will be the address of the caller, while `calledContract` is the address of the receiver.
+
+### Additional Notes on the Keywords
+- They are not arbitrary variables that can be combined or manipulated further. You can only pass them into your summary function (e.g., `saveContracts`) or reference them directly in your specification.  
+
+## 4. Run the Example
+To run the example use:
+```
+certoraRun CalledContractAndExecutingContract.conf
+```
+
+[The report of this run](https://prover.certora.com/output/15800/c768f4f7ac724e2db90104a412b7a89b?anonymousKey=2c30fbec58b46141e53e0d2d1693b8b6dab00e27)