From 54bc64370a462797e40c96df45672f7938773008 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 12 Feb 2025 11:54:23 +0200 Subject: [PATCH 1/5] CERT 8248 Add Revert Example --- CVLByExample/RevertKeyWord/C.sol | 49 +++++++++++++++++++++ CVLByExample/RevertKeyWord/README.md | 41 ++++++++++++++++++ CVLByExample/RevertKeyWord/example.conf | 12 ++++++ CVLByExample/RevertKeyWord/example.spec | 57 +++++++++++++++++++++++++ 4 files changed, 159 insertions(+) create mode 100644 CVLByExample/RevertKeyWord/C.sol create mode 100644 CVLByExample/RevertKeyWord/README.md create mode 100644 CVLByExample/RevertKeyWord/example.conf create mode 100644 CVLByExample/RevertKeyWord/example.spec 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..cd684e4e --- /dev/null +++ b/CVLByExample/RevertKeyWord/README.md @@ -0,0 +1,41 @@ +# 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. + - Additional helper functions: `callFooFromContract`, `summarizeMe`, `callSummarizeMe`. + +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. + - Verifying the `lastReverted` flag matches expected behavior. + +## 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/5891181678d0461cb8bcf35122816e8a?anonymousKey=1980299435d6469aa3673d883de13982c204431a) + + +3. **Examine the Rules** + - **`testFooWithRevert`** confirms that calling `foo` with `@withrevert` sets `lastReverted` exactly when the argument is false. + - **`testCvlFunctionWithRevert`** confirms that a CVL function can revert and sets `lastReverted` accordingly. + - **`testCanRevert`** uses a wrapper function to capture the return value of the revert signal from `canRevert`. + + +## Conclusion + +With these files (`C.sol`, `example.spec`, and this `README.md`), you can see how the new CVL revert feature works in practice. By enabling `-cvlFunctionRevert`, 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. diff --git a/CVLByExample/RevertKeyWord/example.conf b/CVLByExample/RevertKeyWord/example.conf new file mode 100644 index 00000000..ab7cdb2a --- /dev/null +++ b/CVLByExample/RevertKeyWord/example.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "C.sol" + ], + "independent_satisfy": true, + "process": "emv", + "solc": "solc8.26", + "verify": "C:example.spec", + "prover_args": [ + "-cvlFunctionRevert true" + ] +} diff --git a/CVLByExample/RevertKeyWord/example.spec b/CVLByExample/RevertKeyWord/example.spec new file mode 100644 index 00000000..ecb6686e --- /dev/null +++ b/CVLByExample/RevertKeyWord/example.spec @@ -0,0 +1,57 @@ +// We declare the external methods (functions) that we want to call or reference: +methods { + function foo(bool) external envfree; + function canRevert(bool) external returns bool envfree; +} + +// -------------------- +// Example CVL function that can revert: +// -------------------- +function cvlFunctionThatMayRevert(bool input) { + // The new 'revert' keyword in CVL + if (!input) { + revert("Input was false in CVL function"); + } +} + +// -------------------- +// Example rule: calling 'foo' with @withrevert +// -------------------- +rule testFooWithRevert { + bool condition; + // Using @withrevert to capture whether 'foo' reverts + foo@withrevert(condition); + + // 'lastReverted' is true if and only if 'foo' reverts + // 'foo' reverts when 'condition' is false + assert lastReverted <=> !condition; +} + +// -------------------- +// Example rule: calling a CVL function with @withrevert +// -------------------- +rule testCvlFunctionWithRevert { + bool condition; + // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' is set to true + cvlFunctionThatMayRevert@withrevert(condition); + + // This rule checks that 'lastReverted' is exactly when 'condition' is false + assert lastReverted <=> !condition; +} + +// -------------------- +// Example rule: calling 'canRevert' within a CVL wrapper and using @withrevert +// -------------------- +function wrapperForCanRevert(bool condition) returns bool { + // If 'canRevert(condition)' reverts, 'lastReverted' is set to true here + canRevert@withrevert(condition); + return lastReverted; +} + +rule testCanRevert { + bool condition; + bool outcome = wrapperForCanRevert(condition); + + // This rule checks that 'lastReverted' is exactly when 'condition' is false + assert outcome <=> !condition; +} From a6fb7cf0de66b44d1f0d2023b690922d4a780c4e Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 12 Feb 2025 11:57:07 +0200 Subject: [PATCH 2/5] Update README --- CVLByExample/README.md | 1 + 1 file changed, 1 insertion(+) 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) | From ae2eca20d8e6caf378ff10cf8066ecfc45d3658d Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 12 Feb 2025 13:39:24 +0200 Subject: [PATCH 3/5] Address Christiane review --- CVLByExample/RevertKeyWord/README.md | 13 ++--- CVLByExample/RevertKeyWord/example.spec | 74 ++++++++++++++++--------- 2 files changed, 55 insertions(+), 32 deletions(-) diff --git a/CVLByExample/RevertKeyWord/README.md b/CVLByExample/RevertKeyWord/README.md index cd684e4e..64cf340c 100644 --- a/CVLByExample/RevertKeyWord/README.md +++ b/CVLByExample/RevertKeyWord/README.md @@ -17,7 +17,7 @@ This folder demonstrates the newly introduced **CVL revert functionality** and t 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. - - Verifying the `lastReverted` flag matches expected behavior. + - 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. ## Usage @@ -29,13 +29,12 @@ This folder demonstrates the newly introduced **CVL revert functionality** and t - 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/5891181678d0461cb8bcf35122816e8a?anonymousKey=1980299435d6469aa3673d883de13982c204431a) - 3. **Examine the Rules** - - **`testFooWithRevert`** confirms that calling `foo` with `@withrevert` sets `lastReverted` exactly when the argument is false. - - **`testCvlFunctionWithRevert`** confirms that a CVL function can revert and sets `lastReverted` accordingly. - - **`testCanRevert`** uses a wrapper function to capture the return value of the revert signal from `canRevert`. - + - **`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` from the rule. The internal revert propagates, setting `lastReverted`. ## Conclusion -With these files (`C.sol`, `example.spec`, and this `README.md`), you can see how the new CVL revert feature works in practice. By enabling `-cvlFunctionRevert`, 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. +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 can now propagate reverts just like Solidity calls. diff --git a/CVLByExample/RevertKeyWord/example.spec b/CVLByExample/RevertKeyWord/example.spec index ecb6686e..5ccd9053 100644 --- a/CVLByExample/RevertKeyWord/example.spec +++ b/CVLByExample/RevertKeyWord/example.spec @@ -1,57 +1,81 @@ -// We declare the external methods (functions) that we want to call or reference: +// --------------------------------------------------------- +// 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; } -// -------------------- -// Example CVL function that can revert: -// -------------------- +// --------------------------------------------------------- +// 2. CVL function that explicitly uses the 'revert' keyword +// --------------------------------------------------------- function cvlFunctionThatMayRevert(bool input) { - // The new 'revert' keyword in CVL + // If input is false, we revert with a message if (!input) { revert("Input was false in CVL function"); } } -// -------------------- -// Example rule: calling 'foo' with @withrevert -// -------------------- +// --------------------------------------------------------- +// 3. Demonstration #1: Calling 'foo' with @withrevert directly +// --------------------------------------------------------- rule testFooWithRevert { bool condition; - // Using @withrevert to capture whether 'foo' reverts + // Using @withrevert to see if 'foo' reverts foo@withrevert(condition); - // 'lastReverted' is true if and only if 'foo' reverts - // 'foo' reverts when 'condition' is false + // 'foo' reverts exactly when 'condition' is false + // => 'lastReverted' == !condition assert lastReverted <=> !condition; } -// -------------------- -// Example rule: calling a CVL function with @withrevert -// -------------------- +// --------------------------------------------------------- +// 4. Demonstration #2: Calling a CVL function with @withrevert +// --------------------------------------------------------- rule testCvlFunctionWithRevert { bool condition; - // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' is set to true + // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' becomes true cvlFunctionThatMayRevert@withrevert(condition); - // This rule checks that 'lastReverted' is exactly when 'condition' is false + // Check that 'lastReverted' matches whether 'condition' was false assert lastReverted <=> !condition; } -// -------------------- -// Example rule: calling 'canRevert' within a CVL wrapper and using @withrevert -// -------------------- -function wrapperForCanRevert(bool condition) returns bool { - // If 'canRevert(condition)' reverts, 'lastReverted' is set to true here +// --------------------------------------------------------- +// 5. Demonstration #3 (Old Approach): 'canRevert' using @withrevert INSIDE the wrapper +// --------------------------------------------------------- +function wrapperForCanRevertInline(bool condition) returns bool { + // Here we call canRevert WITH @withrevert internally canRevert@withrevert(condition); - return lastReverted; + return lastReverted; // We return the revert status } -rule testCanRevert { +rule testCanRevertInline { bool condition; - bool outcome = wrapperForCanRevert(condition); + bool outcome = wrapperForCanRevertInline(condition); - // This rule checks that 'lastReverted' is exactly when 'condition' is false + // 'outcome' is true iff 'canRevert' reverted, which happens if condition == false assert outcome <=> !condition; } + +// --------------------------------------------------------- +// 6. Demonstration #4 (New Approach): Revert "bubbling up" through a CVL function +// --------------------------------------------------------- +// In this approach, 'canRevert' is called WITHOUT @withrevert inside the function. +// Then, from the rule, we call the wrapper itself with @withrevert, allowing the +// revert to "bubble up" and set 'lastReverted' if an internal revert occurs. +function wrapperForCanRevertBubble(bool condition) { + // Notice: no @withrevert here + canRevert(condition); +} + +rule testCanRevertBubbleUp { + bool condition; + // We call the wrapper with @withrevert from the rule + wrapperForCanRevertBubble@withrevert(condition); + + // If 'canRevert(condition)' reverts internally when condition == false, + // that revert will bubble up and set 'lastReverted' to true. + assert lastReverted <=> !condition; +} From e1406fc304b0b02e6c6a9b1dbae4c7b585d6e35c Mon Sep 17 00:00:00 2001 From: Niv Date: Tue, 25 Feb 2025 12:28:29 +0200 Subject: [PATCH 4/5] Update example based on Nurit Review --- CVLByExample/RevertKeyWord/README.md | 23 ++++++--- CVLByExample/RevertKeyWord/example.conf | 3 +- CVLByExample/RevertKeyWord/example.spec | 64 ++++++++++++++++++------- 3 files changed, 64 insertions(+), 26 deletions(-) diff --git a/CVLByExample/RevertKeyWord/README.md b/CVLByExample/RevertKeyWord/README.md index 64cf340c..47363c65 100644 --- a/CVLByExample/RevertKeyWord/README.md +++ b/CVLByExample/RevertKeyWord/README.md @@ -11,13 +11,16 @@ This folder demonstrates the newly introduced **CVL revert functionality** and t 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. - - Additional helper functions: `callFooFromContract`, `summarizeMe`, `callSummarizeMe`. + - `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 @@ -27,14 +30,20 @@ This folder demonstrates the newly introduced **CVL revert functionality** and t ``` 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/5891181678d0461cb8bcf35122816e8a?anonymousKey=1980299435d6469aa3673d883de13982c204431a) + - 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` from the rule. The internal revert propagates, setting `lastReverted`. + - **`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 can now propagate reverts just like Solidity calls. +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 index ab7cdb2a..6a697400 100644 --- a/CVLByExample/RevertKeyWord/example.conf +++ b/CVLByExample/RevertKeyWord/example.conf @@ -8,5 +8,6 @@ "verify": "C:example.spec", "prover_args": [ "-cvlFunctionRevert true" - ] + ], + "rule_sanity": "basic" } diff --git a/CVLByExample/RevertKeyWord/example.spec b/CVLByExample/RevertKeyWord/example.spec index 5ccd9053..699467e3 100644 --- a/CVLByExample/RevertKeyWord/example.spec +++ b/CVLByExample/RevertKeyWord/example.spec @@ -5,37 +5,51 @@ 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 is false, we revert with a message if (!input) { revert("Input was false in CVL function"); } } // --------------------------------------------------------- -// 3. Demonstration #1: Calling 'foo' with @withrevert directly +// 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 see if 'foo' reverts + // Using @withrevert to capture whether 'foo' reverts foo@withrevert(condition); - // 'foo' reverts exactly when 'condition' is false - // => 'lastReverted' == !condition + // 'foo' reverts when 'condition' is false assert lastReverted <=> !condition; } // --------------------------------------------------------- -// 4. Demonstration #2: Calling a CVL function with @withrevert +// 5. Example rule: calling a CVL function with @withrevert // --------------------------------------------------------- rule testCvlFunctionWithRevert { bool condition; - // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' becomes true + // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' is set to true cvlFunctionThatMayRevert@withrevert(condition); // Check that 'lastReverted' matches whether 'condition' was false @@ -43,7 +57,7 @@ rule testCvlFunctionWithRevert { } // --------------------------------------------------------- -// 5. Demonstration #3 (Old Approach): 'canRevert' using @withrevert INSIDE the wrapper +// 6. Demonstration #1 for canRevert: inline approach // --------------------------------------------------------- function wrapperForCanRevertInline(bool condition) returns bool { // Here we call canRevert WITH @withrevert internally @@ -55,27 +69,41 @@ rule testCanRevertInline { bool condition; bool outcome = wrapperForCanRevertInline(condition); - // 'outcome' is true iff 'canRevert' reverted, which happens if condition == false + // 'outcome' is true exactly when 'condition' is false (i.e., canRevert reverts) assert outcome <=> !condition; } // --------------------------------------------------------- -// 6. Demonstration #4 (New Approach): Revert "bubbling up" through a CVL function +// 7. Demonstration #2 for canRevert: revert "bubbling up" // --------------------------------------------------------- -// In this approach, 'canRevert' is called WITHOUT @withrevert inside the function. -// Then, from the rule, we call the wrapper itself with @withrevert, allowing the -// revert to "bubble up" and set 'lastReverted' if an internal revert occurs. +// We call 'canRevert(condition)' WITHOUT '@withrevert' inside the wrapper, +// letting the revert bubble up to the outer call (the rule). function wrapperForCanRevertBubble(bool condition) { - // Notice: no @withrevert here - canRevert(condition); + canRevert(condition); } rule testCanRevertBubbleUp { bool condition; - // We call the wrapper with @withrevert from the rule + // We call the wrapper with @withrevert, so if 'canRevert' reverts, it bubbles up wrapperForCanRevertBubble@withrevert(condition); - // If 'canRevert(condition)' reverts internally when condition == false, - // that revert will bubble up and set 'lastReverted' to true. + // 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 'sanity' tag 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; } From e91c2ed3368d0cdaa9fdc9a25be22f52dfff861c Mon Sep 17 00:00:00 2001 From: Niv Date: Tue, 25 Feb 2025 12:30:11 +0200 Subject: [PATCH 5/5] Clean --- CVLByExample/RevertKeyWord/example.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CVLByExample/RevertKeyWord/example.spec b/CVLByExample/RevertKeyWord/example.spec index 699467e3..a6a1f9bf 100644 --- a/CVLByExample/RevertKeyWord/example.spec +++ b/CVLByExample/RevertKeyWord/example.spec @@ -96,7 +96,7 @@ rule testCanRevertBubbleUp { // --------------------------------------------------------- // The contract function callSummarizeMe(b) calls summarizeMe(b), // which is summarized by cvlSummarizeMe(b). That summary reverts -// if b == false. We'll use the 'sanity' tag to see the call trace. +// 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),