Sitvanit/add curve #14
Conversation
CVLByExample/Curve/README.md
Outdated
|
|
||
| #Curve | ||
|
|
||
| This directory contains the contract Curve which has the read only reentrancy weakness. |
There was a problem hiding this comment.
| This directory contains the contract Curve which has the read only reentrancy weakness. | |
| This directory contains the Curve contract which has the read only reentrancy weakness. |
CVLByExample/Curve/README.md
Outdated
|
|
||
|
|
||
| ##Specs | ||
| certora/specs contains two spec files for exposing this weakness. |
There was a problem hiding this comment.
| certora/specs contains two spec files for exposing this weakness. | |
| `certora/specs` contains two spec files for exposing this weakness. |
CVLByExample/Curve/README.md
Outdated
| ##Specs | ||
| certora/specs contains two spec files for exposing this weakness. | ||
|
|
||
| 1. BuiltinViewReentrancy.spec uses the builtin rule viewReentrancy that checks that for every solidity function and every |
There was a problem hiding this comment.
| 1. BuiltinViewReentrancy.spec uses the builtin rule viewReentrancy that checks that for every solidity function and every | |
| 1. `BuiltinViewReentrancy.spec` uses the builtin rule `viewReentrancy` that checks that for every Solidity function and every |
changes of this style should be applied everywhere, not adding more comments on it
CVLByExample/Curve/README.md
Outdated
|
|
||
| 1. BuiltinViewReentrancy.spec uses the builtin rule viewReentrancy that checks that for every solidity function and every | ||
| view function the read only reentrancy weakness is not present. | ||
| 2. ViewReentrancy.spec uses regular rules for checking that for every solidity function but only for the view function |
There was a problem hiding this comment.
the sentence is not coherent
CVLByExample/Curve/README.md
Outdated
| 1. The value of getVirtualPrice() at the current state. | ||
| 2. The value of getVirtualPrice() before the unresolved call present in the solidity function. | ||
| 3. The value of getVirtualPrice() after the unresolved call present in the solidity function. | ||
| 4. The existence of read only weakness with respect to getVirtualPrice(). |
There was a problem hiding this comment.
| 4. The existence of read only weakness with respect to getVirtualPrice(). | |
| 4. The existence of a read only weakness with respect to getVirtualPrice(). |
|
|
||
|
|
||
|
|
||
| // constructor(uint256 _future_A_time, uint256 _future_A, uint256 _initial_A_time, uint256 _initial_A, address owner ) { |
| } | ||
|
|
||
|
|
||
| // function get_D(uint xp_0, uint xp_1) |
| return xp[0] + xp[1]; | ||
| // Simplification end | ||
|
|
||
| for (uint256 _x=0;_x<xp.length;_x++){ |
There was a problem hiding this comment.
this is the original code and currently it's unreachable. it cleaner to just remove or comment out with a comment saying we simplified this function, and why it's okay in the context of read-only reentrancy checks
There was a problem hiding this comment.
I guess everything after the line 65 (return xp[0] + xp[1];) in this function is unreachable and redundant.
There was a problem hiding this comment.
Commented out but @DanieLion55 please review as you are the author.
| // uint256 x; | ||
| // return _DEMO_D; | ||
| // return _DEMO_D_MAPPING[xp[0]][xp[1]][amp]; | ||
| return xp[0] + xp[1]; |
There was a problem hiding this comment.
not really unconstrained ghost...
There was a problem hiding this comment.
I guess you mean not unconstrained const. Removed from the comment.
| uint256 S = 0; | ||
| uint256 Dprev = 0; | ||
| // Demo simplificaiton - unconstrained CONST | ||
| // get_D currently crashes the prover's pre-SMT analysis or something |
There was a problem hiding this comment.
we need to say that to reduce the running time of the example this function was simplified
| function _A() view internal returns(uint256) { | ||
|
|
||
| // Demo simplificaiton - return unconstrained CONST | ||
| return future_A; |
There was a problem hiding this comment.
Everything in this function after this line is redundant.
There was a problem hiding this comment.
Commented out. Might be needed later for a better simplification.
| revert(); | ||
| } | ||
|
|
||
| function _A() view internal returns(uint256) { |
There was a problem hiding this comment.
I think we should add some documentation for this function.
Also, I would prefer a more meaningful name than _A.
There was a problem hiding this comment.
I don't understand the meaning of A, D and others. @DanieLion55 ?
There was a problem hiding this comment.
A, D are the names from the original Curve so better leave them. I added comments on what I know.
|
|
||
| // function get_D(uint xp_0, uint xp_1) | ||
|
|
||
| function get_D(uint256[2] memory xp,uint256 amp) public view returns(uint256) { |
There was a problem hiding this comment.
Can you add an explanation as to what this function does?
There was a problem hiding this comment.
I just commented on the symplification. I don't understand the original function. @DanieLion55 ?
| f(e, data); | ||
| require after_func1 == getVirtualPrice(e_external); | ||
| assert cond; | ||
| } |
There was a problem hiding this comment.
this is extremely hard to understand, lets wait for the summarization that can call solidity and it will be clean and easy to follow.
all this example should move under readonlyReentrancy folder
Add contract Curve with 2 specs: regular rule and builtin rule. This is using the munge version.