diff --git a/docs/arch-split.md b/docs/arch-split.md index 39705dd083..70331aeb85 100644 --- a/docs/arch-split.md +++ b/docs/arch-split.md @@ -220,6 +220,10 @@ done for any type, constant or fact: type, constant or fact, so that the unqualified name unambiguously denotes the architecture-specific concept for the current architecture. +Note: the `requalify_*` commands will warn when the unqualified name is already +available in the global context (see: Dealing with name clashes). To suppress +this warning, pass `(aliasing)` as the first parameter. + We do this in a generic theory: - `l4v/proof/invariant-abstract/ADT_AI.thy` @@ -298,6 +302,40 @@ This disparity will only get worse as the Arch context grows bigger, and might indicate the need for some alternative functionality. +### Requalifying into the Arch locale + +The `requalify` commands support a target parameter, e.g. + +```isabelle +requalify_facts (in Arch) user_mem_dom_cong +``` + +Which prevents exporting the name into the global theory context, exporting it +under `Arch.` instead: + +```isabelle +thm user_mem_dom_cong (* ERROR *) +thm ARM.user_mem_dom_cong (* ok *) +thm Arch.user_mem_dom_cong (* ok *) +``` + +This functionality can be useful when we want to give an architecture-specific +constant/type/fact a generic name, but not mix it with generic namespace (see +also Dealing with name clashes, as this affects lookup order inside +interpretations). + +One can target any locale in this fashion, although the usefulness to arch-split +is then decreased, since short names might not be visible past a naming prefix: + +```isabelle +requalify_facts (in Some_Locale) ARM.user_mem_dom_cong + +thm user_mem_dom_cong (* ERROR *) +thm ARM.user_mem_dom_cong (* ok *) +thm Some_Locale.user_mem_dom_cong (* ok *) +``` + + ### Dealing with name clashes Things are a bit more complicated when a generic theory needs to refer to an @@ -327,7 +365,7 @@ term deriveCap (* In the Arch context, this is the deriveCap funct term RetypeDecls_H.deriveCap (* This is the arch-generic deriveCap function. *) (* The following makes Arch.deriveCap refer to the architecture-specific constant. *) -requalify_consts deriveCap +requalify_consts deriveCap (* Warning: Name "deriveCap" already exists in theory context *) (* Unfortunately, the above also means that in a context in which Arch is interpreted, `deriveCap` unqualified would refer to the arch-specific constant, which may break existing proofs. diff --git a/lib/ROOT b/lib/ROOT index 10c3726175..84a5431195 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -127,6 +127,7 @@ session LibTest (lib) in test = Refine + Named_Eta_Test Rules_Tac_Test MonadicRewrite_Test + Requalify_Test (* use virtual memory function as an example, only makes sense on ARM: *) theories [condition = "L4V_ARCH_IS_ARM"] CorresK_Test diff --git a/lib/Requalify.thy b/lib/Requalify.thy index b06fdb3719..84dffdc8b5 100644 --- a/lib/Requalify.thy +++ b/lib/Requalify.thy @@ -1,82 +1,135 @@ (* + * Copyright 2024, Proofcraft Pty Ltd * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) (* - Requalify constants, types and facts into the current naming + Requalify constants, types and facts into the current naming. + Includes command variants that support implicitly using the L4V_ARCH environment variable. + *) +text \See theory @{text "test/Requalify_Test.thy"} for commented examples and usage scenarios.\ + theory Requalify imports Main -keywords "requalify_facts" :: thy_decl and "requalify_types" :: thy_decl and "requalify_consts" :: thy_decl and - "global_naming" :: thy_decl +keywords "requalify_facts" :: thy_decl + and "requalify_types" :: thy_decl + and "requalify_consts" :: thy_decl + and "global_naming" :: thy_decl + and "arch_requalify_facts" :: thy_decl + and "arch_requalify_types" :: thy_decl + and "arch_requalify_consts" :: thy_decl + and "arch_global_naming" :: thy_decl begin ML \ local - fun all_facts_of ctxt = - let - val thy = Proof_Context.theory_of ctxt; - val global_facts = Global_Theory.facts_of thy; - in - Facts.dest_static false [] global_facts - end; + Proof_Context.theory_of ctxt + |> Global_Theory.facts_of + |> Facts.dest_static false []; + +fun tl' (_ :: xs) = xs + | tl' _ = [] + +(* Alias binding to fully-qualified name "name" in both global and local context *) +fun bind_alias global_alias_fn local_alias_fn binding (name : string) = + Local_Theory.declaration {syntax = false, pos = Position.none, pervasive = true} (fn phi => + let val binding' = Morphism.binding phi binding; + in Context.mapping (global_alias_fn binding' name) (local_alias_fn binding' name) end); + +(* Instantiate global and local aliasing functions for consts, types and facts *) +val const_alias = bind_alias Sign.const_alias Proof_Context.const_alias; +val type_alias = bind_alias Sign.type_alias Proof_Context.type_alias; +val alias_fact = bind_alias Global_Theory.alias_fact Proof_Context.alias_fact; + +(* Locate global fact matching supplied name. + When we specify a fact name that resolves to a global name, return the normal fact lookup result. + Note: Locale_Name.fact_name outside the locale resolves to a global name. + When we are inside a locale, the lookup is more interesting. Supplying "short_name" will result + in "local.short_name", which we then need to match to some name in the global context. We do + this by going through *all* the fact names in the current context, searching for matches + of the form "X.Y.short_name", where we hope X is some theory, and Y is some locale. + + Since "X.Y.short_name" is not sufficiently unique, we must also check that the theorems under + the discovered name match the ones under "local.short_name". *) fun global_fact ctxt nm = let val facts = Proof_Context.facts_of ctxt; val {name, thms, ...} = (Facts.retrieve (Context.Proof ctxt) facts (nm, Position.none)); - fun tl' (_ :: xs) = xs - | tl' _ = [] - - fun matches suf (gnm, gthms) = - let - val gsuf = Long_Name.explode gnm |> tl' |> tl' |> Long_Name.implode; - - in suf = gsuf andalso eq_list (Thm.equiv_thm (Proof_Context.theory_of ctxt)) (thms, gthms) - end + fun matches suffix (global_name, global_thms) = + suffix = (Long_Name.explode global_name |> tl' |> tl' |> Long_Name.implode) + andalso eq_list (Thm.equiv_thm (Proof_Context.theory_of ctxt)) (thms, global_thms) in - case Long_Name.dest_local name of NONE => (name, thms) | SOME suf => - (case (find_first (matches suf) (all_facts_of ctxt)) of - SOME x => x - | NONE => raise Fail ("Couldn't find global equivalent of local fact: " ^ nm)) + case Long_Name.dest_local name of + NONE => (name, thms) + | SOME suffix => + (case (find_first (matches suffix) (all_facts_of ctxt)) of + SOME x => x + | NONE => raise Fail ("Couldn't find global equivalent of local fact: " ^ nm)) end -fun syntax_alias global_alias local_alias b (name : string) = - Local_Theory.declaration {syntax = false, pos = Position.none, pervasive = true} (fn phi => - let val b' = Morphism.binding phi b - in Context.mapping (global_alias b' name) (local_alias b' name) end); +val alias = Parse.reserved "aliasing" >> K true +val alias_default = false -val alias_fact = syntax_alias Global_Theory.alias_fact Proof_Context.alias_fact; -val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias; -val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias; +(* (aliasing) only *) +val generic_options = Scan.optional (Args.parens alias >> (fn x => (x, ""))) (alias_default, "") -in - -fun gen_requalify get_proper_nm parse_nm check_nm alias = - (Parse.opt_target -- Scan.repeat1 (Parse.position (Scan.ahead parse_nm -- Parse.name)) - >> (fn (target,bs) => - Toplevel.local_theory NONE target (fn lthy => - let +(* e.g. ARM, ARM_A, ARM_H *) +val arch_suffix = ((Parse.reserved "A" || Parse.reserved "H") >> (fn s => "_" ^ s)) +fun arch_prefix suffix = getenv_strict "L4V_ARCH" ^ suffix - fun read_entry ((entry, t), pos) lthy = - let - val local_nm = get_proper_nm lthy t; - val _ = check_nm lthy (entry, (local_nm, pos)); - val b = Binding.make (Long_Name.base_name t, pos) +(* ([aliasing][,] [A|H]) in that order *) +val arch_options = + Scan.optional ( + Args.parens ( + (alias --| Parse.$$$ "," -- arch_suffix) + || (alias >> (fn x => (x, ""))) + || (arch_suffix >> (fn x => (alias_default, x))) + )) (alias_default, "") - val lthy' = lthy - |> alias b local_nm +val arch_global_opts = Scan.optional (Args.parens arch_suffix) "" - in lthy' end +in - in fold read_entry bs lthy end))) +fun gen_requalify get_proper_nm parse_nm check_parsed_nm alias_fn arch = +let + val options = if arch then arch_options else generic_options +in + (Parse.opt_target -- options -- Scan.repeat1 (Parse.position (Scan.ahead parse_nm -- Parse.name)) + >> (fn ((target, (aliasing, arch_suffix)), names) => + Toplevel.local_theory NONE target (fn lthy => + let + val global_ctxt = Proof_Context.theory_of lthy |> Proof_Context.init_global + + fun requalify_entry ((entry, orig_name), pos) lthy = + let + val name = if arch then arch_prefix arch_suffix ^ "." ^ orig_name else orig_name + val local_name = get_proper_nm lthy name; + val _ = check_parsed_nm lthy (entry, (local_name, pos)); + + (* Check whether the short (base) name is already available in theory context if no + locale target is supplied and the "aliasing" option is not supplied. + Note: currently no name collision warning when exporting into locale *) + val base_name = Long_Name.base_name name; + val global_base = try (get_proper_nm global_ctxt) (Long_Name.base_name name); + val _ = (case (global_base, target, aliasing) of + (SOME _, NONE, false) => warning ("Name \"" ^ base_name + ^ "\" already exists in theory context") + | _ => ()) + + val b = Binding.make (base_name, pos) + val lthy' = lthy |> alias_fn b local_name + in lthy' end + in fold requalify_entry names lthy end))) +end local @@ -84,142 +137,71 @@ val get_const_nm = ((fst o dest_Const) oo (Proof_Context.read_const {proper = tr val get_type_nm = ((fst o dest_Type) oo (Proof_Context.read_type_name {proper = true, strict = false})) val get_fact_nm = (fst oo global_fact) +(* For a theorem name, we want to additionally make sure that global fact names found by + global_fact are accessible in the current context. *) fun check_fact lthy (_, (nm, pos)) = Proof_Context.get_fact lthy (Facts.Named ((nm,pos), NONE)) in val _ = Outer_Syntax.command @{command_keyword requalify_consts} "alias const with current naming" - (gen_requalify get_const_nm Parse.const (fn lthy => fn (e, _) => get_const_nm lthy e) const_alias) + (gen_requalify get_const_nm Parse.const (fn lthy => fn (e, _) => get_const_nm lthy e) const_alias + false) val _ = Outer_Syntax.command @{command_keyword requalify_types} "alias type with current naming" - (gen_requalify get_type_nm Parse.typ (fn lthy => fn (e, _) => get_type_nm lthy e) type_alias) + (gen_requalify get_type_nm Parse.typ (fn lthy => fn (e, _) => get_type_nm lthy e) type_alias + false) val _ = Outer_Syntax.command @{command_keyword requalify_facts} "alias fact with current naming" - (gen_requalify get_fact_nm Parse.thm check_fact alias_fact) + (gen_requalify get_fact_nm Parse.thm check_fact alias_fact false) val _ = Outer_Syntax.command @{command_keyword global_naming} "change global naming of context block" (Parse.binding >> (fn naming => Toplevel.local_theory NONE NONE - (Local_Theory.map_background_naming (Name_Space.parent_path #> Name_Space.qualified_path true naming)))) - -end - -end -\ - -(*Tests and examples *) - -locale Requalify_Locale -begin - -typedecl requalify_type - -definition "requalify_const == (undefined :: requalify_type)" - - -end - -typedecl requalify_type -definition "requalify_const == (undefined :: requalify_type)" - -context Requalify_Locale begin global_naming Requalify_Locale2 - -requalify_consts requalify_const -requalify_types requalify_type -requalify_facts requalify_const_def - -end - -term "requalify_const :: requalify_type" -term "Requalify_Locale2.requalify_const :: Requalify_Locale2.requalify_type" -lemma "Requalify_Locale2.requalify_const = (undefined :: Requalify_Locale2.requalify_type)" - by (simp add: Requalify_Locale2.requalify_const_def) - -consts requalify_test_f :: "'a \ 'b \ bool" - -lemma - assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" - and f2: "requalify_test_f Requalify_Locale2.requalify_const Requalify.requalify_const" - shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" - apply (rule f1)? - apply (rule f2) - apply (simp add: requalify_const_def) - done - -context Requalify_Locale begin - -lemma - assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" - and f2: "requalify_test_f Requalify_Locale2.requalify_const Requalify.requalify_const" - shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" - apply (rule f2)? - apply (rule f1) - apply (simp add: requalify_const_def) - done - -end - -context Requalify_Locale begin global_naming global - -requalify_consts Requalify.requalify_const -requalify_types Requalify.requalify_type -requalify_facts Requalify.requalify_const_def - -end - -context Requalify_Locale begin - -lemma - assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" - and f2: "requalify_test_f Requalify_Locale2.requalify_const global.requalify_const" - shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" - apply (rule f1)? - apply (rule f2) - apply (simp add: requalify_const_def) - done -end - -context begin interpretation Requalify_Locale . + (Local_Theory.map_background_naming (Name_Space.parent_path + #> Name_Space.qualified_path true naming)))) -lemma - assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" - and f2: "requalify_test_f Requalify_Locale2.requalify_const global.requalify_const" - shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" - apply (rule f1)? - apply (rule f2) - apply (simp add: requalify_const_def) - done -end +(* Arch variants use the L4V_ARCH variable and an additional A/H option, so that when L4V_ARCH=ARM + "arch_requalify_consts (H) const" becomes "requalify_consts ARM_H.const" + This allows them to be used in a architecture-generic theory. -locale Requalify_Locale3 -begin + For consts and types, we don't perform extra checking on the results of Parse.const and Parse.typ + because their "strings" contain embedded syntax, which means prepending a normal string to them + causes malformed syntax and YXML exceptions. It shouldn't matter, we are looking up the name and + checking it's a constant/type anyway. *) -typedecl requalify_type2 -definition "requalify_const2 == (undefined :: requalify_type2)" +val _ = + Outer_Syntax.command @{command_keyword arch_requalify_consts} + "alias const with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" + (gen_requalify get_const_nm Parse.const (fn _ => fn (_, _) => ()) const_alias + true) -end +val _ = + Outer_Syntax.command @{command_keyword arch_requalify_types} + "alias type with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" + (gen_requalify get_type_nm Parse.typ (fn _ => fn (_, _) => ()) type_alias + true) -context begin interpretation Requalify_Locale3 . +val _ = + Outer_Syntax.command @{command_keyword arch_requalify_facts} + "alias fact with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" + (gen_requalify get_fact_nm Parse.thm check_fact alias_fact true) -requalify_consts requalify_const2 -requalify_types requalify_type2 -requalify_facts requalify_const2_def +val _ = + Outer_Syntax.command @{command_keyword arch_global_naming} + "change global naming of context block to \"($L4V_ARCH)_[A|H]\" using env. variable" + (arch_global_opts >> (fn arch_suffix => + Toplevel.local_theory NONE NONE + (Local_Theory.map_background_naming + (Name_Space.parent_path + #> Name_Space.qualified_path true (Binding.make (arch_prefix arch_suffix, @{here})))))) end -lemma "(requalify_const2 :: requalify_type2) = undefined" - by (simp add: requalify_const2_def) - -context Requalify_Locale3 begin - -lemma "(requalify_const2 :: requalify_type2) = undefined" - by (simp add: requalify_const2_def) - end - +\ end diff --git a/lib/test/Requalify_Test.thy b/lib/test/Requalify_Test.thy new file mode 100644 index 0000000000..009eea83da --- /dev/null +++ b/lib/test/Requalify_Test.thy @@ -0,0 +1,382 @@ +(* + * Copyright 2024, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Requalify_Test +imports Lib.Requalify +begin + +section \Tests and examples for requalify commands\ + +subsection \Generic\ + +subsubsection \Exporting types, constants and facts from a locale into the theory context\ + +locale Requalify_Example1 + +context Requalify_Example1 begin +typedecl ex1_type +definition "ex1_const \ undefined :: ex1_type" +end + +(* these will all generate errors: +typ ex1_type +term "ex1_const :: ex1_type" +thm ex1_const_def +*) + +typ Requalify_Example1.ex1_type +term "Requalify_Example1.ex1_const :: Requalify_Example1.ex1_type" +thm Requalify_Example1.ex1_const_def + +(* exporting will make types/consts/facts available *) + +requalify_types Requalify_Example1.ex1_type +typ ex1_type + +requalify_consts Requalify_Example1.ex1_const +term "ex1_const :: ex1_type" + +requalify_facts Requalify_Example1.ex1_const_def +thm ex1_const_def + +(* trying to export into theory context that already has that name will result in warnings *) +requalify_types Requalify_Example1.ex1_type +requalify_consts Requalify_Example1.ex1_const +requalify_facts Requalify_Example1.ex1_const_def + +(* warnings can be suppressed if naming collision is on purpose, but see caveats in next sections *) +requalify_types (aliasing) Requalify_Example1.ex1_type +requalify_consts (aliasing) Requalify_Example1.ex1_const +requalify_facts (aliasing) Requalify_Example1.ex1_const_def + +(* requalification can also occur via interpretation, using internal names, but this is slower *) +context begin interpretation Requalify_Example1 . +requalify_types ex1_type +requalify_consts ex1_const +requalify_facts ex1_const_def +end + + +subsubsection \Exporting types, constants and facts from a locale into a locale context\ + +locale Requalify_Example2 + +(* the target of the export can be a locale (this mode cannot be used from an interpretation) *) + +requalify_types (in Requalify_Example2) Requalify_Example1.ex1_type +requalify_consts (in Requalify_Example2) Requalify_Example1.ex1_const +requalify_facts (in Requalify_Example2) Requalify_Example1.ex1_const_def + +(* this is equivalent to doing the requalifications in the original locale context *) +context Requalify_Example1 begin +requalify_types (in Requalify_Example2) ex1_type +requalify_consts (in Requalify_Example2) ex1_const +requalify_facts (in Requalify_Example2) ex1_const_def +end + +typ Requalify_Example2.ex1_type +term "Requalify_Example2.ex1_const :: Requalify_Example2.ex1_type" +thm Requalify_Example2.ex1_const_def + +(* unfortunately, there is currently no warning on name collisions into locales *) +requalify_types (in Requalify_Example2) Requalify_Example1.ex1_type (* no warning *) +requalify_consts (in Requalify_Example2) Requalify_Example1.ex1_const (* no warning *) +requalify_facts (in Requalify_Example2) Requalify_Example1.ex1_const_def (* no warning *) + + +subsubsection \Using global naming to ensure a name prefix within a locale\ + +locale Requalify_Example_G + +context Requalify_Example_G begin global_naming EXAMPLE1 +typedecl ex_g_type +definition "ex_g_const \ undefined :: ex_g_type" +end + +(* note the prefixed names in the global context *) +typ EXAMPLE1.ex_g_type +term "EXAMPLE1.ex_g_const :: EXAMPLE1.ex_g_type" +thm EXAMPLE1.ex_g_const_def + +(* the locale names will not work, these will all generate errors: +typ Requalify_Example_G.ex_g_type +term "Requalify_Example_G.ex_g_const :: Requalify_Example_G.ex_g_type" +thm Requalify_Example_G.ex_g_const_def +*) + +(* Looking up the local unprefixed name inside the locale will work as expected *) +context Requalify_Example_G begin +thm ex_g_const_def +end + +(* using the new name, we can export as usual: *) +requalify_types EXAMPLE1.ex_g_type +requalify_consts EXAMPLE1.ex_g_const +requalify_facts EXAMPLE1.ex_g_const_def + +(* inside a locale interpretation, the names can be accessed without a prefix *) +context begin interpretation Requalify_Example_G . +requalify_types ex_g_type +requalify_consts ex_g_const +requalify_facts ex_g_const_def +end + +(* We can also re-export the name to the same locale in order to make an un-prefixed alias *) +requalify_types (in Requalify_Example_G) EXAMPLE1.ex_g_type +requalify_consts (in Requalify_Example_G) EXAMPLE1.ex_g_const +requalify_facts (in Requalify_Example_G) EXAMPLE1.ex_g_const_def + +(* This makes the names available via the locale name as well *) +typ Requalify_Example_G.ex_g_type +term "Requalify_Example_G.ex_g_const :: Requalify_Example_G.ex_g_type" +thm Requalify_Example_G.ex_g_const_def + + +subsubsection \Managing collisions and global naming\ + +(* In previous sections we generated collisions by repeatedly exporting the same thing. + Generally, exporting the same name from a locale into the global context is not advised, + as it will only cause confusion. + + However, a more realistic example is when global_naming is involved. Let's say we have a + Arch locale that's supposed to hide some architecture-specific details, and a name + prefix of BOARD for a specific architecture. It makes more sense with constants and types, + but those are harder to tell apart in a demo. +*) + +lemma requalify_collision: + "False = False" + by simp + +locale Arch + +context Arch begin global_naming BOARD +lemma requalify_collision: + "True = True" + by simp +end + +(* If we access the name, we get what we expect: *) +thm requalify_collision (* False = False *) + +(* Exporting requalify_collision to the theory context would now be ill-advised, as it would + make the global name inconvenient to access. What makes more sense is to export it such + that we can access the architecture specific name under Fake_Arch (and not talk about the + specific board), while maintaining access to the global name. Let's try: *) + +requalify_facts (in Arch) BOARD.requalify_collision + +(* global context: good *) +thm requalify_collision (* False = False *) +thm Arch.requalify_collision (* True = True *) + +(* context post-interpretation: we don't have convenient access to the global name anymore *) +context begin interpretation Arch . +thm requalify_collision (* True = True *) +thm Arch.requalify_collision (* True = True *) +end + +(* This is because whatever name was last interpreted takes precedence. If we want to fix this, we + need to re-export the global name *from* the Fake_Arch locale. + By convention we also give it a "global." prefix: *) +context Arch begin + context begin global_naming global + requalify_facts (aliasing) Requalify_Test.requalify_collision + end +end + +(* After this convolution, the names are now consistently available: *) + +(* globally *) +thm requalify_collision (* False = False *) +thm global.requalify_collision (* False = False *) +thm Arch.requalify_collision (* True = True *) + +(* when interpreted *) +context begin interpretation Arch . +thm requalify_collision (* False = False *) +thm global.requalify_collision (* False = False *) +thm Arch.requalify_collision (* True = True *) +end + +(* and in the locale context *) +context Arch begin +thm requalify_collision (* False = False *) +thm global.requalify_collision (* False = False *) +thm Arch.requalify_collision (* True = True *) +end + + +subsection \Architecture-specific (requires L4V_ARCH environment variable set to work)\ + +(* The above documentation and examples attempted to be somewhat generic. In the seL4 verification + repository, we have a specific setup: + + * A number of architectures (e.g. ARM, ARM_HYP, RISCV64, X64, AARCH64) parametrised by the + L4V_ARCH environment variable. + * An Arch locale for containing architecture-specific definitions, types and proofs, wherein + global naming wraps the architecture as follows: + * ($L4V_ARCH)_A for the Abstract spec (e.g. ARM_A) + * ($L4V_ARCH)_H for the Haskell spec (e.g. ARM_H) + * as per L4V_ARCH for everything else (e.g. ARM) (though other namespaces may appear in future) + + The arch_requalify and arch_global_naming variants lean on this, by being able to generically + say something about a requirement each specific architecture needs to fulfill. +*) + +context Arch begin + arch_global_naming (* equivalent to "global_naming ARM" on ARM *) + typedecl arch_specific_type + definition "arch_specific_const \ undefined :: arch_specific_type" + lemma arch_specific_lemma: "arch_specific_const = arch_specific_const" by simp + + arch_global_naming (A) (* equivalent to "global_naming ARM_A" on ARM *) + definition "arch_specific_const_a \ undefined :: arch_specific_type" + + arch_global_naming (H) (* equivalent to "global_naming ARM_A" on ARM *) + definition "arch_specific_const_h \ undefined :: arch_specific_type" +end + +(* confirm these are the ARM, ARM_A, and ARM_H prefixes respectively: *) +find_theorems name:arch_specific_const + +(* we requalify these prefixed constants without knowing what arch we are on: *) +arch_requalify_types arch_specific_type +arch_requalify_consts arch_specific_const +arch_requalify_facts arch_specific_lemma +arch_requalify_consts (A) arch_specific_const_a +arch_requalify_consts (H) arch_specific_const_h +arch_requalify_consts (H) arch_specific_const_h (* warnings work as usual *) +arch_requalify_consts (aliasing, H) arch_specific_const_h (* warnings suppression *) + +(* this has placed all names into the global context *) +typ arch_specific_type +thm arch_specific_lemma +term "arch_specific_const :: arch_specific_type" +term "arch_specific_const_a :: arch_specific_type" +term "arch_specific_const_h :: arch_specific_type" + +(* If we wish to create a generic name that does not compete with a global name, we need to export + into the Arch locale, then fix up the interpretation order of any collisions as described in + "Managing collisions and global naming" *) +arch_requalify_consts (in Arch) (A) arch_specific_const_a + +(* this now works *) +term Arch.arch_specific_const_a + + +section "Misc tests / usage examples" + +locale Requalify_Locale +begin + +typedecl requalify_type + +definition "requalify_const == (undefined :: requalify_type)" + + +end + +typedecl requalify_type +definition "requalify_const == (undefined :: requalify_type)" + +context Requalify_Locale begin global_naming Requalify_Locale2 + +requalify_consts requalify_const +requalify_types requalify_type +requalify_facts requalify_const_def + +end + +term "requalify_const :: requalify_type" +term "Requalify_Locale2.requalify_const :: Requalify_Locale2.requalify_type" +lemma "Requalify_Locale2.requalify_const = (undefined :: Requalify_Locale2.requalify_type)" + by (simp add: Requalify_Locale2.requalify_const_def) + +consts requalify_test_f :: "'a \ 'b \ bool" + +lemma + assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" + and f2: "requalify_test_f Requalify_Locale2.requalify_const Requalify_Test.requalify_const" + shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" + apply (rule f1)? + apply (rule f2) + apply (simp add: requalify_const_def) + done + +context Requalify_Locale begin + +lemma + assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" + and f2: "requalify_test_f Requalify_Locale2.requalify_const Requalify_Test.requalify_const" + shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" + apply (rule f2)? + apply (rule f1) + apply (simp add: requalify_const_def) + done + +end + +context Requalify_Locale begin global_naming global + +requalify_consts Requalify_Test.requalify_const +requalify_types Requalify_Test.requalify_type +requalify_facts Requalify_Test.requalify_const_def + +end + +context Requalify_Locale begin + +lemma + assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" + and f2: "requalify_test_f Requalify_Locale2.requalify_const global.requalify_const" + shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" + apply (rule f1)? + apply (rule f2) + apply (simp add: requalify_const_def) + done +end + +context begin interpretation Requalify_Locale . + +lemma + assumes f1: "requalify_test_f requalify_const Requalify_Locale2.requalify_const" + and f2: "requalify_test_f Requalify_Locale2.requalify_const global.requalify_const" + shows "requalify_test_f Requalify_Locale2.requalify_const requalify_const" "requalify_const = undefined" + apply (rule f1)? + apply (rule f2) + apply (simp add: requalify_const_def) + done +end + +locale Requalify_Locale3 +begin + +typedecl requalify_type2 +definition "requalify_const2 == (undefined :: requalify_type2)" + +end + +context begin interpretation Requalify_Locale3 . + +requalify_consts requalify_const2 +requalify_types requalify_type2 +requalify_facts requalify_const2_def + +end + +lemma "(requalify_const2 :: requalify_type2) = undefined" + by (simp add: requalify_const2_def) + +context Requalify_Locale3 begin + +lemma "(requalify_const2 :: requalify_type2) = undefined" + by (simp add: requalify_const2_def) + +end + +end diff --git a/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy b/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy index 5f77c0be35..5dce18b02c 100644 --- a/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy +++ b/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy @@ -82,7 +82,7 @@ lemma device_frame_in_device_region: by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def) global_naming Arch -named_theorems AInvsPre_asms +named_theorems AInvsPre_assms lemma get_vspace_of_thread_asid_or_global_pt: "(\asid. vspace_for_asid asid s = Some (get_vspace_of_thread (kheap s) (arch_state s) t)) @@ -102,7 +102,7 @@ lemma get_page_info_gpd_kmaps: table_base_pt_slot_offset[where level=max_pt_level, simplified]) done -lemma ptable_rights_imp_frame[AInvsPre_asms]: +lemma ptable_rights_imp_frame[AInvsPre_assms]: assumes "valid_state s" shows "\ ptable_rights t s vptr \ {}; ptable_lift t s vptr = Some (addrFromPPtr p) \ \ in_user_frame p s \ in_device_frame p s" @@ -140,7 +140,7 @@ end interpretation AInvsPre?: AInvsPre proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?) qed requalify_facts diff --git a/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy index f448888f1d..d00dbc5846 100644 --- a/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy @@ -11,16 +11,16 @@ begin context Arch begin global_naming AARCH64 -named_theorems Detype_AI_asms +named_theorems Detype_AI_assms -lemma valid_globals_irq_node[Detype_AI_asms]: +lemma valid_globals_irq_node[Detype_AI_assms]: "\ valid_global_refs s; cte_wp_at ((=) cap) ptr s \ \ interrupt_irq_node s irq \ cap_range cap" apply (erule(1) valid_global_refsD) apply (simp add: global_refs_def) done -lemma caps_of_state_ko[Detype_AI_asms]: +lemma caps_of_state_ko[Detype_AI_assms]: "valid_cap cap s \ is_untyped_cap cap \ cap_range cap = {} \ @@ -34,7 +34,7 @@ lemma caps_of_state_ko[Detype_AI_asms]: split: option.splits if_splits)+ done -lemma mapM_x_storeWord[Detype_AI_asms]: +lemma mapM_x_storeWord[Detype_AI_assms]: (* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *) assumes al: "is_aligned ptr word_size_bits" shows "mapM_x (\x. storeWord (ptr + of_nat x * word_size) 0) [0..x. if x \ S then {} else state_hyp_refs_of s x)" by (rule ext, simp add: state_hyp_refs_of_def detype_def) -lemma valid_ioports_detype[Detype_AI_asms]: +lemma valid_ioports_detype[Detype_AI_assms]: "valid_ioports s \ valid_ioports (detype (untyped_range cap) s)" by simp @@ -118,7 +118,7 @@ interpretation Detype_AI?: Detype_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Detype_AI_asms)?) + by (intro_locales; (unfold_locales; fact Detype_AI_assms)?) qed context detype_locale_arch begin diff --git a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy index 91241010b0..1390c0a215 100644 --- a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy @@ -11,7 +11,7 @@ begin context Arch begin -named_theorems Finalise_AI_asms +named_theorems Finalise_AI_assms global_naming AARCH64 @@ -221,17 +221,17 @@ lemma unmap_page_tcb_cap_valid: global_naming Arch -lemma (* replaceable_cdt_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_cdt_update *)[simp,Finalise_AI_assms]: "replaceable (cdt_update f s) = replaceable s" by (fastforce simp: replaceable_def tcb_cap_valid_def reachable_frame_cap_def reachable_target_def) -lemma (* replaceable_revokable_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_revokable_update *)[simp,Finalise_AI_assms]: "replaceable (is_original_cap_update f s) = replaceable s" by (fastforce simp: replaceable_def is_final_cap'_def2 tcb_cap_valid_def reachable_frame_cap_def reachable_target_def) -lemma (* replaceable_more_update *) [simp,Finalise_AI_asms]: +lemma (* replaceable_more_update *) [simp,Finalise_AI_assms]: "replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'" by (simp add: replaceable_def reachable_frame_cap_def reachable_target_def) @@ -243,9 +243,9 @@ lemma reachable_frame_cap_trans_state[simp]: "reachable_frame_cap cap (trans_state f s) = reachable_frame_cap cap s" by (simp add: reachable_frame_cap_def) -lemmas [Finalise_AI_asms] = obj_refs_obj_ref_of (* used under name obj_ref_ofI *) +lemmas [Finalise_AI_assms] = obj_refs_obj_ref_of (* used under name obj_ref_ofI *) -lemma (* empty_slot_invs *) [Finalise_AI_asms]: +lemma (* empty_slot_invs *) [Finalise_AI_assms]: "\\s. invs s \ cte_wp_at (replaceable s sl cap.NullCap) sl s \ emptyable sl s \ (info \ NullCap \ post_cap_delete_pre info ((caps_of_state s) (sl \ NullCap)))\ @@ -325,7 +325,7 @@ lemma (* empty_slot_invs *) [Finalise_AI_asms]: apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state) by fastforce -lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: +lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_assms]: "dom tcb_cap_cases = {xs. length xs = 3 \ unat (of_bl xs :: machine_word) < 5}" apply (rule set_eqI, rule iffI) apply clarsimp @@ -335,7 +335,7 @@ lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: apply (clarsimp simp: nat_to_cref_unat_of_bl') done -lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]: +lemma (* unbind_notification_final *) [wp,Finalise_AI_assms]: "\is_final_cap' cap\ unbind_notification t \ \rv. is_final_cap' cap\" unfolding unbind_notification_def apply (wp final_cap_lift thread_set_caps_of_state_trivial hoare_drop_imps @@ -364,7 +364,7 @@ crunch prepare_thread_delete for caps_of_state[wp]: "\s. P (caps_of_state s)" (wp: crunch_wps ignore: do_machine_op) -declare prepare_thread_delete_caps_of_state [Finalise_AI_asms] +declare prepare_thread_delete_caps_of_state [Finalise_AI_assms] lemma dissociate_vcpu_tcb_final_cap[wp]: "\is_final_cap' cap\ dissociate_vcpu_tcb v t \\rv. is_final_cap' cap\" @@ -378,7 +378,7 @@ lemma length_and_unat_of_bl_length: "(length xs = x \ unat (of_bl xs :: 'a::len word) < 2 ^ x) = (length xs = x)" by (auto simp: unat_of_bl_length) -lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: +lemma (* finalise_cap_cases1 *)[Finalise_AI_assms]: "\\s. final \ is_final_cap' cap s \ cte_wp_at ((=) cap) slot s\ finalise_cap cap final @@ -417,12 +417,12 @@ crunch dissociate_vcpu_tcb ignore: do_machine_op set_object) crunch arch_finalise_cap - for typ_at[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" (wp: crunch_wps simp: crunch_simps unless_def assertE_def ignore: maskInterrupt set_object) crunch prepare_thread_delete - for typ_at[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" crunch arch_thread_set for tcb_at[wp]: "\s. tcb_at p s" @@ -441,7 +441,7 @@ crunch dissociate_vcpu_tcb crunch prepare_thread_delete for tcb_at[wp]: "\s. tcb_at p s" -lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]: +lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_assms]: "\valid_cap cap\ finalise_cap cap x \\rv. valid_cap (fst rv)\" apply (cases cap; simp) apply (wp suspend_valid_cap prepare_thread_delete_typ_at @@ -1080,7 +1080,7 @@ crunch vcpu_finalise for invs[wp]: invs (ignore: dissociate_vcpu_tcb) -lemma arch_finalise_cap_invs' [wp,Finalise_AI_asms]: +lemma arch_finalise_cap_invs' [wp,Finalise_AI_assms]: "\invs and valid_cap (ArchObjectCap cap)\ arch_finalise_cap cap final \\rv. invs\" @@ -1140,14 +1140,14 @@ lemma arch_finalise_cap_vcpu: apply (wpsimp wp: wps simp: simps reachable_frame_cap_def | strengthen strg)+ done -lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_asms]: +lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r \ \ typ_at (AArch AVCPU) r s) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: live_def valid_cap_def valid_arch_cap_ref_def obj_at_def a_type_arch_live valid_cap_simps hyp_live_def arch_live_def split: arch_cap.split_asm if_splits) -lemma obj_at_not_live_valid_arch_cap_strg' [Finalise_AI_asms]: +lemma obj_at_not_live_valid_arch_cap_strg' [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r \ cap \ VCPUCap r) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: live_def valid_cap_def valid_arch_cap_ref_def obj_at_def @@ -1403,7 +1403,7 @@ lemma arch_finalise_cap_replaceable: done global_naming Arch -lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_assms]: "\if_unsafe_then_cap and valid_global_refs and cte_wp_at (\cp. cap_irqs cp \ {}) sl\ deleting_irq_handler irq @@ -1424,7 +1424,7 @@ lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: apply (clarsimp simp: appropriate_cte_cap_def split: cap.split_asm) done -lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_assms]: "\ cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap \ \ no_cap_to_obj_with_diff_ref cap' {p} s" @@ -1446,7 +1446,7 @@ lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: gen_obj_refs_Int) done -lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]: +lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_assms]: "\no_cap_to_obj_with_diff_ref cap S\ suspend t \\rv. no_cap_to_obj_with_diff_ref cap S\" @@ -1490,7 +1490,7 @@ lemma prepare_thread_delete_unlive[wp]: apply (clarsimp simp: obj_at_def, case_tac ko, simp_all add: is_tcb_def live_def) done -lemma finalise_cap_replaceable [Finalise_AI_asms]: +lemma finalise_cap_replaceable [Finalise_AI_assms]: "\\s. s \ cap \ x = is_final_cap' cap s \ valid_mdb s \ cte_wp_at ((=) cap) sl s \ valid_objs s \ sym_refs (state_refs_of s) \ (cap_irqs cap \ {} \ if_unsafe_then_cap s \ valid_global_refs s) @@ -1542,7 +1542,7 @@ lemma finalise_cap_replaceable [Finalise_AI_asms]: | simp add: valid_cap_simps is_nondevice_page_cap_simps)+)) done -lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_assms]: assumes x: "\cap. P cap \ \ can_fast_finalise cap" shows "\cte_wp_at P p\ deleting_irq_handler irq \\rv. cte_wp_at P p\" apply (simp add: deleting_irq_handler_def) @@ -1561,15 +1561,15 @@ lemma arch_thread_set_cte_wp_at[wp]: done crunch dissociate_vcpu_tcb - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set) crunch prepare_thread_delete - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set) crunch arch_finalise_cap - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set) end @@ -1578,7 +1578,7 @@ interpretation Finalise_AI_1?: Finalise_AI_1 proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming AARCH64 @@ -1603,7 +1603,7 @@ lemma fast_finalise_replaceable[wp]: done global_naming Arch -lemma (* cap_delete_one_invs *) [Finalise_AI_asms,wp]: +lemma (* cap_delete_one_invs *) [Finalise_AI_assms,wp]: "\invs and emptyable ptr\ cap_delete_one ptr \\rv. invs\" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (rule hoare_pre) @@ -1617,7 +1617,7 @@ end interpretation Finalise_AI_2?: Finalise_AI_2 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming AARCH64 @@ -1629,7 +1629,7 @@ crunch (wp: crunch_wps subset_refl) crunch prepare_thread_delete - for irq_node[Finalise_AI_asms,wp]: "\s. P (interrupt_irq_node s)" + for irq_node[Finalise_AI_assms,wp]: "\s. P (interrupt_irq_node s)" (wp: crunch_wps simp: crunch_simps) crunch arch_finalise_cap @@ -1780,7 +1780,7 @@ crunch prepare_thread_delete for invs[wp]: invs (ignore: set_object do_machine_op wp: dmo_invs_lift) -lemma (* finalise_cap_invs *)[Finalise_AI_asms]: +lemma (* finalise_cap_invs *)[Finalise_AI_assms]: shows "\invs and cte_wp_at ((=) cap) slot\ finalise_cap cap x \\rv. invs\" apply (cases cap, simp_all split del: if_split) apply (wp cancel_all_ipc_invs cancel_all_signals_invs unbind_notification_invs @@ -1797,14 +1797,14 @@ lemma (* finalise_cap_invs *)[Finalise_AI_asms]: apply (auto dest: cte_wp_at_valid_objs_valid_cap) done -lemma (* finalise_cap_irq_node *)[Finalise_AI_asms]: +lemma (* finalise_cap_irq_node *)[Finalise_AI_assms]: "\\s. P (interrupt_irq_node s)\ finalise_cap a b \\_ s. P (interrupt_irq_node s)\" by (case_tac a, wpsimp+) -lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_asms] +lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_assms] = hoare_use_eq_irq_node [OF arch_finalise_cap_irq_node arch_finalise_cap_cte_wp_at] -lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: +lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_assms]: "\st_tcb_at P t and K (\st. simple st \ P st)\ deleting_irq_handler irq \\rv. st_tcb_at P t\" @@ -1813,11 +1813,11 @@ lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: apply simp done -lemma irq_node_global_refs_ARCH [Finalise_AI_asms]: +lemma irq_node_global_refs_ARCH [Finalise_AI_assms]: "interrupt_irq_node s irq \ global_refs s" by (simp add: global_refs_def) -lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: +lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_assms]: "\invs\ get_irq_slot irq \cte_wp_at can_fast_finalise\" apply (simp add: get_irq_slot_def) apply wp @@ -1839,12 +1839,12 @@ lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: apply (clarsimp simp: cap_range_def) done -lemma (* replaceable_or_arch_update_same *) [Finalise_AI_asms]: +lemma (* replaceable_or_arch_update_same *) [Finalise_AI_assms]: "replaceable_or_arch_update s slot cap cap" by (clarsimp simp: replaceable_or_arch_update_def replaceable_def is_arch_update_def is_cap_simps) -lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: +lemma (* replace_cap_invs_arch_update *)[Finalise_AI_assms]: "\\s. cte_wp_at (replaceable_or_arch_update s p cap) p s \ invs s \ cap \ cap.NullCap @@ -1869,7 +1869,7 @@ lemma dmo_pred_tcb_at[wp]: apply (clarsimp simp: pred_tcb_at_def obj_at_def) done -lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: +lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_assms]: "do_machine_op mop \\s. P (tcb_cap_valid cap ptr s)\" apply (simp add: tcb_cap_valid_def no_cap_to_obj_with_diff_ref_def) apply (wp_pre, wps, rule hoare_vcg_prop) @@ -1887,7 +1887,7 @@ lemma dmo_reachable_target[wp]: apply simp done -lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_asms,wp]: +lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_assms,wp]: "\\s. replaceable_or_arch_update s slot cap cap'\ do_machine_op mo \\r s. replaceable_or_arch_update s slot cap cap'\" @@ -1909,7 +1909,7 @@ interpretation Finalise_AI_3?: Finalise_AI_3 proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming AARCH64 @@ -1927,7 +1927,7 @@ interpretation Finalise_AI_4?: Finalise_AI_4 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming AARCH64 @@ -1967,9 +1967,9 @@ lemma arch_finalise_cap_valid_cap[wp]: global_naming Arch -lemmas clearMemory_invs[wp,Finalise_AI_asms] = clearMemory_invs +lemmas clearMemory_invs[wp,Finalise_AI_assms] = clearMemory_invs -lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: +lemma valid_idle_has_null_cap_ARCH[Finalise_AI_assms]: "\ if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; caps_of_state s (idle_thread s, v) = Some cap \ \ cap = NullCap" @@ -1985,7 +1985,7 @@ lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: apply (drule_tac x=word in spec, simp) done -lemma (* zombie_cap_two_nonidles *)[Finalise_AI_asms]: +lemma (* zombie_cap_two_nonidles *)[Finalise_AI_assms]: "\ caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s \ \ fst ptr \ idle_thread s \ ptr' \ idle_thread s" apply (frule valid_global_refsD2, clarsimp+) @@ -2011,7 +2011,7 @@ interpretation Finalise_AI_5?: Finalise_AI_5 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed end diff --git a/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy b/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy index 4ef745e647..7a880be79a 100644 --- a/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy @@ -24,16 +24,16 @@ primrec arch_irq_control_inv_valid_real :: defs arch_irq_control_inv_valid_def: "arch_irq_control_inv_valid \ arch_irq_control_inv_valid_real" -named_theorems Interrupt_AI_asms +named_theorems Interrupt_AI_assms -lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]: +lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_assms]: "\P\ decode_irq_control_invocation label args slot caps \\rv. P\" apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def arch_decode_irq_control_invocation_def whenE_def, safe) apply (wp | simp)+ done -lemma decode_irq_control_valid [Interrupt_AI_asms]: +lemma decode_irq_control_valid [Interrupt_AI_assms]: "\\s. invs s \ (\cap \ set caps. s \ cap) \ (\cap \ set caps. is_cnode_cap cap \ (\r \ cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) @@ -51,7 +51,7 @@ lemma decode_irq_control_valid [Interrupt_AI_asms]: apply (intro conjI impI; clarsimp) done -lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: +lemma get_irq_slot_different_ARCH[Interrupt_AI_assms]: "\\s. valid_global_refs s \ ex_cte_cap_wp_to is_cnode_cap ptr s\ get_irq_slot irq \\rv s. rv \ ptr\" @@ -63,7 +63,7 @@ lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def) done -lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: +lemma is_derived_use_interrupt_ARCH[Interrupt_AI_assms]: "(is_ntfn_cap cap \ interrupt_derived cap cap') \ (is_derived m p cap cap')" apply (clarsimp simp: is_cap_simps) apply (clarsimp simp: interrupt_derived_def is_derived_def) @@ -71,7 +71,7 @@ lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def) done -lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]: +lemma maskInterrupt_invs_ARCH[Interrupt_AI_assms]: "\invs and (\s. \b \ interrupt_states s irq \ IRQInactive)\ do_machine_op (maskInterrupt b irq) \\rv. invs\" @@ -91,13 +91,13 @@ lemma dmo_plic_complete_claim[wp]: apply (auto simp: plic_complete_claim_def machine_op_lift_def machine_rest_lift_def in_monad select_f_def) done -lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]: +lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_assms]: "no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \" by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state obj_ref_none_no_asid) -lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: +lemma (* set_irq_state_valid_cap *)[Interrupt_AI_assms]: "\valid_cap cap\ set_irq_state IRQSignal irq \\rv. valid_cap cap\" apply (clarsimp simp: set_irq_state_def) apply (wp do_machine_op_valid_cap) @@ -107,9 +107,9 @@ lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: done crunch set_irq_state - for valid_global_refs[Interrupt_AI_asms]: "valid_global_refs" + for valid_global_refs[Interrupt_AI_assms]: "valid_global_refs" -lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: +lemma invoke_irq_handler_invs'[Interrupt_AI_assms]: assumes dmo_ex_inv[wp]: "\f. \invs and ex_inv\ do_machine_op f \\rv::unit. ex_inv\" assumes cap_insert_ex_inv[wp]: "\cap src dest. \ex_inv and invs and K (src \ dest)\ @@ -165,7 +165,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: done qed -lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: +lemma (* invoke_irq_control_invs *) [Interrupt_AI_assms]: "\invs and irq_control_inv_valid i\ invoke_irq_control i \\rv. invs\" apply (cases i, simp_all) apply (wp cap_insert_simple_invs @@ -189,7 +189,7 @@ lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: crunch resetTimer for device_state_inv[wp]: "\ms. P (device_state ms)" -lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: +lemma resetTimer_invs_ARCH[Interrupt_AI_assms]: "\invs\ do_machine_op resetTimer \\_. invs\" apply (wp dmo_invs) apply safe @@ -202,11 +202,11 @@ lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption) done -lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (ackInterrupt irq)" by (wp | simp add: ackInterrupt_def)+ -lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (maskInterrupt f irq)" by (wp | simp add: maskInterrupt_def)+ @@ -269,7 +269,7 @@ lemma handle_reserved_irq_invs[wp]: "\invs\ handle_reserved_irq irq \\_. invs\" unfolding handle_reserved_irq_def by (wpsimp simp: non_kernel_IRQs_def) -lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: +lemma (* handle_interrupt_invs *) [Interrupt_AI_assms]: "\invs\ handle_interrupt irq \\_. invs\" apply (simp add: handle_interrupt_def) apply (rule conjI; rule impI) @@ -286,7 +286,7 @@ lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: | rule conjI)+ done -lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_asms]: +lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_assms]: "\arch_irq_control_inv_valid i\ set_thread_state t st \\rv. arch_irq_control_inv_valid i\" @@ -303,7 +303,7 @@ end interpretation Interrupt_AI?: Interrupt_AI proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_assms)?) qed end diff --git a/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy b/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy index 40371a827a..fe7b74429a 100644 --- a/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy @@ -10,11 +10,11 @@ begin context Arch begin global_naming AARCH64 -named_theorems IpcCancel_AI_asms +named_theorems IpcCancel_AI_assms crunch arch_post_cap_deletion - for typ_at[wp, IpcCancel_AI_asms]: "\s. P (typ_at T p s)" - and idle_thread[wp, IpcCancel_AI_asms]: "\s. P (idle_thread s)" + for typ_at[wp, IpcCancel_AI_assms]: "\s. P (typ_at T p s)" + and idle_thread[wp, IpcCancel_AI_assms]: "\s. P (idle_thread s)" end @@ -22,7 +22,7 @@ interpretation IpcCancel_AI?: IpcCancel_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact IpcCancel_AI_asms)?) + by (intro_locales; (unfold_locales; fact IpcCancel_AI_assms)?) qed diff --git a/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy b/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy index b482dcb70f..29af15a82c 100644 --- a/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy @@ -11,9 +11,9 @@ begin context Arch begin global_naming AARCH64 -named_theorems Schedule_AI_asms +named_theorems Schedule_AI_assms -lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: +lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_assms]: "do_machine_op (mapM (\p. storeWord p 0) S) \invs\" apply (simp add: dom_mapM) apply (rule mapM_UNIV_wp) @@ -30,16 +30,16 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: global_naming Arch -lemma arch_stt_invs [wp,Schedule_AI_asms]: +lemma arch_stt_invs [wp,Schedule_AI_assms]: "arch_switch_to_thread t' \invs\" apply (wpsimp simp: arch_switch_to_thread_def) by (rule sym_refs_VCPU_hyp_live; fastforce) -lemma arch_stt_tcb [wp,Schedule_AI_asms]: +lemma arch_stt_tcb [wp,Schedule_AI_assms]: "arch_switch_to_thread t' \tcb_at t'\" by (wpsimp simp: arch_switch_to_thread_def wp: tcb_at_typ_at) -lemma arch_stt_runnable[Schedule_AI_asms]: +lemma arch_stt_runnable[Schedule_AI_assms]: "arch_switch_to_thread t \st_tcb_at runnable t\" by (wpsimp simp: arch_switch_to_thread_def) @@ -55,7 +55,7 @@ crunch and ct[wp]: "\s. P (cur_thread s)" (wp: mapM_x_wp mapM_wp subset_refl) -lemma arch_stit_invs[wp, Schedule_AI_asms]: +lemma arch_stit_invs[wp, Schedule_AI_assms]: "arch_switch_to_idle_thread \invs\" by (wpsimp simp: arch_switch_to_idle_thread_def) @@ -68,19 +68,19 @@ crunch set_vm_root and it[wp]: "\s. P (idle_thread s)" (simp: crunch_simps wp: hoare_drop_imps) -lemma arch_stit_activatable[wp, Schedule_AI_asms]: +lemma arch_stit_activatable[wp, Schedule_AI_assms]: "arch_switch_to_idle_thread \ct_in_state activatable\" apply (clarsimp simp: arch_switch_to_idle_thread_def) apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift) done -lemma stit_invs [wp,Schedule_AI_asms]: +lemma stit_invs [wp,Schedule_AI_assms]: "switch_to_idle_thread \invs\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wpsimp|strengthen idle_strg)+ done -lemma stit_activatable[Schedule_AI_asms]: +lemma stit_activatable[Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\_. ct_in_state activatable\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wpsimp simp: ct_in_state_def) @@ -88,7 +88,7 @@ lemma stit_activatable[Schedule_AI_asms]: elim!: pred_tcb_weaken_strongerE) done -lemma stt_invs [wp,Schedule_AI_asms]: +lemma stt_invs [wp,Schedule_AI_assms]: "switch_to_thread t' \invs\" apply (simp add: switch_to_thread_def) apply wp @@ -108,14 +108,14 @@ interpretation Schedule_AI_U?: Schedule_AI_U proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed interpretation Schedule_AI?: Schedule_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed end diff --git a/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy b/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy index 70765d9317..5ad151b3e7 100644 --- a/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy @@ -11,17 +11,17 @@ begin context Arch begin global_naming AARCH64 -named_theorems Tcb_AI_asms +named_theorems Tcb_AI_assms -lemma activate_idle_invs[Tcb_AI_asms]: +lemma activate_idle_invs[Tcb_AI_assms]: "\invs and ct_idle\ arch_activate_idle_thread thread \\rv. invs and ct_idle\" by (simp add: arch_activate_idle_thread_def) -declare getRegister_empty_fail [Tcb_AI_asms] +declare getRegister_empty_fail [Tcb_AI_assms] lemma same_object_also_valid: (* arch specific *) "\ same_object_as cap cap'; s \ cap'; wellformed_cap cap; @@ -35,7 +35,7 @@ lemma same_object_also_valid: (* arch specific *) split: cap.split_asm arch_cap.split_asm option.splits)+) done -lemma same_object_obj_refs[Tcb_AI_asms]: +lemma same_object_obj_refs[Tcb_AI_assms]: "\ same_object_as cap cap' \ \ obj_refs cap = obj_refs cap'" apply (cases cap, simp_all add: same_object_as_def) @@ -122,13 +122,13 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *) done crunch arch_get_sanitise_register_info, arch_post_modify_registers - for tcb_at[wp, Tcb_AI_asms]: "tcb_at a" + for tcb_at[wp, Tcb_AI_assms]: "tcb_at a" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for invs[wp, Tcb_AI_asms]: "invs" + for invs[wp, Tcb_AI_assms]: "invs" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for ex_nonz_cap_to[wp, Tcb_AI_asms]: "ex_nonz_cap_to a" + for ex_nonz_cap_to[wp, Tcb_AI_assms]: "ex_nonz_cap_to a" -lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: +lemma finalise_cap_not_cte_wp_at[Tcb_AI_assms]: assumes x: "P cap.NullCap" shows "\\s. \cp \ ran (caps_of_state s). P cp\ finalise_cap cap fin @@ -145,7 +145,7 @@ lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: done -lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: +lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_assms]: "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" by (simp add:free_index_update_def table_cap_ref_def split:cap.splits) @@ -156,7 +156,7 @@ global_interpretation Tcb_AI_1?: Tcb_AI_1 and is_cnode_or_valid_arch = is_cnode_or_valid_arch proof goal_cases interpret Arch . - case 1 show ?case by (unfold_locales; (fact Tcb_AI_asms)?) + case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?) qed context Arch begin global_naming AARCH64 @@ -175,7 +175,7 @@ lemma use_no_cap_to_obj_asid_strg: (* arch specific *) by (fastforce simp: table_cap_ref_def vspace_asid_def valid_cap_simps obj_at_def split: cap.splits arch_cap.splits option.splits prod.splits) -lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: +lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_assms]: "\no_cap_to_obj_dr_emp cap\ cap_delete slot \\rv. no_cap_to_obj_dr_emp cap\" @@ -209,7 +209,7 @@ lemma option_case_eq_None: "((case m of None \ None | Some (a,b) \ Some a) = None) = (m = None)" by (clarsimp split: option.splits) -lemma tc_invs[Tcb_AI_asms]: +lemma tc_invs[Tcb_AI_assms]: "\invs and tcb_at a and (case_option \ (valid_cap o fst) e) and (case_option \ (valid_cap o fst) f) @@ -285,7 +285,7 @@ lemma check_valid_ipc_buffer_inv: (* arch_specific *) apply (wp | simp add: if_apply_def2 split del: if_split | wpcw)+ done -lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: +lemma check_valid_ipc_buffer_wp[Tcb_AI_assms]: "\\(s::'state_ext::state_ext state). is_arch_cap cap \ is_cnode_or_valid_arch cap \ valid_ipc_buffer_cap cap vptr \ is_aligned vptr msg_align_bits @@ -301,7 +301,7 @@ lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: valid_ipc_buffer_cap_def) done -lemma derive_no_cap_asid[wp,Tcb_AI_asms]: +lemma derive_no_cap_asid[wp,Tcb_AI_assms]: "\(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\bool\ derive_cap slot cap \\rv. no_cap_to_obj_with_diff_ref rv S\,-" @@ -315,7 +315,7 @@ lemma derive_no_cap_asid[wp,Tcb_AI_asms]: done -lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: +lemma decode_set_ipc_inv[wp,Tcb_AI_assms]: "\P::'state_ext::state_ext state \ bool\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" apply (simp add: decode_set_ipc_buffer_def whenE_def split_def @@ -324,7 +324,7 @@ lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: apply simp done -lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_assms]: "no_cap_to_obj_with_diff_ref c S s \ no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" apply (case_tac "update_cap_data P x c = NullCap") @@ -341,7 +341,7 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: done -lemma update_cap_valid[Tcb_AI_asms]: +lemma update_cap_valid[Tcb_AI_assms]: "valid_cap cap (s::'state_ext::state_ext state) \ valid_cap (case capdata of None \ cap_rights_update rs cap @@ -385,7 +385,7 @@ global_interpretation Tcb_AI?: Tcb_AI where is_cnode_or_valid_arch = AARCH64.is_cnode_or_valid_arch proof goal_cases interpret Arch . - case 1 show ?case by (unfold_locales; (fact Tcb_AI_asms)?) + case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?) qed end diff --git a/proof/invariant-abstract/ARM/ArchAInvsPre.thy b/proof/invariant-abstract/ARM/ArchAInvsPre.thy index 97956e008c..b2fe17307a 100644 --- a/proof/invariant-abstract/ARM/ArchAInvsPre.thy +++ b/proof/invariant-abstract/ARM/ArchAInvsPre.thy @@ -178,11 +178,11 @@ lemma device_frame_in_device_region: global_naming Arch -named_theorems AInvsPre_asms +named_theorems AInvsPre_assms -lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]: +lemma (* ptable_rights_imp_frame *)[AInvsPre_assms]: assumes "valid_state s" shows "ptable_rights t s x \ {} \ ptable_lift t s x = Some (addrFromPPtr y) \ @@ -225,7 +225,7 @@ end global_interpretation AInvsPre?: AInvsPre proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, fact AInvsPre_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales, fact AInvsPre_assms)?) qed requalify_facts diff --git a/proof/invariant-abstract/ARM/ArchDetype_AI.thy b/proof/invariant-abstract/ARM/ArchDetype_AI.thy index 4d902bae2c..2588299497 100644 --- a/proof/invariant-abstract/ARM/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetype_AI.thy @@ -10,16 +10,16 @@ begin context Arch begin global_naming ARM -named_theorems Detype_AI_asms +named_theorems Detype_AI_assms -lemma valid_globals_irq_node[Detype_AI_asms]: +lemma valid_globals_irq_node[Detype_AI_assms]: "\ valid_global_refs s; cte_wp_at ((=) cap) ptr s \ \ interrupt_irq_node s irq \ cap_range cap" apply (erule(1) valid_global_refsD) apply (simp add: global_refs_def) done -lemma caps_of_state_ko[Detype_AI_asms]: +lemma caps_of_state_ko[Detype_AI_assms]: "valid_cap cap s \ is_untyped_cap cap \ cap_range cap = {} \ @@ -34,7 +34,7 @@ lemma caps_of_state_ko[Detype_AI_asms]: done -lemma mapM_x_storeWord[Detype_AI_asms]: +lemma mapM_x_storeWord[Detype_AI_assms]: (* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *) assumes al: "is_aligned ptr word_size_bits" shows "mapM_x (\x. storeWord (ptr + of_nat x * word_size) 0) [0..x. if x \ S then {} else state_hyp_refs_of s x)" by (rule ext, simp add: state_hyp_refs_of_def detype_def) -lemma valid_ioports_detype[Detype_AI_asms]: +lemma valid_ioports_detype[Detype_AI_assms]: "valid_ioports s \ valid_ioports (detype (untyped_range cap) s)" by auto @@ -124,7 +124,7 @@ interpretation Detype_AI?: Detype_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Detype_AI_asms)?) + by (intro_locales; (unfold_locales; fact Detype_AI_assms)?) qed context detype_locale_arch begin diff --git a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy index a4b9752fde..c7a2201c31 100644 --- a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy @@ -10,9 +10,9 @@ begin context Arch begin -named_theorems Finalise_AI_asms +named_theorems Finalise_AI_assms -lemma (* obj_at_not_live_valid_arch_cap_strg *) [Finalise_AI_asms]: +lemma (* obj_at_not_live_valid_arch_cap_strg *) [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: valid_cap_def obj_at_def @@ -20,7 +20,7 @@ lemma (* obj_at_not_live_valid_arch_cap_strg *) [Finalise_AI_asms]: split: arch_cap.split_asm if_splits) crunch prepare_thread_delete - for caps_of_state[wp,Finalise_AI_asms]: "\s. P (caps_of_state s)" + for caps_of_state[wp,Finalise_AI_assms]: "\s. P (caps_of_state s)" global_naming ARM @@ -234,22 +234,22 @@ lemma unmap_page_tcb_cap_valid: global_naming Arch -lemma (* replaceable_cdt_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_cdt_update *)[simp,Finalise_AI_assms]: "replaceable (cdt_update f s) = replaceable s" by (fastforce simp: replaceable_def tcb_cap_valid_def) -lemma (* replaceable_revokable_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_revokable_update *)[simp,Finalise_AI_assms]: "replaceable (is_original_cap_update f s) = replaceable s" by (fastforce simp: replaceable_def is_final_cap'_def2 tcb_cap_valid_def) -lemma (* replaceable_more_update *) [simp,Finalise_AI_asms]: +lemma (* replaceable_more_update *) [simp,Finalise_AI_assms]: "replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'" by (simp add: replaceable_def) -lemma (* obj_ref_ofI *) [Finalise_AI_asms]: "obj_refs cap = {x} \ obj_ref_of cap = x" +lemma (* obj_ref_ofI *) [Finalise_AI_assms]: "obj_refs cap = {x} \ obj_ref_of cap = x" by (case_tac cap, simp_all) (rename_tac arch_cap, case_tac arch_cap, simp_all) -lemma (* empty_slot_invs *) [Finalise_AI_asms]: +lemma (* empty_slot_invs *) [Finalise_AI_assms]: "\\s. invs s \ cte_wp_at (replaceable s sl cap.NullCap) sl s \ emptyable sl s \ (info \ NullCap \ post_cap_delete_pre info ((caps_of_state s) (sl \ NullCap)))\ @@ -325,7 +325,7 @@ lemma (* empty_slot_invs *) [Finalise_AI_asms]: apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state) done -lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: +lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_assms]: "dom tcb_cap_cases = {xs. length xs = 3 \ unat (of_bl xs :: machine_word) < 5}" apply (rule set_eqI, rule iffI) apply clarsimp @@ -335,7 +335,7 @@ lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: apply (clarsimp simp: nat_to_cref_unat_of_bl') done -lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]: +lemma (* unbind_notification_final *) [wp,Finalise_AI_assms]: "\is_final_cap' cap\ unbind_notification t \ \rv. is_final_cap' cap\" unfolding unbind_notification_def apply (wp final_cap_lift thread_set_caps_of_state_trivial hoare_drop_imps @@ -345,7 +345,7 @@ lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]: crunch prepare_thread_delete for is_final_cap'[wp]: "is_final_cap' cap" -lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: +lemma (* finalise_cap_cases1 *)[Finalise_AI_assms]: "\\s. final \ is_final_cap' cap s \ cte_wp_at ((=) cap) slot s\ finalise_cap cap final @@ -376,14 +376,14 @@ lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: done crunch arch_finalise_cap,prepare_thread_delete - for typ_at_arch[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at_arch[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" (wp: crunch_wps simp: crunch_simps unless_def assertE_def ignore: maskInterrupt ) crunch prepare_thread_delete for tcb_at[wp]: "\s. tcb_at p s" -lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]: +lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_assms]: "\valid_cap cap\ finalise_cap cap x \\rv. valid_cap (fst rv)\" apply (cases cap, simp_all) apply (wp suspend_valid_cap @@ -397,7 +397,7 @@ lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]: split del: if_split|clarsimp|wpc)+ done -lemma (* arch_finalise_cap_invs *)[wp,Finalise_AI_asms]: +lemma (* arch_finalise_cap_invs *)[wp,Finalise_AI_assms]: "\invs and valid_cap (ArchObjectCap cap)\ arch_finalise_cap cap final \\rv. invs\" @@ -408,7 +408,7 @@ lemma (* arch_finalise_cap_invs *)[wp,Finalise_AI_asms]: apply (auto simp: mask_def vmsz_aligned_def) done -lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_asms]: +lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: valid_cap_def obj_at_def @@ -457,7 +457,7 @@ lemma arch_finalise_cap_replaceable[wp]: done global_naming Arch -lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_assms]: "\if_unsafe_then_cap and valid_global_refs and cte_wp_at (\cp. cap_irqs cp \ {}) sl\ deleting_irq_handler irq @@ -478,7 +478,7 @@ lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: apply (clarsimp simp: appropriate_cte_cap_def split: cap.split_asm) done -lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_assms]: "\ cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap \ \ no_cap_to_obj_with_diff_ref cap' {p} s" @@ -500,7 +500,7 @@ lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: gen_obj_refs_Int) done -lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]: +lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_assms]: "\no_cap_to_obj_with_diff_ref cap S\ suspend t \\rv. no_cap_to_obj_with_diff_ref cap S\" @@ -529,7 +529,7 @@ lemma suspend_unlive': apply simp done -lemma finalise_cap_replaceable [Finalise_AI_asms]: +lemma finalise_cap_replaceable [Finalise_AI_assms]: "\\s. s \ cap \ x = is_final_cap' cap s \ valid_mdb s \ cte_wp_at ((=) cap) sl s \ valid_objs s \ sym_refs (state_refs_of s) \ (cap_irqs cap \ {} \ if_unsafe_then_cap s \ valid_global_refs s) @@ -581,7 +581,7 @@ lemma finalise_cap_replaceable [Finalise_AI_asms]: | simp add: valid_cap_simps is_nondevice_page_cap_simps)+) done -lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_assms]: assumes x: "\cap. P cap \ \ can_fast_finalise cap" shows "\cte_wp_at P p\ deleting_irq_handler irq \\rv. cte_wp_at P p\" apply (simp add: deleting_irq_handler_def) @@ -590,11 +590,11 @@ lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]: crunch arch_finalise_cap - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at) crunch prepare_thread_delete - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at) end @@ -602,7 +602,7 @@ end interpretation Finalise_AI_1?: Finalise_AI_1 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM @@ -627,7 +627,7 @@ lemma fast_finalise_replaceable[wp]: done global_naming Arch -lemma (* cap_delete_one_invs *) [Finalise_AI_asms,wp]: +lemma (* cap_delete_one_invs *) [Finalise_AI_assms,wp]: "\invs and emptyable ptr\ cap_delete_one ptr \\rv. invs\" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (rule hoare_pre) @@ -641,7 +641,7 @@ end interpretation Finalise_AI_2?: Finalise_AI_2 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM @@ -651,7 +651,7 @@ crunch arch_finalise_cap (wp: crunch_wps simp: crunch_simps) crunch prepare_thread_delete - for irq_node[wp,Finalise_AI_asms]: "\s. P (interrupt_irq_node s)" + for irq_node[wp,Finalise_AI_assms]: "\s. P (interrupt_irq_node s)" crunch arch_finalise_cap for pred_tcb_at[wp]: "pred_tcb_at proj P t" @@ -1233,7 +1233,7 @@ global_naming Arch crunch prepare_thread_delete for invs[wp]: invs -lemma (* finalise_cap_invs *)[Finalise_AI_asms]: +lemma (* finalise_cap_invs *)[Finalise_AI_assms]: shows "\invs and cte_wp_at ((=) cap) slot\ finalise_cap cap x \\rv. invs\" apply (cases cap, simp_all split del: if_split) apply (wp cancel_all_ipc_invs cancel_all_signals_invs unbind_notification_invs @@ -1250,16 +1250,16 @@ lemma (* finalise_cap_invs *)[Finalise_AI_asms]: apply (auto dest: cte_wp_at_valid_objs_valid_cap) done -lemma (* finalise_cap_irq_node *)[Finalise_AI_asms]: +lemma (* finalise_cap_irq_node *)[Finalise_AI_assms]: "\\s. P (interrupt_irq_node s)\ finalise_cap a b \\_ s. P (interrupt_irq_node s)\" apply (case_tac a,simp_all) apply (wp | clarsimp)+ done -lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_asms] +lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_assms] = hoare_use_eq_irq_node [OF arch_finalise_cap_irq_node arch_finalise_cap_cte_wp_at] -lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: +lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_assms]: "\st_tcb_at P t and K (\st. simple st \ P st)\ deleting_irq_handler irq \\rv. st_tcb_at P t\" @@ -1268,11 +1268,11 @@ lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: apply simp done -lemma irq_node_global_refs_ARCH [Finalise_AI_asms]: +lemma irq_node_global_refs_ARCH [Finalise_AI_assms]: "interrupt_irq_node s irq \ global_refs s" by (simp add: global_refs_def) -lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: +lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_assms]: "\invs\ get_irq_slot irq \cte_wp_at can_fast_finalise\" apply (simp add: get_irq_slot_def) apply wp @@ -1294,12 +1294,12 @@ lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: apply (clarsimp simp: cap_range_def) done -lemma (* replaceable_or_arch_update_same *) [Finalise_AI_asms]: +lemma (* replaceable_or_arch_update_same *) [Finalise_AI_assms]: "replaceable_or_arch_update s slot cap cap" by (clarsimp simp: replaceable_or_arch_update_def replaceable_def is_arch_update_def is_cap_simps) -lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: +lemma (* replace_cap_invs_arch_update *)[Finalise_AI_assms]: "\\s. cte_wp_at (replaceable_or_arch_update s p cap) p s \ invs s \ cap \ cap.NullCap @@ -1317,7 +1317,7 @@ lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: apply simp done -lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: +lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_assms]: "\\s. P (tcb_cap_valid cap ptr s)\ do_machine_op mop \\_ s. P (tcb_cap_valid cap ptr s)\" apply (simp add: tcb_cap_valid_def no_cap_to_obj_with_diff_ref_def) apply (rule hoare_pre) @@ -1326,7 +1326,7 @@ lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: apply simp done -lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_asms,wp]: +lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_assms,wp]: "\\s. replaceable_or_arch_update s slot cap cap'\ do_machine_op mo \\r s. replaceable_or_arch_update s slot cap cap'\" @@ -1348,7 +1348,7 @@ interpretation Finalise_AI_3?: Finalise_AI_3 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM @@ -1366,7 +1366,7 @@ interpretation Finalise_AI_4?: Finalise_AI_4 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM @@ -1661,10 +1661,10 @@ crunch unmap_page_table, invalidate_tlb_by_asid, global_naming Arch -lemmas clearMemory_invs [wp,Finalise_AI_asms] +lemmas clearMemory_invs [wp,Finalise_AI_assms] = clearMemory_invs -lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: +lemma valid_idle_has_null_cap_ARCH[Finalise_AI_assms]: "\ if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s\ \ caps_of_state s (idle_thread s, v) = Some cap \ cap = NullCap" @@ -1680,7 +1680,7 @@ lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: apply (drule_tac x=word in spec, simp) done -lemma (* zombie_cap_two_nonidles *)[Finalise_AI_asms]: +lemma (* zombie_cap_two_nonidles *)[Finalise_AI_assms]: "\ caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s \ \ fst ptr \ idle_thread s \ ptr' \ idle_thread s" apply (frule valid_global_refsD2, clarsimp+) @@ -1706,7 +1706,7 @@ interpretation Finalise_AI_5?: Finalise_AI_5 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed end diff --git a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy index 61058a2bf9..51cc82cb0c 100644 --- a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy @@ -23,16 +23,16 @@ primrec arch_irq_control_inv_valid_real :: defs arch_irq_control_inv_valid_def: "arch_irq_control_inv_valid \ arch_irq_control_inv_valid_real" -named_theorems Interrupt_AI_asms +named_theorems Interrupt_AI_assms -lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]: +lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_assms]: "\P\ decode_irq_control_invocation label args slot caps \\rv. P\" apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def arch_decode_irq_control_invocation_def whenE_def, safe) apply (wp | simp)+ done -lemma decode_irq_control_valid [Interrupt_AI_asms]: +lemma decode_irq_control_valid [Interrupt_AI_assms]: "\\s. invs s \ (\cap \ set caps. s \ cap) \ (\cap \ set caps. is_cnode_cap cap \ (\r \ cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) @@ -49,7 +49,7 @@ lemma decode_irq_control_valid [Interrupt_AI_asms]: apply (cases caps ; fastforce simp: cte_wp_at_eq_simp) done -lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: +lemma get_irq_slot_different_ARCH[Interrupt_AI_assms]: "\\s. valid_global_refs s \ ex_cte_cap_wp_to is_cnode_cap ptr s\ get_irq_slot irq \\rv s. rv \ ptr\" @@ -61,7 +61,7 @@ lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def) done -lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: +lemma is_derived_use_interrupt_ARCH[Interrupt_AI_assms]: "(is_ntfn_cap cap \ interrupt_derived cap cap') \ (is_derived m p cap cap')" apply (clarsimp simp: is_cap_simps) apply (clarsimp simp: interrupt_derived_def is_derived_def) @@ -69,7 +69,7 @@ lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def) done -lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]: +lemma maskInterrupt_invs_ARCH[Interrupt_AI_assms]: "\invs and (\s. \b \ interrupt_states s irq \ IRQInactive)\ do_machine_op (maskInterrupt b irq) \\rv. invs\" @@ -79,13 +79,13 @@ lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]: valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def) done -lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]: +lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_assms]: "no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \" by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state obj_ref_none_no_asid) -lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: +lemma (* set_irq_state_valid_cap *)[Interrupt_AI_assms]: "\valid_cap cap\ set_irq_state IRQSignal irq \\rv. valid_cap cap\" apply (clarsimp simp: set_irq_state_def) apply (wp do_machine_op_valid_cap) @@ -95,12 +95,12 @@ lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: done crunch set_irq_state - for valid_global_refs[Interrupt_AI_asms]: "valid_global_refs" + for valid_global_refs[Interrupt_AI_assms]: "valid_global_refs" crunch arch_invoke_irq_handler for typ_at[wp]: "\s. P (typ_at T p s)" -lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: +lemma invoke_irq_handler_invs'[Interrupt_AI_assms]: assumes dmo_ex_inv[wp]: "\f. \invs and ex_inv\ do_machine_op f \\rv::unit. ex_inv\" assumes cap_insert_ex_inv[wp]: "\cap src dest. \ex_inv and invs and K (src \ dest)\ @@ -156,7 +156,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: done qed -lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: +lemma (* invoke_irq_control_invs *) [Interrupt_AI_assms]: "\invs and irq_control_inv_valid i\ invoke_irq_control i \\rv. invs\" apply (cases i, simp_all) apply (wp cap_insert_simple_invs @@ -180,7 +180,7 @@ lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: crunch resetTimer for device_state_inv[wp]: "\ms. P (device_state ms)" -lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: +lemma resetTimer_invs_ARCH[Interrupt_AI_assms]: "\invs\ do_machine_op resetTimer \\_. invs\" apply (wp dmo_invs) apply safe @@ -193,15 +193,15 @@ lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption) done -lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (ackInterrupt irq)" by (wp | simp add: ackInterrupt_def)+ -lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (maskInterrupt f irq)" by (wp | simp add: maskInterrupt_def)+ -lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: +lemma (* handle_interrupt_invs *) [Interrupt_AI_assms]: "\invs\ handle_interrupt irq \\_. invs\" apply (simp add: handle_interrupt_def) apply (rule conjI; rule impI) @@ -217,7 +217,7 @@ lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: | simp add: get_irq_state_def handle_reserved_irq_def)+ done -lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_asms]: +lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_assms]: "\arch_irq_control_inv_valid i\ set_thread_state t st \\rv. arch_irq_control_inv_valid i\" @@ -232,7 +232,7 @@ end interpretation Interrupt_AI?: Interrupt_AI proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_assms)?) qed end diff --git a/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy b/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy index 8f0e8b96a3..ca35fa7912 100644 --- a/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy @@ -10,11 +10,11 @@ begin context Arch begin global_naming ARM -named_theorems IpcCancel_AI_asms +named_theorems IpcCancel_AI_assms crunch arch_post_cap_deletion - for typ_at[wp, IpcCancel_AI_asms]: "\s. P (typ_at T p s)" - and idle_thread[wp, IpcCancel_AI_asms]: "\s. P (idle_thread s)" + for typ_at[wp, IpcCancel_AI_assms]: "\s. P (typ_at T p s)" + and idle_thread[wp, IpcCancel_AI_assms]: "\s. P (idle_thread s)" end @@ -22,7 +22,7 @@ interpretation IpcCancel_AI?: IpcCancel_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact IpcCancel_AI_asms)?) + by (intro_locales; (unfold_locales; fact IpcCancel_AI_assms)?) qed diff --git a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy index 713560f6b5..72f9324db3 100644 --- a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy @@ -10,9 +10,9 @@ begin context Arch begin global_naming ARM -named_theorems Schedule_AI_asms +named_theorems Schedule_AI_assms -lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: +lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_assms]: "valid invs (do_machine_op (mapM (\p. storeWord p 0) S)) (\_. invs)" apply (simp add: dom_mapM ef_storeWord) apply (rule mapM_UNIV_wp) @@ -40,25 +40,25 @@ lemma clearExMonitor_invs [wp]: global_naming Arch -lemma arch_stt_invs [wp,Schedule_AI_asms]: +lemma arch_stt_invs [wp,Schedule_AI_assms]: "\invs\ arch_switch_to_thread t' \\_. invs\" apply (simp add: arch_switch_to_thread_def) apply wp done -lemma arch_stt_tcb [wp,Schedule_AI_asms]: +lemma arch_stt_tcb [wp,Schedule_AI_assms]: "\tcb_at t'\ arch_switch_to_thread t' \\_. tcb_at t'\" apply (simp add: arch_switch_to_thread_def) apply (wp) done -lemma arch_stt_runnable[Schedule_AI_asms]: +lemma arch_stt_runnable[Schedule_AI_assms]: "\st_tcb_at runnable t\ arch_switch_to_thread t \\r . st_tcb_at runnable t\" apply (simp add: arch_switch_to_thread_def) apply wp done -lemma arch_stit_invs[wp, Schedule_AI_asms]: +lemma arch_stit_invs[wp, Schedule_AI_assms]: "\invs\ arch_switch_to_idle_thread \\r. invs\" by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def) @@ -72,20 +72,20 @@ crunch set_vm_root for ct[wp]: "\s. P (cur_thread s)" (wp: crunch_wps simp: crunch_simps) -lemma arch_stit_activatable[wp, Schedule_AI_asms]: +lemma arch_stit_activatable[wp, Schedule_AI_assms]: "\ct_in_state activatable\ arch_switch_to_idle_thread \\rv . ct_in_state activatable\" apply (clarsimp simp: arch_switch_to_idle_thread_def) apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift) done -lemma stit_invs [wp,Schedule_AI_asms]: +lemma stit_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv. invs\" apply (simp add: switch_to_idle_thread_def) apply (wp sct_invs) by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def) -lemma stit_activatable[Schedule_AI_asms]: +lemma stit_activatable[Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv . ct_in_state activatable\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wp | simp add: ct_in_state_def)+ @@ -93,7 +93,7 @@ lemma stit_activatable[Schedule_AI_asms]: elim!: pred_tcb_weaken_strongerE) done -lemma stt_invs [wp,Schedule_AI_asms]: +lemma stt_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_thread t' \\_. invs\" apply (simp add: switch_to_thread_def) apply wp @@ -113,14 +113,14 @@ interpretation Schedule_AI_U?: Schedule_AI_U proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed interpretation Schedule_AI?: Schedule_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed end diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy index 3fbd5199e5..a9bb4e3b8a 100644 --- a/proof/invariant-abstract/ARM/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -10,17 +10,17 @@ begin context Arch begin global_naming ARM -named_theorems Tcb_AI_asms +named_theorems Tcb_AI_assms -lemma activate_idle_invs[Tcb_AI_asms]: +lemma activate_idle_invs[Tcb_AI_assms]: "\invs and ct_idle\ arch_activate_idle_thread thread \\rv. invs and ct_idle\" by (simp add: arch_activate_idle_thread_def) -lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]: +lemma empty_fail_getRegister [intro!, simp, Tcb_AI_assms]: "empty_fail (getRegister r)" by (simp add: getRegister_def) @@ -37,7 +37,7 @@ lemma same_object_also_valid: (* arch specific *) split: cap.split_asm arch_cap.split_asm option.splits)+) done -lemma same_object_obj_refs[Tcb_AI_asms]: +lemma same_object_obj_refs[Tcb_AI_assms]: "\ same_object_as cap cap' \ \ obj_refs cap = obj_refs cap'" apply (cases cap, simp_all add: same_object_as_def) @@ -135,13 +135,13 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *) done crunch arch_get_sanitise_register_info, arch_post_modify_registers - for tcb_at[wp, Tcb_AI_asms]: "tcb_at a" + for tcb_at[wp, Tcb_AI_assms]: "tcb_at a" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for invs[wp, Tcb_AI_asms]: "invs" + for invs[wp, Tcb_AI_assms]: "invs" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for ex_nonz_cap_to[wp, Tcb_AI_asms]: "ex_nonz_cap_to a" + for ex_nonz_cap_to[wp, Tcb_AI_assms]: "ex_nonz_cap_to a" -lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: +lemma finalise_cap_not_cte_wp_at[Tcb_AI_assms]: assumes x: "P cap.NullCap" shows "\\s. \cp \ ran (caps_of_state s). P cp\ finalise_cap cap fin @@ -158,7 +158,7 @@ lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: done -lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: +lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_assms]: "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" by (simp add: free_index_update_def table_cap_ref_def split: cap.splits) @@ -166,7 +166,7 @@ lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: interpretation Tcb_AI_1? : Tcb_AI_1 where state_ext_t = state_ext_t and is_cnode_or_valid_arch = is_cnode_or_valid_arch -by (unfold_locales; fact Tcb_AI_asms) +by (unfold_locales; fact Tcb_AI_assms) lemma use_no_cap_to_obj_asid_strg: (* arch specific *) @@ -183,7 +183,7 @@ lemma use_no_cap_to_obj_asid_strg: (* arch specific *) apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+ done -lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: +lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_assms]: "\no_cap_to_obj_dr_emp cap\ cap_delete slot \\rv. no_cap_to_obj_dr_emp cap\" @@ -212,7 +212,7 @@ lemma as_user_ipc_tcb_cap_valid4[wp]: apply (clarsimp simp: get_tcb_def) done -lemma tc_invs[Tcb_AI_asms]: +lemma tc_invs[Tcb_AI_assms]: "\invs and tcb_at a and (case_option \ (valid_cap o fst) e) and (case_option \ (valid_cap o fst) f) @@ -291,7 +291,7 @@ lemma check_valid_ipc_buffer_inv: apply (wp | simp add: whenE_def if_apply_def2 | wpcw)+ done -lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: +lemma check_valid_ipc_buffer_wp[Tcb_AI_assms]: "\\(s::'state_ext::state_ext state). is_arch_cap cap \ is_cnode_or_valid_arch cap \ valid_ipc_buffer_cap cap vptr \ is_aligned vptr msg_align_bits @@ -307,7 +307,7 @@ lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: valid_ipc_buffer_cap_def) done -lemma derive_no_cap_asid[wp,Tcb_AI_asms]: +lemma derive_no_cap_asid[wp,Tcb_AI_assms]: "\(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\bool\ derive_cap slot cap \\rv. no_cap_to_obj_with_diff_ref rv S\,-" @@ -321,7 +321,7 @@ lemma derive_no_cap_asid[wp,Tcb_AI_asms]: done -lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: +lemma decode_set_ipc_inv[wp,Tcb_AI_assms]: "\P::'state_ext::state_ext state \ bool\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" apply (simp add: decode_set_ipc_buffer_def whenE_def split_def @@ -330,7 +330,7 @@ lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: apply simp done -lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_assms]: "no_cap_to_obj_with_diff_ref c S s \ no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" apply (case_tac "update_cap_data P x c = NullCap") @@ -347,7 +347,7 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: done -lemma update_cap_valid[Tcb_AI_asms]: +lemma update_cap_valid[Tcb_AI_assms]: "valid_cap cap (s::'state_ext::state_ext state) \ valid_cap (case capdata of None \ cap_rights_update rs cap @@ -389,7 +389,7 @@ global_interpretation Tcb_AI?: Tcb_AI proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; fact Tcb_AI_asms) + by (unfold_locales; fact Tcb_AI_assms) qed end diff --git a/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy b/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy index 102cd05218..f4d3214e53 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy @@ -98,13 +98,13 @@ lemma device_frame_in_device_region: global_naming Arch -named_theorems AInvsPre_asms +named_theorems AInvsPre_assms lemma get_page_info_0[simp]: "get_page_info (\obj. get_arch_obj (kheap s obj)) 0 x = None" by (simp add: get_page_info_def) -lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]: +lemma (* ptable_rights_imp_frame *)[AInvsPre_assms]: assumes "valid_state s" shows "ptable_rights t s x \ {} \ ptable_lift t s x = Some (addrFromPPtr y) \ @@ -138,7 +138,7 @@ end global_interpretation AInvsPre?: AInvsPre proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, fact AInvsPre_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales, fact AInvsPre_assms)?) qed requalify_facts diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy index ae44dac57a..5400266d68 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy @@ -10,16 +10,16 @@ begin context Arch begin global_naming ARM_HYP -named_theorems Detype_AI_asms +named_theorems Detype_AI_assms -lemma valid_globals_irq_node[Detype_AI_asms]: +lemma valid_globals_irq_node[Detype_AI_assms]: "\ valid_global_refs s; cte_wp_at ((=) cap) ptr s \ \ interrupt_irq_node s irq \ cap_range cap" apply (erule(1) valid_global_refsD) apply (simp add: global_refs_def) done -lemma caps_of_state_ko[Detype_AI_asms]: +lemma caps_of_state_ko[Detype_AI_assms]: "valid_cap cap s \ is_untyped_cap cap \ cap_range cap = {} \ @@ -38,7 +38,7 @@ lemma caps_of_state_ko[Detype_AI_asms]: is_cap_simps )+ done -lemma mapM_x_storeWord[Detype_AI_asms]: +lemma mapM_x_storeWord[Detype_AI_assms]: (* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *) assumes al: "is_aligned ptr word_size_bits" shows "mapM_x (\x. storeWord (ptr + of_nat x * word_size) 0) [0..x. if x \ S then {} else state_hyp_refs_of s x)" by (rule ext, simp add: state_hyp_refs_of_def detype_def) -lemma valid_ioports_detype[Detype_AI_asms]: +lemma valid_ioports_detype[Detype_AI_assms]: "valid_ioports s \ valid_ioports (detype (untyped_range cap) s)" by auto @@ -128,7 +128,7 @@ interpretation Detype_AI?: Detype_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Detype_AI_asms)?) + by (intro_locales; (unfold_locales; fact Detype_AI_assms)?) qed context detype_locale_arch begin diff --git a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy index 9ca314bcf0..ff6033c15f 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy @@ -11,13 +11,13 @@ begin context Arch begin -named_theorems Finalise_AI_asms +named_theorems Finalise_AI_assms crunch prepare_thread_delete for caps_of_state[wp]: "\s. P (caps_of_state s)" (wp: crunch_wps) -declare prepare_thread_delete_caps_of_state [Finalise_AI_asms] +declare prepare_thread_delete_caps_of_state [Finalise_AI_assms] global_naming ARM_HYP @@ -242,22 +242,22 @@ lemma unmap_page_tcb_cap_valid: global_naming Arch -lemma (* replaceable_cdt_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_cdt_update *)[simp,Finalise_AI_assms]: "replaceable (cdt_update f s) = replaceable s" by (fastforce simp: replaceable_def tcb_cap_valid_def) -lemma (* replaceable_revokable_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_revokable_update *)[simp,Finalise_AI_assms]: "replaceable (is_original_cap_update f s) = replaceable s" by (fastforce simp: replaceable_def is_final_cap'_def2 tcb_cap_valid_def) -lemma (* replaceable_more_update *) [simp,Finalise_AI_asms]: +lemma (* replaceable_more_update *) [simp,Finalise_AI_assms]: "replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'" by (simp add: replaceable_def) -lemma (* obj_ref_ofI *) [Finalise_AI_asms]: "obj_refs cap = {x} \ obj_ref_of cap = x" +lemma (* obj_ref_ofI *) [Finalise_AI_assms]: "obj_refs cap = {x} \ obj_ref_of cap = x" by (case_tac cap, simp_all) (rename_tac arch_cap, case_tac arch_cap, simp_all) -lemma (* empty_slot_invs *) [Finalise_AI_asms]: +lemma (* empty_slot_invs *) [Finalise_AI_assms]: "\\s. invs s \ cte_wp_at (replaceable s sl cap.NullCap) sl s \ emptyable sl s \ (info \ NullCap \ post_cap_delete_pre info ((caps_of_state s) (sl \ NullCap)))\ @@ -333,7 +333,7 @@ lemma (* empty_slot_invs *) [Finalise_AI_asms]: apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state) done -lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: +lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_assms]: "dom tcb_cap_cases = {xs. length xs = 3 \ unat (of_bl xs :: machine_word) < 5}" apply (rule set_eqI, rule iffI) apply clarsimp @@ -343,7 +343,7 @@ lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: apply (clarsimp simp: nat_to_cref_unat_of_bl') done -lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]: +lemma (* unbind_notification_final *) [wp,Finalise_AI_assms]: "\is_final_cap' cap\ unbind_notification t \ \rv. is_final_cap' cap\" unfolding unbind_notification_def apply (wp final_cap_lift thread_set_caps_of_state_trivial hoare_drop_imps @@ -371,7 +371,7 @@ lemma prepare_thread_delete_final[wp]: | wpc | clarsimp simp add: tcb_cap_cases_def)+ done -lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: +lemma (* finalise_cap_cases1 *)[Finalise_AI_assms]: "\\s. final \ is_final_cap' cap s \ cte_wp_at ((=) cap) slot s\ finalise_cap cap final @@ -411,12 +411,12 @@ crunch dissociate_vcpu_tcb ignore: do_machine_op set_object) (* ARMHYP fix *) crunch arch_finalise_cap - for typ_at[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" (wp: crunch_wps simp: crunch_simps unless_def assertE_def ignore: maskInterrupt set_object) (* ARMHYP fix *) crunch prepare_thread_delete - for typ_at[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" crunch arch_thread_set for tcb_at[wp]: "\s. tcb_at p s" @@ -437,7 +437,7 @@ crunch dissociate_vcpu_tcb crunch prepare_thread_delete for tcb_at[wp]: "\s. tcb_at p s" -lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]: +lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_assms]: "\valid_cap cap\ finalise_cap cap x \\rv. valid_cap (fst rv)\" apply (cases cap, simp_all) apply (wp suspend_valid_cap prepare_thread_delete_typ_at @@ -1076,7 +1076,7 @@ crunch vcpu_finalise for invs[wp]: invs (ignore: dissociate_vcpu_tcb) -lemma arch_finalise_cap_invs' [wp,Finalise_AI_asms]: +lemma arch_finalise_cap_invs' [wp,Finalise_AI_assms]: "\invs and valid_cap (ArchObjectCap cap)\ arch_finalise_cap cap final \\rv. invs\" @@ -1139,14 +1139,14 @@ lemma arch_finalise_cap_vcpu: done -lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_asms]: +lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r \ \ typ_at (AArch AVCPU) r s) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: live_def valid_cap_def obj_at_def a_type_arch_live valid_cap_simps hyp_live_def arch_live_def split: arch_cap.split_asm if_splits) -lemma obj_at_not_live_valid_arch_cap_strg' [Finalise_AI_asms]: +lemma obj_at_not_live_valid_arch_cap_strg' [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r \ cap \ VCPUCap r) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: live_def valid_cap_def obj_at_def @@ -1197,7 +1197,7 @@ lemma arch_finalise_cap_replaceable1: global_naming Arch -lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_assms]: "\if_unsafe_then_cap and valid_global_refs and cte_wp_at (\cp. cap_irqs cp \ {}) sl\ deleting_irq_handler irq @@ -1218,7 +1218,7 @@ lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: apply (clarsimp simp: appropriate_cte_cap_def split: cap.split_asm) done -lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_assms]: "\ cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap \ \ no_cap_to_obj_with_diff_ref cap' {p} s" @@ -1240,7 +1240,7 @@ lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: gen_obj_refs_Int) done -lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]: +lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_assms]: "\no_cap_to_obj_with_diff_ref cap S\ suspend t \\rv. no_cap_to_obj_with_diff_ref cap S\" @@ -1293,7 +1293,7 @@ lemma arch_finalise_cap_replaceable: \\rv s. replaceable s sl (fst rv) (cap.ArchObjectCap cap)\" by (cases cap; simp add: arch_finalise_cap_vcpu arch_finalise_cap_replaceable1) -lemma finalise_cap_replaceable [Finalise_AI_asms]: +lemma finalise_cap_replaceable [Finalise_AI_assms]: "\\s. s \ cap \ x = is_final_cap' cap s \ valid_mdb s \ cte_wp_at ((=) cap) sl s \ valid_objs s \ sym_refs (state_refs_of s) \ (cap_irqs cap \ {} \ if_unsafe_then_cap s \ valid_global_refs s) @@ -1347,7 +1347,7 @@ lemma finalise_cap_replaceable [Finalise_AI_asms]: | simp add: valid_cap_simps is_nondevice_page_cap_simps)+) done -lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_assms]: assumes x: "\cap. P cap \ \ can_fast_finalise cap" shows "\cte_wp_at P p\ deleting_irq_handler irq \\rv. cte_wp_at P p\" apply (simp add: deleting_irq_handler_def) @@ -1366,22 +1366,22 @@ lemma arch_thread_set_cte_wp_at[wp]: done crunch dissociate_vcpu_tcb - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set) crunch prepare_thread_delete - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set) crunch arch_finalise_cap - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set) end interpretation Finalise_AI_1?: Finalise_AI_1 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM_HYP @@ -1406,7 +1406,7 @@ lemma fast_finalise_replaceable[wp]: done global_naming Arch -lemma (* cap_delete_one_invs *) [Finalise_AI_asms,wp]: +lemma (* cap_delete_one_invs *) [Finalise_AI_assms,wp]: "\invs and emptyable ptr\ cap_delete_one ptr \\rv. invs\" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (rule hoare_pre) @@ -1420,7 +1420,7 @@ end interpretation Finalise_AI_2?: Finalise_AI_2 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM_HYP @@ -1432,7 +1432,7 @@ crunch (wp: crunch_wps subset_refl) crunch prepare_thread_delete - for irq_node[Finalise_AI_asms,wp]: "\s. P (interrupt_irq_node s)" + for irq_node[Finalise_AI_assms,wp]: "\s. P (interrupt_irq_node s)" (wp: crunch_wps simp: crunch_simps) crunch arch_finalise_cap @@ -2001,7 +2001,7 @@ crunch prepare_thread_delete for invs[wp]: invs (ignore: set_object) -lemma (* finalise_cap_invs *)[Finalise_AI_asms]: +lemma (* finalise_cap_invs *)[Finalise_AI_assms]: shows "\invs and cte_wp_at ((=) cap) slot\ finalise_cap cap x \\rv. invs\" apply (cases cap, simp_all split del: if_split) apply (wp cancel_all_ipc_invs cancel_all_signals_invs unbind_notification_invs @@ -2018,16 +2018,16 @@ lemma (* finalise_cap_invs *)[Finalise_AI_asms]: apply (auto dest: cte_wp_at_valid_objs_valid_cap) done -lemma (* finalise_cap_irq_node *)[Finalise_AI_asms]: +lemma (* finalise_cap_irq_node *)[Finalise_AI_assms]: "\\s. P (interrupt_irq_node s)\ finalise_cap a b \\_ s. P (interrupt_irq_node s)\" apply (case_tac a,simp_all) apply (wp | clarsimp)+ done -lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_asms] +lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_assms] = hoare_use_eq_irq_node [OF arch_finalise_cap_irq_node arch_finalise_cap_cte_wp_at] -lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: +lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_assms]: "\st_tcb_at P t and K (\st. simple st \ P st)\ deleting_irq_handler irq \\rv. st_tcb_at P t\" @@ -2036,11 +2036,11 @@ lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: apply simp done -lemma irq_node_global_refs_ARCH [Finalise_AI_asms]: +lemma irq_node_global_refs_ARCH [Finalise_AI_assms]: "interrupt_irq_node s irq \ global_refs s" by (simp add: global_refs_def) -lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: +lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_assms]: "\invs\ get_irq_slot irq \cte_wp_at can_fast_finalise\" apply (simp add: get_irq_slot_def) apply wp @@ -2062,12 +2062,12 @@ lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: apply (clarsimp simp: cap_range_def) done -lemma (* replaceable_or_arch_update_same *) [Finalise_AI_asms]: +lemma (* replaceable_or_arch_update_same *) [Finalise_AI_assms]: "replaceable_or_arch_update s slot cap cap" by (clarsimp simp: replaceable_or_arch_update_def replaceable_def is_arch_update_def is_cap_simps) -lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: +lemma (* replace_cap_invs_arch_update *)[Finalise_AI_assms]: "\\s. cte_wp_at (replaceable_or_arch_update s p cap) p s \ invs s \ cap \ cap.NullCap @@ -2085,7 +2085,7 @@ lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: apply simp done -lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: +lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_assms]: "\\s. P (tcb_cap_valid cap ptr s)\ do_machine_op mop \\_ s. P (tcb_cap_valid cap ptr s)\" apply (simp add: tcb_cap_valid_def no_cap_to_obj_with_diff_ref_def) apply (rule hoare_pre) @@ -2094,7 +2094,7 @@ lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: apply simp done -lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_asms,wp]: +lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_assms,wp]: "\\s. replaceable_or_arch_update s slot cap cap'\ do_machine_op mo \\r s. replaceable_or_arch_update s slot cap cap'\" @@ -2116,7 +2116,7 @@ interpretation Finalise_AI_3?: Finalise_AI_3 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM_HYP @@ -2134,7 +2134,7 @@ interpretation Finalise_AI_4?: Finalise_AI_4 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming ARM_HYP @@ -2428,10 +2428,10 @@ lemma arch_finalise_cap_valid_cap [wp]: global_naming Arch -lemmas clearMemory_invs [wp,Finalise_AI_asms] +lemmas clearMemory_invs [wp,Finalise_AI_assms] = clearMemory_invs -lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: +lemma valid_idle_has_null_cap_ARCH[Finalise_AI_assms]: "\ if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s\ \ caps_of_state s (idle_thread s, v) = Some cap \ cap = NullCap" @@ -2447,7 +2447,7 @@ lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: apply (drule_tac x=word in spec, simp) done -lemma (* zombie_cap_two_nonidles *)[Finalise_AI_asms]: +lemma (* zombie_cap_two_nonidles *)[Finalise_AI_assms]: "\ caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s \ \ fst ptr \ idle_thread s \ ptr' \ idle_thread s" apply (frule valid_global_refsD2, clarsimp+) @@ -2473,7 +2473,7 @@ interpretation Finalise_AI_5?: Finalise_AI_5 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed end diff --git a/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy index d193d18e47..45fa392485 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchInterrupt_AI.thy @@ -23,16 +23,16 @@ primrec arch_irq_control_inv_valid_real :: defs arch_irq_control_inv_valid_def: "arch_irq_control_inv_valid \ arch_irq_control_inv_valid_real" -named_theorems Interrupt_AI_asms +named_theorems Interrupt_AI_assms -lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]: +lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_assms]: "\P\ decode_irq_control_invocation label args slot caps \\rv. P\" apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def arch_decode_irq_control_invocation_def whenE_def, safe) apply (wp | simp)+ done -lemma decode_irq_control_valid [Interrupt_AI_asms]: +lemma decode_irq_control_valid [Interrupt_AI_assms]: "\\s. invs s \ (\cap \ set caps. s \ cap) \ (\cap \ set caps. is_cnode_cap cap \ (\r \ cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) @@ -49,7 +49,7 @@ lemma decode_irq_control_valid [Interrupt_AI_asms]: apply (cases caps ; fastforce simp: cte_wp_at_eq_simp) done -lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: +lemma get_irq_slot_different_ARCH[Interrupt_AI_assms]: "\\s. valid_global_refs s \ ex_cte_cap_wp_to is_cnode_cap ptr s\ get_irq_slot irq \\rv s. rv \ ptr\" @@ -61,7 +61,7 @@ lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def) done -lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: +lemma is_derived_use_interrupt_ARCH[Interrupt_AI_assms]: "(is_ntfn_cap cap \ interrupt_derived cap cap') \ (is_derived m p cap cap')" apply (clarsimp simp: is_cap_simps) apply (clarsimp simp: interrupt_derived_def is_derived_def) @@ -69,15 +69,15 @@ lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def) done -lemmas maskInterrupt_invs_ARCH[Interrupt_AI_asms] = maskInterrupt_invs +lemmas maskInterrupt_invs_ARCH[Interrupt_AI_assms] = maskInterrupt_invs -lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]: +lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_assms]: "no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \" by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state obj_ref_none_no_asid) -lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: +lemma (* set_irq_state_valid_cap *)[Interrupt_AI_assms]: "\valid_cap cap\ set_irq_state IRQSignal irq \\rv. valid_cap cap\" apply (clarsimp simp: set_irq_state_def) apply (wp do_machine_op_valid_cap) @@ -87,13 +87,13 @@ lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: done crunch set_irq_state - for valid_global_refs[Interrupt_AI_asms]: "valid_global_refs" + for valid_global_refs[Interrupt_AI_assms]: "valid_global_refs" crunch arch_invoke_irq_handler for typ_at[wp]: "\s. P (typ_at T p s)" and valid_list[wp]: valid_list -lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: +lemma invoke_irq_handler_invs'[Interrupt_AI_assms]: assumes dmo_ex_inv[wp]: "\f. \invs and ex_inv\ do_machine_op f \\rv::unit. ex_inv\" assumes cap_insert_ex_inv[wp]: "\cap src dest. \ex_inv and invs and K (src \ dest)\ @@ -149,7 +149,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: done qed -lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: +lemma (* invoke_irq_control_invs *) [Interrupt_AI_assms]: "\invs and irq_control_inv_valid i\ invoke_irq_control i \\rv. invs\" apply (cases i, simp_all) apply (wp cap_insert_simple_invs @@ -174,7 +174,7 @@ lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: crunch resetTimer for device_state_inv[wp]: "\ms. P (device_state ms)" -lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: +lemma resetTimer_invs_ARCH[Interrupt_AI_assms]: "\invs\ do_machine_op resetTimer \\_. invs\" apply (wp dmo_invs) apply safe @@ -187,11 +187,11 @@ lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption) done -lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (ackInterrupt irq)" by (wp | simp add: ackInterrupt_def)+ -lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (maskInterrupt f irq)" by (wp | simp add: maskInterrupt_def)+ @@ -254,7 +254,7 @@ lemma handle_reserved_irq_invs[wp]: "\invs\ handle_reserved_irq irq \\_. invs\" unfolding handle_reserved_irq_def by (wpsimp simp: non_kernel_IRQs_def) -lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: +lemma (* handle_interrupt_invs *) [Interrupt_AI_assms]: "\invs\ handle_interrupt irq \\_. invs\" apply (simp add: handle_interrupt_def) apply (rule conjI; rule impI) @@ -271,7 +271,7 @@ lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: | rule conjI)+ done -lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_asms]: +lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_assms]: "\arch_irq_control_inv_valid i\ set_thread_state t st \\rv. arch_irq_control_inv_valid i\" @@ -286,7 +286,7 @@ end interpretation Interrupt_AI?: Interrupt_AI proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_assms)?) qed end diff --git a/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy index 658ec7663e..04dc01db01 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchIpcCancel_AI.thy @@ -10,11 +10,11 @@ begin context Arch begin global_naming ARM_HYP -named_theorems IpcCancel_AI_asms +named_theorems IpcCancel_AI_assms crunch arch_post_cap_deletion - for typ_at[wp, IpcCancel_AI_asms]: "\s. P (typ_at T p s)" - and idle_thread[wp, IpcCancel_AI_asms]: "\s. P (idle_thread s)" + for typ_at[wp, IpcCancel_AI_assms]: "\s. P (typ_at T p s)" + and idle_thread[wp, IpcCancel_AI_assms]: "\s. P (idle_thread s)" end @@ -22,7 +22,7 @@ interpretation IpcCancel_AI?: IpcCancel_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact IpcCancel_AI_asms)?) + by (intro_locales; (unfold_locales; fact IpcCancel_AI_assms)?) qed diff --git a/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy index 296b00e0bf..f93a31d494 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy @@ -10,9 +10,9 @@ begin context Arch begin global_naming ARM_HYP -named_theorems Schedule_AI_asms +named_theorems Schedule_AI_assms -lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: +lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_assms]: "valid invs (do_machine_op (mapM (\p. storeWord p 0) S)) (\_. invs)" apply (simp add: dom_mapM ef_storeWord) apply (rule mapM_UNIV_wp) @@ -41,17 +41,17 @@ lemma clearExMonitor_invs [wp]: global_naming Arch -lemma arch_stt_invs [wp,Schedule_AI_asms]: +lemma arch_stt_invs [wp,Schedule_AI_assms]: "\invs\ arch_switch_to_thread t' \\_. invs\" apply (wpsimp simp: arch_switch_to_thread_def) by (rule sym_refs_VCPU_hyp_live; fastforce) -lemma arch_stt_tcb [wp,Schedule_AI_asms]: +lemma arch_stt_tcb [wp,Schedule_AI_assms]: "\tcb_at t'\ arch_switch_to_thread t' \\_. tcb_at t'\" by (wpsimp simp: arch_switch_to_thread_def wp: tcb_at_typ_at) -lemma arch_stt_runnable[Schedule_AI_asms]: +lemma arch_stt_runnable[Schedule_AI_assms]: "\st_tcb_at runnable t\ arch_switch_to_thread t \\r. st_tcb_at runnable t\" by (wpsimp simp: arch_switch_to_thread_def) @@ -71,7 +71,7 @@ crunch and ct[wp]: "\s. P (cur_thread s)" (wp: mapM_x_wp mapM_wp subset_refl) -lemma arch_stit_invs[wp, Schedule_AI_asms]: +lemma arch_stit_invs[wp, Schedule_AI_assms]: "\invs\ arch_switch_to_idle_thread \\r. invs\" by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def) @@ -86,19 +86,19 @@ crunch set_vm_root and it[wp]: "\s. P (idle_thread s)" (simp: crunch_simps wp: hoare_drop_imps) -lemma arch_stit_activatable[wp, Schedule_AI_asms]: +lemma arch_stit_activatable[wp, Schedule_AI_assms]: "\ct_in_state activatable\ arch_switch_to_idle_thread \\rv . ct_in_state activatable\" apply (clarsimp simp: arch_switch_to_idle_thread_def) apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift) done -lemma stit_invs [wp,Schedule_AI_asms]: +lemma stit_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv. invs\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wpsimp|strengthen idle_strg)+ done -lemma stit_activatable[Schedule_AI_asms]: +lemma stit_activatable[Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv . ct_in_state activatable\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wp | simp add: ct_in_state_def)+ @@ -106,7 +106,7 @@ lemma stit_activatable[Schedule_AI_asms]: elim!: pred_tcb_weaken_strongerE) done -lemma stt_invs [wp,Schedule_AI_asms]: +lemma stt_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_thread t' \\_. invs\" apply (simp add: switch_to_thread_def) apply wp @@ -126,14 +126,14 @@ interpretation Schedule_AI_U?: Schedule_AI_U proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed interpretation Schedule_AI?: Schedule_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed end diff --git a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy index e6a5abc176..2fed220f2a 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy @@ -10,17 +10,17 @@ begin context Arch begin global_naming ARM_HYP -named_theorems Tcb_AI_asms +named_theorems Tcb_AI_assms -lemma activate_idle_invs[Tcb_AI_asms]: +lemma activate_idle_invs[Tcb_AI_assms]: "\invs and ct_idle\ arch_activate_idle_thread thread \\rv. invs and ct_idle\" by (simp add: arch_activate_idle_thread_def) -lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]: +lemma empty_fail_getRegister [intro!, simp, Tcb_AI_assms]: "empty_fail (getRegister r)" by (simp add: getRegister_def) @@ -37,7 +37,7 @@ lemma same_object_also_valid: (* arch specific *) split: cap.split_asm arch_cap.split_asm option.splits)+) done -lemma same_object_obj_refs[Tcb_AI_asms]: +lemma same_object_obj_refs[Tcb_AI_assms]: "\ same_object_as cap cap' \ \ obj_refs cap = obj_refs cap'" apply (cases cap, simp_all add: same_object_as_def) @@ -135,13 +135,13 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *) done crunch arch_get_sanitise_register_info, arch_post_modify_registers - for tcb_at[wp, Tcb_AI_asms]: "tcb_at a" + for tcb_at[wp, Tcb_AI_assms]: "tcb_at a" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for invs[wp, Tcb_AI_asms]: "invs" + for invs[wp, Tcb_AI_assms]: "invs" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for ex_nonz_cap_to[wp, Tcb_AI_asms]: "ex_nonz_cap_to a" + for ex_nonz_cap_to[wp, Tcb_AI_assms]: "ex_nonz_cap_to a" -lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: +lemma finalise_cap_not_cte_wp_at[Tcb_AI_assms]: assumes x: "P cap.NullCap" shows "\\s. \cp \ ran (caps_of_state s). P cp\ finalise_cap cap fin @@ -159,7 +159,7 @@ lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: done -lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: +lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_assms]: "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" by (simp add:free_index_update_def table_cap_ref_def split:cap.splits) @@ -167,7 +167,7 @@ lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: interpretation Tcb_AI_1? : Tcb_AI_1 where state_ext_t = state_ext_t and is_cnode_or_valid_arch = is_cnode_or_valid_arch -by (unfold_locales; fact Tcb_AI_asms) +by (unfold_locales; fact Tcb_AI_assms) lemma use_no_cap_to_obj_asid_strg: (* arch specific *) @@ -185,7 +185,7 @@ lemma use_no_cap_to_obj_asid_strg: (* arch specific *) done declare arch_cap_fun_lift_simps [simp del] -lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: +lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_assms]: "\no_cap_to_obj_dr_emp cap\ cap_delete slot \\rv. no_cap_to_obj_dr_emp cap\" @@ -214,7 +214,7 @@ lemma as_user_ipc_tcb_cap_valid4[wp]: apply (clarsimp simp: get_tcb_def) done -lemma tc_invs[Tcb_AI_asms]: +lemma tc_invs[Tcb_AI_assms]: "\invs and tcb_at a and (case_option \ (valid_cap o fst) e) and (case_option \ (valid_cap o fst) f) @@ -292,7 +292,7 @@ lemma check_valid_ipc_buffer_inv: (* arch_specific *) apply (wp | simp add: if_apply_def2 split del: if_split | wpcw)+ done -lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: +lemma check_valid_ipc_buffer_wp[Tcb_AI_assms]: "\\(s::'state_ext::state_ext state). is_arch_cap cap \ is_cnode_or_valid_arch cap \ valid_ipc_buffer_cap cap vptr \ is_aligned vptr msg_align_bits @@ -308,7 +308,7 @@ lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: valid_ipc_buffer_cap_def) done -lemma derive_no_cap_asid[wp,Tcb_AI_asms]: +lemma derive_no_cap_asid[wp,Tcb_AI_assms]: "\(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\bool\ derive_cap slot cap \\rv. no_cap_to_obj_with_diff_ref rv S\,-" @@ -322,7 +322,7 @@ lemma derive_no_cap_asid[wp,Tcb_AI_asms]: done -lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: +lemma decode_set_ipc_inv[wp,Tcb_AI_assms]: "\P::'state_ext::state_ext state \ bool\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" apply (simp add: decode_set_ipc_buffer_def whenE_def split_def @@ -331,7 +331,7 @@ lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: apply simp done -lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_assms]: "no_cap_to_obj_with_diff_ref c S s \ no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" apply (case_tac "update_cap_data P x c = NullCap") @@ -348,7 +348,7 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: done -lemma update_cap_valid[Tcb_AI_asms]: +lemma update_cap_valid[Tcb_AI_assms]: "valid_cap cap (s::'state_ext::state_ext state) \ valid_cap (case capdata of None \ cap_rights_update rs cap @@ -390,7 +390,7 @@ global_interpretation Tcb_AI?: Tcb_AI proof goal_cases interpret Arch . case 1 show ?case - by (unfold_locales; fact Tcb_AI_asms) + by (unfold_locales; fact Tcb_AI_assms) qed end diff --git a/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy b/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy index b9609db770..20e3ccdf61 100644 --- a/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy +++ b/proof/invariant-abstract/RISCV64/ArchAInvsPre.thy @@ -214,7 +214,7 @@ lemma device_frame_in_device_region: by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def) global_naming Arch -named_theorems AInvsPre_asms +named_theorems AInvsPre_assms lemma get_vspace_of_thread_asid_or_global_pt: "(\asid. vspace_for_asid asid s = Some (get_vspace_of_thread (kheap s) (arch_state s) t)) @@ -222,7 +222,7 @@ lemma get_vspace_of_thread_asid_or_global_pt: by (auto simp: get_vspace_of_thread_def split: option.split kernel_object.split cap.split arch_cap.split) -lemma ptable_rights_imp_frame[AInvsPre_asms]: +lemma ptable_rights_imp_frame[AInvsPre_assms]: assumes "valid_state s" shows "\ ptable_rights t s x \ {}; ptable_lift t s x = Some (addrFromPPtr y) \ \ in_user_frame y s \ in_device_frame y s" @@ -264,7 +264,7 @@ end interpretation AInvsPre?: AInvsPre proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?) qed requalify_facts diff --git a/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy index c8dc4f125b..38b49ffa7e 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy @@ -10,16 +10,16 @@ begin context Arch begin global_naming RISCV64 -named_theorems Detype_AI_asms +named_theorems Detype_AI_assms -lemma valid_globals_irq_node[Detype_AI_asms]: +lemma valid_globals_irq_node[Detype_AI_assms]: "\ valid_global_refs s; cte_wp_at ((=) cap) ptr s \ \ interrupt_irq_node s irq \ cap_range cap" apply (erule(1) valid_global_refsD) apply (simp add: global_refs_def) done -lemma caps_of_state_ko[Detype_AI_asms]: +lemma caps_of_state_ko[Detype_AI_assms]: "valid_cap cap s \ is_untyped_cap cap \ cap_range cap = {} \ @@ -33,7 +33,7 @@ lemma caps_of_state_ko[Detype_AI_asms]: split: option.splits if_splits)+ done -lemma mapM_x_storeWord[Detype_AI_asms]: +lemma mapM_x_storeWord[Detype_AI_assms]: (* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *) assumes al: "is_aligned ptr word_size_bits" shows "mapM_x (\x. storeWord (ptr + of_nat x * word_size) 0) [0..x. if x \ S then {} else state_hyp_refs_of s x)" by (rule ext, simp add: state_hyp_refs_of_def detype_def) -lemma valid_ioports_detype[Detype_AI_asms]: +lemma valid_ioports_detype[Detype_AI_assms]: "valid_ioports s \ valid_ioports (detype (untyped_range cap) s)" by simp @@ -117,7 +117,7 @@ interpretation Detype_AI?: Detype_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Detype_AI_asms)?) + by (intro_locales; (unfold_locales; fact Detype_AI_assms)?) qed context detype_locale_arch begin diff --git a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy index 655652f695..24f036acec 100644 --- a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy @@ -10,13 +10,13 @@ begin context Arch begin -named_theorems Finalise_AI_asms +named_theorems Finalise_AI_assms crunch prepare_thread_delete for caps_of_state[wp]: "\s. P (caps_of_state s)" (wp: crunch_wps) -declare prepare_thread_delete_caps_of_state [Finalise_AI_asms] +declare prepare_thread_delete_caps_of_state [Finalise_AI_assms] global_naming RISCV64 @@ -162,17 +162,17 @@ lemma unmap_page_tcb_cap_valid: global_naming Arch -lemma (* replaceable_cdt_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_cdt_update *)[simp,Finalise_AI_assms]: "replaceable (cdt_update f s) = replaceable s" by (fastforce simp: replaceable_def tcb_cap_valid_def reachable_frame_cap_def reachable_target_def) -lemma (* replaceable_revokable_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_revokable_update *)[simp,Finalise_AI_assms]: "replaceable (is_original_cap_update f s) = replaceable s" by (fastforce simp: replaceable_def is_final_cap'_def2 tcb_cap_valid_def reachable_frame_cap_def reachable_target_def) -lemma (* replaceable_more_update *) [simp,Finalise_AI_asms]: +lemma (* replaceable_more_update *) [simp,Finalise_AI_assms]: "replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'" by (simp add: replaceable_def reachable_frame_cap_def reachable_target_def) @@ -184,9 +184,9 @@ lemma reachable_frame_cap_trans_state[simp]: "reachable_frame_cap cap (trans_state f s) = reachable_frame_cap cap s" by (simp add: reachable_frame_cap_def) -lemmas [Finalise_AI_asms] = obj_refs_obj_ref_of (* used under name obj_ref_ofI *) +lemmas [Finalise_AI_assms] = obj_refs_obj_ref_of (* used under name obj_ref_ofI *) -lemma (* empty_slot_invs *) [Finalise_AI_asms]: +lemma (* empty_slot_invs *) [Finalise_AI_assms]: "\\s. invs s \ cte_wp_at (replaceable s sl cap.NullCap) sl s \ emptyable sl s \ (info \ NullCap \ post_cap_delete_pre info ((caps_of_state s) (sl \ NullCap)))\ @@ -266,7 +266,7 @@ lemma (* empty_slot_invs *) [Finalise_AI_asms]: apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state) by fastforce -lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: +lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_assms]: "dom tcb_cap_cases = {xs. length xs = 3 \ unat (of_bl xs :: machine_word) < 5}" apply (rule set_eqI, rule iffI) apply clarsimp @@ -276,7 +276,7 @@ lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: apply (clarsimp simp: nat_to_cref_unat_of_bl') done -lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]: +lemma (* unbind_notification_final *) [wp,Finalise_AI_assms]: "\is_final_cap' cap\ unbind_notification t \ \rv. is_final_cap' cap\" unfolding unbind_notification_def apply (wp final_cap_lift thread_set_caps_of_state_trivial hoare_drop_imps @@ -309,7 +309,7 @@ lemma length_and_unat_of_bl_length: "(length xs = x \ unat (of_bl xs :: 'a::len word) < 2 ^ x) = (length xs = x)" by (auto simp: unat_of_bl_length) -lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: +lemma (* finalise_cap_cases1 *)[Finalise_AI_assms]: "\\s. final \ is_final_cap' cap s \ cte_wp_at ((=) cap) slot s\ finalise_cap cap final @@ -343,12 +343,12 @@ crunch arch_thread_set (wp: crunch_wps set_object_typ_at) crunch arch_finalise_cap - for typ_at[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" (wp: crunch_wps simp: crunch_simps unless_def assertE_def ignore: maskInterrupt set_object) crunch prepare_thread_delete - for typ_at[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" crunch arch_thread_set for tcb_at[wp]: "\s. tcb_at p s" @@ -360,7 +360,7 @@ crunch arch_thread_get crunch prepare_thread_delete for tcb_at[wp]: "\s. tcb_at p s" -lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]: +lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_assms]: "\valid_cap cap\ finalise_cap cap x \\rv. valid_cap (fst rv)\" apply (cases cap; simp) apply (wp suspend_valid_cap prepare_thread_delete_typ_at @@ -639,7 +639,7 @@ lemma as_user_valid_ioc[wp]: "\valid_ioc\ as_user t f \\rv. valid_ioc\" unfolding valid_ioc_def by (wpsimp wp: hoare_vcg_imp_lift hoare_vcg_all_lift) -lemma arch_finalise_cap_invs' [wp,Finalise_AI_asms]: +lemma arch_finalise_cap_invs' [wp,Finalise_AI_assms]: "\invs and valid_cap (ArchObjectCap cap)\ arch_finalise_cap cap final \\rv. invs\" @@ -656,7 +656,7 @@ lemma as_user_unlive[wp]: apply (wpsimp wp: set_object_wp) by (clarsimp simp: obj_at_def live_def hyp_live_def arch_tcb_context_set_def dest!: get_tcb_SomeD) -lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_asms]: +lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: valid_cap_def obj_at_def valid_arch_cap_ref_def @@ -826,7 +826,7 @@ lemma arch_finalise_cap_replaceable: global_naming Arch -lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_assms]: "\if_unsafe_then_cap and valid_global_refs and cte_wp_at (\cp. cap_irqs cp \ {}) sl\ deleting_irq_handler irq @@ -847,7 +847,7 @@ lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: apply (clarsimp simp: appropriate_cte_cap_def split: cap.split_asm) done -lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_assms]: "\ cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap \ \ no_cap_to_obj_with_diff_ref cap' {p} s" @@ -869,7 +869,7 @@ lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: gen_obj_refs_Int) done -lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]: +lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_assms]: "\no_cap_to_obj_with_diff_ref cap S\ suspend t \\rv. no_cap_to_obj_with_diff_ref cap S\" @@ -903,7 +903,7 @@ lemma prepare_thread_delete_unlive[wp]: apply (clarsimp simp: obj_at_def, case_tac ko, simp_all add: is_tcb_def live_def) done -lemma finalise_cap_replaceable [Finalise_AI_asms]: +lemma finalise_cap_replaceable [Finalise_AI_assms]: "\\s. s \ cap \ x = is_final_cap' cap s \ valid_mdb s \ cte_wp_at ((=) cap) sl s \ valid_objs s \ sym_refs (state_refs_of s) \ (cap_irqs cap \ {} \ if_unsafe_then_cap s \ valid_global_refs s) @@ -954,7 +954,7 @@ lemma finalise_cap_replaceable [Finalise_AI_asms]: | simp add: valid_cap_simps is_nondevice_page_cap_simps)+)) done -lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_assms]: assumes x: "\cap. P cap \ \ can_fast_finalise cap" shows "\cte_wp_at P p\ deleting_irq_handler irq \\rv. cte_wp_at P p\" apply (simp add: deleting_irq_handler_def) @@ -973,10 +973,10 @@ lemma arch_thread_set_cte_wp_at[wp]: done crunch prepare_thread_delete - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" crunch arch_finalise_cap - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set) end @@ -984,7 +984,7 @@ end interpretation Finalise_AI_1?: Finalise_AI_1 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming RISCV64 @@ -1009,7 +1009,7 @@ lemma fast_finalise_replaceable[wp]: done global_naming Arch -lemma (* cap_delete_one_invs *) [Finalise_AI_asms,wp]: +lemma (* cap_delete_one_invs *) [Finalise_AI_assms,wp]: "\invs and emptyable ptr\ cap_delete_one ptr \\rv. invs\" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (rule hoare_pre) @@ -1023,13 +1023,13 @@ end interpretation Finalise_AI_2?: Finalise_AI_2 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming RISCV64 crunch prepare_thread_delete - for irq_node[Finalise_AI_asms,wp]: "\s. P (interrupt_irq_node s)" + for irq_node[Finalise_AI_assms,wp]: "\s. P (interrupt_irq_node s)" crunch arch_finalise_cap for irq_node[wp]: "\s. P (interrupt_irq_node s)" @@ -1160,7 +1160,7 @@ crunch prepare_thread_delete for invs[wp]: invs (ignore: set_object) -lemma (* finalise_cap_invs *)[Finalise_AI_asms]: +lemma (* finalise_cap_invs *)[Finalise_AI_assms]: shows "\invs and cte_wp_at ((=) cap) slot\ finalise_cap cap x \\rv. invs\" apply (cases cap, simp_all split del: if_split) apply (wp cancel_all_ipc_invs cancel_all_signals_invs unbind_notification_invs @@ -1177,16 +1177,16 @@ lemma (* finalise_cap_invs *)[Finalise_AI_asms]: apply (auto dest: cte_wp_at_valid_objs_valid_cap) done -lemma (* finalise_cap_irq_node *)[Finalise_AI_asms]: +lemma (* finalise_cap_irq_node *)[Finalise_AI_assms]: "\\s. P (interrupt_irq_node s)\ finalise_cap a b \\_ s. P (interrupt_irq_node s)\" apply (case_tac a,simp_all) apply (wp | clarsimp)+ done -lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_asms] +lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_assms] = hoare_use_eq_irq_node [OF arch_finalise_cap_irq_node arch_finalise_cap_cte_wp_at] -lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: +lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_assms]: "\st_tcb_at P t and K (\st. simple st \ P st)\ deleting_irq_handler irq \\rv. st_tcb_at P t\" @@ -1195,11 +1195,11 @@ lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: apply simp done -lemma irq_node_global_refs_ARCH [Finalise_AI_asms]: +lemma irq_node_global_refs_ARCH [Finalise_AI_assms]: "interrupt_irq_node s irq \ global_refs s" by (simp add: global_refs_def) -lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: +lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_assms]: "\invs\ get_irq_slot irq \cte_wp_at can_fast_finalise\" apply (simp add: get_irq_slot_def) apply wp @@ -1221,12 +1221,12 @@ lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: apply (clarsimp simp: cap_range_def) done -lemma (* replaceable_or_arch_update_same *) [Finalise_AI_asms]: +lemma (* replaceable_or_arch_update_same *) [Finalise_AI_assms]: "replaceable_or_arch_update s slot cap cap" by (clarsimp simp: replaceable_or_arch_update_def replaceable_def is_arch_update_def is_cap_simps) -lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: +lemma (* replace_cap_invs_arch_update *)[Finalise_AI_assms]: "\\s. cte_wp_at (replaceable_or_arch_update s p cap) p s \ invs s \ cap \ cap.NullCap @@ -1251,7 +1251,7 @@ lemma dmo_pred_tcb_at[wp]: apply (clarsimp simp: pred_tcb_at_def obj_at_def) done -lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: +lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_assms]: "do_machine_op mop \\s. P (tcb_cap_valid cap ptr s)\" apply (simp add: tcb_cap_valid_def no_cap_to_obj_with_diff_ref_def) apply (wp_pre, wps, rule hoare_vcg_prop) @@ -1269,7 +1269,7 @@ lemma dmo_reachable_target[wp]: apply simp done -lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_asms,wp]: +lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_assms,wp]: "\\s. replaceable_or_arch_update s slot cap cap'\ do_machine_op mo \\r s. replaceable_or_arch_update s slot cap cap'\" @@ -1290,7 +1290,7 @@ interpretation Finalise_AI_3?: Finalise_AI_3 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming RISCV64 @@ -1308,7 +1308,7 @@ interpretation Finalise_AI_4?: Finalise_AI_4 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming RISCV64 @@ -1347,9 +1347,9 @@ lemma arch_finalise_cap_valid_cap[wp]: global_naming Arch -lemmas clearMemory_invs[wp,Finalise_AI_asms] = clearMemory_invs +lemmas clearMemory_invs[wp,Finalise_AI_assms] = clearMemory_invs -lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: +lemma valid_idle_has_null_cap_ARCH[Finalise_AI_assms]: "\ if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; caps_of_state s (idle_thread s, v) = Some cap \ \ cap = NullCap" @@ -1365,7 +1365,7 @@ lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: apply (drule_tac x=word in spec, simp) done -lemma (* zombie_cap_two_nonidles *)[Finalise_AI_asms]: +lemma (* zombie_cap_two_nonidles *)[Finalise_AI_assms]: "\ caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s \ \ fst ptr \ idle_thread s \ ptr' \ idle_thread s" apply (frule valid_global_refsD2, clarsimp+) @@ -1391,7 +1391,7 @@ interpretation Finalise_AI_5?: Finalise_AI_5 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed end diff --git a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy index 62e1bc469d..818c7c6062 100644 --- a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy @@ -23,16 +23,16 @@ primrec arch_irq_control_inv_valid_real :: defs arch_irq_control_inv_valid_def: "arch_irq_control_inv_valid \ arch_irq_control_inv_valid_real" -named_theorems Interrupt_AI_asms +named_theorems Interrupt_AI_assms -lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]: +lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_assms]: "\P\ decode_irq_control_invocation label args slot caps \\rv. P\" apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def arch_decode_irq_control_invocation_def whenE_def, safe) apply (wp | simp)+ done -lemma decode_irq_control_valid [Interrupt_AI_asms]: +lemma decode_irq_control_valid [Interrupt_AI_assms]: "\\s. invs s \ (\cap \ set caps. s \ cap) \ (\cap \ set caps. is_cnode_cap cap \ (\r \ cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) @@ -54,7 +54,7 @@ lemma decode_irq_control_valid [Interrupt_AI_asms]: apply fast done -lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: +lemma get_irq_slot_different_ARCH[Interrupt_AI_assms]: "\\s. valid_global_refs s \ ex_cte_cap_wp_to is_cnode_cap ptr s\ get_irq_slot irq \\rv s. rv \ ptr\" @@ -66,7 +66,7 @@ lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def) done -lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: +lemma is_derived_use_interrupt_ARCH[Interrupt_AI_assms]: "(is_ntfn_cap cap \ interrupt_derived cap cap') \ (is_derived m p cap cap')" apply (clarsimp simp: is_cap_simps) apply (clarsimp simp: interrupt_derived_def is_derived_def) @@ -74,7 +74,7 @@ lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def) done -lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]: +lemma maskInterrupt_invs_ARCH[Interrupt_AI_assms]: "\invs and (\s. \b \ interrupt_states s irq \ IRQInactive)\ do_machine_op (maskInterrupt b irq) \\rv. invs\" @@ -94,13 +94,13 @@ lemma dmo_plic_complete_claim[wp]: apply (auto simp: plic_complete_claim_def machine_op_lift_def machine_rest_lift_def in_monad select_f_def) done -lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]: +lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_assms]: "no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \" by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state obj_ref_none_no_asid) -lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: +lemma (* set_irq_state_valid_cap *)[Interrupt_AI_assms]: "\valid_cap cap\ set_irq_state IRQSignal irq \\rv. valid_cap cap\" apply (clarsimp simp: set_irq_state_def) apply (wp do_machine_op_valid_cap) @@ -110,9 +110,9 @@ lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: done crunch set_irq_state - for valid_global_refs[Interrupt_AI_asms]: "valid_global_refs" + for valid_global_refs[Interrupt_AI_assms]: "valid_global_refs" -lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: +lemma invoke_irq_handler_invs'[Interrupt_AI_assms]: assumes dmo_ex_inv[wp]: "\f. \invs and ex_inv\ do_machine_op f \\rv::unit. ex_inv\" assumes cap_insert_ex_inv[wp]: "\cap src dest. \ex_inv and invs and K (src \ dest)\ @@ -168,7 +168,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: done qed -lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: +lemma (* invoke_irq_control_invs *) [Interrupt_AI_assms]: "\invs and irq_control_inv_valid i\ invoke_irq_control i \\rv. invs\" apply (cases i, simp_all) apply (wp cap_insert_simple_invs @@ -192,7 +192,7 @@ lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: crunch resetTimer for device_state_inv[wp]: "\ms. P (device_state ms)" -lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: +lemma resetTimer_invs_ARCH[Interrupt_AI_assms]: "\invs\ do_machine_op resetTimer \\_. invs\" apply (wp dmo_invs) apply safe @@ -205,11 +205,11 @@ lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption) done -lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (ackInterrupt irq)" by (wp | simp add: ackInterrupt_def)+ -lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (maskInterrupt f irq)" by (wp | simp add: maskInterrupt_def)+ @@ -236,7 +236,7 @@ lemma handle_reserved_irq_invs[wp]: "\invs\ handle_reserved_irq irq \\_. invs\" unfolding handle_reserved_irq_def by (wpsimp simp: non_kernel_IRQs_def) -lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: +lemma (* handle_interrupt_invs *) [Interrupt_AI_assms]: "\invs\ handle_interrupt irq \\_. invs\" apply (simp add: handle_interrupt_def) apply (rule conjI; rule impI) @@ -253,7 +253,7 @@ lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: | rule conjI)+ done -lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_asms]: +lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_assms]: "\arch_irq_control_inv_valid i\ set_thread_state t st \\rv. arch_irq_control_inv_valid i\" @@ -270,7 +270,7 @@ end interpretation Interrupt_AI?: Interrupt_AI proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_assms)?) qed end diff --git a/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy b/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy index 84a5cdca86..d8d0f9b2c7 100644 --- a/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchIpcCancel_AI.thy @@ -10,11 +10,11 @@ begin context Arch begin global_naming RISCV64 -named_theorems IpcCancel_AI_asms +named_theorems IpcCancel_AI_assms crunch arch_post_cap_deletion - for typ_at[wp, IpcCancel_AI_asms]: "\s. P (typ_at T p s)" - and idle_thread[wp, IpcCancel_AI_asms]: "\s. P (idle_thread s)" + for typ_at[wp, IpcCancel_AI_assms]: "\s. P (typ_at T p s)" + and idle_thread[wp, IpcCancel_AI_assms]: "\s. P (idle_thread s)" end @@ -22,7 +22,7 @@ interpretation IpcCancel_AI?: IpcCancel_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact IpcCancel_AI_asms)?) + by (intro_locales; (unfold_locales; fact IpcCancel_AI_assms)?) qed diff --git a/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy b/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy index 24d12b1b3f..d7e6e25eb2 100644 --- a/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy @@ -10,9 +10,9 @@ begin context Arch begin global_naming RISCV64 -named_theorems Schedule_AI_asms +named_theorems Schedule_AI_assms -lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: +lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_assms]: "do_machine_op (mapM (\p. storeWord p 0) S) \invs\" apply (simp add: dom_mapM ef_storeWord) apply (rule mapM_UNIV_wp) @@ -29,19 +29,19 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: global_naming Arch -lemma arch_stt_invs [wp,Schedule_AI_asms]: +lemma arch_stt_invs [wp,Schedule_AI_assms]: "\invs\ arch_switch_to_thread t' \\_. invs\" apply (simp add: arch_switch_to_thread_def) apply wp done -lemma arch_stt_tcb [wp,Schedule_AI_asms]: +lemma arch_stt_tcb [wp,Schedule_AI_assms]: "\tcb_at t'\ arch_switch_to_thread t' \\_. tcb_at t'\" apply (simp add: arch_switch_to_thread_def) apply (wp) done -lemma arch_stt_runnable[Schedule_AI_asms]: +lemma arch_stt_runnable[Schedule_AI_assms]: "\st_tcb_at runnable t\ arch_switch_to_thread t \\r . st_tcb_at runnable t\" apply (simp add: arch_switch_to_thread_def) apply wp @@ -52,7 +52,7 @@ lemma idle_strg: by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def) -lemma arch_stit_invs[wp, Schedule_AI_asms]: +lemma arch_stit_invs[wp, Schedule_AI_assms]: "\invs\ arch_switch_to_idle_thread \\r. invs\" by (wpsimp simp: arch_switch_to_idle_thread_def) @@ -67,19 +67,19 @@ crunch set_vm_root and it[wp]: "\s. P (idle_thread s)" (simp: crunch_simps wp: hoare_drop_imps) -lemma arch_stit_activatable[wp, Schedule_AI_asms]: +lemma arch_stit_activatable[wp, Schedule_AI_assms]: "\ct_in_state activatable\ arch_switch_to_idle_thread \\rv . ct_in_state activatable\" apply (clarsimp simp: arch_switch_to_idle_thread_def) apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift) done -lemma stit_invs [wp,Schedule_AI_asms]: +lemma stit_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv. invs\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wpsimp|strengthen idle_strg)+ done -lemma stit_activatable[Schedule_AI_asms]: +lemma stit_activatable[Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv . ct_in_state activatable\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wp | simp add: ct_in_state_def)+ @@ -87,7 +87,7 @@ lemma stit_activatable[Schedule_AI_asms]: elim!: pred_tcb_weaken_strongerE) done -lemma stt_invs [wp,Schedule_AI_asms]: +lemma stt_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_thread t' \\_. invs\" apply (simp add: switch_to_thread_def) apply wp @@ -107,14 +107,14 @@ interpretation Schedule_AI_U?: Schedule_AI_U proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed interpretation Schedule_AI?: Schedule_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed end diff --git a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy index 3760f53e18..3e989e415f 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy @@ -10,17 +10,17 @@ begin context Arch begin global_naming RISCV64 -named_theorems Tcb_AI_asms +named_theorems Tcb_AI_assms -lemma activate_idle_invs[Tcb_AI_asms]: +lemma activate_idle_invs[Tcb_AI_assms]: "\invs and ct_idle\ arch_activate_idle_thread thread \\rv. invs and ct_idle\" by (simp add: arch_activate_idle_thread_def) -lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]: +lemma empty_fail_getRegister [intro!, simp, Tcb_AI_assms]: "empty_fail (getRegister r)" by (simp add: getRegister_def) @@ -37,7 +37,7 @@ lemma same_object_also_valid: (* arch specific *) split: cap.split_asm arch_cap.split_asm option.splits)+) done -lemma same_object_obj_refs[Tcb_AI_asms]: +lemma same_object_obj_refs[Tcb_AI_assms]: "\ same_object_as cap cap' \ \ obj_refs cap = obj_refs cap'" apply (cases cap, simp_all add: same_object_as_def) @@ -124,13 +124,13 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *) done crunch arch_get_sanitise_register_info, arch_post_modify_registers - for tcb_at[wp, Tcb_AI_asms]: "tcb_at a" + for tcb_at[wp, Tcb_AI_assms]: "tcb_at a" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for invs[wp, Tcb_AI_asms]: "invs" + for invs[wp, Tcb_AI_assms]: "invs" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for ex_nonz_cap_to[wp, Tcb_AI_asms]: "ex_nonz_cap_to a" + for ex_nonz_cap_to[wp, Tcb_AI_assms]: "ex_nonz_cap_to a" -lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: +lemma finalise_cap_not_cte_wp_at[Tcb_AI_assms]: assumes x: "P cap.NullCap" shows "\\s. \cp \ ran (caps_of_state s). P cp\ finalise_cap cap fin @@ -147,7 +147,7 @@ lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: done -lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: +lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_assms]: "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" by (simp add:free_index_update_def table_cap_ref_def split:cap.splits) @@ -158,7 +158,7 @@ global_interpretation Tcb_AI_1?: Tcb_AI_1 and is_cnode_or_valid_arch = is_cnode_or_valid_arch proof goal_cases interpret Arch . - case 1 show ?case by (unfold_locales; (fact Tcb_AI_asms)?) + case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?) qed context Arch begin global_naming RISVB64 @@ -177,7 +177,7 @@ lemma use_no_cap_to_obj_asid_strg: (* arch specific *) by (fastforce simp: table_cap_ref_def vspace_asid_def valid_cap_simps obj_at_def split: cap.splits arch_cap.splits option.splits prod.splits) -lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: +lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_assms]: "\no_cap_to_obj_dr_emp cap\ cap_delete slot \\rv. no_cap_to_obj_dr_emp cap\" @@ -211,7 +211,7 @@ lemma option_case_eq_None: "((case m of None \ None | Some (a,b) \ Some a) = None) = (m = None)" by (clarsimp split: option.splits) -lemma tc_invs[Tcb_AI_asms]: +lemma tc_invs[Tcb_AI_assms]: "\invs and tcb_at a and (case_option \ (valid_cap o fst) e) and (case_option \ (valid_cap o fst) f) @@ -289,7 +289,7 @@ lemma check_valid_ipc_buffer_inv: (* arch_specific *) apply (wp | simp add: if_apply_def2 split del: if_split | wpcw)+ done -lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: +lemma check_valid_ipc_buffer_wp[Tcb_AI_assms]: "\\(s::'state_ext::state_ext state). is_arch_cap cap \ is_cnode_or_valid_arch cap \ valid_ipc_buffer_cap cap vptr \ is_aligned vptr msg_align_bits @@ -305,7 +305,7 @@ lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: valid_ipc_buffer_cap_def) done -lemma derive_no_cap_asid[wp,Tcb_AI_asms]: +lemma derive_no_cap_asid[wp,Tcb_AI_assms]: "\(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\bool\ derive_cap slot cap \\rv. no_cap_to_obj_with_diff_ref rv S\,-" @@ -319,7 +319,7 @@ lemma derive_no_cap_asid[wp,Tcb_AI_asms]: done -lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: +lemma decode_set_ipc_inv[wp,Tcb_AI_assms]: "\P::'state_ext::state_ext state \ bool\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" apply (simp add: decode_set_ipc_buffer_def whenE_def split_def @@ -328,7 +328,7 @@ lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: apply simp done -lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_assms]: "no_cap_to_obj_with_diff_ref c S s \ no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" apply (case_tac "update_cap_data P x c = NullCap") @@ -345,7 +345,7 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: done -lemma update_cap_valid[Tcb_AI_asms]: +lemma update_cap_valid[Tcb_AI_assms]: "valid_cap cap (s::'state_ext::state_ext state) \ valid_cap (case capdata of None \ cap_rights_update rs cap @@ -389,7 +389,7 @@ global_interpretation Tcb_AI?: Tcb_AI where is_cnode_or_valid_arch = RISCV64.is_cnode_or_valid_arch proof goal_cases interpret Arch . - case 1 show ?case by (unfold_locales; (fact Tcb_AI_asms)?) + case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?) qed end diff --git a/proof/invariant-abstract/X64/ArchAInvsPre.thy b/proof/invariant-abstract/X64/ArchAInvsPre.thy index f345647dda..0c3249c888 100644 --- a/proof/invariant-abstract/X64/ArchAInvsPre.thy +++ b/proof/invariant-abstract/X64/ArchAInvsPre.thy @@ -179,9 +179,9 @@ lemma device_frame_in_device_region: by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def) global_naming Arch -named_theorems AInvsPre_asms +named_theorems AInvsPre_assms -lemma ptable_rights_imp_frame[AInvsPre_asms]: +lemma ptable_rights_imp_frame[AInvsPre_assms]: assumes "valid_state s" shows "ptable_rights t s x \ {} \ ptable_lift t s x = Some (addrFromPPtr y) \ @@ -223,7 +223,7 @@ end interpretation AInvsPre?: AInvsPre proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?) qed requalify_facts diff --git a/proof/invariant-abstract/X64/ArchDetype_AI.thy b/proof/invariant-abstract/X64/ArchDetype_AI.thy index 17a3f8a37b..b236706142 100644 --- a/proof/invariant-abstract/X64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetype_AI.thy @@ -10,16 +10,16 @@ begin context Arch begin global_naming X64 -named_theorems Detype_AI_asms +named_theorems Detype_AI_assms -lemma valid_globals_irq_node[Detype_AI_asms]: +lemma valid_globals_irq_node[Detype_AI_assms]: "\ valid_global_refs s; cte_wp_at ((=) cap) ptr s \ \ interrupt_irq_node s irq \ cap_range cap" apply (erule(1) valid_global_refsD) apply (simp add: global_refs_def) done -lemma caps_of_state_ko[Detype_AI_asms]: +lemma caps_of_state_ko[Detype_AI_assms]: "valid_cap cap s \ is_untyped_cap cap \ cap_range cap = {} \ @@ -33,7 +33,7 @@ lemma caps_of_state_ko[Detype_AI_asms]: split: option.splits if_splits)+ done -lemma mapM_x_storeWord[Detype_AI_asms]: +lemma mapM_x_storeWord[Detype_AI_assms]: (* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *) assumes al: "is_aligned ptr word_size_bits" shows "mapM_x (\x. storeWord (ptr + of_nat x * word_size) 0) [0..x. if x \ S then {} else state_hyp_refs_of s x)" by (rule ext, simp add: state_hyp_refs_of_def detype_def) -lemma valid_ioports_detype[Detype_AI_asms]: +lemma valid_ioports_detype[Detype_AI_assms]: "valid_ioports s \ valid_ioports (detype (untyped_range cap) s)" apply (clarsimp simp: valid_ioports_def all_ioports_issued_def ioports_no_overlap_def issued_ioports_def more_update.caps_of_state_update) apply (clarsimp simp: detype_def cap_ioports_def ran_def elim!: ranE split: if_splits cap.splits arch_cap.splits) @@ -121,7 +121,7 @@ interpretation Detype_AI?: Detype_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Detype_AI_asms)?) + by (intro_locales; (unfold_locales; fact Detype_AI_assms)?) qed context detype_locale_arch begin diff --git a/proof/invariant-abstract/X64/ArchFinalise_AI.thy b/proof/invariant-abstract/X64/ArchFinalise_AI.thy index c0282a4598..989b824bb4 100644 --- a/proof/invariant-abstract/X64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/X64/ArchFinalise_AI.thy @@ -10,9 +10,9 @@ begin context Arch begin -named_theorems Finalise_AI_asms +named_theorems Finalise_AI_assms -lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_asms]: +lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_assms]: "(s \ ArchObjectCap cap \ aobj_ref cap = Some r) \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: valid_cap_def obj_at_def @@ -205,22 +205,22 @@ lemma unmap_page_tcb_cap_valid: global_naming Arch -lemma (* replaceable_cdt_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_cdt_update *)[simp,Finalise_AI_assms]: "replaceable (cdt_update f s) = replaceable s" by (fastforce simp: replaceable_def tcb_cap_valid_def) -lemma (* replaceable_revokable_update *)[simp,Finalise_AI_asms]: +lemma (* replaceable_revokable_update *)[simp,Finalise_AI_assms]: "replaceable (is_original_cap_update f s) = replaceable s" by (fastforce simp: replaceable_def is_final_cap'_def2 tcb_cap_valid_def) -lemma (* replaceable_more_update *) [simp,Finalise_AI_asms]: +lemma (* replaceable_more_update *) [simp,Finalise_AI_assms]: "replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'" by (simp add: replaceable_def) -lemma (* obj_ref_ofI *) [Finalise_AI_asms]: "obj_refs cap = {x} \ obj_ref_of cap = x" +lemma (* obj_ref_ofI *) [Finalise_AI_assms]: "obj_refs cap = {x} \ obj_ref_of cap = x" by (case_tac cap, simp_all) (rename_tac arch_cap, case_tac arch_cap, simp_all) -lemma (* empty_slot_invs *) [Finalise_AI_asms]: +lemma (* empty_slot_invs *) [Finalise_AI_assms]: "\\s. invs s \ cte_wp_at (replaceable s sl cap.NullCap) sl s \ emptyable sl s \ (info \ NullCap \ post_cap_delete_pre info ((caps_of_state s) (sl \ NullCap)))\ @@ -301,7 +301,7 @@ lemma (* empty_slot_invs *) [Finalise_AI_asms]: apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state) done -lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: +lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_assms]: "dom tcb_cap_cases = {xs. length xs = 3 \ unat (of_bl xs :: machine_word) < 5}" apply (rule set_eqI, rule iffI) apply clarsimp @@ -311,7 +311,7 @@ lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]: apply (clarsimp simp: nat_to_cref_unat_of_bl'[simplified word_bits_def]) done -lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]: +lemma (* unbind_notification_final *) [wp,Finalise_AI_assms]: "\is_final_cap' cap\ unbind_notification t \ \rv. is_final_cap' cap\" unfolding unbind_notification_def apply (wp final_cap_lift thread_set_caps_of_state_trivial hoare_drop_imps @@ -321,7 +321,7 @@ lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]: crunch prepare_thread_delete for is_final_cap'[wp]: "is_final_cap' cap" -lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: +lemma (* finalise_cap_cases1 *)[Finalise_AI_assms]: "\\s. final \ is_final_cap' cap s \ cte_wp_at ((=) cap) slot s\ finalise_cap cap final @@ -353,7 +353,7 @@ lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: done crunch arch_finalise_cap, prepare_thread_delete - for typ_at_arch[wp,Finalise_AI_asms]: "\s. P (typ_at T p s)" + for typ_at_arch[wp,Finalise_AI_assms]: "\s. P (typ_at T p s)" (wp: crunch_wps simp: crunch_simps unless_def assertE_def ignore: maskInterrupt ) @@ -362,11 +362,11 @@ crunch prepare_thread_delete crunch prepare_thread_delete for tcb_at[wp]: "tcb_at p" crunch prepare_thread_delete - for cte_wp_at[wp, Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp, Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" crunch prepare_thread_delete - for irq_node[wp, Finalise_AI_asms]: "\s. P (interrupt_irq_node s)" + for irq_node[wp, Finalise_AI_assms]: "\s. P (interrupt_irq_node s)" crunch prepare_thread_delete - for caps_of_state[wp, Finalise_AI_asms]: "\s. P (caps_of_state s)" + for caps_of_state[wp, Finalise_AI_assms]: "\s. P (caps_of_state s)" crunch nativeThreadUsingFPU, switchFpuOwner for device_state_inv[wp]: "\ms. P (device_state ms)" @@ -395,7 +395,7 @@ crunch prepare_thread_delete for invs[wp]: invs (ignore: do_machine_op) -lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]: +lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_assms]: "\valid_cap cap\ finalise_cap cap x \\rv. valid_cap (fst rv)\" apply (cases cap, simp_all) apply (wp suspend_valid_cap @@ -409,7 +409,7 @@ lemma (* finalise_cap_new_valid_cap *)[wp,Finalise_AI_asms]: split del: if_split|clarsimp|wpc)+ done -lemma (* arch_finalise_cap_invs *)[wp,Finalise_AI_asms]: +lemma (* arch_finalise_cap_invs *)[wp,Finalise_AI_assms]: "\invs and valid_cap (ArchObjectCap cap)\ arch_finalise_cap cap final \\rv. invs\" @@ -461,7 +461,7 @@ lemma arch_finalise_cap_replaceable[wp]: done global_naming Arch -lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_assms]: "\if_unsafe_then_cap and valid_global_refs and cte_wp_at (\cp. cap_irqs cp \ {}) sl\ deleting_irq_handler irq @@ -482,7 +482,7 @@ lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]: apply (clarsimp simp: appropriate_cte_cap_def split: cap.split_asm) done -lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_assms]: "\ cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap \ \ no_cap_to_obj_with_diff_ref cap' {p} s" @@ -504,7 +504,7 @@ lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]: gen_obj_refs_Int) done -lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]: +lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_assms]: "\no_cap_to_obj_with_diff_ref cap S\ suspend t \\rv. no_cap_to_obj_with_diff_ref cap S\" @@ -535,13 +535,13 @@ crunch fpu_thread_delete for obj_at[wp]: "\s. P' (obj_at P p s)" (wp: whenE_wp simp: crunch_simps) -lemma (* fpu_thread_delete_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]: +lemma (* fpu_thread_delete_no_cap_to_obj_ref *)[wp,Finalise_AI_assms]: "\no_cap_to_obj_with_diff_ref cap S\ fpu_thread_delete thread \\rv. no_cap_to_obj_with_diff_ref cap S\" by (wpsimp simp: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state) -lemma finalise_cap_replaceable [Finalise_AI_asms]: +lemma finalise_cap_replaceable [Finalise_AI_assms]: "\\s. s \ cap \ x = is_final_cap' cap s \ valid_mdb s \ cte_wp_at ((=) cap) sl s \ valid_objs s \ sym_refs (state_refs_of s) \ (cap_irqs cap \ {} \ if_unsafe_then_cap s \ valid_global_refs s) @@ -594,7 +594,7 @@ lemma finalise_cap_replaceable [Finalise_AI_asms]: | simp add: valid_cap_simps is_nondevice_page_cap_simps)+) done -lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]: +lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_assms]: assumes x: "\cap. P cap \ \ can_fast_finalise cap" shows "\cte_wp_at P p\ deleting_irq_handler irq \\rv. cte_wp_at P p\" apply (simp add: deleting_irq_handler_def) @@ -613,7 +613,7 @@ lemma set_asid_pool_cte_wp_at: crunch arch_finalise_cap - for cte_wp_at[wp,Finalise_AI_asms]: "\s. P (cte_wp_at P' p s)" + for cte_wp_at[wp,Finalise_AI_assms]: "\s. P (cte_wp_at P' p s)" (simp: crunch_simps assertE_def set_arch_obj_simps wp: set_aobject_cte_wp_at crunch_wps set_object_cte_at ignore: set_object) @@ -623,7 +623,7 @@ end interpretation Finalise_AI_1?: Finalise_AI_1 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming X64 @@ -648,7 +648,7 @@ lemma fast_finalise_replaceable[wp]: done global_naming Arch -lemma (* cap_delete_one_invs *) [Finalise_AI_asms,wp]: +lemma (* cap_delete_one_invs *) [Finalise_AI_assms,wp]: "\invs and emptyable ptr\ cap_delete_one ptr \\rv. invs\" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (rule hoare_pre) @@ -662,7 +662,7 @@ end interpretation Finalise_AI_2?: Finalise_AI_2 proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming X64 @@ -1254,7 +1254,7 @@ crunch do_machine_op global_naming Arch -lemma (* finalise_cap_invs *)[Finalise_AI_asms]: +lemma (* finalise_cap_invs *)[Finalise_AI_assms]: shows "\invs and cte_wp_at ((=) cap) slot\ finalise_cap cap x \\rv. invs\" apply (cases cap, simp_all split del: if_split) apply (wp cancel_all_ipc_invs cancel_all_signals_invs unbind_notification_invs @@ -1271,16 +1271,16 @@ lemma (* finalise_cap_invs *)[Finalise_AI_asms]: apply (auto dest: cte_wp_at_valid_objs_valid_cap) done -lemma (* finalise_cap_irq_node *)[Finalise_AI_asms]: +lemma (* finalise_cap_irq_node *)[Finalise_AI_assms]: "\\s. P (interrupt_irq_node s)\ finalise_cap a b \\_ s. P (interrupt_irq_node s)\" apply (case_tac a,simp_all) apply (wp | clarsimp)+ done -lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_asms] +lemmas (*arch_finalise_cte_irq_node *) [wp,Finalise_AI_assms] = hoare_use_eq_irq_node [OF arch_finalise_cap_irq_node arch_finalise_cap_cte_wp_at] -lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: +lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_assms]: "\st_tcb_at P t and K (\st. simple st \ P st)\ deleting_irq_handler irq \\rv. st_tcb_at P t\" @@ -1289,11 +1289,11 @@ lemma (* deleting_irq_handler_st_tcb_at *) [Finalise_AI_asms]: apply simp done -lemma irq_node_global_refs_ARCH [Finalise_AI_asms]: +lemma irq_node_global_refs_ARCH [Finalise_AI_assms]: "interrupt_irq_node s irq \ global_refs s" by (simp add: global_refs_def) -lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: +lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_assms]: "\invs\ get_irq_slot irq \cte_wp_at can_fast_finalise\" apply (simp add: get_irq_slot_def) apply wp @@ -1315,12 +1315,12 @@ lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]: apply (clarsimp simp: cap_range_def) done -lemma (* replaceable_or_arch_update_same *) [Finalise_AI_asms]: +lemma (* replaceable_or_arch_update_same *) [Finalise_AI_assms]: "replaceable_or_arch_update s slot cap cap" by (clarsimp simp: replaceable_or_arch_update_def replaceable_def is_arch_update_def is_cap_simps) -lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: +lemma (* replace_cap_invs_arch_update *)[Finalise_AI_assms]: "\\s. cte_wp_at (replaceable_or_arch_update s p cap) p s \ invs s \ cap \ cap.NullCap @@ -1341,7 +1341,7 @@ lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: crunch hw_asid_invalidate for pred_tcb_at_P[wp]: "\s. P (pred_tcb_at proj Q p s)" -lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: +lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_assms]: "\\s. P (tcb_cap_valid cap ptr s)\ do_machine_op mop \\_ s. P (tcb_cap_valid cap ptr s)\" apply (simp add: tcb_cap_valid_def no_cap_to_obj_with_diff_ref_def) apply (rule hoare_pre) @@ -1350,7 +1350,7 @@ lemma dmo_tcb_cap_valid_ARCH [Finalise_AI_asms]: apply simp done -lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_asms,wp]: +lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_assms,wp]: "\\s. replaceable_or_arch_update s slot cap cap'\ do_machine_op mo \\r s. replaceable_or_arch_update s slot cap cap'\" @@ -1372,14 +1372,14 @@ interpretation Finalise_AI_3?: Finalise_AI_3 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed interpretation Finalise_AI_4?: Finalise_AI_4 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed context Arch begin global_naming X64 @@ -1617,9 +1617,9 @@ crunch unmap_page_table, (wp: mapM_wp_inv mapM_x_wp' crunch_wps simp: crunch_simps set_arch_obj_simps ignore: set_object) -lemmas clearMemory_invs[wp, Finalise_AI_asms] = clearMemory_invs +lemmas clearMemory_invs[wp, Finalise_AI_assms] = clearMemory_invs -lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: +lemma valid_idle_has_null_cap_ARCH[Finalise_AI_assms]: "\ if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s\ \ caps_of_state s (idle_thread s, v) = Some cap \ cap = NullCap" @@ -1635,7 +1635,7 @@ lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]: apply (drule_tac x=word in spec, simp) done -lemma (* zombie_cap_two_nonidles *)[Finalise_AI_asms]: +lemma (* zombie_cap_two_nonidles *)[Finalise_AI_assms]: "\ caps_of_state s ptr = Some (Zombie ptr' zbits n); invs s \ \ fst ptr \ idle_thread s \ ptr' \ idle_thread s" apply (frule valid_global_refsD2, clarsimp+) @@ -1684,7 +1684,7 @@ interpretation Finalise_AI_5?: Finalise_AI_5 where replaceable_or_arch_update = replaceable_or_arch_update proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed end diff --git a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy index 25468596be..2572c3e91d 100644 --- a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy @@ -32,9 +32,9 @@ where defs arch_irq_control_inv_valid_def: "arch_irq_control_inv_valid \ arch_irq_control_inv_valid_real" -named_theorems Interrupt_AI_asms +named_theorems Interrupt_AI_assms -lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]: +lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_assms]: "\P\ decode_irq_control_invocation label args slot caps \\rv. P\" apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def arch_decode_irq_control_invocation_def whenE_def split del: if_split) @@ -129,7 +129,7 @@ lemma arch_decode_irq_control_valid[wp]: done end -lemma (* decode_irq_control_valid *)[Interrupt_AI_asms]: +lemma (* decode_irq_control_valid *)[Interrupt_AI_assms]: "\\s. invs s \ (\cap \ set caps. s \ cap) \ (\cap \ set caps. is_cnode_cap cap \ (\r \ cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) @@ -144,7 +144,7 @@ lemma (* decode_irq_control_valid *)[Interrupt_AI_asms]: | wp (once) hoare_drop_imps)+ done -lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: +lemma get_irq_slot_different_ARCH[Interrupt_AI_assms]: "\\s. valid_global_refs s \ ex_cte_cap_wp_to is_cnode_cap ptr s\ get_irq_slot irq \\rv s. rv \ ptr\" @@ -156,7 +156,7 @@ lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]: apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def) done -lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: +lemma is_derived_use_interrupt_ARCH[Interrupt_AI_assms]: "(is_ntfn_cap cap \ interrupt_derived cap cap') \ (is_derived m p cap cap')" apply (clarsimp simp: is_cap_simps) apply (clarsimp simp: interrupt_derived_def is_derived_def) @@ -164,7 +164,7 @@ lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]: apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def) done -lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]: +lemma maskInterrupt_invs_ARCH[Interrupt_AI_assms]: "\invs and (\s. \b \ interrupt_states s irq \ IRQInactive)\ do_machine_op (maskInterrupt b irq) \\rv. invs\" @@ -174,7 +174,7 @@ lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]: valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def) done -lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]: +lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_assms]: "no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \" by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state @@ -183,7 +183,7 @@ lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]: crunch do_machine_op for valid_cap: "valid_cap cap" -lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: +lemma (* set_irq_state_valid_cap *)[Interrupt_AI_assms]: "\valid_cap cap\ set_irq_state IRQSignal irq \\rv. valid_cap cap\" apply (clarsimp simp: set_irq_state_def) apply (wp do_machine_op_valid_cap) @@ -193,12 +193,12 @@ lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: done crunch set_irq_state - for valid_global_refs[Interrupt_AI_asms]: "valid_global_refs" + for valid_global_refs[Interrupt_AI_assms]: "valid_global_refs" crunch arch_invoke_irq_handler for typ_at[wp]: "\s. P (typ_at T p s)" -lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: +lemma invoke_irq_handler_invs'[Interrupt_AI_assms]: assumes dmo_ex_inv[wp]: "\f. \invs and ex_inv\ do_machine_op f \\rv::unit. ex_inv\" assumes cap_insert_ex_inv[wp]: "\cap src dest. \ex_inv and invs and K (src \ dest)\ @@ -314,7 +314,7 @@ lemma arch_invoke_irq_control_invs[wp]: maxUserIRQ_def maxIRQ_def order.trans ex_cte_cap_to_cnode_always_appropriate_strg) -lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: +lemma (* invoke_irq_control_invs *) [Interrupt_AI_assms]: "\invs and irq_control_inv_valid i\ invoke_irq_control i \\rv. invs\" apply (cases i, simp_all) apply (rule hoare_pre) @@ -331,7 +331,7 @@ lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]: crunch resetTimer for device_state_inv[wp]: "\ms. P (device_state ms)" -lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: +lemma resetTimer_invs_ARCH[Interrupt_AI_assms]: "\invs\ do_machine_op resetTimer \\_. invs\" apply (wp dmo_invs) apply safe @@ -344,15 +344,15 @@ lemma resetTimer_invs_ARCH[Interrupt_AI_asms]: apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption) done -lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (ackInterrupt irq)" by (wp | simp add: ackInterrupt_def)+ -lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]: +lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_assms]: "empty_fail (maskInterrupt f irq)" by (wp | simp add: maskInterrupt_def)+ -lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: +lemma (* handle_interrupt_invs *) [Interrupt_AI_assms]: "\invs\ handle_interrupt irq \\_. invs\" apply (simp add: handle_interrupt_def ) apply (rule conjI; rule impI) @@ -367,7 +367,7 @@ lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]: apply (wp hoare_drop_imps resetTimer_invs_ARCH | simp add: get_irq_state_def handle_reserved_irq_def)+ done -lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_asms]: +lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_assms]: "\arch_irq_control_inv_valid i\ set_thread_state t st \\rv. arch_irq_control_inv_valid i\" @@ -387,7 +387,7 @@ end interpretation Interrupt_AI?: Interrupt_AI proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_assms)?) qed end diff --git a/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy b/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy index a9a291e562..dff61cc619 100644 --- a/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/X64/ArchIpcCancel_AI.thy @@ -10,26 +10,26 @@ begin context Arch begin global_naming X64 -named_theorems IpcCancel_AI_asms +named_theorems IpcCancel_AI_assms crunch set_endpoint - for v_ker_map[wp,IpcCancel_AI_asms]: "valid_kernel_mappings" + for v_ker_map[wp,IpcCancel_AI_assms]: "valid_kernel_mappings" (ignore: set_object wp: set_object_v_ker_map crunch_wps) crunch set_endpoint - for eq_ker_map[wp,IpcCancel_AI_asms]: "equal_kernel_mappings" + for eq_ker_map[wp,IpcCancel_AI_assms]: "equal_kernel_mappings" (ignore: set_object wp: set_object_equal_mappings crunch_wps) crunch arch_post_cap_deletion - for typ_at[wp, IpcCancel_AI_asms]: "\s. P (typ_at T p s)" - and idle_thread[wp, IpcCancel_AI_asms]: "\s. P (idle_thread s)" + for typ_at[wp, IpcCancel_AI_assms]: "\s. P (typ_at T p s)" + and idle_thread[wp, IpcCancel_AI_assms]: "\s. P (idle_thread s)" end interpretation IpcCancel_AI?: IpcCancel_AI proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales; fact IpcCancel_AI_asms)?) + case 1 show ?case by (intro_locales; (unfold_locales; fact IpcCancel_AI_assms)?) qed end diff --git a/proof/invariant-abstract/X64/ArchSchedule_AI.thy b/proof/invariant-abstract/X64/ArchSchedule_AI.thy index 09ba73456b..29e13fc0c8 100644 --- a/proof/invariant-abstract/X64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/X64/ArchSchedule_AI.thy @@ -10,9 +10,9 @@ begin context Arch begin global_naming X64 -named_theorems Schedule_AI_asms +named_theorems Schedule_AI_assms -lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: +lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_assms]: "valid invs (do_machine_op (mapM (\p. storeWord p 0) S)) (\_. invs)" apply (simp add: dom_mapM ef_storeWord) apply (rule mapM_UNIV_wp) @@ -30,25 +30,25 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: global_naming Arch -lemma arch_stt_invs [wp,Schedule_AI_asms]: +lemma arch_stt_invs [wp,Schedule_AI_assms]: "\invs\ arch_switch_to_thread t' \\_. invs\" apply (simp add: arch_switch_to_thread_def) apply wp done -lemma arch_stt_tcb [wp,Schedule_AI_asms]: +lemma arch_stt_tcb [wp,Schedule_AI_assms]: "\tcb_at t'\ arch_switch_to_thread t' \\_. tcb_at t'\" apply (simp add: arch_switch_to_thread_def) apply (wp) done -lemma arch_stt_runnable[Schedule_AI_asms]: +lemma arch_stt_runnable[Schedule_AI_assms]: "\st_tcb_at runnable t\ arch_switch_to_thread t \\r . st_tcb_at runnable t\" apply (simp add: arch_switch_to_thread_def) apply wp done -lemma arch_stit_invs[wp, Schedule_AI_asms]: +lemma arch_stit_invs[wp, Schedule_AI_assms]: "\invs\ arch_switch_to_idle_thread \\r. invs\" by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def) @@ -66,20 +66,20 @@ crunch set_vm_root for ct[wp]: "\s. P (cur_thread s)" (wp: crunch_wps simp: crunch_simps) -lemma arch_stit_activatable[wp, Schedule_AI_asms]: +lemma arch_stit_activatable[wp, Schedule_AI_assms]: "\ct_in_state activatable\ arch_switch_to_idle_thread \\rv . ct_in_state activatable\" apply (clarsimp simp: arch_switch_to_idle_thread_def) apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift) done -lemma stit_invs [wp,Schedule_AI_asms]: +lemma stit_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv. invs\" apply (simp add: switch_to_idle_thread_def) apply (wp sct_invs) apply (clarsimp simp: invs_def valid_state_def valid_idle_def pred_tcb_at_tcb_at) done -lemma stit_activatable[Schedule_AI_asms]: +lemma stit_activatable[Schedule_AI_assms]: "\invs\ switch_to_idle_thread \\rv . ct_in_state activatable\" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wp | simp add: ct_in_state_def)+ @@ -87,7 +87,7 @@ lemma stit_activatable[Schedule_AI_asms]: elim!: pred_tcb_weaken_strongerE) done -lemma stt_invs [wp,Schedule_AI_asms]: +lemma stt_invs [wp,Schedule_AI_assms]: "\invs\ switch_to_thread t' \\_. invs\" apply (simp add: switch_to_thread_def) apply wp @@ -107,14 +107,14 @@ interpretation Schedule_AI_U?: Schedule_AI_U proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed interpretation Schedule_AI?: Schedule_AI proof goal_cases interpret Arch . case 1 show ?case - by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) + by (intro_locales; (unfold_locales; fact Schedule_AI_assms)?) qed end diff --git a/proof/invariant-abstract/X64/ArchTcb_AI.thy b/proof/invariant-abstract/X64/ArchTcb_AI.thy index f1b0533036..947de34676 100644 --- a/proof/invariant-abstract/X64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/X64/ArchTcb_AI.thy @@ -10,17 +10,17 @@ begin context Arch begin global_naming X64 -named_theorems Tcb_AI_asms +named_theorems Tcb_AI_assms -lemma activate_idle_invs[Tcb_AI_asms]: +lemma activate_idle_invs[Tcb_AI_assms]: "\invs and ct_idle\ arch_activate_idle_thread thread \\rv. invs and ct_idle\" by (simp add: arch_activate_idle_thread_def) -lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]: +lemma empty_fail_getRegister [intro!, simp, Tcb_AI_assms]: "empty_fail (getRegister r)" by (simp add: getRegister_def) @@ -37,7 +37,7 @@ lemma same_object_also_valid: (* arch specific *) split: cap.split_asm arch_cap.split_asm option.splits)+) done -lemma same_object_obj_refs[Tcb_AI_asms]: +lemma same_object_obj_refs[Tcb_AI_assms]: "\ same_object_as cap cap' \ \ obj_refs cap = obj_refs cap'" apply (cases cap, simp_all add: same_object_as_def) @@ -141,13 +141,13 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *) done crunch arch_get_sanitise_register_info, arch_post_modify_registers - for tcb_at[wp, Tcb_AI_asms]: "tcb_at a" + for tcb_at[wp, Tcb_AI_assms]: "tcb_at a" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for invs[wp, Tcb_AI_asms]: "invs" + for invs[wp, Tcb_AI_assms]: "invs" crunch arch_get_sanitise_register_info, arch_post_modify_registers - for ex_nonz_cap_to[wp, Tcb_AI_asms]: "ex_nonz_cap_to a" + for ex_nonz_cap_to[wp, Tcb_AI_assms]: "ex_nonz_cap_to a" -lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: +lemma finalise_cap_not_cte_wp_at[Tcb_AI_assms]: assumes x: "P cap.NullCap" shows "\\s. \cp \ ran (caps_of_state s). P cp\ finalise_cap cap fin @@ -164,7 +164,7 @@ lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: done -lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: +lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_assms]: "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" by (simp add:free_index_update_def table_cap_ref_def split:cap.splits) @@ -175,7 +175,7 @@ global_interpretation Tcb_AI_1?: Tcb_AI_1 and is_cnode_or_valid_arch = is_cnode_or_valid_arch proof goal_cases interpret Arch . - case 1 show ?case by (unfold_locales; (fact Tcb_AI_asms)?) + case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?) qed context Arch begin global_naming X64 @@ -194,7 +194,7 @@ lemma use_no_cap_to_obj_asid_strg: (* arch specific *) apply (fastforce simp: table_cap_ref_def valid_cap_simps wellformed_mapdata_def elim!: asid_low_high_bits)+ done -lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: +lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_assms]: "\no_cap_to_obj_dr_emp cap\ cap_delete slot \\rv. no_cap_to_obj_dr_emp cap\" @@ -207,7 +207,7 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: | rule obj_ref_none_no_asid)+ done -lemma tc_invs[Tcb_AI_asms]: +lemma tc_invs[Tcb_AI_assms]: "\invs and tcb_at a and (case_option \ (valid_cap o fst) e) and (case_option \ (valid_cap o fst) f) @@ -286,7 +286,7 @@ lemma check_valid_ipc_buffer_inv: (* arch_specific *) apply (wp | simp add: if_apply_def2 split del: if_split | wpcw)+ done -lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: +lemma check_valid_ipc_buffer_wp[Tcb_AI_assms]: "\\(s::'state_ext::state_ext state). is_arch_cap cap \ is_cnode_or_valid_arch cap \ valid_ipc_buffer_cap cap vptr \ is_aligned vptr msg_align_bits @@ -302,7 +302,7 @@ lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: valid_ipc_buffer_cap_def) done -lemma derive_no_cap_asid[wp,Tcb_AI_asms]: +lemma derive_no_cap_asid[wp,Tcb_AI_assms]: "\(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\bool\ derive_cap slot cap \\rv. no_cap_to_obj_with_diff_ref rv S\,-" @@ -316,7 +316,7 @@ lemma derive_no_cap_asid[wp,Tcb_AI_asms]: done -lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: +lemma decode_set_ipc_inv[wp,Tcb_AI_assms]: "\P::'state_ext::state_ext state \ bool\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" apply (simp add: decode_set_ipc_buffer_def whenE_def split_def @@ -325,7 +325,7 @@ lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: apply simp done -lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: +lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_assms]: "no_cap_to_obj_with_diff_ref c S s \ no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" apply (case_tac "update_cap_data P x c = NullCap") @@ -342,7 +342,7 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: done -lemma update_cap_valid[Tcb_AI_asms]: +lemma update_cap_valid[Tcb_AI_assms]: "valid_cap cap (s::'state_ext::state_ext state) \ valid_cap (case capdata of None \ cap_rights_update rs cap @@ -386,7 +386,7 @@ global_interpretation Tcb_AI?: Tcb_AI where is_cnode_or_valid_arch = X64.is_cnode_or_valid_arch proof goal_cases interpret Arch . - case 1 show ?case by (unfold_locales; (fact Tcb_AI_asms)?) + case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?) qed end