diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,523 +1,524 @@ 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 Hello_World 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 +Relational-Incorrectness-Logic 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 WOOT_Strong_Eventual_Consistency Word_Lib WorkerWrapper XML Zeta_Function Zeta_3_Irrational ZFC_in_HOL pGCL diff --git a/thys/Relational-Incorrectness-Logic/ROOT b/thys/Relational-Incorrectness-Logic/ROOT new file mode 100644 --- /dev/null +++ b/thys/Relational-Incorrectness-Logic/ROOT @@ -0,0 +1,10 @@ +chapter AFP + +session "Relational-Incorrectness-Logic" (AFP) = "HOL-IMP" + + options [timeout = 600] + theories + RelationalIncorrectness + + document_files + "root.bib" + "root.tex" diff --git a/thys/Relational-Incorrectness-Logic/RelationalIncorrectness.thy b/thys/Relational-Incorrectness-Logic/RelationalIncorrectness.thy new file mode 100644 --- /dev/null +++ b/thys/Relational-Incorrectness-Logic/RelationalIncorrectness.thy @@ -0,0 +1,834 @@ +theory RelationalIncorrectness + imports "HOL-IMP.Big_Step" +begin + +(* Author: Toby Murray *) + +section "Under-Approximate Relational Judgement" + +text {* + This is the relational analogue of OHearn's~\cite{OHearn_19} and de Vries \& Koutavas'~\cite{deVries_Koutavas_11} + judgements. + + Note that in our case it doesn't really make sense to talk about ``erroneous'' states: the + presence of an error can be seen only by the violation of a relation. Unlike O'Hearn, we cannot + encode it directly into the semantics of our programs, without giving them a relational semantics. + We use the standard big step semantics of IMP unchanged. +*} + +type_synonym rassn = "state \ state \ bool" + +definition + ir_valid :: "rassn \ com \ com \ rassn \ bool" + where + "ir_valid P c c' Q \ (\ t t'. Q t t' \ (\s s'. P s s' \ (c,s) \ t \ (c',s') \ t'))" + + +section "Rules of the Logic" + +definition + flip :: "rassn \ rassn" + where + "flip P \ \s s'. P s' s" + + +inductive + ir_hoare :: "rassn \ com \ com \ rassn \ bool" + where + ir_Skip: "(\t t'. Q t t' \ \s'. P t s' \ (c',s') \ t') \ + ir_hoare P SKIP c' Q" | + ir_If_True: "ir_hoare (\s s'. P s s' \ bval b s) c\<^sub>1 c' Q \ + ir_hoare P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) c' Q" | + ir_If_False: "ir_hoare (\s s'. P s s' \ \ bval b s) c\<^sub>2 c' Q \ + ir_hoare P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) c' Q" | + ir_Seq1: "ir_hoare P c c' Q \ ir_hoare Q d SKIP R \ ir_hoare P (Seq c d) c' R" | + ir_Assign: "ir_hoare (\t t'. \ v. P (t(x := v)) t' \ (t x) = aval e (t(x := v))) SKIP c' Q \ + ir_hoare P (Assign x e) c' Q" | + ir_While_False: "ir_hoare (\s s'. P s s' \ \ bval b s) SKIP c' Q \ + ir_hoare P (WHILE b DO c) c' Q" | + ir_While_True: "ir_hoare (\s s'. P s s' \ bval b s) (c;; WHILE b DO c) c' Q \ + ir_hoare P (WHILE b DO c) c' Q" | + ir_While_backwards_frontier: "(\n. ir_hoare (\ s s'. P n s s' \ bval b s) c SKIP (P (Suc n))) \ + ir_hoare (\s s'. \n. P n s s') (WHILE b DO c) c' Q \ + ir_hoare (P 0) (WHILE b DO c) c' Q" | + ir_conseq: "ir_hoare P c c' Q \ (\s s'. P s s' \ P' s s') \ (\s s'. Q' s s' \ Q s s') \ + ir_hoare P' c c' Q'" | + ir_disj: "ir_hoare P\<^sub>1 c c' Q\<^sub>1 \ ir_hoare P\<^sub>2 c c' Q\<^sub>2 \ + ir_hoare (\s s'. P\<^sub>1 s s' \ P\<^sub>2 s s') c c' (\ t t'. Q\<^sub>1 t t' \ Q\<^sub>2 t t')" | + ir_sym: "ir_hoare (flip P) c c' (flip Q) \ ir_hoare P c' c Q" + +section "Simple Derived Rules" + +lemma meh_simp[simp]: "(SKIP, s') \ t' = (s' = t')" + by auto + + +lemma ir_pre: "ir_hoare P c c' Q \ (\s s'. P s s' \ P' s s') \ + ir_hoare P' c c' Q" + by(erule ir_conseq, blast+) + +lemma ir_post: "ir_hoare P c c' Q \ (\s s'. Q' s s' \ Q s s') \ + ir_hoare P c c' Q'" + by(erule ir_conseq, blast+) + +section "Soundness" + +lemma Skip_ir_valid[intro]: + "(\t t'. Q t t' \ \s'. P t s' \ (c', s') \ t') \ ir_valid P SKIP c' Q" + by(auto simp: ir_valid_def) + +lemma sym_ir_valid[intro]: + "ir_valid (flip P) c' c (flip Q) \ ir_valid P c c' Q" + by(fastforce simp: ir_valid_def flip_def) + +lemma If_True_ir_valid[intro]: + "ir_valid (\a c. P a c \ bval b a) c\<^sub>1 c' Q \ + ir_valid P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) c' Q" + by(fastforce simp: ir_valid_def) + +lemma If_False_ir_valid[intro]: + "ir_valid (\a c. P a c \ \ bval b a) c\<^sub>2 c' Q \ + ir_valid P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) c' Q" + by(fastforce simp: ir_valid_def) + +lemma Seq1_ir_valid[intro]: + "ir_valid P c c' Q \ ir_valid Q d SKIP R \ ir_valid P (c;; d) c' R" + by(fastforce simp: ir_valid_def) + +lemma Seq2_ir_valid[intro]: + "ir_valid P c SKIP Q \ ir_valid Q d c' R \ ir_valid P (c;; d) c' R" + by(fastforce simp: ir_valid_def) + +lemma Seq_ir_valid[intro]: + "ir_valid P c c' Q \ ir_valid Q d d' R \ ir_valid P (c;; d) (c';; d') R" + by(fastforce simp: ir_valid_def) + +lemma Assign_blah[intro]: + "t x = aval e (t(x := v)) + \ (x ::= e, t(x := v)) \ t" + using Assign + by (metis fun_upd_triv fun_upd_upd) + +lemma Assign_ir_valid[intro]: + "ir_valid (\t t'. \ v. P (t(x := v)) t' \ (t x) = aval e (t(x := v))) SKIP c' Q \ ir_valid P (Assign x e) c' Q" + by(fastforce simp: ir_valid_def) + +lemma While_False_ir_valid[intro]: + "ir_valid (\s s'. P s s' \ \ bval b s) SKIP c' Q \ + ir_valid P (WHILE b DO c) c' Q" + by(fastforce simp: ir_valid_def) + +lemma While_True_ir_valid[intro]: + "ir_valid (\s s'. P s s' \ bval b s) (Seq c (WHILE b DO c)) c' Q \ + ir_valid P (WHILE b DO c) c' Q" + by(clarsimp simp: ir_valid_def, blast) + + +lemma While_backwards_frontier_ir_valid': + assumes asm: "\n. \t t'. P (k + Suc n) t t' \ + (\s. P (k + n) s t' \ bval b s \ (c, s) \ t)" + assumes last: "\t t'. Q t t' \ (\s s'. (\n. P (k + n) s s') \ (WHILE b DO c, s) \ t \ (c', s') \ t')" + assumes post: "Q t t'" + shows "\s s'. P k s s' \ (WHILE b DO c, s) \ t \ (c', s') \ t'" +proof - + from post last obtain s s' n where + "P (k + n) s s'" "(WHILE b DO c, s) \ t" "(c', s') \ t'" + by blast + with asm show ?thesis + proof(induction n arbitrary: k t t') + case 0 + then show ?case + by (metis WhileFalse WhileTrue add.right_neutral) + next + case (Suc n) + from Suc + obtain r r' where final_iteration: "P (Suc k) r r'" "(WHILE b DO c, r) \ t" "(c', r') \ t'" + by (metis add_Suc_shift) + from final_iteration(1) obtain q q' where + "P k q r' \ bval b q \ (c, q) \ r" + by (metis Nat.add_0_right Suc.prems(1) plus_1_eq_Suc semiring_normalization_rules(24)) + with final_iteration show ?case by blast + qed +qed + + +lemma While_backwards_frontier_ir_valid[intro]: + "(\n. ir_valid (\ s s'. P n s s' \ bval b s) c SKIP (P (Suc n))) \ + ir_valid (\s s'. \n. P n s s') (WHILE b DO c) c' Q \ + ir_valid (P 0) (WHILE b DO c) c' Q" + by(auto simp: meh_simp ir_valid_def intro: While_backwards_frontier_ir_valid') + +lemma conseq_ir_valid: + "ir_valid P c c' Q \ (\s s'. P s s' \ P' s s') \ (\s s'. Q' s s' \ Q s s') \ + ir_valid P' c c' Q'" + by(clarsimp simp: ir_valid_def, blast) + +lemma disj_ir_valid[intro]: + "ir_valid P\<^sub>1 c c' Q\<^sub>1 \ ir_valid P\<^sub>2 c c' Q\<^sub>2 \ + ir_valid (\s s'. P\<^sub>1 s s' \ P\<^sub>2 s s') c c' (\ t t'. Q\<^sub>1 t t' \ Q\<^sub>2 t t')" + by(fastforce simp: ir_valid_def) + + +theorem soundness: + "ir_hoare P c c' Q \ ir_valid P c c' Q" + apply(induction rule: ir_hoare.induct) + apply(blast intro!: Skip_ir_valid) + by (blast intro: conseq_ir_valid)+ + +section "Completeness" + +lemma ir_Skip_Skip[intro]: + "ir_hoare P SKIP SKIP P" + by(rule ir_Skip, simp) + +lemma ir_hoare_Skip_Skip[simp]: + "ir_hoare P SKIP SKIP Q = (\s s'. Q s s' \ P s s')" + using soundness ir_valid_def meh_simp ir_conseq ir_Skip by metis + +lemma ir_valid_Seq1: + "ir_valid P (c1;; c2) c' Q \ ir_valid P c1 c' (\t t'. \s s'. P s s' \ (c1,s) \ t \ (c',s') \ t' \ (\u. (c2,t) \ u \ Q u t'))" + by(auto simp: ir_valid_def) + +lemma ir_valid_Seq1': + "ir_valid P (c1;; c2) c' Q \ ir_valid (\t t'. \s s'. P s s' \ (c1,s) \ t \ (c',s') \ t' \ (\u. (c2,t) \ u \ Q u t')) c2 SKIP Q" + by(clarsimp simp: ir_valid_def, meson SeqE) + +lemma ir_valid_track_history: + "ir_valid P c c' Q \ + ir_valid P c c' (\t t'. Q s s' \ (\s s'. P s s' \ (c,s) \ t \ (c',s') \ t'))" + by(auto simp: ir_valid_def) + +lemma ir_valid_If: + "ir_valid (\s s'. P s s') (IF b THEN c1 ELSE c2) c' Q \ + ir_valid (\s s'. P s s' \ bval b s) c1 c' (\t t'. Q t t' \ (\s s'. P s s' \ (c1,s) \ t \ (c',s') \ t' \ bval b s)) \ + ir_valid (\s s'. P s s' \ \ bval b s) c2 c' (\t t'. Q t t' \ (\s s'. P s s' \ (c2,s) \ t \ (c',s') \ t' \ \ bval b s))" + by(clarsimp simp: ir_valid_def, blast) + +text {* + Inspired by the + ``@{text "p(n) = {\ | you can get back from \ to some state in p by executing C backwards n times}"}'' + part of OHearn~\cite{OHearn_19}. +*} +primrec get_back where + "get_back P b c 0 = (\t t'. P t t')" | + "get_back P b c (Suc n) = (\t t'. \s. (c,s) \ t \ bval b s \ get_back P b c n s t')" + +(* Currently not used anywhere *) +lemma ir_valid_get_back: + "ir_valid (get_back P b c (Suc k)) (WHILE b DO c) c' Q \ + ir_valid (get_back P b c k) (WHILE b DO c) c' Q" +proof(induct k) + case 0 + then show ?case by(clarsimp simp: ir_valid_def, blast) +next + case (Suc k) + then show ?case using WhileTrue get_back.simps(2) ir_valid_def by smt +qed + +(* both this an the next one get used in the completeness proof *) +lemma ir_valid_While1: + "ir_valid (get_back P b c k) (WHILE b DO c) c' Q \ + (ir_valid (\s s'. get_back P b c k s s' \ bval b s) c SKIP (\t t'. get_back P b c (Suc k) t t' \ (\u u'. (WHILE b DO c,t) \ u \ (c',t') \ u' \ Q u u')))" +proof (subst ir_valid_def, clarsimp) + fix t t' s u u' + assume "ir_valid (get_back P b c k) (WHILE b DO c) c' Q" + "(WHILE b DO c, t) \ u" + "(c, s) \ t" + "(c', t') \ u'" + "Q u u'" + "bval b s" + "get_back P b c k s t'" + thus "\s. get_back P b c k s t' \ bval b s \ (c, s) \ t" + proof(induction k arbitrary: t t' s u u') + case 0 + then show ?case + by auto + next + case (Suc k) + show ?case + using Suc.prems(3) Suc.prems(6) Suc.prems(7) by blast + qed +qed + +lemma ir_valid_While3: + "ir_valid (get_back P b c k) (WHILE b DO c) c' Q \ + (ir_valid (\s s'. get_back P b c k s s' \ bval b s) c c' (\t t'. (\s'. (c',s') \ t' \ get_back P b c (Suc k) t s' \ (\u. (WHILE b DO c,t) \ u \ Q u t'))))" + apply(subst ir_valid_def, clarsimp) +proof - + fix t t' s' s u + assume "ir_valid (get_back P b c k) (WHILE b DO c) c' Q" + "(WHILE b DO c, t) \ u" + "(c, s) \ t" + "(c', s') \ t'" + "Q u t'" + "bval b s" + "get_back P b c k s s'" + thus "\s s'. get_back P b c k s s' \ bval b s \ (c, s) \ t \ (c',s') \ t'" + proof(induction k arbitrary: t t' s' s u) + case 0 + then show ?case + by auto + next + case (Suc k) + show ?case + using Suc.prems(3) Suc.prems(4) Suc.prems(6) Suc.prems(7) by blast + qed +qed + +(* not used anywhere *) +lemma ir_valid_While2: + "ir_valid P (WHILE b DO c) c' Q \ + ir_valid (\s s'. P s s' \ \ bval b s) SKIP c' (\t t'. Q t t' \ (\s'. (c',s') \ t' \ P t s' \ \ bval b t))" + by(clarsimp simp: ir_valid_def, blast) + +lemma assign_upd_blah: + "(\a. if a = x1 then s x1 else (s(x1 := aval x2 s)) a) = s" + by(rule ext, auto) + +lemma Assign_complete: + assumes v: "ir_valid P (x1 ::= x2) c' Q" + assumes q: "Q t t'" + shows "\s'. (\v. P (t(x1 := v)) s' \ t x1 = aval x2 (t(x1 := v))) \ (c', s') \ t'" +proof - + from v and q obtain s s' where a: "P s s' \ (x1 ::= x2,s) \ t \ (c',s') \ t'" + using ir_valid_def by smt + hence "P (\a. if a = x1 then s x1 else (s(x1 := aval x2 s)) a) s' \ aval x2 s = aval x2 (s(x1 := s x1))" + using assign_upd_blah + by simp + thus ?thesis + using assign_upd_blah a + by (metis AssignE fun_upd_same fun_upd_triv fun_upd_upd) +qed + +lemmas ir_Skip_sym = ir_sym[OF ir_Skip, simplified flip_def] + +theorem completeness: + "ir_valid P c c' Q \ ir_hoare P c c' Q" +proof(induct c arbitrary: P c' Q) +case SKIP + show ?case + apply(rule ir_Skip) + using SKIP by(fastforce simp: ir_valid_def) +next + case (Assign x1 x2) + show ?case + apply(rule ir_Assign) + apply(rule ir_Skip) + using Assign_complete Assign by blast +next + case (Seq c1 c2) + have a: "ir_hoare P c1 c' (\t t'. \s s'. P s s' \ (c1, s) \ t \ (c', s') \ t' \ (\u. (c2, t) \ u \ Q u t'))" + using ir_valid_Seq1 Seq by blast + show ?case + apply(rule ir_Seq1) + apply (blast intro: a) + apply(rule ir_Skip_sym) + by(metis SeqE ir_valid_def Seq) +next + case (If x1 c1 c2) + have t: "ir_hoare (\s s'. P s s' \ bval x1 s) c1 c' + (\t t'. Q t t' \ (\s s'. P s s' \ (c1, s) \ t \ (c', s') \ t' \ bval x1 s))" and + f: " ir_hoare (\s s'. P s s' \ \ bval x1 s) c2 c' + (\t t'. Q t t' \ (\s s'. P s s' \ (c2, s) \ t \ (c', s') \ t' \ \ bval x1 s))" + using ir_valid_If If by blast+ + show ?case + (* consider both cases of the if via conseq, disj, then _True and _False *) + apply(rule ir_conseq) + apply(rule ir_disj) + apply(rule ir_If_True,fastforce intro: t) + apply(rule ir_If_False, fastforce intro: f) + apply blast + by (smt IfE ir_valid_def If) +next + case (While x1 c) + have a: "\n. ir_hoare (\s s'. get_back P x1 c n s s' \ bval x1 s) c SKIP (get_back P x1 c (Suc n))" + using ir_valid_While1 While + by (smt get_back.simps(2) ir_valid_def meh_simp) + have b: "ir_hoare (\s s'. P s s' \ bval x1 s) c c' + (\t t'. \s'. (c', s') \ t' \ (\s. (c, s) \ t \ bval x1 s \ P s s') \ + (\u. (WHILE x1 DO c, t) \ u \ Q u t'))" + using ir_valid_While3[where k=0,simplified] While by blast + have gb: "\t t'. Q t t' \ (\s'. (c', s') \ t' \ P t s' \ \ bval x1 t) \ + \s'. ((\n. get_back P x1 c n t s') \ \ bval x1 t) \ (c', s') \ t'" + by (meson get_back.simps(1)) + + show ?case + (* use the frontier rule much as in OHearn POPL *) + apply(rule ir_conseq) + apply(rule_tac P="get_back P x1 c" in ir_While_backwards_frontier) + apply(blast intro: a) + (* consider both cases of the While via conseq, disj, then _True and _False *) + apply(rule ir_conseq) + apply(rule ir_disj) + apply(rule_tac P="\s s'. \n. get_back P x1 c n s s'" and Q="(\t t'. Q t t' \ (\s'. (c', s') \ t' \ P t s' \ \ bval x1 t))" in ir_While_False) + apply(rule ir_Skip, blast intro: gb) + apply(rule ir_While_True) + apply(rule ir_Seq1[OF b]) + apply(rule ir_Skip_sym) + apply(fastforce) + apply (metis get_back.simps(1)) + apply assumption + apply simp + by (metis While.prems WhileE ir_valid_def) +qed + + + + +section "A Decomposition Principle: Proofs via Under-Approximate Hoare Logic" + +text {* + We show the under-approximate analogue holds for Beringer's~\cite{Beringer_11} decomposition + principle for over-approximate relational logic. +*} + + +definition + decomp :: "rassn \ com \ com \ rassn \ rassn" where + "decomp P c c' Q \ \t s'. \s t'. P s s' \ (c,s) \ t \ (c',s') \ t' \ Q t t'" + + +lemma ir_valid_decomp1: + "ir_valid P c c' Q \ ir_valid P c SKIP (decomp P c c' Q) \ ir_valid (decomp P c c' Q) SKIP c' Q" + by(fastforce simp: ir_valid_def meh_simp decomp_def) + +lemma ir_valid_decomp2: + "ir_valid P c SKIP R \ ir_valid R SKIP c' Q \ ir_valid P c c' Q" + by(fastforce simp: ir_valid_def meh_simp decomp_def) + +lemma ir_valid_decomp: + "ir_valid P c c' Q = (ir_valid P c SKIP (decomp P c c' Q) \ ir_valid (decomp P c c' Q) SKIP c' Q)" + using ir_valid_decomp1 ir_valid_decomp2 by blast + +text {* + Completeness with soundness means we can prove proof rules about @{term ir_hoare} in terms + of @{term ir_valid}. +*} + +lemma ir_to_Skip: + "ir_hoare P c c' Q = (ir_hoare P c SKIP (decomp P c c' Q) \ ir_hoare (decomp P c c' Q) SKIP c' Q)" + using soundness completeness ir_valid_decomp + by meson + +text {* + O'Hearn's under-approximate Hoare triple, for the ``ok'' case (since that is the only case we have) + This is also likely the same as from the "Reverse Hoare Logic" paper (SEFM). +*} +type_synonym assn = "state \ bool" +definition + ohearn :: "assn \ com \ assn \ bool" + where + "ohearn P c Q \ (\t. Q t \ (\s. P s \ (c,s) \ t))" + +lemma fold_ohearn1: + "ir_valid P c SKIP Q = (\t'. ohearn (\t. P t t') c (\t. Q t t'))" + by(fastforce simp add: ir_valid_def ohearn_def) + +lemma fold_ohearn2: + "ir_valid P SKIP c' Q = (\t. ohearn (P t) c' (Q t))" + by(simp add: ir_valid_def ohearn_def) + +theorem relational_via_hoare: + "ir_hoare P c c' Q = ((\t'. ohearn (\t. P t t') c (\t. decomp P c c' Q t t')) \ (\t. ohearn (decomp P c c' Q t) c' (Q t)))" +proof - + have a: "\P c c' Q. ir_hoare P c c' Q = ir_valid P c c' Q" + using soundness completeness by auto + show ?thesis + using ir_to_Skip a fold_ohearn1 fold_ohearn2 by metis +qed + +section "Deriving Proof Rules from Completeness" + +text {* + Note that we can more easily derive proof rules sometimes by appealing to the + corresponding properties of @{term ir_valid} than from the proof rules directly. + + We see more examples of this later on when we consider examples. +*} + +lemma ir_Seq2: + "ir_hoare P c SKIP Q \ ir_hoare Q d c' R \ ir_hoare P (Seq c d) c' R" + using soundness completeness Seq2_ir_valid by metis + +lemma ir_Seq: + "ir_hoare P c c' Q \ ir_hoare Q d d' R \ ir_hoare P (Seq c d) (Seq c' d') R" + using soundness completeness Seq_ir_valid by metis + +section "Examples" + +subsection "Some Derived Proof Rules" + +text {* +First derive some proof rules -- here not by appealing to completeness but just using +the existing rules +*} + +lemma ir_If_True_False: + "ir_hoare (\s s'. P s s' \ bval b s \ \ bval b' s') c\<^sub>1 c\<^sub>2' Q \ + ir_hoare P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (IF b' THEN c\<^sub>1' ELSE c\<^sub>2') Q" + apply(rule ir_If_True) + apply(rule ir_sym) + apply(rule ir_If_False) + apply(rule ir_sym) + by(simp add: flip_def) + + +lemma ir_Assign_Assign: + "ir_hoare P (x ::= e) (x' ::= e') (\t t'. \v v'. P (t(x := v)) (t'(x' := v')) \ t x = aval e (t(x := v)) \ t' x' = aval e' (t'(x' := v')))" + apply(rule ir_Assign) + apply(rule ir_sym) + apply(rule ir_Assign) + by(simp add: flip_def, auto) + +subsection "prog1" + +text {* + A tiny insecure program. Note that we only need to reason on one path through this program to + detect that it is insecure. +*} + +abbreviation low_eq :: rassn where "low_eq s s' \ s ''low'' = s' ''low''" +abbreviation low_neq :: rassn where "low_neq s s' \ \ low_eq s s'" +definition prog1 :: com where + "prog1 \ (IF (Less (N 0) (V ''x'')) THEN (Assign ''low'' (N 1)) ELSE (Assign ''low'' (N 0)))" + +text {* + We prove that @{term prog1} is definitely insecure. To do that, we need to find some non-empty + post-relation that implies insecurity. The following property encodes the idea that the + post-relation is non-empty, i.e. represents a feasible pair of execution paths. +*} +definition + nontrivial :: "rassn \ bool" + where + "nontrivial Q \ (\t t'. Q t t')" + +text {* + Note the property we prove here explicitly encodes the fact that the postcondition can be anything + that implies insecurity, i.e. implies @{term low_neq}. In particular we should not necessarily + expect it to cover the entirely of all states that satisfy @{term low_neq}. + + Also note that we also have to prove that the postcondition is non-trivial. This is necessary to + make sure that the violation we find is not an infeasible path. +*} +lemma prog1: + "\Q. ir_hoare low_eq prog1 prog1 Q \ (\s s'. Q s s' \ low_neq s s') \ nontrivial Q" + apply(rule exI) + apply(rule conjI) + apply(simp add: prog1_def) + apply(rule ir_If_True_False) + apply(rule ir_Assign_Assign) + apply(rule conjI) + apply auto[1] + apply(clarsimp simp: nontrivial_def) + apply(rule_tac x="\v. 1" in exI) + apply simp + apply(rule_tac x="\v. 0" in exI) + by auto + +subsection "More Derived Proof Rules for Examples" + +definition BEq :: "aexp \ aexp \ bexp" where + "BEq a b \ And (Less a (Plus b (N 1))) (Less b (Plus a (N 1)))" + + +lemma BEq_aval[simp]: + "bval (BEq a b) s = ((aval a s) = (aval b s))" + by(auto simp add: BEq_def) + +lemma ir_If_True_True: + "ir_hoare (\s s'. P s s' \ bval b s \ bval b' s') c\<^sub>1 c\<^sub>1' Q\<^sub>1 \ + ir_hoare P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (IF b' THEN c\<^sub>1' ELSE c\<^sub>2') (\t t'. Q\<^sub>1 t t')" + by(simp add: ir_If_True ir_sym flip_def) + +lemma ir_If_False_False: + "ir_hoare (\s s'. P s s' \ \ bval b s \ \ bval b' s') c\<^sub>2 c\<^sub>2' Q\<^sub>2 \ + ir_hoare P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (IF b' THEN c\<^sub>1' ELSE c\<^sub>2') (\t t'. Q\<^sub>2 t t')" + by(simp add: ir_If_False ir_sym flip_def) + +lemma ir_If': + "ir_hoare (\s s'. P s s' \ bval b s \ bval b' s') c\<^sub>1 c\<^sub>1' Q\<^sub>1 \ + ir_hoare (\s s'. P s s' \ \ bval b s \ \ bval b' s') c\<^sub>2 c\<^sub>2' Q\<^sub>2 \ + ir_hoare P (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (IF b' THEN c\<^sub>1' ELSE c\<^sub>2') (\t t'. Q\<^sub>1 t t' \ Q\<^sub>2 t t')" + apply(rule ir_pre) + apply(rule ir_disj) + apply(rule ir_If_True_True) + apply assumption + apply(rule ir_If_False_False) + apply assumption + apply blast + done + +lemma ir_While_triv: + "ir_hoare (\s s'. P s s' \ \ bval b s \ \ bval b' s') SKIP SKIP Q\<^sub>2 \ + ir_hoare P (WHILE b DO c) (WHILE b' DO c') (\s s'. (Q\<^sub>2 s s'))" + by(simp add: ir_While_False ir_sym flip_def) + +lemma ir_While': + "ir_hoare (\s s'. P s s' \ bval b s \ bval b' s') (c;;WHILE b DO c) (c';;WHILE b' DO c') Q\<^sub>1 \ + ir_hoare (\s s'. P s s' \ \ bval b s \ \ bval b' s') SKIP SKIP Q\<^sub>2 \ + ir_hoare P (WHILE b DO c) (WHILE b' DO c') (\s s'. (Q\<^sub>1 s s' \ Q\<^sub>2 s s'))" + apply(rule ir_pre) + apply(rule ir_disj) + apply(rule ir_While_True) + apply(rule ir_sym) + apply(simp add: flip_def) + apply(rule ir_While_True) + apply(rule ir_sym) + apply(simp add: flip_def) + apply(rule ir_While_triv) + apply assumption + apply simp + done + +subsection "client0" + +definition low_eq_strong where + "low_eq_strong s s' \ (s ''high'' \ s' ''high'') \ low_eq s s'" + +lemma low_eq_strong_upd[simp]: + "var \ ''high'' \ var \ ''low'' \ low_eq_strong(s(var := v)) (s'(var := v')) = low_eq_strong s s'" + by(auto simp: low_eq_strong_def) + +text {* + A variation on client0 from O'Hearn~\cite{OHearn_19}: how to reason about loops via a single unfolding +*} +definition client0 :: com where + "client0 \ (Assign ''x'' (N 0);; + (While (Less (N 0) (V ''n'')) + ((Assign ''x'' (Plus (V ''x'') (V ''n'')));; + (Assign ''n'' (V ''nondet''))));; + (If (BEq (V ''x'') (N 2000000)) (Assign ''low'' (V ''high'')) SKIP))" + + + +lemma client0: + "\Q. ir_hoare low_eq client0 client0 Q \ (\s s'. Q s s' \ low_neq s s') \ nontrivial Q" + apply(rule exI, rule conjI, simp add: client0_def) + apply(rule_tac P=low_eq_strong in ir_pre) + apply(rule ir_Seq) + apply(rule ir_Seq) + apply(rule ir_Assign_Assign) + apply clarsimp + + apply(rule ir_While') + apply clarsimp + + apply(rule ir_Seq) + apply(rule ir_Seq) + apply(rule ir_Assign_Assign) + apply(rule ir_Assign_Assign) + apply clarsimp + + apply(rule ir_While_triv) + apply clarsimp + apply assumption + + apply clarsimp + apply assumption + + + apply(rule ir_If_True_True) + apply(rule ir_Assign_Assign) + apply(fastforce simp: low_eq_strong_def) + apply(rule conjI) + apply(clarsimp simp: low_eq_strong_def split: if_splits) + + (* ugh having to manually do constraint solving here... *) + apply(clarsimp simp: low_eq_strong_def nontrivial_def) + apply(rule_tac x="\v. if v = ''x'' then 2000000 else if v = ''high'' then 1 else if v = ''n'' then -1 else if v = ''nondet'' then -1 else if v = ''low'' then 1 else undefined" in exI) + apply(rule_tac x="\v. if v = ''x'' then 2000000 else if v = ''high'' then 0 else if v = ''n'' then -1 else if v = ''nondet'' then -1 else if v = ''low'' then 0 else undefined" in exI) + apply clarsimp + done + +(* Not needed? *) +lemma ir_While_backwards: + "(\n. ir_hoare (\ s s'. P n s s' \ bval b s) c SKIP (P (Suc n))) \ + ir_hoare (\s s'. \n. P n s s' \ \ bval b s) SKIP c' Q \ + ir_hoare (P 0) (WHILE b DO c) c' Q" + apply(rule ir_While_backwards_frontier) + apply assumption + apply(rule ir_While_False) + apply auto + done + +subsection "Derive a variant of the backwards variant rule" + +text {* Here we appeal to completeness again to derive this rule from the corresponding + property about @{term ir_valid}. *} + +subsection "A variant of the frontier rule" + +text {* + Agin we derive this rule by appealing to completeness and the corresponding property of + @{term ir_valid} +*} + +lemma While_backwards_frontier_both_ir_valid': + assumes asm: "\n. \t t'. P (k + Suc n) t t' \ + (\s s'. P (k + n) s s' \ bval b s \ bval b' s' \ (c, s) \ t \ (c', s') \ t')" + assumes last: "\t t'. Q t t' \ (\s s'. (\n. P (k + n) s s') \ (WHILE b DO c, s) \ t \ (WHILE b' DO c', s') \ t')" + assumes post: "Q t t'" + shows "\s s'. P k s s' \ (WHILE b DO c, s) \ t \ (WHILE b' DO c', s') \ t'" +proof - + from post last obtain s s' n where + "P (k + n) s s'" "(WHILE b DO c, s) \ t" "(WHILE b' DO c', s') \ t'" + by blast + with asm show ?thesis + proof(induction n arbitrary: k t t') + case 0 + then show ?case + by (metis WhileFalse WhileTrue add.right_neutral) + next + case (Suc n) + from Suc + obtain r r' where final_iteration: "P (Suc k) r r'" "(WHILE b DO c, r) \ t" "(WHILE b' DO c', r') \ t'" + by (metis add_Suc_shift) + from final_iteration(1) obtain q q' where + "P k q q' \ bval b q \ bval b' q' \ (c, q) \ r \ (c', q') \ r'" + by (metis Nat.add_0_right Suc.prems(1) plus_1_eq_Suc semiring_normalization_rules(24)) + with final_iteration show ?case by blast + qed +qed + +lemma While_backwards_frontier_both_ir_valid[intro]: + "(\n. ir_valid (\ s s'. P n s s' \ bval b s \ bval b' s') c c' (P (Suc n))) \ + ir_valid (\s s'. \n. P n s s') (WHILE b DO c) (WHILE b' DO c') Q \ + ir_valid (P 0) (WHILE b DO c) (WHILE b' DO c') (\s s'. Q s s')" + by(auto simp: ir_valid_def intro: While_backwards_frontier_both_ir_valid') + +lemma ir_While_backwards_frontier_both: + "\\n. ir_hoare (\s s'. P n s s' \ bval b s \ bval b' s') c c' (P (Suc n)); + ir_hoare (\s s'. \n. P n s s') (WHILE b DO c) (WHILE b' DO c') Q\ + \ ir_hoare (P 0) (WHILE b DO c) (WHILE b' DO c') (\s s'. Q s s')" + using soundness completeness While_backwards_frontier_both_ir_valid by auto + +text {* + The following rule then follows easily as a special case +*} +lemma ir_While_backwards_both: + "(\n. ir_hoare (\ s s'. P n s s' \ bval b s \ bval b' s') c c' (P (Suc n))) \ + ir_hoare (P 0) (WHILE b DO c) (WHILE b' DO c') (\s s'. \n. P n s s' \ \ bval b s \ \ bval b' s')" + apply(rule ir_While_backwards_frontier_both) + apply blast + by(simp add: ir_While_False ir_sym flip_def) + + +subsection "client1" + + +text {* + An example roughly equivalent to cient1 from O'Hearn~\cite{OHearn_19}0 + + In particular we use the backwards variant rule to reason about the loop. +*} +definition client1 :: com where + "client1 \ (Assign ''x'' (N 0);; + (While (Less (V ''x'') (V ''n'')) + ((Assign ''x'' (Plus (V ''x'') (N 1)))));; + (If (BEq (V ''x'') (N 2000000)) (Assign ''low'' (V ''high'')) SKIP))" + + +lemma client1: + "\Q. ir_hoare low_eq client1 client1 Q \ (\s s'. Q s s' \ low_neq s s') \ nontrivial Q" + apply(rule exI, rule conjI, simp add: client1_def) + apply(rule_tac P=low_eq_strong in ir_pre) + apply(rule ir_Seq) + apply(rule ir_Seq) + apply(rule ir_Assign_Assign) + apply clarsimp + + apply(rule ir_pre) + apply(rule ir_While_backwards_both[where P="\n s s'. low_eq_strong s s' \ s ''x'' = int n \ s' ''x'' = int n \ int n \ s ''n'' \ int n \ s' ''n''"]) + apply(rule ir_post) + apply(rule ir_Assign_Assign) + apply clarsimp + + apply clarsimp + + apply(rule ir_If_True_True) + apply(rule ir_Assign_Assign) + apply(fastforce simp: low_eq_strong_def) + apply(rule conjI) + apply(clarsimp simp: low_eq_strong_def split: if_splits) + + apply clarsimp + (* ugh having to manually do constraint solving here... *) + apply(clarsimp simp: low_eq_strong_def nontrivial_def) + apply(rule_tac x="\v. if v = ''x'' then 2000000 else if v = ''high'' then 1 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 1 else undefined" in exI) + apply(rule_tac x="\v. if v = ''x'' then 2000000 else if v = ''high'' then 0 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 0 else undefined" in exI) + apply clarsimp + done + + +subsection "client2" + +text {* + An example akin to client2 from O'Hearn~\cite{OHearn_19}. + + Note that this example is carefully written to show use of the frontier rule first to + reason up to the broken loop iteration, and then we unfold the loop at that point to + reason about the broken iteration, and then use the plain backwards variant rule to + reason over the remainder of the loop. +*} +definition client2 :: com where + "client2 \ (Assign ''x'' (N 0);; + (While (Less (V ''x'') (N 4000000)) + ((Assign ''x'' (Plus (V ''x'') (N 1)));; + (If (BEq (V ''x'') (N 2000000)) (Assign ''low'' (V ''high'')) SKIP)) + ) + )" + +lemma client2: + "\Q. ir_hoare low_eq client2 client2 Q \ (\s s'. Q s s' \ low_neq s s') \ nontrivial Q" + apply(rule exI, rule conjI, simp add: client2_def) + apply(rule_tac P=low_eq_strong in ir_pre) + apply(rule ir_Seq) + apply(rule ir_Assign_Assign) + apply clarsimp + + apply(rule ir_pre) + apply(rule ir_While_backwards_frontier_both[where P="\n s s'. low_eq_strong s s' \ s ''x'' = int n \ s' ''x'' = int n \ s ''x'' \ 0 \ s ''x'' \ 2000000 - 1 \ s' ''x'' \ 0 \ s' ''x'' \ 2000000 - 1"]) + apply(rule ir_Seq) + apply(rule ir_Assign_Assign) + apply clarsimp + apply(rule ir_post) + apply(rule ir_If') + apply(rule ir_Assign_Assign) + apply(rule ir_Skip_Skip) + apply clarsimp + + apply clarsimp + apply(rule ir_While') + apply clarsimp + apply(rule ir_Seq) + apply(rule ir_Seq) + apply(rule ir_Assign_Assign) + apply(rule ir_If_True_True) + apply(rule ir_Assign_Assign) + apply clarsimp + + apply(rule ir_pre) + apply(rule ir_While_backwards_both[where P="\n s s'. s ''x'' = 2000000 + int n \ s' ''x'' = 2000000 + int n \ s ''x'' \ 2000000 \ s ''x'' \ 4000000 \ s' ''x'' \ 2000000 \ s' ''x'' \ 4000000 \ s ''low'' = s ''high'' \ s' ''low'' = s' ''high'' \ s ''high'' \ s' ''high''"]) + + + apply(rule ir_Seq) + apply(rule ir_Assign_Assign) + apply(rule ir_If_False_False) + apply fastforce + apply (fastforce simp: low_eq_strong_def) + apply fastforce + apply(fastforce simp: low_eq_strong_def) + apply(fastforce simp: low_eq_strong_def) + + apply(rule conjI) + apply(clarsimp simp: low_eq_strong_def split: if_splits) + + apply clarsimp + (* ugh having to manually do constraint solving here... *) + apply(clarsimp simp: low_eq_strong_def nontrivial_def) + apply(rule_tac x="\v. if v = ''x'' then 4000000 else if v = ''high'' then 1 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 1 else undefined" in exI) + apply(rule_tac x="\v. if v = ''x'' then 4000000 else if v = ''high'' then 0 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 0 else undefined" in exI) + apply clarsimp + done + +end diff --git a/thys/Relational-Incorrectness-Logic/document/root.bib b/thys/Relational-Incorrectness-Logic/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Relational-Incorrectness-Logic/document/root.bib @@ -0,0 +1,37 @@ +@article{OHearn_19, + title={Incorrectness logic}, + author={O'Hearn, Peter W}, + journal={Proceedings of the ACM on Programming Languages}, + volume={4}, + number={POPL}, + pages={1--32}, + year={2019}, + publisher={ACM New York, NY, USA} +} + +@inproceedings{deVries_Koutavas_11, + title={Reverse hoare logic}, + author={De Vries, Edsko and Koutavas, Vasileios}, + booktitle={International Conference on Software Engineering and Formal Methods (SEFM)}, + pages={155--171}, + year={2011}, + publisher={Springer} + } + +@inproceedings{Beringer_11, + title={Relational Decomposition}, + author={Beringer, Lennart}, + booktitle={International Conference on Interactive Theorem Proving (ITP)}, + pages={39--54}, + year={2011}, + publisher={Springer}, +} + + +@misc{murray2020underapproximate, + title={An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation \& More}, + author={Toby Murray}, + year={2020}, + howpublished={arXiv eprint arXiv:2003.04791 [cs.LO]}, + note = {\url{https://arxiv.org/abs/2003.04791}} +} \ No newline at end of file diff --git a/thys/Relational-Incorrectness-Logic/document/root.tex b/thys/Relational-Incorrectness-Logic/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Relational-Incorrectness-Logic/document/root.tex @@ -0,0 +1,50 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{An Under-Approximate Relational Logic} +\author{Toby Murray} +\maketitle + +\begin{abstract} + Recently, authors have proposed \emph{under-approximate} logics for + reasoning about programs~\cite{OHearn_19,deVries_Koutavas_11}. + So far, all such logics have been confined to + reasoning about individual program behaviours. Yet there exist many + over-approximate \emph{relational} logics for reasoning about pairs of + programs and relating their behaviours. + + We present the first under-approximate relational + logic, for the simple imperative language IMP. + We prove our logic + is both sound and complete. + Additionally, + we show how reasoning in this logic + can be decomposed into non-relational reasoning in an under-approximate + Hoare logic, mirroring Beringer's result for over-approximate + relational logics. + We illustrate the application of our logic on some small + examples in which we provably demonstrate the presence of insecurity. + + These proofs accompany a paper~\cite{murray2020underapproximate} + that explains the results in more detail. +\end{abstract} + +\tableofcontents + +% include generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document}