Niv/cert 8248 revert example

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