Skip to content

Commit

Permalink
Summary fidUpdate function with 3 parameters (#41)
Browse files Browse the repository at this point in the history 
* Introducing `fidUpdate` summary

* Renaming `fidUpdate`with 4 parameters

* Deleting trailing whitespaces
  • Loading branch information
@Robertorosmaninho
Robertorosmaninho authored Sep 25, 2024
1 parent 82b5ff5 commit 57ce82c
Showing 1 changed file with 77 additions and 12 deletions.
89 changes: 77 additions & 12 deletions src/uniswap-summaries.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ module SOLIDITY-UNISWAP-INIT-SUMMARY
rule <k> _:Program => .K ...</k>
<summarize> true </summarize>
(_:CompileCell =>
(_:CompileCell =>
<compile>
<current-body>
uniswapV2SwapTest
Expand Down Expand Up @@ -2682,7 +2682,7 @@ endmodule
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)
Expand Down Expand Up @@ -2725,7 +2725,7 @@ module SOLIDITY-UNISWAP-GETAMOUNTIN-SUMMARY
endmodule
```

```k
```k
module SOLIDITY-UNISWAP-PAIRFOR-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-EXPRESSION
Expand Down Expand Up @@ -2775,7 +2775,7 @@ endmodule
```

```k
module SOLIDITY-UNISWAP-FIDUPDATE-SUMMARY
module SOLIDITY-UNISWAP-FIDUPDATE-4-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-UNISWAP-TOKENS
Expand All @@ -2785,7 +2785,7 @@ module SOLIDITY-UNISWAP-FIDUPDATE-SUMMARY
<contract-address> THIS </contract-address>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3) ListItem(V4)
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3) ListItem(V4)
ListItem(roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32}) // blockTimestamp
ListItem(roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32} -MInt {Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}) // timeElapsed
</store>
Expand All @@ -2794,9 +2794,9 @@ module SOLIDITY-UNISWAP-FIDUPDATE-SUMMARY
[ price1CumulativeLast <- {Storage[price1CumulativeLast] orDefault 0p256}:>MInt{256} +MInt roundMInt(V3:MInt{112} /uMInt V4:MInt{112}):MInt{256} *MInt roundMInt(roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32} -MInt {Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}):MInt{256} ]
[ reserve0 <- roundMInt(V1):MInt{112} ]
[ reserve1 <- roundMInt(V2):MInt{112} ]
</contract-storage>
</contract-storage>
<block-timestamp> Timestamp </block-timestamp>
requires V1 <=uMInt {Storage[constUINT112MAX] orDefault 0p256}:>MInt{256}
requires V1 <=uMInt {Storage[constUINT112MAX] orDefault 0p256}:>MInt{256}
andBool V2 <=uMInt {Storage[constUINT112MAX] orDefault 0p256}:>MInt{256}
andBool (roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32} -MInt {Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}) >uMInt 0p32
andBool V3 =/=MInt 0p112
Expand All @@ -2809,31 +2809,96 @@ module SOLIDITY-UNISWAP-FIDUPDATE-SUMMARY
<contract-address> THIS </contract-address>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3) ListItem(V4)
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3) ListItem(V4)
ListItem(roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32}) // blockTimestamp
ListItem(roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32} -MInt {Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}) // timeElapsed
</store>
<contract-storage> Storage => Storage [ blockTimestampLast <- roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32} ]
[ reserve0 <- roundMInt(V1):MInt{112} ]
[ reserve1 <- roundMInt(V2):MInt{112} ]
</contract-storage>
</contract-storage>
<block-timestamp> Timestamp </block-timestamp>
requires V1 <=uMInt {Storage[constUINT112MAX] orDefault 0p256}:>MInt{256}
andBool V2 <=uMInt {Storage[constUINT112MAX] orDefault 0p256}:>MInt{256}
andBool ((roundMInt(Timestamp %uMInt Int2MInt(2 ^Int 32):MInt{256}):MInt{32} -MInt {Storage[blockTimestampLast] orDefault 0p32}:>MInt{32}) <=uMInt 0p32
orBool V3 ==MInt 0p112
orBool V3 ==MInt 0p112
orBool V4 ==MInt 0p112) [priority(40)]
endmodule
```

```k
module SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-EXPRESSION
imports SOLIDITY-UNISWAP-TOKENS
// from == 0p160 and to == 0p160
rule <k> fidUpdate:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), v(V3:MInt{256}, uint256)) => void ...</k>
<summarize> true </summarize>
<this> THIS </this>
<contract-address> THIS </contract-address>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3) </store>
requires V1 ==MInt 0p160 andBool V2 ==MInt 0p160 [priority(40)]
// from == 0p160 and to != 0p160
rule <k> fidUpdate:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), v(V3:MInt{256}, uint256)) => void ...</k>
<summarize> true </summarize>
<this> THIS </this>
<contract-address> THIS </contract-address>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3) </store>
<contract-storage> Storage => Storage [ vidTotalSupply <- {Storage[vidTotalSupply] orDefault 0p256}:>MInt{256} +MInt V3:MInt{256} ]
[ vidBalances <- write({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V2), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V2), (mapping ( address account => uint256 )))}:>MInt{256} +MInt V3:MInt{256}), (mapping ( address account => uint256))) ]
</contract-storage>
requires V1 ==MInt 0p160 andBool V2 =/=MInt 0p160 [priority(40)]
// from != 0p160 and to == 0p160
rule <k> fidUpdate:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), v(V3:MInt{256}, uint256)) => void ...</k>
<summarize> true </summarize>
<this> THIS </this>
<contract-address> THIS </contract-address>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
ListItem(read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 ))))
</store>
<contract-storage> Storage => Storage [ vidTotalSupply <- {Storage[vidTotalSupply] orDefault 0p256}:>MInt{256} -MInt V3:MInt{256} ]
[ vidBalances <- write({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} -MInt V3:MInt{256}), (mapping ( address account => uint256))) ]
</contract-storage>
requires V1 =/=MInt 0p160 andBool V2 ==MInt 0p160
andBool {read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} >=uMInt V3:MInt{256} [priority(40)]
// from != 0p160 and to != 0p160
rule <k> fidUpdate:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), v(V3:MInt{256}, uint256)) => void ...</k>
<summarize> true </summarize>
<this> THIS </this>
<contract-address> THIS </contract-address>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<store> S => S ListItem(V1) ListItem(V2) ListItem(V3)
ListItem(read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 ))))
</store>
<contract-storage> Storage => Storage [ vidBalances <- write({write({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} -MInt V3:MInt{256}), (mapping ( address account => uint256)))}:>Value, ListItem(V2), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V2), (mapping ( address account => uint256 )))}:>MInt{256} +MInt V3:MInt{256}), (mapping ( address account => uint256))) ] </contract-storage>
requires V1 =/=MInt 0p160 andBool V2 =/=MInt 0p160
andBool {read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} >=uMInt V3:MInt{256} [priority(40)]
endmodule
```

```k
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
imports SOLIDITY-UNISWAP-FIDUPDATE-SUMMARY
imports SOLIDITY-UNISWAP-FIDUPDATE-4-SUMMARY
imports SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY
endmodule
```
```

0 comments on commit 57ce82c

Please sign in to comment.