From d0bab9c79f0d6fb86d85b2a185bbe6db2dd0c327 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 10 Oct 2023 08:54:45 +1100 Subject: [PATCH 01/67] misc/scripts: remove Darwin cpp wrapper This wrapper around Apple llvm-gcc has been obsolete and unused for a few years now. Remove to avoid confusion. Signed-off-by: Gerwin Klein --- misc/scripts/cpp | 13 ------------- 1 file changed, 13 deletions(-) delete mode 100755 misc/scripts/cpp diff --git a/misc/scripts/cpp b/misc/scripts/cpp deleted file mode 100755 index 5984ff080c..0000000000 --- a/misc/scripts/cpp +++ /dev/null @@ -1,13 +0,0 @@ -#!/bin/bash -# -# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) -# -# SPDX-License-Identifier: BSD-2-Clause -# - -# -# Wrapper for clang C preprocessor on MacOS -# -export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre" - -llvm-gcc -Wno-invalid-pp-token -E -x c $@ From 03a045309ef2271e72af1f5c1e5c4f2f026c0b1b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 12 Oct 2023 11:37:35 +1100 Subject: [PATCH 02/67] lib/monads: add AFP document setup Abstract and author list for upcoming AFP entry. Author list is determined separate for each session (ML_Utils, Eisbach_Tools, Monads) by lines added/removed over the repo history. Acknowledgements are from the repo history. The latter might be incomplete, because git has trouble following more than a single file through renames, and these files were renamed a lot. Signed-off-by: Gerwin Klein --- lib/Monads/ROOT | 4 ++ lib/Monads/document/root.tex | 81 ++++++++++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+) create mode 100644 lib/Monads/document/root.tex diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT index 5fe32ad49e..05570bfffc 100644 --- a/lib/Monads/ROOT +++ b/lib/Monads/ROOT @@ -7,6 +7,7 @@ chapter Lib session Monads (lib) = HOL + + options [document = pdf] sessions "HOL-Library" @@ -52,3 +53,6 @@ session Monads (lib) = HOL + Strengthen Nondet_Strengthen_Setup Strengthen_Demo + + document_files + "root.tex" diff --git a/lib/Monads/document/root.tex b/lib/Monads/document/root.tex new file mode 100644 index 0000000000..034c05ab93 --- /dev/null +++ b/lib/Monads/document/root.tex @@ -0,0 +1,81 @@ +% +% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) +% +% SPDX-License-Identifier: CC-BY-SA-4.0 +% + +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\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{tt} + + +\begin{document} + +\title{State Monad Library} +\author{David Greenaway, + Gerwin Klein, + Corey Lewis, + Daniel Matichuk, + Thomas Sewell} +\maketitle + +\begin{abstract} + This entry contains a library of different state monads with a large set of + operators, laws, Hoare Logic, weakest precondition rules, and corresponding + automation. The formalisation is designed for reasoning about total and + partial correctness, as well as for reasoning about failure separately from + normal behaviour. Partial correctness in this context ignores program failure. + Total correctness implies the absence of program failure. + + The main monads formalised in this entry are a non-deterministic state monad + with failure, and a state-based trace monad for modelling concurrent executions. + Both support roughly the same set of operators. They come with a standard + Hoare Logic and Rely-Guarantee logic respectively. The entry also contains an + option reader monad that combines well with the non-deterministic state monad. + The option reader monad provides additional operators useful for building + state projections that can be used both in monadic functions and Hoare-Logic + assertions, enhancing specification re-use in proofs. + + This monad library is used in the verification of the seL4 microkernel and + predates some of the monad developments in the Isabelle library. In + particular, it defines its own syntax for do-notation, which can be overridden + with the generic monad syntax in the Isabelle library. We have opted not to do + so by default, because the overloading-based syntax from the Isabelle library + often necessitates additional type annotations when mixing different monad + types within one specification. For similar reasons, no attempt is made to + state generic state monad laws in a type class or locale and then instantiate + them for the two main monad instances. The resulting duplication from two + instances is still easy to handle, but if more instances are added to this + library, additional work on genericity would be useful. + + This library has grown over more than a decade with many substantial + contributions. We would specifically like to acknowledge the contributions by + Nelson Billing, Andrew Boyton, Matthew Brecknell, David Cock, Matthias Daum, + Alejandro Gomez-Londono, Rafal Kolanski, Japheth Lim, Michael McInerney, Toby + Murray, Lars Noschinski, Edward Pierzchalski, Sean Seefried, Miki Tanaka, Vernon + Tang, and Simon Windwood. +\end{abstract} + +\tableofcontents + +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: From b2dd5db6d1c7b713d7736fc67ec4f19b7b4db6cc Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 12 Oct 2023 12:26:44 +1100 Subject: [PATCH 03/67] lib/monads: fix document preparation issues Fix remaining unquoted underscore names and similar to make the LaTeX document preparation pass. Signed-off-by: Gerwin Klein --- lib/Monads/Fun_Pred_Syntax.thy | 4 +++- lib/Monads/Strengthen_Demo.thy | 8 ++++---- lib/Monads/document/root.tex | 2 +- lib/Monads/nondet/Nondet_Empty_Fail.thy | 2 +- lib/Monads/nondet/Nondet_No_Throw.thy | 2 +- lib/Monads/nondet/Nondet_Total.thy | 2 +- lib/Monads/nondet/Nondet_VCG.thy | 2 +- lib/Monads/nondet/Nondet_While_Loop_Rules.thy | 10 +++++----- lib/Monads/reader_option/Reader_Option_Monad.thy | 4 ++-- lib/Monads/trace/Trace_Monad.thy | 4 ++-- lib/Monads/trace/Trace_VCG.thy | 2 +- lib/Monads/wp/Datatype_Schematic.thy | 16 ++++++++-------- lib/Monads/wp/Eisbach_WP.thy | 8 ++++---- lib/Monads/wp/WPI.thy | 14 +++++++------- 14 files changed, 41 insertions(+), 39 deletions(-) diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy index 691b929717..2068d04855 100644 --- a/lib/Monads/Fun_Pred_Syntax.thy +++ b/lib/Monads/Fun_Pred_Syntax.thy @@ -137,7 +137,9 @@ lemma pred_bot_comp[simp]: by (simp add: comp_def) -text \We would get these for free if we could instantiate pred_top/pred_bot to top/bot directly:\ +text \ + We would get these for free if we could instantiate @{const pred_top}/@{const pred_bot} to + @{const top}/@{const bot} directly:\ lemmas pred_top_left_neutral[simp] = inf_top.left_neutral[where 'a="'a \ bool", unfolded pred_top_def] diff --git a/lib/Monads/Strengthen_Demo.thy b/lib/Monads/Strengthen_Demo.thy index f34409fa39..befb994d19 100644 --- a/lib/Monads/Strengthen_Demo.thy +++ b/lib/Monads/Strengthen_Demo.thy @@ -73,11 +73,11 @@ thm subset_UNIV subset_UNIV[mk_strg] text \Rules which would introduce schematics are adjusted by @{attribute mk_strg} to introduce quantifiers -instead. The argument I to mk_strg prevents this step. +instead. The argument I to @{attribute mk_strg} prevents this step. \ thm subsetD subsetD[mk_strg I] subsetD[mk_strg] -text \The first argument to mk_strg controls the way +text \The first argument to @{attribute mk_strg} controls the way the rule will be applied. I: use rule in introduction style, matching its conclusion. D: use rule in destruction (forward) style, matching its first premise. @@ -101,10 +101,10 @@ lemma (* oops, overdid it *) oops -text \Subsequent arguments to mk_strg capture premises for +text \Subsequent arguments to @{attribute mk_strg} capture premises for special treatment. The 'A' argument (synonym 'E') specifies that a premise should be solved by assumption. Our fancy proof above -used a strengthen rule bexI[mk_strg I _ A], which tells strengthen +used a strengthen rule @{text "bexI[mk_strg I _ A]"}, which tells strengthen to do approximately the same thing as \apply (rule bexI) prefer 2 apply assumption\ diff --git a/lib/Monads/document/root.tex b/lib/Monads/document/root.tex index 034c05ab93..5b20e177ec 100644 --- a/lib/Monads/document/root.tex +++ b/lib/Monads/document/root.tex @@ -4,7 +4,7 @@ % SPDX-License-Identifier: CC-BY-SA-4.0 % -\documentclass[11pt,a4paper]{article} +\documentclass[11pt,a4paper]{report} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} diff --git a/lib/Monads/nondet/Nondet_Empty_Fail.thy b/lib/Monads/nondet/Nondet_Empty_Fail.thy index 889f170c80..c0bcf38ddf 100644 --- a/lib/Monads/nondet/Nondet_Empty_Fail.thy +++ b/lib/Monads/nondet/Nondet_Empty_Fail.thy @@ -14,7 +14,7 @@ begin section \Monads that are wellformed w.r.t. failure\ text \ - Usually, well-formed monads constructed from the primitives in Nondet_Monad will have the following + Usually, well-formed monads constructed from the primitives in @{text Nondet_Monad} will have the following property: if they return an empty set of results, they will have the failure flag set.\ definition empty_fail :: "('s,'a) nondet_monad \ bool" where "empty_fail m \ \s. fst (m s) = {} \ snd (m s)" diff --git a/lib/Monads/nondet/Nondet_No_Throw.thy b/lib/Monads/nondet/Nondet_No_Throw.thy index 03de80df87..aa8f5b80de 100644 --- a/lib/Monads/nondet/Nondet_No_Throw.thy +++ b/lib/Monads/nondet/Nondet_No_Throw.thy @@ -32,7 +32,7 @@ lemma no_throw_def': by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits) -subsection \no_throw rules\ +subsection \@{text no_throw} rules\ lemma no_throw_returnOk[simp]: "no_throw P (returnOk a)" diff --git a/lib/Monads/nondet/Nondet_Total.thy b/lib/Monads/nondet/Nondet_Total.thy index 5eac5abd4b..ea649aa4b0 100644 --- a/lib/Monads/nondet/Nondet_Total.thy +++ b/lib/Monads/nondet/Nondet_Total.thy @@ -11,7 +11,7 @@ theory Nondet_Total imports Nondet_No_Fail begin -section \Total correctness for Nondet_Monad and Nondet_Monad with exceptions\ +section \Total correctness for @{text Nondet_Monad} and @{text Nondet_Monad} with exceptions\ subsection Definitions diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy index 4c926f36b0..f68d32c8cf 100644 --- a/lib/Monads/nondet/Nondet_VCG.thy +++ b/lib/Monads/nondet/Nondet_VCG.thy @@ -33,7 +33,7 @@ text \ the empty set, the triple is trivially valid. This means @{term "assert P"} does not require us to prove that @{term P} holds, but rather allows us to assume @{term P}! Proving non-failure is done via a separate predicate and - calculus (see Nondet_No_Fail).\ + calculus (see theory @{text Nondet_No_Fail}).\ definition valid :: "('s \ bool) \ ('s,'a) nondet_monad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\") where diff --git a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy index e41a9d6460..fe8a706b1a 100644 --- a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy +++ b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy @@ -198,7 +198,7 @@ lemma whileLoop_results_induct_lemma3 [consumes 1]: apply clarsimp done -subsection "Inductive reasoning about whileLoop results" +subsection "Inductive reasoning about @{const whileLoop} results" lemma in_whileLoop_induct[consumes 1]: assumes in_whileLoop: "(r', s') \ fst (whileLoop C B r s)" @@ -278,7 +278,7 @@ lemma whileLoop_terminatesE_induct [consumes 1]: apply (force simp: lift_def split: sum.splits) done -subsection "Direct reasoning about whileLoop components" +subsection "Direct reasoning about @{const whileLoop} components" lemma fst_whileLoop_cond_false: assumes loop_result: "(r', s') \ fst (whileLoop C B r s)" @@ -618,7 +618,7 @@ lemma whileLoopE_liftE: apply (rule set_eqI, rule iffI) apply clarsimp apply (clarsimp simp: in_liftE whileLoop_def) - \ \The schematic existential is instantiated by 'subst isr_Inr_proj' ... 'rule refl' in two lines\ + \ \The schematic existential is instantiated by @{text "subst isr_Inr_projr ... rule refl"} in two lines\ apply (rule exI) apply (rule conjI) apply (subst isr_Inr_projr) @@ -788,7 +788,7 @@ lemma whileLoopE_wp_inv [wp]: apply (rule validE_whileLoopE [where I=I], auto) done -subsection "Stronger whileLoop rules" +subsection "Stronger @{const whileLoop} rules" lemma whileLoop_rule_strong: assumes init_U: "\ \s'. s' = s \ whileLoop C B r \ \r s. (r, s) \ fst Q \" @@ -848,7 +848,7 @@ lemma snd_whileLoop_subset: done -subsection "Some rules for whileM" +subsection "Some rules for @{const whileM}" lemma whileM_wp_gen: assumes termin:"\s. I False s \ Q s" diff --git a/lib/Monads/reader_option/Reader_Option_Monad.thy b/lib/Monads/reader_option/Reader_Option_Monad.thy index 83a7c23e96..68b98c1310 100644 --- a/lib/Monads/reader_option/Reader_Option_Monad.thy +++ b/lib/Monads/reader_option/Reader_Option_Monad.thy @@ -22,7 +22,7 @@ section \Projections\ type_synonym ('s,'a) lookup = "'s \ 'a option" -text \Similar to map_option but the second function returns option as well\ +text \Similar to @{const map_option} but the second function returns @{text option} as well\ definition opt_map :: "('s,'a) lookup \ ('a \ 'b option) \ ('s,'b) lookup" (infixl "|>" 54) where "f |> g \ \s. case f s of None \ None | Some x \ g x" @@ -241,7 +241,7 @@ abbreviation ogets :: "('s \ 'a) \ ('s, 'a) lookup" wher text \ Integration with exception monad. - Corresponding bindE would be analogous to lifting in Nondet_Monad.\ + Corresponding bindE would be analogous to lifting in @{text Nondet_Monad}.\ definition "oreturnOk x = K (Some (Inr x))" diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index f0d093b77e..87fb2ba58d 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -40,7 +40,7 @@ abbreviation map_tmres_rv :: "('a \ 'b) \ ('s, 'a) tmres text \ tmonad returns a set of non-deterministic computations, including - a trace as a list of "thread identifier" \ state, and an optional + a trace as a list of @{text "thread identifier \ state"}, and an optional pair of result and state when the computation did not fail.\ type_synonym ('s, 'a) tmonad = "'s \ ((tmid \ 's) list \ ('s, 'a) tmres) set" @@ -713,7 +713,7 @@ definition whileLoop :: notation (output) whileLoop ("(whileLoop (_)// (_))" [1000, 1000] 1000) -\ \FIXME: why does this differ to Nondet_Monad?\ +\ \FIXME: why does this differ to @{text Nondet_Monad}?\ definition whileLoopT :: "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ ('s, 'r) tmonad" where diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy index f3fca936c0..7ffb2a7c13 100644 --- a/lib/Monads/trace/Trace_VCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -33,7 +33,7 @@ text \ computation is the empty set then the triple is trivially valid. This means @{term "assert P"} does not require us to prove that @{term P} holds, but rather allows us to assume @{term P}! Proving non-failure is done via a - separate predicate and calculus (see Trace_No_Fail).\ + separate predicate and calculus (see @{text Trace_No_Fail}).\ definition valid :: "('s \ bool) \ ('s,'a) tmonad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\") where diff --git a/lib/Monads/wp/Datatype_Schematic.thy b/lib/Monads/wp/Datatype_Schematic.thy index 399b045615..9701c97e0b 100644 --- a/lib/Monads/wp/Datatype_Schematic.thy +++ b/lib/Monads/wp/Datatype_Schematic.thy @@ -26,7 +26,7 @@ text \ schematic does not have as parameters. In the "constructor expression" case, we let users supply additional - constructor handlers via the `datatype_schematic` attribute. The method uses + constructor handlers via the @{text "datatype_schematic"} attribute. The method uses rules of the following form: @{term "\x1 x2 x3. getter (constructor x1 x2 x3) = x2"} @@ -69,18 +69,18 @@ structure Datatype_Schematic_Data = Generic_Data ( \ \ Keys are names of datatype constructors (like @{const Cons}), values are - `(index, function_name, thm)`. + @{text "(index, function_name, thm)"}. - - `function_name` is the name of an "accessor" function that accesses part + - @{text function_name} is the name of an "accessor" function that accesses part of the constructor specified by the key (so the accessor @{const hd} is related to the constructor/key @{const Cons}). - - `thm` is a theorem showing that the function accesses one of the + - @{text thm} is a theorem showing that the function accesses one of the arguments to the constructor (like @{thm list.sel(1)}). - - `idx` is the index of the constructor argument that the accessor - accesses. (eg. since `hd` accesses the first argument, `idx = 0`; since - `tl` accesses the second argument, `idx = 1`). + - @{text idx} is the index of the constructor argument that the accessor + accesses. (eg. since @{const hd} accesses the first argument, @{text "idx = 0"}; since + @{const tl} accesses the second argument, @{text "idx = 1"}). \ type T = ((int * string * thm) list) Symtab.table; val empty = Symtab.empty; @@ -287,7 +287,7 @@ lemma selectively_exposing_datatype_arugments: notes get_basic_0.simps[datatype_schematic] shows "\x. \a b. x (basic a b) = a" apply (rule exI, (rule allI)+) - apply datatype_schem \ \Only exposes `a` to the schematic.\ + apply datatype_schem \ \Only exposes @{text a} to the schematic.\ by (rule refl) lemma method_handles_primrecs_with_two_constructors: diff --git a/lib/Monads/wp/Eisbach_WP.thy b/lib/Monads/wp/Eisbach_WP.thy index e2ac244ee0..86e13443f4 100644 --- a/lib/Monads/wp/Eisbach_WP.thy +++ b/lib/Monads/wp/Eisbach_WP.thy @@ -17,10 +17,10 @@ begin text \ - Methods for manipulating the post conditions of hoare triples as if they + Methods for manipulating the post conditions of Hoare triples as if they were proper subgoals. - post_asm can be used with the @ attribute to modify existing proofs. Useful + @{text post_asm} can be used with the \@ attribute to modify existing proofs. Useful for proving large postconditions in one proof and then subsequently decomposing it. \ @@ -98,8 +98,8 @@ end text \ - Method (meant to be used with @ as an attribute) used for producing multiple facts out of - a single hoare triple with a conjunction in its post condition. + Method (meant to be used with \@ as an attribute) used for producing multiple facts out of + a single Hoare triple with a conjunction in its post condition. \ context begin diff --git a/lib/Monads/wp/WPI.thy b/lib/Monads/wp/WPI.thy index 3b67c283ed..f078015eb0 100644 --- a/lib/Monads/wp/WPI.thy +++ b/lib/Monads/wp/WPI.thy @@ -43,7 +43,7 @@ lemma bool_function_four_cases: by (auto simp add: fun_eq_iff all_bool_eq) -text \The ML version of repeat_new is slightly faster than the Eisbach one.\ +text \The ML version of @{text repeat_new} is slightly faster than the Eisbach one.\ method_setup repeat_new = \Method.text_closure >> (fn m => fn ctxt => fn facts => @@ -142,7 +142,7 @@ private lemma by (simp add: atomic_def ) text \Decomposing a static term is a waste of time as we know we can lift it - out all in one go. Additionally this stops wp_drop_imp from uselessly taking it apart.\ + out all in one go. Additionally this stops @{text wp_drop_imp} from uselessly taking it apart.\ private definition "static Q = (\r s. Q)" @@ -186,7 +186,7 @@ private lemma private lemma trips_True: "trip True" by (simp add: trip_def) -text \We need to push the quantifiers into the hoare triples. +text \We need to push the quantifiers into the Hoare triples. This is an unfortunate bit of manual work, but anything more than 2 levels of nesting is unlikely.\ @@ -209,7 +209,7 @@ text \Existentials are hard, and we don't see them often we fail to process the triple and it won't be lifted. Some more work here to allow the heuristics to drop any added implications - if they're deemed unecessary.\ + if they're deemed unnecessary.\ private lemma trips_push_ex1: "trip (\x. \\s. Q s\ f \\r s. Q' x r s\) \ @@ -269,7 +269,7 @@ private method uses_arg for C :: "'a \ 'b \ bool" = determ \(match (C) in "\r s. ?discard_r s" (cut) \ \fail\ \ _ \ \-\)\ text \Here the "test" constant holds information about the logical context of the atomic postcondition - in the original hoare triple. "f" is the function with its arguments, "C" is all the collected + in the original Hoare triple. "f" is the function with its arguments, "C" is all the collected premises and "Q" is the atomic postcondition that we want to solve in isolation. The method succeeds if the atomic postcondition seems to not depend on its context, i.e. @@ -305,7 +305,7 @@ private method make_goals methods wp_weak wp_strong tests = text \Once all the triples exist we simplify them all in one go to find trivial or self-contradictory rules. This avoids invoking the simplifier - once per postcondition. imp_conjL is used to curry our generated implications. + once per postcondition. @{thm imp_conjL} is used to curry our generated implications. If all the postconditions together are contradictory, the simplifier won't use it to strengthen the postcondition. As an optimization we simply bail out in that case, rather than @@ -324,7 +324,7 @@ method post_strengthen methods wp_weak wp_strong simp' tests = rule trip_drop, (rule hoare_vcg_prop)?) -text \The "wpi" named theorem is used to avoid the safety heuristics, effectively +text \The @{text wpi} named theorem is used to avoid the safety heuristics, effectively saying that the presence of that postcondition indicates that it should always be lifted.\ named_theorems wpi From 4cbfb4ab0b051f818eaa8e609c39a2c3d626c46b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 12 Oct 2023 12:30:25 +1100 Subject: [PATCH 04/67] lib/monads: minor style + warning cleanup K_def is now [simp], so doesn't need to be added explicitly any more. Signed-off-by: Gerwin Klein --- .../reader_option/Reader_Option_Monad.thy | 32 +++++++++---------- lib/Monads/trace/Trace_Monad.thy | 2 +- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/lib/Monads/reader_option/Reader_Option_Monad.thy b/lib/Monads/reader_option/Reader_Option_Monad.thy index 68b98c1310..2f502e5f8b 100644 --- a/lib/Monads/reader_option/Reader_Option_Monad.thy +++ b/lib/Monads/reader_option/Reader_Option_Monad.thy @@ -250,10 +250,10 @@ definition "othrow e = K (Some (Inl e))" definition - "oguard G \ (\s. if G s then Some () else None)" + "oguard G \ \s. if G s then Some () else None" definition - "ocondition c L R \ (\s. if c s then L s else R s)" + "ocondition c L R \ \s. if c s then L s else R s" definition "oskip \ oreturn ()" @@ -266,26 +266,26 @@ subsection \Monad laws\ lemma oreturn_bind[simp]: "(oreturn x |>> f) = f x" - by (auto simp add: oreturn_def obind_def K_def) + by (auto simp add: oreturn_def obind_def) lemma obind_return[simp]: "(m |>> oreturn) = m" - by (auto simp add: oreturn_def obind_def K_def split: option.splits) + by (auto simp add: oreturn_def obind_def split: option.splits) lemma obind_assoc: "(m |>> f) |>> g = m |>> (\x. f x |>> g)" - by (auto simp add: oreturn_def obind_def K_def split: option.splits) + by (auto simp add: oreturn_def obind_def split: option.splits) subsection \Binding and fail\ lemma obind_fail [simp]: "f |>> (\_. ofail) = ofail" - by (auto simp add: ofail_def obind_def K_def split: option.splits) + by (auto simp add: ofail_def obind_def split: option.splits) lemma ofail_bind [simp]: "ofail |>> m = ofail" - by (auto simp add: ofail_def obind_def K_def split: option.splits) + by (auto simp add: ofail_def obind_def split: option.splits) subsection \Function package setup\ @@ -348,11 +348,11 @@ lemma ocondition_True: lemma in_oreturn [simp]: "(oreturn x s = Some v) = (v = x)" - by (auto simp: oreturn_def K_def) + by (auto simp: oreturn_def) lemma oreturn_None[simp]: "\ oreturn x s = None" - by (simp add: oreturn_def K_def) + by (simp add: oreturn_def) lemma oreturnE: "\oreturn x s = Some v; v = x \ P\ \ P" @@ -360,7 +360,7 @@ lemma oreturnE: lemma in_ofail[simp]: "ofail s \ Some v" - by (auto simp: ofail_def K_def) + by (auto simp: ofail_def) lemma ofailE: "ofail s = Some v \ P" @@ -408,7 +408,7 @@ lemma obindE: lemma in_othrow_eq[simp]: "(othrow e s = Some v) = (v = Inl e)" - by (auto simp: othrow_def K_def) + by (auto simp: othrow_def) lemma othrowE: "\othrow e s = Some v; v = Inl e \ P\ \ P" @@ -416,7 +416,7 @@ lemma othrowE: lemma in_oreturnOk_eq[simp]: "(oreturnOk x s = Some v) = (v = Inr x)" - by (auto simp: oreturnOk_def K_def) + by (auto simp: oreturnOk_def) lemma oreturnOkE: "\oreturnOk x s = Some v; v = Inr x \ P\ \ P" @@ -434,11 +434,11 @@ lemma in_opt_map_Some_None_eq[simp]: lemma oreturn_comp[simp]: "oreturn x \ f = oreturn x" - by (simp add: oreturn_def K_def o_def) + by (simp add: oreturn_def o_def) lemma ofail_comp[simp]: "ofail \ f = ofail" - by (auto simp: ofail_def K_def) + by (auto simp: ofail_def) lemma oassert_comp[simp]: "oassert P \ f = oassert P" @@ -446,7 +446,7 @@ lemma oassert_comp[simp]: lemma fail_apply[simp]: "ofail s = None" - by (simp add: ofail_def K_def) + by (simp add: ofail_def) lemma oassert_apply[simp]: "oassert P s = (if P then Some () else None)" @@ -474,7 +474,7 @@ lemma if_comp_dist: lemma obindK_is_opt_map: "f \ (\x. K $ g x) = f |> g" - by (simp add: obind_def opt_map_def K_def) + by (simp add: obind_def opt_map_def) section \"While" loops over option monad.\ diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index 87fb2ba58d..5ba6f18005 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -795,7 +795,7 @@ definition parallel :: "('s,'a) tmonad \ ('s,'a) tmonad \ (map (\(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps xs), rv) \ g s})" abbreviation(input) - "parallel_mrg \ ((\((idn, s), (idn', _)). (if idn = Env then idn' else idn, s)))" + "parallel_mrg \ \((idn, s), (idn', _)). (if idn = Env then idn' else idn, s)" lemma parallel_def2: "parallel f g = (\s. {(xs, rv). \ys zs. (ys, rv) \ f s \ (zs, rv) \ g s From 598e19dd63b1b4b1026f838edc317b8538b21370 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 12 Oct 2023 12:28:46 +1100 Subject: [PATCH 05/67] lib/monads: coherent document structure Now that we're producing a proof document, theory order and chapter/section nesting matters more. Signed-off-by: Gerwin Klein --- lib/Monads/Fun_Pred_Syntax.thy | 2 ++ lib/Monads/ROOT | 17 +++++++++-------- lib/Monads/Strengthen.thy | 2 ++ .../reader_option/Reader_Option_Monad.thy | 2 ++ lib/Monads/wp/WP.thy | 2 ++ lib/Monads/wp/WP_Pre.thy | 2 ++ 6 files changed, 19 insertions(+), 8 deletions(-) diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy index 2068d04855..a284367ea5 100644 --- a/lib/Monads/Fun_Pred_Syntax.thy +++ b/lib/Monads/Fun_Pred_Syntax.thy @@ -7,6 +7,8 @@ (* Syntax for using multi-argument functions as predicates, e.g "P and Q" where P and Q are functions to bool, taking one or more parameters. *) +chapter \Function Predicate Syntax\ + theory Fun_Pred_Syntax imports Main begin diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT index 05570bfffc..be82d31d19 100644 --- a/lib/Monads/ROOT +++ b/lib/Monads/ROOT @@ -22,14 +22,7 @@ session Monads (lib) = HOL + trace theories - WPBang - WPFix - Eisbach_WP - WPI - WPC - WP_Pre - WP - Datatype_Schematic + Fun_Pred_Syntax Nondet_Monad Nondet_Lemmas Nondet_VCG @@ -53,6 +46,14 @@ session Monads (lib) = HOL + Strengthen Nondet_Strengthen_Setup Strengthen_Demo + WPBang + WPFix + Eisbach_WP + WPI + WPC + WP_Pre + WP + Datatype_Schematic document_files "root.tex" diff --git a/lib/Monads/Strengthen.thy b/lib/Monads/Strengthen.thy index 71171e2235..b2fcce21e1 100644 --- a/lib/Monads/Strengthen.thy +++ b/lib/Monads/Strengthen.thy @@ -4,6 +4,8 @@ * SPDX-License-Identifier: BSD-2-Clause *) +section \Manipulating Hoare Logic Assertions\ + theory Strengthen imports Main begin diff --git a/lib/Monads/reader_option/Reader_Option_Monad.thy b/lib/Monads/reader_option/Reader_Option_Monad.thy index 2f502e5f8b..1e77af0c84 100644 --- a/lib/Monads/reader_option/Reader_Option_Monad.thy +++ b/lib/Monads/reader_option/Reader_Option_Monad.thy @@ -11,6 +11,8 @@ * Option monad while loop formalisation. *) +chapter \State Projections and Reader Option Monad\ + theory Reader_Option_Monad imports Monad_Lib diff --git a/lib/Monads/wp/WP.thy b/lib/Monads/wp/WP.thy index 0be5d04381..9adec60420 100644 --- a/lib/Monads/wp/WP.thy +++ b/lib/Monads/wp/WP.thy @@ -4,6 +4,8 @@ * SPDX-License-Identifier: BSD-2-Clause *) +section \Weakest Preconditions\ + theory WP imports WP_Pre diff --git a/lib/Monads/wp/WP_Pre.thy b/lib/Monads/wp/WP_Pre.thy index 827771e642..410ea041ac 100644 --- a/lib/Monads/wp/WP_Pre.thy +++ b/lib/Monads/wp/WP_Pre.thy @@ -12,6 +12,8 @@ imports "HOL-Eisbach.Eisbach_Tools" begin +section \Creating Schematic Preconditions\ + ML \ structure WP_Pre = struct From 4d00865673c50296cbd6c0103931249f69dba80d Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 12 Oct 2023 14:34:37 +1100 Subject: [PATCH 06/67] lib/monads: add new Trace_* files to ROOT As the AFP submission system correctly points out, these theory files had not been included in any session yet. Signed-off-by: Gerwin Klein --- lib/Monads/ROOT | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT index be82d31d19..426cea7dce 100644 --- a/lib/Monads/ROOT +++ b/lib/Monads/ROOT @@ -43,6 +43,17 @@ session Monads (lib) = HOL + Trace_Lemmas Trace_VCG Trace_Det + Trace_No_Throw + Trace_Empty_Fail + Trace_No_Trace + Trace_Total + Trace_Strengthen_Setup + Trace_Monad_Equations + Trace_RG + Trace_In_Monad + Trace_More_VCG + Trace_No_Fail + Trace_Sat Strengthen Nondet_Strengthen_Setup Strengthen_Demo From bd5026438582f3ff5c444818527391545a6d30df Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 12 Oct 2023 14:42:49 +1100 Subject: [PATCH 07/67] lib/monads: fix remaining document preparation issues Fix document preparation issues in the theory files that have been added to ROOT in the previous commit. Signed-off-by: Gerwin Klein --- lib/Monads/trace/Trace_Empty_Fail.thy | 6 +++--- lib/Monads/trace/Trace_Monad_Equations.thy | 2 +- lib/Monads/trace/Trace_No_Fail.thy | 2 +- lib/Monads/trace/Trace_No_Throw.thy | 2 +- lib/Monads/trace/Trace_RG.thy | 6 +++--- lib/Monads/trace/Trace_Total.thy | 2 +- 6 files changed, 10 insertions(+), 10 deletions(-) diff --git a/lib/Monads/trace/Trace_Empty_Fail.thy b/lib/Monads/trace/Trace_Empty_Fail.thy index 472ec988af..1a5ebcef91 100644 --- a/lib/Monads/trace/Trace_Empty_Fail.thy +++ b/lib/Monads/trace/Trace_Empty_Fail.thy @@ -14,9 +14,9 @@ begin section \Monads that are wellformed w.r.t. failure\ text \ - Usually, well-formed monads constructed from the primitives in Trace_Monad will have the following - property: if they return an empty set of completed results, there exists a trace corresponding to - a failed result.\ + Usually, well-formed monads constructed from the primitives in @{text Trace_Monad} will have the + following property: if they return an empty set of completed results, there exists a trace + corresponding to a failed result.\ definition empty_fail :: "('s,'a) tmonad \ bool" where "empty_fail m \ \s. mres (m s) = {} \ Failed \ snd ` (m s)" diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy index 00156438b8..ff544d598f 100644 --- a/lib/Monads/trace/Trace_Monad_Equations.thy +++ b/lib/Monads/trace/Trace_Monad_Equations.thy @@ -376,7 +376,7 @@ lemma select_empty_bind[simp]: by (simp add: select_def bind_def) -subsection \Alternative env_steps with repeat\ +subsection \Alternative @{text env_steps} with repeat\ lemma mapM_Cons: "mapM f (x # xs) = do diff --git a/lib/Monads/trace/Trace_No_Fail.thy b/lib/Monads/trace/Trace_No_Fail.thy index 0c0d958edf..93b3fb60f5 100644 --- a/lib/Monads/trace/Trace_No_Fail.thy +++ b/lib/Monads/trace/Trace_No_Fail.thy @@ -144,7 +144,7 @@ lemma no_fail_assume_pre: "(\s. P s \ no_fail P f) \ no_fail P f" by (simp add: no_fail_def) -\ \lemma no_fail_liftM_eq[simp]: +\<^cancel>\lemma no_fail_liftM_eq[simp]: "no_fail P (liftM f m) = no_fail P m" by (auto simp: liftM_def no_fail_def bind_def return_def)\ diff --git a/lib/Monads/trace/Trace_No_Throw.thy b/lib/Monads/trace/Trace_No_Throw.thy index f5174f1ecd..6bffb6fa6c 100644 --- a/lib/Monads/trace/Trace_No_Throw.thy +++ b/lib/Monads/trace/Trace_No_Throw.thy @@ -31,7 +31,7 @@ lemma no_throw_def': by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits) -subsection \no_throw rules\ +subsection \@{const no_throw} rules\ lemma no_throw_returnOk[simp]: "no_throw P (returnOk a)" diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy index 3dec5f51b0..b441289ce4 100644 --- a/lib/Monads/trace/Trace_RG.thy +++ b/lib/Monads/trace/Trace_RG.thy @@ -17,7 +17,7 @@ section \Rely-Guarantee Logic\ subsection \Validity\ text \ - This section defines a Rely_Guarantee logic for partial correctness for + This section defines a Rely-Guarantee logic for partial correctness for the interference trace monad. The logic is defined semantically. Rules work directly on the @@ -36,7 +36,7 @@ text \ trace and no successful results then the quintuple is trivially valid. This means @{term "assert P"} does not require us to prove that @{term P} holds, but rather allows us to assume @{term P}! Proving non-failure is done via a - separate predicate and calculus (see Trace_No_Fail).\ + separate predicate and calculus (see @{text Trace_No_Fail}).\ primrec trace_steps :: "(tmid \ 's) list \ 's \ (tmid \ 's \ 's) set" where "trace_steps (elem # trace) s0 = {(fst elem, s0, snd elem)} \ trace_steps trace (snd elem)" @@ -56,7 +56,7 @@ next done qed -text \rg_pred type: Rely-Guaranty predicates (state before => state after => bool)\ +text \@{text rg_pred} type: Rely-Guaranty predicates (@{text "state before => state after => bool"})\ type_synonym 's rg_pred = "'s \ 's \ bool" text \Abbreviations for trivial postconditions (taking three arguments):\ diff --git a/lib/Monads/trace/Trace_Total.thy b/lib/Monads/trace/Trace_Total.thy index ea86da1600..7118a6bf21 100644 --- a/lib/Monads/trace/Trace_Total.thy +++ b/lib/Monads/trace/Trace_Total.thy @@ -11,7 +11,7 @@ theory Trace_Total imports Trace_No_Fail begin -section \Total correctness for Trace_Monad and Trace_Monad with exceptions\ +section \Total correctness for @{text Trace_Monad} and @{text Trace_Monad} with exceptions\ subsection Definitions From 67c0109b742ec3bf46cee4ce855f5becbe1adfc2 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 12 Oct 2023 15:13:13 +1100 Subject: [PATCH 08/67] lib/monads: avoid clarsimp as initial Isar method The AFP linter is stricter about this than we are, and it is definitely bad style to start with "proof (clarsimp ..)" Signed-off-by: Gerwin Klein --- lib/Monads/nondet/Nondet_While_Loop_Rules.thy | 53 ++++++++++--------- 1 file changed, 28 insertions(+), 25 deletions(-) diff --git a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy index fe8a706b1a..8cd774ab7d 100644 --- a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy +++ b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy @@ -447,33 +447,36 @@ lemma exs_valid_whileLoop: and wf_R: "wf R" and final_I: "\r s. \ T r s; \ C r s \ \ Q r s" shows "\ P \ whileLoop C B r \\ Q \" -proof (clarsimp simp: exs_valid_def Bex_def) - fix s - assume "P s" - +proof - { - fix x - have "T (fst x) (snd x) \ \r' s'. (r', s') \ fst (whileLoop C B (fst x) (snd x)) \ T r' s'" - using wf_R - proof induct - case (less x) - then show ?case - apply atomize - apply (cases "C (fst x) (snd x)") - apply (subst whileLoop_unroll) - apply (clarsimp simp: condition_def bind_def') - apply (cut_tac iter_I[where ?s0.0="snd x" and r="fst x"]) - apply (clarsimp simp: exs_valid_def) - apply blast - apply (subst whileLoop_unroll) - apply (cases x) - apply (clarsimp simp: condition_def bind_def' return_def) - done - qed + fix s + assume "P s" + + { + fix x + have "T (fst x) (snd x) \ \r' s'. (r', s') \ fst (whileLoop C B (fst x) (snd x)) \ T r' s'" + using wf_R + proof induct + case (less x) + then show ?case + apply atomize + apply (cases "C (fst x) (snd x)") + apply (subst whileLoop_unroll) + apply (clarsimp simp: condition_def bind_def') + apply (cut_tac iter_I[where ?s0.0="snd x" and r="fst x"]) + apply (clarsimp simp: exs_valid_def) + apply blast + apply (subst whileLoop_unroll) + apply (cases x) + apply (clarsimp simp: condition_def bind_def' return_def) + done + qed + } + + then have "\r' s'. (r', s') \ fst (whileLoop C B r s) \ Q r' s'" + by (metis \P s\ fst_conv init_T snd_conv final_I fst_whileLoop_cond_false) } - - thus "\r' s'. (r', s') \ fst (whileLoop C B r s) \ Q r' s'" - by (metis \P s\ fst_conv init_T snd_conv final_I fst_whileLoop_cond_false) + thus ?thesis by (clarsimp simp: exs_valid_def Bex_def) qed lemma empty_fail_whileLoop[empty_fail_cond, intro!, wp]: From b2cd1ce4ad38b236cf9aa2014c4906cb24d905a2 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 18 Aug 2023 12:05:50 +1000 Subject: [PATCH 09/67] aarch64 asmrefine: copy ArchSetup from RISCV64 Signed-off-by: Rafal Kolanski --- tools/asmrefine/AARCH64/ArchSetup.thy | 33 +++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tools/asmrefine/AARCH64/ArchSetup.thy diff --git a/tools/asmrefine/AARCH64/ArchSetup.thy b/tools/asmrefine/AARCH64/ArchSetup.thy new file mode 100644 index 0000000000..e2de86c9c6 --- /dev/null +++ b/tools/asmrefine/AARCH64/ArchSetup.thy @@ -0,0 +1,33 @@ +(* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory ArchSetup +imports + "CLib.CTranslationNICTA" +begin + +abbreviation (input) + "(arch_load_machine_word + (load_word32 :: word32 mem_read) + (load_word64 :: word64 mem_read) + :: machine_word mem_read) + \ load_word64" + +abbreviation (input) + "(arch_store_machine_word + (store_word32 :: word32 mem_upd) + (store_word64 :: word64 mem_upd) + :: machine_word mem_upd) + \ store_word64" + +abbreviation (input) + "(arch_machine_word_constructor + (from_word32 :: word32 \ 'a) + (from_word64 :: word64 \ 'a) + :: machine_word \ 'a) + \ from_word64" + +end From 32a672412c5f4722762bbc411b334fb586d2c016 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 18 Aug 2023 12:08:12 +1000 Subject: [PATCH 10/67] aarch64 cspec: add Kernel_C.thy to base CKernel image on Signed-off-by: Rafal Kolanski --- spec/cspec/AARCH64/Kernel_C.thy | 110 ++++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 spec/cspec/AARCH64/Kernel_C.thy diff --git a/spec/cspec/AARCH64/Kernel_C.thy b/spec/cspec/AARCH64/Kernel_C.thy new file mode 100644 index 0000000000..60636c5c8d --- /dev/null +++ b/spec/cspec/AARCH64/Kernel_C.thy @@ -0,0 +1,110 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory Kernel_C +imports + "ExecSpec.MachineTypes" + "CLib.CTranslationNICTA" + "AsmRefine.CommonOps" +begin + +external_file + "../c/build/$L4V_ARCH/kernel_all.c_pp" + +context begin interpretation Arch . + +requalify_types + machine_state + +end + +declare [[populate_globals=true]] + +context begin interpretation Arch . (*FIXME: arch_split*) + +type_synonym cghost_state = "(machine_word \ vmpage_size) * (machine_word \ nat) + * ghost_assertions" + +definition + gs_clear_region :: "addr \ nat \ cghost_state \ cghost_state" where + "gs_clear_region ptr bits gs \ + (%x. if x \ {ptr..+2 ^ bits} then None else fst gs x, + %x. if x \ {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))" + +definition + gs_new_frames:: "vmpage_size \ addr \ nat \ cghost_state \ cghost_state" + where + "gs_new_frames sz ptr bits \ \gs. + if bits < pageBitsForSize sz then gs + else (\x. if \n\mask (bits - pageBitsForSize sz). + x = ptr + n * 2 ^ pageBitsForSize sz then Some sz + else fst gs x, snd gs)" + +definition + gs_new_cnodes:: "nat \ addr \ nat \ cghost_state \ cghost_state" + where + "gs_new_cnodes sz ptr bits \ \gs. + if bits < sz + 4 then gs + else (fst gs, \x. if \n\mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4) + then Some sz + else fst (snd gs) x, snd (snd gs))" + +abbreviation + gs_get_assn :: "int \ cghost_state \ machine_word" + where + "gs_get_assn k \ ghost_assertion_data_get k (snd o snd)" + +abbreviation + gs_set_assn :: "int \ machine_word \ cghost_state \ cghost_state" + where + "gs_set_assn k v \ ghost_assertion_data_set k v (apsnd o apsnd)" + +declare [[record_codegen = false]] +declare [[allow_underscore_idents = true]] + +end + +(* workaround for the fact that the C parser wants to know the vmpage sizes*) +(* create appropriately qualified aliases *) +context begin interpretation Arch . global_naming vmpage_size +requalify_consts ARMSmallPage ARMLargePage ARMHugePage +end + +definition + ctcb_size_bits :: nat +where + "ctcb_size_bits \ 10" + +definition + ctcb_offset :: "64 word" +where + "ctcb_offset \ 2 ^ ctcb_size_bits" + +lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def + +cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS + +install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp" + [machinety=machine_state, ghostty=cghost_state] + +text \Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix + for these:\ +hide_const (open) + numDomains + +(* hide vmpage sizes again *) +hide_const + vmpage_size.ARMSmallPage + vmpage_size.ARMLargePage + vmpage_size.ARMHugePage + +(* re-allow fully qualified accesses (for consistency). Slightly clunky *) +context Arch begin +global_naming "AARCH64.vmpage_size" requalify_consts ARMSmallPage ARMLargePage ARMHugePage +global_naming "AARCH64" requalify_consts ARMSmallPage ARMLargePage ARMHugePage +end + +end From 402a8342dbee7fb704031acae7ca9d5a5abfc208 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 18 Aug 2023 12:09:46 +1000 Subject: [PATCH 11/67] run_tests: enable CBaseRefine for AARCH64 Switch exclusion to CRefine. Signed-off-by: Rafal Kolanski --- run_tests | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/run_tests b/run_tests index 8704a934df..731b395a68 100755 --- a/run_tests +++ b/run_tests @@ -64,12 +64,10 @@ EXCLUDE["RISCV64"]=[ EXCLUDE["AARCH64"]=[ # To be eliminated/refined as development progresses "ASepSpec", - "CKernel", - "CBaseRefine", + "CRefine", "Access", # Tools and unrelated content, removed for development - "CParser", "AutoCorres", "CamkesGlueSpec", "Sep_Algebra", From 1cce5b3ff71a139b539fcbc6265fdda65bd9ec88 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 10 Oct 2023 11:34:08 +1100 Subject: [PATCH 12/67] proof: switch AArch64 quick_and_dirty from Refine to CRefine Refine for AArch64 is now completed and doesn't need quick_and_dirty any more. CRefine is now in development mode. Signed-off-by: Gerwin Klein --- proof/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/proof/Makefile b/proof/Makefile index ffa463db9e..8781240b1e 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -10,9 +10,9 @@ default: images test test: all: images test -# Allow sorry command in AARCH64 Refine during development: +# Allow sorry command in AARCH64 CRefine during development: ifeq "$(L4V_ARCH)" "AARCH64" - export REFINE_QUICK_AND_DIRTY=1 + export CREFINE_QUICK_AND_DIRTY=1 endif # From 56323239796b59da1a1392c306417af9a38d28c1 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 10 Oct 2023 11:38:37 +1100 Subject: [PATCH 13/67] run_tests+proof: exclude SimplExportAndRefine for AARCH64 The SimplExportAndRefine session is only needed for binary verification and is currently failing. There are no plans yet for binary verification on AArch64, so the session will remain disabled for now. Signed-off-by: Gerwin Klein --- run_tests | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/run_tests b/run_tests index 731b395a68..0921cb0c85 100755 --- a/run_tests +++ b/run_tests @@ -81,7 +81,8 @@ EXCLUDE["AARCH64"]=[ "DSpec", "DBaseRefine", "CamkesGlueProofs", - "AsmRefine" + "AsmRefine", + "SimplExportAndRefine" ] # Check EXCLUDE is exhaustive over the available architectures From 8c59df4495389ca9c10e6e872811a996e9862d02 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Fri, 13 Oct 2023 10:08:01 +1100 Subject: [PATCH 14/67] lib/monads: remove more uses of _tac methods Signed-off-by: Corey Lewis --- .../reader_option/Reader_Option_VCG.thy | 6 +- lib/Monads/trace/Trace_Det.thy | 6 +- lib/Monads/trace/Trace_Empty_Fail.thy | 8 +- lib/Monads/trace/Trace_Lemmas.thy | 4 +- lib/Monads/trace/Trace_Monad.thy | 1 + lib/Monads/trace/Trace_Monad_Equations.thy | 27 ++----- lib/Monads/trace/Trace_More_VCG.thy | 80 +++++++++---------- lib/Monads/trace/Trace_RG.thy | 23 +++--- lib/Monads/trace/Trace_VCG.thy | 2 +- lib/Monads/wp/WPFix.thy | 2 + lib/Monads/wp/WPI.thy | 1 + 11 files changed, 71 insertions(+), 89 deletions(-) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 837b0c8c25..f1b2d6960c 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -116,8 +116,8 @@ lemma owhile_ovalid[wp]: \ ovalid (I a) (owhile_inv C B a I M) Q" unfolding owhile_inv_def owhile_def ovalid_def apply clarify - apply (frule_tac I = "\a. I a s" in option_while_rule) - apply auto + apply (frule (1) option_while_rule[where I = "\a. I a s" for s]) + apply auto done definition ovalid_property where "ovalid_property P x = (\s f. (\r. Some r = x s f \ P r s))" @@ -187,7 +187,7 @@ lemma owhile_NF[wp]: \ ovalidNF (I a) (owhile_inv C B a I M) Q" unfolding owhile_inv_def ovalidNF_def ovalid_def apply clarify - apply (rule_tac I = I and M = "measure (\r. M r s)" in owhile_rule) + apply (rule owhile_rule[where I = I and M = "measure (\r. M r s)" and s = s for s]) apply fastforce apply fastforce apply fastforce diff --git a/lib/Monads/trace/Trace_Det.thy b/lib/Monads/trace/Trace_Det.thy index 4b17f18dbf..54c7f03151 100644 --- a/lib/Monads/trace/Trace_Det.thy +++ b/lib/Monads/trace/Trace_Det.thy @@ -55,10 +55,8 @@ lemma det_UN: lemma bind_detI[simp, intro!]: "\ det f; \x. det (g x) \ \ det (f >>= g)" unfolding bind_def det_def - apply clarsimp - apply (erule_tac x=s in allE) - apply clarsimp - done + apply (erule all_reg[rotated]) + by clarsimp lemma det_modify[iff]: "det (modify f)" diff --git a/lib/Monads/trace/Trace_Empty_Fail.thy b/lib/Monads/trace/Trace_Empty_Fail.thy index 1a5ebcef91..74cef7f1c2 100644 --- a/lib/Monads/trace/Trace_Empty_Fail.thy +++ b/lib/Monads/trace/Trace_Empty_Fail.thy @@ -58,8 +58,7 @@ lemma empty_failD3: lemma empty_fail_bindD1: "empty_fail (a >>= b) \ empty_fail a" unfolding empty_fail_def bind_def - apply clarsimp - apply (drule_tac x=s in spec) + apply (erule all_reg[rotated]) by (force simp: split_def mres_def vimage_def split: tmres.splits) @@ -112,10 +111,7 @@ lemma empty_fail_select[empty_fail_cond]: lemma mres_bind_empty: "mres ((f >>= g) s) = {} \ mres (f s) = {} \ (\res\mres (f s). mres (g (fst res) (snd res)) = {})" - apply clarsimp - apply (clarsimp simp: mres_def split_def vimage_def bind_def) - apply (rename_tac rv s' trace) - apply (drule_tac x=rv in spec, drule_tac x=s' in spec) + apply (clarsimp simp: bind_def mres_def split_def) apply (clarsimp simp: image_def) apply fastforce done diff --git a/lib/Monads/trace/Trace_Lemmas.thy b/lib/Monads/trace/Trace_Lemmas.thy index 557c2a855d..eb504156f8 100644 --- a/lib/Monads/trace/Trace_Lemmas.thy +++ b/lib/Monads/trace/Trace_Lemmas.thy @@ -204,8 +204,8 @@ lemma liftE_liftM: lemma liftME_liftM: "liftME f = liftM (case_sum Inl (Inr \ f))" unfolding liftME_def liftM_def bindE_def returnOk_def lift_def - apply (rule ext, rename_tac x) - apply (rule_tac f="bind x" in arg_cong) + apply (rule ext) + apply (rule arg_cong[where f="bind m" for m]) apply (fastforce simp: throwError_def split: sum.splits) done diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index 5ba6f18005..97050596d4 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -806,6 +806,7 @@ lemma parallel_def2: apply (rule exI, rule conjI, assumption)+ apply (simp add: list_all2_conv_all_nth list_eq_iff_nth_eq split_def prod_eq_iff) apply clarsimp + apply (rename_tac ys zs) apply (rule_tac x="map (((\) Env) o fst) ys" in exI) apply (simp add: zip_map1 o_def split_def) apply (strengthen subst[where P="\xs. (xs, v) \ S" for v S, mk_strg I _ E]) diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy index ff544d598f..5887fb7169 100644 --- a/lib/Monads/trace/Trace_Monad_Equations.thy +++ b/lib/Monads/trace/Trace_Monad_Equations.thy @@ -117,35 +117,22 @@ lemma gets_the_returns: by (simp_all add: returnOk_def throwError_def gets_the_return) -lemma all_rv_choice_fn_eq_pred: - "\ \rv. P rv \ \fn. f rv = g fn \ \ \fn. \rv. P rv \ f rv = g (fn rv)" - apply (rule_tac x="\rv. SOME h. f rv = g h" in exI) - apply (clarsimp split: if_split) - by (meson someI_ex) - -lemma all_rv_choice_fn_eq: - "\ \rv. \fn. f rv = g fn \ - \ \fn. f = (\rv. g (fn rv))" - using all_rv_choice_fn_eq_pred[where f=f and g=g and P=\] - by (simp add: fun_eq_iff) - lemma gets_the_eq_bind: - "\ \fn. f = gets_the (fn o fn'); \rv. \fn. g rv = gets_the (fn o fn') \ + "\ f = gets_the (fn_f o fn'); \rv. g rv = gets_the (fn_g rv o fn') \ \ \fn. (f >>= g) = gets_the (fn o fn')" - apply (clarsimp dest!: all_rv_choice_fn_eq) - apply (rule_tac x="\s. case (fn s) of None \ None | Some v \ fna v s" in exI) + apply clarsimp + apply (rule exI[where x="\s. case (fn_f s) of None \ None | Some v \ fn_g v s"]) apply (simp add: gets_the_def bind_assoc exec_gets assert_opt_def fun_eq_iff split: option.split) done lemma gets_the_eq_bindE: - "\ \fn. f = gets_the (fn o fn'); \rv. \fn. g rv = gets_the (fn o fn') \ + "\ f = gets_the (fn_f o fn'); \rv. g rv = gets_the (fn_g rv o fn') \ \ \fn. (f >>=E g) = gets_the (fn o fn')" - apply (simp add: bindE_def) - apply (erule gets_the_eq_bind) + unfolding bindE_def + apply (erule gets_the_eq_bind[where fn_g="\rv s. case rv of Inl e \ Some (Inl e) | Inr v \ fn_g v s"]) apply (simp add: lift_def gets_the_returns split: sum.split) - apply fastforce done lemma gets_the_fail: @@ -531,7 +518,7 @@ lemma put_trace_mapM_x: lemma rev_surj: "surj rev" - by (rule_tac f=rev in surjI, simp) + by (rule surjI[where f=rev], simp) lemma select_image: "select (f ` S) = do x \ select S; return (f x) od" diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy index 927bb04272..8ae996e52f 100644 --- a/lib/Monads/trace/Trace_More_VCG.thy +++ b/lib/Monads/trace/Trace_More_VCG.thy @@ -137,8 +137,8 @@ lemma hoare_split_bind_case_sum: "\rv. \S rv\ h rv \Q\" assumes y: "\P\ f \S\,\R\" shows "\P\ f >>= case_sum g h \Q\" - apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]]) - apply (case_tac x, simp_all add: x) + apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]]) + apply (wpsimp wp: x split: sum.splits) done lemma hoare_split_bind_case_sumE: @@ -147,8 +147,8 @@ lemma hoare_split_bind_case_sumE: assumes y: "\P\ f \S\,\R\" shows "\P\ f >>= case_sum g h \Q\,\E\" apply (unfold validE_def) - apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]]) - apply (case_tac x, simp_all add: x [unfolded validE_def]) + apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]]) + apply (wpsimp wp: x[unfolded validE_def] split: sum.splits) done lemma assertE_sp: @@ -256,12 +256,11 @@ lemma doesn't_grow_proof: assumes x: "\x. \\s. x \ S s \ P s\ f \\rv s. x \ S s\" shows "\\s. card (S s) < n \ P s\ f \\rv s. card (S s) < n\" apply (clarsimp simp: valid_def) - apply (subgoal_tac "S b \ S s") - apply (drule card_mono [OF y], simp) + apply (erule le_less_trans[rotated]) + apply (rule card_mono[OF y]) apply clarsimp apply (rule ccontr) - apply (subgoal_tac "x \ S b", simp) - apply (erule use_valid [OF _ x]) + apply (drule (2) use_valid[OF _ x, OF _ conjI]) apply simp done @@ -297,13 +296,12 @@ lemma shrinks_proof: assumes w: "\s. P s \ x \ S s" shows "\\s. card (S s) \ n \ P s\ f \\rv s. card (S s) < n\" apply (clarsimp simp: valid_def) - apply (subgoal_tac "S b \ S s") - apply (drule psubset_card_mono [OF y], simp) + apply (erule less_le_trans[rotated]) + apply (rule psubset_card_mono[OF y]) apply (rule psubsetI) apply clarsimp apply (rule ccontr) - apply (subgoal_tac "x \ S b", simp) - apply (erule use_valid [OF _ x]) + apply (drule (2) use_valid[OF _ x, OF _ conjI]) apply simp by (metis use_valid w z) @@ -393,13 +391,12 @@ lemma P_bool_lift: assumes f: "\\s. \Q s\ f \\r s. \Q s\" shows "\\s. P (Q s)\ f \\r s. P (Q s)\" apply (clarsimp simp: valid_def) - apply (subgoal_tac "Q b = Q s") - apply simp + apply (rule back_subst[where P=P], assumption) apply (rule iffI) - apply (rule classical) - apply (drule (1) use_valid [OF _ f]) - apply simp - apply (erule (1) use_valid [OF _ t]) + apply (erule (1) use_valid [OF _ t]) + apply (rule classical) + apply (drule (1) use_valid [OF _ f]) + apply simp done lemmas fail_inv = hoare_fail_any[where Q="\_. P" and P=P for P] @@ -416,11 +413,10 @@ lemma hoare_Ball_helper: assumes y: "\P. \\s. P (S s)\ f \\rv s. P (S s)\" shows "\\s. \x \ S s. P x s\ f \\rv s. \x \ S s. Q x rv s\" apply (clarsimp simp: valid_def) - apply (subgoal_tac "S b = S s") - apply (erule post_by_hoare2 [OF x]) - apply (clarsimp simp: Ball_def) - apply (erule_tac P1="\x. x = S s" in post_by_hoare2 [OF y]) - apply (rule refl) + apply (drule bspec, erule back_subst[where P="\A. x\A" for x]) + apply (erule post_by_hoare[OF y, rotated]) + apply (rule refl) + apply (erule (1) post_by_hoare[OF x]) done lemma handy_prop_divs: @@ -479,14 +475,14 @@ lemma hoare_in_monad_post: assumes x: "\P. \P\ f \\x. P\" shows "\\\ f \\rv s. (rv, s) \ mres (f s)\" apply (clarsimp simp: valid_def) - apply (subgoal_tac "s = b", simp) - apply (simp add: state_unchanged [OF x]) + apply (rule back_subst[where P="\s. x\mres (f s)" for x], assumption) + apply (simp add: state_unchanged[OF x]) done lemma list_case_throw_validE_R: "\ \y ys. xs = y # ys \ \P\ f y ys \Q\,- \ \ \P\ case xs of [] \ throwError e | x # xs \ f x xs \Q\,-" - apply (case_tac xs, simp_all) + apply (cases xs, simp_all) apply wp done @@ -522,13 +518,13 @@ lemma wp_split_const_if: assumes x: "\P\ f \Q\" assumes y: "\P'\ f \Q'\" shows "\\s. (G \ P s) \ (\ G \ P' s)\ f \\rv s. (G \ Q rv s) \ (\ G \ Q' rv s)\" - by (case_tac G, simp_all add: x y) + by (cases G, simp_all add: x y) lemma wp_split_const_if_R: assumes x: "\P\ f \Q\,-" assumes y: "\P'\ f \Q'\,-" shows "\\s. (G \ P s) \ (\ G \ P' s)\ f \\rv s. (G \ Q rv s) \ (\ G \ Q' rv s)\,-" - by (case_tac G, simp_all add: x y) + by (cases G, simp_all add: x y) lemma hoare_disj_division: "\ P \ Q; P \ \R\ f \S\; Q \ \T\ f \S\ \ @@ -589,11 +585,12 @@ lemma univ_wp: lemma univ_get_wp: assumes x: "\P. \P\ f \\rv. P\" shows "\\s. \(rv, s') \ mres (f s). s = s' \ Q rv s'\ f \Q\" - apply (rule hoare_pre_imp [OF _ univ_wp]) + apply (rule hoare_pre_imp[OF _ univ_wp]) apply clarsimp apply (drule bspec, assumption, simp) - apply (subgoal_tac "s = b", simp) - apply (simp add: state_unchanged [OF x]) + apply (drule mp) + apply (simp add: state_unchanged[OF x]) + apply simp done lemma other_hoare_in_monad_post: @@ -630,10 +627,10 @@ lemma bindE_split_recursive_asm: apply (clarsimp simp: validE_def valid_def bindE_def in_bind lift_def) apply (erule allE, erule(1) impE) apply (drule(1) bspec, simp) - apply (case_tac x, simp_all add: in_throwError) + apply (clarsimp simp: in_throwError split: sum.splits) apply (drule x) apply (clarsimp simp: validE_def valid_def) - apply (drule(1) bspec, simp) + apply (drule(1) bspec, simp split: sum.splits) done lemma validE_R_abstract_rv: @@ -687,9 +684,8 @@ lemma valid_rv_split: lemma hoare_rv_split: "\\P\ f \\rv s. rv \ (Q rv s)\; \P\ f \\rv s. (\rv) \ (Q rv s)\\ \ \P\ f \Q\" - apply (clarsimp simp: valid_def) - apply (case_tac a, fastforce+) - done + apply (clarsimp simp: valid_def split_def) + by (metis (full_types) fst_eqD snd_conv) lemma combine_validE: "\ \ P \ x \ Q \,\ E \; \ P' \ x \ Q' \,\ E' \ \ @@ -718,23 +714,19 @@ lemma validE_pre_satisfies_post: lemma hoare_validE_R_conjI: "\ \P\ f \Q\, - ; \P\ f \Q'\, - \ \ \P\ f \\rv s. Q rv s \ Q' rv s\, -" - apply (clarsimp simp: Ball_def validE_R_def validE_def valid_def) - by (case_tac a; fastforce) + by (fastforce simp: Ball_def validE_R_def validE_def valid_def split: sum.splits) lemma hoare_validE_E_conjI: "\ \P\ f -, \Q\ ; \P\ f -, \Q'\ \ \ \P\ f -, \\rv s. Q rv s \ Q' rv s\" - apply (clarsimp simp: Ball_def validE_E_def validE_def valid_def) - by (case_tac a; fastforce) + by (fastforce simp: Ball_def validE_E_def validE_def valid_def split: sum.splits) lemma validE_R_post_conjD1: "\P\ f \\r s. Q r s \ R r s\,- \ \P\ f \Q\,-" - apply (clarsimp simp: validE_R_def validE_def valid_def) - by (case_tac a; fastforce) + by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits) lemma validE_R_post_conjD2: "\P\ f \\r s. Q r s \ R r s\,- \ \P\ f \R\,-" - apply (clarsimp simp: validE_R_def validE_def valid_def) - by (case_tac a; fastforce) + by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits) lemma throw_opt_wp[wp]: "\if v = None then E ex else Q (the v)\ throw_opt ex v \Q\,\E\" diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy index b441289ce4..ee7b6d915d 100644 --- a/lib/Monads/trace/Trace_RG.thy +++ b/lib/Monads/trace/Trace_RG.thy @@ -272,8 +272,8 @@ proof (induct n arbitrary: res) case 0 then show ?case by auto next case (Suc n) - have drop_1: "\tr res. (tr, res) \ f s \ \res'. (drop 1 tr, res') \ f s" - by (case_tac tr; fastforce dest: prefix_closedD[rotated] intro: Suc) + have drop_1: "(tr, res) \ f s \ \res'. (drop 1 tr, res') \ f s" for tr res + by (cases tr; fastforce dest: prefix_closedD[rotated] intro: Suc) show ?case using Suc.hyps[OF Suc.prems] by (metis drop_1[simplified] drop_drop add_0 add_Suc) @@ -291,7 +291,8 @@ lemma parallel_prefix_closed[wp_split]: "\prefix_closed f; prefix_closed g\ \ prefix_closed (parallel f g)" apply (subst prefix_closed_def, clarsimp simp: parallel_def) - apply (case_tac f_steps; clarsimp) + apply (subst (asm) zip.zip_Cons) + apply (clarsimp split: list.splits) apply (drule(1) prefix_closedD)+ apply fastforce done @@ -338,7 +339,7 @@ lemma guar_cond_drop_Suc: "\guar_cond R s0 (drop (Suc n) xs); fst (xs ! n) \ Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\ \ guar_cond R s0 (drop n xs)" - by (case_tac "n < length xs"; simp add: guar_cond_drop_Suc_eq) + by (cases "n < length xs"; simp add: guar_cond_drop_Suc_eq) lemma rely_cond_Cons_eq: "rely_cond R s0 (x # xs) @@ -427,8 +428,9 @@ proof - hd_drop_conv_nth hd_append) apply (fastforce simp: split_def intro!: nth_equalityI) apply clarsimp - apply (erule_tac x=n in meta_allE)+ apply (drule meta_mp, erule rely_cond_is_drop, simp) + apply clarsimp + apply (erule meta_allE, drule meta_mp, assumption)+ apply (subst(asm) rely_cond_drop_Suc_eq[where xs="map f xs" for f xs], simp) apply (clarsimp simp: last_st_tr_drop_map_zip_hd if_split[where P="\x. x = Env"] split_def) @@ -493,7 +495,7 @@ lemma put_trace_res: \ \n. tr = drop n xs \ n \ length xs \ res = (case n of 0 \ Result ((), s) | _ \ Incomplete)" apply (clarsimp simp: put_trace_eq_drop) - apply (case_tac n; auto intro: exI[where x=0]) + apply (auto simp: gr0_conv_Suc intro: exI[where x=0]) done lemma put_trace_twp[wp]: @@ -732,13 +734,16 @@ lemmas modify_prefix_closed[simp] = modify_wp[THEN valid_validI_wp[OF no_trace_all(3)], THEN validI_prefix_closed] lemmas await_prefix_closed[simp] = Await_sync_twp[THEN validI_prefix_closed] +lemma repeat_n_prefix_closed[intro!]: + "prefix_closed f \ prefix_closed (repeat_n n f)" + apply (induct n; simp) + apply (auto intro: prefix_closed_bind) + done + lemma repeat_prefix_closed[intro!]: "prefix_closed f \ prefix_closed (repeat f)" apply (simp add: repeat_def) apply (rule prefix_closed_bind; clarsimp) - apply (rename_tac n) - apply (induct_tac n; simp) - apply (auto intro: prefix_closed_bind) done lemma rely_cond_True[simp]: diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy index 7ffb2a7c13..bd68d0cedd 100644 --- a/lib/Monads/trace/Trace_VCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -1016,7 +1016,7 @@ lemmas liftME_E_E_wp[wp_split] = validE_validE_E [OF liftME_wp, simplified, OF v lemma assert_opt_wp: "\\s. x \ None \ Q (the x) s\ assert_opt x \Q\" unfolding assert_opt_def - by (case_tac x; wpsimp wp: fail_wp return_wp) + by (cases x; wpsimp wp: fail_wp return_wp) lemma gets_the_wp: "\\s. (f s \ None) \ Q (the (f s)) s\ gets_the f \Q\" diff --git a/lib/Monads/wp/WPFix.thy b/lib/Monads/wp/WPFix.thy index 1428c8fae7..619d43a0b9 100644 --- a/lib/Monads/wp/WPFix.thy +++ b/lib/Monads/wp/WPFix.thy @@ -242,11 +242,13 @@ lemma demo2: \ (\x. I x \ (case x of None \ R (Inl 8) | Some y \ R (Inr y))) \ (\x. I x \ (case x of None \ R (Inr 9) | Some y \ R (Inl (y - 1))))" apply (intro exI conjI[rotated] allI) + apply (rename_tac x) apply (case_tac x; simp) apply wpfix apply (rule P) apply wpfix apply (rule P) + apply (rename_tac x) apply (case_tac x; simp) apply wpfix apply (rule P) diff --git a/lib/Monads/wp/WPI.thy b/lib/Monads/wp/WPI.thy index f078015eb0..de84fbbaa8 100644 --- a/lib/Monads/wp/WPI.thy +++ b/lib/Monads/wp/WPI.thy @@ -116,6 +116,7 @@ private lemma (atomic f (\s. A' s \ Pres' s) (\r s. A r s \ Pres r s) B Q' \ trip Ts) \ trip Ts" apply (erule meta_mp) apply (clarsimp simp: valid_def atomic_def) + apply (rename_tac P s r s') apply (drule_tac x=P in spec) apply (drule_tac x=P in meta_spec) apply (drule_tac x=s in spec)+ From 82b9548170b782a73526394bcf8ee8b360bcf05c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 6 Oct 2023 19:52:21 +1030 Subject: [PATCH 15/67] clib: improve ccorres_call_getter_setter This generalises the rule ccorres_call_getter_setter by allowing the return relation between the "getter" and the C function called to be arbitrary, rather than just the identity relation. A variant of this rule, ccorres_call_getter_setter_dc, is provided for when we do not care about the return relation. Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 36 +++++++++++++++++++++++++++++++++++- lib/clib/Corres_UL_C.thy | 8 ++++---- 2 files changed, 39 insertions(+), 5 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 8f712fb50a..fe2425677c 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -5,7 +5,7 @@ *) theory CCorresLemmas -imports CCorres_Rewrite +imports CCorres_Rewrite MonadicRewrite_C begin lemma ccorres_rel_imp2: @@ -1177,4 +1177,38 @@ lemma ccorres_inr_rrel_Inr[simp]: = ccorres_underlying srel \ r xf ar axf P Q hs m c" by (simp cong: ccorres_context_cong)+ +lemma add_remove_return: + "getter >>= setter = do (do val \ getter; setter val; return val od); return () od" + by (simp add: bind_assoc) + +lemma ccorres_call_getter_setter_dc: + assumes cul: "ccorresG sr \ r' xf' P (i ` P') [] getter (Call f)" + and gsr: "\x x' s t rv. + \ (x, t) \ sr; r' rv (xf' t); ((), x') \ fst (setter rv x) \ + \ (x', g s t (clean s t)) \ sr" + and ist: "\x s. (x, s) \ sr \ (x, i s) \ sr" + and ef: "\val. empty_fail (setter val)" + shows "ccorresG sr \ dc xfdc P P' hs + (getter >>= setter) + (call i f clean (\s t. Basic (g s t)))" + apply (rule ccorres_guard_imp) + apply (rule monadic_rewrite_ccorres_assemble[rotated]) + apply (rule monadic_rewrite_is_refl) + apply (rule add_remove_return) + apply (rule ccorres_seq_skip'[THEN iffD1]) + apply (rule ccorres_split_nothrow_novcg) + apply (rule ccorres_call_getter_setter) + apply (fastforce intro: cul) + apply (fastforce intro: gsr) + apply (simp add: gsr) + apply (fastforce intro: ist) + apply (fastforce intro: ef) + apply (rule ceqv_refl) + apply (fastforce intro: ccorres_return_Skip) + apply wpsimp + apply (clarsimp simp: guard_is_UNIV_def) + apply wpsimp + apply fastforce + done + end diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index 2a5c678be8..9ba8fb9ab5 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -830,14 +830,14 @@ text \ between the values set on the concrete and abstract side. The @{thm bind_assoc_return_reverse} rule may assist with rewriting statements to add the extra return needed by this rule\ lemma ccorres_call_getter_setter: - assumes cul: "ccorresG sr \ (=) xf' P (i ` P') [] getter (Call f)" + assumes cul: "ccorresG sr \ r' xf' P (i ` P') [] getter (Call f)" and gsr: "\x x' s t rv rv'. - \ (x, t) \ sr; rv = xf' t; (rv', x') \ fst (setter rv x) \ + \ (x, t) \ sr; r' rv (xf' t); (rv', x') \ fst (setter rv x) \ \ (x', g s t (clean s t)) \ sr" - and res: "\s t rv. rv = xf' t \ rv = xf (g s t (clean s t))" + and res: "\s t rv. r' rv (xf' t) \ r rv (xf (g s t (clean s t)))" and ist: "\x s. (x, s) \ sr \ (x, i s) \ sr" and ef: "\val. empty_fail (setter val)" - shows "ccorresG sr \ (=) xf P P' hs + shows "ccorresG sr \ r xf P P' hs (do val \ getter; setter val; return val od) (call i f clean (\s t. Basic (g s t)))" apply (rule ccorresI') From 8c433c0850654403caa9f40dd6084cf65ec426e8 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 9 Oct 2023 11:37:13 +1030 Subject: [PATCH 16/67] clib: add some rules for hoarep Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 43 ---------------------------- lib/clib/SIMPL_Lemmas.thy | 58 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+), 43 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index fe2425677c..69d8fa2674 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -1040,49 +1040,6 @@ lemma ccorres_Guard_True_Seq: \ ccorres_underlying sr \ r xf arrel axf A C hs a (Guard F \True\ c ;; d)" by (simp, ccorres_rewrite, assumption) -lemma exec_While_final_inv'': - "\ \ \ \b, x\ \ s'; b = While C B; x = Normal s; - \s. s \ C \ I s (Normal s); - \t t' t''. \ t \ C; \\ \B, Normal t\ \ Normal t'; \\ \While C B, Normal t'\ \ t''; - I t' t'' \ \ I t t''; - \t t'. \ t \ C; \\ \B, Normal t\ \ Abrupt t' \ \ I t (Abrupt t'); - \t. \ t \ C; \ \ \B, Normal t\ \ Stuck \ \ I t Stuck; - \t f. \ t \ C; \\ \B, Normal t\ \ Fault f \ \ I t (Fault f) \ - \ I s s'" - apply (induct arbitrary: s rule: exec.induct; simp) - apply (erule exec_elim_cases; fastforce simp: exec.WhileTrue exec.WhileFalse) - done - -lemma intermediate_Normal_state: - "\\ \ \Seq c\<^sub>1 c\<^sub>2, Normal t\ \ t''; t \ P; \ \ P c\<^sub>1 Q\ - \ \t'. \ \ \c\<^sub>1, Normal t\ \ Normal t' \ \ \ \c\<^sub>2, Normal t'\ \ t''" - apply (erule exec_Normal_elim_cases(8)) - apply (insert hoarep_exec) - apply fastforce - done - -lemma While_inv_from_body: - "\ \ (G \ C) B G \ \ \ G While C B G" - apply (drule hoare_sound)+ - apply (rule hoare_complete) - apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) - by (erule exec_While_final_inv''[where I="\s s'. s \ G \ s' \ Normal ` G", THEN impE], - fastforce+) - -lemma While_inv_from_body_setter: - "\\ \ G setter (G \ {s. s \ C \ s \ Cnd}); \ \ (G \ Cnd) B G\ - \ \ \ (G \ {s. s \ C \ s \ Cnd}) While C (Seq B setter) G" - apply (drule hoare_sound)+ - apply (rule hoare_complete) - apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) - by (rule exec_While_final_inv'' - [where I="\s s'. s \ G \ (s \ C \ s \ Cnd) \ s' \ Normal ` G", THEN impE], - (fastforce dest!: intermediate_Normal_state[where c\<^sub>1=B and P="G \ Cnd" and Q=G] - intro: hoare_complete - simp: cvalid_def HoarePartialDef.valid_def)+) - -lemmas hoarep_Int_pre_fix = hoarep_Int[where P=P and P'=P for P, simplified] - lemma ccorres_While: assumes body_ccorres: "\r. ccorresG srel \ (=) xf (G and (\s. the (C r s))) (G' \ C') hs (B r) B'" diff --git a/lib/clib/SIMPL_Lemmas.thy b/lib/clib/SIMPL_Lemmas.thy index 6f4d592886..6cc9034016 100644 --- a/lib/clib/SIMPL_Lemmas.thy +++ b/lib/clib/SIMPL_Lemmas.thy @@ -72,6 +72,7 @@ lemma hoarep_Int: apply fastforce done +lemmas hoarep_Int_pre_fix = hoarep_Int[where P=P and P'=P for P, simplified] lemma Normal_result: "\ \ \c, s\ \ Normal t' \ \t. s = Normal t" @@ -350,5 +351,62 @@ lemma hoarep_revert: apply simp done +lemma intermediate_Normal_state: + "\\ \ \Seq c\<^sub>1 c\<^sub>2, Normal t\ \ t''; t \ P; \ \ P c\<^sub>1 Q\ + \ \t'. \ \ \c\<^sub>1, Normal t\ \ Normal t' \ \ \ \c\<^sub>2, Normal t'\ \ t''" + apply (erule exec_Normal_elim_cases(8)) + apply (insert hoarep_exec) + apply fastforce + done + +lemma hoarep_ex_pre: + "(\x. \ \ {s. P x s} c Q) \ \ \ {s. \x. P x s} c Q" + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + apply (fastforce dest: hoarep_exec'[rotated]) + done + +lemma hoarep_ex_lift: + "(\x. \ \ {s. P x s} c {s. Q x s}) \ \ \ {s. \x. P x s} c {s. \x. Q x s}" + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + apply (rename_tac s x) + apply (drule_tac x=x in meta_spec) + apply (prop_tac "s \ Collect (P x)") + apply fastforce + apply (frule (2) hoarep_exec) + apply fastforce + done + +lemma hoarep_conj_lift_pre_fix: + "\\ \ P c {s. Q s}; \ \ P c {s. Q' s}\ + \ \ \ P c {s. Q s \ Q' s}" + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + apply (frule (2) hoarep_exec[where Q="Collect Q"]) + apply (frule (2) hoarep_exec[where Q="Collect Q'"]) + apply fastforce + done + +lemma exec_While_final_inv'': + "\ \ \ \b, x\ \ s'; b = While C B; x = Normal s; + \s. s \ C \ I s (Normal s); + \t t' t''. \ t \ C; \\ \B, Normal t\ \ Normal t'; \\ \While C B, Normal t'\ \ t''; + I t' t'' \ \ I t t''; + \t t'. \ t \ C; \\ \B, Normal t\ \ Abrupt t' \ \ I t (Abrupt t'); + \t. \ t \ C; \ \ \B, Normal t\ \ Stuck \ \ I t Stuck; + \t f. \ t \ C; \\ \B, Normal t\ \ Fault f \ \ I t (Fault f) \ + \ I s s'" + apply (induct arbitrary: s rule: exec.induct; simp) + apply (erule exec_elim_cases; fastforce simp: exec.WhileTrue exec.WhileFalse) + done + +lemma While_inv_from_body: + "\ \ (G \ C) B G \ \ \ G While C B G" + apply (drule hoare_sound)+ + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + by (erule exec_While_final_inv''[where I="\s s'. s \ G \ s' \ Normal ` G", THEN impE], + fastforce+) end From 49ff8457f2f07173dd88e5ab17e21a4500d0a870 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 6 Oct 2023 20:09:31 +1030 Subject: [PATCH 17/67] clib+crefine: improve and consolidate variants of ccorres_to_vcg Signed-off-by: Michael McInerney --- lib/clib/Corres_UL_C.thy | 53 ++++++++++++++++-------------- proof/crefine/ARM_HYP/Retype_C.thy | 15 --------- proof/crefine/RISCV64/Retype_C.thy | 15 --------- proof/crefine/X64/Retype_C.thy | 15 --------- 4 files changed, 28 insertions(+), 70 deletions(-) diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index 9ba8fb9ab5..2ec5b2c808 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -288,26 +288,37 @@ lemma ccorres_from_vcg_nofail: apply (rule hoare_complete, simp add: HoarePartialDef.valid_def) done - -lemma ccorres_to_vcg: - "ccorres_underlying srel \ rrel xf arrel axf P P' [] a c \ - (\\. \ snd (a \) \ \ \ {s. P \ \ s \ P' \ (\, s) \ srel} - c - {s. (\(rv, \') \ fst (a \). (\', s) \ srel \ rrel rv (xf s))})" - apply - - apply rule - apply (rule impI) +lemma ccorres_to_vcg_with_prop: + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; no_fail Q a; \P\ a \R\\ + \ \ \ {s'. P s \ Q s \ s' \ P' \ (s, s') \ srel} + c {t'. \(rv, t) \ fst (a s). (t, t') \ srel \ rrel rv (xf t') \ R rv t}" apply (rule hoare_complete) - apply (simp add: HoarePartialDef.valid_def cvalid_def) - apply (intro impI allI) + apply (clarsimp simp: HoarePartialDef.valid_def cvalid_def no_fail_def) + apply (drule_tac x=s in spec) apply clarsimp apply (frule (5) ccorres_empty_handler_abrupt) - apply (erule (4) ccorresE) - apply (erule (1) EHOther) - apply clarsimp - apply rule - apply simp - apply (fastforce simp: unif_rrel_simps) + apply (fastforce elim!: ccorresE EHOther simp: unif_rrel_simps valid_def) + done + +lemma ccorres_to_vcg: + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; no_fail Q a\ + \ \ \ {s'. P s \ Q s \ s' \ P' \ (s, s') \ srel} + c {t'. \(rv, t) \ fst (a s). (t, t') \ srel \ rrel rv (xf t')}" + apply (frule (1) ccorres_to_vcg_with_prop[where R="\\"]) + apply wpsimp + apply fastforce + done + +lemma ccorres_to_vcg_gets_the: + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\ + \ \ \ (P' \ {s'. (s, s') \ srel \ P s}) + c {t'. (s, t') \ srel \ P s \ (r s \ None) \ rrel (the (r s)) (xf t')}" + apply (frule ccorres_to_vcg_with_prop[where R="\_. P" and s=s]) + apply (erule no_ofail_gets_the) + apply wpsimp + apply (clarsimp simp: gets_the_def simpler_gets_def bind_def return_def get_def assert_opt_def + fail_def conseq_under_new_pre + split: option.splits) done lemma exec_handlers_Seq_cases0': @@ -1402,14 +1413,6 @@ lemma ccorres_move_Guard: section "novcg" -lemma ccorres_to_vcg': - "\ ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; \ snd (a \) \ \ - \\ {s. P \ \ s \ P' \ (\, s) \ srel} c - {s. \(rv, \')\fst (a \). (\', s) \ srel \ rrel rv (xf s)}" - apply (drule ccorres_to_vcg) - apply clarsimp - done - lemma exec_handlers_Hoare_UNIV: "guard_is_UNIV r xf Q \ exec_handlers_Hoare \ UNIV cs (ccHoarePost r xf Q) UNIV" diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy index 767dcac4dc..23030fcc21 100644 --- a/proof/crefine/ARM_HYP/Retype_C.thy +++ b/proof/crefine/ARM_HYP/Retype_C.thy @@ -2422,21 +2422,6 @@ next done qed -(* FIXME: move *) -lemma ccorres_to_vcg_nf: - "\ccorres rrel xf P P' [] a c; no_fail Q a; \s. P s \ Q s\ - \ \\ {s. P \ \ s \ P' \ (\, s) \ rf_sr} c - {s. \(rv, \')\fst (a \). (\', s) \ rf_sr \ rrel rv (xf s)}" - apply (rule HoarePartial.conseq_exploit_pre) - apply clarsimp - apply (rule conseqPre) - apply (drule ccorres_to_vcg') - prefer 2 - apply simp - apply (simp add: no_fail_def) - apply clarsimp - done - lemma mdb_node_get_mdbNext_heap_ccorres: "ccorres (=) ret__unsigned_' \ UNIV hs (liftM (mdbNext \ cteMDBNode) (getCTE parent)) diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy index dfadb59a5e..07db6d2d96 100644 --- a/proof/crefine/RISCV64/Retype_C.thy +++ b/proof/crefine/RISCV64/Retype_C.thy @@ -2225,21 +2225,6 @@ next done qed -(* FIXME: move *) -lemma ccorres_to_vcg_nf: - "\ccorres rrel xf P P' [] a c; no_fail Q a; \s. P s \ Q s\ - \ \\ {s. P \ \ s \ P' \ (\, s) \ rf_sr} c - {s. \(rv, \')\fst (a \). (\', s) \ rf_sr \ rrel rv (xf s)}" - apply (rule HoarePartial.conseq_exploit_pre) - apply clarsimp - apply (rule conseqPre) - apply (drule ccorres_to_vcg') - prefer 2 - apply simp - apply (simp add: no_fail_def) - apply clarsimp - done - lemma mdb_node_get_mdbNext_heap_ccorres: "ccorres (=) ret__unsigned_longlong_' \ UNIV hs (liftM (mdbNext \ cteMDBNode) (getCTE parent)) diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy index 4f37ce630d..ba09bf95e1 100644 --- a/proof/crefine/X64/Retype_C.thy +++ b/proof/crefine/X64/Retype_C.thy @@ -2771,21 +2771,6 @@ next done qed -(* FIXME: move *) -lemma ccorres_to_vcg_nf: - "\ccorres rrel xf P P' [] a c; no_fail Q a; \s. P s \ Q s\ - \ \\ {s. P \ \ s \ P' \ (\, s) \ rf_sr} c - {s. \(rv, \')\fst (a \). (\', s) \ rf_sr \ rrel rv (xf s)}" - apply (rule HoarePartial.conseq_exploit_pre) - apply clarsimp - apply (rule conseqPre) - apply (drule ccorres_to_vcg') - prefer 2 - apply simp - apply (simp add: no_fail_def) - apply clarsimp - done - lemma mdb_node_get_mdbNext_heap_ccorres: "ccorres (=) ret__unsigned_longlong_' \ UNIV hs (liftM (mdbNext \ cteMDBNode) (getCTE parent)) From b3c6df48a2e1667e84a2f6453e1fa56fe1a3bbc4 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 9 Oct 2023 11:50:59 +1030 Subject: [PATCH 18/67] clib: improve ccorres_While Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 199 +++++++++++++++++++++++++++++-------- 1 file changed, 160 insertions(+), 39 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 69d8fa2674..bb467af531 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -1040,76 +1040,197 @@ lemma ccorres_Guard_True_Seq: \ ccorres_underlying sr \ r xf arrel axf A C hs a (Guard F \True\ c ;; d)" by (simp, ccorres_rewrite, assumption) +lemma ccorres_While_Normal_helper: + assumes setter_inv: + "\ \ {s'. \rv s. G rv s s'} setter {s'. \rv s. G rv s s' \ (cond_xf s' \ 0 \ Cnd rv s s')}" + assumes body_inv: "\ \ {s'. \rv s. G rv s s' \ Cnd rv s s'} B {s'. \rv s. G rv s s'}" + shows "\ \ ({s'. \rv s. G rv s s' \ (cond_xf s' \ 0 \ Cnd rv s s')}) + While {s'. cond_xf s' \ 0} (Seq B setter) + {s'. \rv s. G rv s s'}" + apply (insert assms) + apply (rule hoare_complete) + apply (simp add: cvalid_def HoarePartialDef.valid_def) + apply (intro allI) + apply (rename_tac xstate xstate') + apply (rule impI) + apply (case_tac "\ isNormal xstate") + apply fastforce + apply (simp add: isNormal_def) + apply (elim exE) + apply (simp add: image_def) + apply (erule exec_While_final_inv''[where C="{s'. cond_xf s' \ 0}" and B="B;; setter"]; clarsimp) + apply (frule intermediate_Normal_state[OF _ _ body_inv]) + apply fastforce + apply clarsimp + apply (rename_tac inter_t) + apply (frule hoarep_exec[OF _ _ body_inv, rotated], fastforce) + apply (frule_tac s=inter_t in hoarep_exec[rotated 2], fastforce+)[1] + apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_abrupt mem_Collect_eq) + apply (metis (mono_tags, lifting) HoarePartial.SeqSwap exec_stuck mem_Collect_eq) + apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_fault mem_Collect_eq) + done + lemma ccorres_While: assumes body_ccorres: - "\r. ccorresG srel \ (=) xf (G and (\s. the (C r s))) (G' \ C') hs (B r) B'" - and cond_ccorres: - "\r. ccorresG srel \ (\rv rv'. rv = to_bool rv') cond_xf G G' hs (gets_the (C r)) setter" - and nf: "\r. no_fail (G and (\s. the (C r s))) (B r)" - and no_ofail: "\r. no_ofail G (C r)" - and body_inv: "\r. \G and (\s. the (C r s))\ B r \\_. G\" - "\ \ (G' \ C') B' G'" - and setter_inv_cond: "\ \ G' setter (G' \ {s'. cond_xf s' \ 0 \ s' \ C'})" - and setter_xf_inv: "\val. \ \ {s'. xf s' = val} setter {s'. xf s' = val}" - shows "ccorresG srel \ (=) xf G (G' \ {s'. xf s' = r}) hs - (whileLoop (\r s. the (C r s)) B r) - (Seq setter (While {s'. cond_xf s' \ 0} (Seq B' setter)))" + "\r. ccorresG srel \ rrel xf (\s. G r s \ C r s = Some True) (G' \ C') [] (B r) B'" + assumes setter_ccorres: + "\r. ccorresG srel \ (\rv rv'. rv = to_bool rv') cond_xf (G r) G' [] (gets_the (C r)) setter" + assumes nf: "\r. no_fail (\s. G r s \ C r s = Some True) (B r)" + assumes no_ofail: "\r. no_ofail (G r) (C r)" + assumes body_inv: + "\r. \\s. G r s \ C r s = Some True\ B r \G\" + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s') + \ s' \ C' \ C r s = Some True} + B' G'" + assumes setter_inv_cond: + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} + setter + {s'. s' \ G' \ (cond_xf s' \ 0 \ s' \ C')}" + assumes setter_rrel: + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} + setter + {s'. rrel r (xf s')}" + shows + "ccorresG srel \ rrel xf (G r) (G' \ {s'. rrel r (xf s')}) hs + (whileLoop (\r s. the (C r s)) B r) + (setter;; (While {s'. cond_xf s' \ 0} (B';; setter)))" proof - note unif_rrel_def[simp add] to_bool_def[simp add] have helper: "\state xstate'. \ \ \While {s'. cond_xf s' \ 0} (Seq B' setter), Normal state\ \ xstate' \ \st r s. Normal st = xstate' \ (s, state) \ srel - \ (cond_xf state \ 0) = the (C r s) \ xf state = r \ G s - \ state \ G' \ (cond_xf state \ 0 \ state \ C') + \ (C r s \ None) \ (cond_xf state \ 0) = the (C r s) + \ rrel r (xf state) \ G r s \ state \ G' \ (cond_xf state \ 0 \ state \ C') \ (\rv s'. (rv, s') \ fst (whileLoop (\r s. the (C r s)) B r s) - \ (s', st) \ srel \ rv = xf st)" - apply (erule exec_While_final_inv''; simp) + \ (s', st) \ srel \ rrel rv (xf st))" + apply (erule_tac C="{s'. cond_xf s' \ 0}" in exec_While_final_inv''; simp) apply (fastforce simp: whileLoop_cond_fail return_def) apply clarsimp - apply (rename_tac t t' t'' s) - apply (frule intermediate_Normal_state[where P="G' \ C'"]) + apply (rename_tac t t' t'' r s y) + apply (frule_tac P="{s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s') + \ s' \ C' \ (C r s \ None) \ the (C r s)}" + in intermediate_Normal_state) apply fastforce - apply (fastforce intro: body_inv) + apply (fastforce intro: body_inv conseqPre) apply clarsimp apply (rename_tac inter_t) - apply (prop_tac "\s'. (xf inter_t, s') \ fst (B (xf t) s) \ (s', inter_t) \ srel") - subgoal by (erule ccorresE[OF body_ccorres]) - (fastforce simp: no_fail_def nf[simplified no_fail_def] dest: EHOther)+ + apply (prop_tac "\rv' s'. rrel rv' (xf inter_t) \ (rv', s') \ fst (B r s) + \ (s', inter_t) \ srel") + apply (insert body_ccorres)[1] + apply (drule_tac x=r in meta_spec) + apply (erule (1) ccorresE) + apply fastforce + apply fastforce + using nf apply (fastforce simp: no_fail_def) + apply (fastforce dest!: EHOther) + apply fastforce apply clarsimp - apply (prop_tac "G s'") + apply (prop_tac "G rv' s'") apply (fastforce dest: use_valid intro: body_inv) apply (prop_tac "inter_t \ G'") apply (fastforce dest: hoarep_exec[rotated] intro: body_inv) + apply (drule_tac x=rv' in spec) apply (drule_tac x=s' in spec) + apply (prop_tac "rrel rv' (xf inter_t)") + apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated]) apply (elim impE) - apply (drule_tac s'=inter_t and r1="xf t'" in ccorresE_gets_the[OF cond_ccorres]; assumption?) + apply (frule_tac s'=inter_t and r1=rv' in ccorresE_gets_the[OF setter_ccorres]; assumption?) apply (fastforce intro: no_ofail) apply (fastforce dest: EHOther) - subgoal by (fastforce dest: hoarep_exec intro: setter_inv_cond) - apply (prop_tac "xf inter_t = xf t'") - apply (fastforce dest: hoarep_exec[rotated] intro: setter_xf_inv) + apply (intro conjI) + apply fastforce + using no_ofail apply (fastforce elim!: no_ofailD) + apply fastforce + apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated]) apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3)) done + have setter_hoarep: + "\r s s' n xstate. + \\\<^sub>h \(setter;; While {s'. cond_xf s' \ 0} (B';; setter)) # hs,s'\ \ (n, xstate) + \ \\ {s' \ G'. (s, s') \ srel \ G r s \ rrel r (xf s')} + setter + {s'. (s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')) + \ (cond_xf s' \ 0 \ (s' \ C' \ C r s = Some True))}" + apply (insert setter_ccorres) + apply (drule_tac x=r in meta_spec) + apply (frule_tac s=s in ccorres_to_vcg_gets_the) + apply (fastforce intro: no_ofail) + apply (insert setter_rrel) + apply (drule_tac x=s in meta_spec) + apply (drule_tac x=r in meta_spec) + apply (rule hoarep_conj_lift_pre_fix) + apply (rule hoarep_conj_lift_pre_fix) + apply (insert setter_inv_cond)[1] + apply (drule_tac x=s in meta_spec) + apply (drule_tac x=r in meta_spec) + apply (rule_tac Q'="{s' \ G'. cond_xf s' \ 0 \ s' \ C'}" in conseqPost; fastforce) + apply (fastforce intro!: hoarep_conj_lift_pre_fix simp: Collect_mono conseq_under_new_pre) + apply (insert setter_inv_cond) + apply (drule_tac x=s in meta_spec) + apply (drule_tac x=r in meta_spec) + apply (simp add: imp_conjR) + apply (rule hoarep_conj_lift_pre_fix) + apply (simp add: Collect_mono conseq_under_new_pre) + apply (rule_tac Q'="{s'. C r s \ None \ the (C r s) = (cond_xf s' \ 0)}" + in conseqPost[rotated]) + apply fastforce + apply fastforce + apply (simp add: Collect_mono conseq_under_new_pre) + done + show ?thesis apply (clarsimp simp: ccorres_underlying_def) apply (rename_tac s s' n xstate) - apply (frule (1) exec_handlers_use_hoare_nothrow_hoarep) - apply (rule_tac R="G' \ {s'. s' \ {t. cond_xf t \ 0} \ s' \ C'}" in HoarePartial.Seq) - apply (fastforce intro: setter_inv_cond) - apply (fastforce intro: While_inv_from_body_setter setter_inv_cond body_inv) - apply clarsimp - apply (frule (1) intermediate_Normal_state) - apply (fastforce intro: setter_inv_cond) + apply (frule_tac R'="{s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')}" + and Q'="{s'. \rv s. s' \ G' \ (s, s') \ srel \ G rv s \ rrel rv (xf s')}" + in exec_handlers_use_hoare_nothrow_hoarep) + apply fastforce + apply (rule HoarePartial.Seq) + apply (erule setter_hoarep) + apply (rule conseqPre) + apply (rule ccorres_While_Normal_helper) + apply (fastforce intro!: setter_hoarep hoarep_ex_lift) + apply (intro hoarep_ex_pre, rename_tac rv new_s) + apply (insert setter_inv_cond)[1] + apply (drule_tac x=new_s in meta_spec) + apply (drule_tac x=rv in meta_spec) + apply (insert body_ccorres)[1] + apply (drule_tac x=rv in meta_spec) + apply (insert body_inv(2))[1] + apply (drule_tac x=new_s in meta_spec) + apply (drule_tac x=rv in meta_spec) + apply (frule_tac s=new_s in ccorres_to_vcg_with_prop) + using nf apply fastforce + using body_inv apply fastforce + apply (rule_tac Q'="{s'. s' \ G' + \ (\(rv, s) \fst (B rv new_s). (s, s') \ srel \ rrel rv (xf s') + \ G rv s)}" + in conseqPost; + fastforce?) + apply (rule hoarep_conj_lift_pre_fix; + fastforce simp: Collect_mono conseq_under_new_pre) + apply fastforce + apply (case_tac xstate; clarsimp) + apply (frule intermediate_Normal_state[OF _ _ setter_hoarep]; assumption?) + apply fastforce apply clarsimp apply (rename_tac inter_t) - apply (drule (2) ccorresE_gets_the[OF cond_ccorres _ _ _ no_ofail]) + apply (insert setter_ccorres) + apply (drule_tac x=r in meta_spec) + apply (drule (3) ccorresE_gets_the) + apply (fastforce intro: no_ofail) apply (fastforce dest: EHOther) - apply (prop_tac "xf inter_t = xf s'") - apply (fastforce dest: hoarep_exec[rotated] intro: setter_xf_inv) - apply (clarsimp simp: isNormal_def) - apply (auto dest: hoarep_exec dest!: helper spec intro: setter_inv_cond) + apply (prop_tac "rrel r (xf inter_t)") + apply (fastforce dest: hoarep_exec[rotated] intro: setter_rrel) + apply (case_tac "\ the (C r s)") + apply (fastforce elim: exec_Normal_elim_cases simp: whileLoop_cond_fail return_def) + apply (insert no_ofail) + apply (fastforce dest!: helper hoarep_exec[OF _ _ setter_inv_cond, rotated] no_ofailD) done qed From 1fa8d8c08f8e9fc500169ba38431b90cfd62da00 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 28 Oct 2023 09:35:02 +1100 Subject: [PATCH 19/67] cspec: adjust for kernel build change PR seL4/seL4#1105 moves config generation back to configure time. This means we can revert eaf735c38f. Signed-off-by: Gerwin Klein --- spec/cspec/c/kernel.mk | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/cspec/c/kernel.mk b/spec/cspec/c/kernel.mk index f6a973404c..98a9f1dc85 100644 --- a/spec/cspec/c/kernel.mk +++ b/spec/cspec/c/kernel.mk @@ -148,7 +148,6 @@ ${CONFIG_DONE}: ${KERNEL_DEPS} gen-config-thy.py ${OVERLAY} ${KERNEL_CMAKE_OPTIMISATION} ${KERNEL_CMAKE_EXTRA_OPTIONS} \ ${OVERLAY_OPT} \ -G Ninja ${SOURCE_ROOT} - cd ${KERNEL_CONFIG_ROOT} && ninja gen_config/kernel/gen_config.json @touch ${CONFIG_DONE} ifneq ($(L4V_ARCH),X64) @if [ "$$(diff -q ${OVERLAY} ${DEFAULT_OVERLAY})" ]; then \ From 7a4b08160c9ae61f3b2d026974955ce9de426d86 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 09:34:38 +1100 Subject: [PATCH 20/67] c-parser: remove obsolete mkrelease checks The @License tags are no longer used, and SPDX tags are checked in CI, and name tags are no longer used in the sources either. Signed-off-by: Gerwin Klein --- tools/c-parser/mkrelease | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/tools/c-parser/mkrelease b/tools/c-parser/mkrelease index be3278e6ee..4df89e63b2 100755 --- a/tools/c-parser/mkrelease +++ b/tools/c-parser/mkrelease @@ -183,7 +183,6 @@ sed ' ' < standalone-parser/Makefile > "$outputdir/src/c-parser/standalone-parser/Makefile" popd > /dev/null - echo "Making PDF of ctranslation file." cd "$outputdir/src/c-parser/doc" make ctranslation.pdf > /dev/null @@ -192,22 +191,6 @@ mv ctranslation.pdf "$outputdir/doc" popd > /dev/null -lookforlicense=$(find "$outputdir" \! -name '*.lex.sml' \! -name '*.grm.sml' \! -type d -exec grep -q @LICENSE \{\} \; -print) -if [ -n "$lookforlicense" ] -then - die "### @LICENSE detected in file(s) $lookforlicense" -else - echo "No @LICENSEs remain unexpanded - good." -fi - -lookformichaeln=$(find "$outputdir" \! -name RELEASES.md \! -type d -exec grep -q /michaeln \{\} \; -print) -if [ -n "$lookformichaeln" ] -then - die "### /michaeln detected in file(s) $lookformichaeln" -else - echo "No occurrences of \"/michaeln\" - good." -fi - echo -n "Compressing into $stem.tar.gz: " mv "$tmpdir/c-parser" "$tmpdir/$stem" From a9f492672c1c4579ab0291be6b824ef2e88b2c91 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 09:36:58 +1100 Subject: [PATCH 21/67] c-parser: clarify mkrelease command line The script does not expect the tag (e.g. c-parser-1.20), but only the version number in the tag. Signed-off-by: Gerwin Klein --- tools/c-parser/mkrelease | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tools/c-parser/mkrelease b/tools/c-parser/mkrelease index 4df89e63b2..f03d54d289 100755 --- a/tools/c-parser/mkrelease +++ b/tools/c-parser/mkrelease @@ -32,7 +32,8 @@ die () if [ $# -ne 1 ] then echo "Usage:" >&2 - die " $0 tag" >&2 + echo " $0 " + die "e.g. $0 1.20" >&2 fi # Get the directory that this script is running in. From 4e55740215272285eba453920820df4c726087d9 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 09:42:57 +1100 Subject: [PATCH 22/67] c-parser: update mkrelease for changed lib sessions - Basics and ML_Utils are their own sessions now; include their ROOT files - remove separate obsolete lib/ROOT file Signed-off-by: Gerwin Klein --- tools/c-parser/mkrelease | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/tools/c-parser/mkrelease b/tools/c-parser/mkrelease index f03d54d289..97afbdddd4 100755 --- a/tools/c-parser/mkrelease +++ b/tools/c-parser/mkrelease @@ -110,27 +110,17 @@ done # other misc files cp -v lib/Word_Lib/ROOT "$outputdir/src/lib/Word_Lib/" +cp -v lib/Basics/ROOT "$outputdir/src/lib/Basics/" +cp -v lib/ML_Utils/ROOT "$outputdir/src/lib/ML_Utils/" echo "Creating ROOTS file" cat >"$outputdir/src/ROOTS" < "$outputdir/src/lib/ROOT" < Date: Fri, 3 Nov 2023 10:01:56 +1100 Subject: [PATCH 23/67] c-parser: bump Isabelle version in docs Signed-off-by: Gerwin Klein --- tools/c-parser/INSTALL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/c-parser/INSTALL.md b/tools/c-parser/INSTALL.md index 0fb46808f0..67f05281c0 100644 --- a/tools/c-parser/INSTALL.md +++ b/tools/c-parser/INSTALL.md @@ -9,7 +9,7 @@ NB: These instructions apply to the stand-alone release of the C parser. If this is in an L4.verified checkout, see the top-level README.md instead. -This code requires Isabelle2021 and the MLton SML compiler. +This code requires Isabelle2023 and the MLton SML compiler. The C parser supports multiple target architectures: From a46083c6597aa563db0cc3258d3016f47d590698 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 10:02:09 +1100 Subject: [PATCH 24/67] autocorres: bump Isabelle version in docs Signed-off-by: Gerwin Klein --- tools/autocorres/tools/release_files/README | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/autocorres/tools/release_files/README b/tools/autocorres/tools/release_files/README index 74ca3cdba3..85a2444f1e 100644 --- a/tools/autocorres/tools/release_files/README +++ b/tools/autocorres/tools/release_files/README @@ -28,7 +28,7 @@ Contents of this README Installation ------------ -AutoCorres is packaged as a theory for Isabelle2021: +AutoCorres is packaged as a theory for Isabelle2023: https://isabelle.in.tum.de From 5a8dea120c37ca57daa29360fab9181f45b9acc6 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 10:07:51 +1100 Subject: [PATCH 25/67] c-parser: update change log for upcoming release Signed-off-by: Gerwin Klein --- tools/c-parser/RELEASES.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tools/c-parser/RELEASES.md b/tools/c-parser/RELEASES.md index 661fff8f9b..58c9473433 100644 --- a/tools/c-parser/RELEASES.md +++ b/tools/c-parser/RELEASES.md @@ -156,3 +156,9 @@ ##: e.g. `##Function: ctzl` + +## 1.20 + +- Builds with Isabelle2023 +- Rearranged library session structure and included more libraries for heap + reasoning in the release. See e.g. files TypHeapLib.thy and LemmaBucket_C.thy From 723620f084b1d784394f4f7c2512a3eca6e9d917 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 10:12:07 +1100 Subject: [PATCH 26/67] autocorres: update change log for upcoming release Signed-off-by: Gerwin Klein --- tools/autocorres/tools/release_files/ChangeLog | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tools/autocorres/tools/release_files/ChangeLog b/tools/autocorres/tools/release_files/ChangeLog index 45bea706bc..3e58f0847f 100644 --- a/tools/autocorres/tools/release_files/ChangeLog +++ b/tools/autocorres/tools/release_files/ChangeLog @@ -1,3 +1,11 @@ +AutoCorres 1.10 (3 Nov 2023) +-------------- + + * Isabelle2023 edition of both AutoCorres and the C parser. + + * Restructured and cleaned up monad libraries. Removed dependencies + on unrelated l4v libraries. + AutoCorres 1.9 (31 October 2022) -------------- From de58596f23a7d9709be4a467613a69fffc780e2b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 10:15:34 +1100 Subject: [PATCH 27/67] autocorres: format ChangeLog - convert tabs to spaces - add top-level heading - underline headings more nicely Signed-off-by: Gerwin Klein --- .../autocorres/tools/release_files/ChangeLog | 48 ++++++++++--------- 1 file changed, 26 insertions(+), 22 deletions(-) diff --git a/tools/autocorres/tools/release_files/ChangeLog b/tools/autocorres/tools/release_files/ChangeLog index 3e58f0847f..e95f216e9b 100644 --- a/tools/autocorres/tools/release_files/ChangeLog +++ b/tools/autocorres/tools/release_files/ChangeLog @@ -1,51 +1,55 @@ +AutoCorres Change Log +===================== + AutoCorres 1.10 (3 Nov 2023) --------------- +---------------------------- - * Isabelle2023 edition of both AutoCorres and the C parser. + * Isabelle2023 edition of both AutoCorres and the C parser. - * Restructured and cleaned up monad libraries. Removed dependencies + * Restructured and cleaned up monad libraries. Removed dependencies on unrelated l4v libraries. AutoCorres 1.9 (31 October 2022) --------------- +-------------------------------- - * Isabelle2021-1 edition of both AutoCorres and the C parser. + * Isabelle2021-1 edition of both AutoCorres and the C parser. AutoCorres 1.8 (31 October 2021) --------------- +-------------------------------- - * Isabelle2021 edition of both AutoCorres and the C parser. + * Isabelle2021 edition of both AutoCorres and the C parser. AutoCorres 1.7 (2 November 2020) --------------- +-------------------------------- - * Isabelle2020 edition of both AutoCorres and the C parser. + * Isabelle2020 edition of both AutoCorres and the C parser. - * Slight updates to wp: use "wp (once)" instead of "wp_once" + * Slight updates to wp: use "wp (once)" instead of "wp_once" AutoCorres 1.6.1 (3 October 2019) ----------------- - * Correct license for a C parser file. No code changes. +--------------------------------- + + * Correct license for a C parser file. No code changes. AutoCorres 1.6 (5 September 2019) --------------- +---------------------------------- - * Isabelle2019 edition of both AutoCorres and the C parser. + * Isabelle2019 edition of both AutoCorres and the C parser. - * Word abstraction has been extended to C bitwise operators. + * Word abstraction has been extended to C bitwise operators. AutoCorres 1.5 (10 September 2018) --------------- +---------------------------------- - * Isabelle2018 edition of both AutoCorres and the C parser. + * Isabelle2018 edition of both AutoCorres and the C parser. AutoCorres 1.4 (2 March 2018) --------------- +----------------------------- * Isabelle2017 edition of both AutoCorres and the C parser. AutoCorres 1.3 (3 April 2017) --------------- +----------------------------- * Isabelle2016-1 edition of both AutoCorres and the C parser. @@ -54,7 +58,7 @@ AutoCorres 1.3 (3 April 2017) must be selected using L4V_ARCH environment variable. AutoCorres 1.2 (31 March 2016) --------------- +------------------------------ * Isabelle2016 edition of both AutoCorres and the C parser. @@ -67,7 +71,7 @@ AutoCorres 1.2 (31 March 2016) * Several minor bug fixes and improvements. AutoCorres 1.1 (9 Oct 2015) --------------- +--------------------------- * Isabelle2015 edition of both AutoCorres and the C parser. @@ -85,7 +89,7 @@ AutoCorres 1.1 (9 Oct 2015) AutoCorres 1.0 (16 Dec 2014) --------------- +---------------------------- * New option “no_opt” to turn off simplifier stages. (Experimental) From 4743f0bb5753223ad3bfd68cde4b1b8d81228ada Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 10:21:48 +1100 Subject: [PATCH 28/67] autocorres: update release ROOT files and manifest AutoCorres no longer depends on the Lib session. This means: - remove Lib session ROOT parsing in release.py - copy over ROOT files of new library sessions - add new theory NatBitWise to manifest - update release ROOTS and ROOT files Signed-off-by: Gerwin Klein --- tools/autocorres/tools/release.py | 33 +++---------------- .../tools/release_files/AUTOCORRES_FILES | 1 + .../tools/release_files/ROOT.release | 5 ++- .../tools/release_files/ROOTS.base_dir | 5 ++- 4 files changed, 11 insertions(+), 33 deletions(-) diff --git a/tools/autocorres/tools/release.py b/tools/autocorres/tools/release.py index 6e3f03ca1a..7acfbcb06f 100755 --- a/tools/autocorres/tools/release.py +++ b/tools/autocorres/tools/release.py @@ -200,9 +200,10 @@ def copy_manifest(output_dir, manifest_file, manifest_base, target): shutil.copyfile(f_src, f_dest) # Copy various other files. - shutil.copyfile( - os.path.join(args.repository, 'lib', 'Word_Lib', 'ROOT'), - os.path.join(target_dir, 'lib', 'Word_Lib', 'ROOT')) + for session in ['Basics', 'Eisbach_Tools', 'ML_Utils', 'Monads', 'Word_Lib']: + shutil.copyfile( + os.path.join(args.repository, 'lib', session, 'ROOT'), + os.path.join(target_dir, 'lib', session, 'ROOT')) shutil.copyfile( os.path.join(release_files_dir, "ROOT.release"), os.path.join(target_dir, "autocorres", "ROOT")) @@ -222,37 +223,11 @@ def copy_manifest(output_dir, manifest_file, manifest_base, target): os.path.join(args.repository, "LICENSES"), os.path.join(target_dir, "LICENSES")) - # Extract dependent sessions in lib. FIXME: rather kludgy - print('Extracting sessions from lib/ROOT...') - # Set up ROOT for the tests dir, for the thydeps tool subprocess.check_call( ['make', 'tests/ROOT'], cwd=os.path.join(args.repository, 'tools', 'autocorres')) - lib_sessions = ['Lib', 'CLib'] - lib_ROOT = os.path.join(args.repository, 'lib', 'ROOT') - with open(lib_ROOT, 'r') as lib_root: - data = lib_root.read() - # Split out session specs. Assume ROOT file has standard indentation. - chunks = data.split('\nsession ') - # This will have the license header, etc. - header = chunks[0] - # Remaining sections. Try to remove comments - sessions = ['session ' + re.sub(r'\(\*.*?\*\)', '', x, flags=re.DOTALL) - for x in chunks[1:]] - - new_root = header - wanted_specs = {} - for wanted in lib_sessions: - spec = [spec for spec in sessions if spec.startswith('session %s ' % wanted)] - if len(spec) != 1: - print('error: %s session not found in %r' % (wanted, lib_ROOT)) - new_root += '\n' + spec[0] - - with open(os.path.join(target_dir, 'lib', 'ROOT'), 'w') as root_f: - root_f.write(new_root) - # For the examples, generate ".thy" files where appropriate, and also # generate an "All.thy" which contains all the examples. def gen_thy_file(c_file): diff --git a/tools/autocorres/tools/release_files/AUTOCORRES_FILES b/tools/autocorres/tools/release_files/AUTOCORRES_FILES index 1b492950bd..d9716dc5a7 100644 --- a/tools/autocorres/tools/release_files/AUTOCORRES_FILES +++ b/tools/autocorres/tools/release_files/AUTOCORRES_FILES @@ -33,6 +33,7 @@ exception_rewrite.ML: Proof frameworks and code to rewrite monadic specifications to avoid using exceptions where possible. +NatBitwise.thy: WordAbstract.thy: word_abstract.ML: Word abstraction framework and theorems. diff --git a/tools/autocorres/tools/release_files/ROOT.release b/tools/autocorres/tools/release_files/ROOT.release index cbce7e7a8a..f6eb34b726 100644 --- a/tools/autocorres/tools/release_files/ROOT.release +++ b/tools/autocorres/tools/release_files/ROOT.release @@ -8,15 +8,14 @@ session AutoCorres = CParser + sessions "HOL-Eisbach" - Lib - CLib + Monads theories + "DataStructures" "AutoCorres" session AutoCorresTest in "tests" = AutoCorres + sessions "HOL-Number_Theory" - AutoCorres directories "parse-tests" "proof-tests" diff --git a/tools/autocorres/tools/release_files/ROOTS.base_dir b/tools/autocorres/tools/release_files/ROOTS.base_dir index 0d830b5b99..caf4ca8376 100644 --- a/tools/autocorres/tools/release_files/ROOTS.base_dir +++ b/tools/autocorres/tools/release_files/ROOTS.base_dir @@ -1,4 +1,7 @@ -lib +lib/Basics +lib/Eisbach_Tools +lib/ML_Utils +lib/Monads lib/Word_Lib c-parser autocorres From 03e4ef92a41d1416ee3d8976227acafcbc22a3b3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 3 Nov 2023 10:46:06 +1100 Subject: [PATCH 29/67] autocorres: bring CONTRIBUTORS file up to date - remove defunct email addresses - add myself as current maintainer Signed-off-by: Gerwin Klein --- tools/autocorres/tools/release_files/CONTRIBUTORS | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/tools/autocorres/tools/release_files/CONTRIBUTORS b/tools/autocorres/tools/release_files/CONTRIBUTORS index 9b66767c25..9cb732548b 100644 --- a/tools/autocorres/tools/release_files/CONTRIBUTORS +++ b/tools/autocorres/tools/release_files/CONTRIBUTORS @@ -1,19 +1,21 @@ -Core Development Team ---------------------- +Core Developers +--------------- David Greenaway (inactive) - Japheth Lim + Japheth Lim (inactive) + + Gerwin Klein (maintenance) Contributions ------------- - Lars Noschinski + Lars Noschinski "owhile" definitions and related rules, as well as many other contributions to the proof libraries. - Matthew Brecknell + Matthew Brecknell (inactive) Maintenance; integration with seL4's C refinement framework. From d4f0e5a38bf848718dbed7303e06f508134d43a5 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 5 Dec 2023 13:23:58 +1100 Subject: [PATCH 30/67] arm-hyp crefine: update length to word_t for VCPU functions Length argument for these functions was previously unsigned int, which was fine for AArch32, but an implicit downcast on AArch64. Changing it to word_t makes it unsigned long, thus requiring signature update in ccorres proofs. Signed-off-by: Rafal Kolanski --- proof/crefine/ARM_HYP/Arch_C.thy | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy index f651380021..5468bae776 100644 --- a/proof/crefine/ARM_HYP/Arch_C.thy +++ b/proof/crefine/ARM_HYP/Arch_C.thy @@ -4557,14 +4557,14 @@ lemma decodeVCPUWriteReg_ccorres: (invs' and (\s. ksCurThread s = thread) and ct_active' and sch_act_simple and sysargs_rel args buffer and (valid_cap' (ArchObjectCap cp)) and K (isVCPUCap cp)) - (UNIV \ {s. unat (length_' s) = length args} + (UNIV \ {s. unat (length___unsigned_long_' s) = length args} \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} \ {s. buffer_' s = option_to_ptr buffer}) hs (decodeVCPUWriteReg args cp >>= invocationCatch thread isBlocking isCall InvokeArchObject) (Call decodeVCPUWriteReg_'proc)" apply (rule ccorres_grab_asm) - apply (cinit' lift: length_' cap_' buffer_' simp: decodeVCPUWriteReg_def Let_def) + apply (cinit' lift: length___unsigned_long_' cap_' buffer_' simp: decodeVCPUWriteReg_def Let_def) apply (rule ccorres_Cond_rhs_Seq ; clarsimp) apply (rule_tac ccorres_gen_asm[where P="length args < 2"]) apply clarsimp @@ -4688,7 +4688,7 @@ lemma decodeVCPUInjectIRQ_ccorres: and sysargs_rel args buffer and (valid_cap' (ArchObjectCap cp)) and K (isVCPUCap cp)) - (UNIV \ {s. unat (length_' s) = length args} + (UNIV \ {s. unat (length___unsigned_long_' s) = length args} \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} \ {s. buffer_' s = option_to_ptr buffer} ) hs @@ -4696,7 +4696,7 @@ lemma decodeVCPUInjectIRQ_ccorres: >>= invocationCatch thread isBlocking isCall InvokeArchObject) (Call decodeVCPUInjectIRQ_'proc)" apply (rule ccorres_grab_asm) - apply (cinit' lift: length_' cap_' buffer_' + apply (cinit' lift: length___unsigned_long_' cap_' buffer_' simp: decodeVCPUInjectIRQ_def Let_def shiftL_nat ) apply csymbr apply csymbr @@ -4904,14 +4904,14 @@ lemma decodeVCPUReadReg_ccorres: (invs' and (\s. ksCurThread s = thread) and ct_active' and sch_act_simple and sysargs_rel args buffer and (valid_cap' (ArchObjectCap cp))) - (UNIV \ {s. unat (length_' s) = length args} + (UNIV \ {s. unat (length___unsigned_long_' s) = length args} \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} \ {s. buffer_' s = option_to_ptr buffer} \ \\call = from_bool isCall \) hs (decodeVCPUReadReg args cp >>= invocationCatch thread isBlocking isCall InvokeArchObject) (Call decodeVCPUReadReg_'proc)" - apply (cinit' lift: length_' cap_' buffer_' call_') + apply (cinit' lift: length___unsigned_long_' cap_' buffer_' call_') apply (clarsimp simp: decodeVCPUReadReg_def Let_def) apply (rule ccorres_Cond_rhs_Seq) apply (simp add: throwError_bind invocationCatch_def invocation_eq_use_types @@ -5120,7 +5120,7 @@ lemma decodeVCPUAckVPPI_ccorres: and sysargs_rel args buffer and (valid_cap' (ArchObjectCap cp)) and K (isVCPUCap cp)) - (UNIV \ {s. unat (length_' s) = length args} + (UNIV \ {s. unat (length___unsigned_long_' s) = length args} \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} \ {s. buffer_' s = option_to_ptr buffer} ) hs @@ -5142,7 +5142,7 @@ proof - show ?thesis apply (rule ccorres_grab_asm) - apply (cinit' lift: length_' cap_' buffer_') + apply (cinit' lift: length___unsigned_long_' cap_' buffer_') apply (clarsimp simp: decodeVCPUAckVPPI_def) apply (csymbr, rename_tac cp') apply csymbr @@ -5241,7 +5241,7 @@ lemma decodeARMVCPUInvocation_ccorres: and (valid_cap' (ArchObjectCap cp))) (UNIV \ \whoever wrote the C code decided to name this arbitrarily differently from other functions\ \ {s. label___unsigned_long_' s = label} - \ {s. unat (length_' s) = length args} + \ {s. unat (length___unsigned_long_' s) = length args} \ {s. slot_' s = cte_Ptr slot} \ {s. current_extra_caps_' (globals s) = extraCaps'} \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} @@ -5250,7 +5250,7 @@ lemma decodeARMVCPUInvocation_ccorres: (decodeARMVCPUInvocation label args cptr slot cp extraCaps >>= invocationCatch thread isBlocking isCall InvokeArchObject) (Call decodeARMVCPUInvocation_'proc)" - apply (cinit' lift: label___unsigned_long_' length_' slot_' current_extra_caps_' + apply (cinit' lift: label___unsigned_long_' length___unsigned_long_' slot_' current_extra_caps_' cap_' buffer_' call_') apply (clarsimp simp: decodeARMVCPUInvocation_def) From 0ba3f8e8afb0a0f0dbcd1b5e12ccf61c9e2d2448 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Sat, 2 Dec 2023 13:10:41 +1030 Subject: [PATCH 31/67] clib: further improvements to ccorres_While This adds information about the return relation to the C guards and the C preconditions of the assumptions. The C hoare triples for cond have also been consolidated, to help simplify applications where the C guards are minimal. A comment about its intended use is given. Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 83 +++++++++++++++++++++----------------- 1 file changed, 47 insertions(+), 36 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index bb467af531..74870f7ebf 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -1070,11 +1070,20 @@ lemma ccorres_While_Normal_helper: apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_fault mem_Collect_eq) done +text \ + This rule is intended to be used to show correspondence between a Haskell whileLoop and a C + while loop, where in particular, the C while loop is parsed into a Simpl While loop that + updates the cstate as part of the loop condition. In such a case, the CParser will produce a Simpl + program in the form that is seen in the conclusion of this rule.\ lemma ccorres_While: assumes body_ccorres: - "\r. ccorresG srel \ rrel xf (\s. G r s \ C r s = Some True) (G' \ C') [] (B r) B'" - assumes setter_ccorres: - "\r. ccorresG srel \ (\rv rv'. rv = to_bool rv') cond_xf (G r) G' [] (gets_the (C r)) setter" + "\r. ccorresG srel \ rrel xf + (\s. G r s \ C r s = Some True) (G' \ C' \ {s'. rrel r (xf s')}) [] + (B r) B'" + assumes cond_ccorres: + "\r. ccorresG srel \ (\rv rv'. rv = to_bool rv') cond_xf + (G r) (G' \ {s'. rrel r (xf s')}) [] + (gets_the (C r)) cond" assumes nf: "\r. no_fail (\s. G r s \ C r s = Some True) (B r)" assumes no_ofail: "\r. no_ofail (G r) (C r)" assumes body_inv: @@ -1082,23 +1091,19 @@ lemma ccorres_While: "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s') \ s' \ C' \ C r s = Some True} B' G'" - assumes setter_inv_cond: + assumes cond_hoarep: "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} - setter - {s'. s' \ G' \ (cond_xf s' \ 0 \ s' \ C')}" - assumes setter_rrel: - "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} - setter - {s'. rrel r (xf s')}" + cond + {s'. s' \ G' \ (cond_xf s' \ 0 \ s' \ C') \ rrel r (xf s')}" shows "ccorresG srel \ rrel xf (G r) (G' \ {s'. rrel r (xf s')}) hs (whileLoop (\r s. the (C r s)) B r) - (setter;; (While {s'. cond_xf s' \ 0} (B';; setter)))" + (cond;; While {s'. cond_xf s' \ 0} (B';; cond))" proof - note unif_rrel_def[simp add] to_bool_def[simp add] have helper: "\state xstate'. - \ \ \While {s'. cond_xf s' \ 0} (Seq B' setter), Normal state\ \ xstate' \ + \ \ \While {s'. cond_xf s' \ 0} (Seq B' cond), Normal state\ \ xstate' \ \st r s. Normal st = xstate' \ (s, state) \ srel \ (C r s \ None) \ (cond_xf state \ 0) = the (C r s) \ rrel r (xf state) \ G r s \ state \ G' \ (cond_xf state \ 0 \ state \ C') @@ -1133,44 +1138,43 @@ proof - apply (drule_tac x=rv' in spec) apply (drule_tac x=s' in spec) apply (prop_tac "rrel rv' (xf inter_t)") - apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated]) apply (elim impE) - apply (frule_tac s'=inter_t and r1=rv' in ccorresE_gets_the[OF setter_ccorres]; assumption?) + apply (frule_tac s'=inter_t and r1=rv' in ccorresE_gets_the[OF cond_ccorres]; assumption?) + apply fastforce apply (fastforce intro: no_ofail) apply (fastforce dest: EHOther) apply (intro conjI) apply fastforce using no_ofail apply (fastforce elim!: no_ofailD) apply fastforce - apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated]) - apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated]) - apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated]) - apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated]) + apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated]) apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3)) done - have setter_hoarep: + have cond_hoarep': "\r s s' n xstate. - \\\<^sub>h \(setter;; While {s'. cond_xf s' \ 0} (B';; setter)) # hs,s'\ \ (n, xstate) + \\\<^sub>h \(cond;; While {s'. cond_xf s' \ 0} (B';; cond)) # hs,s'\ \ (n, xstate) \ \\ {s' \ G'. (s, s') \ srel \ G r s \ rrel r (xf s')} - setter + cond {s'. (s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')) \ (cond_xf s' \ 0 \ (s' \ C' \ C r s = Some True))}" - apply (insert setter_ccorres) + apply (insert cond_ccorres) apply (drule_tac x=r in meta_spec) apply (frule_tac s=s in ccorres_to_vcg_gets_the) apply (fastforce intro: no_ofail) - apply (insert setter_rrel) + apply (insert cond_hoarep) apply (drule_tac x=s in meta_spec) apply (drule_tac x=r in meta_spec) apply (rule hoarep_conj_lift_pre_fix) apply (rule hoarep_conj_lift_pre_fix) - apply (insert setter_inv_cond)[1] - apply (drule_tac x=s in meta_spec) - apply (drule_tac x=r in meta_spec) - apply (rule_tac Q'="{s' \ G'. cond_xf s' \ 0 \ s' \ C'}" in conseqPost; fastforce) + apply (insert cond_hoarep)[1] + apply (fastforce simp: conseq_under_new_pre) apply (fastforce intro!: hoarep_conj_lift_pre_fix simp: Collect_mono conseq_under_new_pre) - apply (insert setter_inv_cond) + apply (insert cond_hoarep) apply (drule_tac x=s in meta_spec) apply (drule_tac x=r in meta_spec) apply (simp add: imp_conjR) @@ -1183,6 +1187,12 @@ proof - apply (simp add: Collect_mono conseq_under_new_pre) done + have cond_inv_guard: + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} + cond + {s'. s' \ G' \ (cond_xf s' \ 0 \ s' \ C')}" + by (fastforce intro: conseqPost cond_hoarep) + show ?thesis apply (clarsimp simp: ccorres_underlying_def) apply (rename_tac s s' n xstate) @@ -1191,12 +1201,12 @@ proof - in exec_handlers_use_hoare_nothrow_hoarep) apply fastforce apply (rule HoarePartial.Seq) - apply (erule setter_hoarep) + apply (erule cond_hoarep') apply (rule conseqPre) apply (rule ccorres_While_Normal_helper) - apply (fastforce intro!: setter_hoarep hoarep_ex_lift) + apply (fastforce intro!: cond_hoarep' hoarep_ex_lift) apply (intro hoarep_ex_pre, rename_tac rv new_s) - apply (insert setter_inv_cond)[1] + apply (insert cond_inv_guard)[1] apply (drule_tac x=new_s in meta_spec) apply (drule_tac x=rv in meta_spec) apply (insert body_ccorres)[1] @@ -1216,21 +1226,22 @@ proof - fastforce simp: Collect_mono conseq_under_new_pre) apply fastforce apply (case_tac xstate; clarsimp) - apply (frule intermediate_Normal_state[OF _ _ setter_hoarep]; assumption?) + apply (frule intermediate_Normal_state[OF _ _ cond_hoarep]; assumption?) apply fastforce apply clarsimp apply (rename_tac inter_t) - apply (insert setter_ccorres) + apply (insert cond_ccorres) apply (drule_tac x=r in meta_spec) - apply (drule (3) ccorresE_gets_the) + apply (drule (2) ccorresE_gets_the) + apply fastforce apply (fastforce intro: no_ofail) apply (fastforce dest: EHOther) apply (prop_tac "rrel r (xf inter_t)") - apply (fastforce dest: hoarep_exec[rotated] intro: setter_rrel) + apply (fastforce dest: hoarep_exec[rotated] intro: cond_hoarep) apply (case_tac "\ the (C r s)") apply (fastforce elim: exec_Normal_elim_cases simp: whileLoop_cond_fail return_def) apply (insert no_ofail) - apply (fastforce dest!: helper hoarep_exec[OF _ _ setter_inv_cond, rotated] no_ofailD) + apply (fastforce dest!: helper hoarep_exec[OF _ _ cond_inv_guard, rotated] no_ofailD) done qed From 1278a8d06ec9f6ae92da985dc5907b2e4a87a219 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 8 Dec 2023 14:43:43 +0100 Subject: [PATCH 32/67] github: docs for platform branch rebase workflow Signed-off-by: Gerwin Klein --- .github/workflows/proof-deploy.yml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml index bf2006f651..cbb22db562 100644 --- a/.github/workflows/proof-deploy.yml +++ b/.github/workflows/proof-deploy.yml @@ -77,6 +77,13 @@ jobs: token: ${{ secrets.PRIV_REPO_TOKEN }} tag: "l4v/proof-deploy/${{ github.event_name }}" +# Automatically rebase platform branches on pushes to master. +# This workflow here on the master branch attempts a git rebase of the platform +# branches listed in the build matrix below. If the rebase succeeds, the rebased +# branch is pushed under the name `-rebased`. This triggers the build +# workflow on the `-rebased` branch, which will run the proofs. If the +# proofs succeed, the `-rebased` branch is force-pushed over +# ``, becoming the new platform branch. rebase: name: Rebase platform branches runs-on: ubuntu-latest From a828b996db008fded7ac3c34b9f1dd1dc6edd585 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 10 Dec 2023 11:44:14 +0100 Subject: [PATCH 33/67] cspec/c: provide NUM_DOMAINS build override option Setting the environment variable INPUT_NUM_DOMAINS will cause the build to override the KernelNumDomains setting in the config file with the provided setting. Signed-off-by: Gerwin Klein --- spec/cspec/c/kernel.mk | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/spec/cspec/c/kernel.mk b/spec/cspec/c/kernel.mk index 98a9f1dc85..efcc48a92c 100644 --- a/spec/cspec/c/kernel.mk +++ b/spec/cspec/c/kernel.mk @@ -108,6 +108,10 @@ ${OVERLAY}: ${DEFAULT_OVERLAY} @cp $< $@ endif +ifdef INPUT_NUM_DOMAINS +KERNEL_CMAKE_EXTRA_OPTIONS += -DKernelNumDomains=${INPUT_NUM_DOMAINS} +endif + # Initialize the CMake build. We purge the build directory and start again # whenever any of the kernel sources change, so that we can reliably pick up # changes to the build config. From 81840fe2781cdb531e8cef0277fe6f47b8d04690 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 10 Dec 2023 11:49:39 +0100 Subject: [PATCH 34/67] github: add NUM_DOMAINS test matrix This will now test with the following num_domains settings: - PRs: default as in config file, no matrix - push to master: with NUM_DOMAINS = 1 and default (= '') - weekly test: with NUM_DOMAINS = 1, 7, and default The default in the current config files is 16. 1 leads to structural code changes is the setting most likely to break. 7 is for checking that the proofs also work with a value that is not a power of 2. Signed-off-by: Gerwin Klein --- .github/workflows/proof-deploy.yml | 2 ++ .github/workflows/weekly-clean.yml | 2 ++ 2 files changed, 4 insertions(+) diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml index cbb22db562..ace111657b 100644 --- a/.github/workflows/proof-deploy.yml +++ b/.github/workflows/proof-deploy.yml @@ -37,6 +37,7 @@ jobs: fail-fast: false matrix: arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] + num_domains: ['1', ''] # test only most recent push: concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }} steps: @@ -45,6 +46,7 @@ jobs: with: L4V_ARCH: ${{ matrix.arch }} xml: ${{ needs.code.outputs.xml }} + NUM_DOMAINS: ${{ matrix.num_domains }} env: AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }} AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }} diff --git a/.github/workflows/weekly-clean.yml b/.github/workflows/weekly-clean.yml index 4bc06134ce..4363b48531 100644 --- a/.github/workflows/weekly-clean.yml +++ b/.github/workflows/weekly-clean.yml @@ -18,11 +18,13 @@ jobs: fail-fast: false matrix: arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] + num_domains: ['1', '7', ''] steps: - name: Proofs uses: seL4/ci-actions/aws-proofs@master with: L4V_ARCH: ${{ matrix.arch }} + NUM_DOMAINS: ${{ matrix.num_domains }} cache_read: '' # start with empty cache, but write cache back (default) env: AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }} From 62f0e202efe62bf59a8c25d32c47d3b1d410ef36 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 10 Dec 2023 12:58:22 +0100 Subject: [PATCH 35/67] runtest: echo NUM_DOMAINS override Signed-off-by: Gerwin Klein --- run_tests | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/run_tests b/run_tests index 0921cb0c85..0b7b023291 100755 --- a/run_tests +++ b/run_tests @@ -122,7 +122,9 @@ returncode = 0 for arch in archs: features = os.environ.get("L4V_FEATURES", "") plat = os.environ.get("L4V_PLAT", "") - print(f"Testing for L4V_ARCH='{arch}', L4V_FEATURES='{features}', L4V_PLAT='{plat}':") + num_domains = os.environ.get("INPUT_NUM_DOMAINS", "") + print(f"Testing for L4V_ARCH='{arch}', L4V_FEATURES='{features}', L4V_PLAT='{plat}', " + f"INPUT_NUM_DOMAINS='{num_domains}'") os.environ["L4V_ARCH"] = arch # Provide L4V_ARCH_IS_ARM for Corres_Test in lib/ROOT From 028c3e6241c00a37663f6a692b27a225b009f2bc Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 12 Dec 2023 11:55:41 +0100 Subject: [PATCH 36/67] github: add num_domains key to artifact upload If we don't provide the additional name fragment, previous artifacts would be overwritten, which leads to a failure with error message on GitHub. Signed-off-by: Gerwin Klein --- .github/workflows/proof-deploy.yml | 2 +- .github/workflows/weekly-clean.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml index ace111657b..11bd68c359 100644 --- a/.github/workflows/proof-deploy.yml +++ b/.github/workflows/proof-deploy.yml @@ -60,7 +60,7 @@ jobs: - name: Upload logs uses: actions/upload-artifact@v3 with: - name: logs-${{ matrix.arch }} + name: logs-${{ matrix.num_domains }}-${{ matrix.arch }} path: logs.tar.xz deploy: diff --git a/.github/workflows/weekly-clean.yml b/.github/workflows/weekly-clean.yml index 4363b48531..8fa5fb9533 100644 --- a/.github/workflows/weekly-clean.yml +++ b/.github/workflows/weekly-clean.yml @@ -40,7 +40,7 @@ jobs: - name: Upload logs uses: actions/upload-artifact@v3 with: - name: logs-${{ matrix.arch }} + name: logs-${{ matrix.num_domains }}-${{ matrix.arch }} path: logs.tar.xz binary-verification: From e76c69ee0736dcff47b9f84cf3793634186be68e Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 13 Jan 2024 09:24:38 +1100 Subject: [PATCH 37/67] lib: provide warning suppression for Eisbach methods Contexts have the "visible" flag that determine whether warnings such as duplicate rewrite rules are shown or not. Make setting this flag to false available in Eisbach methods. Signed-off-by: Gerwin Klein --- lib/Eisbach_Tools/Eisbach_Methods.thy | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/lib/Eisbach_Tools/Eisbach_Methods.thy b/lib/Eisbach_Tools/Eisbach_Methods.thy index 5e6b2a7a84..64c1d88470 100644 --- a/lib/Eisbach_Tools/Eisbach_Methods.thy +++ b/lib/Eisbach_Tools/Eisbach_Methods.thy @@ -17,6 +17,17 @@ imports Local_Method begin +section \Warnings\ + +method_setup not_visible = + \Method.text_closure >> (fn m => fn ctxt => fn facts => + let + val ctxt' = Context_Position.set_visible false ctxt + fun tac st' = method_evaluate m ctxt' facts st' + in SIMPLE_METHOD tac facts end)\ + \set context visibility to false for suppressing warnings in method execution\ + + section \Debugging methods\ method print_concl = (match conclusion in P for P \ \print_term P\) From 449cfc702e956de6ad22c6c0e876acb543e16fcb Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 13 Jan 2024 09:26:36 +1100 Subject: [PATCH 38/67] clib: suppress simp warnings in simpl_rewrite This gets rid of the simplified warning for Collect_const that ccorres_rewrite produces in many CRefine proofs. Signed-off-by: Gerwin Klein --- lib/clib/Simpl_Rewrite.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/clib/Simpl_Rewrite.thy b/lib/clib/Simpl_Rewrite.thy index 26b5e4b681..90ceb4cead 100644 --- a/lib/clib/Simpl_Rewrite.thy +++ b/lib/clib/Simpl_Rewrite.thy @@ -460,7 +460,7 @@ text \Methods to automate rewriting.\ method do_rewrite uses hom ruleset declares C_simp_simps = (rule com_ctxt_focus_rewrite[OF hom], rule ruleset, - #break "simpl_rewrite_rewrite", (simp add: C_simp_simps; fail))+ + #break "simpl_rewrite_rewrite", (not_visible \simp add: C_simp_simps\; fail))+ method rewrite_pre uses hom declares C_simp_pre C_simp_simps = (do_rewrite hom: hom ruleset: C_simp_pre) From dc62bfdfeb5fe8274221b02f8fb48cfb811ac292 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 15:51:44 +1030 Subject: [PATCH 39/67] lib+refine: strengthen corres_assert_assume_l and move to Lib Signed-off-by: Michael McInerney --- lib/Corres_UL.thy | 5 +++++ proof/refine/AARCH64/Schedule_R.thy | 5 ----- proof/refine/ARM/Schedule_R.thy | 5 ----- proof/refine/ARM_HYP/Schedule_R.thy | 5 ----- proof/refine/RISCV64/Schedule_R.thy | 5 ----- proof/refine/X64/Schedule_R.thy | 5 ----- 6 files changed, 5 insertions(+), 25 deletions(-) diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index 93804f156c..f62ee89b13 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -740,6 +740,11 @@ lemma corres_assert_assume: by (auto simp: bind_def assert_def fail_def return_def corres_underlying_def) +lemma corres_assert_assume_l: + "corres_underlying sr nf nf' rrel P Q (f ()) g + \ corres_underlying sr nf nf' rrel (P and (\s. P')) Q (assert P' >>= f) g" + by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) + lemma corres_assert_gen_asm_cross: "\ \s s'. \(s, s') \ sr; P' s; Q' s'\ \ A; A \ corres_underlying sr nf nf' r P Q f (g ()) \ diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy index ec6dffbdf6..e31be58437 100644 --- a/proof/refine/AARCH64/Schedule_R.thy +++ b/proof/refine/AARCH64/Schedule_R.thy @@ -1575,11 +1575,6 @@ lemma corres_assert_ret: apply (simp add: assert_def return_def fail_def) done -lemma corres_assert_assume_l: - "corres dc P Q (f ()) g - \ corres dc (P and (\s. P')) Q (assert P' >>= f) g" - by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) - lemma corres_assert_assume_r: "corres dc P Q f (g ()) \ corres dc P (Q and (\s. Q')) f (assert Q' >>= g)" diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index 1eeb7b4351..8b3d92fa3e 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -1454,11 +1454,6 @@ lemma corres_assert_ret: apply (simp add: assert_def return_def fail_def) done -lemma corres_assert_assume_l: - "corres dc P Q (f ()) g - \ corres dc (P and (\s. P')) Q (assert P' >>= f) g" - by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) - lemma corres_assert_assume_r: "corres dc P Q f (g ()) \ corres dc P (Q and (\s. Q')) f (assert Q' >>= g)" diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index 0b6d59bdc9..b4edbdf7f4 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -1550,11 +1550,6 @@ lemma corres_assert_ret: apply (simp add: assert_def return_def fail_def) done -lemma corres_assert_assume_l: - "corres dc P Q (f ()) g - \ corres dc (P and (\s. P')) Q (assert P' >>= f) g" - by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) - lemma corres_assert_assume_r: "corres dc P Q f (g ()) \ corres dc P (Q and (\s. Q')) f (assert Q' >>= g)" diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 8524d6bdd5..2637f53166 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -1419,11 +1419,6 @@ lemma corres_assert_ret: apply (simp add: assert_def return_def fail_def) done -lemma corres_assert_assume_l: - "corres dc P Q (f ()) g - \ corres dc (P and (\s. P')) Q (assert P' >>= f) g" - by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) - lemma corres_assert_assume_r: "corres dc P Q f (g ()) \ corres dc P (Q and (\s. Q')) f (assert Q' >>= g)" diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index c1827abcf3..3aa19c9a3f 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -1418,11 +1418,6 @@ lemma corres_assert_ret: apply (simp add: assert_def return_def fail_def) done -lemma corres_assert_assume_l: - "corres dc P Q (f ()) g - \ corres dc (P and (\s. P')) Q (assert P' >>= f) g" - by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) - lemma corres_assert_assume_r: "corres dc P Q f (g ()) \ corres dc P (Q and (\s. Q')) f (assert Q' >>= g)" From 1e32077cf1d7367b5d641e2279fd2cf375ab989c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 15:57:11 +1030 Subject: [PATCH 40/67] lib: add corres_if_strong Signed-off-by: Michael McInerney --- lib/Corres_UL.thy | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index f62ee89b13..5054ec5a40 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -481,6 +481,18 @@ lemma corres_if3: (if G then a else b) (if G' then c else d)" by simp +lemma corres_if_strong: + "\\s s'. \(s, s') \ sr; R s; R' s'\ \ G = G'; + \G; G'\ \ corres_underlying sr nf nf' r P P' a c; + \\ G; \ G'\ \ corres_underlying sr nf nf' r Q Q' b d \ + \ corres_underlying sr nf nf' r + (R and (if G then P else Q)) (R' and (if G' then P' else Q')) + (if G then a else b) (if G' then c else d)" + by (fastforce simp: corres_underlying_def) + +lemmas corres_if_strong' = + corres_if_strong[where R=R and P=R and Q=R for R, + where R'=R' and P'=R' and Q'=R' for R', simplified] text \Some equivalences about liftM and other useful simps\ From ea9bfb0284e5d7b8fd4460855dcf8b704ebbcdb6 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 15:59:19 +1030 Subject: [PATCH 41/67] lib: add some rules involving ex_abs_underlying, including corres_from_valid Signed-off-by: Michael McInerney --- lib/ExtraCorres.thy | 120 ++++++++++++++++++++++++++++++++++++++------ 1 file changed, 106 insertions(+), 14 deletions(-) diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy index b92de195f0..ef09f84086 100644 --- a/lib/ExtraCorres.thy +++ b/lib/ExtraCorres.thy @@ -5,7 +5,7 @@ *) theory ExtraCorres -imports Corres_UL +imports Corres_UL DetWPLib begin (* FIXME: the S in this rule is mainly to make the induction work, we don't actually need it in @@ -181,12 +181,17 @@ qed text \Some results concerning the interaction of abstract and concrete states\ +definition ex_abs_underlying :: "('a \ 'b) set \ ('a \ bool) \ 'b \ bool" where + "ex_abs_underlying sr P s' \ \s. (s,s') \ sr \ P s" + +lemma ex_absI[intro!]: + "(s, s') \ sr \ P s \ ex_abs_underlying sr P s'" + by (auto simp add: ex_abs_underlying_def) + lemma corres_u_nofail: - "corres_underlying S nf True r P P' f g \ (nf \ no_fail P f) \ - no_fail (\s'. \s. (s,s') \ S \ P s \ P' s') g" - apply (clarsimp simp add: corres_underlying_def no_fail_def) - apply fastforce - done + "\corres_underlying S nf True r P P' f g; nf \ no_fail P f\ + \ no_fail (P' and ex_abs_underlying S P) g" + by (fastforce simp: corres_underlying_def ex_abs_underlying_def no_fail_def) lemma wp_from_corres_u: "\ corres_underlying R nf nf' r G G' f f'; \P\ f \Q\; \P'\ f' \Q'\; nf \ no_fail P f \ \ @@ -204,7 +209,7 @@ lemma wp_from_corres_u_unit: lemma corres_nofail: "corres_underlying state_relation nf True r P P' f g \ (nf \ no_fail P f) \ no_fail (\s'. \s. (s,s') \ state_relation \ P s \ P' s') g" - by (rule corres_u_nofail) + by (fastforce intro: no_fail_pre corres_u_nofail simp: ex_abs_underlying_def) lemma wp_from_corres_unit: "\ corres_underlying state_relation nf nf' r G G' f f'; @@ -213,13 +218,6 @@ lemma wp_from_corres_unit: f' \\_ s'. \s. (s,s') \ state_relation \ Q s \ Q' s'\" by (auto intro!: wp_from_corres_u_unit) -definition ex_abs_underlying :: "('a \ 'b) set \ ('a \ bool) \ 'b \ bool" where - "ex_abs_underlying sr P s' \ \s. (s,s') \ sr \ P s" - -lemma ex_absI[intro!]: - "(s, s') \ sr \ P s \ ex_abs_underlying sr P s'" - by (auto simp add: ex_abs_underlying_def) - lemma corres_underlying_split_ex_abs: assumes ac: "corres_underlying srel nf nf' r' G G' a c" assumes bd: "\rv rv'. r' rv rv' \ @@ -251,6 +249,100 @@ lemma hoare_from_abs_inv: using assms by (fastforce intro: hoare_from_abs[where R=\ and S=\ and R'=\ and Q="\_. P" , simplified]) +lemma corres_from_valid: + assumes nf': "nf' \ no_fail (P' and ex_abs_underlying srel P) f'" + assumes + "\s. \\s'. P s \ P' s' \ (s, s') \ srel\ + f' \\rv' t'. \(rv, t) \ fst (f s). (t, t') \ srel \ rrel rv rv'\" + shows "corres_underlying srel nf nf' rrel P P' f f'" + using assms + by (fastforce simp: corres_underlying_def valid_def no_fail_def) + +lemma corres_from_valid_det: + assumes det: "det_wp P f" + assumes nf': "nf' \ no_fail (P' and ex_abs_underlying srel P) f'" + assumes valid: + "\s rv t. + \fst (f s) = {(rv, t)}; P s\ + \ \\s'. P' s' \ (s, s') \ srel\ f' \\rv' t'. (t, t') \ srel \ rrel rv rv'\" + shows "corres_underlying srel nf nf' rrel P P' f f'" + apply (clarsimp simp: corres_underlying_def) + apply (intro conjI) + apply (insert det) + apply (clarsimp simp: det_wp_def) + apply (force dest: use_valid[OF _ valid]) + apply (fastforce dest: nf' simp: no_fail_def ex_abs_underlying_def) + done + +lemma corres_noop_ex_abs: + assumes P: "\s. P s \ \\s'. (s, s') \ sr \ P' s'\ f \\rv s'. (s, s') \ sr \ r x rv\" + assumes nf': "nf' \ no_fail (P' and ex_abs_underlying sr P) f" + shows "corres_underlying sr nf nf' r P P' (return x) f" + apply (simp add: corres_underlying_def return_def) + apply clarsimp + apply (frule P) + apply (insert nf') + apply (fastforce simp: valid_def no_fail_def ex_abs_underlying_def) + done + +lemma corres_symb_exec_r_conj_ex_abs: + assumes z: "\rv. corres_underlying sr nf nf' r Q (R' rv) x (y rv)" + assumes y: "\Q'\ m \R'\" + assumes x: "\s. Q s \ \\s'. (s, s') \ sr \ P' s'\ m \\rv s'. (s, s') \ sr\" + assumes nf: "nf' \ no_fail (P' and ex_abs_underlying sr Q) m" + shows "corres_underlying sr nf nf' r Q (P' and Q') x (m >>= (\rv. y rv))" +proof - + have P: "corres_underlying sr nf nf' dc Q P' (return undefined) m" + apply (rule corres_noop_ex_abs) + apply (simp add: x) + apply (erule nf) + done + show ?thesis + apply (rule corres_guard_imp) + apply (subst return_bind[symmetric], rule corres_split[OF P]) + apply (rule z) + apply wp + apply (rule y) + apply simp+ + done +qed + +lemmas corres_symb_exec_r_conj_ex_abs_forwards = + corres_symb_exec_r_conj_ex_abs[where P'=P' and Q'=P' for P', simplified] + +lemma gets_the_corres_ex_abs': + "\no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\ \ + corres_underlying sr False True r P P' (gets_the a) (gets_the b) + = (\s s'. P s \ P' s' \ (s, s') \ sr \ r (the (a s)) (the (b s')))" + by (fastforce simp: gets_the_def no_ofail_def corres_underlying_def split_def exec_gets + assert_opt_def fail_def return_def ex_abs_underlying_def) + +lemmas gets_the_corres_ex_abs = gets_the_corres_ex_abs'[THEN iffD2] + +lemma gets_the_corres': + "\no_ofail P a; no_ofail P' b\ \ + corres_underlying sr False True r P P' (gets_the a) (gets_the b) + = (\s s'. P s \ P' s' \ (s, s') \ sr \ r (the (a s)) (the (b s')))" + apply (erule gets_the_corres_ex_abs') + apply (fastforce intro: no_ofail_pre_imp) + done + +lemmas gets_the_corres = gets_the_corres'[THEN iffD2] + +lemma gets_the_corres_relation: + "\no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f'); + P s; P' s'; (s, s') \ sr\ + \ r (the (f s)) (the (f' s'))" + apply (rule_tac P=P and a=f and b=f' and P'=P' + in gets_the_corres_ex_abs'[THEN iffD1, rule_format]; + fastforce?) + apply (rule no_ofail_gets_the_eq[THEN iffD2]) + apply (fastforce intro: corres_u_nofail) + done + + +\ \Some @{term corres_underlying} rules for @{term whileLoop}\ + lemma in_whileLoop_corres: assumes body_corres: "\r r'. rrel r r' \ From 918ec7a2837a10fd2592ac180caeee3c6823ec24 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 16:01:14 +1030 Subject: [PATCH 42/67] lib: strengthen no_ofail_gets_the Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index f1b2d6960c..4338dd0612 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -287,11 +287,14 @@ lemma no_ofail_oassert[simp, wp]: "no_ofail (\_. P) (oassert P)" by (simp add: oassert_def no_ofail_def) -lemma no_ofail_gets_the: - "no_ofail P f \ no_fail P (gets_the (f :: ('s, 'a) lookup))" - by (fastforce simp: no_ofail_def no_fail_def gets_the_def gets_def - get_def assert_opt_def bind_def return_def fail_def - split: option.split) +lemma no_ofail_gets_the_eq: + "no_ofail P f \ no_fail P (gets_the (f :: ('s, 'a) lookup))" + by (auto simp: no_ofail_def no_fail_def gets_the_def gets_def + get_def assert_opt_def bind_def return_def fail_def + split: option.split) + +lemmas no_ofail_gets_the = + no_ofail_gets_the_eq[THEN iffD1] lemma no_ofail_is_triple[wp_trip]: "no_ofail P f = triple_judgement P f (\s f. f s \ None)" From 97e40a03bf24713e3531b9311fed7837b2e2a8f8 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 18:20:51 +1030 Subject: [PATCH 43/67] lib: add monadic_rewrite_guard_arg_cong Signed-off-by: Michael McInerney --- lib/MonadicRewrite.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy index 3058fd921b..4cce55331e 100644 --- a/lib/MonadicRewrite.thy +++ b/lib/MonadicRewrite.thy @@ -81,6 +81,10 @@ lemma monadic_rewrite_pre_imp_eq: "\ \s. P s \ f s = g s \ \ monadic_rewrite F E P f g" by (simp add: monadic_rewrite_def) +lemma monadic_rewrite_guard_arg_cong: + "(\s. P s \ x = y) \ monadic_rewrite F E P (f x) (f y)" + by (clarsimp simp: monadic_rewrite_def) + lemma monadic_rewrite_exists: "(\v. monadic_rewrite F E (Q v) m m') \ monadic_rewrite F E ((\s. \v. P v s \ Q v s) and (\s. \v. P v s)) m m'" From 11614b920e29f351e2d788dfef236c369fbd0a10 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 18:21:26 +1030 Subject: [PATCH 44/67] lib: generalise monadic_rewrite_is_valid Signed-off-by: Michael McInerney --- lib/MonadicRewrite.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy index 4cce55331e..f08e04fd9e 100644 --- a/lib/MonadicRewrite.thy +++ b/lib/MonadicRewrite.thy @@ -697,7 +697,7 @@ lemma monadic_rewrite_refine_validE_R: by (simp add: validE_R_def validE_def monadic_rewrite_refine_valid) lemma monadic_rewrite_is_valid: - "\ monadic_rewrite False False P' f f'; \P\ do x <- f; g x od \Q\ \ + "\ monadic_rewrite False E P' f f'; \P\ do x <- f; g x od \Q\ \ \ \P and P'\ do x <- f'; g x od \Q\" by (fastforce simp: monadic_rewrite_def valid_def bind_def) From 3c9065f0da82a239fb9fc467e3ee4784f5303971 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 18:21:47 +1030 Subject: [PATCH 45/67] lib: add monadic_rewrite_corres_r_generic_ex_abs Signed-off-by: Michael McInerney --- lib/MonadicRewrite.thy | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy index f08e04fd9e..e4fbed6481 100644 --- a/lib/MonadicRewrite.thy +++ b/lib/MonadicRewrite.thy @@ -10,7 +10,7 @@ theory MonadicRewrite imports Monads.Nondet_VCG - Corres_UL + ExtraCorres Monads.Nondet_Empty_Fail Rules_Tac begin @@ -744,6 +744,13 @@ lemma monadic_rewrite_corres_r_generic: \ corres_underlying R nf nf' r P (P' and Q) a c" by (fastforce simp: corres_underlying_def monadic_rewrite_def) +lemma monadic_rewrite_corres_r_generic_ex_abs: + "\ monadic_rewrite F E (\s'. Q s' \ ex_abs_underlying sr P s') c' c; + corres_underlying sr nf nf'' r P P' a c'; + F \ nf''; nf' \ nf'' \ + \ corres_underlying sr nf nf' r P (P' and Q) a c" + by (fastforce simp: corres_underlying_def monadic_rewrite_def) + lemma monadic_rewrite_corres_r: "\ monadic_rewrite False True Q c c'; corres_underlying R nf nf' r P P' a c' \ From 0cdce52f0b6f5942351bfa39bc38d344430c62c4 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 19:07:01 +1030 Subject: [PATCH 46/67] lib: add ifM_to_top_of_bind Signed-off-by: Michael McInerney --- lib/ExtraCorres.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy index ef09f84086..7201a00896 100644 --- a/lib/ExtraCorres.thy +++ b/lib/ExtraCorres.thy @@ -543,4 +543,8 @@ lemma notM_corres: apply wpsimp+ done +lemma ifM_to_top_of_bind: + "((ifM test true false) >>= z) = ifM test (true >>= z) (false >>= z)" + by (force simp: ifM_def bind_def split: if_splits) + end From 7a14a48ba5ffc6c47f653aacadc527eceacb1872 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 19:07:18 +1030 Subject: [PATCH 47/67] lib: add ifM_corres' and orM_corres' Signed-off-by: Michael McInerney --- lib/ExtraCorres.thy | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy index 7201a00896..0054e44ace 100644 --- a/lib/ExtraCorres.thy +++ b/lib/ExtraCorres.thy @@ -514,6 +514,10 @@ lemma ifM_corres: apply (wpsimp wp: abs_valid conc_valid hoare_vcg_if_lift2)+ done +lemmas ifM_corres' = + ifM_corres[where A=A and B=A and C=A for A, simplified, + where A'=A' and B'=A' and C'=A' for A', simplified] + lemma orM_corres: "\corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) R R' b b'; \B\ a \\c s. \ c \ R s\; \B'\ a' \\c s. \ c \ R' s\\ @@ -524,6 +528,9 @@ lemma orM_corres: apply (wpsimp | fastforce)+ done +lemmas orM_corres' = + orM_corres[where A=A and B=A for A, simplified, where A'=A' and B'=A' for A', simplified] + lemma andM_corres: "\corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b'; \B\ a \\c s. c \ Q s\; \B'\ a' \\c s. c \ Q' s\\ From 45cde7049b27fca2863f4c562e8e2e6f5aa3fa2f Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 19:36:05 +1030 Subject: [PATCH 48/67] lib: reorder assumptions of no_fail_bind In order to aid wp-style reasoning Signed-off-by: Michael McInerney --- lib/Monads/nondet/Nondet_No_Fail.thy | 2 +- proof/crefine/lib/AutoCorres_C.thy | 8 ++--- proof/infoflow/refine/ADT_IF_Refine_C.thy | 29 +++++++++---------- proof/invariant-abstract/ARM/Machine_AI.thy | 3 +- .../invariant-abstract/ARM_HYP/Machine_AI.thy | 3 +- proof/refine/AARCH64/TcbAcc_R.thy | 5 ++-- proof/refine/ARM/TcbAcc_R.thy | 5 ++-- proof/refine/ARM/Tcb_R.thy | 4 +-- proof/refine/ARM_HYP/TcbAcc_R.thy | 5 ++-- proof/refine/RISCV64/TcbAcc_R.thy | 5 ++-- proof/refine/RISCV64/Tcb_R.thy | 4 +-- proof/refine/X64/IpcCancel_R.thy | 5 +--- proof/refine/X64/TcbAcc_R.thy | 5 ++-- proof/refine/X64/Tcb_R.thy | 2 +- .../tests/examples/FactorialTest.thy | 2 +- 15 files changed, 36 insertions(+), 51 deletions(-) diff --git a/lib/Monads/nondet/Nondet_No_Fail.thy b/lib/Monads/nondet/Nondet_No_Fail.thy index 8bf7c5fd0b..6e30a191c2 100644 --- a/lib/Monads/nondet/Nondet_No_Fail.thy +++ b/lib/Monads/nondet/Nondet_No_Fail.thy @@ -130,7 +130,7 @@ lemma no_fail_returnOK[simp, wp]: by (simp add: returnOk_def) lemma no_fail_bind[wp]: - "\ no_fail P f; \rv. no_fail (R rv) (g rv); \Q\ f \R\ \ \ no_fail (P and Q) (f >>= (\rv. g rv))" + "\ \rv. no_fail (R rv) (g rv); \Q\ f \R\; no_fail P f \ \ no_fail (P and Q) (f >>= (\rv. g rv))" unfolding no_fail_def bind_def using post_by_hoare by fastforce diff --git a/proof/crefine/lib/AutoCorres_C.thy b/proof/crefine/lib/AutoCorres_C.thy index 6b3f6b7abf..1b189f0a66 100644 --- a/proof/crefine/lib/AutoCorres_C.thy +++ b/proof/crefine/lib/AutoCorres_C.thy @@ -934,10 +934,10 @@ lemma terminates_spec_no_fail: using normal by auto show ?thesis apply (clarsimp simp: ac AC_call_L1_def L2_call_L1_def) - apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select - wp_del: select_f_wp) - apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce) - apply (wpsimp wp: nf_pre)+ + apply (wpsimp wp_del: select_f_wp) + apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce) + apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select)+ + apply (fastforce simp: nf_pre) done qed diff --git a/proof/infoflow/refine/ADT_IF_Refine_C.thy b/proof/infoflow/refine/ADT_IF_Refine_C.thy index ec9dff489c..60d409bff2 100644 --- a/proof/infoflow/refine/ADT_IF_Refine_C.thy +++ b/proof/infoflow/refine/ADT_IF_Refine_C.thy @@ -193,23 +193,20 @@ lemma handleInterrupt_no_fail: lemma handleEvent_Interrupt_no_fail: "no_fail (invs' and ex_abs einvs) (handleEvent Interrupt)" apply (simp add: handleEvent_def) - apply (rule no_fail_pre) apply wp - apply (rule handleInterrupt_no_fail) - apply (simp add: crunch_simps) - apply (rule_tac Q="\r s. ex_abs (einvs) s \ invs' s \ - (\irq. r = Some irq - \ intStateIRQTable (ksInterruptState s) irq \ irqstate.IRQInactive)" - in hoare_strengthen_post) - apply (rule hoare_vcg_conj_lift) - apply (rule corres_ex_abs_lift) - apply (rule dmo_getActiveIRQ_corres) - apply wp - apply simp - apply wp - apply simp - apply (rule doMachineOp_getActiveIRQ_IRQ_active) - apply clarsimp + apply (rule handleInterrupt_no_fail) + apply (simp add: crunch_simps) + apply (rule_tac Q="\r s. ex_abs (einvs) s \ invs' s \ + (\irq. r = Some irq + \ intStateIRQTable (ksInterruptState s) irq \ irqstate.IRQInactive)" + in hoare_strengthen_post) + apply (rule hoare_vcg_conj_lift) + apply (rule corres_ex_abs_lift) + apply (rule dmo_getActiveIRQ_corres) + apply wpsimp + apply (wpsimp wp: doMachineOp_getActiveIRQ_IRQ_active) + apply clarsimp + apply wpsimp apply (clarsimp simp: invs'_def valid_state'_def) done diff --git a/proof/invariant-abstract/ARM/Machine_AI.thy b/proof/invariant-abstract/ARM/Machine_AI.thy index ab2f402f20..9077037067 100644 --- a/proof/invariant-abstract/ARM/Machine_AI.thy +++ b/proof/invariant-abstract/ARM/Machine_AI.thy @@ -271,8 +271,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]: lemma no_fail_invalidateCacheRange_RAM[simp, wp]: "no_fail \ (invalidateCacheRange_RAM s e p)" apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def) - apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp) - apply (auto intro: hoare_post_taut) + apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb) done lemma no_fail_branchFlushRange[simp, wp]: diff --git a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy index 5a172f2603..b98d74625b 100644 --- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy @@ -280,8 +280,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]: lemma no_fail_invalidateCacheRange_RAM[simp, wp]: "no_fail \ (invalidateCacheRange_RAM s e p)" apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def) - apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp) - apply (auto intro: hoare_post_taut) + apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb) done lemma no_fail_branchFlushRange[simp, wp]: diff --git a/proof/refine/AARCH64/TcbAcc_R.thy b/proof/refine/AARCH64/TcbAcc_R.thy index 2ae604d46e..d495a8db2d 100644 --- a/proof/refine/AARCH64/TcbAcc_R.thy +++ b/proof/refine/AARCH64/TcbAcc_R.thy @@ -1599,9 +1599,8 @@ lemma no_fail_asUser [wp]: "no_fail \ f \ no_fail (tcb_at' t) (asUser t f)" apply (simp add: asUser_def split_def) apply wp - apply (simp add: no_fail_def) - apply (wp hoare_drop_imps) - apply simp + apply (simp add: no_fail_def) + apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+ done lemma asUser_setRegister_corres: diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index b697dafd55..f040d40a8e 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -1534,9 +1534,8 @@ lemma no_fail_asUser [wp]: "no_fail \ f \ no_fail (tcb_at' t) (asUser t f)" apply (simp add: asUser_def split_def) apply wp - apply (simp add: no_fail_def) - apply (wp hoare_drop_imps) - apply simp + apply (simp add: no_fail_def) + apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+ done lemma asUser_setRegister_corres: diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index 6ca57825eb..07f0317cbc 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -341,9 +341,7 @@ lemma invokeTCB_WriteRegisters_corres: apply (rule asUser_corres) apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def) apply (rule corres_Id, simp+) - apply (rule no_fail_pre, wp no_fail_mapM) - apply clarsimp - apply (wp no_fail_setRegister | simp)+ + apply (wpsimp wp: no_fail_mapM no_fail_setRegister)+ apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]]) apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]]) apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]]) diff --git a/proof/refine/ARM_HYP/TcbAcc_R.thy b/proof/refine/ARM_HYP/TcbAcc_R.thy index 409f3d5673..cecb49920c 100644 --- a/proof/refine/ARM_HYP/TcbAcc_R.thy +++ b/proof/refine/ARM_HYP/TcbAcc_R.thy @@ -1581,9 +1581,8 @@ lemma no_fail_asUser [wp]: "no_fail \ f \ no_fail (tcb_at' t) (asUser t f)" apply (simp add: asUser_def split_def) apply wp - apply (simp add: no_fail_def) - apply (wp hoare_drop_imps) - apply simp + apply (simp add: no_fail_def) + apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+ done lemma asUser_setRegister_corres: diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index 708fdaedcc..2cee7bc860 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -1568,9 +1568,8 @@ lemma no_fail_asUser [wp]: "no_fail \ f \ no_fail (tcb_at' t) (asUser t f)" apply (simp add: asUser_def split_def) apply wp - apply (simp add: no_fail_def) - apply (wp hoare_drop_imps) - apply simp + apply (simp add: no_fail_def) + apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+ done lemma asUser_setRegister_corres: diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index c4f071c007..4c9e2ac531 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -329,8 +329,8 @@ lemma invokeTCB_WriteRegisters_corres: apply (clarsimp simp: mask_def user_vtop_def cong: if_cong) apply simp - apply (rule no_fail_pre, wp no_fail_mapM) - apply (clarsimp, (wp no_fail_setRegister | simp)+) + apply (wpsimp wp: no_fail_mapM no_fail_setRegister) + apply simp apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]]) apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]]) apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]]) diff --git a/proof/refine/X64/IpcCancel_R.thy b/proof/refine/X64/IpcCancel_R.thy index 1c0bde4875..d18d63fc87 100644 --- a/proof/refine/X64/IpcCancel_R.thy +++ b/proof/refine/X64/IpcCancel_R.thy @@ -1448,10 +1448,7 @@ lemma no_fail_nativeThreadUsingFPU[wp]: "no_fail (\ and \) (X64.nativeThreadUsingFPU thread)" supply Collect_const[simp del] apply (simp only: X64.nativeThreadUsingFPU_def) - apply (rule no_fail_bind) - apply (simp add: Arch.no_fail_machine_op_lift) - apply simp - apply wp + apply (wpsimp wp: Arch.no_fail_machine_op_lift) done lemma (in delete_one) prepareThreadDelete_corres: diff --git a/proof/refine/X64/TcbAcc_R.thy b/proof/refine/X64/TcbAcc_R.thy index d4a9418bee..a93e6af8f7 100644 --- a/proof/refine/X64/TcbAcc_R.thy +++ b/proof/refine/X64/TcbAcc_R.thy @@ -1561,9 +1561,8 @@ lemma no_fail_asUser [wp]: "no_fail \ f \ no_fail (tcb_at' t) (asUser t f)" apply (simp add: asUser_def split_def) apply wp - apply (simp add: no_fail_def) - apply (wp hoare_drop_imps) - apply simp + apply (simp add: no_fail_def) + apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+ done lemma asUser_setRegister_corres: diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy index 5d33d79026..f90c895e5b 100644 --- a/proof/refine/X64/Tcb_R.thy +++ b/proof/refine/X64/Tcb_R.thy @@ -344,7 +344,7 @@ lemma invokeTCB_WriteRegisters_corres: mask_def user_vtop_def cong: if_cong) apply simp - apply (rule no_fail_pre, wp no_fail_mapM) + apply (wpsimp wp: no_fail_mapM no_fail_setRegister) apply (clarsimp simp: sanitiseOrFlags_def sanitiseAndFlags_def) apply ((safe)[1], (wp no_fail_setRegister | simp)+) apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]]) diff --git a/tools/autocorres/tests/examples/FactorialTest.thy b/tools/autocorres/tests/examples/FactorialTest.thy index de0314c599..0cad8e4130 100644 --- a/tools/autocorres/tests/examples/FactorialTest.thy +++ b/tools/autocorres/tests/examples/FactorialTest.thy @@ -47,7 +47,7 @@ proof (induct n arbitrary: m rule: less_induct) show "no_ofail (\_. unat x < m) (factorial' m x)" apply (subst factorial'.simps) - apply (wp induct_asm ovalid_post_triv) + apply (wpsimp wp: induct_asm ovalid_post_triv) apply unat_arith done qed From 04d4575be5542c88acd4f9157f40ce5d8bab25e0 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 19:44:10 +1030 Subject: [PATCH 49/67] lib: modify no_ofail_obind and no_ofail_pre_imp In order to aid wp-style reasoning Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 4338dd0612..1795fbc82a 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -247,7 +247,7 @@ lemma no_ofail_ogets[wp]: by simp lemma no_ofail_obind[wp]: - "\ \r. no_ofail (P r) (g r); no_ofail Q f; ovalid Q f P \ \ no_ofail Q (obind f g)" + "\ \r. no_ofail (R r) (g r); \Q\ f \R\; no_ofail P f \ \ no_ofail (P and Q) (f |>> g)" by (auto simp: no_ofail_def obind_def ovalid_def) lemma no_ofail_K_bind[wp]: @@ -351,7 +351,7 @@ lemma ovalidNF_pre_imp: by (simp add: ovalidNF_def) lemma no_ofail_pre_imp: - "\ \s. P' s \ P s; no_ofail P f \ \ no_ofail P' f" + "\ no_ofail P f; \s. P' s \ P s \ \ no_ofail P' f" by (simp add: no_ofail_def) lemma ovalid_post_imp: From 0b10a21b8c0e13886fe1b0f2e20a9ffeb1677089 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 19:47:51 +1030 Subject: [PATCH 50/67] lib: add ovalid_post_taut Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 1795fbc82a..af71bedb29 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -59,6 +59,10 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric] (* WP rules for ovalid. *) +lemma ovalid_post_taut[wp]: + "\P\ f \\\\" + by (simp add: ovalid_def) + lemma ovalid_inv[wp]: "ovalid P f (\_. P)" by (simp add: ovalid_def) From 5ac61807425c802d0574f1ff4f488ff9ce6ed162 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 20:29:08 +1030 Subject: [PATCH 51/67] lib: add no_ofail_if Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index af71bedb29..278d25a24f 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -279,6 +279,11 @@ lemma no_ofail_oassert_opt[simp, wp]: "no_ofail (\_. P \ None) (oassert_opt P)" by (simp add: no_ofail_def oassert_opt_def split: option.splits) +lemma no_ofail_if[wp]: + "\ P \ no_ofail Q f; \ P \ no_ofail R g \ + \ no_ofail (if P then Q else R) (if P then f else g)" + by simp + lemma no_ofail_owhen[wp]: "(P \ no_ofail Q f) \ no_ofail (if P then Q else \) (owhen P f)" by (simp add: no_ofail_def owhen_def) From 4905a8ee97c62a548cfe9601dfcfef5f47492c76 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 10 Jan 2024 10:54:38 +1030 Subject: [PATCH 52/67] lib: add defn of list_insert_before, and some lemmas Signed-off-by: Michael McInerney --- lib/ListLibLemmas.thy | 26 ++++++++++++++++++++++++++ lib/List_Lib.thy | 6 ++++++ 2 files changed, 32 insertions(+) diff --git a/lib/ListLibLemmas.thy b/lib/ListLibLemmas.thy index bdb72d61f8..fdb3ba42cf 100644 --- a/lib/ListLibLemmas.thy +++ b/lib/ListLibLemmas.thy @@ -371,6 +371,32 @@ lemma list_insert_after_after: apply fastforce done +lemma list_insert_before_not_found: + "a \ set ls \ list_insert_before ls a new = ls" + by (induct ls; fastforce) + +lemma list_insert_before_nonempty: + "ls \ [] \ list_insert_before ls a new \ []" + by (induct ls; clarsimp) + +lemma list_insert_before_head: + "xs \ [] \ list_insert_before xs (hd xs) new = new # xs" + by (induct xs; fastforce) + +lemma last_of_list_insert_before: + "xs \ [] \ last (list_insert_before xs a new) = last xs" + by (induct xs; clarsimp simp: list_insert_before_nonempty) + +lemma list_insert_before_distinct: + "\distinct (xs @ ys); ys \ []\ \ list_insert_before (xs @ ys) (hd ys) new = xs @ new # ys" + by (induct xs; fastforce simp add: list_insert_before_head) + +lemma set_list_insert_before: + "\new \ set ls; before \ set ls\ \ set (list_insert_before ls before new) = set ls \ {new}" + apply (induct ls; clarsimp) + apply fastforce + done + lemma list_remove_removed: "set (list_remove list x) = (set list) - {x}" apply (induct list,simp+) diff --git a/lib/List_Lib.thy b/lib/List_Lib.thy index 936f86e6e6..e6471707cb 100644 --- a/lib/List_Lib.thy +++ b/lib/List_Lib.thy @@ -26,6 +26,12 @@ primrec list_insert_after :: "'a list \ 'a \ 'a \ \Inserts the value new immediately before the first occurence of a (if any) in the list\ +primrec list_insert_before :: "'a list \ 'a \ 'a \ 'a list" where + "list_insert_before [] a new = []" | + "list_insert_before (x # xs) a new = (if x = a then new # x # xs + else x # list_insert_before xs a new)" + primrec list_remove :: "'a list \ 'a \ 'a list" where "list_remove [] a = []" | "list_remove (x # xs) a = (if x = a then (list_remove xs a) From d5db58fbe9c2203b243d1d8aee7b1d8fb875cc49 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 10 Jan 2024 11:15:36 +1030 Subject: [PATCH 53/67] lib: add Heap_List.thy, for reasoning about linked lists on heaps From the rt branch Signed-off-by: Michael McInerney --- lib/Heap_List.thy | 348 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 348 insertions(+) create mode 100644 lib/Heap_List.thy diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy new file mode 100644 index 0000000000..3b64851eac --- /dev/null +++ b/lib/Heap_List.thy @@ -0,0 +1,348 @@ +(* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +(* Singly-linked lists on heaps or projections from heaps, as predicate and as recursive function. + Loosely after ~~/src/HOL/Hoare/Pointer_Examples.thy *) + +theory Heap_List +imports Main "HOL-Library.Prefix_Order" +begin + +(* Given a heap projection that returns the next-pointer for an object at address x, + given a start pointer x, and an end pointer y, determine if the given list + is the path of addresses visited when following the next-pointers from x to y *) +primrec heap_path :: "('a \ 'a) \ 'a option \ 'a list \ 'a option \ bool" where + "heap_path hp x [] y = (x = y)" +| "heap_path hp x (a#as) y = (x = Some a \ heap_path hp (hp a) as y)" + +(* When a path ends in None, it is a singly-linked list *) +abbreviation heap_ls :: "('a \ 'a) \ 'a option \ 'a list \ bool" where + "heap_ls hp x xs \ heap_path hp x xs None" + +(* Walk a linked list of next pointers, recording which it visited. + Terminates artificially at loops, and otherwise because the address domain is finite *) +function heap_walk :: "('a::finite \ 'a) \ 'a option \ 'a list \ 'a list" where + "heap_walk hp None xs = xs" +| "heap_walk hp (Some x) xs = (if x \ set xs then xs else heap_walk hp (hp x) (xs@[x]))" + by pat_completeness auto + +lemma card_set_UNIV: + fixes xs :: "'a::finite list" + assumes "x \ set xs" + shows "card (set xs) < card(UNIV::'a set)" +proof - + have "finite (UNIV::'a set)" by simp + moreover + from assms have "set xs \ UNIV" by blast + ultimately + show ?thesis by (rule psubset_card_mono) +qed + +termination heap_walk + by (relation "measure (\(_, _, xs). card(UNIV :: 'a set) - card (set xs))"; + simp add: card_set_UNIV diff_less_mono2) + +lemma heap_path_append[simp]: + "heap_path hp start (xs @ ys) end = (\x. heap_path hp start xs x \ heap_path hp x ys end)" + by (induct xs arbitrary: start; simp) + +lemma heap_path_None[simp]: + "heap_path hp None xs end = (xs = [] \ end = None)" + by (cases xs, auto) + +lemma heap_ls_unique: + "\ heap_ls hp x xs; heap_ls hp x ys \ \ xs = ys" + by (induct xs arbitrary: ys x; simp) (case_tac ys; clarsimp) + +lemma heap_ls_hd_not_in_tl: + "heap_ls hp (hp x) xs \ x \ set xs" +proof + assume "x \ set xs" + then obtain ys zs where xs: "xs = ys @ x # zs" by (auto simp: in_set_conv_decomp) + moreover assume "heap_ls hp (hp x) xs" + moreover from this xs have "heap_ls hp (hp x) zs" by clarsimp + ultimately show False by (fastforce dest: heap_ls_unique) +qed + +lemma heap_ls_distinct: + "heap_ls hp x xs \ distinct xs" + by (induct xs arbitrary: x; clarsimp simp: heap_ls_hd_not_in_tl) + +lemma heap_ls_is_walk': + "\ heap_ls hp x xs; set xs \ set ys = {} \ \ heap_walk hp x ys = ys @ xs" + by (frule heap_ls_distinct) (induct xs arbitrary: x ys; clarsimp) + +lemma heap_ls_is_walk: + "heap_ls hp x xs \ heap_walk hp x [] = xs" + using heap_ls_is_walk' by fastforce + +lemma heap_path_end_unique: + "heap_path hp x xs y \ heap_path hp x xs y' \ y = y'" + by (induct xs arbitrary: x; clarsimp) + +lemma heap_path_head: + "heap_path hp x xs y \ xs \ [] \ x = Some (hd xs)" + by (induct xs arbitrary: x; clarsimp) + +lemma heap_path_non_nil_lookup_next: + "heap_path hp x (xs@z#ys) y \ hp z = (case ys of [] \ y | _ \ Some (hd ys))" + by (cases ys; fastforce) + +lemma heap_path_prefix: + "heap_path hp st ls ed \ \xs\ls. heap_path hp st xs (if xs = [] then st else hp (last xs))" + apply clarsimp + apply (erule Prefix_Order.prefixE) + by (metis append_butlast_last_id heap_path_append heap_path_non_nil_lookup_next list.case(1)) + +lemma heap_path_butlast: + "heap_path hp st ls ed \ ls \ [] \ heap_path hp st (butlast ls) (Some (last ls))" + by (induct ls rule: rev_induct; simp) + +lemma in_list_decompose_takeWhile: + "x \ set xs \ + xs = (takeWhile ((\) x) xs) @ x # (drop (length (takeWhile ((\) x) xs) + 1) xs)" + by (induct xs arbitrary: x; clarsimp) + +lemma takeWhile_neq_hd_eq_Nil[simp]: + "takeWhile ((\) (hd xs)) xs = Nil" + by (metis (full_types) hd_Cons_tl takeWhile.simps(1) takeWhile.simps(2)) + +lemma heap_not_in_dom[simp]: + "ptr \ dom hp \ hp(ptr := None) = hp" + by (auto simp: dom_def) + +lemma heap_path_takeWhile_lookup_next: + "\ heap_path hp st rs ed; r \ set rs \ + \ heap_path hp st (takeWhile ((\) r) rs) (Some r)" + apply (drule heap_path_prefix) + apply (subgoal_tac "takeWhile ((\) r) rs @ [r] \ rs", fastforce) + by (fastforce dest!: in_list_decompose_takeWhile intro: Prefix_Order.prefixI) + +lemma heap_path_heap_upd_not_in: + "\heap_path hp st rs ed; r \ set rs\ \ heap_path (hp(r:= x)) st rs ed" + by (induct rs arbitrary: st; clarsimp) + +lemma heap_walk_lb: + "heap_walk hp x xs \ xs" + apply (induct xs rule: heap_walk.induct; clarsimp) + by (metis Prefix_Order.prefixE Prefix_Order.prefixI append_assoc) + +lemma heal_walk_Some_nonempty': + "heap_walk hp (Some x) [] > []" + by (fastforce intro: heap_walk_lb less_le_trans[where y="[x]"]) + +lemma heal_walk_Some_nonempty: + "heap_walk hp (Some x) [] \ []" + by (metis less_list_def heal_walk_Some_nonempty') + +lemma heap_walk_Nil_None: + "heap_walk hp st [] = [] \ st = None" + by (case_tac st; simp only: heal_walk_Some_nonempty) + +lemma heap_ls_last_None: + "heap_ls hp st xs \ xs \ [] \ hp (last xs) = None" + by (induct xs rule: rev_induct; clarsimp) + +(* sym_heap *) + +definition sym_heap where + "sym_heap hp hp' \ \p p'. hp p = Some p' \ hp' p' = Some p" + +lemma sym_heapD1: + "sym_heap hp hp' \ hp p = Some p' \ hp' p' = Some p" + by (clarsimp simp: sym_heap_def) + +lemma sym_heapD2: + "sym_heap hp hp' \ hp' p' = Some p \ hp p = Some p'" + by (clarsimp simp: sym_heap_def) + +lemma sym_heap_symmetric: + "sym_heap hp hp' \ sym_heap hp' hp" + unfolding sym_heap_def by blast + +lemma sym_heap_None: + "\sym_heap hp hp'; hp p = None\ \ \p'. hp' p' \ Some p" unfolding sym_heap_def by force + +lemma sym_heap_path_reverse: + "sym_heap hp hp' \ + heap_path hp (Some p) (p#ps) (Some p') + \ heap_path hp' (Some p') (p'#(rev ps)) (Some p)" + unfolding sym_heap_def by (induct ps arbitrary: p p' rule: rev_induct; force) + +lemma sym_heap_ls_rev_Cons: + "\sym_heap hp hp'; heap_ls hp (Some p) (p#ps)\ + \ heap_path hp' (Some (last (p#ps))) (rev ps) (Some p)" + supply rev.simps[simp del] + apply (induct ps arbitrary: p rule: rev_induct; simp add: rev.simps) + by (auto dest!: sym_heap_path_reverse[THEN iffD1]) + +lemma sym_heap_ls_rev: + "\sym_heap hp hp'; heap_ls hp (Some p) ps\ + \ heap_path hp' (Some (last ps)) (butlast (rev ps)) (Some p) + \ hp (last ps) = None" + apply (induct ps arbitrary: p rule: rev_induct, simp) + apply (frule heap_path_head; clarsimp) + by (auto dest!: sym_heap_path_reverse[THEN iffD1]) + +(* more on heap_path : next/prev in path *) + +lemma heap_path_extend: + "heap_path hp st (ls @ [p]) (hp p) \ heap_path hp st ls (Some p)" + by (induct ls rule: rev_induct; simp) + +lemma heap_path_prefix_heap_ls: + "\heap_ls hp st xs; heap_path hp st ys ed\ \ ys \ xs" + apply (induct xs arbitrary: ys st, simp) + apply (case_tac ys; clarsimp) + done + +lemma distinct_decompose2: + "\distinct xs; xs = ys @ x # y # zs\ + \ x \ y \ x \ set ys \ y \ set ys \ x \ set zs \ y \ set zs" + by (simp add: in_set_conv_decomp) + +lemma heap_path_distinct_next_cases: (* the other direction needs sym_heap *) + "\heap_path hp st xs ed; distinct xs; p \ set xs; hp p = Some np\ + \ ed = Some p \ ed = Some np \ np \ set xs" + apply (cases ed; simp) + apply (frule in_list_decompose_takeWhile) + apply (subgoal_tac "heap_ls hp st (takeWhile ((\) p) xs @ p # drop (length (takeWhile ((\) p) xs) + 1) xs)") + apply (drule heap_path_non_nil_lookup_next) + apply (case_tac "drop (length (takeWhile ((\) p) xs) + 1) xs"; simp) + apply (metis in_set_dropD list.set_intros(1)) + apply simp + apply (frule in_list_decompose_takeWhile) + apply (subgoal_tac "heap_path hp st (takeWhile ((\) p) xs @ p # drop (length (takeWhile ((\) p) xs) + 1) xs) ed") + apply (frule heap_path_non_nil_lookup_next) + apply (case_tac "drop (length (takeWhile ((\) p) xs) + 1) xs", simp) + apply (simp split: if_split_asm) + apply (drule (1) distinct_decompose2) + apply clarsimp + by (metis in_set_dropD list.set_intros(1)) simp + +lemma heap_ls_next_in_list: + "\heap_ls hp st xs; p \ set xs; hp p = Some np\ + \ np \ set xs" + apply (subgoal_tac "distinct xs") + by (fastforce dest!: heap_path_distinct_next_cases) (erule heap_ls_distinct) + +lemma heap_path_distinct_sym_prev_cases: + "\heap_path hp st xs ed; distinct xs; np \ set xs; hp p = Some np; sym_heap hp hp'\ + \ st = Some np \ p \ set xs" + apply (cases st; simp) + apply (rename_tac stp) + apply (case_tac "stp = np"; simp) + apply (cases xs; simp del: heap_path.simps) + apply (frule heap_path_head, simp) + apply (cases ed, clarsimp) + apply (frule sym_heap_ls_rev_Cons, fastforce) + apply (drule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def) + apply simp + apply (simp del: heap_path.simps) + apply (frule (1) sym_heap_path_reverse[where hp'=hp', THEN iffD1]) + apply simp + apply (frule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def) + apply fastforce + done + +lemma heap_ls_prev_cases: + "\heap_ls hp st xs; np \ set xs; hp p = Some np; sym_heap hp hp'\ + \ st = Some np \ p \ set xs" + apply (subgoal_tac "distinct xs") + by (fastforce dest!: heap_path_distinct_sym_prev_cases) (erule heap_ls_distinct) + +lemma heap_ls_prev_not_in: + "\heap_ls hp st xs; np \ set xs; hp p = Some np\ + \ p \ set xs" + by (meson heap_ls_next_in_list) + +lemma heap_path_distinct_prev_not_in: + "\heap_path hp st xs ed; distinct xs; np \ set xs; hp p = Some np; ed \ Some np; ed \ Some p\ + \ p \ set xs" + using heap_path_distinct_next_cases + by fastforce + +lemma heap_path_distinct_next_not_in: + "\heap_path hp st xs ed; distinct xs; p \ set xs; hp p = Some np; + sym_heap hp hp'; st \ Some np\ + \ np \ set xs" + by (fastforce dest!: heap_path_distinct_sym_prev_cases[simplified]) + +lemma heap_ls_next_not_in: + "\heap_ls hp st xs; p \ set xs; hp p = Some np; sym_heap hp hp'; st \ Some np\ + \ np \ set xs" + by (fastforce dest!: heap_ls_prev_cases[simplified]) + +(* more on heap_path *) + +(* moved from ListLibLemmas *) +lemma distinct_inj_middle: "distinct list \ list = (xa @ x # xb) \ list = (ya @ x # yb) \ xa = ya \ xb = yb" + apply (induct list arbitrary: xa ya) + apply simp + apply clarsimp + apply (case_tac "xa") + apply simp + apply (case_tac "ya") + apply simp + apply clarsimp + apply clarsimp + apply (case_tac "ya") + apply (simp (no_asm_simp)) + apply simp + apply clarsimp + done + +lemma heap_ls_next_takeWhile_append: + "\heap_ls hp st xs; p \ set xs; hp p = Some np\ + \ takeWhile ((\) np) xs = (takeWhile ((\) p) xs) @ [p]" + apply (frule heap_ls_distinct) + apply (frule in_list_decompose_takeWhile) + apply (subgoal_tac "heap_ls hp st (takeWhile ((\) p) xs @ p # drop (length (takeWhile ((\) p) xs) + 1) xs)") + prefer 2 apply simp + apply (drule heap_path_non_nil_lookup_next) + apply (case_tac "drop (length (takeWhile ((\) p) xs) + 1) xs"; simp) + apply (subgoal_tac "np \ set xs") + prefer 2 apply (erule (2) heap_ls_next_in_list) + apply (frule in_list_decompose_takeWhile[where x=np]) + apply (drule (1) distinct_inj_middle[where x=np and xa="takeWhile ((\) np) xs" and ya="takeWhile ((\) p) xs @ [p]"]) + apply simp+ + done + +(* RT FIXME: Move *) +lemma takeWhile_neq_notin_same: + "x \ set xs \ takeWhile ((\) x) xs = xs" + using takeWhile_eq_all_conv by blast + +lemma heap_path_extend_takeWhile: + "\heap_ls hp st xs; heap_path hp st (takeWhile ((\) p) xs) (Some p); hp p = Some np\ + \ heap_path hp st (takeWhile ((\) np) xs) (Some np)" + apply (case_tac "p \ set xs") + apply (subst heap_ls_next_takeWhile_append[where p=p and np=np and hp=hp]; simp) + apply (drule takeWhile_neq_notin_same, simp) + apply (drule (1) heap_path_end_unique, simp) + done + +lemma heap_ls_next_takeWhile_append_sym: + "\heap_ls hp st xs; np \ set xs; st \ Some np; hp p = Some np; sym_heap hp hp'\ + \takeWhile ((\) np) xs = (takeWhile ((\) p) xs) @ [p]" + apply (frule (3) heap_ls_prev_cases, simp) + apply (fastforce elim!: heap_ls_next_takeWhile_append) + done + +lemma heap_path_curtail_takeWhile: + "\heap_ls hp st xs; heap_path hp st (takeWhile ((\) np) xs) (Some np); + st \ Some np; hp p = Some np; sym_heap hp hp'\ + \ heap_path hp st (takeWhile ((\) p) xs) (Some p)" + apply (case_tac "np \ set xs") + apply (drule (4) heap_ls_next_takeWhile_append_sym) + apply simp + apply (drule takeWhile_neq_notin_same, simp) + apply (drule (1) heap_path_end_unique, simp) + done + +(* more on heap_path : end *) + +end \ No newline at end of file From a3eb113e750b23fdf115d60d93bcf0a7dfefd435 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 10 Jan 2024 11:20:05 +1030 Subject: [PATCH 54/67] lib: heap_ls lemmas relating an update to the list to an update to the heap Signed-off-by: Michael McInerney --- lib/Heap_List.thy | 103 +++++++++++++++++++++++++++++++++++++--------- 1 file changed, 83 insertions(+), 20 deletions(-) diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy index 3b64851eac..b3e7e78ce9 100644 --- a/lib/Heap_List.thy +++ b/lib/Heap_List.thy @@ -8,7 +8,7 @@ Loosely after ~~/src/HOL/Hoare/Pointer_Examples.thy *) theory Heap_List -imports Main "HOL-Library.Prefix_Order" +imports Main "HOL-Library.Prefix_Order" ListLibLemmas begin (* Given a heap projection that returns the next-pointer for an object at address x, @@ -125,6 +125,10 @@ lemma heap_path_heap_upd_not_in: "\heap_path hp st rs ed; r \ set rs\ \ heap_path (hp(r:= x)) st rs ed" by (induct rs arbitrary: st; clarsimp) +lemma heap_path_last_update: + "\heap_path hp st xs end; xs \ []; distinct xs\ \ heap_path (hp(last xs := new)) st xs new" + by (induct xs arbitrary: st rule: rev_induct; simp add: heap_path_heap_upd_not_in) + lemma heap_walk_lb: "heap_walk hp x xs \ xs" apply (induct xs rule: heap_walk.induct; clarsimp) @@ -142,10 +146,12 @@ lemma heap_walk_Nil_None: "heap_walk hp st [] = [] \ st = None" by (case_tac st; simp only: heal_walk_Some_nonempty) -lemma heap_ls_last_None: - "heap_ls hp st xs \ xs \ [] \ hp (last xs) = None" +lemma heap_path_last_end: + "heap_path hp st xs end \ xs \ [] \ hp (last xs) = end" by (induct xs rule: rev_induct; clarsimp) +lemmas heap_ls_last_None = heap_path_last_end[where ?end=None] + (* sym_heap *) definition sym_heap where @@ -278,23 +284,6 @@ lemma heap_ls_next_not_in: (* more on heap_path *) -(* moved from ListLibLemmas *) -lemma distinct_inj_middle: "distinct list \ list = (xa @ x # xb) \ list = (ya @ x # yb) \ xa = ya \ xb = yb" - apply (induct list arbitrary: xa ya) - apply simp - apply clarsimp - apply (case_tac "xa") - apply simp - apply (case_tac "ya") - apply simp - apply clarsimp - apply clarsimp - apply (case_tac "ya") - apply (simp (no_asm_simp)) - apply simp - apply clarsimp - done - lemma heap_ls_next_takeWhile_append: "\heap_ls hp st xs; p \ set xs; hp p = Some np\ \ takeWhile ((\) np) xs = (takeWhile ((\) p) xs) @ [p]" @@ -345,4 +334,78 @@ lemma heap_path_curtail_takeWhile: (* more on heap_path : end *) + +\ \Lemmas relating an update to the list to an update to the heap\ + +lemma heap_ls_prepend: + "\heap_ls hp st xs; new \ set xs; xs \ []\ + \ heap_ls (hp(new := Some (hd xs))) (Some new) (new # xs)" + apply simp + apply (erule heap_path_heap_upd_not_in[rotated]) + apply (frule (1) heap_path_head) + apply fastforce + done + +lemma heap_ls_append: + "\heap_ls hp st xs; xs \ []; new \ set xs\ + \ heap_ls (hp(last xs := Some new, new := None)) st (xs @ [new])" + apply (frule heap_ls_distinct) + apply simp + apply (rule heap_path_heap_upd_not_in) + apply (fastforce simp: heap_path_last_update) + apply assumption + done + +lemma heap_ls_list_insert_before: + "\heap_ls hp st (xs @ ys); new \ set (xs @ ys); xs \ []; ys \ []\ + \ heap_ls (hp(last xs := Some new, new := Some (hd ys))) st + (list_insert_before (xs @ ys) (hd ys) new)" + apply (frule heap_ls_distinct) + apply (subst list_insert_before_distinct; fastforce?) + apply simp + apply (rule conjI) + \ \the path until new\ + apply (fastforce intro: heap_path_heap_upd_not_in heap_path_last_update) + \ \the path from hd ys\ + apply (metis disjoint_iff_not_equal heap_path_head heap_path_heap_upd_not_in last_in_set) + done + +lemma heap_ls_remove_singleton: + "heap_ls hp st [x] \ heap_ls (hp(x := None)) None []" + by simp + +lemma heap_ls_remove_head_not_singleton: + "\heap_ls hp st xs; tl xs \ []\ + \ heap_ls (hp(hd xs := None)) (Some (hd (tl xs))) (tl xs)" + apply (frule heap_ls_distinct) + apply (cases xs; simp) + apply clarsimp + apply (frule heap_path_head) + apply fastforce + apply (fastforce elim!: heap_path_heap_upd_not_in) + done + +lemma heap_ls_remove_last_not_singleton: + "\heap_ls hp st xs; butlast xs \ []\ + \ heap_ls (hp((last (butlast xs)) := None)) st (butlast xs)" + apply (frule heap_ls_distinct) + apply (frule distinct_butlast) + apply (fastforce dest: heap_path_last_update heap_path_butlast) + done + +lemma heap_ls_remove_middle: + "\heap_ls hp st (xs @ a # ys); xs \ []; ys \ []\ + \ heap_ls (hp(last xs := Some (hd ys), a := None)) st (xs @ ys)" + apply (frule heap_ls_distinct) + apply simp + apply (rule_tac x="Some (hd ys)" in exI) + apply (rule conjI) + apply (fastforce intro: heap_path_heap_upd_not_in heap_path_last_update) + apply (rule heap_path_heap_upd_not_in) + apply (rule heap_path_heap_upd_not_in) + using heap_path_head apply fastforce + apply force + apply fastforce + done + end \ No newline at end of file From b6b89fe713aa4a24a34cd38bbaeb1cd40a172d81 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jan 2024 23:55:31 +1030 Subject: [PATCH 55/67] lib: add heap_path_sym_heap_non_nil_lookup_prev Signed-off-by: Michael McInerney --- lib/Heap_List.thy | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy index b3e7e78ce9..0d20cf0a0e 100644 --- a/lib/Heap_List.thy +++ b/lib/Heap_List.thy @@ -193,6 +193,16 @@ lemma sym_heap_ls_rev: apply (frule heap_path_head; clarsimp) by (auto dest!: sym_heap_path_reverse[THEN iffD1]) +lemma heap_path_sym_heap_non_nil_lookup_prev: + "\heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \ []\ \ hp' z = (Some (last xs))" + supply heap_path_append[simp del] + apply (cut_tac xs="butlast xs" and z="last xs" and ys="z # ys" + in heap_path_non_nil_lookup_next[where hp=hp and x=x and y=None]) + apply (frule append_butlast_last_id) + apply (metis append_eq_Cons_conv append_eq_append_conv2) + apply (fastforce dest: sym_heapD1) + done + (* more on heap_path : next/prev in path *) lemma heap_path_extend: From 10f91566b1e5dec6f87975f40b70da0717124adb Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 10 Jan 2024 00:00:06 +1030 Subject: [PATCH 56/67] lib: add fun_upd_swap Signed-off-by: Michael McInerney --- lib/Lib.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Lib.thy b/lib/Lib.thy index 69c29df3f7a..1374020d11 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -2558,6 +2558,10 @@ lemma ranD: "v \ ran f \ \x. f x = Some v" by (auto simp: ran_def) +lemma fun_upd_swap: + "a \ c \ hp(c := d, a := b) = hp(a := b, c := d)" + by fastforce + text \Prevent clarsimp and others from creating Some from not None by folding this and unfolding again when safe.\ From 3255722e1acaa7ca95866aa680168d564987b1aa Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 10 Jan 2024 00:20:30 +1030 Subject: [PATCH 57/67] lib: several miscellaneous lemmas for heap_ls Signed-off-by: Michael McInerney --- lib/Heap_List.thy | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy index 0d20cf0a0e..85dbb4ea55 100644 --- a/lib/Heap_List.thy +++ b/lib/Heap_List.thy @@ -292,6 +292,22 @@ lemma heap_ls_next_not_in: \ np \ set xs" by (fastforce dest!: heap_ls_prev_cases[simplified]) +lemma sym_heap_prev_None_is_start: + "\heap_ls hp st xs; sym_heap hp hp'; p \ set xs; hp' p = None\ + \ Some p = st" + using split_list_last heap_path_sym_heap_non_nil_lookup_prev + by fastforce + +lemma not_last_next_not_None: + "\heap_ls hp st xs; p \ set xs; p \ last xs\ \ hp p \ None" + by (fastforce intro: heap_path_head dest: split_list) + +lemma not_head_prev_not_None: + "\heap_ls hp st xs; p \ set xs; p \ hd xs; sym_heap hp hp'\ + \ hp' p \ None" + using sym_heap_prev_None_is_start heap_path_head + by fastforce + (* more on heap_path *) lemma heap_ls_next_takeWhile_append: From a463ca7a9ab98f8bcdfecfb69a2f428e0bf20517 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 10 Jan 2024 00:34:40 +1030 Subject: [PATCH 58/67] lib: add "no loops" lemmas for heap_ls Signed-off-by: Michael McInerney --- lib/Heap_List.thy | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy index 85dbb4ea55..80aabd2d25 100644 --- a/lib/Heap_List.thy +++ b/lib/Heap_List.thy @@ -203,6 +203,16 @@ lemma heap_path_sym_heap_non_nil_lookup_prev: apply (fastforce dest: sym_heapD1) done +lemma heap_ls_no_loops: + "\heap_ls hp st xs; p \ set xs\ \ hp p \ Some p" + apply (frule heap_ls_distinct) + apply (fastforce dest: split_list heap_path_non_nil_lookup_next split: list.splits) + done + +lemma heap_ls_prev_no_loops: + "\heap_ls hp st xs; p \ set xs; sym_heap hp hp'\ \ hp' p \ Some p" + by (fastforce dest: heap_ls_no_loops sym_heapD2) + (* more on heap_path : next/prev in path *) lemma heap_path_extend: From afcbba9a6d30e3527309cdad724f6bdd498ed764 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 10 Jan 2024 00:56:15 +1030 Subject: [PATCH 59/67] lib: some sym_heap lemmas regarding heap updates Signed-off-by: Michael McInerney --- lib/Heap_List.thy | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy index 80aabd2d25..e8bae311db 100644 --- a/lib/Heap_List.thy +++ b/lib/Heap_List.thy @@ -172,6 +172,38 @@ lemma sym_heap_symmetric: lemma sym_heap_None: "\sym_heap hp hp'; hp p = None\ \ \p'. hp' p' \ Some p" unfolding sym_heap_def by force +lemma sym_heap_remove_only: + "\sym_heap hp hp'; hp' y = Some x\ \ sym_heap (hp(x := None)) (hp'(y := None))" + apply (clarsimp simp: sym_heap_def) + apply (metis option.inject) + done + +lemma sym_heap_remove_only': + "\sym_heap hp hp'; hp y = Some x\ \ sym_heap (hp(y := None)) (hp'(x := None))" + apply (clarsimp simp: sym_heap_def) + apply (metis option.inject) + done + +lemma sym_heap_remove_middle_from_chain: + "\sym_heap hp hp'; before \ middle; middle \ after; + hp before = Some middle; hp middle = Some after\ + \ sym_heap (hp(before := Some after, middle := None)) + (hp'(after := Some before, middle := None))" + apply (clarsimp simp: sym_heap_def) + apply (metis option.simps(1)) + done + +lemma sym_heap_connect: + "\sym_heap hp hp'; hp a = None; hp' b = None \ \ sym_heap (hp(a \ b)) (hp'(b \ a))" + by (force simp: sym_heap_def) + +lemma sym_heap_insert_into_middle_of_chain: + "\sym_heap hp hp'; hp before = Some after; hp middle = None; hp' middle = None\ + \ sym_heap (hp(before \ middle, middle \ after)) (hp'(after \ middle, middle \ before))" + apply (clarsimp simp: sym_heap_def) + apply (metis option.simps) + done + lemma sym_heap_path_reverse: "sym_heap hp hp' \ heap_path hp (Some p) (p#ps) (Some p') From 52b4ba509195a554c96b108d48c2993bc39c8e23 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 4 Jan 2024 11:15:22 +1100 Subject: [PATCH 60/67] aarch64 machine+aspec+cspec: pt_type ghost+table array sizes - add ghost state corresponding to gsPTTypes in Haskell and ASpec - add ghost type comments - style update for old definitions since we need to touch most of these - define vs/pt_array_len for use in C annotations - make NormalPT_T/VSRootPT_T names available for use in C annotations Signed-off-by: Gerwin Klein --- spec/abstract/AARCH64/Arch_Structs_A.thy | 43 +------------ spec/cspec/AARCH64/Kernel_C.thy | 79 +++++++++++++++--------- spec/machine/AARCH64/Platform.thy | 59 ++++++++++++++++++ 3 files changed, 110 insertions(+), 71 deletions(-) diff --git a/spec/abstract/AARCH64/Arch_Structs_A.thy b/spec/abstract/AARCH64/Arch_Structs_A.thy index 075a7e3b26..fbc5113380 100644 --- a/spec/abstract/AARCH64/Arch_Structs_A.thy +++ b/spec/abstract/AARCH64/Arch_Structs_A.thy @@ -113,48 +113,7 @@ definition pte_base_addr :: "pte \ paddr" where definition ppn_from_pptr :: "obj_ref \ ppn" where "ppn_from_pptr p = ucast (addrFromPPtr p >> pageBits)" -definition vs_index_bits :: nat where - "vs_index_bits \ if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)" - -lemma vs_index_bits_ge0[simp, intro!]: "0 < vs_index_bits" - by (simp add: vs_index_bits_def) - -(* A dependent-ish type in Isabelle. We use typedef here instead of value_type so that we can - retain a symbolic value (vs_index_bits) for the size of the type instead of getting a plain - number such as 9 or 10. *) -typedef vs_index_len = "{n :: nat. n < vs_index_bits}" by auto - -end - -instantiation AARCH64_A.vs_index_len :: len0 -begin - interpretation Arch . - definition len_of_vs_index_len: "len_of (x::vs_index_len itself) \ CARD(vs_index_len)" - instance .. -end - -instantiation AARCH64_A.vs_index_len :: len -begin - interpretation Arch . - instance - proof - show "0 < LENGTH(vs_index_len)" - by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len]) - qed -end - -context Arch begin global_naming AARCH64_A - -type_synonym vs_index = "vs_index_len word" - -type_synonym pt_index_len = 9 -type_synonym pt_index = "pt_index_len word" - -text \Sanity check:\ -lemma length_vs_index_len[simp]: - "LENGTH(vs_index_len) = vs_index_bits" - by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len]) - +(* Sanity check for page table type sizes -- ptTranslationBits not yet available at definition site *) lemma vs_index_ptTranslationBits: "ptTranslationBits VSRootPT_T = LENGTH(vs_index_len)" by (simp add: ptTranslationBits_def vs_index_bits_def) diff --git a/spec/cspec/AARCH64/Kernel_C.thy b/spec/cspec/AARCH64/Kernel_C.thy index 60636c5c8d..254e030c7f 100644 --- a/spec/cspec/AARCH64/Kernel_C.thy +++ b/spec/cspec/AARCH64/Kernel_C.thy @@ -18,6 +18,8 @@ context begin interpretation Arch . requalify_types machine_state + pt_array_len + vs_array_len end @@ -25,54 +27,73 @@ declare [[populate_globals=true]] context begin interpretation Arch . (*FIXME: arch_split*) -type_synonym cghost_state = "(machine_word \ vmpage_size) * (machine_word \ nat) - * ghost_assertions" +(* Sanity checks for array sizes. ptTranslationBits not yet available at definition site. *) +lemma ptTranslationBits_vs_index_bits: + "ptTranslationBits VSRootPT_T = vs_index_bits" + by (simp add: ptTranslationBits_def vs_index_bits_def) -definition - gs_clear_region :: "addr \ nat \ cghost_state \ cghost_state" where +(* FIXME AARCH64: this is guaranteed to always succeed even though config_ARM_PA_SIZE_BITS_40 + is unfolded. It'd be nicer if we could also get something symbolic out of value_type, though *) +lemma ptTranslationBits_vs_array_len': + "2 ^ ptTranslationBits VSRootPT_T = vs_array_len" + by (simp add: vs_array_len_def ptTranslationBits_vs_index_bits vs_index_bits_def + Kernel_Config.config_ARM_PA_SIZE_BITS_40_def) + +lemmas ptTranslationBits_vs_array_len = ptTranslationBits_vs_array_len'[unfolded vs_array_len_def] + +type_synonym cghost_state = + "(machine_word \ vmpage_size) \ \ \Frame sizes\ + (machine_word \ nat) \ \ \CNode sizes\ + (machine_word \ pt_type) \ \ \PT types\ + ghost_assertions" \ \ASMRefine assertions\ + +definition gs_clear_region :: "addr \ nat \ cghost_state \ cghost_state" where "gs_clear_region ptr bits gs \ - (%x. if x \ {ptr..+2 ^ bits} then None else fst gs x, - %x. if x \ {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))" + (\x. if x \ {ptr..+2 ^ bits} then None else fst gs x, + \x. if x \ {ptr..+2 ^ bits} then None else fst (snd gs) x, + \x. if x \ {ptr..+2 ^ bits} then None else fst (snd (snd gs)) x, + snd (snd (snd gs)))" -definition - gs_new_frames:: "vmpage_size \ addr \ nat \ cghost_state \ cghost_state" - where +definition gs_new_frames:: "vmpage_size \ addr \ nat \ cghost_state \ cghost_state" where "gs_new_frames sz ptr bits \ \gs. - if bits < pageBitsForSize sz then gs - else (\x. if \n\mask (bits - pageBitsForSize sz). - x = ptr + n * 2 ^ pageBitsForSize sz then Some sz - else fst gs x, snd gs)" + if bits < pageBitsForSize sz then gs + else (\x. if \n\mask (bits - pageBitsForSize sz). + x = ptr + n * 2 ^ pageBitsForSize sz then Some sz + else fst gs x, snd gs)" -definition - gs_new_cnodes:: "nat \ addr \ nat \ cghost_state \ cghost_state" - where +definition gs_new_cnodes:: "nat \ addr \ nat \ cghost_state \ cghost_state" where "gs_new_cnodes sz ptr bits \ \gs. - if bits < sz + 4 then gs - else (fst gs, \x. if \n\mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4) - then Some sz - else fst (snd gs) x, snd (snd gs))" + if bits < sz + 4 then gs + else (fst gs, \x. if \n\mask (bits - sz - 4). x = ptr + n * 2 ^ (sz + 4) + then Some sz + else fst (snd gs) x, snd (snd gs))" + +definition gs_new_pt_t:: "pt_type \ addr \ cghost_state \ cghost_state" where + "gs_new_pt_t pt_t ptr \ + \gs. (fst gs, fst (snd gs), (fst (snd (snd gs))) (ptr \ pt_t), snd (snd (snd gs)))" -abbreviation - gs_get_assn :: "int \ cghost_state \ machine_word" - where - "gs_get_assn k \ ghost_assertion_data_get k (snd o snd)" +abbreviation gs_get_assn :: "int \ cghost_state \ machine_word" where + "gs_get_assn k \ ghost_assertion_data_get k (snd \ snd \ snd)" -abbreviation - gs_set_assn :: "int \ machine_word \ cghost_state \ cghost_state" - where - "gs_set_assn k v \ ghost_assertion_data_set k v (apsnd o apsnd)" +abbreviation gs_set_assn :: "int \ machine_word \ cghost_state \ cghost_state" where + "gs_set_assn k v \ ghost_assertion_data_set k v (apsnd \ apsnd \ apsnd)" declare [[record_codegen = false]] declare [[allow_underscore_idents = true]] end -(* workaround for the fact that the C parser wants to know the vmpage sizes*) +(* Workaround for the fact that the retype annotations need the vmpage sizes*) (* create appropriately qualified aliases *) context begin interpretation Arch . global_naming vmpage_size requalify_consts ARMSmallPage ARMLargePage ARMHugePage end +(* Also need pt_type constructors for retype annotations. We leave them available globally for C. *) +context begin interpretation Arch . +requalify_consts NormalPT_T VSRootPT_T +end + definition ctcb_size_bits :: nat where diff --git a/spec/machine/AARCH64/Platform.thy b/spec/machine/AARCH64/Platform.thy index 40f0b3e7e9..6d6c5c712a 100644 --- a/spec/machine/AARCH64/Platform.thy +++ b/spec/machine/AARCH64/Platform.thy @@ -101,5 +101,64 @@ definition irqVTimerEvent :: irq where definition pageColourBits :: nat where "pageColourBits \ undefined" \ \not implemented on this platform\ + +section \Page table sizes\ + +definition vs_index_bits :: nat where + "vs_index_bits \ if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)" + +end + +(* Need to declare code equation outside Arch locale *) +declare AARCH64.vs_index_bits_def[code] + +context Arch begin global_naming AARCH64 + +lemma vs_index_bits_ge0[simp, intro!]: "0 < vs_index_bits" + by (simp add: vs_index_bits_def) + +(* A dependent-ish type in Isabelle. We use typedef here instead of value_type so that we can + retain a symbolic value (vs_index_bits) for the size of the type instead of getting a plain + number such as 9 or 10. *) +typedef vs_index_len = "{n :: nat. n < vs_index_bits}" by auto + end + +instantiation AARCH64.vs_index_len :: len0 +begin + interpretation Arch . + definition len_of_vs_index_len: "len_of (x::vs_index_len itself) \ CARD(vs_index_len)" + instance .. +end + +instantiation AARCH64.vs_index_len :: len +begin + interpretation Arch . + instance + proof + show "0 < LENGTH(vs_index_len)" + by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len]) + qed +end + +context Arch begin global_naming AARCH64 + +type_synonym vs_index = "vs_index_len word" + +type_synonym pt_index_len = 9 +type_synonym pt_index = "pt_index_len word" + +text \Sanity check:\ +lemma length_vs_index_len[simp]: + "LENGTH(vs_index_len) = vs_index_bits" + by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len]) + + +section \C array sizes corresponding to page table sizes\ + +value_type pt_array_len = "(2::nat) ^ LENGTH(pt_index_len)" +value_type vs_array_len = "(2::nat) ^ vs_index_bits" + +end + end From dd315e16dd47ccc92bc0e96760eab7ea90eb6bc2 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 15 Jan 2024 18:13:01 +1030 Subject: [PATCH 61/67] lib: add Heap_List to ROOT Signed-off-by: Michael McInerney --- lib/ROOT | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/ROOT b/lib/ROOT index 9ff4b9c4a1..5a2970e13a 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -67,6 +67,7 @@ session Lib (lib) = Word_Lib + Value_Type Named_Eta Rules_Tac + Heap_List (* should move to Monads: *) NonDetMonadLemmaBucket From 4d7cc19ec0592fb344a4a7a472078369525b9f3d Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 16 Jan 2024 10:03:42 +1100 Subject: [PATCH 62/67] c-parser+autocorres: update Simpl links Avoid redirects, link to current canonical version. Signed-off-by: Gerwin Klein --- tools/autocorres/doc/quickstart/document/root.bib | 2 +- tools/autocorres/tools/release_files/README | 2 +- tools/c-parser/README.md | 2 +- tools/c-parser/Simpl/README.md | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tools/autocorres/doc/quickstart/document/root.bib b/tools/autocorres/doc/quickstart/document/root.bib index 78fdd1bbec..a1afca31e7 100644 --- a/tools/autocorres/doc/quickstart/document/root.bib +++ b/tools/autocorres/doc/quickstart/document/root.bib @@ -44,7 +44,7 @@ @article{Simpl-AFP journal = {Archive of Formal Proofs}, month = feb, year = 2008, - url = {https://www.isa-afp.org/entries/Simpl.shtml}, + url = {https://www.isa-afp.org/entries/Simpl.html}, note = {Formal proof development}, ISSN = {2150-914X}, } diff --git a/tools/autocorres/tools/release_files/README b/tools/autocorres/tools/release_files/README index 85a2444f1e..4e5611f891 100644 --- a/tools/autocorres/tools/release_files/README +++ b/tools/autocorres/tools/release_files/README @@ -112,7 +112,7 @@ This package contains: * Norbert Schirmer's Simpl language and associated VCG tool. The C parser translates C into Schirmer's Simpl language: - https://www.isa-afp.org/entries/Simpl.shtml + https://www.isa-afp.org/entries/Simpl.html * Code from SML/NJ, including an implementation of binary sets (Binaryset.ML) and the mllex and mlyacc tools diff --git a/tools/c-parser/README.md b/tools/c-parser/README.md index 87628fa5e8..ca00754bde 100644 --- a/tools/c-parser/README.md +++ b/tools/c-parser/README.md @@ -31,7 +31,7 @@ The translation tool builds on various open source projects by others. Sources for this are found in the Simpl/ directory. The code is covered by an LGPL licence. - See + See 2. Code from SML/NJ: - an implementation of binary sets (Binaryset.ML) diff --git a/tools/c-parser/Simpl/README.md b/tools/c-parser/Simpl/README.md index 30275d46d4..7d9987174c 100644 --- a/tools/c-parser/Simpl/README.md +++ b/tools/c-parser/Simpl/README.md @@ -10,4 +10,4 @@ Simpl This directory contains Norbert Schirmer's Simpl language and associated VCG tool. The code is covered by an LGPL licence. -See +See From b6645c1a067f25394aad2235d2e3623742ee07a1 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 16 Jan 2024 10:05:16 +1100 Subject: [PATCH 63/67] docs+README: update Isabelle links to https Link to canonical https location; link checker is too impatient for the redirect. Signed-off-by: Gerwin Klein --- README.md | 4 ++-- docs/find-theorems.md | 2 +- docs/setup.md | 2 +- tools/autocorres/README.md | 2 +- tools/autocorres/tools/release_files/README | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index daa4038153..8fa990f058 100644 --- a/README.md +++ b/README.md @@ -28,8 +28,8 @@ assistant [Isabelle/HOL][2]. For an introduction to Isabelle, see its [official website][2] and [documentation][3]. [1]: https://github.com/seL4/l4v "L4.verified Repository" - [2]: http://isabelle.in.tum.de "Isabelle Website" - [3]: http://isabelle.in.tum.de/documentation.html "Isabelle Documentation" + [2]: https://isabelle.in.tum.de "Isabelle Website" + [3]: https://isabelle.in.tum.de/documentation.html "Isabelle Documentation" Setup diff --git a/docs/find-theorems.md b/docs/find-theorems.md index 0dcb829bc7..e5df394155 100644 --- a/docs/find-theorems.md +++ b/docs/find-theorems.md @@ -10,7 +10,7 @@ This command is for searching for theorems. If you are looking for a constant/function instead, look at [find_consts](find-consts.md). There is an introduction to the `find_theorems` command in the -[Isabelle/HOL tutorial](http://isabelle.in.tum.de/documentation.html). +[Isabelle/HOL tutorial](https://isabelle.in.tum.de/documentation.html). Here we cover some additional material and useful patterns. `find_theorems` can be written in the theory as a diagnostic command, or diff --git a/docs/setup.md b/docs/setup.md index 29abf3de03..8f602f22ff 100644 --- a/docs/setup.md +++ b/docs/setup.md @@ -243,4 +243,4 @@ proof-context aware than the 'original' indenter. Pressing `ctrl+i` while some subgoal depth and maintaining the relative indentation of multi-line `apply` statements. -[isabelle]: http://isabelle.in.tum.de +[isabelle]: https://isabelle.in.tum.de diff --git a/tools/autocorres/README.md b/tools/autocorres/README.md index 0df7002d52..9240587f6d 100644 --- a/tools/autocorres/README.md +++ b/tools/autocorres/README.md @@ -15,7 +15,7 @@ in [Isabelle/HOL][1]. In particular, it uses Norrish's abstracts the result to produce a result that is (hopefully) more pleasant to reason about. - [1]: https://www.cl.cam.ac.uk/research/hvg/Isabelle/ + [1]: https://isabelle.in.tum.de [2]: https://trustworthy.systems/software/TS/c-parser/ diff --git a/tools/autocorres/tools/release_files/README b/tools/autocorres/tools/release_files/README index 4e5611f891..f3f2a79b6b 100644 --- a/tools/autocorres/tools/release_files/README +++ b/tools/autocorres/tools/release_files/README @@ -7,7 +7,7 @@ in [Isabelle/HOL][1]. In particular, it uses Norrish's abstracts the result to produce a result that is (hopefully) more pleasant to reason about. - [1]: https://www.cl.cam.ac.uk/research/hvg/Isabelle/ + [1]: https://isabelle.in.tum.de/ [2]: https://trustworthy.systems/software/TS/c-parser/ From 4d8ad41f93df88a2132f831fbe81f16de3c43cbc Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 16 Jan 2024 10:11:25 +1100 Subject: [PATCH 64/67] autocorres: point C parser links to GitHub TS C parser web page has been retired. Signed-off-by: Gerwin Klein --- tools/autocorres/README.md | 2 +- tools/autocorres/doc/quickstart/Chapter1_MinMax.thy | 4 ++-- tools/autocorres/doc/quickstart/document/root.bib | 2 +- tools/autocorres/tools/release_files/README | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tools/autocorres/README.md b/tools/autocorres/README.md index 9240587f6d..e564e53413 100644 --- a/tools/autocorres/README.md +++ b/tools/autocorres/README.md @@ -16,7 +16,7 @@ abstracts the result to produce a result that is (hopefully) more pleasant to reason about. [1]: https://isabelle.in.tum.de - [2]: https://trustworthy.systems/software/TS/c-parser/ + [2]: https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md diff --git a/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy b/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy index 99aea61e16..25ad830ce8 100644 --- a/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy +++ b/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy @@ -69,8 +69,8 @@ text \ As mentioned earlier, AutoCorres does not handle C code directly. The first step is to apply the - C-Parser\footnote{\url{https://trustworthy.systems/software/TS/c-parser}} to - obtain a SIMPL translation. We do this using the \texttt{install-C-file} + C-Parser\footnote{\url{https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md}} + to obtain a SIMPL translation. We do this using the \texttt{install-C-file} command in Isabelle, as shown. \ diff --git a/tools/autocorres/doc/quickstart/document/root.bib b/tools/autocorres/doc/quickstart/document/root.bib index a1afca31e7..9450bc9518 100644 --- a/tools/autocorres/doc/quickstart/document/root.bib +++ b/tools/autocorres/doc/quickstart/document/root.bib @@ -25,7 +25,7 @@ @misc{CParser_download title = {{C-to-Isabelle} Parser, version 1.13.0}, year = 2013, month = may, - url = {https://trustworthy.systems/software/TS/c-parser/}, + url = {https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md}, note = {Accessed May 2016} } diff --git a/tools/autocorres/tools/release_files/README b/tools/autocorres/tools/release_files/README index f3f2a79b6b..45a68444ee 100644 --- a/tools/autocorres/tools/release_files/README +++ b/tools/autocorres/tools/release_files/README @@ -8,7 +8,7 @@ abstracts the result to produce a result that is (hopefully) more pleasant to reason about. [1]: https://isabelle.in.tum.de/ - [2]: https://trustworthy.systems/software/TS/c-parser/ + [2]: https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md @@ -107,7 +107,7 @@ This package contains: * Michael Norrish's C parser, used to translate C code into Isabelle: - https://trustworthy.systems/software/TS/c-parser/ + https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md * Norbert Schirmer's Simpl language and associated VCG tool. The C parser translates C into Schirmer's Simpl language: From f9359ead94c0792bc826a7764215e2b078da0f43 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 16 Jan 2024 10:14:22 +1100 Subject: [PATCH 65/67] autocorres: update AFP links The canonical URL is now .htlm (no longer .shtml) Signed-off-by: Gerwin Klein --- tools/autocorres/doc/quickstart/document/root.bib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/autocorres/doc/quickstart/document/root.bib b/tools/autocorres/doc/quickstart/document/root.bib index 9450bc9518..4457e72d2d 100644 --- a/tools/autocorres/doc/quickstart/document/root.bib +++ b/tools/autocorres/doc/quickstart/document/root.bib @@ -55,7 +55,7 @@ @article{Separation_Algebra-AFP journal = {Archive of Formal Proofs}, month = may, year = 2012, - url = {https://www.isa-afp.org/entries/Separation_Algebra.shtml}, + url = {https://www.isa-afp.org/entries/Separation_Algebra.html}, note = {Formal proof development}, ISSN = {2150-914x}, } From c84bb143626b5287da50b4fec9b93266524d4a17 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 16 Jan 2024 11:32:36 +1100 Subject: [PATCH 66/67] c-parser: turn README into main C-parser website Signed-off-by: Gerwin Klein --- tools/c-parser/README.md | 123 ++++++++++++++++++++++++++++++++++----- 1 file changed, 109 insertions(+), 14 deletions(-) diff --git a/tools/c-parser/README.md b/tools/c-parser/README.md index ca00754bde..f765baeea4 100644 --- a/tools/c-parser/README.md +++ b/tools/c-parser/README.md @@ -1,4 +1,5 @@ + +# Commit Messages + +## Objective + +The l4v repository is relatively large, active, and long-lived. It has a public +history of about one decade, and an additional decade of unreleased private +history. It will hopefully live on for another 20 years. + +This means that the commit history is important. Examples of questions the commit +history should be able to answer reasonably quickly and painlessly are: + +- > Is this written in a strange way for good reasons, or were we just in a hurry? + > What was the reason? Does it still apply? + +- > When did we change doing things this way and why? + +- > Has this always been broken or was there a seemingly unrelated change that broke it? + +- > How long did it take to finish this proof? + +- > How much change was necessary to do this proof? + +- > Where did this library lemma come from? + +## General + +The [seL4 repository guidelines][git-conventions] apply to the `l4v` repository, +with the following exceptions and additions: + +- header can be max 78 characters +- body is wrapped at 78 characters +- we use tags in the header to indicate which part of the repository + the commit applies to + +We are using 78 for the header because of the tags, which take up some space. If +you can manage to stay within 50 characters anyway, that is appreciated, but it's +not always practical. Using a body wrap of 72 is also allowed, since that is the +default for other seL4 repositories. + +We use tags, because the repository is relatively large and most commits only +apply to small parts of it. The tags make it easy to identify relevance of a +commit at a glance while scanning through a large number of commits. + +The general guidelines prescribe capitalising the commit header. We do not +capitalise the tag or after the tag, but we do capitalise the (rare) cases where +there is no tag in the commit header. + +## Header and Body + +There is good general advice on [commit message writing][commit-messages] +available on the internet and it is as relevant to proofs as it is to code. +You should read it, it's not long and it's good advice. + +Repeating some high-level points: + +- Use imperative voice (e.g. `proof: rename lemma foo to bar`) +- The header should be a short summary, focusing on "what" +- The body should explain what is going on in more detail (also in imperative + voice), but much more importantly *why* it is going on (is `bar` more + consistent than `foo`? Is the name `foo` needed for something else? Does `bar` + just better describe what is going on?). +- You are trying to explain things to your future self or a future colleague + 5-10 years from now. You can assume knowledge of the repository in general, + but you should not assume specific context that is obvious to you right now, + but that will not be known to a different person 5 years from now. + +## Tags + +- We use tags to indicate which part of the repository the commit applies to, + and if it is architecture-specific, then to which architecture it applies to. + +- We do not usually use branch tags, because git branches are ephemeral and we + are using rebase branches for most of our work. The one exception is the `rt` + branch, which has been alive for over half a decade. For this branch, we allow + merge commits (from branch `master` into `rt` only), and we want to be able to + reconstruct a rebase history from that at the end of the branch's life. + + This means, we do use the tag `rt` for commits that only make sense on this + branch. If you could apply the commit to the master branch directly (e.g. you're + adding a lemma to a library), it should not get the tag. Otherwise it should. + +### Tag Examples + +The main tags we use are mostly the directory names of the main proof something +is in, e.g. `refine`, `crefine`, `sys-init`, `camkes`. For some of these, there +are abbreviations, mainly `aspec` for the abstract spec and `ainvs` for the +abstract invariants. + +For large directories that have logical sub parts, we use slashes, e.g. +`lib/monads`. Not so much because the change is in that directory, but because +we want to see that it's a library change and applies to the monad part of the +library. + +If the change applies to many proofs, for instance large lemma renaming commits, +we use tags such as `proof` and `spec`. + +We combine tags with `+` if a change applies to multiple parts, e.g. +`clib+crefine` or `lib+proof`. + +If something is specific to an architecture we preface the tag with the +architecture, e.g. `arm refine:` or `aarch64 aspec+ainvs:`. The current +architecture tags are: `arm`, `arm-hyp`, `x64`, `riscv`, `aarch64`. +Please use these spellings only. + +More tag examples: + +- `trivial`: for small trivial changes like fixing a typo, where no proofs or + specs have changed, i.e.\ that would not need a proof CI run. +- `cleanup:` for cleanups that do not change proof content +- `github:` for GitHub CI changes +- `run_tests`: for changes to the top-level `run_tests` file +- `isabelle20xx`: for easily identifying commits related to Isabelle updates + +For more consistency there is an order between tags. More abstract/general +things should come first, e.g. `lib` < `aspec` < `haskell` < `ainvs` < `refine` +`orphanage` < `crefine`. Or `dspec` < `drefine` and `access` < `infoflow`. Specs +< proofs and `infoflow` < refinement proofs. This is not a total order, it's Ok +to use your own judgement. + +Because `lib` has many subdirectories and separate parts, it's fine to use +session names as tags there to shorten things a bit, e.g. `clib`, `monads`, +`word_lib` instead of `lib/clib`, `lib/monads`, or `lib/word_lib`. This makes +sense when the tags are session names. + +See also the longer example list of [good tags](#good-tags) below. + +## Tips and Tools + +### Looking at history + +The main tools to interact with the git history are browsing it on GitHub and +various forms of `git log`: + +```sh +git log --oneline # show only headings +git log # show commit info with author, date, message +git log --stat # additionally show which files have changed +git log --p # additionally show full diff +``` + +For all of these, you can supply a path to restrict the log to a certain file +or directory in the repo. You can also supply a branch, or a commit range like +`master..rt` to restrict the output. + +Especially `git log --oneline` is useful for quickly getting an overview. Example +output: + +``` +b3c6df48a clib: improve ccorres_While +49ff8457f clib+crefine: improve and consolidate variants of ccorres_to_vcg +8c433c085 clib: add some rules for hoarep +82b954817 clib: improve ccorres_call_getter_setter +8c59df449 lib/monads: remove more uses of _tac methods +563232397 run_tests+proof: exclude SimplExportAndRefine for AARCH64 +1cce5b3ff proof: switch AArch64 quick_and_dirty from Refine to CRefine +402a8342d run_tests: enable CBaseRefine for AARCH64 +32a672412 aarch64 cspec: add Kernel_C.thy to base CKernel image on +b2cd1ce4a aarch64 asmrefine: copy ArchSetup from RISCV64 +67c0109b7 lib/monads: avoid clarsimp as initial Isar method +bd5026438 lib/monads: fix remaining document preparation issues +4d0086567 lib/monads: add new Trace_* files to ROOT +598e19dd6 lib/monads: coherent document structure +4cbfb4ab0 lib/monads: minor style + warning cleanup +b2dd5db6d lib/monads: fix document preparation issues +03a045309 lib/monads: add AFP document setup +d0bab9c79 misc/scripts: remove Darwin cpp wrapper +``` + +You can very quickly see that C verification has been active recently, that +new tests were added, that AARCH64 refinement proofs have been done, and that there was +some work to do with the AFP and the monad library. You can see that nothing +has happened with the system initialiser or other user-level proofs, and that there +are no changes that should affect, for instance, the C parser. + +You only see such things quickly when the messages are consistent and follow the +same kind of pattern. It's not so important what the pattern is. It is important +that it is consistent. + +Note in e.g. `proof: switch AArch64 quick_and_dirty from Refine to CRefine` that +the architecture tag is used only when the change is specific to files for that +architecture. In this commit, the overall ROOTS file is changed, so it shouldn't +get the architecture tag. + +### What tag should I pick? + +If you're uncertain what tag to pick for a certain file or directory, the +easiest way to figure it out is to do + +```sh +git log --oneline +``` + +Do your tags the same way people have done before. This will make the pattern +consistent and should be reasonably easy to read even if it's not perfect. Look +at a few commits, not only a single one, so you can course correct instead of +amplify if someone happened to invent a new flavour. + +You can even do that when you're in the middle of writing a commit message, it's +safe to interrupt `git commit` with `Ctrl-Z`, then `bg` in your shell to put +it into the background, and then `git log --online ` to see the history. + +Any operation that doesn't change the state of the repository is fine (even +those that do are fine, but then the commit will probably fail). + +When you're looking into history for tags, use mainly commits from roughly 2018 +onwards. We weren't very consistent with tags before that. The more recent the +more consistent. + +### Good tags + +Here's a list of tags that have been used in the past and that follow the +guidelines above. + +``` +aarch64 ainvs +aarch64 ainvs+refine +aarch64 asmrefine +aarch64 aspec +aarch64 aspec+ainvs +aarch64 aspec+design +aarch64 aspec+haskell +aarch64 aspec+machine +aarch64 cspec +aarch64 design +aarch64 design+machine +aarch64 haskell +aarch64 haskell+design +aarch64 haskell+machine +aarch64 machine+ainvs +aarch64 proof +aarch64 refine +aarch64 spec+haskell +access+infoflow+drefine +access+infoflow+crefine+drefine +ainvs +ainvs+crefine +ainvs+refine +arm aspec+design +arm access +arm access+infoflow +arm ainvs +arm aspec +arm crefine +arm haskell +arm infoflow +arm refine +arm+arm-hyp crefine +arm+arm-hyp machine +arm-hyp aspec +arm-hyp aspec+design +arm-hyp ainvs +arm-hyp crefine +arm-hyp design +arm-hyp haskell +arm-hyp haskell+refine +arm-hyp machine +arm-hyp refine +asmrefine +aspec +aspec+access +aspec+ainvs +aspec+design+haskell +aspec+haskell +autocorres +bisim +c-parser +c-parser+autocorres +c-parser+crefine +camkes +capDL +ckernel +cleanup +cleanup ainvs +clib +clib+crefine +crefine +crefine+capDL +cspec +design +docs +dpolicy +drefine +dspec +dspec+drefine+infoflow +github +haskell +haskell+design +haskell-translator +infoflow +infoflow+crefine +infoflow+dpolicy+cdl-refine +isabelle-2021 +isabelle-2021 access +isabelle-2021 c-parser +lib +lib+READMEs +lib+aarch64 ainvs +lib+aarch64 refine +lib+ainvs +lib+ainvs+aarch64 ainvs +lib+ainvs+aarch64 refine +lib+ainvs+access+refine +lib+autocorres +lib+c-parser +lib+crefine +lib+proof +lib+proof+autocorres +lib+proof+tools +lib+proof +lib+refine+crefine +lib+spec +lib+spec+proof+autocorres +lib+spec+proof +lib+sysinit +lib+tools +lib/apply_debug +lib/clib +lib/corres_method +lib/crunch +lib/monads +lib/sep_algebra +license +misc +misc/regression +misc/scripts +misc/stats +proof +proof+autocorres +proof/Makefile +proof/ROOT +refine +refine cleanup +refine+crefine +refine+orphanage +riscv +riscv access +riscv ainvs +riscv ainvs+access +riscv aspec +riscv aspec+ainvs +riscv aspec+haskell +riscv crefine +riscv cspec+crefine +riscv design +riscv haskell +riscv haskell+design +riscv haskell+proof +riscv haskell+refine +riscv infoflow +riscv machine +riscv machine+ainvs +riscv machine+design+crefine +riscv orphanage +riscv platform +riscv refine +riscv access+infoflow+refine+crefine +riscv spec +riscv+aarch64 ainvs+refine +riscv+x64 crefine +riscv64+aarch64 ainvs +run_tests +run_tests+proof +spec+proof +style +sys-init +tools +tools/asmrefine +trivial +word_lib +word_lib+crefine +x64 ainvs+refine+crefine +x64 aspec +x64 crefine +x64 design +x64 design/skel +x64 haskell +x64 machine +x64 refine +x64 refine+crefine +``` + +Most of these could be prefixed with `rt` if they only made sense on the `rt` +branch, e.g. `rt arm ainv+refine:` + +[git-conventions]: https://docs.sel4.systems/processes/git-conventions.html +[commit-messages]: https://chris.beams.io/posts/git-commit/