7.29.1 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/ConfInheritance/MainContract.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+contract MainContract 
+{
+    address currentBidder;
+    uint256 public currentBid;
+
+    // At the entrance to `bid` address(this).balance is already increased by msg.value,
+    // so the receiver gets  `msg.value + address(this).balance` before.
+    // This reverts only if msg.value < address(this).balance
+    function bid() public payable
+    {
+        require(msg.value >= address(this).balance);
+        payable(currentBidder).transfer(address(this).balance);
+        currentBidder = msg.sender; 
+        currentBid = msg.value;
+    }
+}

CVLByExample/ConfInheritance/MainSpec.spec

@@ -0,0 +1,44 @@
+/**
+ * @title  Native balances Example
+ *
+ * This is an example specification for using nativeBalances.
+ */
+
+methods {
+    function currentBid() external returns uint256 envfree; 
+}
+
+/// @title Basic rules ////////////////////////////////////////////////////
+
+/***
+ This rule demonstrates how the source of amount transferred affects the balance of the current contract.
+ This rule fails for `Auction.sol` because:
+ 1. The balance of `currentContract` is increased by `msg.value` at the entrance to `bid()`.
+ 2. the sender changes to `currentContract` in internal `bid()` and all his balance is transferred, so his balance does not increase.
+ This rule passes for `AuctionFixed.sol` because only `currentBid` is transferred.
+ */
+rule bidIncreasesAssets() {
+    env e;
+    require(e.msg.sender != currentContract);
+    require(e.msg.value > currentBid() );
+    uint256 balanceBefore = nativeBalances[currentContract];
+    bid(e);
+    assert nativeBalances[currentContract] > balanceBefore;
+}
+
+/***
+ This rule demonstrates how the source of amount transferred affects the balance of the current contract.
+ This rule passes vacuously for `Auction.sol` because of the `require e.msg.value > nativeBalances[currentContract]` in the spec
+ and `require msg.value >= msg.value + nativeBalances[currentContract]` in the code where `nativeBalances[currentContract] > 0`.
+ It passes non-vacuously for AuctionFixed.sol because the amount transferred is `currentBid` for which `msg.value >= currentBid`
+ can hold.
+ */
+rule bidSuccessfullyExpectVacuous() {
+    env e;
+    uint256 balanceBefore = nativeBalances[currentContract];
+    require(e.msg.sender != currentContract);
+    require(e.msg.value > 0 &&  e.msg.value > balanceBefore);
+    require (balanceBefore > 0);
+    bid(e);
+    assert nativeBalances[currentContract] >= balanceBefore;
+}

CVLByExample/ConfInheritance/README.md

@@ -0,0 +1,109 @@
+# Configuration File Inheritance Example
+
+This folder demonstrates how to use the **`override_base_config`** feature to inherit and selectively modify Certora Prover configuration files. By defining **common** settings in a **base** config (`base.conf`) and referencing it from different child configs, you can avoid duplication and streamline maintenance.
+
+---
+
+## Files
+
+1. **`MainContract.sol`**  
+   A minimal Solidity contract to be verified.
+
+2. **`base.conf`**  
+   **Base** configuration with shared defaults:
+   ```jsonc
+   {
+     "files": ["MainContract.sol"],
+     "verify": "MainContract:MainContract.spec",
+     "msg": "Main contract",
+     "optimistic_loop": true,
+     "loop_iter": "3",
+     "rule_sanity": "basic"
+   }
+   ```
+   - Defines the source files, contract–spec pairing, default loop settings, etc.
+
+3. **`new_fields.conf`**  
+   Child config **adding** a new field (`optimistic_hashing`) not present in `base.conf`:
+   ```jsonc
+   {
+     "override_base_config": "base.conf",
+     "optimistic_hashing": true
+   }
+   ```
+
+4. **`override_fields.conf`**  
+   Child config **overriding** certain fields from `base.conf`:
+   ```jsonc
+   {
+     "override_base_config": "base.conf",
+     "loop_iter": "10",
+     "optimistic_loop": false
+   }
+   ```
+
+5. **`invalid_base.conf`**  
+   A config that **incorrectly** attempts to act as a base while also referencing **another** base:
+   ```jsonc
+   {
+     "files": ["MainContract.sol"],
+     "verify": "MainContract:MainContract.spec",
+     "msg": "Main contract",
+     "optimistic_loop": true,
+     "loop_iter": "3",
+     "rule_sanity": "basic",
+     "override_base_config": "base.conf"
+   }
+   ```
+   - **This is invalid** because a base config must **not** itself contain `override_base_config`.
+   - The feature currently supports **only one** level of inheritance (no nested base configs).
+
+---
+
+## Usage Examples
+
+### Merging **`base.conf`** + **`new_fields.conf`**
+```bash
+certoraRun new_fields.conf
+```
+- Inherits `base.conf` and **adds** `"optimistic_hashing": true`.
+
+### Merging **`base.conf`** + **`override_fields.conf`**
+```bash
+certoraRun override_fields.conf
+```
+- Changes `loop_iter` from `"3"` to `"10"` and sets `optimistic_loop` to `false`.
+
+---
+
+## Invalid Base Example
+### Attempting to Use **`invalid_base.conf`**
+```bash
+certoraRun invalid_base.conf
+```
+Error:
+```
+certoraRun invalid_base.conf
+
+Cannot load base config: override_fields.conf
+base config cannot include 'override_base_config'
+
+Error when reading invalid_base.conf: Cannot load base config: override_fields.conf
+base config cannot include 'override_base_config'
+```
+
+- **`invalid_base.conf`** tries to reference `override_fields.conf` as a base config.
+- **This is disallowed** because the feature only supports **single-level inheritance**: a base config **cannot** itself specify an `override_base_config` field.
+
+---
+
+## Why Use `override_base_config`?
+
+1. **Reduce Duplication**  
+   Common fields (e.g., file lists, compiler version, environment arguments) live in **one** place.
+
+2. **Clear Overrides**  
+   Child configs only show what differs from the parent.
+
+3. **Easier Maintenance**  
+   Updating a shared parameter (e.g., loop iterations) means editing just one file.

CVLByExample/ConfInheritance/base.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "MainContract.sol",
+  ],
+  "verify": "MainContract:MainSpec.spec",
+  "msg": "Main contract",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic"
+}

CVLByExample/ConfInheritance/invalid_base.conf

@@ -0,0 +1,11 @@
+{
+  "files": [
+    "MainContract.sol",
+  ],
+  "verify": "MainContract:MainSpec.spec",
+  "msg": "Main contract",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic",
+  "override_base_config": "override_fields.conf",
+}

CVLByExample/ConfInheritance/new_fields.conf

@@ -0,0 +1,5 @@
+{
+  "override_base_config": "base.conf",
+  "optimistic_hashing": true,
+}
+

CVLByExample/ConfInheritance/override_fields.conf

@@ -0,0 +1,6 @@
+{
+  "override_base_config": "base.conf",
+  "loop_iter": "10",
+  "optimistic_loop": 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"
+}