updated

Author: xqyww123

Uniswap_Pool.phi-cache

@@ -57,7 +57,6 @@ proc (nodef) fee[\<phi>synthesis 1100]:
   output \<open>fee_rate \<Ztypecolon> \<v>\<a>\<l> \<real>\<close>
   \<medium_left_bracket> apply_rule op_const_areal[where x=fee_rate] \<medium_right_bracket>.
 
-
 locale Pool = Tickmap_spec + Tick_spec +
   fixes Pool :: \<open>(fiction, pool) \<phi>\<close>
     and op_get_pool_price :: \<open>VAL proc\<close>
@@ -231,7 +230,7 @@ proc swap:
     \<open>0 \<Ztypecolon> \<real>\<close> \<rightarrow> var amount_calculated
     get_pool_price \<rightarrow> var price
     get_pool_tick \<rightarrow> var tick
-    sel (\<open>growth.fee0 (pool.growth _)\<close> \<open>growth.fee1 (pool.growth _)\<close> $zeroForOne)
+    sel (\<open>growth.fee0 (pool.growth _)\<close>, \<open>growth.fee1 (pool.growth _)\<close>, $zeroForOne)
       is \<open>I_fee_growth_global growth\<close> \<rightarrow> var fee_growth_global
     \<open>0 \<Ztypecolon> \<real>\<close> \<rightarrow> var protocolFee
     $liquidityStart \<rightarrow> var liquidity ;;
@@ -502,6 +501,6 @@ proc swap:
 
 \<medium_right_bracket>.
 
-end 
+end
 
 end

Uniswap_Pool.thy

@@ -12,8 +12,8 @@ proc getAmount0Delta':
   output \<open>\<bar>liq / rA - liq / rB\<bar> \<Ztypecolon> \<v>\<a>\<l> \<real>\<close>
   is [routine]
   \<medium_left_bracket> 
-    $rA $rB \<rightarrow> var rA, rB ;;
-    if \<open>$rA > $rB\<close> \<medium_left_bracket> $rB $rA \<rightarrow> rA, rB \<medium_right_bracket> \<medium_left_bracket> \<medium_right_bracket> ;; 
+    ($rA, $rB) \<rightarrow> var rA, rB ;;
+    if \<open>$rA > $rB\<close> \<medium_left_bracket> ($rB, $rA) \<rightarrow> rA, rB \<medium_right_bracket> \<medium_left_bracket> \<medium_right_bracket> ;; 
 
     $liq \<rightarrow> val numerator1 ;;
     \<open>$rB - $rA\<close> \<rightarrow> val numerator2 ;;
@@ -43,8 +43,8 @@ proc getAmount1Delta':
   output \<open>\<bar>liq * (rB - rA)\<bar> \<Ztypecolon> \<v>\<a>\<l> \<real>\<close>
   is [routine]
   \<medium_left_bracket> 
-    $rA $rB \<rightarrow> var rA, rB ;;
-    if \<open>$rA > $rB\<close> \<medium_left_bracket> $rB $rA \<rightarrow> rA, rB \<medium_right_bracket> \<medium_left_bracket> \<medium_right_bracket> ;; 
+    ($rA, $rB) \<rightarrow> var rA, rB ;;
+    if \<open>$rA > $rB\<close> \<medium_left_bracket> ($rB, $rA) \<rightarrow> rA, rB \<medium_right_bracket> \<medium_left_bracket> \<medium_right_bracket> ;; 
 
     \<open>$liq * ($rB - $rA)\<close>
   \<medium_right_bracket>.
@@ -68,7 +68,7 @@ proc getAmount0Delta'_rounded:
                       else nat \<lfloor> \<bar>real liq / rA - real liq / rB\<bar> \<rfloor>) \<Ztypecolon> \<v>\<a>\<l> \<nat>\<close>
   is [routine]
 \<medium_left_bracket>
-  $rA $rB \<rightarrow> var rA, rB ;;
+  ($rA, $rB) \<rightarrow> var rA, rB ;;
   if ($rA > $rB) \<medium_left_bracket> ($rB, $rA) \<rightarrow> rA, rB \<medium_right_bracket> \<medium_left_bracket> \<medium_right_bracket> ;; 
 
   $liq to_real \<rightarrow> val numerator1 ;;
@@ -90,8 +90,8 @@ proc getAmount0Delta_rounded:
                       else \<lceil> real_of_int liq / rA - real_of_int liq / rB \<rceil>) \<Ztypecolon> \<v>\<a>\<l> \<int>\<close>
   is [routine]
   \<medium_left_bracket> if \<open>$liq < 0\<close>
-    \<medium_left_bracket> $rA $rB \<open>-$liq\<close> \<open>False\<close> getAmount0Delta'_rounded \<medium_right_bracket>
-    \<medium_left_bracket> $rA $rB $liq \<open>True\<close> getAmount0Delta'_rounded \<medium_right_bracket>
+    \<medium_left_bracket> getAmount0Delta'_rounded ($rA, $rB, \<open>-$liq\<close>, \<open>False\<close>)  \<medium_right_bracket>
+    \<medium_left_bracket> getAmount0Delta'_rounded ($rA, $rB, $liq, \<open>True\<close>) \<medium_right_bracket>
   \<medium_right_bracket>.
 
 proc getNextSqrtPriceFromAmount0:

Uniswap_SqrtPriceMath.phi-cache

@@ -2,8 +2,6 @@ theory Uniswap_SwapMath
   imports Uniswap_SqrtPriceMath Uniswap_Tick_Math Uniswap_Tick
 begin
 
-declare [[\<phi>trace_processing]]
-
 definition reserve_change_in_a_step :: \<open>real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<times> real\<close>
   where \<open>reserve_change_in_a_step L price0 price1
     = (L / price0 - L / price1 \<comment> \<open>reserve change in token0\<close>,
@@ -927,7 +925,7 @@ proc computeSwapStep:
     note max_def[\<phi>sledgehammer_simps] min_def[\<phi>sledgehammer_simps] ;;
 
     var next_price, feeAmount ;;
-    \<open>0 \<Ztypecolon> \<real>\<close> \<open>0 \<Ztypecolon> \<real>\<close> \<rightarrow> var amountIn, amountOut (*TODO: support converge-of-branch between initialized and uninitialized variables*)
+    (\<open>0 \<Ztypecolon> \<real>\<close>, \<open>0 \<Ztypecolon> \<real>\<close>) \<rightarrow> var amountIn, amountOut (*TODO: support converge-of-branch between initialized and uninitialized variables*)
     \<open>$price \<ge> $price_target\<close> \<rightarrow> val zeroForOne ;;
     \<open>$amount_remain \<ge> 0\<close> \<rightarrow> val exactIn