Summary for sync (#63)

* Sync summaries. * Sync summary: fidUpdate return -> function return. * Added comments.
Pi-Squared-Inc · Oct 15, 2024 · 2818ed2 · 2818ed2
1 parent 4233736
commit 2818ed2
Showing 1 changed file with 45 additions and 0 deletions.
diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
@@ -3703,6 +3703,50 @@ module SOLIDITY-UNISWAP-MINT-SUMMARY
 endmodule
 ```
 
+```k
+module SOLIDITY-UNISWAP-SYNC-SUMMARY
+  imports SOLIDITY-CONFIGURATION
+  imports SOLIDITY-UNISWAP-TOKENS
+  imports SOLIDITY-EXPRESSION
+  imports SOLIDITY-STATEMENT
+
+  // bind to first balanceOf call.
+  // Note that due to the evaluation order of the arguments' list (of fidUpdate),
+  // the call that appears second in the argument list is evaluated first.
+  rule <k> bind ( _STORE , .List , .List , .TypedVals , .List , .List ) ~> fidUpdate ( iERC20 ( token0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , iERC20 ( token1 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) , reserve0 , reserve1 , .TypedVals ) ; Ss:Statements => v ( {S[token1] orDefault 0p160}:>Value , iERC20 ) . balanceOf ( v ( THIS , address ) , .TypedVals ) ~> freezerCallArgumentListTail ( v ( {S[reserve0] orDefault 0p112}:>Value , uint112 ) , v ( {S[reserve1] orDefault 0p112}:>Value , uint112 ) , .TypedVals ) ~> freezerCallArgumentListHead ( iERC20 ( token0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ) ~> freezerCallId ( fidUpdate ) ~> freezerExpressionStatement ( ) ~> Ss ...</k>
+       <summarize> true </summarize>
+       <this> THIS </this>
+       <this-type> TYPE </this-type>
+       <contract-id> TYPE </contract-id>
+       <contract-state>... (token1 |-> address) (reserve0 |-> uint112) (reserve1 |-> uint112) ...</contract-state>
+       <contract-address> THIS </contract-address>
+       <contract-storage> S </contract-storage>
+       <current-function> sync </current-function> [priority(40)]
+
+  // First balanceOf return to second balanceOf call
+  rule <k> v ( B1 , uint256 ) ~> freezerCallArgumentListTail ( v ( R0 , uint112 ) , v ( R1 , uint112 ) , .TypedVals ) ~> freezerCallArgumentListHead ( iERC20 ( token0 , .TypedVals ) . balanceOf ( address ( this , .TypedVals ) , .TypedVals ) ) =>  v ( {S[token0] orDefault 0p160}:>Value , iERC20 ) . balanceOf ( v ( THIS , address ) , .TypedVals ) ~> freezerCallArgumentListTail ( v ( B1 , uint256 ) , v ( R0 , uint112 ) , v ( R1 , uint112 ) , .TypedVals ) ...</k>
+       <summarize> true </summarize>
+       <this> THIS </this>
+       <this-type> TYPE </this-type>
+       <contract-id> TYPE </contract-id>
+       <contract-state>... (token0 |-> address) ...</contract-state>
+       <contract-address> THIS </contract-address>
+       <contract-storage> S </contract-storage>
+       <current-function> sync </current-function> [priority(40)]
+
+  // Second balanceOf return to fidUpdate call
+  rule <k>  v ( B0 , uint256 ) ~> freezerCallArgumentListTail ( v ( B1 , uint256 ) , v ( R0 , uint112 ) , v ( R1 , uint112 ) , .TypedVals ) ~> freezerCallId ( fidUpdate ) => fidUpdate ( v ( B0 , uint256 ) , v ( B1 , uint256 ) , v ( R0 , uint112 ) , v ( R1 , uint112 ) , .TypedVals ) ...</k>
+       <summarize> true </summarize>
+       <current-function> sync </current-function> [priority(40)]
+
+  // fidUpdate return to function return
+  rule <k> void ~> freezerExpressionStatement ( ) ~> .Statements ~> return void ; ~> .K => return void ; ~> .K </k>
+       <summarize> true </summarize>
+       <current-function> sync </current-function> [priority(40)]
+
+endmodule
+```
+
 ```k
 module SOLIDITY-UNISWAP-APPROVE-SUMMARY
   imports SOLIDITY-CONFIGURATION
@@ -3808,6 +3852,7 @@ module SOLIDITY-UNISWAP-SUMMARIES
   imports SOLIDITY-UNISWAP-SETUP-SUMMARY
   imports SOLIDITY-MATHSQRT-SUMMARY
   imports SOLIDITY-UNISWAP-MINT-SUMMARY
+  imports SOLIDITY-UNISWAP-SYNC-SUMMARY
   imports SOLIDITY-UNISWAP-APPROVE-SUMMARY
   imports SOLIDITY-UNISWAP-TRANSFERFROM-SUMMARY