Summaries for SortTokens function (for non reverting cases).

Pi-Squared-Inc / solidity-demo-semantics

Demonstration Solidity Semantics in K

2 stars 2 forks source link

Summaries for SortTokens function (for non reverting cases). #34

Closed mariaKt closed 1 month ago

mariaKt commented 2 months ago

This PR adds the first summarized rules w.r.t. program execution. These two rules summarize the uniswapV2LibrarySortTokens function. We focus on the two cases that satisfy the requires clauses, and thus will not revert. Each rule summarizes the execution of about 114 steps.