Some summaries for swap. #57
Conversation
of new scope to if condition evaluation.
| // Bind to getReserves call | ||
| rule <k> bind ( _STORE , ListItem(amount0Out) ListItem(amount1Out) ListItem(to) , ListItem(uint256) ListItem(uint256) ListItem(address) , v(V1, uint256), v(V2, uint256), v(V3, address), .TypedVals, .List, .List) ~> require ( amount0Out > 0 || amount1Out > 0 , "UniswapV2: INSUFFICIENT_OUTPUT_AMOUNT" , .TypedVals ) ; uint112 [ ] memory reserves = getReserves ( .TypedVals ) ; Ss:Statements => getReserves ( .TypedVals ) ~> freezerVariableDeclarationStatementA ( uint112 [ ] memory reserves ) ~> Ss ...</k> | ||
| <summarize> true </summarize> | ||
| <env> .Map => .Map (amount0Out |-> var(size(S), uint256)) |
There was a problem hiding this comment.
I usually do ENV => ENV... to be more generic even when it starts as .Map on the --depth .... Is using .Map instead the right way to do it?
There was a problem hiding this comment.
Well, there is no right or wrong, it is just unneeded generality here that potentially can let mistakes through, so why let it through?
To elaborate, I agree with being as generic as possible. But, not when that might lead to matching something that is wrong. In this case, a non empty environment would be a mistake. Since we are at the beginning of a function call, <env> should always be empty. We would not want to be able to match if this ever was, for some reason, not empty.
There was a problem hiding this comment.
There are cases when <env> is empty but would not always be, in all executions. In those cases, ENV => ENV ... is definitely right.
At least, that is how I am thinking about it.
There was a problem hiding this comment.
Makes sense! Thanks for the clarification!
This PR includes some summaries for swap. They do not cover all of the function yet.
The steps are reduced by 878 (from 19933 to 19055).