From be92a259bd198287e19e291d0bcf016bc7892ef1 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Fri, 4 Oct 2024 17:19:52 -0300 Subject: [PATCH 1/4] Introducing `approve` summary from `bind` to `return` on `dAIMock` --- src/uniswap-summaries.md | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 350e009..86ab7ff 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3430,7 +3430,7 @@ module SOLIDITY-UNISWAP-MINT-SUMMARY ListItem(V2) // wad - ENV => ENV [ usr <- var(size(S) , address) ] + ENV => ENV [ usr <- var(size(S) , address) ] [ wad <- var(size(S) +Int 1, uint256) ] Storage => Storage [ totalSupply <- {Storage[totalSupply] orDefault 0p256}:>MInt{256} +MInt V2:MInt{256} ] @@ -3439,6 +3439,40 @@ module SOLIDITY-UNISWAP-MINT-SUMMARY endmodule ``` +```k +module SOLIDITY-UNISWAP-APPROVE-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-EXPRESSION + imports SOLIDITY-UNISWAP-TOKENS + + syntax KItem ::= "stopFunction" + + rule 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 ) ; ... + true + THIS + THIS + TYPE + TYPE + approve + S => S ListItem(V1) // usr + ListItem(V2) // wad + + + ENV => ENV [ usr <- var(size(S) , address) ] + [ wad <- var(size(S) +Int 1, uint256) ] + + SENDER + + Storage => Storage [ allowance <- write( {Storage [ allowance ] orDefault .Map}:>Value, ListItem(SENDER), (V1 |-> V2:MInt{256}), (mapping ( address daiownr => mapping ( address daispdr => uint256))) )] + [priority(40)] +endmodule +``` + ```k module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-INIT-SUMMARY @@ -3455,6 +3489,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 ``` From b331b19be433f6cadf714ba75263283c78dc8472 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Mon, 7 Oct 2024 08:50:29 -0300 Subject: [PATCH 2/4] Deleting temporary symbol --- src/uniswap-summaries.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 86ab7ff..5fe5103 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3445,8 +3445,6 @@ module SOLIDITY-UNISWAP-APPROVE-SUMMARY imports SOLIDITY-EXPRESSION imports SOLIDITY-UNISWAP-TOKENS - syntax KItem ::= "stopFunction" - rule bind ( _STORE, ListItem ( usr ) ListItem ( wad ), ListItem ( address ) ListItem ( uint256 ) , From 22d2494aa29fefe10b318910ed8746f99fa3026f Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Mon, 7 Oct 2024 17:37:42 -0300 Subject: [PATCH 3/4] Fixing approve rule --- src/uniswap-summaries.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 5fe5103..67d23bc 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3450,7 +3450,7 @@ module SOLIDITY-UNISWAP-APPROVE-SUMMARY 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 ) ; ... + .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 ; ... true THIS THIS @@ -3466,7 +3466,7 @@ module SOLIDITY-UNISWAP-APPROVE-SUMMARY SENDER - Storage => Storage [ allowance <- write( {Storage [ allowance ] orDefault .Map}:>Value, ListItem(SENDER), (V1 |-> V2:MInt{256}), (mapping ( address daiownr => mapping ( address daispdr => uint256))) )] + 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))))] [priority(40)] endmodule ``` From 13975b93de7a416407a5a0eba4f3d45e3ed28955 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 8 Oct 2024 14:36:27 -0300 Subject: [PATCH 4/4] Matching contract-state --- src/uniswap-summaries.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 4547f74..7306d7a 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3519,6 +3519,7 @@ module SOLIDITY-UNISWAP-APPROVE-SUMMARY TYPE TYPE approve + (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) S => S ListItem(V1) // usr ListItem(V2) // wad