diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.conf b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.conf new file mode 100644 index 00000000..9c5c9649 --- /dev/null +++ b/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" +} \ No newline at end of file diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.sol b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.sol new file mode 100644 index 00000000..ba02615e --- /dev/null +++ b/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 { } +} \ No newline at end of file diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec new file mode 100644 index 00000000..69ea61d3 --- /dev/null +++ b/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; +} diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/README.md b/CVLByExample/Summarization/CalledContractAndExecutingContract/README.md new file mode 100644 index 00000000..6e010c79 --- /dev/null +++ b/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)