diff --git a/.circleci/config.yml b/.circleci/config.yml index 4fc7b72e..edd10bcc 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -69,7 +69,7 @@ jobs: check-release: docker: - - image: &img public.ecr.aws/certora/cvt-image:2024.06.13-3755-0351582 + - image: &cvt public.ecr.aws/certora/cvt-image:2024.10.16-4473-ba570af resource_class: small working_directory: ~/repo steps: @@ -116,7 +116,7 @@ jobs: type: string default: "" docker: - - image: &img public.ecr.aws/certora/cvt-image:2024.06.13-3755-0351582 + - image: *cvt resource_class: small working_directory: ~/repo environment: @@ -162,7 +162,7 @@ jobs: certora_cli_package: type: string docker: - - image: &img public.ecr.aws/certora/cvt-image:2024.06.13-3755-0351582 + - image: *cvt resource_class: small working_directory: ~/repo steps: @@ -183,7 +183,6 @@ jobs: path: ~/repo - parameters: run_regtest: default: false diff --git a/CVLByExample/README.md b/CVLByExample/README.md index 0570a367..19596221 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -44,6 +44,7 @@ | **ContractAlias** | [example](https://github.com/Certora/Examples/blob/42395eb745d20c40c14f297fd28b3a658f87f889/CVLByExample/ContractAlias/ContractAlias.spec#L1-L3) | | **StoreToArray** | [example](https://github.com/Certora/Examples/blob/niv/CERT-6524/CVLByExample/Types/StoreToArray/StoreToArray.spec#L4) | | **HookOnResetStorageCommand** | [example](https://github.com/Certora/Examples/blob/niv/CERT-7022-Add-Hook-On-Reset-Storage-Example/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec#L1-L10) | +| **RevertKeyWord** | [example](https://github.com/Certora/Examples/blob/niv/CERT-8248-Revert-Example/CVLByExample/RevertKeyWord/example.spec#L13) | diff --git a/CVLByExample/RevertKeyWord/C.sol b/CVLByExample/RevertKeyWord/C.sol new file mode 100644 index 00000000..fad61a85 --- /dev/null +++ b/CVLByExample/RevertKeyWord/C.sol @@ -0,0 +1,49 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +/** + * @title C + * @dev A simple contract demonstrating functions that can revert + */ +contract C { + bool public fooWasCalled; + + /** + * @notice Sets fooWasCalled and reverts if the input b is false + */ + function foo(bool b) external { + fooWasCalled = true; + if (!b) { + revert("foo reverted"); + } + } + + /** + * @notice Calls foo and can therefore revert if foo reverts + */ + function callFooFromContract(bool b) external { + this.foo(b); + } + + /** + * @notice Dummy function that can be used to demonstrate "summary" usage + */ + function summarizeMe(bool b) external {} + + /** + * @notice Returns b or reverts if b is false + */ + function canRevert(bool b) external returns (bool) { + if (!b) { + revert("canRevert reverted"); + } + return b; + } + + /** + * @notice Calls summarizeMe and can be used for demonstration of deeper calls + */ + function callSummarizeMe(bool b) external { + this.summarizeMe(b); + } +} diff --git a/CVLByExample/RevertKeyWord/README.md b/CVLByExample/RevertKeyWord/README.md new file mode 100644 index 00000000..47363c65 --- /dev/null +++ b/CVLByExample/RevertKeyWord/README.md @@ -0,0 +1,49 @@ +# CVL Revert Feature Example + +This folder demonstrates the newly introduced **CVL revert functionality** and the **`@withrevert`** annotation. These features allow you to: + +1. **Explicitly revert** inside CVL functions (e.g. `revert("some reason")`). +2. **Capture revert signals** when calling any function—Solidity or CVL—using the `@withrevert` annotation, which sets the built-in CVL variable `lastReverted` to `true` if a revert occurs. + +## Files + +1. **`C.sol`** + A simple Solidity contract with functions that may revert. The contract contains: + - `foo(bool b)`: sets a flag and reverts if `b` is false. + - `canRevert(bool b)`: returns `b` or reverts if `b` is false. + - `summarizeMe(bool b)`: a dummy function, used for demonstrating a CVL summary that can also revert. + - `callSummarizeMe(bool b)`: calls `summarizeMe`; used to show how reverts in a summary can bubble up. + - Additional helper functions like `callFooFromContract`. + +2. **`example.spec`** + A CVL spec demonstrating: + - Calling a Solidity function with `@withrevert`, e.g. `foo@withrevert(b)`. + - Writing a CVL function (`cvlFunctionThatMayRevert`) that explicitly reverts when a condition fails. + - Two different ways to handle potential reverts from `canRevert(bool)`, illustrating how revert can either be captured inline or bubble up through a CVL wrapper. + - A **“summarize”** function, `cvlSummarizeMe`, that can revert if its boolean parameter is false, invoked via the contract function `callSummarizeMe@withrevert(b)`. + +## Usage + +1. **Command** + ```shell + certoraRun example.conf --server production --prover_version master + ``` +2. **Expected Output** + - The output should confirm that the spec passes, with the expected behavior of `lastReverted` in each case. + - Link: [Example Output](https://prover.certora.com/output/1512/3919ff99f4e84203a04e4aeab4fc8c11?anonymousKey=3a7682aefc6e9b26f248f7fc7a1aff60557281cf) + +3. **Examine the Rules** + - **`testFooWithRevert`** + Confirms that calling `foo` with `@withrevert` sets `lastReverted` exactly when the argument is false. + - **`testCvlFunctionWithRevert`** + Demonstrates how a CVL function (`cvlFunctionThatMayRevert`) can explicitly revert, and how `@withrevert` captures that. + - **`testCanRevertInline`** + Uses `wrapperForCanRevertInline(bool)`, which internally calls `canRevert@withrevert(condition)`, returning `lastReverted`. + - **`testCanRevertBubbleUp`** + Illustrates revert **bubbling up**. In `wrapperForCanRevertBubble(bool)`, we call `canRevert(condition)` *without* `@withrevert`, but then call the wrapper itself with `@withrevert`. The internal revert propagates, setting `lastReverted`. + - **`testCallSummarizeMe`** + Demonstrates a contract function (`callSummarizeMe`) that calls a **CVL summary** (`cvlSummarizeMe`). If the summary reverts (when the boolean input is false), the revert bubbles up to the contract caller, setting `lastReverted`. + +## Conclusion + +With these files (`C.sol`, `example.spec`, `Example.conf`, and this `README.md`), you can see how the new CVL revert feature works in practice. By enabling the `-cvlFunctionRevert` flag, you can write more expressive and accurate specs that treat reverts in CVL and Solidity calls consistently, capturing those reverts in **`lastReverted`** for precise modeling in your verification. The **bubble-up** behavior especially highlights how deeper CVL calls (including **summaries**) can now propagate reverts just like Solidity calls. diff --git a/CVLByExample/RevertKeyWord/example.conf b/CVLByExample/RevertKeyWord/example.conf new file mode 100644 index 00000000..6a697400 --- /dev/null +++ b/CVLByExample/RevertKeyWord/example.conf @@ -0,0 +1,13 @@ +{ + "files": [ + "C.sol" + ], + "independent_satisfy": true, + "process": "emv", + "solc": "solc8.26", + "verify": "C:example.spec", + "prover_args": [ + "-cvlFunctionRevert true" + ], + "rule_sanity": "basic" +} diff --git a/CVLByExample/RevertKeyWord/example.spec b/CVLByExample/RevertKeyWord/example.spec new file mode 100644 index 00000000..a6a1f9bf --- /dev/null +++ b/CVLByExample/RevertKeyWord/example.spec @@ -0,0 +1,109 @@ +// --------------------------------------------------------- +// 1. Declare the contract methods we want to verify/inspect +// --------------------------------------------------------- +methods { + // Contract functions that may revert + function foo(bool) external envfree; + function canRevert(bool) external returns bool envfree; + + // For demonstrating summary usage + function callSummarizeMe(bool) external envfree; + function summarizeMe(bool b) external => cvlSummarizeMe(b); +} + +// --------------------------------------------------------- +// 2. CVL function that explicitly uses the 'revert' keyword +// --------------------------------------------------------- +function cvlFunctionThatMayRevert(bool input) { + if (!input) { + revert("Input was false in CVL function"); + } +} + +// --------------------------------------------------------- +// 3. A summary function that can revert. +// --------------------------------------------------------- +// The contract's `summarizeMe(bool b)` is mapped to `cvlSummarizeMe(b)` in CVL. +// If `b` is false, we revert with a message. When called via `callSummarizeMe@withrevert(b)`, +// any revert here bubbles up and sets `lastReverted`. +function cvlSummarizeMe(bool b) { + if (!b) { + revert("Summarize revert because b is false"); + } +} + +// --------------------------------------------------------- +// 4. Example rule: calling 'foo' with @withrevert +// --------------------------------------------------------- +rule testFooWithRevert { + bool condition; + // Using @withrevert to capture whether 'foo' reverts + foo@withrevert(condition); + + // 'foo' reverts when 'condition' is false + assert lastReverted <=> !condition; +} + +// --------------------------------------------------------- +// 5. Example rule: calling a CVL function with @withrevert +// --------------------------------------------------------- +rule testCvlFunctionWithRevert { + bool condition; + // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' is set to true + cvlFunctionThatMayRevert@withrevert(condition); + + // Check that 'lastReverted' matches whether 'condition' was false + assert lastReverted <=> !condition; +} + +// --------------------------------------------------------- +// 6. Demonstration #1 for canRevert: inline approach +// --------------------------------------------------------- +function wrapperForCanRevertInline(bool condition) returns bool { + // Here we call canRevert WITH @withrevert internally + canRevert@withrevert(condition); + return lastReverted; // We return the revert status +} + +rule testCanRevertInline { + bool condition; + bool outcome = wrapperForCanRevertInline(condition); + + // 'outcome' is true exactly when 'condition' is false (i.e., canRevert reverts) + assert outcome <=> !condition; +} + +// --------------------------------------------------------- +// 7. Demonstration #2 for canRevert: revert "bubbling up" +// --------------------------------------------------------- +// We call 'canRevert(condition)' WITHOUT '@withrevert' inside the wrapper, +// letting the revert bubble up to the outer call (the rule). +function wrapperForCanRevertBubble(bool condition) { + canRevert(condition); +} + +rule testCanRevertBubbleUp { + bool condition; + // We call the wrapper with @withrevert, so if 'canRevert' reverts, it bubbles up + wrapperForCanRevertBubble@withrevert(condition); + + // If 'condition' is false => 'canRevert' reverts => bubble up => lastReverted = true + assert lastReverted <=> !condition; +} + +// --------------------------------------------------------- +// 8. Summarize-Me case: the "most interesting" scenario +// --------------------------------------------------------- +// The contract function callSummarizeMe(b) calls summarizeMe(b), +// which is summarized by cvlSummarizeMe(b). That summary reverts +// if b == false. We'll use the 'rule sanity basic' flag to see the call trace. +rule testCallSummarizeMe{ + bool condition; + // Because summarizeMe is mapped to cvlSummarizeMe in CVL (which can revert), +// calling callSummarizeMe with @withrevert will set lastReverted if condition == false. + callSummarizeMe@withrevert(condition); + + // If condition is false => revert => lastReverted = true + // If condition is true => no revert => lastReverted = false + assert lastReverted <=> !condition; +} 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)