Re routing example #180

nivcertora · 2025-07-01T10:36:26Z

No description provided.

nd-certora · 2025-07-01T14:36:42Z

CVLByExample/ReroutingSummaries/StoragePointerExample.spec

+/**
+ * @notice Rule to verify data integrity during storage pointer operations
+ */
+rule testDataIntegrity(env e) {


what's interesting in this rule?

I am not sure what our policy for the Certora Examples here is, but this rule seems to be a sanity check that re-routing summaries doesn't break the data, while it's good to have, my opinion is that this should rather be a test in EVMVerifier than living here in examples, as it is just unnecessary noise for the example. @yoav-el-certora what do you think?

If you agree, I'll remove the test.

Not sure what was the motivation for writing this example.
If you both agree, we can probably remove it.

nd-certora · 2025-07-01T14:43:39Z

CVLByExample/ReroutingSummaries/StoragePointerExample.spec

+        "Current data length should match new data length";
+
+    // Verify operation counter was incremented
+    assert operationCounter() == initialCounter + 1,


so this will fail, right?

nd-certora · 2025-07-01T14:44:01Z

CVLByExample/ReroutingSummaries/StoragePointerExample.spec

+ * @notice Invariant to ensure operation counter only increases
+ */
+invariant operationCounterMonotonic()
+    operationCounter() >= 0


so with the summary it will not increase, right?

nd-certora · 2025-07-01T14:46:16Z

CVLByExample/ReroutingSummaries/README.md

+
+## Problem Statement
+
+In traditional CVL specifications, internal functions that accept storage pointers (especially mappings) are difficult to summarize because:


Suggested change

In traditional CVL specifications, internal functions that accept storage pointers (especially mappings) are difficult to summarize because:

Internal functions that accept storage pointers (especially mappings) can not be summarized to a CVL function that uses the arguments

yoav-el-certora · 2025-07-24T07:07:46Z

Assigning @johspaeth (or someone from his team) to complete and merge this Example.

johspaeth

From my side, this is good to go modulo deletion of the noise that I will take care of when Yoav agrees.

@nd-certora can you re-review?

johspaeth · 2025-07-29T11:24:03Z

CVLByExample/ReroutingSummaries/StoragePointerExample.spec

+/**
+ * @notice Rule to verify data integrity during storage pointer operations
+ */
+rule testDataIntegrity(env e) {


I am not sure what our policy for the Certora Examples here is, but this rule seems to be a sanity check that re-routing summaries doesn't break the data, while it's good to have, my opinion is that this should rather be a test in EVMVerifier than living here in examples, as it is just unnecessary noise for the example. @yoav-el-certora what do you think?

If you agree, I'll remove the test.

johspaeth · 2025-07-29T11:25:02Z

CVLByExample/ReroutingSummaries/StoragePointerExample.spec

-/**
- * @notice Invariant to ensure operation counter only increases
- */
-invariant operationCounterMonotonic()
-    operationCounter() >= 0
-    {
-        preserved {
-            require operationCounter() <= max_uint256 - 1;
-        }
-    }


The invariant is excluded from verification in .conf and I don't see it's value. I removed it to reduce the noise here.

# Conflicts: # CVLByExample/README.md

* Add an example on how to reason about events in CVL (#174) * 7.26.0 Release (#163) * Niv/cert 8248 revert example (#155) * CERT 8248 Add Revert Example * Update README * Address Christiane review * Update example based on Nurit Review * Clean * Update config.yml (#160) Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> * Example ready * christiane cr * Code reviews --------- Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> * Bug fixed * Add an example on how to reason about events in CVL * Addressing code reviews * Addressing Christiane's CR * Issue with merge resolution * Revert "Bug fixed" This reverts commit 33b87b9. * Reverse incorrect change after merge --------- Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: Otakar <Otakar@certora.com> * Removed Process from conf file * Removed send_only from conf file * add a simple example with a transient field and hooks and direct storage accesses on it * remove rule sanity Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> * remove ambiguity * CERT 8687 Realistic example (#167) * CERT 8687 Realistic example * fix spec, sanity issue * fix * require invariant example * Update README * Update CVLByExample/Invariant/RequireInvariantArray/README.md * Addressing Nurit's CR --------- Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> Co-authored-by: Johannes Spaeth <johannes@certora.com> * Re routing example (#180) * Re routing example * Updating example --------- Co-authored-by: Johannes Spaeth <johannes@certora.com> * Niv/fix sanity failure (#183) * Fix some of the sanity failure * Fixing specification to not have sanity failures runFullPool.conf -> https://vaas-stg.certora.com/output/53900/a7ab7f221da84eb4accea1c95e936803?anonymousKey=e063b8e60bae944b4a9d0d0431999b5bd4b578ea runBroken.con -> https://vaas-stg.certora.com/output/53900/c85b8c49fec24d32ac0de00043d7ddd6?anonymousKey=a6c585f91d010a7c13f1c6d8935143b894a0c05d * Updates to spec * Self-Review --------- Co-authored-by: Johannes Spaeth <johannes@certora.com> Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> * Added fixes to breaking changes (#190) * foundry toml * comment * branch * branch * branch * Add an example for internal function calls (#191) * add an example for internal function calls * Update CVLByExample/InternalFunctionsFromCVL/README.md Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> --------- Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> * Added foundry installation to CI (#194) --------- Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: Otakar <Otakar@certora.com> Co-authored-by: Christiane Goltz <christiane@certora.com> Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Co-authored-by: Johannes Spaeth <johannes@certora.com> Co-authored-by: rahav <rahav@certora.com> Co-authored-by: Rahav <103361134+rahav-certora@users.noreply.github.com> Co-authored-by: Naftali Goldstein <44599898+naftali-g@users.noreply.github.com>

Re routing example

3009de7

nivcertora requested a review from nd-certora July 1, 2025 10:36

nivcertora self-assigned this Jul 1, 2025

yoav-el-certora requested a review from johspaeth July 1, 2025 10:50

nd-certora requested changes Jul 1, 2025

View reviewed changes

yoav-el-certora assigned johspaeth and unassigned nivcertora Jul 24, 2025

johspaeth added the release8.0 label Jul 29, 2025

Updating example

4cea3e1

johspaeth approved these changes Jul 29, 2025

View reviewed changes

johspaeth requested a review from nd-certora July 29, 2025 11:26

nd-certora approved these changes Aug 3, 2025

View reviewed changes

Merge branch 'cli-beta' into niv/CERT-9245

41fa81a

# Conflicts: # CVLByExample/README.md

johspaeth merged commit ce303a1 into cli-beta Aug 4, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Re routing example #180

Re routing example #180

Uh oh!

nivcertora commented Jul 1, 2025

Uh oh!

nd-certora Jul 1, 2025

Uh oh!

johspaeth Jul 29, 2025

Uh oh!

yoav-el-certora Jul 29, 2025

Uh oh!

nd-certora Jul 1, 2025

Uh oh!

nd-certora Jul 1, 2025

Uh oh!

nd-certora Jul 1, 2025

Uh oh!

yoav-el-certora commented Jul 24, 2025

Uh oh!

johspaeth left a comment

Uh oh!

johspaeth Jul 29, 2025

Uh oh!

johspaeth Jul 29, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants


		## Problem Statement

		In traditional CVL specifications, internal functions that accept storage pointers (especially mappings) are difficult to summarize because:

	In traditional CVL specifications, internal functions that accept storage pointers (especially mappings) are difficult to summarize because:
	Internal functions that accept storage pointers (especially mappings) can not be summarized to a CVL function that uses the arguments

Re routing example #180

Re routing example #180

Uh oh!

Conversation

nivcertora commented Jul 1, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yoav-el-certora commented Jul 24, 2025

Uh oh!

johspaeth left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants