Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Summary for uniswapV2LibraryGetAmountOut and uniswapV2LibraryGetAmountIn #35

Merged
merged 4 commits into from
Sep 23, 2024
Merged

Summary for uniswapV2LibraryGetAmountOut and uniswapV2LibraryGetAmountIn #35

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9962dc2
Summary for `uniswapV2LibraryGetAmountOut`
Robertorosmaninho Sep 19, 2024
c61031b
Summary for `uniswapV2LibraryGetAmountIn`
Robertorosmaninho Sep 19, 2024
ab826f8
Merge branch 'main' into getamountout-summary
Robertorosmaninho Sep 19, 2024
3cf87df
Merge branch 'main' into getamountout-summary
Robertorosmaninho Sep 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 50 additions & 0 deletions src/uniswap-summaries.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2679,6 +2679,53 @@ endmodule
```

```k
module SOLIDITY-UNISWAP-GETAMOUNTOUT-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-UNISWAP-TOKENS

rule <k> uniswapV2LibraryGetAmountOut:Id ( v(V1:MInt{256}, uint256 #as T), v(V2:MInt{256}, T), v(V3:MInt{256}, T), .TypedVals ) => v((V1 *MInt 997p256 *MInt V3) /uMInt (V2 *MInt 1000p256 +MInt V1 *MInt 997p256), T) ...</k>
<summarize> true </summarize>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
ListItem((V1 *MInt 997p256 *MInt V3) /uMInt (V2 *MInt 1000p256 +MInt V1 *MInt 997p256) ) // amountOut
ListItem( V1 *MInt 997p256) // amountInWithFee
ListItem( V1 *MInt 997p256 *MInt V3) // numerator
ListItem( V2 *MInt 1000p256 +MInt V1 *MInt 997p256) // denominator
</store>
requires V1 >uMInt 0p256 andBool V2 >uMInt 0p256 andBool V3 >uMInt 0p256 [priority(40)]

endmodule
```

```k
module SOLIDITY-UNISWAP-GETAMOUNTIN-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-UNISWAP-TOKENS

rule <k> uniswapV2LibraryGetAmountIn:Id ( v(V1:MInt{256}, uint256 #as T), v(V2:MInt{256}, T), v(V3:MInt{256}, T), .TypedVals ) => v(((V2 *MInt V1 *MInt 1000p256) /uMInt ((V3 -MInt V1) *MInt 997p256)) +MInt 1p256, T) ...</k>
<summarize> true </summarize>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
ListItem(((V2 *MInt V1 *MInt 1000p256) /uMInt ((V3 -MInt V1) *MInt 997p256)) +MInt 1p256) // amountIn
ListItem(V2 *MInt V1 *MInt 1000p256) // numerator
ListItem((V3 -MInt V1) *MInt 997p256) // denominator
</store>
requires V1 >uMInt 0p256 andBool V2 >uMInt 0p256 andBool V3 >uMInt 0p256
andBool ((V3 -MInt V1) *MInt 997p256) =/=MInt 0p256 [priority(40)]


rule <k> uniswapV2LibraryGetAmountIn:Id ( v(V1:MInt{256}, uint256 #as T), v(V2:MInt{256}, T), v(V3:MInt{256}, T), .TypedVals ) => v(1p256, T) ...</k>
<summarize> true </summarize>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
ListItem(1p256) // amountIn
ListItem(V2 *MInt V1 *MInt 1000p256) // numerator
ListItem((V3 -MInt V1) *MInt 997p256) // denominator
</store>
requires V1 >uMInt 0p256 andBool V2 >uMInt 0p256 andBool V3 >uMInt 0p256
andBool ((V3 -MInt V1) *MInt 997p256) ==MInt 0p256 [priority(40)]

endmodule
```

```k
module SOLIDITY-UNISWAP-PAIRFOR-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-EXPRESSION
Expand Down Expand Up @@ -2731,6 +2778,9 @@ endmodule
module SOLIDITY-UNISWAP-SUMMARIES
imports SOLIDITY-UNISWAP-INIT-SUMMARY
imports SOLIDITY-UNISWAP-SORTTOKENS-SUMMARY
imports SOLIDITY-UNISWAP-GETAMOUNTOUT-SUMMARY
imports SOLIDITY-UNISWAP-GETAMOUNTIN-SUMMARY
imports SOLIDITY-UNISWAP-PAIRFOR-SUMMARY

endmodule
```