Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] String-in-storage invariants #223

Draft
wants to merge 1 commit into
base: shelly/gapsfromvoododocrevert
Choose a base branch
from
Draft

[WIP] String-in-storage invariants #223

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 46 additions & 4 deletions docs/user-guide/gaps.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -425,10 +425,52 @@ argument in calldata (first 4 bytes are the `sighash`, another word is for the p
`arg34_data[0x4]` holds the relative offset to the string)
`arg34_data[0x4+arg34_data[0x4]]` holds the length of the string.

;### Strings-in-storage invariant
;
;TODO
;
### Strings-in-storage invariant

We consider the following code and specification:
```solidity
contract StringInStorage {
string name;
function setName() external {
name = "Certora";
}
}
```

```cvl
methods {
function setName() external envfree;
}

rule revertSetName {
setName@withrevert();
assert !lastReverted;
}
```

This revert check would fail, because the Prover has no assumptions on the integrity
of the state of the contract prior to the call, and the Solidity compiler instruments
an invariant check on the state before setting the string in storage.

Let's consider first the revert cause emitted by the Prover:
`!(((tacSCANON0!!5[skey_basic:bif(0x0)]&0x1)-(((tacSCANON0!!5[skey_basic:bif(0x0)]&0x1)>0x0 ? tacSCANON0!!5[skey_basic:bif(0x0)]/0x2 : (tacSCANON0!!5[skey_basic:bif(0x0)]/0x2)&0x7f)<0x20 ? 0x1 : 0x0))>0x0)`
It looks very complicated, so to ease on reading we do some trivial logical simplifications:
```
(tacSCANON0!!5[skey_basic:bif(0x0)]&0x1)==0x1 // 0 or 1 - is odd check
<=> (
(
(tacSCANON0!!5[skey_basic:bif(0x0)]&0x1)>0x0
? tacSCANON0!!5[skey_basic:bif(0x0)]/0x2
: (tacSCANON0!!5[skey_basic:bif(0x0)]/0x2)&0x7f
) < 0x20
)


(tacSCANON0!!5[skey_basic:bif(0x0)]&0x1) == 0x1 && tacSCANON0!!5[skey_basic:bif(0x0)]/0x2 < 0x20
||
(tacSCANON0!!5[skey_basic:bif(0x0)]&0x1) == 0x0 && (tacSCANON0!!5[skey_basic:bif(0x0)]/0x2)&0x7f < 0x20
```

;### Assumptions on array elements
;
;TODO
Loading