diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,520 +1,521 @@ AODV Auto2_HOL Auto2_Imperative_HOL AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS AutoFocus-Stream Automatic_Refinement AxiomaticCategoryTheory BDD BNF_Operations Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BNF_CC Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK 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 Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Completeness Complete_Non_Orders Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series Discrete_Summation DiscretePricing DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Factored_Transition_System_Bounding Farkas FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Falling_Factorial_Sum FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite_Automata_HF First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover GPU_Kernel_PL Gabow_SCC Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interval_Arithmetic_Word32 Iptables_Semantics Irrationality_J_Hancl Isabelle_C Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_to_DRA LTL_to_GBA LTL_Master_Theorem Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_KBOs Lambda_Free_RPOs Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Lambda_Free_EPO Launchbury Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option 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 Lowe_Ontological_Argument Lower_Semicontinuous Lp MFMC_Countable MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mersenne_Primes MFOTL_Monitor MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multirelations Multi_Party_Computation Myhill-Nerode Name_Carrying_Type_Inference Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions Open_Induction OpSets Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinals_and_Cardinals Ordinary_Differential_Equations PCF PLM Pell POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Perfect-Number-Thm Perron_Frobenius Pi_Calculus Pi_Transcendental Planarity_Certificates Polynomial_Factorization Polynomial_Interpolation Polynomials Poincare_Bendixson Poincare_Disc Pop_Refinement Posix-Lexing Possibilistic_Noninterference Pratt_Certificate 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 Projective_Geometry Program-Conflict-Analysis Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Randomised_BSTs Random_Graph_Subgraph_Threshold Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Root_Balanced_Tree Routing Roy_Floyd_Warshall Safe_OCL SATSolverVerification SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts 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 Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Universal_Turing_Machine UPF UPF_Firewall UpDown_Scheme UTP Valuation VectorSpace +VeriComp Verified-Prover VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML Zeta_Function Zeta_3_Irrational ZFC_in_HOL pGCL diff --git a/thys/VeriComp/Behaviour.thy b/thys/VeriComp/Behaviour.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Behaviour.thy @@ -0,0 +1,14 @@ +theory Behaviour + imports Main +begin + +datatype 'state behaviour = + Terminates 'state | Diverges | is_wrong: Goes_wrong 'state + +text \ +Terminating behaviours are annotated with the last state of the execution in order to compare the result of two executions with the @{const rel_behaviour} relation. + +The exact meaning of the three behaviours is defined in the semantics locale +\ + +end \ No newline at end of file diff --git a/thys/VeriComp/Compiler.thy b/thys/VeriComp/Compiler.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Compiler.thy @@ -0,0 +1,154 @@ +section \Compiler Between Static Representations\ + +theory Compiler + imports Language Simulation +begin + +definition option_comp :: "('a \ 'b option) \ ('c \ 'a option) \ 'c \ 'b option" (infix "\" 50) where + "(f \ g) x \ Option.bind (g x) f" + +context + fixes f :: "('a \ 'a option)" +begin + +fun option_comp_pow :: "nat \ 'a \ 'a option" where + "option_comp_pow 0 = (\_. None)" | + "option_comp_pow (Suc 0) = f" | + "option_comp_pow (Suc n) = (option_comp_pow n \ f)" + +end + +locale compiler = + L1: language step1 final1 load1 + + L2: language step2 final2 load2 + + backward_simulation step1 step2 final1 final2 order match + for + step1 and step2 and + final1 and final2 and + load1 :: "'prog1 \ 'state1 option" and + load2 :: "'prog2 \ 'state2 option" and + order :: "'index \ 'index \ bool" and + match + + fixes + compile :: "'prog1 \ 'prog2 option" + assumes + compile_load: + "compile p1 = Some p2 \ load1 p1 = Some s1 \ \s2 i. load2 p2 = Some s2 \ match i s1 s2" +begin + +text \ +The @{locale compiler} locale relates two languages, L1 and L2, by a backward simulation and provides a @{term compile} partial function from a concrete program in L1 to a concrete program in L2. +The only assumption is that a successful compilation results in a program which, when loaded, is equivalent to the loaded initial program. +\ + + +subsection \Preservation of behaviour\ + +corollary behaviour_preservation: + assumes + compiles: "compile p1 = Some p2" and + loads: "load1 p1 = Some s1" "load2 p2 = Some s2" and + behaves: "L2.behaves s2 b2" and + not_wrong: "\ is_wrong b2" + shows "\b1 i. L1.behaves s1 b1 \ rel_behaviour (match i) b1 b2" +proof - + obtain i where "match i s1 s2" + using compile_load[OF compiles] loads by auto + then show ?thesis + using simulation_behaviour[OF behaves not_wrong] + by simp +qed + +end + +subsection \Composition of compilers\ + +lemma compiler_composition: + assumes + "compiler step1 step2 final1 final2 load1 load2 order1 match1 compile1" and + "compiler step2 step3 final2 final3 load2 load3 order2 match2 compile2" + shows "compiler step1 step3 final1 final3 load1 load3 + (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2) (compile2 \ compile1)" +proof (rule compiler.intro) + show "language step1 final1" + using assms(1)[THEN compiler.axioms(1)] . +next + show "language step3 final3" + using assms(2)[THEN compiler.axioms(2)] . +next + show "backward_simulation step1 step3 final1 final3 + (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2)" + using backward_simulation_composition[OF assms[THEN compiler.axioms(3)]] . +next + show "compiler_axioms load1 load3 (rel_comp match1 match2) (compile2 \ compile1)" + proof unfold_locales + fix p1 p3 s1 + assume + compile: "(compile2 \ compile1) p1 = Some p3" and + load: "load1 p1 = Some s1" + obtain p2 where "compile1 p1 = Some p2" and "compile2 p2 = Some p3" + using compile by (auto simp: bind_eq_Some_conv option_comp_def) + then obtain s2 i where "load2 p2 = Some s2" and "match1 i s1 s2" + using assms(1)[THEN compiler.compile_load] load + by blast + moreover obtain s3 i' where "load3 p3 = Some s3" and "match2 i' s2 s3" + using assms(2)[THEN compiler.compile_load, OF \compile2 p2 = Some p3\ \load2 p2 = Some s2\] + by auto + ultimately show "\s3 i. load3 p3 = Some s3 \ rel_comp match1 match2 i s1 s3" + unfolding rel_comp_def by auto + qed +qed + +lemma compiler_composition_pow: + assumes + "compiler step step final final load load order match compile" + shows "compiler step step final final load load + (lexp order\<^sup>+\<^sup>+) (rel_comp_pow match) (option_comp_pow compile n)" +proof (induction n rule: option_comp_pow.induct) + case 1 + show ?case + using assms + by (auto intro: compiler.axioms compiler.intro compiler_axioms.intro backward_simulation_pow) +next + case 2 + show ?case + proof (rule compiler.intro) + show "compiler_axioms load load (rel_comp_pow match) (option_comp_pow compile (Suc 0))" + proof unfold_locales + fix p1 p2 s1 + assume + "option_comp_pow compile (Suc 0) p1 = Some p2" and + "load p1 = Some s1" + thus "\s2 i. load p2 = Some s2 \ rel_comp_pow match i s1 s2" + using compiler.compile_load[OF assms(1)] + by (metis option_comp_pow.simps(2) rel_comp_pow.simps(2)) + qed + qed (auto intro: assms compiler.axioms backward_simulation_pow) +next + case (3 n') + show ?case + proof (rule compiler.intro) + show "compiler_axioms load load (rel_comp_pow match) (option_comp_pow compile (Suc (Suc n')))" + proof unfold_locales + fix p1 p3 s1 + assume + "option_comp_pow compile (Suc (Suc n')) p1 = Some p3" and + "load p1 = Some s1" + then obtain p2 where + comp: "compile p1 = Some p2" and + comp_IH: "option_comp_pow compile (Suc n') p2 = Some p3" + by (auto simp: option_comp_def bind_eq_Some_conv) + then obtain s2 i where "load p2 = Some s2" and "match i s1 s2" + using compiler.compile_load[OF assms(1) _ \load p1 = Some s1\] by blast + then obtain s3 i' where "load p3 = Some s3" and "rel_comp_pow match i' s2 s3" + using compiler.compile_load[OF "3.IH" comp_IH] by blast + moreover have "rel_comp_pow match (i # i') s1 s3" + using \match i s1 s2\ \rel_comp_pow match i' s2 s3\ + using rel_comp_pow.elims(2) by fastforce + ultimately show "\s3 i. load p3 = Some s3 \ rel_comp_pow match i s1 s3" + by auto + qed + qed (auto intro: assms compiler.axioms backward_simulation_pow) +qed + +end \ No newline at end of file diff --git a/thys/VeriComp/Fixpoint.thy b/thys/VeriComp/Fixpoint.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Fixpoint.thy @@ -0,0 +1,84 @@ +section \Fixpoint of Converging Program Transformations\ + +theory Fixpoint + imports Compiler +begin + +context + fixes + m :: "'a \ nat" and + f :: "'a \ 'a option" +begin + +function fixpoint :: "'a \ 'a option" where + "fixpoint x = ( + case f x of + None \ None | + Some x' \ if m x' < m x then fixpoint x' else Some x' + )" +by pat_completeness auto +termination +proof (relation "measure m") + show "wf (measure m)" by auto +next + fix x x' + assume "f x = Some x'" and "m x' < m x" + thus "(x', x) \ measure m" by simp +qed + +end + +lemma fixpoint_to_comp_pow: + "fixpoint m f x = y \ \n. option_comp_pow f n x = y" +proof (induction x arbitrary: y rule: fixpoint.induct[where f = f and m = m]) + case (1 x) + show ?case + proof (cases "f x") + case None + then show ?thesis + using "1.prems" + by (metis (no_types, lifting) fixpoint.simps option.case_eq_if option_comp_pow.simps(1)) + next + case (Some a) + show ?thesis + proof (cases "m a < m x") + case True + hence "fixpoint m f a = y" + using "1.prems" Some by simp + then show ?thesis + using "1.IH"[OF Some True] + by (metis Some bind.simps(2) old.nat.exhaust option_comp_def option_comp_pow.simps(1,3)) + next + case False + then show ?thesis + using "1.prems" Some + apply simp + by (metis option_comp_pow.simps(2)) + qed + qed +qed + +lemma fixpoint_eq_comp_pow: + "\n. fixpoint m f x = option_comp_pow f n x" + by (metis fixpoint_to_comp_pow) + +lemma compiler_composition_fixpoint: + assumes + "compiler step step final final load load order match compile" + shows "compiler step step final final load load + (lexp order\<^sup>+\<^sup>+) (rel_comp_pow match) (fixpoint m compile)" +proof (rule compiler.intro) + show "compiler_axioms load load (rel_comp_pow match) (fixpoint m compile)" + proof unfold_locales + fix p1 p2 s1 + assume "fixpoint m compile p1 = Some p2" and "load p1 = Some s1" + obtain n where "fixpoint m compile p1 = option_comp_pow compile n p1" + using fixpoint_eq_comp_pow by metis + + thus "\s2 i. load p2 = Some s2 \ rel_comp_pow match i s1 s2" + using \fixpoint m compile p1 = Some p2\ assms compiler.compile_load compiler_composition_pow + using \load p1 = Some s1\ by fastforce + qed +qed (auto intro: assms compiler.axioms backward_simulation_pow) + +end diff --git a/thys/VeriComp/Inf.thy b/thys/VeriComp/Inf.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Inf.thy @@ -0,0 +1,59 @@ +section \Infinitely Transitive Closure\ + +theory Inf + imports Well_founded +begin + +coinductive inf :: "('a \ 'a \ bool) \ 'a \ bool" for r where + inf_step: "r x y \ inf r y \ inf r x" + +coinductive inf_wf :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ 'b \ 'a \ bool" for r order where + inf_wf: "order n m \ inf_wf r order n x \ inf_wf r order m x" | + inf_wf_step: "r\<^sup>+\<^sup>+ x y \ inf_wf r order n y \ inf_wf r order m x" + +lemma inf_wf_to_step_inf_wf: + assumes "well_founded order" + shows "inf_wf r order n x \ \y m. r x y \ inf_wf r order m y" +proof (induction n arbitrary: x rule: well_founded.induct[OF assms(1)]) + case (1 n) + from "1.prems"(1) show ?case + proof (induction rule: inf_wf.cases) + case (inf_wf m n' x') + then show ?case using "1.IH" by simp + next + case (inf_wf_step x' y m n') + then show ?case + by (metis converse_tranclpE inf_wf.inf_wf_step) + qed +qed + +lemma inf_wf_to_inf: + assumes "well_founded order" + shows "inf_wf r order n x \ inf r x" +proof (coinduction arbitrary: x n rule: inf.coinduct) + case (inf x n) + then obtain y m where "r x y" and "inf_wf r order m y" + using inf_wf_to_step_inf_wf[OF assms(1) inf(1)] by metis + thus ?case by auto +qed + +lemma step_inf: + assumes + deterministic: "\x y z. r x y \ r x z \ y = z" + shows "r x y \ inf r x \ inf r y" + by (metis deterministic inf.cases) + +lemma star_inf: + assumes + deterministic: "\x y z. r x y \ r x z \ y = z" + shows "r\<^sup>*\<^sup>* x y \ inf r x \ inf r y" +proof (induction y rule: rtranclp_induct) + case base + then show ?case . +next + case (step y z) + then show ?case + using step_inf deterministic by metis +qed + +end \ No newline at end of file diff --git a/thys/VeriComp/LICENSE.txt b/thys/VeriComp/LICENSE.txt new file mode 100644 --- /dev/null +++ b/thys/VeriComp/LICENSE.txt @@ -0,0 +1,21 @@ +MIT License + +Copyright 2019 Martin Desharnais + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies +of the Software, and to permit persons to whom the Software is furnished to do +so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/thys/VeriComp/Language.thy b/thys/VeriComp/Language.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Language.thy @@ -0,0 +1,24 @@ +section \The Static Representation of a Language\ + +theory Language + imports Semantics +begin + +locale language = + semantics step final + for + step :: "'state \ 'state \ bool" and + final :: "'state \ bool" + + fixes + load :: "'prog \ 'state option" + +context language begin + +text \ +The language locale represents the concrete program representation (type variable @{typ 'prog}), which can be transformed into a program state (type variable @{typ 'state}) by the @{term load } function. +The set of initial states of the transition system is implicitly defined by the codomain of @{term load}. +\ + +end + +end \ No newline at end of file diff --git a/thys/VeriComp/ROOT b/thys/VeriComp/ROOT new file mode 100644 --- /dev/null +++ b/thys/VeriComp/ROOT @@ -0,0 +1,9 @@ +chapter AFP +session VeriComp (AFP) = HOL + + options [timeout = 600] + theories + Compiler + Fixpoint + document_files + "root.bib" + "root.tex" diff --git a/thys/VeriComp/Semantics.thy b/thys/VeriComp/Semantics.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Semantics.thy @@ -0,0 +1,138 @@ +section \The Dynamic Representation of a Language\ + +theory Semantics + imports Main Behaviour Inf begin + +text \ +The definition of programming languages is separated into two parts: an abstract semantics and a concrete program representation. +\ + +definition finished :: "('a \ 'a \ bool) \ 'a \ bool" where + "finished r x = (\y. r x y)" + +lemma finished_star: + assumes "finished r x" + shows "r\<^sup>*\<^sup>* x y \ x = y" +proof (induction y rule: rtranclp_induct) + case base + then show ?case by simp +next + case (step y z) + then show ?case + using assms by (auto simp: finished_def) +qed + +locale semantics = + fixes + step :: "'state \ 'state \ bool" (infix "\" 50) and + final :: "'state \ bool" + assumes + final_finished: "final s \ finished step s" +begin + +text \ +The semantics locale represents the semantics as an abstract machine. +It is expressed by a transition system with a transition relation @{term step}---usually written as an infix @{text \} arrow---and final states @{term final}. +\ + +lemma finished_step: + "step s s' \ \finished step s" +by (auto simp add: finished_def) + +abbreviation eval :: "'state \ 'state \ bool" (infix "\\<^sup>*" 50) where + "eval \ step\<^sup>*\<^sup>*" + +abbreviation inf_step :: "'state \ bool" where + "inf_step \ inf step" + +notation + inf_step ("'(\\<^sup>\')" [] 50) and + inf_step ("_ \\<^sup>\" [55] 50) + +lemma finished_inf: "s \\<^sup>\ \ \ finished step s" + using inf.cases finished_step by metis + +lemma eval_deterministic: + assumes + deterministic: "\x y z. step x y \ step x z \ y = z" + shows "s1 \\<^sup>* s2 \ s1 \\<^sup>* s3 \ finished step s2 \ finished step s3 \ s2 = s3" +proof(induction s1 arbitrary: s3 rule: converse_rtranclp_induct) + case base + then show ?case by (simp add: finished_star) +next + case (step y z) + then show ?case + by (metis converse_rtranclpE deterministic finished_step) +qed + +subsection \Behaviour of a dynamic execution\ + +inductive behaves :: "'state \ 'state behaviour \ bool" (infix "\" 50) where + state_terminates: + "s1 \\<^sup>* s2 \ finished step s2 \ final s2 \ s1 \ (Terminates s2)" | + state_diverges: + "s1 \\<^sup>\ \ s1 \ Diverges" | + state_goes_wrong: + "s1 \\<^sup>* s2 \ finished step s2 \ \ final s2 \ s1 \ (Goes_wrong s2)" + + +text \ +Even though the @{term step} transition relation in the @{locale semantics} locale need not be deterministic, if it happens to be, then the behaviour of a program becomes deterministic too. +\ + +lemma behaves_deterministic: + assumes + deterministic: "\x y z. step x y \ step x z \ y = z" + shows "s \ b1 \ s \ b2 \ b1 = b2" +proof (induction s b1 rule: behaves.induct) + case (state_terminates s1 s2) + show ?case using state_terminates.prems state_terminates.hyps + proof (induction s1 b2 rule: behaves.induct) + case (state_terminates s1 s3) + then show ?case + using eval_deterministic deterministic by simp + next + case (state_diverges s1) + then show ?case + using deterministic star_inf[THEN finished_inf] by simp + next + case (state_goes_wrong s1 s3) + then show ?case + using eval_deterministic deterministic by blast + qed +next + case (state_diverges s1) + show ?case using state_diverges.prems state_diverges.hyps + proof (induction s1 b2 rule: behaves.induct) + case (state_terminates s1 s2) + then show ?case + using deterministic star_inf[THEN finished_inf] by simp + next + case (state_diverges s1) + then show ?case by simp + next + case (state_goes_wrong s1 s2) + then show ?case + using deterministic star_inf[THEN finished_inf] by simp + qed +next + case (state_goes_wrong s1 s2) + show ?case using state_goes_wrong.prems state_goes_wrong.hyps + proof (induction s1 b2) + case (state_terminates s1 s3) + then show ?case + using eval_deterministic deterministic by blast + next + case (state_diverges s1) + then show ?case + using deterministic star_inf[THEN finished_inf] by simp + next + case (state_goes_wrong s1 s3) + then show ?case + using eval_deterministic deterministic by simp + qed +qed + +end + +end \ No newline at end of file diff --git a/thys/VeriComp/Simulation.thy b/thys/VeriComp/Simulation.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Simulation.thy @@ -0,0 +1,445 @@ +section \Simulations Between Dynamic Executions\ + +theory Simulation + imports Semantics Inf Well_founded +begin + +locale backward_simulation = + L1: semantics step1 final1 + + L2: semantics step2 final2 + + well_founded "(\)" + for + step1 :: "'state1 \ 'state1 \ bool" and + step2 :: "'state2 \ 'state2 \ bool" and + final1 :: "'state1 \ bool" and + final2 :: "'state2 \ bool" and + order :: "'index \ 'index \ bool" (infix "\" 70) + + fixes + match :: "'index \ 'state1 \ 'state2 \ bool" + assumes + match_final: + "match i s1 s2 \ final2 s2 \ final1 s1" and + simulation: + "match i1 s1 s2 \ step2 s2 s2' \ + (\i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match i2 s1' s2') \ (\i2. match i2 s1 s2' \ i2 \ i1)" +begin + +text \ +A simulation is defined between two @{locale semantics} L1 and L2. +A @{term match} predicate expresses that two states from L1 and L2 are equivalent. +The @{term match} predicate is also parameterized with an ordering used to avoid stuttering. +The only two assumptions of a backward simulation are that a final state in L2 will also be a final in L1,and that a step in L2 will either represent a non-empty sequence of steps in L1 or will result in an equivalent state. +Stuttering is ruled out by the requirement that the index on the @{term match} predicate decreases with respect to the well-founded @{term order} ordering. +\ + +end + + +locale forward_simulation = + L1: semantics step1 final1 + + L2: semantics step2 final2 + + well_founded "(\)" + for + step1 :: "'state1 \ 'state1 \ bool" and + step2 :: "'state2 \ 'state2 \ bool" and + final1 :: "'state1 \ bool" and + final2 :: "'state2 \ bool" and + order :: "'index \ 'index \ bool" (infix "\" 70) + + fixes + match :: "'index \ 'state1 \ 'state2 \ bool" + assumes + match_final: + "match i s1 s2 \ final1 s1 \ final2 s2" and + simulation: + "match i1 s1 s2 \ step1 s1 s1' \ + (\i' s2'. step2\<^sup>+\<^sup>+ s2 s2' \ match i' s1' s2') \ (\i'. match i' s1 s2' \ i' \ i1)" + +locale bisimulation = + forward_simulation step1 step2 final1 final2 order match + + backward_simulation step1 step2 final1 final2 order match + for + step1 :: "'state1 \ 'state1 \ bool" and + step2 :: "'state2 \ 'state2 \ bool" and + final1 :: "'state1 \ bool" and + final2 :: "'state2 \ bool" and + order :: "'index \ 'index \ bool" and + match :: "'index \ 'state1 \ 'state2 \ bool" + +context backward_simulation begin + +lemma lift_simulation_plus: + "step2\<^sup>+\<^sup>+ s2 s2' \ match i1 s1 s2 \ + (\i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match i2 s1' s2') \ + (\i2. match i2 s1 s2' \ order\<^sup>+\<^sup>+ i2 i1)" + thm tranclp_induct +proof(induction s2' arbitrary: i1 s1 rule: tranclp_induct) + case (base s2') + from simulation[OF base.prems(1) base.hyps(1)] show ?case + by auto +next + case (step s2' s2'') + show ?case + using step.IH[OF \match i1 s1 s2\] + proof + assume "\i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match i2 s1' s2'" + then obtain i2 s1' where "step1\<^sup>+\<^sup>+ s1 s1'" and "match i2 s1' s2'" by auto + from simulation[OF \match i2 s1' s2'\ \step2 s2' s2''\] show ?thesis + proof + assume "\i3 s1''. step1\<^sup>+\<^sup>+ s1' s1'' \ match i3 s1'' s2''" + then obtain i3 s1'' where "step1\<^sup>+\<^sup>+ s1' s1''" and "match i3 s1'' s2''" by auto + then show ?thesis + using tranclp_trans[OF \step1\<^sup>+\<^sup>+ s1 s1'\] by auto + next + assume "\i3. match i3 s1' s2'' \ i3 \ i2" + then obtain i3 where "match i3 s1' s2''" and "i3 \ i2" by auto + then show ?thesis + using \step1\<^sup>+\<^sup>+ s1 s1'\ by auto + qed + next + assume "\i2. match i2 s1 s2' \ (\)\<^sup>+\<^sup>+ i2 i1" + then obtain i3 where "match i3 s1 s2'" and "(\)\<^sup>+\<^sup>+ i3 i1" by auto + then show ?thesis + using simulation[OF \match i3 s1 s2'\ \step2 s2' s2''\] by auto + qed +qed + +lemma lift_simulation_eval: + "L2.eval s2 s2' \ match i1 s1 s2 \ \i2 s1'. L1.eval s1 s1' \ match i2 s1' s2'" +proof(induction s2 arbitrary: i1 s1 rule: converse_rtranclp_induct) + case (base s2) + thus ?case by auto +next + case (step s2 s2'') + from simulation[OF \match i1 s1 s2\ \step2 s2 s2''\] show ?case + proof + assume "\i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match i2 s1' s2''" + thus ?thesis + by (meson rtranclp_trans step.IH tranclp_into_rtranclp) + next + assume "\i2. match i2 s1 s2'' \ i2 \ i1" + thus ?thesis + by (auto intro: step.IH) + qed +qed + +lemma backward_simulation_inf: + assumes + "match i s1 s2" and + "inf step2 s2" + shows "inf step1 s1" +proof - + from assms have "inf_wf step1 order i s1" + proof (coinduction arbitrary: i s1 s2) + case inf_wf + obtain s2' where "step2 s2 s2'" and "inf step2 s2'" + using inf_wf(2) by (auto elim: inf.cases) + from simulation[OF \match i s1 s2\ \step2 s2 s2'\] show ?case + using \inf step2 s2'\ by auto + qed + thus ?thesis using inf_wf_to_inf + by (auto intro: inf_wf_to_inf well_founded_axioms) +qed + +subsection \Preservation of behaviour\ + +text \ +The main correctness theorem states that, for any two matching programs, any not wrong behaviour of the later is also a behaviour of the former. +In other words, if the compiled program does not crash, then its behaviour, whether it terminates or not, is a also a valid behaviour of the source program. +\ + +lemma simulation_behaviour : + "L2.behaves s\<^sub>2 b\<^sub>2 \ \is_wrong b\<^sub>2 \ match i s\<^sub>1 s\<^sub>2 \ + \b\<^sub>1 i'. L1.behaves s\<^sub>1 b\<^sub>1 \ rel_behaviour (match i') b\<^sub>1 b\<^sub>2" +proof(induction rule: L2.behaves.cases) + case (state_terminates s2 s2') + then obtain i' s1' where "L1.eval s\<^sub>1 s1'" and "match i' s1' s2'" + using lift_simulation_eval by blast + hence "final1 s1'" + by (auto intro: state_terminates.hyps match_final) + hence "L1.behaves s\<^sub>1 (Terminates s1')" + using L1.final_finished + by (simp add: L1.state_terminates \L1.eval s\<^sub>1 s1'\) + moreover have "rel_behaviour (match i') (Terminates s1') b\<^sub>2" + by (simp add: \match i' s1' s2'\ state_terminates.hyps) + ultimately show ?case by blast +next + case (state_diverges s2) + then show ?case + using backward_simulation_inf L1.state_diverges by fastforce +next + case (state_goes_wrong s2 s2') + then show ?case using \\is_wrong b\<^sub>2\ by simp +qed + +end + +subsection \Composition of backward simulations\ + +definition rel_comp :: + "('a \ 'b \ 'c \ bool) \ ('d \ 'c \ 'e \ bool) \ ('a \ 'd) \ 'b \ 'e \ bool" where + "rel_comp r1 r2 i \ (r1 (fst i) OO r2 (snd i))" + +lemma backward_simulation_composition: + assumes + "backward_simulation step1 step2 final1 final2 order1 match1" + "backward_simulation step2 step3 final2 final3 order2 match2" + shows + "backward_simulation step1 step3 final1 final3 + (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2)" +proof intro_locales + show "semantics step1 final1" + by (auto intro: backward_simulation.axioms assms) +next + show "semantics step3 final3" + by (auto intro: backward_simulation.axioms assms) +next + show "well_founded (lex_prodp order1\<^sup>+\<^sup>+ order2)" + using assms[THEN backward_simulation.axioms(3)] + by (simp add: lex_prodp_well_founded well_founded.intro well_founded.wf wfP_trancl) +next + show "backward_simulation_axioms step1 step3 final1 final3 + (lex_prodp order1\<^sup>+\<^sup>+ order2) (rel_comp match1 match2)" + proof + fix i s1 s3 + assume + match: "rel_comp match1 match2 i s1 s3" and + final: "final3 s3" + obtain i1 i2 s2 where "match1 i1 s1 s2" and "match2 i2 s2 s3" and "i = (i1, i2)" + using match unfolding rel_comp_def by auto + thus "final1 s1" + using final assms[THEN backward_simulation.match_final] + by simp + next + fix i s1 s3 s3' + assume + match: "rel_comp match1 match2 i s1 s3" and + step: "step3 s3 s3'" + obtain i1 i2 s2 where "match1 i1 s1 s2" and "match2 i2 s2 s3" and i_def: "i = (i1, i2)" + using match unfolding rel_comp_def by auto + from backward_simulation.simulation[OF assms(2) \match2 i2 s2 s3\ step] + show "(\i' s1'. step1\<^sup>+\<^sup>+ s1 s1' \ rel_comp match1 match2 i' s1' s3') \ + (\i'. rel_comp match1 match2 i' s1 s3' \ lex_prodp order1\<^sup>+\<^sup>+ order2 i' i)" + (is "(\i' s1'. ?STEPS i' s1') \ ?STALL") + proof + assume "\i2' s2'. step2\<^sup>+\<^sup>+ s2 s2' \ match2 i2' s2' s3'" + then obtain i2' s2' where "step2\<^sup>+\<^sup>+ s2 s2'" and "match2 i2' s2' s3'" by auto + from backward_simulation.lift_simulation_plus[OF assms(1) \step2\<^sup>+\<^sup>+ s2 s2'\ \match1 i1 s1 s2\] + show ?thesis + proof + assume "\i2 s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match1 i2 s1' s2'" + then obtain i2 s1' where "step1\<^sup>+\<^sup>+ s1 s1'" and "match1 i2 s1' s2'" by auto + hence "?STEPS (i2, i2') s1'" + by (auto intro: \match2 i2' s2' s3'\ simp: rel_comp_def) + thus ?thesis by auto + next + assume "\i2. match1 i2 s1 s2' \ order1\<^sup>+\<^sup>+ i2 i1" + then obtain i2'' where "match1 i2'' s1 s2'" and "order1\<^sup>+\<^sup>+ i2'' i1" by auto + hence ?STALL + unfolding rel_comp_def i_def lex_prodp_def + using \match2 i2' s2' s3'\ by auto + thus ?thesis by simp + qed + next + assume "\i2'. match2 i2' s2 s3' \ order2 i2' i2" + then obtain i2' where "match2 i2' s2 s3'" and "order2 i2' i2" by auto + hence ?STALL + unfolding rel_comp_def i_def lex_prodp_def + using \match1 i1 s1 s2\ by auto + thus ?thesis by simp + qed + qed +qed + +context + fixes r :: "'i \ 'a \ 'a \ bool" +begin + +fun rel_comp_pow where + "rel_comp_pow [] x y = False" | + "rel_comp_pow [i] x y = r i x y" | + "rel_comp_pow (i # is) x z = (\y. r i x y \ rel_comp_pow is y z)" + +end + +lemma backward_simulation_pow: + assumes + "backward_simulation step step final final order match" + shows + "backward_simulation step step final final (lexp order\<^sup>+\<^sup>+) (rel_comp_pow match)" +proof intro_locales + show "semantics step final" + by (auto intro: backward_simulation.axioms assms) +next + show "well_founded (lexp order\<^sup>+\<^sup>+)" + using backward_simulation.axioms(3)[OF assms] lex_list_well_founded + using well_founded.intro well_founded.wf wfP_trancl by blast +next + show "backward_simulation_axioms step step final final (lexp order\<^sup>+\<^sup>+) (rel_comp_pow match)" + proof unfold_locales + fix "is" s1 s2 + assume "rel_comp_pow match is s1 s2" and "final s2" + thus "final s1" thm rel_comp_pow.induct + proof (induction "is" s1 s2 rule: rel_comp_pow.induct) + case (1 x y) + then show ?case by simp + next + case (2 i x y) + then show ?case + using backward_simulation.match_final[OF assms(1)] by simp + next + case (3 i1 i2 "is" x z) + from "3.prems"[simplified] obtain y where + match: "match i1 x y" and "rel_comp_pow match (i2 # is) y z" + by auto + hence "final y" using "3.IH" "3.prems" by simp + thus ?case + using "3.prems" match backward_simulation.match_final[OF assms(1)] by auto + qed + next + fix "is" s1 s3 s3' + assume "rel_comp_pow match is s1 s3" and "step s3 s3'" + hence "(\is' s1'. step\<^sup>+\<^sup>+ s1 s1' \ length is' = length is \ rel_comp_pow match is' s1' s3') \ + (\is'. rel_comp_pow match is' s1 s3' \ lexp order\<^sup>+\<^sup>+ is' is)" + proof (induction "is" s1 s3 arbitrary: s3' rule: rel_comp_pow.induct) + case 1 + then show ?case by simp + next + case (2 i s1 s3) + from backward_simulation.simulation[OF assms(1) "2.prems"[simplified]] show ?case + proof + assume "\i' s1'. step\<^sup>+\<^sup>+ s1 s1' \ match i' s1' s3'" + then obtain i' s1' where "step\<^sup>+\<^sup>+ s1 s1'" and "match i' s1' s3'" by auto + hence "step\<^sup>+\<^sup>+ s1 s1' \ rel_comp_pow match [i'] s1' s3'" by simp + thus ?thesis + by (metis length_Cons) + next + assume "\i'. match i' s1 s3' \ order i' i" + then obtain i' where "match i' s1 s3'" and "order i' i" by auto + hence "rel_comp_pow match [i'] s1 s3' \ lexp order\<^sup>+\<^sup>+ [i'] [i]" + by (simp add: lexp_head tranclp.r_into_trancl) + thus ?thesis by blast + qed + next + case (3 i1 i2 "is" s1 s3) + from "3.prems"[simplified] obtain s2 where + "match i1 s1 s2" and 0: "rel_comp_pow match (i2 # is) s2 s3" + by auto + from "3.IH"[OF 0 "3.prems"(2)] show ?case + proof + assume "\is' s2'. step\<^sup>+\<^sup>+ s2 s2' \ length is' = length (i2 # is) \ + rel_comp_pow match is' s2' s3'" + then obtain i2' is' s2' where + "step\<^sup>+\<^sup>+ s2 s2'" and "length is' = length is" and "rel_comp_pow match (i2' # is') s2' s3'" + by (metis Suc_length_conv) + from backward_simulation.lift_simulation_plus[OF assms(1) \step\<^sup>+\<^sup>+ s2 s2'\ \match i1 s1 s2\] + show ?thesis + proof + assume "\i2 s1'. step\<^sup>+\<^sup>+ s1 s1' \ match i2 s1' s2'" + thus ?thesis + using \rel_comp_pow match (i2' # is') s2' s3'\ + by (metis \length is' = length is\ length_Cons rel_comp_pow.simps(3)) + next + assume "\i2. match i2 s1 s2' \ order\<^sup>+\<^sup>+ i2 i1" + then obtain i1' where "match i1' s1 s2'" and "order\<^sup>+\<^sup>+ i1' i1" by auto + hence "rel_comp_pow match (i1' # i2' # is') s1 s3'" + using \rel_comp_pow match (i2' # is') s2' s3'\ by auto + moreover have "lexp order\<^sup>+\<^sup>+ (i1' # i2' # is') (i1 # i2 # is)" + using \order\<^sup>+\<^sup>+ i1' i1\ \length is' = length is\ + by (auto intro: lexp_head) + ultimately show ?thesis by fast + qed + next + assume "\i'. rel_comp_pow match i' s2 s3' \ lexp order\<^sup>+\<^sup>+ i' (i2 # is)" + then obtain i2' is' where + "rel_comp_pow match (i2' # is') s2 s3'" and "lexp order\<^sup>+\<^sup>+ (i2' # is') (i2 # is)" + by (metis lexp.simps) + thus ?thesis + by (metis \match i1 s1 s2\ lexp.simps(1) rel_comp_pow.simps(3)) + qed + qed + thus "(\is' s1'. step\<^sup>+\<^sup>+ s1 s1' \ rel_comp_pow match is' s1' s3') \ + (\is'. rel_comp_pow match is' s1 s3' \ lexp order\<^sup>+\<^sup>+ is' is)" + by auto + qed +qed + +definition lockstep_backward_simulation where + "lockstep_backward_simulation step1 step2 match \ + \s1 s2 s2'. match s1 s2 \ step2 s2 s2' \ (\s1'. step1 s1 s1' \ match s1' s2')" + +definition plus_backward_simulation where + "plus_backward_simulation step1 step2 match \ + \s1 s2 s2'. match s1 s2 \ step2 s2 s2' \ (\s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match s1' s2')" + +lemma + assumes "lockstep_backward_simulation step1 step2 match" + shows "plus_backward_simulation step1 step2 match" +unfolding plus_backward_simulation_def +proof safe + fix s1 s2 s2' + assume "match s1 s2" and "step2 s2 s2'" + then obtain s1' where "step1 s1 s1'" and "match s1' s2'" + using assms(1) unfolding lockstep_backward_simulation_def by blast + then show "\s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match s1' s2'" + by auto +qed + +lemma lockstep_to_plus_backward_simulation: + fixes + match :: "'state1 \ 'state2 \ bool" and + step1 :: "'state1 \ 'state1 \ bool" and + step2 :: "'state2 \ 'state2 \ bool" + assumes + lockstep_simulation: "\s1 s2 s2'. match s1 s2 \ step2 s2 s2' \ (\s1'. step1 s1 s1' \ match s1' s2')" and + match: "match s1 s2" and + step: "step2 s2 s2'" + shows "\s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match s1' s2'" +proof - + obtain s1' where "step1 s1 s1'" and "match s1' s2'" + using lockstep_simulation[OF match step] by auto + thus ?thesis by auto +qed + +lemma lockstep_to_option_backward_simulation: + fixes + match :: "'state1 \ 'state2 \ bool" and + step1 :: "'state1 \ 'state1 \ bool" and + step2 :: "'state2 \ 'state2 \ bool" and + measure :: "'state2 \ nat" + assumes + lockstep_simulation: "\s1 s2 s2'. match s1 s2 \ step2 s2 s2' \ (\s1'. step1 s1 s1' \ match s1' s2')" and + match: "match s1 s2" and + step: "step2 s2 s2'" + shows "(\s1'. step1 s1 s1' \ match s1' s2') \ match s1 s2' \ measure s2' < measure s2" + using lockstep_simulation[OF match step] .. + +lemma plus_to_star_backward_simulation: + fixes + match :: "'state1 \ 'state2 \ bool" and + step1 :: "'state1 \ 'state1 \ bool" and + step2 :: "'state2 \ 'state2 \ bool" and + measure :: "'state2 \ nat" + assumes + star_simulation: "\s1 s2 s2'. match s1 s2 \ step2 s2 s2' \ (\s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match s1' s2')" and + match: "match s1 s2" and + step: "step2 s2 s2'" + shows "(\s1'. step1\<^sup>+\<^sup>+ s1 s1' \ match s1' s2') \ match s1 s2' \ measure s2' < measure s2" + using star_simulation[OF match step] .. + +lemma lockstep_to_plus_forward_simulation: + fixes + match :: "'state1 \ 'state2 \ bool" and + step1 :: "'state1 \ 'state1 \ bool" and + step2 :: "'state2 \ 'state2 \ bool" + assumes + lockstep_simulation: "\s1 s2 s2'. match s1 s2 \ step1 s1 s1' \ (\s2'. step2 s2 s2' \ match s1' s2')" and + match: "match s1 s2" and + step: "step1 s1 s1'" + shows "\s2'. step2\<^sup>+\<^sup>+ s2 s2' \ match s1' s2'" +proof - + obtain s2' where "step2 s2 s2'" and "match s1' s2'" + using lockstep_simulation[OF match step] by auto + thus ?thesis by auto +qed + +end \ No newline at end of file diff --git a/thys/VeriComp/Well_founded.thy b/thys/VeriComp/Well_founded.thy new file mode 100644 --- /dev/null +++ b/thys/VeriComp/Well_founded.thy @@ -0,0 +1,99 @@ +section \Well-foundedness of Relations Defined as Predicate Functions\ + +theory Well_founded + imports Main +begin + +locale well_founded = + fixes R :: "'a \ 'a \ bool" (infix "\" 70) + assumes + wf: "wfP (\)" +begin + +lemmas induct = wfP_induct_rule[OF wf] + +end + +subsection \Lexicographic product\ + +context + fixes + r1 :: "'a \ 'a \ bool" and + r2 :: "'b \ 'b \ bool" +begin + +definition lex_prodp :: "'a \ 'b \ 'a \ 'b \ bool" where + "lex_prodp x y \ r1 (fst x) (fst y) \ fst x = fst y \ r2 (snd x) (snd y)" + +lemma lex_prodp_lex_prod: + shows "lex_prodp x y \ (x, y) \ lex_prod { (x, y). r1 x y } { (x, y). r2 x y }" + by (auto simp: lex_prod_def lex_prodp_def) + +lemma lex_prodp_wfP: + assumes + "wfP r1" and + "wfP r2" + shows "wfP lex_prodp" +proof (rule wfPUNIVI) + show "\P. \x. (\y. lex_prodp y x \ P y) \ P x \ (\x. P x)" + proof - + fix P + assume "\x. (\y. lex_prodp y x \ P y) \ P x" + hence hyps: "(\y1 y2. lex_prodp (y1, y2) (x1, x2) \ P (y1, y2)) \ P (x1, x2)" for x1 x2 + by fast + show "(\x. P x)" + apply (simp only: split_paired_all) + apply (atomize (full)) + apply (rule allI) + apply (rule wfP_induct_rule[OF assms(1), of "\y. \b. P (y, b)"]) + apply (rule allI) + apply (rule wfP_induct_rule[OF assms(2), of "\b. P (x, b)" for x]) + using hyps[unfolded lex_prodp_def, simplified] + by blast + qed +qed + +end + +lemma lex_prodp_well_founded: + assumes + "well_founded r1" and + "well_founded r2" + shows "well_founded (lex_prodp r1 r2)" + using well_founded.intro lex_prodp_wfP assms[THEN well_founded.wf] by auto + +subsection \Lexicographic list\ + +context + fixes order :: "'a \ 'a \ bool" +begin + +inductive lexp :: "'a list \ 'a list \ bool" where + lexp_head: "order x y \ length xs = length ys \ lexp (x # xs) (y # ys)" | + lexp_tail: "lexp xs ys \ lexp (x # xs) (x # ys)" + +end + +lemma lexp_prepend: "lexp order ys zs \ lexp order (xs @ ys) (xs @ zs)" + by (induction xs) (simp_all add: lexp_tail) + +lemma lexp_lex: "lexp order xs ys \ (xs, ys) \ lex {(x, y). order x y}" +proof + assume "lexp order xs ys" + thus "(xs, ys) \ lex {(x, y). order x y}" + by (induction xs ys rule: lexp.induct) simp_all +next + assume "(xs, ys) \ lex {(x, y). order x y}" + thus "lexp order xs ys" + by (auto intro!: lexp_prepend intro: lexp_head simp: lex_conv) +qed + +lemma lex_list_wfP: "wfP order \ wfP (lexp order)" + by (simp add: lexp_lex wf_lex wfP_def) + +lemma lex_list_well_founded: + assumes "well_founded order" + shows "well_founded (lexp order)" + using well_founded.intro assms(1)[THEN well_founded.wf, THEN lex_list_wfP] by auto + +end \ No newline at end of file diff --git a/thys/VeriComp/document/root.bib b/thys/VeriComp/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/VeriComp/document/root.bib @@ -0,0 +1,8 @@ +@article{desharnais-jfla2020, + title={A Generic Framework for Verified Compilers Using {I}sabelle/{HOL}’s Locales}, + author={Desharnais, Martin and Brunthaler, Stefan}, + journal={31 {\`e}me Journ{\'e}es Francophones des Langages Applicatifs}, + pages={198}, + year = {2020}, + url = {https://hal.inria.fr/hal-02427360} +} diff --git a/thys/VeriComp/document/root.tex b/thys/VeriComp/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/VeriComp/document/root.tex @@ -0,0 +1,67 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{A Generic Framework for Verified Compilers} +\author{Martin Desharnais} +\maketitle + +\begin{abstract} + This is a generic framework for formalizing compiler transformations. + It leverages Isabelle/HOL’s locales to abstract over concrete languages and transformations. + It states common definitions for language semantics, program behaviours, forward and backward simulations, and compilers. + We provide generic operations, such as simulation and compiler composition, and prove general (partial) correctness theorems, resulting in reusable proof components. + For more details, please see our paper \cite{desharnais-jfla2020}. +\end{abstract} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: