From c69fe71d80b42043f98c92f85cc3eb1849638dca Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 26 Sep 2024 13:45:47 -0300 Subject: [PATCH 1/3] Introducing `getReserves` Summary --- src/uniswap-summaries.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 8bf8e8f..604e9a6 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2890,6 +2890,29 @@ module SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY endmodule ``` +```k +module SOLIDITY-UNISWAP-GETRESERVES-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-EXPRESSION + imports SOLIDITY-UNISWAP-TOKENS + + rule reserves = new uint112 [ ] ( 3 , .TypedVals ) ; reserves [ 0 ] = reserve0 ; reserves [ 1 ] = reserve1 ; reserves [ 2 ] = blockTimestampLast ; .Statements ~> return reserves ; ~> .K => return v ( ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) ListItem({Storage[reserve1] orDefault 0p112}:>MInt{112}) ListItem(roundMInt({Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}):MInt{112}) , uint112 [ ] ) ; ~> .K + true + THIS + THIS + TYPE + TYPE + ENV=> ENV [ reserves <- var(1, uint112 []) ] + S => S ListItem( + ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) + ListItem({Storage[reserve1] orDefault 0p112}:>MInt{112}) + ListItem(roundMInt({Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}):MInt{112}) + ) + + Storage [priority(40)] +endmodule +``` + ```k module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-INIT-SUMMARY @@ -2899,6 +2922,7 @@ module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-PAIRFOR-SUMMARY imports SOLIDITY-UNISWAP-FIDUPDATE-4-SUMMARY imports SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY + imports SOLIDITY-UNISWAP-GETRESERVES-SUMMARY endmodule ``` \ No newline at end of file From 58c3316ed2bede78c2dfa59a909584cafe27becd Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 26 Sep 2024 15:29:37 -0300 Subject: [PATCH 2/3] Addinf `bind` to the summary of `getReserves` body --- src/uniswap-summaries.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 604e9a6..b775204 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2896,12 +2896,13 @@ module SOLIDITY-UNISWAP-GETRESERVES-SUMMARY imports SOLIDITY-EXPRESSION imports SOLIDITY-UNISWAP-TOKENS - rule reserves = new uint112 [ ] ( 3 , .TypedVals ) ; reserves [ 0 ] = reserve0 ; reserves [ 1 ] = reserve1 ; reserves [ 2 ] = blockTimestampLast ; .Statements ~> return reserves ; ~> .K => return v ( ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) ListItem({Storage[reserve1] orDefault 0p112}:>MInt{112}) ListItem(roundMInt({Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}):MInt{112}) , uint112 [ ] ) ; ~> .K + rule bind ( _STORE , .List , .List , .TypedVals , ListItem ( uint112 []:TypeName ) , ListItem ( reserves ) ) ~> reserves = new uint112 [ ] ( 3 , .TypedVals ) ; reserves [ 0 ] = reserve0 ; reserves [ 1 ] = reserve1 ; reserves [ 2 ] = blockTimestampLast ; .Statements ~> return reserves ; ~> .K => return v ( ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) ListItem({Storage[reserve1] orDefault 0p112}:>MInt{112}) ListItem(roundMInt({Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}):MInt{112}) , uint112 [ ] ) ; ~> .K true THIS THIS TYPE TYPE + getReserves ENV=> ENV [ reserves <- var(1, uint112 []) ] S => S ListItem( ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) From aba0c51e27f38518b6b50e6beef1d567b80a6e08 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 26 Sep 2024 16:31:42 -0300 Subject: [PATCH 3/3] Fixing `env` cell element setting --- src/uniswap-summaries.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index b775204..865f181 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2903,7 +2903,7 @@ module SOLIDITY-UNISWAP-GETRESERVES-SUMMARY TYPE TYPE getReserves - ENV=> ENV [ reserves <- var(1, uint112 []) ] + ENV=> ENV [ reserves <- var(size(S), uint112 []) ] S => S ListItem( ListItem({Storage[reserve0] orDefault 0p112}:>MInt{112}) ListItem({Storage[reserve1] orDefault 0p112}:>MInt{112})