diff --git a/src/solidity.md b/src/solidity.md index 3b55f6b..82ad844 100644 --- a/src/solidity.md +++ b/src/solidity.md @@ -181,7 +181,7 @@ module SOLIDITY imports SOLIDITY-TRANSACTION imports SOLIDITY-EXPRESSION imports SOLIDITY-STATEMENT - imports SOLIDITY-UNISWAP-INIT-SUMMARY + imports SOLIDITY-UNISWAP-SUMMARIES rule _:PragmaDefinition Ss:SourceUnits => Ss ... false diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index f6969e4..6f1e0ad 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2648,3 +2648,39 @@ module SOLIDITY-UNISWAP-INIT-SUMMARY endmodule ``` + +```k +module SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-EXPRESSION + imports SOLIDITY-UNISWAP-TOKENS + + rule uniswapV2LibrarySortTokens:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), .TypedVals ) => v(ListItem(V1) ListItem(V2), T[]) ... + true + + S => S ListItem(V1) + ListItem(V2) + ListItem(default(T[])) + ListItem(ListItem(V1) ListItem(V2)) + + requires V1 uniswapV2LibrarySortTokens:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), .TypedVals ) => v(ListItem(V2) ListItem(V1), T[]) ... + true + + S => S ListItem(V1) + ListItem(V2) + ListItem(default(T[])) + ListItem(ListItem(V2) ListItem(V1)) + + requires V2