WIP

Author: xqyww123

Uniswap.thy

@@ -0,0 +1,117 @@
+theory Uniswap
+  imports PhiSem_Machine_Integer PhiSem_CF_Basic PhiSem_Variable HOL.Transcendental
+begin
+
+consts Tick  :: \<open>(VAL, int) \<phi>\<close>
+       Price :: \<open>(VAL, real) \<phi>\<close>
+
+definition \<open>FACTOR = (1.0001::real)\<close>
+
+lemma FACTOR_LG_1: \<open>1 < FACTOR\<close> unfolding FACTOR_def by simp
+
+definition price_of :: \<open>int \<Rightarrow> real\<close>
+  where price_of_def': \<open>price_of tick = sqrt (FACTOR powr (of_int tick))\<close>
+
+lemma price_of_def: \<open>price_of t = FACTOR powr (of_int t / 2)\<close>
+  unfolding price_of_def'
+  by (simp add: powr_half_sqrt[symmetric] powr_powr)
+
+hide_fact price_of_def'
+
+lemma price_of_mono': \<open>mono price_of\<close>
+  unfolding price_of_def mono_on_def
+  by (simp add: FACTOR_LG_1)
+
+lemma price_of_smono': \<open>strict_mono price_of\<close>
+  unfolding price_of_def strict_mono_on_def
+  by (simp add: FACTOR_LG_1)
+
+lemma price_of_mono:
+  \<open>price_of x \<le> price_of y \<longleftrightarrow> x \<le> y\<close>
+  using price_of_mono'
+  by (simp add: price_of_smono' strict_mono_less_eq) 
+
+lemma price_of_smono:
+  \<open>price_of x < price_of y \<longleftrightarrow> x < y\<close>
+  using price_of_smono' using strict_mono_less by blast
+
+definition \<open>tick_of_price p = (@t. price_of t \<le> p \<and> p < price_of (t+1)) \<close>
+
+lemma tick_of_price: \<open>tick_of_price (price_of t) = t\<close>
+  unfolding tick_of_price_def
+  by (smt (z3) price_of_smono some_eq_imp)
+
+lemma price_of_tick:
+  assumes \<open>0 < p\<close>
+  shows \<open>price_of (tick_of_price p) \<le> p \<and> p < price_of (tick_of_price p + 1)\<close>
+proof -
+  have \<open>\<exists>t. p < FACTOR powr t\<close>
+    by (metis FACTOR_LG_1 dual_order.strict_trans floor_log_eq_powr_iff linorder_neqE_linordered_idom zero_less_one)
+  then have \<open>\<exists>t. p < price_of t\<close>
+    unfolding price_of_def
+    by (meson FACTOR_LG_1 dual_order.strict_trans ex_less_of_int less_divide_eq_numeral1(1) powr_less_cancel_iff)
+  moreover have \<open>\<exists>t. FACTOR powr t \<le> p\<close>
+    using \<open>0 < p\<close> FACTOR_LG_1 floor_log_eq_powr_iff by blast
+  then have \<open>\<exists>t. price_of t \<le> p\<close>
+    proof -
+      have \<open>\<And>x. \<exists>t. real_of_int t / 2 < x\<close> by (simp add: ex_of_int_less)
+      then show ?thesis
+      unfolding price_of_def
+      by (meson FACTOR_LG_1 \<open>\<exists>t. FACTOR powr t \<le> p\<close> dual_order.trans less_le_not_le powr_le_cancel_iff)
+    qed
+  ultimately have X: \<open>(\<exists>t. price_of t \<le> p \<and> p < price_of (t+1))\<close>
+    proof -
+    obtain t1 where t1: \<open>price_of t1 \<le> p\<close> using \<open>\<exists>t. price_of t \<le> p\<close> by blast
+    obtain t2 where t2: \<open>p < price_of t2\<close> using \<open>\<exists>t. p < price_of t\<close> by blast
+    have le: \<open>t1 < t2\<close> using t1 t2 price_of_smono by fastforce
+    thm int_gr_induct[OF le]
+    have \<open>p < price_of t2 \<longrightarrow> ?thesis\<close>
+    proof (induct rule: int_gr_induct[OF le])
+      case 1
+      then show ?case
+        using t1 by blast
+    next
+      case (2 i)
+      then show ?case
+        by force
+    qed
+    then show ?thesis
+      using t2 by blast
+  qed
+  then show ?thesis
+    unfolding tick_of_price_def
+    by (metis (no_types, lifting) someI_ex)
+qed
+
+
+debt_axiomatization getSqrtRatioAtTick :: \<open>(VAL,VAL) proc'\<close>
+  where getSqrtRatioAtTick_\<phi>app:
+            \<open>\<^bold>p\<^bold>r\<^bold>o\<^bold>c getSqrtRatioAtTick v \<lbrace> t \<Ztypecolon> \<^bold>v\<^bold>a\<^bold>l[v] Tick \<longmapsto> price_of t \<Ztypecolon> \<^bold>v\<^bold>a\<^bold>l Price \<rbrace>\<close>
+    and getTickAtSqrtRatio_\<phi>app:
+            \<open>\<^bold>p\<^bold>r\<^bold>e\<^bold>m\<^bold>i\<^bold>s\<^bold>e 0 < p
+         \<Longrightarrow> \<^bold>p\<^bold>r\<^bold>o\<^bold>c getTickAtSqrtRatio v \<lbrace> p \<Ztypecolon> \<^bold>v\<^bold>a\<^bold>l[v] Price \<longmapsto> tick_of_price p \<Ztypecolon> \<^bold>v\<^bold>a\<^bold>l Tick \<rbrace>\<close>
+
+record tick_info =
+  liquidityGross :: nat
+  liquidityNet   :: int
+  feeGrowthOutside0X128 :: nat
+  feeGrowthOutside1X128 :: nat
+  tickCumulativeOutside :: int
+  secondsPerLiquidityOutsideX128 :: nat
+  secondsOutside :: nat
+  initialized :: bool
+
+definition \<open>growth_Inv f f' delta current =
+  (\<forall>i. f i = (if i \<le> current then (sum f' {j. j \<le> i}) + delta i else (sum f' {j. i < j}) - delta i))\<close>
+  
+
+term sum
+
+
+consts TickInfo'  :: \<open>(VAL, tick_info) \<phi>\<close>
+       TickInfos :: \<open>(assn, int \<Rightarrow> tick_info) \<phi>\<close>
+
+definition \<open>TickInfo = (\<lambda>info. into \<Ztypecolon> TickInfo' \<^bold>s\<^bold>u\<^bold>b\<^bold>j )\<close>
+
+
+end

notes/Contracts — Solidity 0.8.15 documentation.pdf

@@ -0,0 +1,15 @@
+
+
+- envir: singleton {sender: address, code: address}
+- contracts: address -> field-name -> Value
+
+address := nat (it is logically abstract and inifinite therefore)
+field-name := string
+Value := usual-Value | mapping-id | array-id
+
+mapping-id, array-id: MLP
+  (id, type_k, type_v) -> Value -> Value
+  (id, type_v) -> nat -> Value
+
+
+

notes/Structure of a Contract — Solidity 0.8.15 documentation.pdf

@@ -0,0 +1,82 @@
+
+
+
+- payable address,
+
+
+
+
+## Note!
+
+- address is comparable
+- storage of map and array needs Meta Logic Parameter [X no we don't]
+- push() is very tricky! more cautions to deal with it! (low priority, Uniswap never uses storage X[]!)
+
+## Heaps:
+
+- balance: address -> uint256???
+
+
+## Question:
+
+- What is the type of money/ether?
+
+### Need Talk
+
+- **GAS!!!!!**
+- Dangling References, acceptable feature or reject?
+
+## TODO Plan:
+
+- Exception & Revert
+- Mutability: oure, view, payable, non-payable
+- bytes, T[] is a pointer
+X nondeterminism if we want true `send`
+X true exception if we want `break` & `return`
+    Success state | PartCorrect | Error excp state
+- WF while / recursion
+
+### Special Cautions [necessary]
+
+- abi.decode / abi.encodeWithSelector,  .selector
+- staticcall
+- checkNotDelegateCall (How?)
+- It is said before version xx byte is an alias of bytes1. Then what is it now?
+- calldata
+- assignment between different locations!! see [Data location and assignment behavior]
+- the automatic public accessor of mappings
+
+### Special Cautions [less important]
+
+- type expression `type(int32).max` (The uniswap only uses `type(T).max/min`
+- Contract is a type, e.g. `type(MyContract).name`
+- Constant evaluation: `(2**800 + 1) - 2**800 = 1`!
+
+### Special Cautions [info]
+
+- address.code / .balance / .codehash / .send / .transfer
+
+### Delayed / Not important in Uniswap
+
+- call{gas: 10000 / value: 1ether}
+- .code
+- all string
+- enum
+- User defined value type
+- Function pointer
+- bytes**N**
+- Array Slices, basically pointer shift.
+
+
+## Blueprint
+
+- bytesN : fixed-size list (maybe LENGTH('a))
+- keyword external, view: ignore them, since the specification states these info.
+
+
+
+
+## Question:
+
+1. How to deal with `break`
+    Maybe we need true Exception!

notes/Types — Solidity 0.8.15 documentation.pdf

@@ -0,0 +1,16 @@
+1. Do we model GAS?
+2. Push() is very tricky!! read `Dangling References to Storage Array Elements`
+3. Constant evaluation has arbitrary precision. Is is rational number. `1.5 + 1.5 = 3`, `(1.5**800 + 1) - 1.5**800 = 1`
+    https://docs.soliditylang.org/en/v0.8.15/types.html?highlight=Operators#operators
+   Suggestion: It must be done during pre-processing, cuz it never generates the code for, like, `1.5 + 1.5`.
+               Can we use the constant evaluator of Solidity itself?
+
+Small stuffs, not hard but need attention
+1. abi.decode / abi.encodeWithSelector,  .selector
+    These are used in Uniswap! https://docs.soliditylang.org/en/v0.8.15/units-and-global-variables.html?highlight=encodewithselector#abi-encoding-and-decoding-functions
+2. type expression `type(int32).max` (The uniswap only uses `type(T).max/min`
+    https://docs.soliditylang.org/en/v0.8.15/units-and-global-variables.html?highlight=type%20expression#type-information
+
+
+
+indeed, our semantic model can support this, by recording the layout on the reference, but the reasoning can be difficult. so i think, we just make it in semantics at most, and 

notes/heaps.md

@@ -0,0 +1,81 @@
+{} C {..} {\empty}
+
+
+{} C1 {..}, {if P then E1 else \empty }
+{} Throw {...}, {if Q then E2 else \empty }
+
+
+{} C1 >>  Throw, {if P then E1 else if Q then E2 else \empty }
+
+if P then E1 else \empty  \subset       if P then E1 else if Q then E2 else \empty
+if Q then E2 else \empty  \not \subset  if P then E1 else if Q then E2 else \empty
+
+
+
+
+
+
+
+send : Transition Specifiction (TS)
+
+Wrong implementation:
+transfer (address a, int m) = send a 0
+
+{} transfer {X}
+
+a.fallback is certain procedure \subset TS
+
+{(a.fallback : state transition A -> B) * A /\ a.fallback \subset TS } send a { B }
+{balance = M} send a 10 {X }
+{(a.fallback : state transition (A, balance = M-10) -> (B, balance = N')) * (A, balance = M)  /\ a.fallback \subset TS } send a 10 { B, balance = N' }
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+{P} C1 {Q} {A1}
+{Q} C2 {R} {A2}
+-------------------
+{P} C1 {R} {A1 * A2}
+
+A ::= NoErr | Err (type-excep, state)
+NoErr * x = x
+Err y * _ = Err y
+
+type-excep ::= Break | Return | ...
+
+{P} C {Q} {A} := if 
+
+{P} C1 {Q} {if cond then excep else NoErr}
+{P} C {Q} {NoErr}
+
+(if cond1 then excep else NoErr) * (if cond2 then excep else NoErr)
+  = if cond1 then excep else NoErr
+
+
+
+
+
+
+
+
+
+
+
+