diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,757 +1,755 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream -Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel CRDT CRYSTALS-Kyber CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Crypto_Standards Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Statecharts -Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Solidity/Solidity_Symbex.thy b/thys/Solidity/Solidity_Symbex.thy --- a/thys/Solidity/Solidity_Symbex.thy +++ b/thys/Solidity/Solidity_Symbex.thy @@ -1,29 +1,29 @@ section\Towards a Setup for Symbolic Evaluation of Solidity\ text\ In this chapter, we lay out the foundations for a tactic for executing Solidity statements and expressions symbolically. \ theory Solidity_Symbex imports Main "HOL-Eisbach.Eisbach" begin lemma string_literal_cat: "a+b = String.implode ((String.explode a) @ (String.explode b))" by (metis String.implode_explode_eq plus_literal.rep_eq) lemma string_literal_conv: "(map String.ascii_of y = y) \ (x = String.implode y) = (String.explode x = y) " by auto lemmas string_literal_opt = Literal.rep_eq zero_literal.rep_eq plus_literal.rep_eq string_literal_cat string_literal_conv named_theorems solidity_symbex method solidity_symbex declares solidity_symbex = - ((simp add:solidity_symbex cong:unit.case), (simp add:string_literal_opt)?; (code_simp,simp?)+) + ((simp add:solidity_symbex cong:unit.case), (simp add:string_literal_opt)?; (code_simp|simp add:string_literal_opt)+) declare Let_def [solidity_symbex] o_def [solidity_symbex] end diff --git a/thys/Solidity/Statements.thy b/thys/Solidity/Statements.thy --- a/thys/Solidity/Statements.thy +++ b/thys/Solidity/Statements.thy @@ -1,2651 +1,2647 @@ section \Statements\ theory Statements imports Expressions StateMonad begin locale statement_with_gas = expressions_with_gas + fixes costs :: "S \ Environment \ CalldataT \ State \ Gas" assumes while_not_zero[termination_simp]: "\e cd st ex s0. 0 < (costs (WHILE ex s0) e cd st) " and invoke_not_zero[termination_simp]: "\e cd st i xe. 0 < (costs (INVOKE i xe) e cd st)" and external_not_zero[termination_simp]: "\e cd st ad i xe val. 0 < (costs (EXTERNAL ad i xe val) e cd st)" and transfer_not_zero[termination_simp]: "\e cd st ex ad. 0 < (costs (TRANSFER ad ex) e cd st)" and new_not_zero[termination_simp]: "\e cd st i xe val. 0 < (costs (NEW i xe val) e cd st)" begin subsection \Semantics of left expressions\ text \We first introduce lexp.\ fun lexp :: "L \ Environment \ CalldataT \ State \ (LType * Type, Ex, Gas) state_monad" where "lexp (Id i) e _ st g = (case (denvalue e) $$ i of Some (tp, (Stackloc l)) \ return (LStackloc l, tp) | Some (tp, (Storeloc l)) \ return (LStoreloc l, tp) | _ \ throw Err) g" | "lexp (Ref i r) e cd st g = (case (denvalue e) $$ i of Some (tp, Stackloc l) \ (case accessStore l (stack st) of Some (KCDptr _) \ throw Err | Some (KMemptr l') \ do { t \ (case tp of Memory t \ return t | _ \ throw Err); (l'', t') \ msel True t l' r e cd st; return (LMemloc l'', Memory t') } | Some (KStoptr l') \ do { t \ (case tp of Storage t \ return t | _ \ throw Err); (l'', t') \ ssel t l' r e cd st; return (LStoreloc l'', Storage t') } | Some (KValue _) \ throw Err | None \ throw Err) | Some (tp, Storeloc l) \ do { t \ (case tp of Storage t \ return t | _ \ throw Err); (l', t') \ ssel t l r e cd st; return (LStoreloc l', Storage t') } | None \ throw Err) g" lemma lexp_gas[rule_format]: "\l5' t5' g5'. lexp l5 ev5 cd5 st5 g5 = Normal ((l5', t5'), g5') \ g5' \ g5" proof (induct rule: lexp.induct[where ?P="\l5 ev5 cd5 st5 g5. (\l5' t5' g5'. lexp l5 ev5 cd5 st5 g5 = Normal ((l5', t5'), g5') \ g5' \ g5)"]) case (1 i e uv st g) then show ?case using lexp.simps(1) by (simp split: option.split Denvalue.split prod.split) next case (2 i r e cd st g) show ?case proof (rule allI[THEN allI, THEN allI, OF impI]) fix st5' xa xaa assume a1: "lexp (Ref i r) e cd st g = Normal ((st5', xa), xaa)" then show "xaa \ g" proof (cases "fmlookup (denvalue e) i") case None with a1 show ?thesis using lexp.simps(2) by simp next case (Some a) then show ?thesis proof (cases a) case (Pair tp b) then show ?thesis proof (cases b) case (Stackloc l) then show ?thesis proof (cases "accessStore l (stack st)") case None with a1 Some Pair Stackloc show ?thesis using lexp.psimps(2) by simp next case s2: (Some a) then show ?thesis proof (cases a) case (KValue x1) with a1 Some Pair Stackloc s2 show ?thesis using lexp.psimps(2) by simp next case (KCDptr x2) with a1 Some Pair Stackloc s2 show ?thesis using lexp.psimps(2) by simp next case (KMemptr l') then show ?thesis proof (cases tp) case (Value _) with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.simps(2) by simp next case (Calldata _) with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.simps(2) by simp next case (Memory t) then show ?thesis proof (cases "msel True t l' r e cd st g") case (n _ _) with 2 a1 Some Pair Stackloc s2 KMemptr Memory show ?thesis using msel_ssel_expr_load_rexp_gas(1) by (simp split: prod.split_asm) next case (e _) with a1 Some Pair Stackloc s2 KMemptr Memory show ?thesis using lexp.psimps(2) by simp qed next case (Storage _) with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.psimps(2) by simp qed next case (KStoptr l') then show ?thesis proof (cases tp) case (Value _) with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp next case (Calldata _) with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp next case (Memory _) with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp next case (Storage t) then show ?thesis proof (cases "ssel t l' r e cd st g") case (n _ _) with a1 Some Pair Stackloc s2 KStoptr Storage show ?thesis using msel_ssel_expr_load_rexp_gas(2) by (auto split: prod.split_asm) next case (e _) with a1 Some Pair Stackloc s2 KStoptr Storage show ?thesis using lexp.psimps(2) by simp qed qed qed qed next case (Storeloc l) then show ?thesis proof (cases tp) case (Value _) with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp next case (Calldata _) with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp next case (Memory _) with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp next case (Storage t) then show ?thesis proof (cases "ssel t l r e cd st g") case (n _ _) with a1 Some Pair Storeloc Storage show ?thesis using msel_ssel_expr_load_rexp_gas(2) by (auto split: prod.split_asm) next case (e _) with a1 Some Pair Storeloc Storage show ?thesis using lexp.psimps(2) by simp qed qed qed qed qed qed qed subsection \Semantics of statements\ text \The following is a helper function to connect the gas monad with the state monad.\ fun toState :: "(State \ ('a, 'e, Gas) state_monad) \ ('a, 'e, State) state_monad" where "toState gm = (\s. case gm s (gas s) of Normal (a,g) \ Normal(a,s\gas:=g\) | Exception e \ Exception e)" lemma wptoState[wprule]: assumes "\a g. gm s (gas s) = Normal (a, g) \ P a (s\gas:=g\)" and "\e. gm s (gas s) = Exception e \ E e" shows "wp (toState gm) P E s" using assms unfolding wp_def by (simp split:result.split result.split_asm) text \Now we define the semantics of statements.\ function (domintros) stmt :: "S \ Environment \ CalldataT \ (unit, Ex, State) state_monad" where "stmt SKIP e cd st = (do { assert Gas (\st. gas st > costs SKIP e cd st); modify (\st. st\gas := gas st - costs SKIP e cd st\) }) st" | "stmt (ASSIGN lv ex) env cd st = (do { assert Gas (\st. gas st > costs (ASSIGN lv ex) env cd st); modify (\st. st\gas := gas st - costs (ASSIGN lv ex) env cd st\); re \ toState (expr ex env cd); case re of (KValue v, Value t) \ do { rl \ toState (lexp lv env cd); case rl of (LStackloc l, Value t') \ do { v' \ option Err (\_. convert t t' v); modify (\st. st \stack := updateStore l (KValue v') (stack st)\) } | (LStoreloc l, Storage (STValue t')) \ do { v' \ option Err (\_. convert t t' v); modify (\st. st\storage := (storage st) (address env := fmupd l v' (storage st (address env)))\) } | (LMemloc l, Memory (MTValue t')) \ do { v' \ option Err (\_. convert t t' v); modify (\st. st\memory := updateStore l (MValue v') (memory st)\) } | _ \ throw Err } | (KCDptr p, Calldata (MTArray x t)) \ do { rl \ toState (lexp lv env cd); case rl of (LStackloc l, Memory _) \ do { sv \ applyf (\st. accessStore l (stack st)); p' \ case sv of Some (KMemptr p') \ return p' | _ \ throw Err; m \ option Err (\st. cpm2m p p' x t cd (memory st)); modify (\st. st\memory := m\) } | (LStackloc l, Storage _) \ do { sv \ applyf (\st. accessStore l (stack st)); p' \ case sv of Some (KStoptr p') \ return p' | _ \ throw Err; s \ option Err (\st. cpm2s p p' x t cd (storage st (address env))); modify (\st. st \storage := (storage st) (address env := s)\) } | (LStoreloc l, _) \ do { s \ option Err (\st. cpm2s p l x t cd (storage st (address env))); modify (\st. st \storage := (storage st) (address env := s)\) } | (LMemloc l, _) \ do { m \ option Err (\st. cpm2m p l x t cd (memory st)); modify (\st. st \memory := m\) } | _ \ throw Err } | (KMemptr p, Memory (MTArray x t)) \ do { rl \ toState (lexp lv env cd); case rl of (LStackloc l, Memory _) \ modify (\st. st\stack := updateStore l (KMemptr p) (stack st)\) | (LStackloc l, Storage _) \ do { sv \ applyf (\st. accessStore l (stack st)); p' \ case sv of Some (KStoptr p') \ return p' | _ \ throw Err; s \ option Err (\st. cpm2s p p' x t (memory st) (storage st (address env))); modify (\st. st \storage := (storage st) (address env := s)\) } | (LStoreloc l, _) \ do { s \ option Err (\st. cpm2s p l x t (memory st) (storage st (address env))); modify (\st. st \storage := (storage st) (address env := s)\) } | (LMemloc l, _) \ modify (\st. st \memory := updateStore l (MPointer p) (memory st)\) | _ \ throw Err } | (KStoptr p, Storage (STArray x t)) \ do { rl \ toState (lexp lv env cd); case rl of (LStackloc l, Memory _) \ do { sv \ applyf (\st. accessStore l (stack st)); p' \ case sv of Some (KMemptr p') \ return p' | _ \ throw Err; m \ option Err (\st. cps2m p p' x t (storage st (address env)) (memory st)); modify (\st. st\memory := m\) } | (LStackloc l, Storage _) \ modify (\st. st\stack := updateStore l (KStoptr p) (stack st)\) | (LStoreloc l, _) \ do { s \ option Err (\st. copy p l x t (storage st (address env))); modify (\st. st \storage := (storage st) (address env := s)\) } | (LMemloc l, _) \ do { m \ option Err (\st. cps2m p l x t (storage st (address env)) (memory st)); modify (\st. st\memory := m\) } | _ \ throw Err } | (KStoptr p, Storage (STMap t t')) \ do { rl \ toState (lexp lv env cd); l \ case rl of (LStackloc l, _) \ return l | _ \ throw Err; modify (\st. st\stack := updateStore l (KStoptr p) (stack st)\) } | _ \ throw Err }) st" | "stmt (COMP s1 s2) e cd st = (do { assert Gas (\st. gas st > costs (COMP s1 s2) e cd st); modify (\st. st\gas := gas st - costs (COMP s1 s2) e cd st\); stmt s1 e cd; stmt s2 e cd }) st" | "stmt (ITE ex s1 s2) e cd st = (do { assert Gas (\st. gas st > costs (ITE ex s1 s2) e cd st); modify (\st. st\gas := gas st - costs (ITE ex s1 s2) e cd st\); v \ toState (expr ex e cd); b \ (case v of (KValue b, Value TBool) \ return b | _ \ throw Err); if b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True then stmt s1 e cd else if b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False then stmt s2 e cd else throw Err }) st" | "stmt (WHILE ex s0) e cd st = (do { assert Gas (\st. gas st > costs (WHILE ex s0) e cd st); modify (\st. st\gas := gas st - costs (WHILE ex s0) e cd st\); v \ toState (expr ex e cd); b \ (case v of (KValue b, Value TBool) \ return b | _ \ throw Err); if b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True then do { stmt s0 e cd; stmt (WHILE ex s0) e cd } else if b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False then return () else throw Err }) st" | "stmt (INVOKE i xe) e cd st = (do { assert Gas (\st. gas st > costs (INVOKE i xe) e cd st); modify (\st. st\gas := gas st - costs (INVOKE i xe) e cd st\); (ct, _) \ option Err (\_. ep $$ contract e); (fp, f) \ case ct $$ i of Some (Method (fp, False, f)) \ return (fp, f) | _ \ throw Err; let e' = ffold_init ct (emptyEnv (address e) (contract e) (sender e) (svalue e)) (fmdom ct); m\<^sub>o \ applyf memory; (e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l) \ toState (load False fp xe e' emptyStore emptyStore m\<^sub>o e cd); k\<^sub>o \ applyf stack; modify (\st. st\stack:=k\<^sub>l, memory:=m\<^sub>l\); stmt f e\<^sub>l cd\<^sub>l; modify (\st. st\stack:=k\<^sub>o\) }) st" (*External Method calls allow to send some money val with it*) (*However this transfer does NOT trigger a fallback*) (*External methods can only be called from externally*) | "stmt (EXTERNAL ad i xe val) e cd st = (do { assert Gas (\st. gas st > costs (EXTERNAL ad i xe val) e cd st); modify (\st. st\gas := gas st - costs (EXTERNAL ad i xe val) e cd st\); kad \ toState (expr ad e cd); adv \ case kad of (KValue adv, Value TAddr) \ return adv | _ \ throw Err; assert Err (\_. adv \ address e); c \ (\st. case type (accounts st adv) of Some (Contract c) \ return c st | _ \ throw Err st); (ct, _, fb) \ option Err (\_. ep $$ c); kv \ toState (expr val e cd); (v, t) \ case kv of (KValue v, Value t) \ return (v, t) | _ \ throw Err; v' \ option Err (\_. convert t (TUInt 256) v); let e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct); case ct $$ i of Some (Method (fp, True, f)) \ do { (e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l) \ toState (load True fp xe e' emptyStore emptyStore emptyStore e cd); acc \ option Err (\st. transfer (address e) adv v' (accounts st)); (k\<^sub>o, m\<^sub>o) \ applyf (\st. (stack st, memory st)); modify (\st. st\accounts := acc, stack:=k\<^sub>l,memory:=m\<^sub>l\); stmt f e\<^sub>l cd\<^sub>l; modify (\st. st\stack:=k\<^sub>o, memory := m\<^sub>o\) } | None \ do { acc \ option Err (\st. transfer (address e) adv v' (accounts st)); (k\<^sub>o, m\<^sub>o) \ applyf (\st. (stack st, memory st)); modify (\st. st\accounts := acc,stack:=emptyStore, memory:=emptyStore\); stmt fb e' emptyStore; modify (\st. st\stack:=k\<^sub>o, memory := m\<^sub>o\) } | _ \ throw Err }) st" | "stmt (TRANSFER ad ex) e cd st = (do { assert Gas (\st. gas st > costs (TRANSFER ad ex) e cd st); modify (\st. st\gas := gas st - costs (TRANSFER ad ex) e cd st\); kv \ toState (expr ad e cd); adv \ case kv of (KValue adv, Value TAddr) \ return adv | _ \ throw Err; kv' \ toState (expr ex e cd); (v, t) \ case kv' of (KValue v, Value t) \ return (v, t) | _ \ throw Err; v' \ option Err (\_. convert t (TUInt 256) v); acc \ applyf accounts; case type (acc adv) of Some (Contract c) \ do { (ct, _, f) \ option Err (\_. ep $$ c); let e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct); (k\<^sub>o, m\<^sub>o) \ applyf (\st. (stack st, memory st)); acc' \ option Err (\st. transfer (address e) adv v' (accounts st)); modify (\st. st\accounts := acc', stack:=emptyStore, memory:=emptyStore\); stmt f e' emptyStore; modify (\st. st\stack:=k\<^sub>o, memory := m\<^sub>o\) } | Some EOA \ do { acc' \ option Err (\st. transfer (address e) adv v' (accounts st)); modify (\st. (st\accounts := acc'\)) } | None \ throw Err }) st" | "stmt (BLOCK ((id0, tp), None) s) e\<^sub>v cd st = (do { assert Gas (\st. gas st > costs (BLOCK ((id0, tp), None) s) e\<^sub>v cd st); modify (\st. st\gas := gas st - costs (BLOCK ((id0, tp), None) s) e\<^sub>v cd st\); (cd', mem', sck', e') \ option Err (\st. decl id0 tp None False cd (memory st) (storage st) (cd, memory st, stack st, e\<^sub>v)); modify (\st. st\stack := sck', memory := mem'\); stmt s e' cd' }) st" | "stmt (BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st = (do { assert Gas (\st. gas st > costs(BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st); modify (\st. st\gas := gas st - costs (BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st\); (v, t) \ toState (expr ex' e\<^sub>v cd); (cd', mem', sck', e') \ option Err (\st. decl id0 tp (Some (v, t)) False cd (memory st) (storage st) (cd, memory st, stack st, e\<^sub>v)); modify (\st. st\stack := sck', memory := mem'\); stmt s e' cd' }) st" (* Note: We cannot use (ct, (fp, cn), fb) <- option Err (\_. ep $$ i) *) | "stmt (NEW i xe val) e cd st = (do { assert Gas (\st. gas st > costs (NEW i xe val) e cd st); modify (\st. st\gas := gas st - costs (NEW i xe val) e cd st\); adv \ applyf (\st. hash (address e) (ShowL\<^sub>n\<^sub>a\<^sub>t (contracts (accounts st (address e))))); assert Err (\st. type (accounts st adv) = None); kv \ toState (expr val e cd); (v, t) \ case kv of (KValue v, Value t) \ return (v, t) | _ \ throw Err; (ct, cn, _) \ option Err (\_. ep $$ i); let e' = ffold_init ct (emptyEnv adv i (address e) v) (fmdom ct); (e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l) \ toState (load True (fst cn) xe e' emptyStore emptyStore emptyStore e cd); modify (\st. st\accounts := (accounts st)(adv := \bal = ShowL\<^sub>i\<^sub>n\<^sub>t 0, type = Some (Contract i), contracts = 0\), storage:=(storage st)(adv := {$$})\); acc \ option Err (\st. transfer (address e) adv v (accounts st)); (k\<^sub>o, m\<^sub>o) \ applyf (\st. (stack st, memory st)); modify (\st. st\accounts := acc, stack:=k\<^sub>l, memory:=m\<^sub>l\); stmt (snd cn) e\<^sub>l cd\<^sub>l; modify (\st. st\stack:=k\<^sub>o, memory := m\<^sub>o\); modify (incrementAccountContracts (address e)) }) st" by pat_completeness auto subsection \Termination\ text \Again, to prove termination we need a lemma regarding gas consumption.\ lemma stmt_dom_gas[rule_format]: "stmt_dom (s6, ev6, cd6, st6) \ (\st6'. stmt s6 ev6 cd6 st6 = Normal((), st6') \ gas st6' \ gas st6)" proof (induct rule: stmt.pinduct[where ?P="\s6 ev6 cd6 st6. (\st6'. stmt s6 ev6 cd6 st6 = Normal ((), st6') \ gas st6' \ gas st6)"]) case (1 e cd st) then show ?case using stmt.psimps(1) by simp next case (2 lv ex env cd st) define g where "g = costs (ASSIGN lv ex) env cd st" show ?case proof (rule allI[OF impI]) fix st6' assume stmt_def: "stmt (ASSIGN lv ex) env cd st = Normal ((), st6')" then show "gas st6' \ gas st" proof cases assume "gas st \ g" with 2(1) stmt_def show ?thesis using stmt.psimps(2) g_def by simp next assume "\ gas st \ g" define st' where "st' = st\gas := gas st - g\" show ?thesis proof (cases "expr ex env cd st' (gas st - g)") case (n a g') define st'' where "st'' = st'\gas := g'\" then show ?thesis proof (cases a) case (Pair b c) then show ?thesis proof (cases b) case (KValue v) then show ?thesis proof (cases c) case (Value t) then show ?thesis proof (cases "lexp lv env cd st'' g'") case n2: (n a g'') then show ?thesis proof (cases a) case p1: (Pair a b) then show ?thesis proof (cases a) case (LStackloc l) then show ?thesis proof (cases b) case v2: (Value t') then show ?thesis proof (cases "convert t t' v ") case None with stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStackloc v2 show ?thesis using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def by simp next case s3: (Some v') with 2(1) `\ gas st \ g` n Pair KValue Value n2 p1 LStackloc v2 s3 have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''\gas := g'', stack := updateStore l (KValue v') (stack st)\)" using stmt.psimps(2) g_def st'_def st''_def by simp with stmt_def have "st6'= st''\gas := g'', stack := updateStore l (KValue v') (stack st)\" by simp moreover from lexp_gas `\ gas st \ g` n2 p1 have "gas (st''\gas := g'', stack := updateStore l (KValue v') (stack st)\) \ gas (st'\gas := g'\)" using g_def st'_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair KValue Value have "gas (st'\gas := g'\) \ gas (st\gas := gas st - g\)" using g_def by simp ultimately show ?thesis by simp qed next case (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Memory x3) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Storage x4) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (LMemloc l) then show ?thesis proof (cases b) case v2: (Value t') with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Memory x3) then show ?thesis proof (cases x3) case (MTArray x11 x12) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LMemloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (MTValue t') then show ?thesis proof (cases "convert t t' v ") case None with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LMemloc Memory MTValue show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case s3: (Some v') with 2(1) `\ gas st \ g` n Pair KValue Value n2 p1 LMemloc Memory MTValue s3 have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''\gas := g'', memory := updateStore l (MValue v') (memory st'')\)" using stmt.psimps(2) g_def st'_def st''_def by simp with stmt_def have "st6'= (st''\gas := g'', memory := updateStore l (MValue v') (memory st'')\)" by simp moreover from lexp_gas `\ gas st \ g` n2 p1 have "gas (st''\gas := g'', stack := updateStore l (KValue v') (stack st)\) \ gas (st'\gas := g'\)" using g_def st'_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair KValue Value n2 p1 have "gas (st'\gas := g'\) \ gas (st\gas := gas st - g\)" using g_def by simp ultimately show ?thesis by simp qed qed next case (Storage x4) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (LStoreloc l) then show ?thesis proof (cases b) case v2: (Value t') with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Memory x3) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Storage x4) then show ?thesis proof (cases x4) case (STArray x11 x12) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStoreloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (STMap x21 x22) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStoreloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (STValue t') then show ?thesis proof (cases "convert t t' v ") case None with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value n2 p1 LStoreloc Storage STValue show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case s3: (Some v') with 2(1) `\ gas st \ g` n Pair KValue Value n2 p1 LStoreloc Storage STValue s3 have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'' \gas := g'', storage := (storage st'') (address env := fmupd l v' (storage st'' (address env)))\)" using stmt.psimps(2) g_def st'_def st''_def by simp with stmt_def have "st6'= st'' \gas := g'', storage := (storage st'') (address env := fmupd l v' (storage st'' (address env)))\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KValue Value n2 p1 have "gas (st''\gas := g'', stack := updateStore l (KValue v') (stack st)\) \ gas (st'\gas := g'\)" using g_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair KValue Value n2 p1 have "gas (st'\gas := g'\) \ gas (st\gas := gas st - g\)" using g_def by simp ultimately show ?thesis by simp qed qed qed qed qed next case (e x) with 2(1) stmt_def `\ gas st \ g` n Pair KValue Value show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp next case (Memory x3) with 2(1) stmt_def `\ gas st \ g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp next case (Storage x4) with 2(1) stmt_def `\ gas st \ g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp qed next case (KCDptr p) then show ?thesis proof (cases c) case (Value x1) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def by simp next case (Calldata x2) then show ?thesis proof (cases x2) case (MTArray x t) then show ?thesis proof (cases "lexp lv env cd st'' g'") case n2: (n a g'') define st''' where "st''' = st''\gas := g''\" then show ?thesis proof (cases a) case p2: (Pair a b) then show ?thesis proof (cases a) case (LStackloc l) then show ?thesis proof (cases b) case v2: (Value t') with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case c2: (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Memory x3) then show ?thesis proof (cases "accessStore l (stack st''')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case s3: (Some a) then show ?thesis proof (cases a) case (KValue x1) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case c3: (KCDptr x2) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (KMemptr p') then show ?thesis proof (cases "cpm2m p p' x t cd (memory st''')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by (simp split:if_split_asm) next case (Some m') with `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 KMemptr have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' \memory := m'\)" using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st''' \memory := m'\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas (st'''\memory := m'\) \ gas st''" using st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed next case (KStoptr p') with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp qed qed next case (Storage x4) then show ?thesis proof (cases "accessStore l (stack st'')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case s3: (Some a) then show ?thesis proof (cases a) case (KValue x1) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case c3: (KCDptr x2) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (KMemptr x3) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (KStoptr p') then show ?thesis proof (cases "cpm2s p p' x t cd (storage st'' (address env))") case None with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (Some s') with 2(1) `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 KStoptr have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' \storage := (storage st'') (address env := s')\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st''' \storage := (storage st'') (address env := s')\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st''' \ gas st''" using g_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using g_def st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed qed qed qed next case (LMemloc l) then show ?thesis proof (cases "cpm2m p l x t cd (memory st''')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by (simp split:if_split_asm) next case (Some m) with `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LMemloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\memory := m\)" using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= (st'''\memory := m\)" by simp moreover from lexp_gas `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st''' \ gas st''" using st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed next case (LStoreloc l) then show ?thesis proof (cases "cpm2s p l x t cd (storage st'' (address env))") case None with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (Some s) with `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 LStoreloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' \storage := (storage st'') (address env := s)\)" using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= (st'''\storage := (storage st'') (address env := s)\)" by simp moreover from lexp_gas `\ gas st \ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st''' \ gas st''" using st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed qed qed next case (e x) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata MTArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (MTValue x2) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr Calldata show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (Memory x3) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Storage x4) with 2(1) stmt_def `\ gas st \ g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (KMemptr p) then show ?thesis proof (cases c) case (Value x1) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Memory x3) then show ?thesis proof (cases x3) case (MTArray x t) then show ?thesis proof (cases "lexp lv env cd st'' g'") case n2: (n a g'') define st''' where "st''' = st''\gas := g''\" then show ?thesis proof (cases a) case p2: (Pair a b) then show ?thesis proof (cases a) case (LStackloc l) then show ?thesis proof (cases b) case v2: (Value t') with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case c2: (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case m2: (Memory x3) with 2(1) `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\stack := updateStore l (KMemptr p) (stack st'')\)" using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\stack := updateStore l (KMemptr p) (stack st'')\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' \ gas st''" using st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp next case (Storage x4) then show ?thesis proof (cases "accessStore l (stack st''')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case s3: (Some a) then show ?thesis proof (cases a) case (KValue x1) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case c3: (KCDptr x2) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case m3: (KMemptr x3) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (KStoptr p') then show ?thesis proof (cases "cpm2s p p' x t (memory st''') (storage st''' (address env))") case None with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (Some s) with 2(1) `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 KStoptr have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\storage := (storage st''') (address env := s)\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\storage := (storage st''') (address env := s)\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed qed qed qed next case (LMemloc l) with 2(1) `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LMemloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\memory := updateStore l (MPointer p) (memory st''')\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\memory := updateStore l (MPointer p) (memory st''')\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp next case (LStoreloc l) then show ?thesis proof (cases "cpm2s p l x t (memory st''') (storage st'' (address env))") case None with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def using st'_def st''_def st'''_def by simp next case (Some s) with 2(1) `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 LStoreloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\storage := (storage st''') (address env := s)\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\storage := (storage st''') (address env := s)\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed qed qed next case (e _) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory MTArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (MTValue _) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (Storage x4) with 2(1) stmt_def `\ gas st \ g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (KStoptr p) then show ?thesis proof (cases c) case (Value x1) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Memory x3) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Storage x4) then show ?thesis proof (cases x4) case (STArray x t) then show ?thesis proof (cases "lexp lv env cd st'' g'") case n2: (n a g'') define st''' where "st''' = st''\gas := g''\" then show ?thesis proof (cases a) case p2: (Pair a b) then show ?thesis proof (cases a) case (LStackloc l) then show ?thesis proof (cases b) case v2: (Value t') with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case c2: (Calldata x2) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (Memory x3) then show ?thesis proof (cases "accessStore l (stack st''')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case s3: (Some a) then show ?thesis proof (cases a) case (KValue x1) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case c3: (KCDptr x2) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (KMemptr p') then show ?thesis proof (cases "cps2m p p' x t (storage st''' (address env)) (memory st''')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (Some m) with 2(1) `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 KMemptr have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\memory := m\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\memory := m\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KMemptr Storage STArray n2 p2 have "gas (st'''\memory := m\) \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed next case sp2: (KStoptr p') with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp qed qed next case st2: (Storage x4) with 2(1) `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStackloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\stack := updateStore l (KStoptr p) (stack st''')\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\stack := updateStore l (KStoptr p) (stack st''')\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''\stack := updateStore l (KStoptr p) (stack st''')\) \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed next case (LMemloc l) then show ?thesis proof (cases "cps2m p l x t (storage st'' (address env)) (memory st'')") case None with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (Some m) with 2(1) `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LMemloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\memory := m\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= (st'''\memory := m\)" by simp moreover from lexp_gas `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''\memory := m\) \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed next case (LStoreloc l) then show ?thesis proof (cases "copy p l x t (storage st'' (address env))") case None with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp next case (Some s) with 2(1) `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 LStoreloc have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''\storage := (storage st''') (address env := s)\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\storage := (storage st''') (address env := s)\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''\storage := (storage st''') (address env := s')\) \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp qed qed qed next case (e x) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (STMap t t') then show ?thesis proof (cases "lexp lv env cd st'' g'") case n2: (n a g'') define st''' where "st''' = st''\gas := g''\" then show ?thesis proof (cases a) case p2: (Pair a b) then show ?thesis proof (cases a) case (LStackloc l) with 2(1) `\ gas st \ g` n Pair KStoptr Storage STMap n2 p2 have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' \stack := updateStore l (KStoptr p) (stack st''')\)" using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp with stmt_def have "st6'= st'''\stack := updateStore l (KStoptr p) (stack st''')\" by simp moreover from lexp_gas `\ gas st \ g` n Pair KStoptr Storage STMap n2 p2 have "gas (st'''\stack := updateStore l (KStoptr p) (stack st''')\) \ gas st''" using g_def st'_def st''_def st'''_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `\ gas st \ g` n Pair have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp next case (LMemloc x2) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STMap n2 p2 show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp next case (LStoreloc x3) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STMap n2 p2 show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed qed next case (e x) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage STMap show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed next case (STValue x3) with 2(1) stmt_def `\ gas st \ g` n Pair KStoptr Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp qed qed qed qed next case (e x) with 2(1) stmt_def `\ gas st \ g` show ?thesis using stmt.psimps(2) g_def st'_def by simp qed qed qed next case (3 s1 s2 e cd st) define g where "g = costs (COMP s1 s2) e cd st" show ?case proof (rule allI[OF impI]) fix st6' assume stmt_def: "stmt (COMP s1 s2) e cd st = Normal ((), st6')" then show "gas st6' \ gas st" proof cases assume "gas st \ g" with 3(1) stmt_def g_def show ?thesis using stmt.psimps(3) by simp next assume "\ gas st \ g" show ?thesis proof (cases "stmt s1 e cd (st\gas := gas st - g\)") case (n a st') with 3(1) stmt_def `\ gas st \ g` have "stmt (COMP s1 s2) e cd st = stmt s2 e cd st'" using stmt.psimps(3)[of s1 s2 e cd st] g_def by (simp add:Let_def split:unit.split_asm) with 3(3) stmt_def \\ gas st \ g\ n have "gas st6' \ gas st'" using g_def by simp moreover from 3(2)[where ?s'a="st\gas := gas st - g\"] \\ gas st \ g\ n have "gas st' \ gas st" using g_def by simp ultimately show ?thesis by simp next case (e x) with 3 stmt_def `\ gas st \ g` show ?thesis using stmt.psimps(3)[of s1 s2 e cd st] g_def by (simp split: Ex.split_asm) qed qed qed next case (4 ex s1 s2 e cd st) define g where "g = costs (ITE ex s1 s2) e cd st" show ?case proof (rule allI[OF impI]) fix st6' assume stmt_def: "stmt (ITE ex s1 s2) e cd st = Normal ((), st6')" then show "gas st6' \ gas st" proof cases assume "gas st \ g" with 4(1) stmt_def show ?thesis using stmt.psimps(4) g_def by simp next assume "\ gas st \ g" then have l1: "assert Gas (\st. costs (ITE ex s1 s2) e cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: " modify (\st. st\gas := gas st - costs (ITE ex s1 s2) e cd st\) st = Normal ((), st')" using g_def by simp show ?thesis proof (cases "expr ex e cd st' (gas st - g)") case (n a g') define st'' where "st'' = st'\gas := g'\" with n have l3: "toState (expr ex e cd) st' = Normal (a, st'')" using st'_def by simp then show ?thesis proof (cases a) case (Pair b c) then show ?thesis proof (cases b) case (KValue b) then show ?thesis proof (cases c) case (Value x1) then show ?thesis proof (cases x1) case (TSInt x1) with 4(1) stmt_def `\ gas st \ g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def by simp next case (TUInt x2) with 4(1) stmt_def `\ gas st \ g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def by simp next case TBool then show ?thesis proof cases assume "b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True" with 4(1) `\ gas st \ g` n Pair KValue Value TBool have "stmt (ITE ex s1 s2) e cd st = stmt s1 e cd st''" using stmt.psimps(4) g_def st'_def st''_def by simp with 4(2)[OF l1 l2 l3] stmt_def `\ gas st \ g` n Pair KValue Value TBool `b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True` have "gas st6' \ gas st''" using g_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `\ gas st \ g` n Pair KValue Value TBool have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp next assume nt: "\ b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True" show ?thesis proof cases assume "b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False" with 4(1) `\ gas st \ g` n Pair KValue Value TBool nt have "stmt (ITE ex s1 s2) e cd st = stmt s2 e cd st''" using stmt.psimps(4) g_def st'_def st''_def by simp with 4(3)[OF l1 l2 l3] stmt_def `\ gas st \ g` n Pair KValue Value TBool nt `b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False` have "gas st6' \ gas st''" using g_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `\ gas st \ g` n Pair KValue Value TBool have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp next assume "\ b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False" with 4(1) stmt_def `\ gas st \ g` n Pair KValue Value TBool nt show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp qed qed next case TAddr with 4(1) stmt_def `\ gas st \ g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp qed next case (Calldata x2) with 4(1) stmt_def `\ gas st \ g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp next case (Memory x3) with 4(1) stmt_def `\ gas st \ g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp next case (Storage x4) with 4(1) stmt_def `\ gas st \ g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp qed next case (KCDptr x2) with 4(1) stmt_def `\ gas st \ g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp next case (KMemptr x3) with 4(1) stmt_def `\ gas st \ g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp next case (KStoptr x4) with 4(1) stmt_def `\ gas st \ g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp qed qed next case (e e) with 4(1) stmt_def `\ gas st \ g` show ?thesis using stmt.psimps(4) g_def st'_def by simp qed qed qed next case (5 ex s0 e cd st) define g where "g = costs (WHILE ex s0) e cd st" show ?case proof (rule allI[OF impI]) fix st6' assume stmt_def: "stmt (WHILE ex s0) e cd st = Normal ((), st6')" then show "gas st6' \ gas st" proof cases assume "gas st \ g" with 5(1) stmt_def show ?thesis using stmt.psimps(5) g_def by simp next assume gcost: "\ gas st \ g" then have l1: "assert Gas (\st. costs (WHILE ex s0) e cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: " modify (\st. st\gas := gas st - costs (WHILE ex s0) e cd st\) st = Normal ((), st')" using g_def by simp show ?thesis proof (cases "expr ex e cd st' (gas st - g)") case (n a g') define st'' where "st'' = st'\gas := g'\" with n have l3: "toState (expr ex e cd) st' = Normal (a, st'')" using st'_def by simp then show ?thesis proof (cases a) case (Pair b c) then show ?thesis proof (cases b) case (KValue b) then show ?thesis proof (cases c) case (Value x1) then show ?thesis proof (cases x1) case (TSInt x1) with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def by simp next case (TUInt x2) with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def by simp next case TBool then show ?thesis proof cases assume "b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True" then show ?thesis proof (cases "stmt s0 e cd st''") case n2: (n a st''') with 5(1) gcost n Pair KValue Value TBool `b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True` have "stmt (WHILE ex s0) e cd st = stmt (WHILE ex s0) e cd st'''" using stmt.psimps(5)[of ex s0 e cd st] g_def st'_def st''_def by (simp add: Let_def split:unit.split_asm) with 5(3) stmt_def gcost n2 Pair KValue Value TBool `b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True` n have "gas st6' \ gas st'''" using g_def st'_def st''_def by simp moreover from 5(2)[OF l1 l2 l3] gcost n2 Pair KValue Value TBool `b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True` n have "gas st''' \ gas st''" using g_def by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `\ gas st \ g` n Pair KValue Value TBool have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using st'_def by simp next case (e x) with 5(1) stmt_def gcost n Pair KValue Value TBool `b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True` show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp qed next assume nt: "\ b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True" show ?thesis proof cases assume "b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False" with 5(1) gcost n Pair KValue Value TBool nt have "stmt (WHILE ex s0) e cd st = return () st''" using stmt.psimps(5) g_def st'_def st''_def by simp with stmt_def have "gas st6' \ gas st''" by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `\ gas st \ g` n Pair KValue Value TBool have "gas st'' \ gas st'" using st'_def st''_def by simp ultimately show ?thesis using g_def st'_def st''_def by simp next assume "\ b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False" with 5(1) stmt_def gcost n Pair KValue Value TBool nt show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp qed qed next case TAddr with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp qed next case (Calldata x2) with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp next case (Memory x3) with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp next case (Storage x4) with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp qed next case (KCDptr x2) with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp next case (KMemptr x3) with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp next case (KStoptr x4) with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp qed qed next case (e e) with 5(1) stmt_def gcost show ?thesis using stmt.psimps(5) g_def st'_def by simp qed qed qed next case (6 i xe e cd st) define g where "g = costs (INVOKE i xe) e cd st" show ?case proof (rule allI[OF impI]) fix st6' assume a1: "stmt (INVOKE i xe) e cd st = Normal ((), st6')" show "gas st6' \ gas st" proof (cases) assume "gas st \ g" with 6(1) a1 show ?thesis using stmt.psimps(6) g_def by simp next assume gcost: "\ gas st \ g" then have l1: "assert Gas (\st. costs (INVOKE i xe) e cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: "modify (\st. st\gas := gas st - costs (INVOKE i xe) e cd st\) st = Normal ((), st')" using g_def by simp then show ?thesis proof (cases "ep $$ contract e") case None with 6(1) a1 gcost show ?thesis using stmt.psimps(6) g_def by simp next case (Some x) then have l3: "option Err (\_. ep $$ contract e) st' = Normal (x, st')" by simp then show ?thesis proof (cases x) case (fields ct _ _) then show ?thesis proof (cases "fmlookup ct i") case None with 6(1) g_def a1 gcost Some fields show ?thesis using stmt.psimps(6) by simp next case s1: (Some a) then show ?thesis proof (cases a) case (Method x1) then show ?thesis proof (cases x1) case p1: (fields fp ext f) then show ?thesis proof (cases ext) case True with 6(1) a1 g_def gcost Some fields s1 Method p1 show ?thesis using stmt.psimps(6) st'_def by auto next case False then have l4: "(case ct $$ i of None \ throw Err | Some (Method (fp, True, f)) \ throw Err | Some (Method (fp, False, f)) \ return (fp, f) | Some _ \ throw Err) st' = Normal ((fp,f),st')" using s1 Method p1 by simp define m\<^sub>o e' where "m\<^sub>o = memory st'" and "e' = ffold (init ct) (emptyEnv (address e) (contract e) (sender e) (svalue e)) (fmdom ct)" then show ?thesis proof (cases "load False fp xe e' emptyStore emptyStore m\<^sub>o e cd st' (gas st - g)") case s4: (n a g') define st'' where "st'' = st'\gas := g'\" then show ?thesis proof (cases a) case f2: (fields e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l) then have l5: "toState (load False fp xe e' emptyStore emptyStore m\<^sub>o e cd) st' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), st'')" using st'_def st''_def s4 by simp define k\<^sub>o where "k\<^sub>o = stack st'" then show ?thesis proof (cases "stmt f e\<^sub>l cd\<^sub>l (st''\stack:=k\<^sub>l, memory:=m\<^sub>l\)") case n2: (n a st''') with a1 g_def gcost Some fields s1 Method p1 m\<^sub>o_def e'_def s4 f2 k\<^sub>o_def False have "stmt (INVOKE i xe) e cd st = Normal ((), st'''\stack:=k\<^sub>o\)" using stmt.psimps(6)[OF 6(1)] st'_def st''_def by auto with a1 have "gas st6' \ gas st'''" by auto also from 6(2)[OF l1 l2 l3 fields l4 _ _ _ l5, where ?s'g="st''\stack := k\<^sub>l, memory := m\<^sub>l\"] n2 m\<^sub>o_def e'_def have "\ \ gas st''" by auto also from msel_ssel_expr_load_rexp_gas(4)[of False fp xe e' emptyStore emptyStore m\<^sub>o e cd st' "(gas st - g)"] have "\ \ gas st'" using s4 st'_def st''_def f2 by auto finally show ?thesis using st'_def by simp next case (e x) with 6(1) a1 g_def gcost Some fields s1 Method p1 m\<^sub>o_def e'_def s4 f2 show ?thesis using stmt.psimps(6) st'_def st''_def False by auto qed qed next case (e x) with 6(1) a1 g_def gcost Some fields s1 Method p1 m\<^sub>o_def e'_def show ?thesis using stmt.psimps(6) st'_def False by auto qed qed qed next case (Function _) with 6(1) g_def a1 gcost Some fields s1 show ?thesis using stmt.psimps(6) by simp next case (Var _) with 6(1) g_def a1 gcost Some fields s1 show ?thesis using stmt.psimps(6) by simp qed qed qed qed qed qed next case (7 ad i xe val e cd st) define g where "g = costs (EXTERNAL ad i xe val) e cd st" show ?case proof (rule allI[OF impI]) fix st6' assume a1: "stmt (EXTERNAL ad i xe val) e cd st = Normal ((), st6')" show "gas st6' \ gas st" proof (cases) assume "gas st \ g" with 7(1) a1 show ?thesis using stmt.psimps(7) g_def by simp next assume gcost: "\ gas st \ g" then have l1: "assert Gas (\st. costs (EXTERNAL ad i xe val) e cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: " modify (\st. st\gas := gas st - costs (EXTERNAL ad i xe val) e cd st\) st = Normal ((), st')" using g_def by simp then show ?thesis proof (cases "expr ad e cd st' (gas st - g)") case (n a0 g') define st'' where "st'' = st'\gas := g'\" with n have l3: "toState (expr ad e cd) st' = Normal (a0, st'')" using st'_def by simp then show ?thesis proof (cases a0) case (Pair b c) then show ?thesis proof (cases b) case (KValue adv) then show ?thesis proof (cases c) case (Value x1) then show ?thesis proof (cases x1) case (TSInt x1) with 7(1) g_def a1 gcost n Pair KValue Value show ?thesis using stmt.psimps(7) st'_def by auto next case (TUInt x2) with 7(1) g_def a1 gcost n Pair KValue Value show ?thesis using stmt.psimps(7) st'_def by auto next case TBool with 7(1) g_def a1 gcost n Pair KValue Value show ?thesis using stmt.psimps(7) st'_def by auto next case TAddr then have l4: "(case a0 of (KValue adv, Value TAddr) \ return adv | (KValue adv, Value _) \ throw Err | (KValue adv, _) \ throw Err | (_, b) \ throw Err) st'' = Normal (adv, st'')" using Pair KValue Value by simp then show ?thesis proof (cases "adv = address e") case True with 7(1) g_def a1 gcost n Pair KValue Value TAddr show ?thesis using stmt.psimps(7) st'_def by auto next case False then have l5: "assert Err (\_. adv \ address e) st'' = Normal ((), st'')" by simp then show ?thesis proof (cases "type (accounts st'' adv)") case None with 7(1) g_def a1 gcost n Pair KValue Value TAddr False show ?thesis using stmt.psimps(7) st'_def st''_def by auto next case (Some x2) then show ?thesis proof (cases x2) case EOA with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some show ?thesis using stmt.psimps(7) st'_def st''_def by auto next case (Contract c) then have l6: "(\st. case type (accounts st adv) of Some (Contract c) \ return c st | _ \ throw Err st) st'' = Normal (c, st'')" using Some by (simp split:atype.split option.split) then show ?thesis proof (cases "ep $$ c") case None with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Contract Some show ?thesis using stmt.psimps(7) st'_def st''_def by auto next case s2: (Some x) then show ?thesis proof (cases x) case p2: (fields ct x0 fb) then have l7: "option Err (\_. ep $$ c) st'' = Normal ((ct, x0, fb), st'')" using s2 by simp then show ?thesis proof (cases "expr val e cd st'' (gas st'')") case n1: (n kv g'') define st''' where "st''' = st''\gas := g''\" with n1 have l8: "toState (expr val e cd) st'' = Normal (kv, st''')" by simp then show ?thesis proof (cases kv) case p3: (Pair a b) then show ?thesis proof (cases a) case k2: (KValue v) then show ?thesis proof (cases b) case v: (Value t) then have l9: "(case kv of (KValue v, Value t) \ return (v, t) | (KValue v, _) \ throw Err | (_, b) \ throw Err) st''' = Normal ((v,t), st''')" using n1 p3 k2 by simp show ?thesis proof (cases "convert t (TUInt 256) v") case None with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Contract Some s2 p2 None n1 p3 k2 v False show ?thesis using stmt.psimps(7)[OF 7(1)] st'_def st''_def st'''_def by simp next case s3: (Some v') define e' where "e' = ffold (init ct) (emptyEnv adv c (address e) v') (fmdom ct)" show ?thesis proof (cases "fmlookup ct i") case None show ?thesis proof (cases "transfer (address e) adv v' (accounts st''')") case n2: None with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Contract Some s2 p2 None n1 p3 k2 v False s3 show ?thesis using stmt.psimps(7)[OF 7(1)] st'_def st''_def st'''_def by simp next case s4: (Some acc) then have l10: "option Err (\st. transfer (address e) adv v' (accounts st)) st''' = Normal (acc, st''')" by simp define k\<^sub>o m\<^sub>o where "k\<^sub>o = stack st'''" and "m\<^sub>o = memory st'''" show ?thesis proof (cases "stmt fb e' emptyStore (st'''\accounts := acc, stack:=emptyStore, memory:=emptyStore\)") case n2: (n a st'''') with g_def a1 gcost n Pair KValue Value TAddr False Contract Some s2 p2 None n1 p3 k2 v s4 have "stmt (EXTERNAL ad i xe val) e cd st = Normal ((), st''''\stack:=stack st''', memory := memory st'''\)" using stmt.psimps(7)[OF 7(1)] st'_def st''_def st'''_def e'_def False s3 by simp with a1 have "gas st6' \ gas st''''" by auto also from 7(3)[OF l1 l2 l3 l4 l5 l6 l7 _ _ l8 l9 _ _ _ None l10, where ?s'k="st'''" and ?s'l="st'''\accounts := acc,stack:=emptyStore, memory:=emptyStore\" and ?x=e', of "(x0,fb)" x0 fb] n2 have "\ \ gas (st'''\accounts := acc,stack:=emptyStore, memory:=emptyStore\)" using e'_def s3 by simp also from msel_ssel_expr_load_rexp_gas(3)[of val e cd st'' "gas st''"] have "\ \ gas st''" using n1 st'_def st''_def st'''_def p3 by simp also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"] have "\ \ gas st'" using n st'_def st''_def st'''_def p3 by fastforce finally show ?thesis using st'_def by simp next case (e x) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 None n1 p3 k2 v s4 s3 show ?thesis using stmt.psimps(7)[of ad i xe val e cd st] st'_def st''_def st'''_def e'_def by simp qed qed next case s1: (Some a) then show ?thesis proof (cases a) case (Method x1) then show ?thesis proof (cases x1) case p4: (fields fp ext f) then show ?thesis proof (cases ext) case True then show ?thesis proof (cases "load True fp xe e' emptyStore emptyStore emptyStore e cd st''' (gas st''')") case s4: (n a g''') define st'''' where "st'''' = st'''\gas := g'''\" then show ?thesis proof (cases a) case f1: (fields e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l) then have l10: "toState (load True fp xe e' emptyStore emptyStore emptyStore e cd) st''' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), st'''')" using s4 st''''_def by simp show ?thesis proof (cases "transfer (address e) adv v' (accounts st'''')") case n2: None with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v s3 f1 e'_def True s4 show ?thesis using stmt.psimps(7)[of ad i xe val e cd st] st'_def st''_def st'''_def st''''_def by simp next case s5: (Some acc) then have l11: "option Err (\st. transfer (address e) adv v' (accounts st)) st'''' = Normal (acc, st'''')" by simp define k\<^sub>o where "k\<^sub>o = accounts st''''" define m\<^sub>o where "m\<^sub>o = accounts st''''" show ?thesis proof (cases "stmt f e\<^sub>l cd\<^sub>l (st''''\accounts := acc, stack:=k\<^sub>l,memory:=m\<^sub>l\)") case n2: (n a st''''') with 7(1) g_def a1 gcost n Pair KValue Value TAddr Some s2 Contract p2 s1 Method p4 n1 p3 k2 v k\<^sub>o_def m\<^sub>o_def e'_def s3 f1 s4 s5 have "stmt (EXTERNAL ad i xe val) e cd st = Normal ((), st'''''\stack:=stack st'''', memory := memory st''''\)" using stmt.psimps(7)[of ad i xe val e cd st] st'_def st''_def st'''_def st''''_def True False by simp with a1 have "gas st6' \ gas st'''''" by auto also from 7(2)[OF l1 l2 l3 l4 l5 l6 l7 _ _ l8 l9 _ _ _ s1 Method _ _ _ l10 _ _ _ l11, where ?s'm="st''''\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\" and ?s'l=st''''] p4 n2 e'_def True s3 have "\ \ gas (st''''\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\)" by simp also from msel_ssel_expr_load_rexp_gas(4)[of True fp xe e' emptyStore emptyStore emptyStore e cd st''' "gas st'''"] have "\ \ gas st'''" using s3 st'_def st''_def st'''_def st''''_def f1 s4 by simp also from msel_ssel_expr_load_rexp_gas(3)[of val e cd st'' "gas st''"] have "\ \ gas st''" using n1 st'_def st''_def st'''_def by fastforce also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"] have "\ \ gas st'" using n st'_def st''_def st'''_def by fastforce finally show ?thesis using st'_def by simp next case (e x) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v k\<^sub>o_def m\<^sub>o_def e'_def s3 f1 s4 s5 True show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def st''''_def by simp qed qed qed next case (e x) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v e'_def True s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp qed next case f: False with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp qed qed next case (Function _) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 n1 p3 k2 v s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp next case (Var _) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 n1 p3 k2 v s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp qed qed qed next case (Calldata x2) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 k2 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp next case (Memory x3) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 k2 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp next case (Storage x4) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 k2 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp qed next case (KCDptr x2) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp next case (KMemptr x3) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp next case (KStoptr x4) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp qed qed next case n2: (e x) with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 show ?thesis using stmt.psimps(7) st'_def st''_def by simp qed qed qed qed qed qed qed next case (Calldata x2) with 7(1) g_def a1 gcost n Pair KValue show ?thesis using stmt.psimps(7) st'_def st''_def by simp next case (Memory x3) with 7(1) g_def a1 gcost n Pair KValue show ?thesis using stmt.psimps(7) st'_def st''_def by simp next case (Storage x4) with 7(1) g_def a1 gcost n Pair KValue show ?thesis using stmt.psimps(7) st'_def st''_def by simp qed next case (KCDptr x2) with 7(1) g_def a1 gcost n Pair show ?thesis using stmt.psimps(7) st'_def st''_def by simp next case (KMemptr x3) with 7(1) g_def a1 gcost n Pair show ?thesis using stmt.psimps(7) st'_def st''_def by simp next case (KStoptr x4) with 7(1) g_def a1 gcost n Pair show ?thesis using stmt.psimps(7) st'_def st''_def by simp qed qed next case (e _) with 7(1) g_def a1 gcost show ?thesis using stmt.psimps(7) st'_def by simp qed qed qed next case (8 ad ex e cd st) define g where "g = costs (TRANSFER ad ex) e cd st" show ?case proof (rule allI[OF impI]) fix st6' assume stmt_def: "stmt (TRANSFER ad ex) e cd st = Normal ((), st6')" show "gas st6' \ gas st" proof cases assume "gas st \ g" with 8 stmt_def g_def show ?thesis using stmt.psimps(8)[of ad ex e cd st] by simp next assume "\ gas st \ g" then have l1: "assert Gas (\st. costs (TRANSFER ad ex) e cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: " modify (\st. st\gas := gas st - costs (TRANSFER ad ex) e cd st\) st = Normal ((), st')" using g_def by simp show ?thesis proof (cases "expr ad e cd st' (gas st - g)") case (n a0 g') define st'' where "st'' = st'\gas := g'\" with n have l3: "toState (expr ad e cd) st' = Normal (a0, st'')" using st'_def by simp then show ?thesis proof (cases a0) case (Pair b c) then show ?thesis proof (cases b) case (KValue adv) then show ?thesis proof (cases c) case (Value x1) then show ?thesis proof (cases x1) case (TSInt x1) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp next case (TUInt x2) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp next case TBool with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp next case TAddr then have l4: "(case a0 of (KValue adv, Value TAddr) \ return adv | (KValue adv, Value _) \ throw Err | (KValue adv, _) \ throw Err | (_, b) \ throw Err) st'' = Normal (adv, st'')" using Pair KValue Value by simp then show ?thesis proof (cases "expr ex e cd st'' (gas st'')") case n2: (n a1 g'') define st''' where "st''' = st''\gas := g''\" with n2 have l5: "toState (expr ex e cd) st'' = Normal (a1, st''')" by simp then show ?thesis proof (cases a1) case p2: (Pair b c) then show ?thesis proof (cases b) case k2: (KValue v) then show ?thesis proof (cases c) case v2: (Value t) then have l6: "(case a1 of (KValue v, Value t) \ return (v, t) | (KValue v, _) \ throw Err | (_, b) \ throw Err) st''' = Normal ((v,t), st''')" using p2 k2 by simp then show ?thesis proof (cases "convert t (TUInt 256) v") case None with 8(1) stmt_def g_def `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case (Some v') then show ?thesis proof (cases "type (accounts st''' adv)") case None with 8(1) stmt_def g_def `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case s0: (Some a) then show ?thesis proof (cases a) case EOA then show ?thesis proof (cases "transfer (address e) adv v' (accounts st''')") case None with 8(1) stmt_def g_def `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some EOA s0 show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case s1: (Some acc) then have l7: "option Err (\st. transfer (address e) adv v' (accounts st)) st''' = Normal (acc, st''')" using st'''_def by simp with 8(1) `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some EOA g_def s0 have "stmt (TRANSFER ad ex) e cd st = Normal ((),st'''\accounts:=acc\)" using stmt.psimps(8)[of ad ex e cd st] st'_def st''_def st'''_def by simp with stmt_def have "gas st6' = gas (st'''\accounts:=acc\)" by auto also from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st'' "gas st''"] have "\ \ gas st''" using st'_def st''_def st'''_def n2 by fastforce also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"] have "\ \ gas st'" using st'_def st''_def n by fastforce finally show ?thesis using st'_def by simp qed next case (Contract c) then show ?thesis proof (cases "ep $$ c") case None with 8(1) stmt_def g_def `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr Contract Some s0 show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case s2: (Some a) then show ?thesis proof (cases a) case p3: (fields ct cn f) with s2 have l7: "option Err (\_. ep $$ c) st''' = Normal ((ct, cn, f), st''')" by simp define e' where "e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct)" show ?thesis proof (cases "transfer (address e) adv v' (accounts st''')") case None with 8(1) stmt_def g_def `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr Contract Some s2 p3 s0 show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case s3: (Some acc) then have l8: "option Err (\st. transfer (address e) adv v' (accounts st)) st''' = Normal (acc, st''')" by simp then show ?thesis proof (cases "stmt f e' emptyStore (st'''\accounts := acc, stack:=emptyStore, memory:=emptyStore\)") case n3: (n a st'''') with 8(1) `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some s2 p3 g_def Contract s3 s0 have "stmt (TRANSFER ad ex) e cd st = Normal ((),st''''\stack:=stack st''', memory := memory st'''\)" using e'_def stmt.psimps(8)[of ad ex e cd st] st'_def st''_def st'''_def by simp with stmt_def have "gas st6' \ gas st''''" by auto also from 8(2)[OF l1 l2 l3 l4 l5 l6, of v t _ _ "accounts st'''" "st'''", OF _ _ _ s0 Contract l7 _ _ _ _ _ l8, where ?s'k="st'''\accounts := acc, stack := emptyStore, memory := emptyStore\"] `\ gas st \ g` e'_def n3 Some have "\ \ gas (st'''\accounts := acc, stack := emptyStore, memory := emptyStore\)" by simp also from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st'' "gas st''"] have "\ \ gas st''" using st'_def st''_def st'''_def n2 by fastforce also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"] have "\ \ gas st'" using st'_def st''_def n by fastforce finally show ?thesis using st'_def by simp next case (e x) with 8(1) `\ gas st \ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some s2 p3 g_def e'_def stmt_def Contract s3 s0 show ?thesis using stmt.psimps(8)[of ad ex e cd st] st'_def st''_def st'''_def by simp qed qed qed qed qed qed qed next case (Calldata x2) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value TAddr n2 p2 k2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case (Memory x3) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value TAddr n2 p2 k2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case (Storage x4) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value TAddr n2 p2 k2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp qed next case (KCDptr x2) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value TAddr n2 p2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case (KMemptr x3) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value TAddr n2 p2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp next case (KStoptr x4) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value TAddr n2 p2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp qed qed next case (e e) with 8(1) stmt_def `\ gas st \ g` n Pair KValue Value TAddr g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp qed qed next case (Calldata x2) with 8(1) stmt_def `\ gas st \ g` n Pair KValue g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp next case (Memory x3) with 8(1) stmt_def `\ gas st \ g` n Pair KValue g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp next case (Storage x4) with 8(1) stmt_def `\ gas st \ g` n Pair KValue g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp qed next case (KCDptr x2) with 8(1) stmt_def `\ gas st \ g` n Pair g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp next case (KMemptr x3) with 8(1) stmt_def `\ gas st \ g` n Pair g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp next case (KStoptr x4) with 8(1) stmt_def `\ gas st \ g` n Pair g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp qed qed next case (e e) with 8(1) stmt_def `\ gas st \ g` g_def show ?thesis using stmt.psimps(8) st'_def by simp qed qed qed next case (9 id0 tp s e\<^sub>v cd st) define g where "g = costs (BLOCK ((id0, tp), None) s) e\<^sub>v cd st" show ?case proof (rule allI[OF impI]) fix st6' assume stmt_def: "stmt (BLOCK ((id0, tp), None) s) e\<^sub>v cd st = Normal ((), st6')" show "gas st6' \ gas st" proof cases assume "gas st \ g" with 9 stmt_def g_def show ?thesis using stmt.psimps(9) by simp next assume "\ gas st \ g" then have l1: "assert Gas (\st. costs (BLOCK ((id0, tp), None) s) e\<^sub>v cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: "modify (\st. st\gas := gas st - costs (BLOCK ((id0, tp), None) s) e\<^sub>v cd st\) st = Normal ((), st')" using g_def by simp show ?thesis proof (cases "decl id0 tp None False cd (memory st') (storage st') (cd, (memory st'), (stack st'), e\<^sub>v)") case n2: None with 9 stmt_def `\ gas st \ g` g_def show ?thesis using stmt.psimps(9) st'_def by simp next case (Some a) then have l3: "option Err (\st. decl id0 tp None False cd (memory st) (storage st) (cd, memory st, stack st, e\<^sub>v)) st' = Normal (a, st')" by simp then show ?thesis proof (cases a) case (fields cd' mem' sck' e') with 9(1) stmt_def `\ gas st \ g` g_def have "stmt (BLOCK ((id0, tp), None) s) e\<^sub>v cd st = stmt s e' cd' (st\gas := gas st - g, stack := sck', memory := mem'\)" using stmt.psimps(9)[OF 9(1)] Some st'_def by simp with 9(2)[OF l1 l2 l3] stmt_def `\ gas st \ g` fields g_def have "gas st6' \ gas (st\gas := gas st - g, stack := sck', memory := mem'\)" using st'_def by fastforce then show ?thesis by simp qed qed qed qed next case (10 id0 tp ex' s e\<^sub>v cd st) define g where "g = costs (BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st" show ?case proof (rule allI[OF impI]) fix st6' assume stmt_def: "stmt (BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st = Normal ((), st6')" show "gas st6' \ gas st" proof cases assume "gas st \ g" with 10 stmt_def g_def show ?thesis using stmt.psimps(10) by simp next assume "\ gas st \ g" then have l1: "assert Gas (\st. costs (BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: "modify (\st. st\gas := gas st - costs (BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st\) st = Normal ((), st')" using g_def by simp show ?thesis proof (cases "expr ex' e\<^sub>v cd st' (gas st - g)") case (n a g') define st'' where "st'' = st'\gas := g'\" with n have l3: "toState (expr ex' e\<^sub>v cd) st' = Normal (a, st'')" using st''_def st'_def by simp then show ?thesis proof (cases a) case (Pair v t) then show ?thesis proof (cases "decl id0 tp (Some (v, t)) False cd (memory st'') (storage st'') (cd, memory st'', stack st'', e\<^sub>v)") case None with 10(1) stmt_def `\ gas st \ g` n Pair g_def show ?thesis using stmt.psimps(10) st'_def st''_def by simp next case s2: (Some a) then have l4: "option Err (\st. decl id0 tp (Some (v, t)) False cd (memory st) (storage st) (cd, memory st, stack st, e\<^sub>v)) st'' = Normal (a, st'')" by simp then show ?thesis proof (cases a) case (fields cd' mem' sck' e') with 10(1) stmt_def `\ gas st \ g` n Pair s2 g_def have "stmt (BLOCK ((id0, tp), Some ex') s) e\<^sub>v cd st = stmt s e' cd' (st''\stack := sck', memory := mem'\)" using stmt.psimps(10)[of id0 tp ex' s e\<^sub>v cd st] st'_def st''_def by simp with 10(2)[OF l1 l2 l3 Pair l4 fields, where s'd="st''\stack := sck', memory := mem'\"] n stmt_def `\ gas st \ g` s2 fields g_def have "gas st6' \ gas st''" by simp moreover from msel_ssel_expr_load_rexp_gas(3)[of ex' e\<^sub>v cd st' "gas st - g"] n have "gas st'' \ gas st'" using st'_def st''_def by fastforce ultimately show ?thesis using st'_def by simp qed qed qed next case (e e) with 10 stmt_def `\ gas st \ g` g_def show ?thesis using stmt.psimps(10) st'_def by simp qed qed qed next case (11 i xe val e cd st) define g where "g = costs (NEW i xe val) e cd st" show ?case proof (rule allI[OF impI]) fix st6' assume a1: "stmt (NEW i xe val) e cd st = Normal ((), st6')" show "gas st6' \ gas st" proof (cases) assume "gas st \ g" with 11(1) a1 show ?thesis using stmt.psimps(11) g_def by simp next assume gcost: "\ gas st \ g" then have l1: "assert Gas (\st. costs (NEW i xe val) e cd st < gas st) st = Normal ((), st) " using g_def by simp define st' where "st' = st\gas := gas st - g\" then have l2: "modify (\st. st\gas := gas st - costs (NEW i xe val) e cd st\) st = Normal ((), st')" using g_def by simp define adv where "adv = hash (address e) (ShowL\<^sub>n\<^sub>a\<^sub>t (contracts (accounts st' (address e))))" then show ?thesis proof (cases "type (accounts st' adv) = None") case True then show ?thesis proof (cases "expr val e cd st' (gas st')") case n0: (n kv g') define st'' where "st'' = st'\gas := g'\" then have l4: "toState (expr val e cd) st' = Normal (kv, st'')" using n0 by simp then show ?thesis proof (cases kv) case p0: (Pair a b) then show ?thesis proof (cases a) case k0: (KValue v) then show ?thesis proof (cases b) case v0: (Value t) then show ?thesis proof (cases "ep $$ i") case None with a1 gcost g_def True n0 p0 k0 v0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def st''_def by simp next case s0: (Some a) then have l5: "option Err (\_. ep $$ i) st'' = Normal (a, st'')" by simp then show ?thesis proof (cases a) case f0: (fields ct cn _) define e' where "e' = ffold_init ct (emptyEnv adv i (address e) v) (fmdom ct)" then show ?thesis proof (cases "load True (fst cn) xe e' emptyStore emptyStore emptyStore e cd st'' (gas st'')") case n1: (n a g'') define st''' where "st''' = st''\gas := g''\" then have l6: "toState (load True (fst cn) xe e' emptyStore emptyStore emptyStore e cd) st'' = Normal (a, st''')" using n1 by simp then show ?thesis proof (cases a) case f1: (fields e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l) define st'''' where "st'''' = st'''\accounts:=(accounts st''')(adv := \bal = ShowL\<^sub>i\<^sub>n\<^sub>t 0, type = Some (Contract i), contracts = 0\), storage:=(storage st''')(adv := {$$})\" then show ?thesis proof (cases "transfer (address e) adv v (accounts st'''')") case None with a1 gcost g_def True n0 p0 k0 v0 s0 f0 n1 f1 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def e'_def st'_def st''_def st'''_def st''''_def by (simp add:Let_def) next case s1: (Some acc) define st''''' where "st''''' = st''''\accounts := acc, stack:=k\<^sub>l, memory:=m\<^sub>l\" then show ?thesis proof (cases "stmt (snd cn) e\<^sub>l cd\<^sub>l st'''''") case (n a st'''''') define st''''''' where "st''''''' = st''''''\stack:=stack st'''', memory := memory st''''\" define st'''''''' where "st'''''''' = incrementAccountContracts (address e) st'''''''" from a1 gcost g_def True n0 p0 k0 v0 s0 f0 n1 f1 s1 n have "st6' = st''''''''" using st'_def st''_def st'''_def st''''_def st'''''_def st'''''''_def st''''''''_def stmt.psimps(11)[OF 11(1)] adv_def e'_def by (simp add:Let_def) then have "gas st6' = gas st''''''''" by simp also have "\ \ gas st'''''''" using st''''''''_def incrementAccountContracts_def by simp also have "\ \ gas st''''''" using st'''''''_def by simp also have "\ \ gas st'''''" using 11(2)[OF l1 l2 _ _ l4 _ _ l5 _ _ e'_def l6, where ?s'h="st''''" and ?s'i="st''''" and ?s'j="st''''" and ?s'k="st''''\accounts := acc, stack := k\<^sub>l, memory := m\<^sub>l\", of st' "()"] p0 k0 v0 f0 f1 s1 n True st''''_def st'''''_def adv_def by simp also have "\ \ gas st''''" using st'''''_def by simp also have "\ \ gas st'''" using st''''_def by simp also have "\ \ gas st''" using st'''_def msel_ssel_expr_load_rexp_gas(4) n1 f1 by simp also have "\ \ gas st'" using st''_def msel_ssel_expr_load_rexp_gas(3) n0 p0 by simp also have "\ \ gas st" using st'_def by simp finally show ?thesis . next case (e e) with a1 gcost g_def n0 True p0 k0 v0 s0 f0 n1 f1 s1 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def e'_def st'_def st''_def st'''_def st''''_def st'''''_def by (simp add:Let_def) qed qed qed next case (e e) with a1 gcost g_def n0 True p0 k0 v0 s0 f0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def e'_def st'_def st''_def by (simp add:Let_def) qed qed qed next case (Calldata x2) with a1 gcost g_def n0 True p0 k0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp next case (Memory x3) with a1 gcost g_def n0 True p0 k0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp next case (Storage x4) with a1 gcost g_def n0 True p0 k0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp qed next case (KCDptr x2) with a1 gcost g_def n0 True p0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp next case (KMemptr x3) with a1 gcost g_def n0 True p0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp next case (KStoptr x4) with a1 gcost g_def n0 True p0 show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp qed qed next case (e e) with a1 gcost g_def True show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp qed next case False with a1 gcost g_def show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by (simp split:if_split_asm) qed qed qed qed subsection \Termination function\ text \Now we can prove termination using the lemma above.\ fun sgas where "sgas l = gas (snd (snd (snd l)))" fun ssize where "ssize l = size (fst l)" method stmt_dom_gas = match premises in s: "stmt _ _ _ _ = Normal (_,_)" and d[thin]: "stmt_dom _" \ \insert stmt_dom_gas[OF d s]\ method msel_ssel_expr_load_rexp = match premises in e[thin]: "expr _ _ _ _ _ = Normal (_,_)" \ \insert msel_ssel_expr_load_rexp_gas(3)[OF e]\ | match premises in l[thin]: "load _ _ _ _ _ _ _ _ _ _ _ = Normal (_,_)" \ \insert msel_ssel_expr_load_rexp_gas(4)[OF l, THEN conjunct1]\ method costs = match premises in "costs (WHILE ex s0) e cd st < _" for ex s0 and e::Environment and cd::CalldataT and st::State \ \insert while_not_zero[of (unchecked) ex s0 e cd st]\ | match premises in "costs (INVOKE i xe) e cd st < _" for i xe and e::Environment and cd::CalldataT and st::State \ \insert invoke_not_zero[of (unchecked) i xe e cd st]\ | match premises in "costs (EXTERNAL ad i xe val) e cd st < _" for ad i xe val and e::Environment and cd::CalldataT and st::State \ \insert external_not_zero[of (unchecked) ad i xe val e cd st]\ | match premises in "costs (TRANSFER ad ex) e cd st < _" for ad ex and e::Environment and cd::CalldataT and st::State \ \insert transfer_not_zero[of (unchecked) ad ex e cd st]\ | match premises in "costs (NEW i xe val) e cd st < _" for i xe val and e::Environment and cd::CalldataT and st::State \ \insert new_not_zero[of (unchecked) i xe val e cd st]\ termination stmt apply (relation "measures [sgas, ssize]") apply (auto split: if_split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm bool.split_asm atype.split_asm) apply ((stmt_dom_gas | msel_ssel_expr_load_rexp)+, costs?, simp)+ done subsection \Gas Reduction\ text \ The following corollary is a generalization of @{thm [source] msel_ssel_expr_load_rexp_dom_gas}. We first prove that the function is defined for all input values and then obtain the final result as a corollary. \ lemma stmt_dom: "stmt_dom (s6, ev6, cd6, st6)" apply (induct rule: stmt.induct[where ?P="\s6 ev6 cd6 st6. stmt_dom (s6, ev6, cd6, st6)"]) apply (simp_all add: stmt.domintros(1-10)) apply (rule stmt.domintros(11), force) done lemmas stmt_gas = stmt_dom_gas[OF stmt_dom] lemma skip: assumes "stmt SKIP ev cd st = Normal (x, st')" shows "gas st > costs SKIP ev cd st" and "st' = st\gas := gas st - costs SKIP ev cd st\" using assms by (auto split:if_split_asm) lemma assign: assumes "stmt (ASSIGN lv ex) ev cd st = Normal (xx, st')" obtains (1) v t g l t' g' v' where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Value t'),g')" and "convert t t' v = Some v'" and "st' = st\gas := g', stack := updateStore l (KValue v') (stack st)\" | (2) v t g l t' g' v' where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, Storage (STValue t')),g')" and "convert t t' v = Some v'" and "st' = st\gas := g', storage := (storage st) (address ev := (fmupd l v' (storage st (address ev))))\" | (3) v t g l t' g' v' where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, Memory (MTValue t')),g')" and "convert t t' v = Some v'" and "st' = st\gas := g', memory := updateStore l (MValue v') (memory st)\" | (4) p x t g l t' g' p' m where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Memory t'),g')" and "accessStore l (stack st) = Some (KMemptr p')" and "cpm2m p p' x t cd (memory st) = Some m" and "st' = st\gas := g', memory := m\" | (5) p x t g l t' g' p' s where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Storage t'),g')" and "accessStore l (stack st) = Some (KStoptr p')" and "cpm2s p p' x t cd (storage st (address ev)) = Some s" and "st' = st\gas := g', storage := (storage st) (address ev := s)\" | (6) p x t g l t' g' s where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, t'),g')" and "cpm2s p l x t cd (storage st (address ev)) = Some s" and "st' = st\gas := g', storage := (storage st) (address ev := s)\" | (7) p x t g l t' g' m where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, t'),g')" and "cpm2m p l x t cd (memory st) = Some m" and "st' = st\gas := g', memory := m\" | (8) p x t g l t' g' where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Memory t'),g')" and "st' = st\gas := g', stack := updateStore l (KMemptr p) (stack st)\" | (9) p x t g l t' g' p' s where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Storage t'),g')" and "accessStore l (stack st) = Some (KStoptr p')" and "cpm2s p p' x t (memory st) (storage st (address ev)) = Some s" and "st' = st\gas := g', storage := (storage st) (address ev := s)\" | (10) p x t g l t' g' s where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, t'),g')" and "cpm2s p l x t (memory st) (storage st (address ev)) = Some s" and "st' = st\gas := g', storage := (storage st) (address ev := s)\" | (11) p x t g l t' g' where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, t'),g')" and "st' = st\gas := g', memory := updateStore l (MPointer p) (memory st)\" | (12) p x t g l t' g' p' m where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Memory t'),g')" and "accessStore l (stack st) = Some (KMemptr p')" and "cps2m p p' x t (storage st (address ev)) (memory st) = Some m" and "st' = st\gas := g', memory := m\" | (13) p x t g l t' g' where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Storage t'),g')" and "st' = st\gas := g', stack := updateStore l (KStoptr p) (stack st)\" | (14) p x t g l t' g' s where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, t'),g')" and "copy p l x t (storage st (address ev)) = Some s" and "st' = st\gas := g', storage := (storage st) (address ev := s)\" | (15) p x t g l t' g' m where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, t'),g')" and "cps2m p l x t (storage st (address ev)) (memory st) = Some m" and "st' = st\gas := g', memory := m\" | (16) p t t' g l t'' g' where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STMap t t')), g)" and "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, t''),g')" and "st' = st\gas := g', stack := updateStore l (KStoptr p) (stack st)\" proof - from assms consider (1) v t g where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)" | (2) p x t g where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)" | (3) p x t g where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)" | (4) p x t g where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)" | (5) p t t' g where "expr ex ev cd (st\gas := gas st - costs (ASSIGN lv ex) ev cd st\) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STMap t t')), g)" by (auto split:if_split_asm result.split_asm Stackvalue.split_asm Type.split_asm MTypes.split_asm STypes.split_asm) then show ?thesis proof cases case 1 with assms consider (11) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Value t'),g')" | (12) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, Storage (STValue t')),g')" | (13) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, Memory (MTValue t')),g')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm) then show ?thesis proof cases case 11 with 1 assms show ?thesis using that(1) by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm) next case 12 with 1 assms show ?thesis using that(2) by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm) next case 13 with 1 assms show ?thesis using that(3) by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm) qed next case 2 with assms consider (21) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Memory t'),g')" | (22) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Storage t'),g')" | (23) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, t'),g')" | (24) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, t'),g')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm) then show ?thesis proof cases case 21 moreover from assms 2 21 obtain p' where 3: "accessStore l (stack st) = Some (KMemptr p')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) moreover from assms 2 21 3 obtain m where "cpm2m p p' x t cd (memory st) = Some m" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(4) assms 2 21 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 22 moreover from assms 2 22 obtain p' where 3: "accessStore l (stack st) = Some (KStoptr p')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) moreover from assms 2 22 3 4 obtain s where "cpm2s p p' x t cd (storage st (address ev)) = Some s" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(5) assms 2 22 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 23 moreover from assms 2 23 3 4 obtain s where "cpm2s p l x t cd (storage st (address ev)) = Some s" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(6) assms 2 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 24 moreover from assms 2 24 obtain m where "cpm2m p l x t cd (memory st) = Some m" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(7) assms 2 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) qed next case 3 with assms consider (31) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Memory t'),g')" | (32) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Storage t'),g')" | (33) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, t'),g')" | (34) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, t'),g')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm) then show ?thesis proof cases case 31 then show ?thesis using that(8) assms 3 by (auto split:if_split_asm) next case 32 moreover from assms 3 32 obtain p' where 4: "accessStore l (stack st) = Some (KStoptr p')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) moreover from assms 3 32 4 5 obtain s where "cpm2s p p' x t (memory st) (storage st (address ev)) = Some s" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(9) assms 3 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 33 moreover from assms 3 33 3 4 obtain s where "cpm2s p l x t (memory st) (storage st (address ev)) = Some s" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(10) assms 3 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 34 then show ?thesis using that(11) assms 3 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) qed next case 4 with assms consider (41) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Memory t'),g')" | (42) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStackloc l, Storage t'),g')" | (43) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LStoreloc l, t'),g')" | (44) l t' g' where "lexp lv ev cd (st\gas := g\) g = Normal((LMemloc l, t'),g')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm) then show ?thesis proof cases case 41 moreover from assms 4 41 obtain p' where 5: "accessStore l (stack st) = Some (KMemptr p')" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) moreover from assms 4 41 5 6 obtain m where "cps2m p p' x t (storage st (address ev)) (memory st) = Some m" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(12) assms 4 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 42 then show ?thesis using that(13) assms 4 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 43 moreover from assms 4 43 5 obtain s where "copy p l x t (storage st (address ev)) = Some s" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(14) assms 4 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) next case 44 moreover from assms 4 44 5 obtain m where "cps2m p l x t (storage st (address ev)) (memory st) = Some m" by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) ultimately show ?thesis using that(15) assms 4 by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) qed next case 5 then show ?thesis using that(16) assms by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm) qed qed lemma comp: assumes "stmt (COMP s1 s2) ev cd st = Normal (x, st')" obtains (1) st'' where "gas st > costs (COMP s1 s2) ev cd st" and "stmt s1 ev cd (st\gas := gas st - costs (COMP s1 s2) ev cd st\) = Normal((), st'')" and "stmt s2 ev cd st'' = Normal((), st')" using assms by (simp split:if_split_asm result.split_asm prod.split_asm) lemma ite: assumes "stmt (ITE ex s1 s2) ev cd st = Normal (x, st')" obtains (True) g where "gas st > costs (ITE ex s1 s2) ev cd st" and "expr ex ev cd (st\gas := gas st - costs (ITE ex s1 s2) ev cd st\) (gas st - costs (ITE ex s1 s2) ev cd st) = Normal((KValue (ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True), Value TBool), g)" and "stmt s1 ev cd (st\gas := g\) = Normal((), st')" | (False) g where "gas st > costs (ITE ex s1 s2) ev cd st" and "expr ex ev cd (st\gas := gas st - costs (ITE ex s1 s2) ev cd st\) (gas st - costs (ITE ex s1 s2) ev cd st) = Normal((KValue (ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False), Value TBool), g)" and "stmt s2 ev cd (st\gas := g\) = Normal((), st')" using assms by (simp split:if_split_asm result.split_asm prod.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm) lemma while: assumes "stmt (WHILE ex s0) ev cd st = Normal (x, st')" obtains (True) g st'' where "gas st > costs (WHILE ex s0) ev cd st" and "expr ex ev cd (st\gas := gas st - costs (WHILE ex s0) ev cd st\) (gas st - costs (WHILE ex s0) ev cd st) = Normal((KValue (ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True), Value TBool), g)" and "stmt s0 ev cd (st\gas := g\) = Normal((), st'')" and "stmt (WHILE ex s0) ev cd st'' = Normal ((), st')" | (False) g where "gas st > costs (WHILE ex s0) ev cd st" and "expr ex ev cd (st\gas := gas st - costs (WHILE ex s0) ev cd st\) (gas st - costs (WHILE ex s0) ev cd st) = Normal((KValue (ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False), Value TBool), g)" and "st' = st\gas := g\" using assms proof - from assms have 1: "gas st > costs (WHILE ex s0) ev cd st" by (simp split:if_split_asm) moreover from assms 1 have 2: "modify (\st. st\gas := gas st - costs (WHILE ex s0) ev cd st\) st = Normal ((), st\gas := gas st - costs (WHILE ex s0) ev cd st\)" by simp moreover from assms 1 2 obtain b g where 3: "expr ex ev cd (st\gas := gas st - costs (WHILE ex s0) ev cd st\) (gas st - costs (WHILE ex s0) ev cd st) = Normal ((KValue b, Value TBool), g)" by (simp split:result.split_asm prod.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm) ultimately consider (True) "b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True" | (False) "b = ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False" | (None) "b \ ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l True \ b \ ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l False" by auto then show ?thesis proof cases case True moreover from assms 1 2 3 True obtain st' where 4: "stmt s0 ev cd (st\gas := g\) = Normal ((), st')" by (simp split:result.split_asm prod.split_asm) moreover from assms 1 2 3 4 True obtain st'' where 5: "stmt (WHILE ex s0) ev cd st' = Normal ((), st'')" by (simp split:result.split_asm prod.split_asm) ultimately show ?thesis using 1 2 3 that(1) assms by simp next case False then show ?thesis using 1 2 3 that(2) assms true_neq_false by simp next case None then show ?thesis using 1 2 3 assms by simp qed qed lemma invoke: fixes ev defines "e' members \ ffold (init members) (emptyEnv (address ev) (contract ev) (sender ev) (svalue ev)) (fmdom members)" assumes "stmt (INVOKE i xe) ev cd st = Normal (x, st')" obtains ct fb fp f e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g st'' where "gas st > costs (INVOKE i xe) ev cd st" and "ep $$ contract ev = Some (ct, fb)" and "ct $$ i = Some (Method (fp, False, f))" and "load False fp xe (e' ct) emptyStore emptyStore (memory (st\gas := gas st - costs (INVOKE i xe) ev cd st\)) ev cd (st\gas := gas st - costs (INVOKE i xe) ev cd st\) (gas st - costs (INVOKE i xe) ev cd st) = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g)" and "stmt f e\<^sub>l cd\<^sub>l (st\gas:= g, stack:=k\<^sub>l, memory:=m\<^sub>l\) = Normal ((), st'')" and "st' = st''\stack:=stack st\" proof - from assms have 1: "gas st > costs (INVOKE i xe) ev cd st" by (simp split:if_split_asm) moreover from assms 1 obtain ct fb where 2: "ep $$ (contract ev) = Some (ct, fb)" by (simp split: prod.split_asm result.split_asm option.split_asm) moreover from assms 1 2 obtain fp f where 3: "ct $$ i = Some (Method (fp, False, f))" by (simp split: prod.split_asm result.split_asm option.split_asm Member.split_asm bool.split_asm) moreover from assms 1 2 3 obtain e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g where 4: "load False fp xe (e' ct) emptyStore emptyStore (memory (st\gas := gas st - costs (INVOKE i xe) ev cd st\)) ev cd (st\gas := gas st - costs (INVOKE i xe) ev cd st\) (gas st - costs (INVOKE i xe) ev cd st) = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g)" by (simp split: prod.split_asm result.split_asm) moreover from assms 1 2 3 4 obtain st'' where 5: "stmt f e\<^sub>l cd\<^sub>l (st\gas:= g, stack:=k\<^sub>l, memory:=m\<^sub>l\) = Normal ((), st'')" by (simp split: prod.split_asm result.split_asm) moreover from assms 1 2 3 4 5 have "st' = st''\stack:=stack st\" by (simp split: prod.split_asm result.split_asm) ultimately show ?thesis using that by simp qed lemma external: fixes ev defines "e' members adv c v \ ffold (init members) (emptyEnv adv c (address ev) v) (fmdom members)" assumes "stmt (EXTERNAL ad' i xe val) ev cd st = Normal (x, st')" obtains (Some) adv c g ct cn fb' v t g' v' fp f e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g'' acc st'' where "gas st > costs (EXTERNAL ad' i xe val) ev cd st" and "expr ad' ev cd (st\gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st\) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g)" and "adv \ address ev" and "type (accounts (st\gas := g\) adv) = Some (Contract c)" and "ep $$ c = Some (ct, cn, fb')" and "expr val ev cd (st\gas := g\) g = Normal ((KValue v, Value t), g')" and "convert t (TUInt 256) v = Some v'" and "fmlookup ct i = Some (Method (fp, True, f))" and "load True fp xe (e' ct adv c v') emptyStore emptyStore emptyStore ev cd (st\gas := g'\) g' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g'')" and "transfer (address ev) adv v' (accounts (st\gas := g''\)) = Some acc" and "stmt f e\<^sub>l cd\<^sub>l (st\gas := g'', accounts := acc, stack:=k\<^sub>l, memory:=m\<^sub>l\) = Normal ((), st'')" and "st' = st''\stack:=stack st, memory := memory st\" | (None) adv c g ct cn fb' v t g' v' acc st'' where "gas st > costs (EXTERNAL ad' i xe val) ev cd st" and "expr ad' ev cd (st\gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st\) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g)" and "adv \ address ev" and "type (accounts (st\gas := g\) adv) = Some (Contract c)" and "ep $$ c = Some (ct, cn, fb')" and "expr val ev cd (st\gas := g\) g = Normal ((KValue v, Value t), g')" and "convert t (TUInt 256) v = Some v'" and "ct $$ i = None" and "transfer (address ev) adv v' (accounts st) = Some acc" and "stmt fb' (e' ct adv c v') emptyStore (st\gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore\) = Normal ((), st'')" and "st' = st''\stack:=stack st, memory := memory st\" proof - from assms have 1: "gas st > costs (EXTERNAL ad' i xe val) ev cd st" by (simp split:if_split_asm) moreover from assms 1 obtain adv g where 2: "expr ad' ev cd (st\gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st\) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g)" by (simp split: prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm) moreover from assms 1 2 obtain c where 3: "type (accounts (st\gas := g\) adv) = Some (Contract c)" by (simp split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm atype.split_asm) moreover from assms 1 2 3 obtain ct cn fb' where 4: "ep $$ c = Some (ct, cn, fb')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm) moreover from assms 1 2 3 4 obtain v t g' where 5: "expr val ev cd (st\gas := g\) g = Normal ((KValue v, Value t), g')" using 1 2 by (simp split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm) moreover from assms 1 2 3 4 5 have 6: "adv \ address ev" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm) moreover from assms 1 2 3 4 5 6 obtain v' where 7: "convert t (TUInt 256) v = Some v'" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm) ultimately consider (Some) fp f where "ct $$ i = Some (Method (fp, True, f))" | (None) "fmlookup ct i = None" using assms by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm bool.split_asm) then show ?thesis proof cases case (Some fp f) moreover from assms 1 2 3 4 5 6 7 Some obtain e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g'' where 8: "load True fp xe (e' ct adv c v') emptyStore emptyStore emptyStore ev cd (st\gas := g'\) g' = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g'')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 5 6 7 Some 8 obtain acc where 9: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 5 6 7 Some 8 9 obtain st'' where 10: "stmt f e\<^sub>l cd\<^sub>l (st\gas := g'', accounts := acc, stack:=k\<^sub>l, memory:=m\<^sub>l\) = Normal ((), st'')" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 5 6 7 Some 8 9 10 have "st' = st''\stack:=stack st, memory := memory st\" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) ultimately show ?thesis using 1 2 3 4 5 6 7 that(1) by simp next case None moreover from assms 1 2 3 4 5 6 7 None obtain acc where 8: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 5 6 7 None 8 obtain st'' where 9: "stmt fb' (e' ct adv c v') emptyStore (st\gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore\) = Normal ((), st'')" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 5 6 7 None 8 9 have "st' = st''\stack:=stack st, memory := memory st\" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) ultimately show ?thesis using 1 2 3 4 5 6 7 that(2) by simp qed qed lemma transfer: fixes ev defines "e' members adv c st v \ ffold (init members) (emptyEnv adv c (address ev) v) (fmdom members)" assumes "stmt (TRANSFER ad ex) ev cd st = Normal (x, st')" obtains (Contract) v t g adv c g' v' acc ct cn f st'' where "gas st > costs (TRANSFER ad ex) ev cd st" and "expr ad ev cd (st\gas := gas st - costs (TRANSFER ad ex) ev cd st\) (gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)" and "expr ex ev cd (st\gas := g\) g = Normal ((KValue v, Value t), g')" and "convert t (TUInt 256) v = Some v'" and "type (accounts (st\gas := g\) adv) = Some (Contract c)" and "ep $$ c = Some (ct, cn, f)" and "transfer (address ev) adv v' (accounts st) = Some acc" and "stmt f (e' ct adv c (st\gas := g'\) v') emptyStore (st\gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore\) = Normal ((), st'')" and "st' = st''\stack:=stack st, memory := memory st\" | (EOA) v t g adv g' v' acc where "gas st > costs (TRANSFER ad ex) ev cd st" and "expr ad ev cd (st\gas := gas st - costs (TRANSFER ad ex) ev cd st\) (gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)" and "expr ex ev cd (st\gas := g\) g = Normal ((KValue v, Value t), g')" and "convert t (TUInt 256) v = Some v'" and "type (accounts (st\gas := g\) adv) = Some EOA" and "transfer (address ev) adv v' (accounts st) = Some acc" and "st' = st\gas:=g', accounts:=acc\" proof - from assms have 1: "gas st > costs (TRANSFER ad ex) ev cd st" by (simp split:if_split_asm) moreover from assms 1 obtain adv g where 2: "expr ad ev cd (st\gas := gas st - costs (TRANSFER ad ex) ev cd st\) (gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm) moreover from assms 1 2 obtain v t g' where 3: "expr ex ev cd (st\gas := g\) g = Normal ((KValue v, Value t), g')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm) moreover from assms 1 2 3 obtain v' where 4: "convert t (TUInt 256) v = Some v'" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm) ultimately consider (Contract) c where "type (accounts (st\gas := g'\) adv) = Some (Contract c)" | (EOA) "type (accounts (st\gas := g'\) adv) = Some EOA" using assms by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm atype.split_asm) then show ?thesis proof cases case (Contract c) moreover from assms 1 2 3 4 Contract obtain ct cn f where 5: "ep $$ c = Some (ct, cn, f)" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm atype.split_asm atype.split_asm) moreover from assms 1 2 3 4 Contract 5 obtain acc where 6: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 Contract 5 6 obtain st'' where 7: "stmt f (e' ct adv c (st\gas := g'\) v') emptyStore (st\gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore\) = Normal ((), st'')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 Contract 5 6 7 have "st' = st''\stack:=stack st, memory := memory st\" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) ultimately show ?thesis using 1 2 3 4 that(1) by simp next case EOA moreover from assms 1 2 3 4 EOA obtain acc where 5: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) moreover from assms 1 2 3 4 EOA 5 have "st' = st\gas:=g', accounts:=acc\" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm) ultimately show ?thesis using 1 2 3 4 that(2) by simp qed qed lemma blockNone: fixes ev assumes "stmt (BLOCK ((id0, tp), None) s) ev cd st = Normal (x, st')" obtains cd' mem' sck' e' where "gas st > costs (BLOCK ((id0, tp), None) s) ev cd st" and "decl id0 tp None False cd (memory (st\gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st\)) (storage (st\gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st\)) (cd, memory (st\gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st\), stack (st\gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st\), ev) = Some (cd', mem', sck', e')" and "stmt s e' cd' (st\gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st, stack := sck', memory := mem'\) = Normal ((), st')" using assms by (simp split:if_split_asm prod.split_asm option.split_asm) lemma blockSome: fixes ev assumes "stmt (BLOCK ((id0, tp), Some ex') s) ev cd st = Normal (x, st')" obtains v t g cd' mem' sck' e' where "gas st > costs (BLOCK ((id0, tp), Some ex') s) ev cd st" and "expr ex' ev cd (st\gas := gas st - costs (BLOCK ((id0, tp), Some ex') s) ev cd st\) (gas st - costs (BLOCK ((id0, tp), Some ex') s) ev cd st) = Normal((v,t),g)" and "decl id0 tp (Some (v, t)) False cd (memory (st\gas := g\)) (storage (st\gas := g\)) (cd, memory (st\gas := g\), stack (st\gas := g\), ev) = Some (cd', mem', sck', e')" and "stmt s e' cd' (st\gas := g, stack := sck', memory := mem'\) = Normal ((), st')" using assms by (auto split:if_split_asm result.split_asm prod.split_asm option.split_asm) lemma new: fixes i xe val ev cd st defines "st0 \ st\gas := gas st - costs (NEW i xe val) ev cd st\" defines "adv0 \ hash (address ev) (ShowL\<^sub>n\<^sub>a\<^sub>t (contracts (accounts st0 (address ev))))" defines "st1 g \ st\gas := g, accounts := (accounts st)(adv0 := \bal = ShowL\<^sub>i\<^sub>n\<^sub>t 0, type = Some (Contract i), contracts = 0\), storage:=(storage st)(adv0 := {$$})\" defines "e' members c v \ ffold (init members) (emptyEnv adv0 c (address ev) v) (fmdom members)" assumes "stmt (NEW i xe val) ev cd st = Normal (x, st')" obtains v t g ct cn fb e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g' acc st'' where "gas st > costs (NEW i xe val) ev cd st" and "type (accounts st adv0) = None" and "expr val ev cd st0 (gas st0) = Normal((KValue v, Value t),g)" and "ep $$ i = Some (ct, cn, fb)" and "load True (fst cn) xe (e' ct i v) emptyStore emptyStore emptyStore ev cd (st0\gas := g\) g = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g')" and "transfer (address ev) adv0 v (accounts (st1 g')) = Some acc" and "stmt (snd cn) e\<^sub>l cd\<^sub>l (st1 g'\accounts := acc, stack:=k\<^sub>l, memory:=m\<^sub>l\) = Normal ((), st'')" and "st' = incrementAccountContracts (address ev) (st''\stack:=stack st, memory := memory st\)" proof - from assms have 1: "gas st > costs (NEW i xe val) ev cd st" by (simp split:if_split_asm) moreover from st0_def assms 1 have 2: "type (accounts st adv0) = None" by (simp split: if_split_asm) moreover from st0_def assms 1 2 obtain v t g where 3: "expr val ev cd st0 (gas st0) = Normal((KValue v, Value t),g)" by (simp split: prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm) moreover from assms 1 st0_def 2 3 obtain ct cn fb where 4: "ep $$ i = Some(ct, cn, fb)" by (simp split: prod.split_asm result.split_asm option.split_asm) moreover from st0_def adv0_def e'_def assms 1 2 3 4 obtain e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g' where 5: "load True (fst cn) xe (e' ct i v) emptyStore emptyStore emptyStore ev cd (st0\gas := g\) g = Normal ((e\<^sub>l, cd\<^sub>l, k\<^sub>l, m\<^sub>l), g')" by (simp add:Let_def split: prod.split_asm result.split_asm option.split_asm) moreover from st0_def adv0_def e'_def assms 1 2 3 4 5 obtain acc where 6: "transfer (address ev) adv0 v (accounts (st1 g')) = Some acc" by (simp add:Let_def split: prod.split_asm result.split_asm option.split_asm) moreover from st0_def st1_def adv0_def e'_def assms 1 2 3 4 5 6 obtain st'' where "stmt (snd cn) e\<^sub>l cd\<^sub>l (st1 g'\accounts := acc, stack:=k\<^sub>l, memory:=m\<^sub>l\) = Normal ((), st'')" by (simp add:Let_def split: prod.split_asm result.split_asm option.split_asm) ultimately show ?thesis using that assms by simp qed lemma atype_same: assumes "stmt stm ev cd st = Normal (x, st')" and "type (accounts st ad) = Some ctype" shows "type (accounts st' ad) = Some ctype" using assms proof (induction arbitrary: st' rule: stmt.induct) case (1 e cd st) then show ?case using skip[OF 1(1)] by auto next case (2 lv ex env cd st) show ?case by (cases rule: assign[OF 2(1)]; simp add: 2(2)) next case (3 s1 s2 e cd st) show ?case proof (cases rule: comp[OF 3(3)]) case (1 st'') then show ?thesis using 3 by simp qed next case (4 ex s1 s2 e cd st) show ?case proof (cases rule: ite[OF 4(3)]) case (1 g) then show ?thesis using 4 by simp next case (2 g) then show ?thesis using 4 by (simp split: if_split_asm) qed next case (5 ex s0 e cd st) show ?case proof (cases rule: while[OF 5(3)]) case (1 g st'') then show ?thesis using 5 by simp next case (2 g) then show ?thesis using 5 by simp qed next case (6 i xe e cd st) show ?case proof (cases rule: invoke[OF 6(2)]) case (1 ct fb fp f e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g st'') then show ?thesis using 6 by simp qed next case (7 ad' i xe val e cd st) show ?case proof (cases rule: external[OF 7(3)]) case (1 adv c g ct cn fb' v t g' v' fp f e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g'' acc st'') moreover from 7(4) have "type (acc ad) = Some ctype" using transfer_type_same[OF 1(10)] by simp ultimately show ?thesis using 7(1) by simp next case (2 adv c g ct cn fb' v t g' v' acc st'') moreover from 7(4) have "type (acc ad) = Some ctype" using transfer_type_same[OF 2(9)] by simp ultimately show ?thesis using 7(2) by simp qed next case (8 ad' ex e cd st) show ?case proof (cases rule: transfer[OF 8(2)]) case (1 v t g adv c g' v' acc ct cn f st'') moreover from 8(3) have "type (acc ad) = Some ctype" using transfer_type_same[OF 1(7)] by simp ultimately show ?thesis using 8(1) by simp next case (2 v t g adv g' v' acc) moreover from 8(3) have "type (acc ad) = Some ctype" using transfer_type_same[OF 2(6)] by simp ultimately show ?thesis by simp qed next case (9 id0 tp s e\<^sub>v cd st) show ?case proof (cases rule: blockNone[OF 9(2)]) case (1 cd' mem' sck' e') then show ?thesis using 9 by simp qed next case (10 id0 tp ex' s e\<^sub>v cd st) show ?case proof (cases rule: blockSome[OF 10(2)]) case (1 v t g cd' mem' sck' e') then show ?thesis using 10 by simp qed next case (11 i xe val e cd st) show ?case proof (cases rule: new[OF 11(2)]) case (1 v t g ct cn fb e\<^sub>l cd\<^sub>l k\<^sub>l m\<^sub>l g' acc st'') moreover have "hash (address e) \contracts (accounts st (address e))\ \ ad" using 11(3) 1(2) by auto ultimately show ?thesis using 11 transfer_type_same[OF 1(6)] incrementAccountContracts_type by simp qed qed declare lexp.simps[simp del] declare stmt.simps[simp del] end subsection \A minimal cost model\ fun costs_min :: "S \ Environment \ CalldataT \ State \ Gas" where "costs_min SKIP e cd st = 0" | "costs_min (ASSIGN lv ex) e cd st = 0" | "costs_min (COMP s1 s2) e cd st = 0" | "costs_min (ITE ex s1 s2) e cd st = 0" | "costs_min (WHILE ex s0) e cd st = 1" | "costs_min (TRANSFER ad ex) e cd st = 1" | "costs_min (BLOCK ((id0, tp), ex) s) e cd st =0" | "costs_min (INVOKE _ _) e cd st = 1" | "costs_min (EXTERNAL _ _ _ _) e cd st = 1" | "costs_min (NEW _ _ _) e cd st = 1" fun costs_ex :: "E \ Environment \ CalldataT \ State \ Gas" where "costs_ex (E.INT _ _) e cd st = 0" | "costs_ex (UINT _ _) e cd st = 0" | "costs_ex (ADDRESS _) e cd st = 0" | "costs_ex (BALANCE _) e cd st = 0" | "costs_ex THIS e cd st = 0" | "costs_ex SENDER e cd st = 0" | "costs_ex VALUE e cd st = 0" | "costs_ex (TRUE) e cd st = 0" | "costs_ex (FALSE) e cd st = 0" | "costs_ex (LVAL _) e cd st = 0" | "costs_ex (PLUS _ _) e cd st = 0" | "costs_ex (MINUS _ _) e cd st = 0" | "costs_ex (EQUAL _ _) e cd st = 0" | "costs_ex (LESS _ _) e cd st = 0" | "costs_ex (AND _ _) e cd st = 0" | "costs_ex (OR _ _) e cd st = 0" | "costs_ex (NOT _) e cd st = 0" | "costs_ex (CALL _ _) e cd st = 1" | "costs_ex (ECALL _ _ _) e cd st = 1" | "costs_ex CONTRACTS e cd st = 0" global_interpretation solidity: statement_with_gas costs_ex fmempty costs_min defines stmt = "solidity.stmt" and lexp = solidity.lexp and expr = solidity.expr and ssel = solidity.ssel and rexp = solidity.rexp and msel = solidity.msel and load = solidity.load by unfold_locales auto section \Examples\ subsection \msel\ abbreviation mymemory2::MemoryT where "mymemory2 \ \mapping = fmap_of_list [(STR ''3.2'', MPointer STR ''5'')], toploc = 1\" -(* - FIXME - lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT 8 3] eempty emptyStore (mystate\gas:=1\) 1 -= Normal ((STR ''3.2'', MTArray 6 (MTValue TBool)), 1)" by Solidity_Symbex.solidity_symbex += Normal ((STR ''3.2'', MTArray 6 (MTValue TBool)), 1)" by Solidity_Symbex.solidity_symbex lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT 8 3, UINT 8 4] eempty emptyStore (mystate\gas:=1,memory:=mymemory2\) 1 -= Normal ((STR ''4.5'', MTValue TBool), 2)" by Solidity_Symbex.solidity_symbex -*) += Normal ((STR ''4.5'', MTValue TBool), 1)" by Solidity_Symbex.solidity_symbex lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT 8 5] eempty emptyStore (mystate\gas:=1,memory:=mymemory2\) 1 = Exception (Err)" by Solidity_Symbex.solidity_symbex end