Skip to content
This repository was archived by the owner on Aug 20, 2021. It is now read-only.

Commit edcd218

Browse files
d-xoxwvvvvwx
authored andcommitted
acts.md: document isStatic
1 parent adc0de8 commit edcd218

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

acts.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,13 @@ storage
7474
#hashedLocation("Solidity", 0, Someone) |-> PreStateValue => PostStateValue
7575
7676
```
77+
78+
### Static vs Non-Static `act` Specifications
79+
80+
An `act` that does not specify any storage updates (i.e. the storage block contains no `=>` arrows) will generate a `K` reachability claim where the value of the `<static>` cell is set to `_`. Conversely, an `act` with a storage block containing at least one `=>` will have the `<static>` cell in the resulting reachability claim set to `false`.
81+
82+
When running `klab prove`, the `<static>` cell will set to `true` during a `STATICCALL` and `false` otherwise.
83+
7784
## Example: Token
7885
Now we are ready to verify a (simplified) ERC20 token:
7986
```Solidity

0 commit comments

Comments
 (0)