uniswapV2LibraryGetAmountsOut summary

[mariaKt]

This PR adds summarized rules for function uniswapV2LibraryGetAmountsOut.

solidity-demo-semantics/test/examples/swaps/UniswapV2SwapRenamed.sol

Line 256 in c94634e

function uniswapV2LibraryGetAmountsOut(uint amountIn, address[] memory path) private returns (uint[] memory amounts) {

These rules are saving 644 steps.

I would like your opinion for this rule here

  // Skip environment updates when not needed.
  // These occur due to the multiple block statements, introduced by the if
  // statement that the while rewrites to.
  rule <k> restoreEnv( _:Map ) ~> .Statements ~> restoreEnv( E:Map ) => restoreEnv(E) ...</k>
       <summarize> true </summarize>
       <current-function> uniswapV2LibraryGetAmountsOut </current-function> [priority(40)]

This is the same question as in this PR, about whether it is OK to add this rule as a summarized rule.

[Robertorosmaninho]

The same questions in this PR apply here, and I have another one: When using just the <current-function> is enough?

Otherwise, it looks good! The comments really help a lot to better understand it. If we can have more on the <store> cell, it would be even more helpful.

About your question on the current PR description and in this PR, it seems ok to me. Not sure if @dwightguth, knows something more that say this can be prejudicial or is wrong in some way.