[DOC-367] persistent ghosts explained with examples #177
Conversation
| 1. A call to `a.transfer` which cannot be resolved and results in a havoc operation. Non-persistent ghosts are havoced, in particular `reentrancy_happened`. | ||
| 2. A `CALL` hook executes, updating `reentrancy_happened` based on its havoced value, meaning it can turn to true. | ||
|
|
||
| Therefore even if the addresses of `a` and `NotReentrant` are distinct, we could still falsely detect a reentrant call as `reentrancy_happened` was set to true due to non-determinism. |
There was a problem hiding this comment.
I think this is pretty opaque. Worth expanding on why this can happen:
"During a havoc operation, the prover conservatively assumes that almost any possible behavior can occur. In particular, it must assume that during the execution of the transfer call, some reentrancy occurs, and thus considers the case where reentrancy_happened is set to true. Thus, when the CALL hook executes, it does so where the reentrancy_happened value is already true, and thus the value after the hook will remain true."
or something
There was a problem hiding this comment.
reentrancy actually cannot occur. It does not matter because reentrancy_happened is in some state we track based on contracts, not tied to a particular contract. I added the wordier explanation, although for me it's harder to grasp
docs/cvl/ghosts.md
Outdated
|
|
||
| It is expected that the method `userDefinedRequireMsg` and only it will satisfy the rule. |
There was a problem hiding this comment.
"it is expected that the method userDefinedRequireMsg..." is not a complete fragment. I think you forgot a verb?
There was a problem hiding this comment.
"will satisfy". tried to reword
docs/cvl/ghosts.md
Outdated
| It is expected that the method `userDefinedRequireMsg` and only it will satisfy the rule. | ||
| However, if we use regular ghosts, the ghost variable `saw_user_defined_revert_msg` will revert in case the input argument `a` is equal to 0, together with the contract itself. | ||
| This means the value of `saw_user_defined_revert_msg` will remain false, and thus the `satisfy` statement will fail. | ||
| With regular ghosts, the rule would of course fail also for the two other methods, meaning that non-persistent ghosts are not suitable for distinguishing between different reverts. |
There was a problem hiding this comment.
I've read this so many times, and I still have no idea what it's saying.
mdgeorge4153
changed the title
Before requesting review:
spelling_wordlist.txtREADME.mdfor information about style and markdown syntaxJira ticket: TODO
Link to generated documentation: TODO