Transient Storage Field Example

CVLByExample/TransientStorage/TransientFields/Default.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "TransientTest.sol",
+    ],
+    "solc": "solc8.28",
+    "solc_evm_version": "cancun",
+    "verify": "TransientTest:Default.spec"
+}

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

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

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