7.26.0 Release

.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

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) |
 
 
 

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);
+    }
+}

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.

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"
+}

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;
+}

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 { }
+}