diff --git a/thys/Solidity/Contracts.thy b/thys/Solidity/Contracts.thy --- a/thys/Solidity/Contracts.thy +++ b/thys/Solidity/Contracts.thy @@ -1,621 +1,621 @@ section \Contracts\ theory Contracts imports Environment begin subsection \Syntax of Contracts\ datatype L = Id Identifier | Ref Identifier "E list" and E = INT nat int | UINT nat int | ADDRESS String.literal | BALANCE E | THIS | SENDER | VALUE | TRUE | FALSE | LVAL L | PLUS E E | MINUS E E | EQUAL E E | LESS E E | AND E E | OR E E | NOT E | CALL Identifier "E list" | ECALL E Identifier "E list" | CONTRACTS datatype S = SKIP | BLOCK "(Identifier \ Type) \ (E option)" S | ASSIGN L E | TRANSFER E E | COMP S S | ITE E S S | WHILE E S | INVOKE Identifier "E list" | EXTERNAL E Identifier "E list" E | NEW Identifier "E list" E abbreviation "vbits\{8,16,24,32,40,48,56,64,72,80,88,96,104,112,120,128, 136,144,152,160,168,176,184,192,200,208,216,224,232,240,248,256}" lemma vbits_max[simp]: assumes "b1 \ vbits" and "b2 \ vbits" shows "(max b1 b2) \ vbits" proof - consider (b1) "max b1 b2 = b1" | (b2) "max b1 b2 = b2" by (metis max_def) then show ?thesis proof cases case b1 then show ?thesis using assms(1) by simp next case b2 then show ?thesis using assms(2) by simp qed qed lemma vbits_ge_0: "(x::nat)\vbits \ x>0" by auto subsection \State\ type_synonym Gas = nat record State = accounts :: Accounts stack :: Stack memory :: MemoryT storage :: "Address \ StorageT" gas :: Gas lemma all_gas_le: assumes "gas x<(gas y::nat)" and "\z. gas z < gas y \ P z \ Q z" shows "\z. gas z \ gas x \ P z \ Q z" using assms by simp lemma all_gas_less: assumes "\z. gas z < gas y \ P z" and "gas x\(gas y::nat)" shows "\z. gas z < gas x \ P z" using assms by simp definition incrementAccountContracts :: "Address \ State \ State" where "incrementAccountContracts ad st = st \accounts := (accounts st)(ad := (accounts st ad)\contracts := Suc (contracts (accounts st ad))\)\" declare incrementAccountContracts_def [solidity_symbex] lemma incrementAccountContracts_type[simp]: "type (accounts (incrementAccountContracts ad st) ad') = type (accounts st ad')" using incrementAccountContracts_def by simp lemma incrementAccountContracts_bal[simp]: "bal (accounts (incrementAccountContracts ad st) ad') = bal (accounts st ad')" using incrementAccountContracts_def by simp lemma incrementAccountContracts_stack[simp]: "stack (incrementAccountContracts ad st) = stack st" using incrementAccountContracts_def by simp lemma incrementAccountContracts_memory[simp]: "memory (incrementAccountContracts ad st) = memory st" using incrementAccountContracts_def by simp lemma incrementAccountContracts_storage[simp]: "storage (incrementAccountContracts ad st) = storage st" using incrementAccountContracts_def by simp lemma incrementAccountContracts_gas[simp]: "gas (incrementAccountContracts ad st) = gas st" using incrementAccountContracts_def by simp lemma gas_induct: assumes "\s. \s'. gas s' < gas s \ P s' \ P s" shows "P s" using assms by (rule Nat.measure_induct[of "\s. gas s"]) definition emptyStorage :: "Address \ StorageT" where "emptyStorage _ = {$$}" declare emptyStorage_def [solidity_symbex] abbreviation mystate::State where "mystate \ \ accounts = emptyAccount, stack = emptyStore, memory = emptyStore, storage = emptyStorage, gas = 0 \" datatype Ex = Gas | Err subsection \Contracts\ text \ A contract consists of methods, functions, and storage variables. A method is a triple consisting of \<^item> A list of formal parameters \<^item> A flag to signal external methods \<^item> A statement A function is a pair consisting of \<^item> A list of formal parameters \<^item> A flag to signal external functions \<^item> An expression \ datatype(discs_sels) Member = Method "(Identifier \ Type) list \ bool \ S" | Function "(Identifier \ Type) list \ bool \ E" | Var STypes text \ A procedure environment assigns a contract to an address. A contract consists of \<^item> An assignment of contract to identifiers \<^item> A constructor \<^item> A fallback statement which is executed after money is beeing transferred to the contract. \url{https://docs.soliditylang.org/en/v0.8.6/contracts.html#fallback-function} \ type_synonym Contract = "(Identifier, Member) fmap \ ((Identifier \ Type) list \ S) \ S" type_synonym Environment\<^sub>P = "(Identifier, Contract) fmap" definition init::"(Identifier, Member) fmap \ Identifier \ Environment \ Environment" where "init ct i e = (case fmlookup ct i of Some (Var tp) \ updateEnvDup i (Storage tp) (Storeloc i) e | _ \ e)" declare init_def [solidity_symbex] lemma init_s11[simp]: assumes "fmlookup ct i = Some (Var tp)" shows "init ct i e = updateEnvDup i (Storage tp) (Storeloc i) e" using assms init_def by simp lemma init_s12[simp]: assumes "i |\| fmdom (denvalue e)" shows "init ct i e = e" proof (cases "fmlookup ct i") case None then show ?thesis using init_def by simp next case (Some a) then show ?thesis proof (cases a) case (Method _) with Some show ?thesis using init_def by simp next case (Function _) with Some show ?thesis using init_def by simp next case (Var tp) with Some have "init ct i e = updateEnvDup i (Storage tp) (Storeloc i) e" using init_def by simp moreover from assms have "updateEnvDup i (Storage tp) (Storeloc i) e = e" by auto ultimately show ?thesis by simp qed qed lemma init_s13[simp]: assumes "fmlookup ct i = Some (Var tp)" and "\ i |\| fmdom (denvalue e)" shows "init ct i e = updateEnv i (Storage tp) (Storeloc i) e" using assms init_def by auto lemma init_s21[simp]: assumes "fmlookup ct i = None" shows "init ct i e = e" using assms init_def by auto lemma init_s22[simp]: assumes "fmlookup ct i = Some (Method m)" shows "init ct i e = e" using assms init_def by auto lemma init_s23[simp]: assumes "fmlookup ct i = Some (Function f)" shows "init ct i e = e" using assms init_def by auto lemma init_commte: "comp_fun_commute (init ct)" proof fix x y show "init ct y \ init ct x = init ct x \ init ct y" proof fix e show "(init ct y \ init ct x) e = (init ct x \ init ct y) e" proof (cases "fmlookup ct x") case None then show ?thesis by simp next case s1: (Some a) then show ?thesis proof (cases a) case (Method _) with s1 show ?thesis by simp next case (Function _) with s1 show ?thesis by simp next case v1: (Var tp) then show ?thesis proof (cases "x |\| fmdom (denvalue e)") case True with s1 v1 have *: "init ct x e = e" by auto then show ?thesis proof (cases "fmlookup ct y") case None then show ?thesis by simp next case s2: (Some a) then show ?thesis proof (cases a) case (Method _) with s2 show ?thesis by simp next case (Function _) with s2 show ?thesis by simp next case v2: (Var tp') then show ?thesis proof (cases "y |\| fmdom (denvalue e)") case t1: True with s1 v1 True s2 v2 show ?thesis by fastforce next define e' where "e' = updateEnv y (Storage tp') (Storeloc y) e" case False with s2 v2 have "init ct y e = e'" using e'_def by auto with s1 v1 True e'_def * show ?thesis by auto qed qed qed next define e' where "e' = updateEnv x (Storage tp) (Storeloc x) e" case f1: False with s1 v1 have *: "init ct x e = e'" using e'_def by auto then show ?thesis proof (cases "fmlookup ct y") case None then show ?thesis by simp next case s3: (Some a) then show ?thesis proof (cases a) case (Method _) with s3 show ?thesis by simp next case (Function _) with s3 show ?thesis by simp next case v2: (Var tp') then show ?thesis proof (cases "y |\| fmdom (denvalue e)") case t1: True with e'_def have "y |\| fmdom (denvalue e')" by simp with s1 s3 v1 f1 v2 show ?thesis using e'_def by fastforce next define f' where "f' = updateEnv y (Storage tp') (Storeloc y) e" define e'' where "e'' = updateEnv y (Storage tp') (Storeloc y) e'" case f2: False with s3 v2 have **: "init ct y e = f'" using f'_def by auto show ?thesis proof (cases "y = x") case True with s3 v2 e'_def have "init ct y e' = e'" by simp moreover from s3 v2 True f'_def have "init ct x f' = f'" by simp ultimately show ?thesis using True by simp next define f'' where "f'' = updateEnv x (Storage tp) (Storeloc x) f'" case f3: False with f2 have "\ y |\| fmdom (denvalue e')" using e'_def by simp with s3 v2 e''_def have "init ct y e' = e''" by auto with * have "(init ct y \ init ct x) e = e''" by simp moreover have "init ct x f' = f''" proof - from s1 v1 have "init ct x f' = updateEnvDup x (Storage tp) (Storeloc x) f'" by simp moreover from f1 f3 have "x |\| fmdom (denvalue f')" using f'_def by simp ultimately show ?thesis using f''_def by auto qed moreover from f''_def e''_def f'_def e'_def f3 have "Some f'' = Some e''" using env_reorder_neq by simp ultimately show ?thesis using ** by simp qed qed qed qed qed qed qed qed qed lemma init_address[simp]: "address (init ct i e) = address e" proof (cases "fmlookup ct i") case None then show ?thesis by simp next case (Some a) show ?thesis proof (cases a) case (Method _) with Some show ?thesis by simp next case (Function _) with Some show ?thesis by simp next case (Var _) with Some show ?thesis using updateEnvDup_address updateEnvDup_sender by simp qed qed lemma init_sender[simp]: "sender (init ct i e) = sender e" proof (cases "fmlookup ct i") case None then show ?thesis by simp next case (Some a) show ?thesis proof (cases a) case (Method _) with Some show ?thesis by simp next case (Function _) with Some show ?thesis by simp next case (Var _) with Some show ?thesis using updateEnvDup_sender by simp qed qed lemma init_svalue[simp]: "svalue (init ct i e) = svalue e" proof (cases "fmlookup ct i") case None then show ?thesis by simp next case (Some a) show ?thesis proof (cases a) case (Method _) with Some show ?thesis by simp next case (Function _) with Some show ?thesis by simp next case (Var _) with Some show ?thesis using updateEnvDup_svalue by simp qed qed lemma ffold_init_ad_same[rule_format]: "\e'. ffold (init ct) e xs = e' \ address e' = address e \ sender e' = sender e \ svalue e' = svalue e" proof (induct xs) case empty then show ?case by (simp add: ffold_def) next case (insert x xs) then have *: "ffold (init ct) e (finsert x xs) = init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp show ?case proof (rule allI[OF impI]) fix e' assume **: "ffold (init ct) e (finsert x xs) = e'" with * obtain e'' where ***: "ffold (init ct) e xs = e''" by simp with insert have "address e'' = address e \ sender e'' = sender e \ svalue e'' = svalue e" by blast with * ** *** show "address e' = address e \ sender e' = sender e \ svalue e' = svalue e" using init_address init_sender init_svalue by metis qed qed lemma ffold_init_ad[simp]: "address (ffold (init ct) e xs) = address e" using ffold_init_ad_same by simp lemma ffold_init_sender[simp]: "sender (ffold (init ct) e xs) = sender e" using ffold_init_ad_same by simp lemma ffold_init_dom: "fmdom (denvalue (ffold (init ct) e xs)) |\| fmdom (denvalue e) |\| xs" proof (induct "xs") case empty then show ?case proof fix x assume "x |\| fmdom (denvalue (ffold (init ct) e {||}))" moreover have "ffold (init ct) e {||} = e" using FSet.comp_fun_commute.ffold_empty[OF init_commte, of ct e] by simp ultimately show "x |\| fmdom (denvalue e) |\| {||}" by simp qed next case (insert x xs) then have *: "ffold (init ct) e (finsert x xs) = init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp show ?case proof fix x' assume "x' |\| fmdom (denvalue (ffold (init ct) e (finsert x xs)))" with * have **: "x' |\| fmdom (denvalue (init ct x (ffold (init ct) e xs)))" by simp then consider "x' |\| fmdom (denvalue (ffold (init ct) e xs))" | "x'=x" proof (cases "fmlookup ct x") case None then show ?thesis using that ** by simp next case (Some a) then show ?thesis proof (cases a) case (Method _) then show ?thesis using Some ** that by simp next case (Function _) then show ?thesis using Some ** that by simp next case (Var x2) show ?thesis proof (cases "x=x'") case True then show ?thesis using that by simp next case False then have "fmlookup (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs))) x' = fmlookup (denvalue (ffold (init ct) e xs)) x'" using updateEnvDup_dup by simp moreover from ** Some Var have ***:"x' |\| fmdom (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs)))" by simp ultimately have "x' |\| fmdom (denvalue (ffold (init ct) e xs))" by (simp add: fmlookup_dom_iff) then show ?thesis using that by simp qed qed qed then show "x' |\| fmdom (denvalue e) |\| finsert x xs" proof cases case 1 then show ?thesis using insert.hyps by auto next case 2 then show ?thesis by simp qed qed qed lemma ffold_init_fmap: assumes "fmlookup ct i = Some (Var tp)" and "i |\| fmdom (denvalue e)" shows "i|\|xs \ fmlookup (denvalue (ffold (init ct) e xs)) i = Some (Storage tp, Storeloc i)" proof (induct "xs") case empty then show ?case by simp next case (insert x xs) then have *: "ffold (init ct) e (finsert x xs) = init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp from insert.prems consider (a) "i |\| xs" | (b) "\ i |\| xs \ i = x" by auto then show "fmlookup (denvalue (ffold (init ct) e (finsert x xs))) i = Some (Storage tp, Storeloc i)" proof cases case a with insert.hyps(2) have "fmlookup (denvalue (ffold (init ct) e xs)) i = Some (Storage tp, Storeloc i)" by simp moreover have "fmlookup (denvalue (init ct x (ffold (init ct) e xs))) i = fmlookup (denvalue (ffold (init ct) e xs)) i" proof (cases "fmlookup ct x") case None then show ?thesis by simp next case (Some a) then show ?thesis proof (cases a) case (Method _) with Some show ?thesis by simp next case (Function _) with Some show ?thesis by simp next case (Var x2) with Some have "init ct x (ffold (init ct) e xs) = updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs)" using init_def[of ct x "(ffold (init ct) e xs)"] by simp moreover from insert a have "i\x" by auto then have "fmlookup (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs))) i = fmlookup (denvalue (ffold (init ct) e xs)) i" using updateEnvDup_dup[of x i] by simp ultimately show ?thesis by simp qed qed ultimately show ?thesis using * by simp next case b with assms(1) have "fmlookup ct x = Some (Var tp)" by simp moreover from b assms(2) have "\ x |\| fmdom (denvalue (ffold (init ct) e xs))" using ffold_init_dom by auto ultimately have "init ct x (ffold (init ct) e xs) = updateEnv x (Storage tp) (Storeloc x) (ffold (init ct) e xs)" by auto with b * show ?thesis by simp qed qed lemma ffold_init_fmdom: assumes "fmlookup ct i = Some (Var tp)" and "i |\| fmdom (denvalue e)" shows "fmlookup (denvalue (ffold (init ct) e (fmdom ct))) i = Some (Storage tp, Storeloc i)" proof - from assms(1) have "i |\| fmdom ct" by (rule Finite_Map.fmdomI) then show ?thesis using ffold_init_fmap[OF assms] by simp qed -text\The following definition[solidity_symbex]:allows for a more fine-grained configuration of the +text\The following definition allows for a more fine-grained configuration of the code generator. \ definition ffold_init::"(String.literal, Member) fmap \ Environment \ String.literal fset \ Environment" where \ffold_init ct a c = ffold (init ct) a c\ declare ffold_init_def [simp,solidity_symbex] lemma ffold_init_code [code]: \ffold_init ct a c = fold (init ct) (remdups (sorted_list_of_set (fset c))) a\ using comp_fun_commute_on.fold_set_fold_remdups ffold.rep_eq ffold_init_def init_commte sorted_list_of_fset.rep_eq sorted_list_of_fset_simps(1) by (metis comp_fun_commute.comp_fun_commute comp_fun_commute_on.intro order_refl) lemma bind_case_stackvalue_cong [fundef_cong]: assumes "x = x'" and "\v. x = KValue v \ f v s = f' v s" and "\p. x = KCDptr p \ g p s = g' p s" and "\p. x = KMemptr p \ h p s = h' p s" and "\p. x = KStoptr p \ i p s = i' p s" shows "(case x of KValue v \ f v | KCDptr p \ g p | KMemptr p \ h p | KStoptr p \ i p) s = (case x' of KValue v \ f' v | KCDptr p \ g' p | KMemptr p \ h' p | KStoptr p \ i' p) s" using assms by (cases x, auto) lemma bind_case_type_cong [fundef_cong]: assumes "x = x'" and "\t. x = Value t \ f t s = f' t s" and "\t. x = Calldata t \ g t s = g' t s" and "\t. x = Memory t \ h t s = h' t s" and "\t. x = Storage t \ i t s = i' t s" shows "(case x of Value t \ f t | Calldata t \ g t | Memory t \ h t | Storage t \ i t ) s = (case x' of Value t \ f' t | Calldata t \ g' t | Memory t \ h' t | Storage t \ i' t) s" using assms by (cases x, auto) lemma bind_case_denvalue_cong [fundef_cong]: assumes "x = x'" and "\a. x = (Stackloc a) \ f a s = f' a s" and "\a. x = (Storeloc a) \ g a s = g' a s" shows "(case x of (Stackloc a) \ f a | (Storeloc a) \ g a) s = (case x' of (Stackloc a) \ f' a | (Storeloc a) \ g' a) s" using assms by (cases x, auto) lemma bind_case_mtypes_cong [fundef_cong]: assumes "x = x'" and "\a t. x = (MTArray a t) \ f a t s = f' a t s" and "\p. x = (MTValue p) \ g p s = g' p s" shows "(case x of (MTArray a t) \ f a t | (MTValue p) \ g p) s = (case x' of (MTArray a t) \ f' a t | (MTValue p) \ g' p) s" using assms by (cases x, auto) lemma bind_case_stypes_cong [fundef_cong]: assumes "x = x'" and "\a t. x = (STArray a t) \ f a t s = f' a t s" and "\a t. x = (STMap a t) \ g a t s = g' a t s" and "\p. x = (STValue p) \ h p s = h' p s" shows "(case x of (STArray a t) \ f a t | (STMap a t) \ g a t | (STValue p) \ h p) s = (case x' of (STArray a t) \ f' a t | (STMap a t) \ g' a t | (STValue p) \ h' p) s" using assms by (cases x, auto) lemma bind_case_types_cong [fundef_cong]: assumes "x = x'" and "\a. x = (TSInt a) \ f a s = f' a s" and "\a. x = (TUInt a) \ g a s = g' a s" and "x = TBool \ h s = h' s" and "x = TAddr \ i s = i' s" shows "(case x of (TSInt a) \ f a | (TUInt a) \ g a | TBool \ h | TAddr \ i) s = (case x' of (TSInt a) \ f' a | (TUInt a) \ g' a | TBool \ h' | TAddr \ i') s" using assms by (cases x, auto) lemma bind_case_contract_cong [fundef_cong]: assumes "x = x'" and "\a. x = Method a \ f a s = f' a s" and "\a. x = Function a \ g a s = g' a s" and "\a. x = Var a \ h a s = h' a s" shows "(case x of Method a \ f a | Function a \ g a | Var a \ h a) s = (case x' of Method a \ f' a | Function a \ g' a | Var a \ h' a) s" using assms by (cases x, auto) lemma bind_case_memoryvalue_cong [fundef_cong]: assumes "x = x'" and "\a. x = MValue a \ f a s = f' a s" and "\a. x = MPointer a \ g a s = g' a s" shows "(case x of (MValue a) \ f a | (MPointer a) \ g a) s = (case x' of (MValue a) \ f' a | (MPointer a) \ g' a) s" using assms by (cases x, auto) end diff --git a/thys/Solidity/Reentrancy.thy b/thys/Solidity/Reentrancy.thy --- a/thys/Solidity/Reentrancy.thy +++ b/thys/Solidity/Reentrancy.thy @@ -1,838 +1,838 @@ section\Reentrancy\ text \ In the following we use our calculus to verify a contract implementing a simple token. - The contract is defined by definition[solidity_symbex]:*bank* and consist of one state variable and two methods: + The contract is defined by definition *bank* and consist of one state variable and two methods: \<^item> The state variable "balance" is a mapping which assigns a balance to each address. \<^item> Method "deposit" allows to send money to the contract which is then added to the sender's balance. \<^item> Method "withdraw" allows to withdraw the callers balance. \ text \ We then verify that the following invariant (defined by *BANK*) is preserved by both methods: The difference between \<^item> the contracts own account-balance and \<^item> the sum of all the balances kept in the contracts state variable is larger than a certain threshold. \ text \ There are two things to note here: First, Solidity implicitly triggers the call of a so-called fallback method whenever we transfer money to a contract. In particular if another contract calls "withdraw", this triggers an implicit call to the callee's fallback method. This functionality was exploited in the infamous DAO attack which we demonstrate it in terms of an example later on. Since we do not know all potential contracts which call "withdraw", we need to verify our invariant for all possible Solidity programs. \ text \ The second thing to note is that we were not able to verify that the difference is indeed constant. During verification it turned out that this is not the case since in the fallback method a contract could just send us additional money without calling "deposit". In such a case the difference would change. In particular it would grow. However, we were able to verify that the difference does never shrink which is what we actually want to ensure. \ theory Reentrancy imports Weakest_Precondition Solidity_Evaluator "HOL-Eisbach.Eisbach_Tools" begin subsection\Example of Re-entrancy\ definition[solidity_symbex]:"example_env \ loadProc (STR ''Attacker'') ([], ([], SKIP), ITE (LESS (BALANCE THIS) (UINT 256 125)) (EXTERNAL (ADDRESS (STR ''BankAddress'')) (STR ''withdraw'') [] (UINT 256 0)) SKIP) (loadProc (STR ''Bank'') ([(STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))), (STR ''deposit'', Method ([], True, ASSIGN (Ref (STR ''balance'') [SENDER]) (PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE))), (STR ''withdraw'', Method ([], True, ITE (LESS (UINT 256 0) (LVAL (Ref (STR ''balance'') [SENDER]))) (COMP (TRANSFER SENDER (LVAL (Ref (STR ''balance'') [SENDER]))) (ASSIGN (Ref (STR ''balance'') [SENDER]) (UINT 256 0))) SKIP))], ([], SKIP), SKIP) fmempty)" global_interpretation reentrancy: statement_with_gas costs_ex example_env costs_min defines stmt = "reentrancy.stmt" and lexp = reentrancy.lexp and expr = reentrancy.expr and ssel = reentrancy.ssel and rexp = reentrancy.rexp and msel = reentrancy.msel and load = reentrancy.load and eval = reentrancy.eval by unfold_locales auto lemma "eval 1000 (COMP (EXTERNAL (ADDRESS (STR ''BankAddress'')) (STR ''deposit'') [] (UINT 256 10)) (EXTERNAL (ADDRESS (STR ''BankAddress'')) (STR ''withdraw'') [] (UINT 256 0))) (STR ''AttackerAddress'') (STR ''Attacker'') (STR '''') (STR ''0'') [(STR ''BankAddress'', STR ''100'', Contract (STR ''Bank''), 0), (STR ''AttackerAddress'', STR ''100'', Contract (STR ''Attacker''), 0)] [] = STR ''BankAddress: balance==70 - Bank(balance[AttackerAddress]==0\)\AttackerAddress: balance==130 - Attacker()''" by eval subsection\Definition of Contract\ abbreviation myrexp::L where "myrexp \ Ref (STR ''balance'') [SENDER]" abbreviation mylval::E where "mylval \ LVAL myrexp" abbreviation assign::S where "assign \ ASSIGN (Ref (STR ''balance'') [SENDER]) (UINT 256 0)" abbreviation transfer::S where "transfer \ TRANSFER SENDER (LVAL (Id (STR ''bal'')))" abbreviation comp::S where "comp \ COMP assign transfer" abbreviation keep::S where "keep \ BLOCK ((STR ''bal'', Value (TUInt 256)), Some mylval) comp" abbreviation deposit::S where "deposit \ ASSIGN (Ref (STR ''balance'') [SENDER]) (PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE)" abbreviation "banklist \ [ (STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))), (STR ''deposit'', Method ([], True, deposit)), (STR ''withdraw'', Method ([], True, keep))]" definition bank::"(Identifier, Member) fmap" where "bank \ fmap_of_list banklist" subsection\Verification\ locale Reentrancy = Calculus + assumes r0: "cname = STR ''Bank''" and r1: "members = bank" and r2: "fb = SKIP" and r3: "const = ([], SKIP)" begin subsubsection\Method lemmas\ text \ These lemmas are required by @{term vcg_external}. \ lemma mwithdraw[mcontract]: "members $$ STR ''withdraw'' = Some (Method ([], True, keep))" using r1 unfolding bank_def by simp lemma mdeposit[mcontract]: "members $$ STR ''deposit'' = Some (Method ([], True, deposit))" using r1 unfolding bank_def by simp subsubsection\Variable lemma\ lemma balance: "members $$ (STR ''balance'') = Some (Var (STMap TAddr (STValue (TUInt 256))))" using r1 bank_def fmlookup_of_list[of "[(STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))), (STR ''deposit'', Method ([], True, ASSIGN myrexp (PLUS mylval VALUE))), (STR ''withdraw'', Method ([], True, BLOCK ((STR ''bal'', Value (TUInt 256)), Some mylval) (COMP (ASSIGN myrexp (UINT 256 0)) Reentrancy.transfer)))]"] by simp subsubsection\Case lemmas\ text \ These lemmas are required by @{term vcg_transfer}. \ lemma cases_ext: assumes "members $$ mid = Some (Method (fp,True,f))" and "fp = [] \ P deposit" and "fp = [] \ P keep" shows "P f" proof - from assms(1) r1 consider (withdraw) "mid = STR ''withdraw''" | (deposit) "mid = STR ''deposit''" using bank_def fmap_of_list_SomeD[of "[(STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))), (STR ''deposit'', Method ([], True, deposit)), (STR ''withdraw'', Method ([], True, keep))]"] by auto then show ?thesis proof (cases) case withdraw then have "f = keep" and "fp = []" using assms(1) bank_def r1 fmlookup_of_list[of banklist] by simp+ then show ?thesis using assms(3) by simp next case deposit then have "f = deposit" and "fp = []" using assms(1) bank_def r1 fmlookup_of_list[of banklist] by simp+ then show ?thesis using assms(2) by simp qed qed lemma cases_int: assumes "members $$ mid = Some (Method (fp,False,f))" shows "P fp f" using assms r1 bank_def fmap_of_list_SomeD[of "[(STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))), (STR ''deposit'', Method ([], True, deposit)), (STR ''withdraw'', Method ([], True, keep))]"] by auto lemma cases_fb: assumes "P SKIP" shows "P fb" using assms bank_def r2 by simp lemma cases_cons: assumes "fst const = [] \ P (fst const, SKIP)" shows "P const" using assms bank_def r3 by simp subsubsection\Definition of Invariant\ abbreviation "SUMM s \ \(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x. ReadL\<^sub>i\<^sub>n\<^sub>t x" abbreviation "POS s \ \ad x. fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x \ ReadL\<^sub>i\<^sub>n\<^sub>t x \ 0" definition "iv s a \ a \ SUMM s \ POS s" lemma weaken: assumes "iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v)" and "ReadL\<^sub>i\<^sub>n\<^sub>t v \0" shows "iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)))" using assms unfolding iv_def by simp subsubsection\Additional lemmas\ lemma expr_0: assumes "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g1\) g1 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g1')" and "decl STR ''bal'' (Value (TUInt 256)) (Some (lv, lt)) False cd\<^sub>l m\<^sub>l s (cd\<^sub>l, m\<^sub>l, k\<^sub>l, e\<^sub>l) = Some (cd', mem', sck', e')" and "expr (UINT 256 0) ev0 cd0 st0 g0 = Normal ((rv, rt),g''a)" shows "rv= KValue (ShowL\<^sub>i\<^sub>n\<^sub>t 0)" and "rt=Value (TUInt 256)" using assms(3) by (simp add:expr.simps createUInt_def split:if_split_asm)+ lemma load_empty_par: assumes "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g1\) g1 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g1')" shows "load True [] [] (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g1\) g1 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g1')" proof - have "xe=[]" proof (rule ccontr) assume "\ xe=[]" then obtain x and xa where "xe=x # xa" by (meson list.exhaust) then have "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g1\) g1 = throw Err g1" by (simp add:load.simps) with assms show False by simp qed then show ?thesis using assms(1) by simp qed lemma lexp_myrexp_decl: assumes "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g1\) g1 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g1')" and "decl STR ''bal'' (Value (TUInt 256)) (Some (lv, lt)) False cd\<^sub>l m\<^sub>l s (cd\<^sub>l, m\<^sub>l, k\<^sub>l, e\<^sub>l) = Some (cd', mem', sck', e')" and "lexp myrexp e' cd' (st0\accounts := acc, stack := sck', memory := mem', gas := g'a\) g'a = Normal ((rv,rt), g''a)" shows "rv= LStoreloc (address env + (STR ''.'' + STR ''balance''))" and "rt=Storage (STValue (TUInt 256))" proof - have "fmlookup (denvalue (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" unfolding emptyEnv_def using ffold_init_fmdom balance by simp moreover have el_def: "e\<^sub>l = (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))" using load_empty_par[OF assms(1)] by (simp add:load.simps) ultimately have "fmlookup (denvalue e\<^sub>l) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" using assms by auto then have *: "fmlookup (denvalue e') (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" using decl_env[OF assms(2)] by simp moreover obtain g'' where "ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] e' cd' (st0\accounts := acc, stack := sck', memory := mem', gas := g'a\) g'a = Normal (((address env) + (STR ''.'' + STR ''balance''), STValue (TUInt 256)), g'')" proof - have "g'a > costs\<^sub>e SENDER e' cd' (st0\accounts := acc, stack := sck', memory := mem', gas := g'a\)" using assms(3) * by (simp add:expr.simps ssel.simps lexp.simps split:if_split_asm) then obtain g'' where "expr SENDER e' cd' (st0\accounts := acc, stack := sck', memory := mem', gas := g'a\) g'a = Normal ((KValue (sender e'), Value TAddr), g'')" by (simp add:expr.simps) moreover have "sender e\<^sub>l = address env" using el_def ffold_init_ad_same[of members "(emptyEnv ad cname (address env) v)" "fmdom members" e\<^sub>l] unfolding emptyEnv_def by simp then have "sender e' = address env" using decl_env[OF assms(2)] by simp ultimately show ?thesis using that hash_def by (simp add:ssel.simps) qed ultimately show "rv= LStoreloc (address env + (STR ''.'' + STR ''balance''))" and "rt=Storage (STValue (TUInt 256))" using assms(3) by (simp add:lexp.simps)+ qed lemma expr_bal: assumes "expr (LVAL (L.Id STR ''bal'')) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\) g'' = Normal ((KValue lv, Value t), g''')" and "(sck', e') = astack STR ''bal'' (Value (TUInt 256)) (KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s')) (k\<^sub>l, e\<^sub>l)" shows "(\accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s'\::int) = ReadL\<^sub>i\<^sub>n\<^sub>t lv" (is ?G1) and "t = TUInt 256" proof - from assms(1) have "expr (LVAL (L.Id STR ''bal'')) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\) g'' = rexp ((L.Id STR ''bal'')) e' cd' ((st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\)) (g'' - costs\<^sub>e (LVAL (L.Id STR ''bal'')) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\))" by (simp add:expr.simps split:if_split_asm) moreover have "rexp ((L.Id STR ''bal'')) e' cd' ((st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\)) (g'' - costs\<^sub>e (LVAL (L.Id STR ''bal'')) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\)) = Normal ((KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s'), (Value (TUInt 256))),(g'' - costs\<^sub>e (LVAL (L.Id STR ''bal'')) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\)) )" proof - from assms(2) have "fmlookup (denvalue e') (STR ''bal'') = Some (Value (TUInt 256), Stackloc \toploc k\<^sub>l\)" by (simp add:push_def allocate_def updateStore_def ) moreover have "accessStore (\toploc k\<^sub>l\) sck' = Some (KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s'))" using assms(2) by (simp add:push_def allocate_def updateStore_def accessStore_def) ultimately show ?thesis by (simp add:rexp.simps) qed ultimately have "expr (LVAL (L.Id STR ''bal'')) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\) g'' = Normal ((KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s'), (Value (TUInt 256))),(g'' - costs\<^sub>e (LVAL (L.Id STR ''bal'')) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := fmupd l v' s'), gas := g''\)))" and "t = TUInt 256" using assms(1) by simp+ then have "lv = accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s'" using assms(1) by (auto) with `t = TUInt 256` show ?G1 and "t = TUInt 256" by simp+ qed lemma lexp_myrexp: assumes "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g1\) g1 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g1')" and "lexp myrexp e\<^sub>l cd\<^sub>l (st'\gas := g2\) g2 = Normal ((rv,rt), g2')" shows "rv= LStoreloc (address env + (STR ''.'' + STR ''balance''))" and "rt=Storage (STValue (TUInt 256))" proof - have "fmlookup (denvalue (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" unfolding emptyEnv_def using ffold_init_fmdom balance by simp moreover have el_def: "e\<^sub>l = (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))" using load_empty_par[OF assms(1)] by (simp add:load.simps) ultimately have *: "fmlookup (denvalue e\<^sub>l) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" using assms by auto moreover obtain g'' where "ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] e\<^sub>l cd\<^sub>l (st'\gas := g2\) g2 = Normal (((address env) + (STR ''.'' + STR ''balance''), STValue (TUInt 256)), g'')" proof - have "g2 > costs\<^sub>e SENDER e\<^sub>l cd\<^sub>l (st'\gas := g2\)" using assms(2) * by (simp add:expr.simps ssel.simps lexp.simps split:if_split_asm) then obtain g'' where "expr SENDER e\<^sub>l cd\<^sub>l (st'\gas := g2\) g2 = Normal ((KValue (sender e\<^sub>l), Value TAddr), g'')" by (simp add: expr.simps) moreover have "sender e\<^sub>l = address env" using el_def ffold_init_ad_same[of members "(emptyEnv ad cname (address env) v)" "fmdom members" e\<^sub>l] unfolding emptyEnv_def by simp ultimately show ?thesis using that hash_def by (simp add:ssel.simps) qed ultimately show "rv= LStoreloc (address env + (STR ''.'' + STR ''balance''))" and "rt=Storage (STValue (TUInt 256))" using assms(2) by (simp add: lexp.simps)+ qed lemma expr_balance: assumes "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g1\) g1 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g1')" and "expr (LVAL (Ref (STR ''balance'') [SENDER])) e\<^sub>l cd\<^sub>l (st\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g2\) g2 = Normal ((va, ta), g'a)" shows "va= KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) (storage st ad))" and "ta = Value (TUInt 256)" proof - have "fmlookup (denvalue (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" unfolding emptyEnv_def using ffold_init_fmdom balance by simp moreover have el_def: "e\<^sub>l = (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))" using load_empty_par[OF assms(1)] by (simp add:load.simps) ultimately have *: "fmlookup (denvalue e\<^sub>l) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" using assms by auto moreover obtain g'' where "ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] e\<^sub>l cd\<^sub>l (st\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g2\) g2 = Normal (((address env) + (STR ''.'' + STR ''balance''), STValue (TUInt 256)), g'')" proof - have "g2 > costs\<^sub>e SENDER e\<^sub>l cd\<^sub>l (st\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g2\)" using assms(2) * by (simp add: expr.simps ssel.simps rexp.simps split:if_split_asm) then obtain g'' where "expr SENDER e\<^sub>l cd\<^sub>l (st\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g2\) g2 = Normal ((KValue (sender e\<^sub>l), Value TAddr), g'')" by (simp add:expr.simps ssel.simps rexp.simps) moreover have "sender e\<^sub>l = address env" using el_def ffold_init_ad_same[of members "(emptyEnv ad cname (address env) v)" "fmdom members" e\<^sub>l] unfolding emptyEnv_def by simp ultimately show ?thesis using that hash_def by (simp add:expr.simps ssel.simps rexp.simps) qed moreover have "ad = address e\<^sub>l" using el_def ffold_init_ad_same[of members "(emptyEnv ad cname (address env) v)" "fmdom members" e\<^sub>l] unfolding emptyEnv_def by simp ultimately show "va= KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) (storage st ad))" and "ta = Value (TUInt 256)" using assms(2) by (simp add:expr.simps ssel.simps rexp.simps split:if_split_asm)+ qed lemma balance_inj: "inj_on (\(ad, x). (ad + (STR ''.'' + STR ''balance''),x)) {(ad, x). (fmlookup y \ f) ad = Some x}" proof fix v v' assume asm1: "v \ {(ad, x). (fmlookup y \ f) ad = Some x}" and asm2: "v' \ {(ad, x). (fmlookup y \ f) ad = Some x}" and *:"(case v of (ad, x) \ (ad + (STR ''.'' + STR ''balance''),x)) = (case v' of (ad, x) \ (ad + (STR ''.'' + STR ''balance''),x))" then obtain ad ad' x x' where **: "v = (ad,x)" and ***: "v'=(ad',x')" by auto moreover from * ** *** have "ad + (STR ''.'' + STR ''balance'') = ad' + (STR ''.'' + STR ''balance'')" by simp with * ** have "ad = ad'" using String_Cancel[of ad "STR ''.'' + STR ''balance''" ad' ] by simp moreover from asm1 asm2 ** *** have "(fmlookup y \ f) ad = Some x" and "(fmlookup y \ f) ad' = Some x'" by auto with calculation(3) have "x=x'" by simp ultimately show "v=v'" by simp qed lemma fmfinite: "finite ({(ad, x). fmlookup y ad = Some x})" proof - have "{(ad, x). fmlookup y ad = Some x} \ dom (fmlookup y) \ ran (fmlookup y)" proof fix x assume "x \ {(ad, x). fmlookup y ad = Some x}" then have "fmlookup y (fst x) = Some (snd x)" by auto then have "fst x \ dom (fmlookup y)" and "snd x \ ran (fmlookup y)" using Map.ranI by (blast,metis) then show "x \ dom (fmlookup y) \ ran (fmlookup y)" by (simp add: mem_Times_iff) qed thus ?thesis by (simp add: finite_ran finite_subset) qed lemma fmlookup_finite: fixes f :: "'a \ 'a" and y :: "('a, 'b) fmap" assumes "inj_on (\(ad, x). (f ad, x)) {(ad, x). (fmlookup y \ f) ad = Some x}" shows "finite {(ad, x). (fmlookup y \ f) ad = Some x}" proof (cases rule: inj_on_finite[OF assms(1), of "{(ad, x)|ad x. (fmlookup y) ad = Some x}"]) case 1 then show ?case by auto next case 2 then have *: "finite {(ad, x) |ad x. fmlookup y ad = Some x}" using fmfinite[of y] by simp show ?case using finite_image_set[OF *, of "\(ad, x). (ad, x)"] by simp qed lemma expr_plus: assumes "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g3\) g3 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g3')" and "expr (PLUS a0 b0) ev0 cd0 st0 g0 = Normal ((xs, t'0), g'0)" shows "\s. xs = KValue (s)" using assms by (auto simp add:expr.simps split:if_split_asm result.split_asm prod.split_asm Stackvalue.split_asm Type.split_asm option.split_asm) lemma summ_eq_sum: "SUMM s' = (\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr. ReadL\<^sub>i\<^sub>n\<^sub>t x) + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (adr + (STR ''.'' + STR ''balance'')) s')" proof (cases "fmlookup s' (adr + (STR ''.'' + STR ''balance'')) = None") case True then have "accessStorage (TUInt 256) (adr + (STR ''.'' + STR ''balance'')) s' = ShowL\<^sub>i\<^sub>n\<^sub>t 0" unfolding accessStorage_def by simp moreover have "{(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x} = {(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" proof show "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x} \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" proof fix x assume "x \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" then show "x \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" using True by auto qed next show "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr} \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x }" proof fix x assume "x \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" then show "x \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" using True by auto qed qed then have "SUMM s' = (\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr. ReadL\<^sub>i\<^sub>n\<^sub>t x)" by simp ultimately show ?thesis using Read_ShowL_id by simp next case False then obtain val where val_def: "fmlookup s' (adr + (STR ''.'' + STR ''balance'')) = Some val" by auto have "inj_on (\(ad, x). (ad + (STR ''.'' + STR ''balance''), x)) {(ad, x). (fmlookup s' \ (\ad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using balance_inj by simp then have "finite {(ad, x). (fmlookup s' \ (\ad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using fmlookup_finite[of "\ad. (ad + (STR ''.'' + STR ''balance''))" s'] by simp then have sum1: "finite ({(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr})" using finite_subset[of "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}"] by auto moreover have sum2: "(adr,val) \ {(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" by simp moreover from sum1 val_def have "insert (adr,val) {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr} = {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" by auto ultimately show ?thesis using sum.insert[OF sum1 sum2, of "\(ad,x). ReadL\<^sub>i\<^sub>n\<^sub>t x"] val_def unfolding accessStorage_def by simp qed lemma sum_eq_update: assumes s''_def: "s'' = fmupd (adr + (STR ''.'' + STR ''balance'')) v' s'" shows "(\(ad,x)|fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr. ReadL\<^sub>i\<^sub>n\<^sub>t x) =(\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr. ReadL\<^sub>i\<^sub>n\<^sub>t x)" proof - have "{(ad,x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr} = {(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" proof show "{(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr} \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" proof fix xx assume "xx \ {(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" then obtain ad x where "xx = (ad,x)" and "fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x" and "ad \ adr" by auto then have "fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x" using String_Cancel[of ad "(STR ''.'' + STR ''balance'')" "adr"] s''_def by (simp split:if_split_asm) with `ad \ adr` `xx = (ad,x)` show "xx \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" by simp qed next show "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr} \ {(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" proof fix xx assume "xx \ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" then obtain ad x where "xx = (ad,x)" and "fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x" and "ad \ adr" by auto then have "fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x" using String_Cancel[of ad "(STR ''.'' + STR ''balance'')" "adr"] s''_def by (auto split:if_split_asm) with `ad \ adr` `xx = (ad,x)` show "xx \ {(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ adr}" by simp qed qed thus ?thesis by simp qed lemma adapt_deposit: assumes "address env \ ad" and "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st0\gas := g3\) g3 = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g3')" and "Accounts.transfer (address env) ad v a = Some acc" and "iv (storage st0 ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v)" and "lexp myrexp e\<^sub>l cd\<^sub>l (st0\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g'\) g' = Normal ((LStoreloc l, Storage (STValue t')), g''a)" and "expr (PLUS mylval VALUE) e\<^sub>l cd\<^sub>l (st0\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g\) g = Normal ((KValue va, Value ta), g')" and "Valuetypes.convert ta t' va = Some v'" shows "(ad = address e\<^sub>l \ iv (storage st0 (address e\<^sub>l)(l $$:= v')) \bal (acc (address e\<^sub>l))\) \ (ad \ address e\<^sub>l \ iv (storage st0 ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad))))" proof (rule conjI; rule impI) assume "ad = address e\<^sub>l" define s' s'' where "s' = storage st0 (address e\<^sub>l)" and "s'' = storage st0 (address e\<^sub>l)(l $$:= v')" then have "s'' = fmupd l v' s'" by simp moreover from lexp_myrexp[OF assms(2) assms(5)] have "l = address env + (STR ''.'' + STR ''balance'')" and "t'=TUInt 256" by simp+ ultimately have s''_s': "s'' = s' (address env + (STR ''.'' + STR ''balance'') $$:= v')" by simp have "fmlookup (denvalue (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" unfolding emptyEnv_def using ffold_init_fmdom balance by simp moreover have "e\<^sub>l = (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))" using load_empty_par[OF assms(2)] by (simp add:load.simps) ultimately have "fmlookup (denvalue e\<^sub>l) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))" by simp then have va_def: "va = (createUInt 256 ((ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) ((sender e\<^sub>l) + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t (svalue e\<^sub>l))))" and "ta = (TUInt 256)" using assms(6) Read_ShowL_id unfolding s'_def by (auto split:if_split_asm simp add: expr.simps ssel.simps rexp.simps add_def olift.simps hash_def) have "svalue e\<^sub>l = v" and "sender e\<^sub>l = address env" and "address e\<^sub>l = ad" using ffold_init_ad_same msel_ssel_expr_load_rexp_gas(4)[OF assms(2)] unfolding emptyEnv_def by simp+ then have a_frame: "iv s' (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v)" using assms(4) unfolding s'_def by simp from assms(1) have "ReadL\<^sub>i\<^sub>n\<^sub>t (bal (a ad)) + ReadL\<^sub>i\<^sub>n\<^sub>t v < 2^256" using transfer_val2[OF assms(3)] by simp moreover from `address env \ ad` have "ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) = ReadL\<^sub>i\<^sub>n\<^sub>t (bal (a ad)) + ReadL\<^sub>i\<^sub>n\<^sub>t v" using transfer_add[OF assms(3)] by simp ultimately have a_bal: "ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) < 2^256" by simp moreover have a_bounds: "ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) s') + \svalue e\<^sub>l\ < 2 ^ 256 \ ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) s') + \svalue e\<^sub>l\ \ 0" proof (cases "fmlookup s' (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) = None") case True hence "(accessStorage (TUInt 256) (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) s') = ShowL\<^sub>i\<^sub>n\<^sub>t 0" unfolding accessStorage_def by simp moreover have "(\svalue e\<^sub>l\::int) < 2 ^ 256" proof - from a_frame have "\svalue e\<^sub>l\ + SUMM s' \ ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad))" unfolding iv_def using `svalue e\<^sub>l = v` by simp moreover have "0 \ SUMM s'" using a_frame sum_nonneg[of "{(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" "\(ad,x). ReadL\<^sub>i\<^sub>n\<^sub>t x"] unfolding iv_def by auto ultimately have "\svalue e\<^sub>l\ \ ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad))" by simp then show "(\svalue e\<^sub>l\::int) < 2 ^ 256" using a_bal by simp qed moreover have "ReadL\<^sub>i\<^sub>n\<^sub>t v \ 0" using transfer_val1[OF assms(3)] by simp with `svalue e\<^sub>l = v` have "(\svalue e\<^sub>l\::int) \ 0" by simp ultimately show ?thesis using Read_ShowL_id by simp next case False then obtain x where x_def: "fmlookup s' (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) = Some x" by auto moreover from a_frame have "\svalue e\<^sub>l\ + SUMM s' \ ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad))" unfolding iv_def using `svalue e\<^sub>l = v` by simp moreover have "(case (sender e\<^sub>l, x) of (ad, x) \ \x\) \ (\(ad, x)\{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}. ReadL\<^sub>i\<^sub>n\<^sub>t x)" proof (cases rule: member_le_sum[of "(sender e\<^sub>l,x)" "{(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" "\(ad,x). ReadL\<^sub>i\<^sub>n\<^sub>t x"]) case 1 then show ?case using x_def by simp next case (2 x) with a_frame show ?case unfolding iv_def by auto next case 3 have "inj_on (\(ad, x). (ad + (STR ''.'' + STR ''balance''), x)) {(ad, x). (fmlookup s' \ (\ad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using balance_inj by simp then have "finite {(ad, x). (fmlookup s' \ (\ad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using fmlookup_finite[of "\ad. (ad + (STR ''.'' + STR ''balance''))" s'] by simp then show ?case using finite_subset[of "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}"] by auto qed then have "ReadL\<^sub>i\<^sub>n\<^sub>t x \ SUMM s'" by simp ultimately have "\svalue e\<^sub>l\ + ReadL\<^sub>i\<^sub>n\<^sub>t x \ ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad))" by simp then have "\svalue e\<^sub>l\ + ReadL\<^sub>i\<^sub>n\<^sub>t x \ ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad))" by simp with a_bal have "\svalue e\<^sub>l\ + ReadL\<^sub>i\<^sub>n\<^sub>t x < 2^256" by simp then have "\svalue e\<^sub>l\ \ \bal (acc ad)\ - SUMM s'" and lck: "fmlookup s' (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) = Some x" and "ReadL\<^sub>i\<^sub>n\<^sub>t x + \svalue e\<^sub>l\ < 2 ^ 256" using a_frame x_def `svalue e\<^sub>l = v` unfolding iv_def by auto moreover from lck have "(accessStorage (TUInt 256) (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) s') = x" unfolding accessStorage_def by simp moreover have "\svalue e\<^sub>l\ + ReadL\<^sub>i\<^sub>n\<^sub>t x \ 0" proof - have "ReadL\<^sub>i\<^sub>n\<^sub>t v \ 0" using transfer_val1[OF assms(3)] by simp with `svalue e\<^sub>l = v` have "(\svalue e\<^sub>l\::int) \ 0" by simp moreover from a_frame have "ReadL\<^sub>i\<^sub>n\<^sub>t x \ 0" unfolding iv_def using x_def by simp ultimately show ?thesis by simp qed ultimately show ?thesis using Read_ShowL_id by simp qed ultimately have "va = ShowL\<^sub>i\<^sub>n\<^sub>t (ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t (svalue e\<^sub>l))" using createUInt_id[where ?v="ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e\<^sub>l + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t (svalue e\<^sub>l)"] va_def by simp then have v'_def: "v' = ShowL\<^sub>i\<^sub>n\<^sub>t (ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v)" using `sender e\<^sub>l = address env` `svalue e\<^sub>l = v` `t'=TUInt 256` `ta = (TUInt 256)` using assms(7) by auto have "SUMM s'' \ \bal (acc ad)\" proof - have "SUMM s' \ ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v" using a_frame unfolding iv_def by simp moreover have "SUMM s'' = SUMM s' + ReadL\<^sub>i\<^sub>n\<^sub>t v" proof - from summ_eq_sum have s1: "SUMM s' = (\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env. ReadL\<^sub>i\<^sub>n\<^sub>t x) + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s')" by simp have s2: "SUMM s'' = (\(ad,x)|fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env. ReadL\<^sub>i\<^sub>n\<^sub>t x) + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v" proof - have "inj_on (\(ad, x). (ad + (STR ''.'' + STR ''balance''), x)) {(ad, x). (fmlookup s'' \ (\ad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using balance_inj by simp then have "finite {(ad, x). (fmlookup s'' \ (\ad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using fmlookup_finite[of "\ad. (ad + (STR ''.'' + STR ''balance''))" s''] by simp then have sum1: "finite ({(ad,x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env})" using finite_subset[of "{(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env}" "{(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x}"] by auto moreover have sum2: "(address env, ShowL\<^sub>i\<^sub>n\<^sub>t (ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v)) \ {(ad,x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env}" by simp moreover from v'_def s''_s' have "insert (address env, ShowL\<^sub>i\<^sub>n\<^sub>t (ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v)) {(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env} = {(ad, x). fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x}" by auto then show ?thesis using sum.insert[OF sum1 sum2, of "\(ad,x). ReadL\<^sub>i\<^sub>n\<^sub>t x"] Read_ShowL_id by simp qed from sum_eq_update[OF s''_s'] have s3: "(\(ad,x)|fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env. ReadL\<^sub>i\<^sub>n\<^sub>t x) =(\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env. ReadL\<^sub>i\<^sub>n\<^sub>t x)" by simp moreover from s''_s' v'_def have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s'') = ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v" using Read_ShowL_id unfolding accessStorage_def by simp ultimately have "SUMM s''= SUMM s' + ReadL\<^sub>i\<^sub>n\<^sub>t v" proof - from s2 have "SUMM s'' = (\(ad,x)|fmlookup s'' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env. ReadL\<^sub>i\<^sub>n\<^sub>t x) + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v" by simp also from s3 have "\ = (\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ address env. ReadL\<^sub>i\<^sub>n\<^sub>t x) + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v" by simp also from s1 have "\ = SUMM s' - ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') + ReadL\<^sub>i\<^sub>n\<^sub>t v" by simp finally show ?thesis by simp qed then show ?thesis by simp qed ultimately show ?thesis by simp qed moreover have "POS s''" proof (rule allI[OF allI]) fix x xa show "fmlookup s'' (x + (STR ''.'' + STR ''balance'')) = Some xa \ 0 \ (\xa\::int)" proof assume a_lookup: "fmlookup s'' (x + (STR ''.'' + STR ''balance'')) = Some xa" show "0 \ (\xa\::int)" proof (cases "x = address env") case True then show ?thesis using s''_s' a_lookup using Read_ShowL_id v'_def a_bounds `sender e\<^sub>l = address env` `svalue e\<^sub>l = v` by auto next case False then have "fmlookup s' (x + (STR ''.'' + STR ''balance'')) = Some xa" using s''_s' a_lookup String_Cancel[of "address env" "(STR ''.'' + STR ''balance'')" x] by (simp split:if_split_asm) then show ?thesis using a_frame unfolding iv_def by simp qed qed qed ultimately show "iv (storage st0 (address e\<^sub>l)(l $$:= v')) \bal (acc (address e\<^sub>l))\" unfolding iv_def s''_def using `ad = address e\<^sub>l` by simp next assume "ad \ address e\<^sub>l" moreover have "ad = address e\<^sub>l" using ffold_init_ad_same msel_ssel_expr_load_rexp_gas(4)[OF assms(2)] unfolding emptyEnv_def by simp ultimately show "iv (storage st0 ad) \bal (acc ad)\" by simp qed lemma adapt_withdraw: fixes st acc sck' mem' g''a e' l v' xe defines "st' \ st\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st) (address e' := (storage st (address e')) (l $$:= v'))\" assumes "iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v)" and "load True [] xe (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members)) emptyStore emptyStore emptyStore env cd (st\gas := g'\) g' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g'')" and "decl STR ''bal'' (Value (TUInt 256)) (Some (va, ta)) False cd\<^sub>l m\<^sub>l (storage st) (cd\<^sub>l, m\<^sub>l, k\<^sub>l, e\<^sub>l) = Some (cd', mem', sck', e')" and "expr (UINT 256 0) e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := ga\) ga = Normal ((KValue vb, Value tb), g'b)" and "Valuetypes.convert tb t' vb = Some v'" and "lexp myrexp e' cd' (st\accounts := acc, stack := sck', memory := mem', gas := g'b\) g'b = Normal ((LStoreloc l, Storage (STValue t')), g''a)" and "expr mylval e\<^sub>l cd\<^sub>l (st\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g'' - costs keep e\<^sub>l cd\<^sub>l (st\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\)\) (g'' - costs keep e\<^sub>l cd\<^sub>l (st\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\)) = Normal ((va, ta), g'a)" and "Accounts.transfer (address env) ad v (accounts st) = Some acc" and "expr SENDER e' cd' (st' \gas := g\) g = Normal ((KValue adv, Value TAddr), g'x)" and adv_def: "adv \ ad" and bal: "expr (LVAL (L.Id STR ''bal'')) e' cd' (st'\gas := g''b\) g''b = Normal ((KValue lv, Value t), g''')" and con: "Valuetypes.convert t (TUInt 256) lv = Some lv'" shows "iv (storage st' ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (accounts st' ad)) - (ReadL\<^sub>i\<^sub>n\<^sub>t lv'))" proof - define acca where "acca = accounts st' ad" define s' where "s' = storage st (address e')" define s'a where "s'a = storage st' ad" moreover have "address e' = ad" proof - have "address e' = address e\<^sub>l" using decl_env[OF assms(4)] by simp also have "address e\<^sub>l = address (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))" using msel_ssel_expr_load_rexp_gas(4)[OF assms(3)] by simp also have "\ = ad" unfolding emptyEnv_def using ffold_init_ad_same by simp finally show ?thesis . qed ultimately have s'a_def: "s'a = fmupd l v' s'" unfolding s'_def st'_def by simp have "sender e' = address env" proof - have "sender e' = sender e\<^sub>l" using decl_env[OF assms(4)] by simp also have "sender e\<^sub>l = sender (ffold (init members) (emptyEnv ad cname (address env) v) (fmdom members))" using msel_ssel_expr_load_rexp_gas(4)[OF assms(3)] by simp also have "\ = address env" unfolding emptyEnv_def using ffold_init_ad_same by simp finally show ?thesis . qed have "iv s'a (\bal acca\ - \lv'\)" unfolding iv_def proof intros have "SUMM s' \ \bal acca\" proof - from `address e' = ad` have "iv s' (ReadL\<^sub>i\<^sub>n\<^sub>t (bal acca) - ReadL\<^sub>i\<^sub>n\<^sub>t v)" using assms(2,5) unfolding s'_def st'_def acca_def by simp then have "SUMM s' \ \bal (acca)\ - \v\" unfolding iv_def by simp moreover have "ReadL\<^sub>i\<^sub>n\<^sub>t v \ 0" using transfer_val1[OF assms(9)] by simp ultimately show ?thesis by simp qed moreover have "SUMM s'a = SUMM s' - ReadL\<^sub>i\<^sub>n\<^sub>t lv'" proof - from summ_eq_sum have "SUMM s'a = (\(ad,x)|fmlookup s'a (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ sender e'. ReadL\<^sub>i\<^sub>n\<^sub>t x) + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e' + (STR ''.'' + STR ''balance'')) s'a)" by simp moreover from summ_eq_sum have "SUMM s' = (\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ sender e'. ReadL\<^sub>i\<^sub>n\<^sub>t x) + ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e' + (STR ''.'' + STR ''balance'')) s')" by simp moreover from s'a_def lexp_myrexp_decl(1)[OF assms(3,4) assms(7)] have " s'a = s'((sender e' + (STR ''.'' + STR ''balance''))$$:= v')" using `sender e' = address env` by simp with sum_eq_update have "(\(ad,x)|fmlookup s'a (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ sender e'. ReadL\<^sub>i\<^sub>n\<^sub>t x) = (\(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x \ ad \ sender e'. ReadL\<^sub>i\<^sub>n\<^sub>t x)" by simp moreover have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e' + (STR ''.'' + STR ''balance'')) s'a) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e' + (STR ''.'' + STR ''balance'')) s') - ReadL\<^sub>i\<^sub>n\<^sub>t lv'" proof - have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e' + (STR ''.'' + STR ''balance'')) s') = ReadL\<^sub>i\<^sub>n\<^sub>t lv'" proof - from expr_balance[OF assms(3) assms(8)] have "va= KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s')" and "ta = Value (TUInt 256)" using `address e' = ad` unfolding s'_def by simp+ then have "(sck',e') = astack STR ''bal'' (Value (TUInt 256)) (KValue (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s')) (k\<^sub>l, e\<^sub>l)" using decl.simps(2) assms(4) by simp then have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (address env + (STR ''.'' + STR ''balance'')) s') = ReadL\<^sub>i\<^sub>n\<^sub>t lv" and "t = TUInt 256" using expr_bal bal unfolding s'_def st'_def by auto moreover from `t = TUInt 256` have "lv = lv'" using con by simp ultimately show ?thesis using `sender e' = address env` by simp qed moreover have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessStorage (TUInt 256) (sender e' + (STR ''.'' + STR ''balance'')) s'a) = ReadL\<^sub>i\<^sub>n\<^sub>t (ShowL\<^sub>i\<^sub>n\<^sub>t 0)" proof - have "v' = ShowL\<^sub>i\<^sub>n\<^sub>t 0" proof - have "vb = createUInt 256 0" and "tb=TUInt 256" using assms(5) by (simp add: expr.simps load.simps split:if_split_asm)+ moreover have "t'=TUInt 256" using lexp_myrexp_decl(2)[OF assms(3,4) assms(7)] by simp ultimately show ?thesis using assms(6) by (simp add: createUInt_id) qed moreover have "l= (sender e' + (STR ''.'' + STR ''balance''))" using lexp_myrexp_decl(1)[OF assms(3,4) assms(7)] `sender e' = address env` by simp ultimately show ?thesis using s'a_def accessStorage_def by simp qed ultimately show ?thesis using Read_ShowL_id by simp qed ultimately show ?thesis by simp qed ultimately show "SUMM s'a \ \bal acca\ - \lv'\" by simp next fix ad' x assume *: "fmlookup s'a (ad' + (STR ''.'' + STR ''balance'')) = Some x" show "0 \ ReadL\<^sub>i\<^sub>n\<^sub>t x" proof (cases "ad' = sender e'") case True moreover have "v' = ShowL\<^sub>i\<^sub>n\<^sub>t 0" proof - have "vb = createUInt 256 0" and "tb=TUInt 256" using assms(5) by (simp add:expr.simps split:if_split_asm)+ moreover have "t'=TUInt 256" using lexp_myrexp_decl(2)[OF assms(3,4) assms(7)] by simp ultimately show ?thesis using assms(6) by (simp add: createUInt_id) qed moreover have "l= (sender e' + (STR ''.'' + STR ''balance''))" using lexp_myrexp_decl(1)[OF assms(3,4) assms(7)] `sender e' = address env` by simp ultimately show ?thesis using Read_ShowL_id s'a_def * by auto next case False moreover from `address e' = ad` have "iv s' (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v)" using assms(2) unfolding s'_def by simp then have "POS s'" unfolding iv_def by simp moreover have "l= (sender e' + (STR ''.'' + STR ''balance''))" using lexp_myrexp_decl(1)[OF assms(3,4) assms(7)] `sender e' = address env` by simp ultimately show ?thesis using s'a_def * String_Cancel by (auto split:if_split_asm) qed qed then show ?thesis unfolding s'a_def s'_def acca_def st'_def `address e' = ad` by simp qed lemma wp_deposit[external]: assumes "address ev \ ad" and "expr adex ev cd (st\gas := gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0\) (gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0) = Normal ((KValue ad, Value TAddr), g)" and "expr val ev cd (st0\gas := g\) g = Normal ((KValue v, Value t), g')" and "Valuetypes.convert t (TUInt 256) v = Some v'" and "load True [] xe (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore emptyStore emptyStore ev cd (st0\gas := g'\) g' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g'')" and "Accounts.transfer (address ev) ad v' (accounts st0) = Some acc" and "iv (storage st0 ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v')" shows "wpS (stmt (ASSIGN myrexp (PLUS mylval VALUE)) e\<^sub>l cd\<^sub>l) (\st. (iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (accounts st ad))))) (\e. e = Gas \ e = Err) (st0\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\)" apply (vcg_assign expr_rule: expr_plus[OF assms(5)] lexp_rule: lexp_myrexp(1)[OF assms(5)]) by (simp add: adapt_deposit[OF assms(1,5,6,7)]) lemma wptransfer: fixes st0 acc sck' mem' g''a e' l v' defines "st' \ st0\accounts := acc, stack := sck', memory := mem', gas := g''a, storage := (storage st0)(address e' := storage st0 (address e')(l $$:= v'))\" assumes "Pfe ad iv st'" and "address ev \ ad" and "g'' \ gas st" and "type (acc ad) = Some (Contract cname)" and "expr adex ev cd (st0\gas := gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0\) (gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0) = Normal ((KValue ad, Value TAddr), g)" and "expr val ev cd (st0\gas := g\) g = Normal ((KValue gv, Value gt), g')" and "Valuetypes.convert gt (TUInt 256) gv = Some gv'" and "load True [] xe (ffold (init members) (emptyEnv ad cname (address ev) gv') (fmdom members)) emptyStore emptyStore emptyStore ev cd (st0\gas := g'\) g' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g'')" and "Accounts.transfer (address ev) ad gv' (accounts st0) = Some acc" and "iv (storage st0 ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t gv')" and "decl STR ''bal'' (Value (TUInt 256)) (Some (v, t)) False cd\<^sub>l m\<^sub>l (storage st0) (cd\<^sub>l, m\<^sub>l, k\<^sub>l, e\<^sub>l) = Some (cd', mem', sck', e')" and "Valuetypes.convert ta t' va = Some v'" and "lexp myrexp e' cd' (st0\accounts := acc, stack := sck', memory := mem', gas := g'a\) g'a = Normal ((LStoreloc l, Storage (STValue t')), g''a)" and "expr mylval e\<^sub>l cd\<^sub>l (st0\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l, gas := g'' - costs (BLOCK ((STR ''bal'', Value (TUInt 256)), Some mylval) (COMP (ASSIGN myrexp (UINT 256 0)) Reentrancy.transfer)) e\<^sub>l cd\<^sub>l (st0\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\)\) (g'' - costs (BLOCK ((STR ''bal'', Value (TUInt 256)), Some mylval) (COMP (ASSIGN myrexp (UINT 256 0)) Reentrancy.transfer)) e\<^sub>l cd\<^sub>l (st0\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\)) = Normal ((v, t), g''')" and "expr (UINT 256 0) e' cd' (st0\accounts := acc, stack := sck', memory := mem', gas := ga\) ga = Normal ((KValue va, Value ta), g'a)" shows "wpS (stmt Reentrancy.transfer e' cd') (\st. iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (accounts st ad)))) (\e. e = Gas \ e = Err) st'" proof (rule meta_eq_to_obj_eq[THEN iffD1, OF Pfe_def assms(2),rule_format], (rule conjI; (rule conjI)?)) show "address e' = ad" proof - have "address e' = address e\<^sub>l" using decl_env[OF assms(12)] by simp also have "address e\<^sub>l = address (ffold (init members) (emptyEnv ad cname (address ev) gv') (fmdom members))" using msel_ssel_expr_load_rexp_gas(4)[OF assms(9)] by simp also have "\ = ad" unfolding emptyEnv_def using ffold_init_ad_same by simp finally show ?thesis . qed next show "\adv g. expr SENDER e' cd' (st'\gas := gas st' - costs Reentrancy.transfer e' cd' st'\) (gas st' - costs Reentrancy.transfer e' cd' st') = Normal ((KValue adv, Value TAddr), g) \ adv \ ad" proof (intros) fix adv g assume "expr SENDER e' cd' (st'\gas := gas st' - costs Reentrancy.transfer e' cd' st'\) (gas st' - costs Reentrancy.transfer e' cd' st') = Normal ((KValue adv, Value TAddr), g)" moreover have "sender e' \ ad" proof - have "sender e' = sender e\<^sub>l" using decl_env[OF assms(12)] by simp also have "sender e\<^sub>l = sender (ffold (init members) (emptyEnv ad cname (address ev) gv') (fmdom members))" using msel_ssel_expr_load_rexp_gas(4)[OF assms(9)] by simp also have "\ = address ev" unfolding emptyEnv_def using ffold_init_ad_same by simp finally show ?thesis using assms(3) by simp qed ultimately show "adv \ ad" by (simp add:expr.simps split:result.split_asm if_split_asm prod.split_asm) qed next show "\adv g v t g' v'. local.expr SENDER e' cd' (st'\gas := gas st' - costs Reentrancy.transfer e' cd' st'\) (gas st' - costs Reentrancy.transfer e' cd' st') = Normal ((KValue adv, Value TAddr), g) \ adv \ ad \ local.expr (LVAL (L.Id STR ''bal'')) e' cd' (st'\gas := g\) g = Normal ((KValue v, Value t), g') \ Valuetypes.convert t (TUInt 256) v = Some v' \ iv (storage st' ad) (\bal (accounts st' ad)\ - ReadL\<^sub>i\<^sub>n\<^sub>t v')" proof elims fix adv lg lv lt lg' lv' assume a1:"expr SENDER e' cd' (st'\gas := gas st' - costs Reentrancy.transfer e' cd' st'\) (gas st' - costs Reentrancy.transfer e' cd' st') = Normal ((KValue adv, Value TAddr), lg)" and adv_def: "adv \ ad" and bal: "expr (LVAL (L.Id STR ''bal'')) e' cd' (st'\gas := lg\) lg = Normal ((KValue lv, Value lt), lg')" and con: "Valuetypes.convert lt (TUInt 256) lv = Some lv'" show "iv (storage st' ad) (\bal (accounts st' ad)\ - ReadL\<^sub>i\<^sub>n\<^sub>t lv')" using adapt_withdraw[where ?acc=acc, OF assms(11) load_empty_par[OF assms(9)] assms(12,16,13,14,15,10) _ adv_def _] a1 bal con unfolding st'_def by simp qed qed lemma wp_withdraw[external]: assumes "\st'. gas st' \ gas st \ type (accounts st' ad) = Some (Contract cname) \ Pe ad iv st' \ Pi ad (\_ _. True) (\_ _. True) st' \ Pfi ad (\_. True) (\_. True) st' \ Pfe ad iv st'" and "address ev \ ad" and "g'' \ gas st" and "type (acc ad) = Some (Contract cname)" and "expr adex ev cd (st0\gas := gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0\) (gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0) = Normal ((KValue ad, Value TAddr), g)" and "expr val ev cd (st0\gas := g\) g = Normal ((KValue v, Value t), g')" and "Valuetypes.convert t (TUInt 256) v = Some v'" and "load True [] xe (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore emptyStore emptyStore ev cd (st0\gas := g'\) g' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g'')" and "Accounts.transfer (address ev) ad v' (accounts st0) = Some acc" and "iv (storage st0 ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v')" shows "wpS (stmt keep e\<^sub>l cd\<^sub>l) (\st. iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (accounts st ad)))) (\e. e = Gas \ e = Err) (st0\gas := g'', accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\)" apply vcg_block_some apply vcg_comp apply (vcg_assign expr_rule: expr_0[OF assms(8)] lexp_rule: lexp_myrexp_decl[OF assms(8)]) apply (rule wptransfer[OF _ assms(2-10)]) apply (rule_tac assms(1)[THEN conjunct2,THEN conjunct2,THEN conjunct2]) using assms(3,4) by simp lemma wp_fallback: assumes "Accounts.transfer (address ev) ad v (accounts st0) = Some acca" and "iv (storage st0 ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acca ad)) - ReadL\<^sub>i\<^sub>n\<^sub>t v)" shows "wpS (stmt SKIP (ffold (init members) (emptyEnv ad cname (address ev) vc) (fmdom members)) emptyStore) (\st. iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (accounts st ad)))) (\e. e = Gas \ e = Err) (st0\gas := g'c, accounts := acca, stack := emptyStore, memory := emptyStore\)" apply vcg_skip using weaken[where ?acc=acca, OF assms(2) transfer_val1[OF assms(1)]] by auto lemma wp_construct: assumes "Accounts.transfer (address ev) (hash (address ev) \contracts (accounts st (address ev))\) v ((accounts st) (hash (address ev) \contracts (accounts st (address ev))\ := \bal = ShowL\<^sub>i\<^sub>n\<^sub>t 0, type = Some (Contract i), contracts = 0\)) = Some acc" shows "iv fmempty \bal (acc (hash (address ev) \contracts (accounts st (address ev))\))\" proof - define adv where "adv = (hash (address ev) \contracts (accounts st (address ev))\)" moreover have "ReadL\<^sub>i\<^sub>n\<^sub>t (bal (((accounts st) (adv := \bal = ShowL\<^sub>i\<^sub>n\<^sub>t 0, type = Some (Contract i), contracts = 0\)) adv)) = 0" using Read_ShowL_id[of 0] by simp ultimately have "ReadL\<^sub>i\<^sub>n\<^sub>t (bal (acc (hash (address ev) \contracts (accounts st (address ev))\))) \ 0" using transfer_mono[OF assms(1)] by simp then show ?thesis unfolding iv_def by simp qed lemma wp_true[external]: assumes "E Gas" and "E Err" shows "wpS (stmt f e cd) (\st. True) E st" unfolding wpS_def wp_def proof ((split result.split, (split prod.split)?); rule conjI; (rule allI)+; (rule impI)+) fix x1 x1a s assume "x1 = (x1a, s)" and "stmt f e cd st = Normal x1" then show "gas s \ gas st \ True" using stmt_gas by simp next fix x2 assume "stmt f e cd st = Exception x2" show "E x2" using assms Ex.nchotomy by metis qed subsubsection\Final results\ interpretation vcg:VCG costs\<^sub>e ep costs cname members const fb "\_. True" "\_. True" "\_ _. True" "\_ _. True" by (simp add: VCG.intro Calculus_axioms) lemma safe_external: "Qe ad iv (st::State)" apply (external cases: cases_ext) apply (rule wp_deposit;assumption) apply vcg_block_some apply vcg_comp apply (vcg_assign expr_rule: expr_0 lexp_rule: lexp_myrexp_decl) apply (vcg.vcg_transfer_ext ad fallback_int: wp_true fallback_ext: wp_fallback cases_ext:cases_ext cases_int:cases_fb cases_fb:cases_int invariant:adapt_withdraw) done lemma safe_fallback: "Qfe ad iv st" apply (fallback cases: cases_fb) apply (rule wp_fallback; assumption) done lemma safe_constructor: "constructor iv" apply (constructor cases: cases_cons) apply vcg_skip apply (simp add:wp_construct) done theorem safe: assumes "\ad. address ev \ ad \ type (accounts st ad) = Some (Contract cname) \ iv (storage st ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (accounts st ad)))" shows "\(st'::State) ad. stmt f ev cd st = Normal ((), st') \ type (accounts st' ad) = Some (Contract cname) \ address ev \ ad \ iv (storage st' ad) (ReadL\<^sub>i\<^sub>n\<^sub>t (bal (accounts st' ad)))" apply (rule invariant) using assms safe_external safe_fallback safe_constructor by auto end end