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

Introducing approve summary from bind to return on dAIMock #56

Merged
merged 6 commits into from
Oct 8, 2024
Merged

Introducing approve summary from bind to return on dAIMock #56

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
be92a25
Introducing `approve` summary from `bind` to `return` on `dAIMock`
Robertorosmaninho Oct 4, 2024
b331b19
Deleting temporary symbol
Robertorosmaninho Oct 7, 2024
22d2494
Fixing approve rule
Robertorosmaninho Oct 7, 2024
7e3e5f3
Merge branch 'main' into approve-dAIMock-summary
Robertorosmaninho Oct 7, 2024
13975b9
Matching contract-state
Robertorosmaninho Oct 8, 2024
380d252
Merge branch 'main' into approve-dAIMock-summary
Robertorosmaninho Oct 8, 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
36 changes: 35 additions & 1 deletion src/uniswap-summaries.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3493,7 +3493,7 @@ module SOLIDITY-UNISWAP-MINT-SUMMARY
ListItem(V2) // wad
</store>
<env>
ENV => ENV [ usr <- var(size(S) , address) ]
ENV => ENV [ usr <- var(size(S) , address) ]
[ wad <- var(size(S) +Int 1, uint256) ]
</env>
<contract-storage> Storage => Storage [ totalSupply <- {Storage[totalSupply] orDefault 0p256}:>MInt{256} +MInt V2:MInt{256} ]
Expand All @@ -3502,6 +3502,39 @@ module SOLIDITY-UNISWAP-MINT-SUMMARY
endmodule
```

```k
module SOLIDITY-UNISWAP-APPROVE-SUMMARY
imports SOLIDITY-CONFIGURATION
imports SOLIDITY-EXPRESSION
imports SOLIDITY-UNISWAP-TOKENS

rule <k> bind ( _STORE,
ListItem ( usr ) ListItem ( wad ),
ListItem ( address ) ListItem ( uint256 ) ,
v ( V1:MInt{160} , address ),
v ( V2:MInt{256} , uint256 ),
.TypedVals , ListItem ( bool ) , ListItem ( noId ) ) ~> allowance [ msg . sender ] [ usr ] = wad ; emit approvalEvent ( msg . sender , usr , wad , .TypedVals ) ; return true ; .Statements ~> return void ; ~> .K => return v ( true , bool ) ; ~> .Statements ~> return void ; ... </k>
<summarize> true </summarize>
<this> THIS </this>
<contract-address> THIS </contract-address>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<current-function> approve </current-function>
<contract-state> (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) </contract-state>
<store> S => S ListItem(V1) // usr
ListItem(V2) // wad
</store>
<env>
ENV => ENV [ usr <- var(size(S) , address) ]
[ wad <- var(size(S) +Int 1, uint256) ]
</env>
<msg-sender> SENDER </msg-sender>
<contract-storage>
Storage => Storage [ allowance <- write( { Storage [ allowance ] orDefault .Map}:>Value, ListItem(SENDER), write(read({Storage [ allowance ] orDefault .Map}:>Value, ListItem(SENDER), (mapping ( address daiownr => mapping ( address daispdr => uint256)))), ListItem(V1), V2:MInt{256}, (mapping ( address spender => uint256 ))),(mapping ( address daiownr => mapping ( address daispdr => uint256))))]
</contract-storage> [priority(40)]
endmodule
```

```k
module SOLIDITY-UNISWAP-SUMMARIES
imports SOLIDITY-UNISWAP-INIT-SUMMARY
Expand All @@ -3519,6 +3552,7 @@ module SOLIDITY-UNISWAP-SUMMARIES
imports SOLIDITY-UNISWAP-SETUP-SUMMARY
imports SOLIDITY-MATHSQRT-SUMMARY
imports SOLIDITY-UNISWAP-MINT-SUMMARY
imports SOLIDITY-UNISWAP-APPROVE-SUMMARY

endmodule
```