Skip to content

Conversation

@christiane-certora
Copy link
Contributor

add a simple example with a transient field and hooks and direct storage accesses on it

@yoav-el-certora yoav-el-certora changed the base branch from master to cli-beta July 28, 2025 13:32
@christiane-certora christiane-certora changed the base branch from cli-beta to master July 28, 2025 14:17
@christiane-certora christiane-certora changed the base branch from master to cli-beta July 28, 2025 14:17
Copy link
Contributor

@johspaeth johspaeth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

# 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.
Copy link
Contributor

@johspaeth johspaeth Jul 29, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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 them as well.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

it's not direct storage access on the hooks, it's on the fields. Would "on the fields" be clearer? The "them" was meant to refer back to the "such fields".

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lol, of course.

I wanted to clarify what 'them' refers to and remove the ambiguity, clearly failed here by proving the point that it was ambiguous.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess it makes a strong case for some change :D

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

there we go

christiane-certora and others added 2 commits July 29, 2025 11:47
Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com>
@christiane-certora christiane-certora merged commit 1abc1ad into cli-beta Jul 29, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants