From dd6d2d0f2be0564a8d87d871e16717ebcf55d059 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 10 Oct 2024 16:48:42 -0300 Subject: [PATCH] Introducing `transferFrom` function summary on `dAIMock` (#58) * Introducing `transferFrom` function summary on `dAIMock` * Adding requires clause to if-not case * Adding `` and renaming types correctly * Adding rule for if-true case * Addressing comments --------- Co-authored-by: Maria Kotsifakou --- src/uniswap-summaries.md | 55 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index 8febe0e..897dafc 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -3670,6 +3670,60 @@ module SOLIDITY-UNISWAP-APPROVE-SUMMARY endmodule ``` +```k +module SOLIDITY-UNISWAP-TRANSFERFROM-SUMMARY + imports SOLIDITY-CONFIGURATION + imports SOLIDITY-EXPRESSION + imports SOLIDITY-UNISWAP-TOKENS + + rule transferFrom:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), v(V3:MInt{256}, uint256), .TypedVals ) => v ( true , bool ) ... + true + THIS + TYPE + TYPE + THIS + SENDER + ... + (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) + (balanceOf |-> mapping ( address daiact => uint256 )) + (constUINTMAX |-> uint256) ... + + S => S ListItem(V1) // src + ListItem(V2) // dst + ListItem(V3) // wad + + Storage => Storage [ balanceOf <- write({write({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), ({read({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiact => uint256 )))}:>MInt{256} -MInt V3:MInt{256}), (mapping ( address daiact => uint256))) }:>Value, ListItem(V2), ({read({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V2), (mapping ( address daiact => uint256 )))}:>MInt{256} +MInt V3:MInt{256}), (mapping ( address daiact => uint256))) ] + + requires {read({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiact => uint256 )))}:>MInt{256} >=uMInt V3:MInt{256} // balanceOf[src] >= wad + andBool (V1 ==MInt SENDER orBool {read(read({Storage [ allowance ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiownr => mapping ( address daispdr => uint256 ) ))), ListItem(SENDER), (mapping ( address daispdr => uint256 )))}:>MInt{256} ==MInt {Storage[constUINTMAX] orDefault 0p256}:>MInt{256}) [priority(40)] + + rule transferFrom:Id ( v(V1:MInt{160}, address #as T), v(V2:MInt{160}, T), v(V3:MInt{256}, uint256), .TypedVals ) => v ( true , bool ) ... + true + THIS + TYPE + TYPE + THIS + SENDER + ... + (allowance |-> mapping ( address daiownr => mapping ( address daispdr => uint256 ) )) + (balanceOf |-> mapping ( address daiact => uint256 )) + (constUINTMAX |-> uint256) ... + + S => S ListItem(V1) // src + ListItem(V2) // dst + ListItem(V3) // wad + + Storage => Storage [ balanceOf <- write({write({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), ({read({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiact => uint256 )))}:>MInt{256} -MInt V3:MInt{256}), (mapping ( address daiact => uint256))) }:>Value, ListItem(V2), ({read({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V2), (mapping ( address daiact => uint256 )))}:>MInt{256} +MInt V3:MInt{256}), (mapping ( address daiact => uint256))) ] + [ allowance <- write({ Storage [ allowance ] orDefault .Map}:>Value, ListItem(V1), write(read({Storage [ allowance ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiownr => mapping ( address daispdr => uint256 )))), ListItem(SENDER), {read(read( {Storage [ allowance ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiownr => mapping ( address daispdr => uint256 )))), ListItem(SENDER), (mapping ( address daispdr => uint256 )))}:>MInt{256} -MInt V3:MInt{256}, (mapping ( address daispdr => uint256 ))), (mapping ( address daiownr => mapping ( address daispdr => uint256 )))) ] + + requires {read({Storage [ balanceOf ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiact => uint256 )))}:>MInt{256} >=uMInt V3:MInt{256} // balanceOf[src] >= wad + andBool (V1 =/=MInt SENDER andBool {read(read({Storage [ allowance ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiownr => mapping ( address daispdr => uint256 ) ))), ListItem(SENDER), (mapping ( address daispdr => uint256 )))}:>MInt{256} =/=MInt {Storage[constUINTMAX] orDefault 0p256}:>MInt{256}) // src != msg.sender && allowance[src][msg.sender] != constUINTMAX + andBool {read(read({Storage [ allowance ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address daiownr => mapping ( address daispdr => uint256 ) ))), ListItem(SENDER), (mapping ( address daispdr => uint256 )))}:>MInt{256} >=uMInt V3:MInt{256} // allowance[src][msg.sender] >= wad + [priority(40)] + +endmodule +``` + ```k module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-UNISWAP-INIT-SUMMARY @@ -3688,6 +3742,7 @@ module SOLIDITY-UNISWAP-SUMMARIES imports SOLIDITY-MATHSQRT-SUMMARY imports SOLIDITY-UNISWAP-MINT-SUMMARY imports SOLIDITY-UNISWAP-APPROVE-SUMMARY + imports SOLIDITY-UNISWAP-TRANSFERFROM-SUMMARY endmodule ```