Niv/fix sanity failure #183

nivcertora · 2025-07-06T09:49:07Z

No description provided.

johspaeth

Minor nits and questions - looks ok for me.

johspaeth · 2025-07-07T09:29:39Z

CVLByExample/TransientStorage/Hooks/Mutexer.spec

+// invariant version is getting SANITY_FAILURE using the below rule instead
+// invariant lockStatusDontChange()
+//     !contract_lock_status;


Which sanity failure did you receive on this invariant?

I couldn't find a link to a failing job here:
https://certora.atlassian.net/browse/CERT-9252

would also like to know what was wrong with the invariant, it looks ok and we still want such invariants. do you have a link to the original spec with the sanity failures

../repo/CVLByExample/TransientStorage/Hooks/runTransientStorage.conf
https://vaas-stg.certora.com/output/52759/0105a027db864c0bb9897978e361037d?anonymousKey=6f78ed30dd77d25d27ec6cefcbf5ad358a62efe9

I reverted the change by Niv and make this invariant working again.

The issue here is / was that there is a hook on tload/tstore within the constructor and the hooks call out to external solidity function of the same contract which isn't allowed within the constructor (the contract hasn't been created yet). In my fix, I removed all calls that are applied in the hook and changed the accesses to constants that are declared in CVL. This is the only solution I could find here.

johspaeth · 2025-07-07T09:30:41Z

CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec

@@ -129,12 +129,6 @@ hook Sstore _customers[KEY address user].accounts.length uint256 newLength {
    numOfAccounts[user] = newLength;
 }

-/**
- An internal step check to verify that our ghost works as expected, it should mirror the number of accounts.
- Once the sload is defined, this invariant becomes a tautology  


Once the sload is defined, this invariant becomes a tautology

Is sload now defined nowadays, so is this why we see the sanity failure for trivial post condition of the invariant?

After reviewing, I suggest we indeed remove this invariant as it fails on SANITY due to the tautology check.

runFullPool.conf -> https://vaas-stg.certora.com/output/53900/a7ab7f221da84eb4accea1c95e936803?anonymousKey=e063b8e60bae944b4a9d0d0431999b5bd4b578ea runBroken.con -> https://vaas-stg.certora.com/output/53900/c85b8c49fec24d32ac0de00043d7ddd6?anonymousKey=a6c585f91d010a7c13f1c6d8935143b894a0c05d

CERT-9252 | Fix sanity failures in induction base for major version 8

nd-certora · 2025-07-12T19:16:01Z

CVLByExample/TransientStorage/Hooks/Mutexer.spec

+// invariant version is getting SANITY_FAILURE using the below rule instead
+// invariant lockStatusDontChange()
+//     !contract_lock_status;


would also like to know what was wrong with the invariant, it looks ok and we still want such invariants. do you have a link to the original spec with the sanity failures

nd-certora · 2025-07-12T19:17:17Z

CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec

@@ -1,14 +1,11 @@
-invariant isUnlocked(env e) 
-   getLock(e) == 0;
-


what was the sanity failure? we prefer invariant as the requireinvariant is safer

https://vaas-stg.certora.com/output/52759/561cd936b64c4d188853b7b887abb7ff?anonymousKey=6fe5dc8ff22146e9c30a1a60fe712527b66350be

The issue here was that a few functions (repay, borrow, callback) use a modifier onlyLocked that contract with the actual invariant and cause vacuity. I filtered them for this invariant.

johspaeth

@nd-certora @yoav-el-certora please re-review.

The issue with lockStatusDontChange was that a hook in the constructor called an external method on the same contract - this causes vacuity as the contract doesn't exist yet. This is also not allowed in solidity itself.
I added a new function changeLock which shows that the invariant fails for lockStatusDontChange. This is expected, @yoav-el-certora. Please update output.json expectedly.
For isUnlocked a filter for a few function was needed.

johspaeth · 2025-07-18T06:51:30Z

CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec

@@ -129,12 +129,6 @@ hook Sstore _customers[KEY address user].accounts.length uint256 newLength {
    numOfAccounts[user] = newLength;
 }

-/**
- An internal step check to verify that our ghost works as expected, it should mirror the number of accounts.
- Once the sload is defined, this invariant becomes a tautology  


After reviewing, I suggest we indeed remove this invariant as it fails on SANITY due to the tautology check.

johspaeth · 2025-07-18T06:55:28Z

CVLByExample/TransientStorage/Hooks/runTransientStorage.conf

@@ -4,5 +4,6 @@
  ],
  "verify": "MockMutexer:./Mutexer.spec",
  "solc": "solc8.24", 
-  "solc_evm_version": "cancun"
+  "solc_evm_version": "cancun",
+  "prover_args": ["-enableStorageSplitting false"]


This was needed here as we got storage splitting failures otherwise. @christiane-certora do you know if this is expected here?

The contract defines a constant slot via keccak256("Mutexer.CONTRACT_LOCK") and then in spec uses alltload/alltstore.

If the contract uses ALLTLOAD or ALLTSTORE, you should get an error that storage splitting must be disabled, these hook types are not compatible with it (same as the non-transient versions of them).

So should we instead rather use TLOAD and TSTORE here directly (now that we support them?)

It looks like we could, yeah, although the currently used way of course also still works.

But maybe it is not so bad to leave this example, since there are still a lot of patterns with transient storage where we will fail the storage analysis (when the slot accessed is just a parameter, typically), so in that case it could be useful to still see how it can be worked with without.

johspaeth · 2025-07-18T06:55:56Z

CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec

@@ -1,14 +1,11 @@
-invariant isUnlocked(env e) 
-   getLock(e) == 0;
-


The issue here was that a few functions (repay, borrow, callback) use a modifier onlyLocked that contract with the actual invariant and cause vacuity. I filtered them for this invariant.

johspaeth · 2025-07-18T07:00:24Z

CVLByExample/TransientStorage/Hooks/MockMutexer.sol

+        uint256 key = CONTRACT_LOCK;
+        assembly {
+             value := tload(key)
+        }
+        return value == Mutex.Locked;


This should actually be _tload() which is private in the parent contract and cannot be called here.

Fix some of the sanity failure

0b8b272

nivcertora requested a review from liav-certora July 6, 2025 09:49

nivcertora self-assigned this Jul 6, 2025

nivcertora changed the base branch from master to cli-beta July 6, 2025 09:49

nivcertora requested review from nd-certora and yoav-el-certora and removed request for liav-certora July 6, 2025 10:44

yoav-el-certora requested a review from johspaeth July 7, 2025 08:32

johspaeth reviewed Jul 7, 2025

View reviewed changes

johspaeth and others added 2 commits July 11, 2025 09:47

Merge pull request #185 from Certora/niv/johannes/fix-sanity-failures

67d87e2

CERT-9252 | Fix sanity failures in induction base for major version 8

nd-certora reviewed Jul 12, 2025

View reviewed changes

johspaeth added 2 commits July 17, 2025 19:41

Updates to spec

1df0132

Self-Review

2fd6b92

johspaeth reviewed Jul 18, 2025

View reviewed changes

johspaeth requested a review from nd-certora July 18, 2025 07:03

		@@ -1,14 +1,11 @@
		invariant isUnlocked(env e)
		getLock(e) == 0;

Niv/fix sanity failure #183

Are you sure you want to change the base?

Niv/fix sanity failure #183

Conversation

nivcertora commented Jul 6, 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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

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!

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!

Uh oh!