From b97218832625a88c6dffee8dcec8509f4114aa46 Mon Sep 17 00:00:00 2001 From: Christiane Goltz Date: Mon, 28 Jul 2025 15:27:49 +0200 Subject: [PATCH 1/3] add a simple example with a transient field and hooks and direct storage accesses on it --- .../TransientFields/Default.conf | 9 +++++ .../TransientFields/Default.spec | 33 +++++++++++++++++++ .../TransientFields/README.md | 16 +++++++++ .../TransientFields/TransientTest.sol | 16 +++++++++ 4 files changed, 74 insertions(+) create mode 100644 CVLByExample/TransientStorage/TransientFields/Default.conf create mode 100644 CVLByExample/TransientStorage/TransientFields/Default.spec create mode 100644 CVLByExample/TransientStorage/TransientFields/README.md create mode 100644 CVLByExample/TransientStorage/TransientFields/TransientTest.sol diff --git a/CVLByExample/TransientStorage/TransientFields/Default.conf b/CVLByExample/TransientStorage/TransientFields/Default.conf new file mode 100644 index 00000000..9c91c99a --- /dev/null +++ b/CVLByExample/TransientStorage/TransientFields/Default.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "TransientTest.sol", + ], + "rule_sanity": "basic", + "solc": "solc8.28", + "solc_evm_version": "cancun", + "verify": "TransientTest:Default.spec" +} \ No newline at end of file diff --git a/CVLByExample/TransientStorage/TransientFields/Default.spec b/CVLByExample/TransientStorage/TransientFields/Default.spec new file mode 100644 index 00000000..ce297d39 --- /dev/null +++ b/CVLByExample/TransientStorage/TransientFields/Default.spec @@ -0,0 +1,33 @@ +methods { + function TransientTest.lock() external returns (bool) envfree; + function TransientTest.unlock() external returns (bool) envfree; +} + +ghost bool ghostLocked; + + +// We can hook on the transient field locked just like on any normal storage field +hook Tload bool value currentContract.locked { + require ghostLocked == value, "we want our ghost to match the read value"; +} + +hook Tstore currentContract.locked bool value (bool oldValue) { + require ghostLocked == oldValue, "our ghost must have matched the old value before this store"; + ghostLocked = value; +} + + +rule lockLocks() { + // we can also directly access the transient field from cvl, like any normal field + require !currentContract.locked, "initially we want to be in unlocked state"; + lock(); + assert currentContract.locked; + assert ghostLocked; +} + +rule unlockUnlocks() { + require currentContract.locked, "initially we want to be in locked state"; + unlock(); + assert !currentContract.locked; + assert !ghostLocked; +} \ No newline at end of file diff --git a/CVLByExample/TransientStorage/TransientFields/README.md b/CVLByExample/TransientStorage/TransientFields/README.md new file mode 100644 index 00000000..341bedc3 --- /dev/null +++ b/CVLByExample/TransientStorage/TransientFields/README.md @@ -0,0 +1,16 @@ +# TransientStorage Example with transient field syntax + +## Overview +This folder contains a smart contract named `TransientTest` that implements a simple lock via a transient boolean field. The spec file demonstrate how we can use the `Tstore` and `Tload` hooks to hook on accesses to such fields, and shows also that we can use direct storage access from CVL on them as well. + +## Executions + +1. **Certora Run for TransientStorage** + - Command: + ```bash + certoraRun Default.conf --server production + ``` + - Execution Link: [Certora Run Output](https://prover.certora.com/output/950033/96f75ac15d9346bd995b581283f90a84?anonymousKey=19abd76348fe169eca42f406c5da5d9fff3da1a9) + + +For a comprehensive guide on Certora Verification Language, refer to [Certora Documentation](https://docs.certora.com). \ No newline at end of file diff --git a/CVLByExample/TransientStorage/TransientFields/TransientTest.sol b/CVLByExample/TransientStorage/TransientFields/TransientTest.sol new file mode 100644 index 00000000..aed31f92 --- /dev/null +++ b/CVLByExample/TransientStorage/TransientFields/TransientTest.sol @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.28; + +contract TransientTest { + bool transient locked; + + function lock() public returns (bool) { + locked = true; + return true; + } + + function unlock() public returns (bool) { + locked = false; + return false; + } +} \ No newline at end of file From 318855082cec3400888a929ae362cdc290b8903e Mon Sep 17 00:00:00 2001 From: christiane-certora Date: Tue, 29 Jul 2025 11:47:38 +0200 Subject: [PATCH 2/3] remove rule sanity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Johannes Späth --- CVLByExample/TransientStorage/TransientFields/Default.conf | 1 - 1 file changed, 1 deletion(-) diff --git a/CVLByExample/TransientStorage/TransientFields/Default.conf b/CVLByExample/TransientStorage/TransientFields/Default.conf index 9c91c99a..216ae2a9 100644 --- a/CVLByExample/TransientStorage/TransientFields/Default.conf +++ b/CVLByExample/TransientStorage/TransientFields/Default.conf @@ -2,7 +2,6 @@ "files": [ "TransientTest.sol", ], - "rule_sanity": "basic", "solc": "solc8.28", "solc_evm_version": "cancun", "verify": "TransientTest:Default.spec" From 61e52ad92810d6227ec356878a9dffdf231ffd80 Mon Sep 17 00:00:00 2001 From: Christiane Goltz Date: Tue, 29 Jul 2025 11:53:37 +0200 Subject: [PATCH 3/3] remove ambiguity --- CVLByExample/TransientStorage/TransientFields/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CVLByExample/TransientStorage/TransientFields/README.md b/CVLByExample/TransientStorage/TransientFields/README.md index 341bedc3..b04b965a 100644 --- a/CVLByExample/TransientStorage/TransientFields/README.md +++ b/CVLByExample/TransientStorage/TransientFields/README.md @@ -1,7 +1,7 @@ # TransientStorage Example with transient field syntax ## Overview -This folder contains a smart contract named `TransientTest` that implements a simple lock via a transient boolean field. The spec file demonstrate how we can use the `Tstore` and `Tload` hooks to hook on accesses to such fields, and shows also that we can use direct storage access from CVL on them as well. +This folder contains a smart contract named `TransientTest` that implements a simple lock via a transient boolean field. The spec file demonstrates how we can use the `Tstore` and `Tload` hooks to hook on accesses to such fields, and shows also that we can use direct storage access from CVL on such fields as well. ## Executions