secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

lib+spec+proof+autocorres: consistent Nondet filename prefix 

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2023-07-18 14:09:17 +10:00 committed by Corey Lewis
parent 9b9e613c57
commit 2c8f9eeff1
131 changed files with 238 additions and 238 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/BCorres_UL.thy
View File

@ -6,7 +6,7 @@
theory BCorres_UL
imports
Monads.NonDetMonadVCG
Monads.Nondet_VCG
Crunch_Instances_NonDet
begin

4
lib/Bisim_UL.thy
View File

@ -8,9 +8,9 @@
theory Bisim_UL
imports
Monads.NonDetMonadVCG
Monads.Nondet_VCG
Corres_UL
Monads.Empty_Fail
Monads.Nondet_Empty_Fail
begin
(* This still looks a bit wrong to me, although it is more or less what I want \<emdash> we want to be

4
lib/Corres_UL.thy
View File

@ -1284,7 +1284,7 @@ lemma corres_underlying_assert_assert:
lemma corres_underlying_stateAssert_stateAssert:
assumes "\<And>s s'. \<lbrakk> (s,s') \<in> rf_sr; P s; P' s' \<rbrakk> \<Longrightarrow> Q' s' = Q s"
shows "corres_underlying rf_sr nf False dc P P' (stateAssert Q []) (stateAssert Q' [])"
by (auto simp: stateAssert_def get_def NonDetMonad.bind_def corres_underlying_def
by (auto simp: stateAssert_def get_def Nondet_Monad.bind_def corres_underlying_def
assert_def return_def fail_def assms)
(* We can ignore a stateAssert in the middle of a computation even if we don't ignore abstract
@ -1294,7 +1294,7 @@ lemma corres_stateAssert_no_fail:
corres_underlying S False nf' r P Q (do v \<leftarrow> g; h v od) f \<rbrakk> \<Longrightarrow>
corres_underlying S False nf' r P Q (do v \<leftarrow> g; _ \<leftarrow> stateAssert X []; h v od) f"
apply (simp add: corres_underlying_def stateAssert_def get_def assert_def return_def no_fail_def fail_def cong: if_cong)
apply (clarsimp simp: split_def NonDetMonad.bind_def split: if_splits)
apply (clarsimp simp: split_def Nondet_Monad.bind_def split: if_splits)
apply (erule allE, erule (1) impE)
apply (drule (1) bspec, clarsimp)+
done

4
lib/Crunch_Instances_NonDet.thy
View File

@ -8,8 +8,8 @@ theory Crunch_Instances_NonDet
imports
Crunch
Monads.WPEx
Monads.Empty_Fail
Monads.No_Fail
Monads.Nondet_Empty_Fail
Monads.Nondet_No_Fail
begin
lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE

4
lib/CutMon.thy
View File

@ -10,8 +10,8 @@
theory CutMon
imports
Monads.Empty_Fail
Monads.NonDetMonadVCG
Monads.Nondet_Empty_Fail
Monads.Nondet_VCG
begin
definition

2
lib/EVTutorial/EquivValidTutorial.thy
View File

@ -55,7 +55,7 @@ In this sense, EquivValid statements could be thought of as \<^emph>\<open>relat
text \<open> This tutorial will introduce some syntactic sugar to emphasise the similarity
between Hoare triples and EquivValid statements.
(Here, \<open>\<top>\<top>\<close> is an alias provided by Monads.NonDetMonad for the trivial binary predicate,
(Here, \<open>\<top>\<top>\<close> is an alias provided by Monads.Nondet\_Monad for the trivial binary predicate,
which always returns \<open>True\<close>; similarly, there is also \<open>\<bottom>\<bottom>\<close> for \<open>False\<close>.) \<close>
abbreviation

4
lib/HaskellLib_H.thy
View File

@ -13,7 +13,7 @@ theory HaskellLib_H
imports
Lib
More_Numeral_Type
Monads.NonDetMonadVCG
Monads.Nondet_VCG
Monads.Reader_Option_Monad
begin
@ -21,7 +21,7 @@ abbreviation (input) "flip \<equiv> swp"
abbreviation(input) bind_drop :: "('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad
\<Rightarrow> ('a, 'b) nondet_monad" (infixl ">>'_" 60)
where "bind_drop \<equiv> (\<lambda>x y. NonDetMonad.bind x (K_bind y))"
where "bind_drop \<equiv> (\<lambda>x y. Nondet_Monad.bind x (K_bind y))"
lemma bind_drop_test:
"foldr bind_drop x (return ()) = sequence_x x"

2
lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy
View File

@ -6,7 +6,7 @@
theory Hoare_Sep_Tactics
imports
Monads.NonDetMonadVCG
Monads.Nondet_VCG
Sep_Algebra.Sep_Algebra_L4v
begin

2
lib/Injection_Handler.thy
View File

@ -7,7 +7,7 @@
(* Definition of injection_handler and supporting lemmas. *)
theory Injection_Handler
imports Monads.NonDetMonadVCG
imports Monads.Nondet_VCG
begin
definition injection_handler ::

4
lib/Insulin.thy
View File

@ -34,11 +34,11 @@
*
* Another example (l4v libraries):
* > desugar_term "\<lbrace> P and Q \<rbrace> f \<lbrace> \<lambda>r _. r \<in> {0..<5} \<rbrace>!" "\<lbrace>"
* NonDetMonad_Total.validNF (P and Q) f (\<lambda>r _. r \<in> {0\<Colon>'b..<5\<Colon>'b})
* Nondet_Total.validNF (P and Q) f (\<lambda>r _. r \<in> {0\<Colon>'b..<5\<Colon>'b})
*
* Desugar multiple operators:
* > desugar_term "\<lbrace> P and Q \<rbrace> f \<lbrace> \<lambda>r _. r \<in> {0..<5} \<rbrace>!" "\<lbrace>" "and" ".."
* NonDetMonad.validNF (Lib.pred_conj P Q) f
* Nondet_Monad.validNF (Lib.pred_conj P Q) f
* (\<lambda>r _. r \<in> Set_Interval.ord_class.atLeastLessThan (0\<Colon>'b) (5\<Colon>'b))
*
*

2
lib/Monad_Commute.thy
View File

@ -9,7 +9,7 @@
theory Monad_Commute
imports
Monads.Monad_Equations
Monads.Nondet_Monad_Equations
Monad_Lists (* for mapM_x *)
begin

8
lib/Monad_Lists.thy
View File

@ -10,10 +10,10 @@
theory Monad_Lists
imports
Monads.In_Monad
Monads.Det
Monads.Empty_Fail
Monads.No_Fail
Monads.Nondet_In_Monad
Monads.Nondet_Det
Monads.Nondet_Empty_Fail
Monads.Nondet_No_Fail
begin
lemma mapME_Cons:

4
lib/MonadicRewrite.thy
View File

@ -9,9 +9,9 @@
theory MonadicRewrite
imports
Monads.NonDetMonadVCG
Monads.Nondet_VCG
Corres_UL
Monads.Empty_Fail
Monads.Nondet_Empty_Fail
Rules_Tac
begin

2
lib/Monads/Less_Monad_Syntax.thy
View File

@ -12,7 +12,7 @@ begin
no_syntax
"_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
(* remove input version of >>= from Monad_Syntax, avoid clash with NonDetMonad *)
(* remove input version of >>= from Monad_Syntax, avoid clash with Nondet_Monad *)
no_notation
Monad_Syntax.bind (infixl ">>=" 54)

2
lib/Monads/Monad_Lib.thy
View File

@ -5,7 +5,7 @@
*)
(* This theory collects the minimum constant definitions and lemmas for the monad definition
theories (NonDetMonad, TraceMonad etc). Only things that are necessary for these and needed
theories (Nondet_Monad, TraceMonad etc). Only things that are necessary for these and needed
by more than one of them should go in here. *)
theory Monad_Lib

2
lib/Monads/README.md
View File

@ -33,7 +33,7 @@ The directory [`wp/`](./wp/) contains proof methods to reason about these monads
in weakest-precondition style.
[l4v]: https://github.com/seL4/l4v/
[nondet]: ./nondet/NonDetMonad.thy
[nondet]: ./nondet/Nondet_Monad.thy
[option]: ./reader_option/Reader_Option_Monad.thy
[trace]: ./trace/TraceMonad.thy
[AutoCorres]: ../../tools/autocorres/

28
lib/Monads/ROOT
View File

@ -21,29 +21,29 @@ session Monads (lib) = HOL +
trace
theories
WhileLoopRules
Nondet_While_Loop_Rules
TraceMonad
Reader_Option_ND
Reader_Option_VCG
Strengthen_Demo
TraceMonadLemmas
Datatype_Schematic
WhileLoopRulesCompleteness
Nondet_While_Loop_Rules_Completeness
Strengthen
Strengthen_Setup
Nondet_Strengthen_Setup
Reader_Option_Monad
TraceMonadVCG
In_Monad
NonDetMonadVCG
NonDetMonad_Sat
More_NonDetMonadVCG
NonDetMonad
NonDetMonadLemmas
Det
No_Fail
No_Throw
Empty_Fail
Monad_Equations
Nondet_In_Monad
Nondet_VCG
Nondet_Sat
Nondet_More_VCG
Nondet_Monad
Nondet_Lemmas
Nondet_Det
Nondet_No_Fail
Nondet_No_Throw
Nondet_Empty_Fail
Nondet_Monad_Equations
"wp/WPBang"
"wp/WPFix"
"wp/Eisbach_WP"

4
lib/Monads/nondet/Det.thy → lib/Monads/nondet/Nondet_Det.thy
View File

@ -5,9 +5,9 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory Det
theory Nondet_Det
imports
NonDetMonad
Nondet_Monad
begin
subsection "Determinism"

6
lib/Monads/nondet/Empty_Fail.thy → lib/Monads/nondet/Nondet_Empty_Fail.thy
View File

@ -5,16 +5,16 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory Empty_Fail
theory Nondet_Empty_Fail
imports
NonDetMonad
Nondet_Monad
WPSimp
begin
section \<open>Monads that are wellformed w.r.t. failure\<close>
text \<open>
Usually, well-formed monads constructed from the primitives in NonDetMonad will have the following
Usually, well-formed monads constructed from the primitives in Nondet_Monad will have the following
property: if they return an empty set of results, they will have the failure flag set.\<close>
definition empty_fail :: "('s,'a) nondet_monad \<Rightarrow> bool" where
"empty_fail m \<equiv> \<forall>s. fst (m s) = {} \<longrightarrow> snd (m s)"

4
lib/Monads/nondet/In_Monad.thy → lib/Monads/nondet/Nondet_In_Monad.thy
View File

@ -5,8 +5,8 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory In_Monad
imports NonDetMonadLemmas
theory Nondet_In_Monad
imports Nondet_Lemmas
begin
section \<open>Reasoning directly about states\<close>

4
lib/Monads/nondet/NonDetMonadLemmas.thy → lib/Monads/nondet/Nondet_Lemmas.thy
View File

@ -5,8 +5,8 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory NonDetMonadLemmas
imports NonDetMonad
theory Nondet_Lemmas
imports Nondet_Monad
begin
section \<open>General Lemmas Regarding the Nondeterministic State Monad\<close>

2
lib/Monads/nondet/NonDetMonad.thy → lib/Monads/nondet/Nondet_Monad.thy
View File

@ -11,7 +11,7 @@
chapter "Nondeterministic State Monad with Failure"
theory NonDetMonad
theory Nondet_Monad
imports
Fun_Pred_Syntax
Monad_Lib

6
lib/Monads/nondet/MonadEq.thy → lib/Monads/nondet/Nondet_MonadEq.thy
View File

@ -19,10 +19,10 @@
*
* are added to the "monad_eq" set.
*)
theory MonadEq
theory Nondet_MonadEq
imports
In_Monad
NonDetMonadVCG
Nondet_In_Monad
Nondet_VCG
begin
(* Setup "monad_eq" attributes. *)

6
lib/Monads/nondet/MonadEq_Lemmas.thy → lib/Monads/nondet/Nondet_MonadEq_Lemmas.thy
View File

@ -11,10 +11,10 @@
If you are planning to use the monad_eq method, this is the theory you should import.
See MonadEq.thy for definition and description of the method. *)
See Nondet_MonadEq.thy for definition and description of the method. *)
theory MonadEq_Lemmas
imports MonadEq
theory Nondet_MonadEq_Lemmas
imports Nondet_MonadEq
begin
lemma snd_return[monad_eq]:

14
lib/Monads/nondet/Monad_Equations.thy → lib/Monads/nondet/Nondet_Monad_Equations.thy
View File

@ -8,11 +8,11 @@
(* Equations between monads. Conclusions of the form "f = g" where f and g are monads.
Should not be Hoare triples (those go into a different theory). *)
theory Monad_Equations
theory Nondet_Monad_Equations
imports
Empty_Fail
No_Fail
MonadEq_Lemmas
Nondet_Empty_Fail
Nondet_No_Fail
Nondet_MonadEq_Lemmas
begin
lemmas assertE_assert = assertE_liftE
@ -146,7 +146,7 @@ lemma unlessE_throw_catch_If:
lemma whenE_bindE_throwError_to_if:
"whenE P (throwError e) >>=E (\<lambda>_. b) = (if P then (throwError e) else b)"
unfolding whenE_def bindE_def
by (auto simp: NonDetMonad.lift_def throwError_def returnOk_def)
by (auto simp: Nondet_Monad.lift_def throwError_def returnOk_def)
lemma alternative_liftE_returnOk:
"(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)"
@ -431,7 +431,7 @@ lemma liftE_fail[simp]: "liftE fail = fail"
lemma catch_bind_distrib:
"do _ <- m <catch> h; f od = (doE m; liftE f odE <catch> (\<lambda>x. do h x; f od))"
by (force simp: catch_def bindE_def bind_assoc liftE_def NonDetMonad.lift_def bind_def
by (force simp: catch_def bindE_def bind_assoc liftE_def Nondet_Monad.lift_def bind_def
split_def return_def throwError_def
split: sum.splits)
@ -451,7 +451,7 @@ lemma catch_is_if:
od"
apply (simp add: bindE_def catch_def bind_assoc cong: if_cong)
apply (rule bind_cong, rule refl)
apply (clarsimp simp: NonDetMonad.lift_def throwError_def split: sum.splits)
apply (clarsimp simp: Nondet_Monad.lift_def throwError_def split: sum.splits)
done
lemma liftE_K_bind: "liftE ((K_bind (\<lambda>s. A s)) x) = K_bind (liftE (\<lambda>s. A s)) x"

4
lib/Monads/nondet/More_NonDetMonadVCG.thy → lib/Monads/nondet/Nondet_More_VCG.thy
View File

@ -8,9 +8,9 @@
(* Partial correctness Hoare logic lemmas over the nondet monad. Hoare triples, lifting lemmas, etc.
If it doesn't contain a Hoare triple it likely doesn't belong in here. *)
theory More_NonDetMonadVCG
theory Nondet_More_VCG
imports
NonDetMonadVCG
Nondet_VCG
begin
lemma hoare_take_disjunct:

6
lib/Monads/nondet/No_Fail.thy → lib/Monads/nondet/Nondet_No_Fail.thy
View File

@ -7,10 +7,10 @@
(* Lemmas about the no_fail predicate. *)
theory No_Fail
theory Nondet_No_Fail
imports
In_Monad
NonDetMonadVCG
Nondet_In_Monad
Nondet_VCG
WPSimp
begin

8
lib/Monads/nondet/No_Throw.thy → lib/Monads/nondet/Nondet_No_Throw.thy
View File

@ -8,10 +8,10 @@
(* Lemmas about no_throw. Usually should have a conclusion "no_throw P m".
Includes some monad equations that have no_throw as a main assumption. *)
theory No_Throw
theory Nondet_No_Throw
imports
WhileLoopRules
MonadEq_Lemmas
Nondet_While_Loop_Rules
Nondet_MonadEq_Lemmas
begin
section "Basic exception reasoning"
@ -73,7 +73,7 @@ lemma no_throw_fail[simp]:
lemma bindE_fail_propagates:
"\<lbrakk> no_throw \<top> A; empty_fail A \<rbrakk> \<Longrightarrow> A >>=E (\<lambda>_. fail) = fail"
by (fastforce simp: no_throw_def validE_def valid_def bind_def empty_fail_def
bindE_def split_def fail_def NonDetMonad.lift_def throwError_def
bindE_def split_def fail_def Nondet_Monad.lift_def throwError_def
split: sum.splits)
lemma whileLoopE_nothrow:

4
lib/Monads/nondet/NonDetMonad_Sat.thy → lib/Monads/nondet/Nondet_Sat.thy
View File

@ -5,9 +5,9 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory NonDetMonad_Sat
theory Nondet_Sat
imports
NonDetMonad
Nondet_Monad
WPSimp
begin

6
lib/Monads/nondet/Strengthen_Setup.thy → lib/Monads/nondet/Nondet_Strengthen_Setup.thy
View File

@ -5,11 +5,11 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory Strengthen_Setup
theory Nondet_Strengthen_Setup
imports
Strengthen
No_Fail
NonDetMonadVCG
Nondet_No_Fail
Nondet_VCG
begin
section \<open>Strengthen setup.\<close>

8
lib/Monads/nondet/NonDetMonad_Total.thy → lib/Monads/nondet/Nondet_Total.thy
View File

@ -5,13 +5,13 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
(* Total correctness Hoare logic for the NonDetMonad (= valid + no_fail) *)
(* Total correctness Hoare logic for the Nondet_Monad (= valid + no_fail) *)
theory NonDetMonad_Total
imports No_Fail
theory Nondet_Total
imports Nondet_No_Fail
begin
section \<open>Total correctness for NonDetMonad and NonDetMonad with exceptions\<close>
section \<open>Total correctness for Nondet_Monad and Nondet_Monad with exceptions\<close>
subsection Definitions

4
lib/Monads/nondet/NonDetMonadVCG.thy → lib/Monads/nondet/Nondet_VCG.thy
View File

@ -5,9 +5,9 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory NonDetMonadVCG
theory Nondet_VCG
imports
NonDetMonadLemmas
Nondet_Lemmas
WPSimp
begin

8
lib/Monads/nondet/WhileLoopRules.thy → lib/Monads/nondet/Nondet_While_Loop_Rules.thy
View File

@ -4,11 +4,11 @@
* SPDX-License-Identifier: BSD-2-Clause
*)
theory WhileLoopRules
theory Nondet_While_Loop_Rules
imports
Empty_Fail
NonDetMonad_Total
NonDetMonad_Sat
Nondet_Empty_Fail
Nondet_Total
Nondet_Sat
begin
section "Well-ordered measures"

6
lib/Monads/nondet/WhileLoopRulesCompleteness.thy → lib/Monads/nondet/Nondet_While_Loop_Rules_Completeness.thy
View File

@ -6,12 +6,12 @@
(*
* This is a purely theoretical theory containing proofs
* that the whileLoop rules in "WhileLoopRules" are complete.
* that the whileLoop rules in "Nondet_While_Loop_Rules" are complete.
*
* You probably don't care about this.
*)
theory WhileLoopRulesCompleteness
imports WhileLoopRules
theory Nondet_While_Loop_Rules_Completeness
imports Nondet_While_Loop_Rules
begin
lemma whileLoop_rule_strong_complete:

2
lib/Monads/reader_option/Reader_Option_Monad.thy
View File

@ -241,7 +241,7 @@ abbreviation ogets :: "('s \<Rightarrow> 'a) \<Rightarrow> ('s, 'a) lookup" wher
text \<open>
Integration with exception monad.
Corresponding bindE would be analogous to lifting in NonDetMonad.\<close>
Corresponding bindE would be analogous to lifting in Nondet_Monad.\<close>
definition
"oreturnOk x = K (Some (Inr x))"

4
lib/Monads/reader_option/Reader_Option_ND.thy
View File

@ -8,12 +8,12 @@
theory Reader_Option_ND
imports
NonDetMonadLemmas
Nondet_Lemmas
Reader_Option_Monad
begin
(* FIXME: remove this syntax, standardise on do {..} instead *)
(* Syntax defined here so we can reuse NonDetMonad definitions *)
(* Syntax defined here so we can reuse Nondet_Monad definitions *)
syntax
"_doO" :: "[dobinds, 'a] => 'a" ("(DO (_);// (_)//OD)" 100)

2
lib/Monads/reader_option/Reader_Option_VCG.thy
View File

@ -14,7 +14,7 @@ theory Reader_Option_VCG
imports
Reader_Option_ND
WP
No_Fail
Nondet_No_Fail
begin
(* Hoare triples.

2
lib/Monads/wp/Eisbach_WP.thy
View File

@ -9,7 +9,7 @@
theory Eisbach_WP
imports
Eisbach_Tools.Eisbach_Methods
NonDetMonadVCG
Nondet_VCG
Eisbach_Tools.Conjuncts
Eisbach_Tools.Rule_By_Method
WPI

2
lib/Monads/wp/WPBang.thy
View File

@ -8,7 +8,7 @@ theory WPBang
imports
WP
Eisbach_Tools.ProvePart
NonDetMonadVCG
Nondet_VCG
begin
lemma conj_meta_forward:

4
lib/Monads/wp/WPEx.thy
View File

@ -6,8 +6,8 @@
theory WPEx
imports
In_Monad
NonDetMonadVCG
Nondet_In_Monad
Nondet_VCG
Strengthen
begin

2
lib/Monads/wp/WPI.thy
View File

@ -33,7 +33,7 @@
theory WPI
imports
Eisbach_Tools.Eisbach_Methods
NonDetMonadLemmas
Nondet_Lemmas
WPEx
begin

10
lib/NonDetMonadLemmaBucket.thy
View File

@ -8,16 +8,16 @@
theory NonDetMonadLemmaBucket
imports
Lib
Monads.More_NonDetMonadVCG
Monads.Nondet_More_VCG
Monad_Lists
Monads.Monad_Equations
Monads.Nondet_Monad_Equations
Monad_Commute
Monads.No_Fail
Monads.No_Throw
Monads.Nondet_No_Fail
Monads.Nondet_No_Throw
CutMon
Oblivious
Injection_Handler
Monads.WhileLoopRulesCompleteness
Monads.Nondet_While_Loop_Rules_Completeness
"Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *)
Monads.Reader_Option_VCG
begin

4
lib/Oblivious.thy
View File

@ -12,8 +12,8 @@
theory Oblivious
imports
Monads.In_Monad
Monads.NonDetMonadVCG
Monads.Nondet_In_Monad
Monads.Nondet_VCG
begin

2
lib/SubMonadLib.thy
View File

@ -6,7 +6,7 @@
theory SubMonadLib
imports
Monads.Empty_Fail
Monads.Nondet_Empty_Fail
Corres_UL
begin

4
lib/clib/Corres_UL_C.thy
View File

@ -48,7 +48,7 @@ lemma exec_handlers_use_hoare_nothrow:
apply -
apply (drule hoare_sound)
apply (clarsimp elim: exec_Normal_elim_cases
simp: NonDetMonad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
simp: Nondet_Monad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
apply (erule exec_handlers.cases)
apply clarsimp
apply (drule spec, drule spec, drule (1) mp)
@ -1045,7 +1045,7 @@ lemma ccorres_liftM_simp [simp]:
apply (rule ccorresI')
apply simp
apply (erule (5) ccorresE)
apply (simp add: liftM_def NonDetMonad.bind_def return_def)
apply (simp add: liftM_def Nondet_Monad.bind_def return_def)
apply (erule bexI [rotated])
apply (simp add: unif_rrel_def split: if_split_asm)
done

2
lib/test/Crunch_Test_NonDet.thy
View File

@ -26,7 +26,7 @@ definition
crunch_foo1 13
od"
crunch_ignore (valid, empty_fail, no_fail) (add: NonDetMonad.bind)
crunch_ignore (valid, empty_fail, no_fail) (add: Nondet_Monad.bind)
crunch (empty_fail) empty_fail: crunch_foo2

2
lib/test/Match_Abbreviation_Test.thy
View File

@ -7,7 +7,7 @@ theory Match_Abbreviation_Test
imports
Lib.Match_Abbreviation
Monads.NonDetMonad
Monads.Nondet_Monad
begin
experiment

2
proof/capDL-api/Arch_DP.thy
View File

@ -25,7 +25,7 @@ lemma cdl_lookup_pt_slot_rv:
apply (rule validE_validE_R)
apply (clarsimp simp : cdl_lookup_pt_slot_def)
apply (clarsimp simp: validE_def valid_def bindE_def
bind_def bind_assoc NonDetMonad.lift_def)
bind_def bind_assoc Nondet_Monad.lift_def)
apply (case_tac a)
apply (clarsimp simp:liftE_def bindE_def bind_def return_def)
apply (clarsimp simp:liftE_def bindE_def bind_def return_def)

2
proof/capDL-api/ProofHelpers_DP.thy
View File

@ -11,7 +11,7 @@ imports
begin
crunch_ignore (add:
NonDetMonad.bind return "when" get gets fail
Nondet_Monad.bind return "when" get gets fail
assert put modify unless select
alternative assert_opt gets_the
returnOk throwError lift bindE

2
proof/crefine/ARM/ADT_C.thy
View File

@ -84,7 +84,7 @@ lemma setTCBContext_C_corres:
apply clarsimp
apply (frule getObject_eq [rotated -1], simp)
apply (simp add: objBits_simps')
apply (simp add: NonDetMonad.bind_def split_def)
apply (simp add: Nondet_Monad.bind_def split_def)
apply (rule bexI)
prefer 2
apply assumption

4
proof/crefine/ARM/Fastpath_Equiv.thy
View File

@ -1515,9 +1515,9 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
apply wp
apply (rule monadic_rewrite_trans)
apply (rule_tac rv=rab_ret
in monadic_rewrite_gets_known[where m="NonDetMonad.lift f"
in monadic_rewrite_gets_known[where m="Nondet_Monad.lift f"
for f, folded bindE_def])
apply (simp add: NonDetMonad.lift_def isRight_case_sum)
apply (simp add: Nondet_Monad.lift_def isRight_case_sum)
apply monadic_rewrite_symb_exec_l
apply (rename_tac ep_cap2)
apply (rule_tac P="cteCap ep_cap2 = cteCap ep_cap" in monadic_rewrite_gen_asm)

2
proof/crefine/ARM/IsolatedThreadAction.thy
View File

@ -915,7 +915,7 @@ lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
(is "NonDetMonadVCG.valid ?P ?f ?Q")
(is "Nondet_VCG.valid ?P ?f ?Q")
apply (simp add: setThreadState_def setSchedulerAction_def)
apply (wp hoare_pre_cont[where f=rescheduleRequired])
apply (rule_tac Q="\<lambda>_. ?P and st_tcb_at' ((=) st) t" in hoare_post_imp)

6
proof/crefine/ARM/Refine_C.thy
View File

@ -479,7 +479,7 @@ lemma ccorres_corres_u_xf:
apply (drule (1) bspec)
apply (clarsimp simp: exec_C_def no_fail_def)
apply (drule_tac x = a in spec)
apply (clarsimp simp:gets_def NonDetMonad.bind_def get_def return_def)
apply (clarsimp simp:gets_def Nondet_Monad.bind_def get_def return_def)
apply (rule conjI)
apply clarsimp
apply (erule_tac x=0 in allE)
@ -820,7 +820,7 @@ lemma user_memory_update_corres_C:
prefer 2
apply (clarsimp simp add: doMachineOp_def user_memory_update_def
simpler_modify_def simpler_gets_def select_f_def
NonDetMonad.bind_def return_def)
Nondet_Monad.bind_def return_def)
apply (thin_tac P for P)+
apply (case_tac a, clarsimp)
apply (case_tac ksMachineStatea, clarsimp)
@ -847,7 +847,7 @@ lemma device_update_corres_C:
apply (clarsimp simp add: setDeviceState_C_def simpler_modify_def)
apply (rule ballI)
apply (clarsimp simp: simpler_modify_def setDeviceState_C_def)
apply (clarsimp simp: doMachineOp_def device_memory_update_def NonDetMonad.bind_def in_monad
apply (clarsimp simp: doMachineOp_def device_memory_update_def Nondet_Monad.bind_def in_monad
gets_def get_def return_def simpler_modify_def select_f_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
cmachine_state_relation_def)

2
proof/crefine/ARM/Schedule_C.thy
View File

@ -514,7 +514,7 @@ lemma schedule_ccorres:
apply clarsimp
apply (rule conseqPre, vcg)
apply (fastforce simp: isHighestPrio_def' gets_def return_def get_def
NonDetMonad.bind_def
Nondet_Monad.bind_def
split: prod.split)
apply ceqv
apply (clarsimp simp: to_bool_def)

2
proof/crefine/ARM/VSpace_C.thy
View File

@ -914,7 +914,7 @@ lemma findPDForASID_ccorres:
apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: throwError_def return_def bindE_def bind_def NonDetMonad.lift_def)
apply (clarsimp simp: throwError_def return_def bindE_def bind_def Nondet_Monad.lift_def)
apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def)
apply (simp add: lookup_fault_lift_invalid_root)

2
proof/crefine/ARM_HYP/ADT_C.thy
View File

@ -93,7 +93,7 @@ lemma setTCBContext_C_corres:
apply clarsimp
apply (frule getObject_eq [rotated -1], simp)
apply (simp add: objBits_simps')
apply (simp add: NonDetMonad.bind_def split_def)
apply (simp add: Nondet_Monad.bind_def split_def)
apply (rule bexI)
prefer 2
apply assumption

2
proof/crefine/ARM_HYP/CSpace_RAB_C.thy
View File

@ -54,7 +54,7 @@ lemma ccorres_remove_bind_returnOk_noguard:
apply clarsimp
apply (drule not_snd_bindE_I1)
apply (erule (4) ccorresE[OF ac])
apply (clarsimp simp add: bindE_def returnOk_def NonDetMonad.lift_def bind_def return_def
apply (clarsimp simp add: bindE_def returnOk_def Nondet_Monad.lift_def bind_def return_def
split_def)
apply (rule bexI [rotated], assumption)
apply (simp add: throwError_def return_def unif_rrel_def

4
proof/crefine/ARM_HYP/Fastpath_Equiv.thy
View File

@ -1518,9 +1518,9 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
apply wp
apply (rule monadic_rewrite_trans)
apply (rule_tac rv=rab_ret
in monadic_rewrite_gets_known[where m="NonDetMonad.lift f"
in monadic_rewrite_gets_known[where m="Nondet_Monad.lift f"
for f, folded bindE_def])
apply (simp add: NonDetMonad.lift_def isRight_case_sum)
apply (simp add: Nondet_Monad.lift_def isRight_case_sum)
apply monadic_rewrite_symb_exec_l
apply (rename_tac ep_cap2)
apply (rule_tac P="cteCap ep_cap2 = cteCap ep_cap" in monadic_rewrite_gen_asm)

2
proof/crefine/ARM_HYP/IsolatedThreadAction.thy
View File

@ -1203,7 +1203,7 @@ lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
(is "NonDetMonadVCG.valid ?P ?f ?Q")
(is "Nondet_VCG.valid ?P ?f ?Q")
apply (simp add: setThreadState_def setSchedulerAction_def)
apply (wp hoare_pre_cont[where f=rescheduleRequired])
apply (rule_tac Q="\<lambda>_. ?P and st_tcb_at' ((=) st) t" in hoare_post_imp)

6
proof/crefine/ARM_HYP/Refine_C.thy
View File

@ -472,7 +472,7 @@ lemma ccorres_corres_u_xf:
apply (drule (1) bspec)
apply (clarsimp simp: exec_C_def no_fail_def)
apply (drule_tac x = a in spec)
apply (clarsimp simp:gets_def NonDetMonad.bind_def get_def return_def)
apply (clarsimp simp:gets_def Nondet_Monad.bind_def get_def return_def)
apply (rule conjI)
apply clarsimp
apply (erule_tac x=0 in allE)
@ -836,7 +836,7 @@ lemma user_memory_update_corres_C:
prefer 2
apply (clarsimp simp add: doMachineOp_def user_memory_update_def
simpler_modify_def simpler_gets_def select_f_def
NonDetMonad.bind_def return_def)
Nondet_Monad.bind_def return_def)
apply (thin_tac P for P)+
apply (case_tac a, clarsimp)
apply (case_tac ksMachineState, clarsimp)
@ -863,7 +863,7 @@ lemma device_update_corres_C:
apply (clarsimp simp add: setDeviceState_C_def simpler_modify_def)
apply (rule ballI)
apply (clarsimp simp: simpler_modify_def setDeviceState_C_def)
apply (clarsimp simp: doMachineOp_def device_memory_update_def NonDetMonad.bind_def in_monad
apply (clarsimp simp: doMachineOp_def device_memory_update_def Nondet_Monad.bind_def in_monad
gets_def get_def return_def simpler_modify_def select_f_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
cmachine_state_relation_def)

2
proof/crefine/ARM_HYP/Schedule_C.thy
View File

@ -568,7 +568,7 @@ lemma schedule_ccorres:
apply clarsimp
apply (rule conseqPre, vcg)
apply (fastforce simp: isHighestPrio_def' gets_def return_def get_def
NonDetMonad.bind_def
Nondet_Monad.bind_def
split: prod.split)
apply ceqv
apply (clarsimp simp: to_bool_def)

2
proof/crefine/ARM_HYP/VSpace_C.thy
View File

@ -989,7 +989,7 @@ lemma findPDForASID_ccorres:
apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: throwError_def return_def bindE_def bind_def NonDetMonad.lift_def)
apply (clarsimp simp: throwError_def return_def bindE_def bind_def Nondet_Monad.lift_def)
apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def)
apply (simp add: lookup_fault_lift_invalid_root)

4
proof/crefine/Move_C.thy
View File

@ -679,7 +679,7 @@ lemma asUser_mapM_x:
apply (rule bind_apply_cong [OF refl])+
apply (clarsimp simp: in_monad dest!: fst_stateAssertD)
apply (drule use_valid, rule mapM_wp', rule asUser_typ_ats, assumption)
apply (simp add: stateAssert_def get_def NonDetMonad.bind_def)
apply (simp add: stateAssert_def get_def Nondet_Monad.bind_def)
done
lemma asUser_threadGet_tcbFault_comm:
@ -1204,7 +1204,7 @@ lemma ctes_of_valid_strengthen:
lemma finaliseCap_Reply:
"\<lbrace>Q (NullCap,NullCap) and K (isReplyCap cap)\<rbrace> finaliseCapTrue_standin cap is_final \<lbrace>Q\<rbrace>"
apply (rule NonDetMonadVCG.hoare_gen_asm)
apply (rule Nondet_VCG.hoare_gen_asm)
apply (wpsimp simp: finaliseCapTrue_standin_def isCap_simps)
done

2
proof/crefine/RISCV64/ADT_C.thy
View File

@ -86,7 +86,7 @@ lemma setTCBContext_C_corres:
apply clarsimp
apply (frule getObject_eq [rotated -1], simp)
apply (simp add: objBits_simps')
apply (simp add: NonDetMonad.bind_def split_def)
apply (simp add: Nondet_Monad.bind_def split_def)
apply (rule bexI)
prefer 2
apply assumption

4
proof/crefine/RISCV64/Arch_C.thy
View File

@ -669,7 +669,7 @@ lemma liftME_option_catch_bind:
apply (rule ext)
apply (clarsimp simp: return_def)
apply (case_tac "m s", clarsimp)
apply (auto simp: split_def throwError_def return_def NonDetMonad.lift_def
apply (auto simp: split_def throwError_def return_def Nondet_Monad.lift_def
split: prod.splits sum.splits)
done
@ -1839,7 +1839,7 @@ lemma decodeRISCVFrameInvocation_ccorres:
lookup_fault_missing_capability_new_'proc *)
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: throwError_def return_def bindE_def NonDetMonad.lift_def
apply (clarsimp simp: throwError_def return_def bindE_def Nondet_Monad.lift_def
exception_defs lookup_fault_lift_invalid_root)
apply (clarsimp simp: syscall_error_rel_def exception_defs syscall_error_to_H_def
syscall_error_type_defs)

2
proof/crefine/RISCV64/CSpace_RAB_C.thy
View File

@ -54,7 +54,7 @@ lemma ccorres_remove_bind_returnOk_noguard:
apply clarsimp
apply (drule not_snd_bindE_I1)
apply (erule (4) ccorresE[OF ac])
apply (clarsimp simp add: bindE_def returnOk_def NonDetMonad.lift_def bind_def return_def
apply (clarsimp simp add: bindE_def returnOk_def Nondet_Monad.lift_def bind_def return_def
split_def)
apply (rule bexI [rotated], assumption)
apply (simp add: throwError_def return_def unif_rrel_def

2
proof/crefine/RISCV64/IsolatedThreadAction.thy
View File

@ -964,7 +964,7 @@ lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
(is "NonDetMonadVCG.valid ?P ?f ?Q")
(is "Nondet_VCG.valid ?P ?f ?Q")
apply (simp add: setThreadState_def setSchedulerAction_def)
apply (wp hoare_pre_cont[where f=rescheduleRequired])
apply (rule_tac Q="\<lambda>_. ?P and st_tcb_at' ((=) st) t" in hoare_post_imp)

6
proof/crefine/RISCV64/Refine_C.thy
View File

@ -456,7 +456,7 @@ lemma ccorres_corres_u_xf:
apply (drule (1) bspec)
apply (clarsimp simp: exec_C_def no_fail_def)
apply (drule_tac x = a in spec)
apply (clarsimp simp:gets_def NonDetMonad.bind_def get_def return_def)
apply (clarsimp simp:gets_def Nondet_Monad.bind_def get_def return_def)
apply (rule conjI)
apply clarsimp
apply (erule_tac x=0 in allE)
@ -802,7 +802,7 @@ lemma user_memory_update_corres_C:
prefer 2
apply (clarsimp simp add: doMachineOp_def user_memory_update_def
simpler_modify_def simpler_gets_def select_f_def
NonDetMonad.bind_def return_def)
Nondet_Monad.bind_def return_def)
apply (thin_tac P for P)+
apply (case_tac a, clarsimp)
apply (case_tac ksMachineState, clarsimp)
@ -829,7 +829,7 @@ lemma device_update_corres_C:
apply (clarsimp simp add: setDeviceState_C_def simpler_modify_def)
apply (rule ballI)
apply (clarsimp simp: simpler_modify_def setDeviceState_C_def)
apply (clarsimp simp: doMachineOp_def device_memory_update_def NonDetMonad.bind_def in_monad
apply (clarsimp simp: doMachineOp_def device_memory_update_def Nondet_Monad.bind_def in_monad
gets_def get_def return_def simpler_modify_def select_f_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
cmachine_state_relation_def)

2
proof/crefine/RISCV64/Schedule_C.thy
View File

@ -540,7 +540,7 @@ lemma schedule_ccorres:
apply clarsimp
apply (rule conseqPre, vcg)
apply (fastforce simp: isHighestPrio_def' gets_def return_def get_def
NonDetMonad.bind_def
Nondet_Monad.bind_def
split: prod.split)
apply ceqv
apply (clarsimp simp: to_bool_def)

2
proof/crefine/RISCV64/VSpace_C.thy
View File

@ -719,7 +719,7 @@ lemma findVSpaceForASID_ccorres:
apply clarsimp
apply (rule_tac P="valid_arch_state' and _" and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: throwError_def return_def bindE_def NonDetMonad.lift_def
apply (clarsimp simp: throwError_def return_def bindE_def Nondet_Monad.lift_def
EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def
lookup_fault_lift_invalid_root asid_wf_table_guard)
apply (frule rf_sr_asidTable_None[where asid=asid, THEN iffD2],

2
proof/crefine/X64/ADT_C.thy
View File

@ -84,7 +84,7 @@ lemma setTCBContext_C_corres:
apply clarsimp
apply (frule getObject_eq [rotated -1], simp)
apply (simp add: objBits_simps')
apply (simp add: NonDetMonad.bind_def split_def)
apply (simp add: Nondet_Monad.bind_def split_def)
apply (rule bexI)
prefer 2
apply assumption

2
proof/crefine/X64/CSpace_RAB_C.thy
View File

@ -54,7 +54,7 @@ lemma ccorres_remove_bind_returnOk_noguard:
apply clarsimp
apply (drule not_snd_bindE_I1)
apply (erule (4) ccorresE[OF ac])
apply (clarsimp simp add: bindE_def returnOk_def NonDetMonad.lift_def bind_def return_def
apply (clarsimp simp add: bindE_def returnOk_def Nondet_Monad.lift_def bind_def return_def
split_def)
apply (rule bexI [rotated], assumption)
apply (simp add: throwError_def return_def unif_rrel_def

2
proof/crefine/X64/IsolatedThreadAction.thy
View File

@ -973,7 +973,7 @@ lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
(is "NonDetMonadVCG.valid ?P ?f ?Q")
(is "Nondet_VCG.valid ?P ?f ?Q")
apply (simp add: setThreadState_def setSchedulerAction_def)
apply (wp hoare_pre_cont[where f=rescheduleRequired])
apply (rule_tac Q="\<lambda>_. ?P and st_tcb_at' ((=) st) t" in hoare_post_imp)

6
proof/crefine/X64/Refine_C.thy
View File

@ -458,7 +458,7 @@ lemma ccorres_corres_u_xf:
apply (drule (1) bspec)
apply (clarsimp simp: exec_C_def no_fail_def)
apply (drule_tac x = a in spec)
apply (clarsimp simp:gets_def NonDetMonad.bind_def get_def return_def)
apply (clarsimp simp:gets_def Nondet_Monad.bind_def get_def return_def)
apply (rule conjI)
apply clarsimp
apply (erule_tac x=0 in allE)
@ -802,7 +802,7 @@ lemma user_memory_update_corres_C:
prefer 2
apply (clarsimp simp add: doMachineOp_def user_memory_update_def
simpler_modify_def simpler_gets_def select_f_def
NonDetMonad.bind_def return_def)
Nondet_Monad.bind_def return_def)
apply (thin_tac P for P)+
apply (case_tac a, clarsimp)
apply (case_tac ksMachineState, clarsimp)
@ -829,7 +829,7 @@ lemma device_update_corres_C:
apply (clarsimp simp add: setDeviceState_C_def simpler_modify_def)
apply (rule ballI)
apply (clarsimp simp: simpler_modify_def setDeviceState_C_def)
apply (clarsimp simp: doMachineOp_def device_memory_update_def NonDetMonad.bind_def in_monad
apply (clarsimp simp: doMachineOp_def device_memory_update_def Nondet_Monad.bind_def in_monad
gets_def get_def return_def simpler_modify_def select_f_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
cmachine_state_relation_def)

2
proof/crefine/X64/Schedule_C.thy
View File

@ -536,7 +536,7 @@ lemma schedule_ccorres:
apply clarsimp
apply (rule conseqPre, vcg)
apply (fastforce simp: isHighestPrio_def' gets_def return_def get_def
NonDetMonad.bind_def
Nondet_Monad.bind_def
split: prod.split)
apply ceqv
apply (clarsimp simp: to_bool_def)

2
proof/crefine/X64/VSpace_C.thy
View File

@ -892,7 +892,7 @@ lemma findVSpaceForASID_ccorres:
apply clarsimp
apply (rule_tac P="valid_arch_state' and _" and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: throwError_def return_def bindE_def NonDetMonad.lift_def
apply (clarsimp simp: throwError_def return_def bindE_def Nondet_Monad.lift_def
EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def lookup_fault_lift_invalid_root)
apply (frule rf_sr_asidTable_None[where asid=asid, THEN iffD2],
simp add: asid_wf_def3, assumption, assumption)

6
proof/crefine/autocorres-test/AutoCorresTest.thy
View File

@ -77,7 +77,7 @@ lemma reorder_gets:
(do g;
x \<leftarrow> gets f;
h x od)"
by (fastforce simp: bind_def' NonDetMonadVCG.valid_def gets_def get_def return_def)
by (fastforce simp: bind_def' Nondet_VCG.valid_def gets_def get_def return_def)
thm
(* no arguments, no precondition, dc return *)
@ -100,7 +100,7 @@ lemma (* handleYield_ccorres: *)
(* Show that current thread is unmodified.
* FIXME: proper way to do this? *)
apply (subst reorder_gets[symmetric, unfolded K_bind_def])
using tcbSchedDequeue'_modifies apply (fastforce simp: NonDetMonadVCG.valid_def)
using tcbSchedDequeue'_modifies apply (fastforce simp: Nondet_VCG.valid_def)
apply (subst double_gets_drop_regets)
apply (rule corres_pre_getCurThread_wrapper)
apply (rule corres_split[OF tcbSchedDequeue_ccorres[ac]])
@ -146,7 +146,7 @@ lemma corres_noop2_no_exs:
apply (clarsimp simp: corres_underlying_def)
apply (rule conjI)
apply (drule x, drule y)
apply (clarsimp simp: NonDetMonadVCG.valid_def empty_fail_def Ball_def Bex_def)
apply (clarsimp simp: Nondet_VCG.valid_def empty_fail_def Ball_def Bex_def)
apply fast
apply (insert z)
apply (clarsimp simp: no_fail_def)

8
proof/crefine/lib/AutoCorres_C.thy
View File

@ -69,10 +69,10 @@ FIXME: Move this change into AutoCorres itself, or the underlying VCG library.
lemmas [wp del] =
NonDetMonadEx.validE_whenE
NonDetMonadVCG.whenE_wps
Nondet_VCG.whenE_wps
lemmas hoare_whenE_wp2 [wp] =
NonDetMonadVCG.whenE_wps[simplified if_apply_def2]
Nondet_VCG.whenE_wps[simplified if_apply_def2]
section \<open>Rules for proving @{term ccorres_underlying} goals\<close>
@ -694,7 +694,7 @@ lemma exec_no_fault:
using valid ce asms
apply -
apply (frule hoare_sound)
apply (clarsimp simp: NonDetMonad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
apply (clarsimp simp: Nondet_Monad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
apply (drule spec, drule spec, drule (1) mp)
apply auto
done
@ -707,7 +707,7 @@ lemma exec_no_stuck:
using valid ce asms
apply -
apply (frule hoare_sound)
apply (clarsimp simp: NonDetMonad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
apply (clarsimp simp: Nondet_Monad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
apply (drule spec, drule spec, drule (1) mp)
apply auto
done

4
proof/crefine/lib/Corres_C.thy
View File

@ -837,7 +837,7 @@ lemma ccorres_sequence_x_while_genQ':
\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ len_of TYPE('c);
\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; j > 0 \<rbrakk>
\<Longrightarrow> ccorres (\<lambda>rv i'. i' = of_nat (i + length xs * of_nat j)) xf (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = of_nat i} \<inter> Q) hs
(NonDetMonad.sequence_x xs)
(Nondet_Monad.sequence_x xs)
(While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))"
apply (simp add: sequence_x_sequence liftM_def[symmetric]
@ -856,7 +856,7 @@ lemma ccorres_sequence_x_while_gen':
\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n * j)\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>; i + length xs * j < 2 ^ len_of TYPE('c);
\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s; 0 < j \<rbrakk>
\<Longrightarrow> ccorres (\<lambda>rv i'. i' = of_nat (i + length xs * of_nat j)) xf (F 0) {s. xf s = of_nat i} hs
(NonDetMonad.sequence_x xs)
(Nondet_Monad.sequence_x xs)
(While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))"
apply (simp add: sequence_x_sequence liftM_def[symmetric]

4
proof/crefine/lib/Ctac.thy
View File

@ -1818,8 +1818,8 @@ lemmas mapME_x_simpl_sequence_same
lemmas call_ignore_cong = refl[of "call i f g r" for i f g r]
(* These could be done with ML patterns, but this fits in better with tactics *)
lemmas match_valid = trivial[of "NonDetMonadVCG.valid P a P'" for P a P']
lemmas match_validE = trivial[of "NonDetMonadVCG.validE P a P' P''" for P a P' P'']
lemmas match_valid = trivial[of "Nondet_VCG.valid P a P'" for P a P']
lemmas match_validE = trivial[of "Nondet_VCG.validE P a P' P''" for P a P' P'']
lemmas match_hoare = trivial[of "HoarePartialDef.hoarep G T F P C P' A" for G T F P C P' A]
lemmas match_all_hoare = trivial[of "\<forall>x. HoarePartialDef.hoarep G T F (P x) C (P' x) (A x)" for G T F P C P' A]
lemmas match_xpres = trivial[of "xpres xf v \<Gamma> c" for xf v \<Gamma> c]

2
proof/drefine/Untyped_DR.thy
View File

@ -65,7 +65,7 @@ next
apply (rule someI2_ex, fastforce+)+
done
(* FIXME: For some reason In_Monad.in_fail doesn't fire below. This version would probably
(* FIXME: For some reason Nondet_In_Monad.in_fail doesn't fire below. This version would probably
have been better in the first place. *)
have [simp]: "\<And>s. fst (fail s) = {}" by (simp add: fail_def)

8
proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy
View File

@ -118,7 +118,7 @@ lemma corres_dmo_getExMonitor_C:
apply (rule_tac r'="\<lambda>(r, ms) (r', ms'). r = r' \<and> ms = rv \<and> ms' = rv'"
in corres_split)
apply (rule corres_trivial, rule corres_select_f')
apply (clarsimp simp: getExMonitor_def machine_rest_lift_def NonDetMonad.bind_def gets_def
apply (clarsimp simp: getExMonitor_def machine_rest_lift_def Nondet_Monad.bind_def gets_def
get_def return_def modify_def put_def select_f_def)
apply (clarsimp simp: getExMonitor_no_fail[simplified no_fail_def])
apply (clarsimp simp: split_def)
@ -132,7 +132,7 @@ lemma corres_dmo_getExMonitor_C:
cmachine_state_relation_def Let_def)
apply (rule corres_trivial, clarsimp)
apply (wp hoare_TrueI)+
apply (rule TrueI conjI | clarsimp simp: getExMonitor_def machine_rest_lift_def NonDetMonad.bind_def
apply (rule TrueI conjI | clarsimp simp: getExMonitor_def machine_rest_lift_def Nondet_Monad.bind_def
gets_def get_def return_def modify_def put_def select_f_def)+
done
@ -150,7 +150,7 @@ lemma corres_dmo_setExMonitor_C:
ms' = rv'\<lparr>exclusive_state := es\<rparr>"
in corres_split)
apply (rule corres_trivial, rule corres_select_f')
apply (clarsimp simp: setExMonitor_def machine_rest_lift_def NonDetMonad.bind_def gets_def
apply (clarsimp simp: setExMonitor_def machine_rest_lift_def Nondet_Monad.bind_def gets_def
get_def return_def modify_def put_def select_f_def)
apply (clarsimp simp: setExMonitor_no_fail[simplified no_fail_def])
apply (simp add: split_def)
@ -162,7 +162,7 @@ lemma corres_dmo_setExMonitor_C:
apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def
cmachine_state_relation_def Let_def)
apply (wp hoare_TrueI)+
apply (rule TrueI conjI | clarsimp simp: setExMonitor_def machine_rest_lift_def NonDetMonad.bind_def
apply (rule TrueI conjI | clarsimp simp: setExMonitor_def machine_rest_lift_def Nondet_Monad.bind_def
gets_def get_def return_def modify_def put_def select_f_def)+
done

6
proof/invariant-abstract/AARCH64/Machine_AI.thy
View File

@ -58,7 +58,7 @@ setup \<open>
\<close>
crunch_ignore (no_irq) (add:
NonDetMonad.bind return "when" get gets fail
Nondet_Monad.bind return "when" get gets fail
assert put modify unless select
alternative assert_opt gets_the
returnOk throwError lift bindE
@ -89,7 +89,7 @@ text \<open>Failure on empty result\<close>
crunches loadWord, storeWord, machine_op_lift, clearMemory
for (empty_fail) empty_fail[intro!, wp, simp]
(ignore: NonDetMonad.bind mapM_x simp: machine_op_lift_def empty_fail_cond)
(ignore: Nondet_Monad.bind mapM_x simp: machine_op_lift_def empty_fail_cond)
lemmas ef_machine_op_lift = machine_op_lift_empty_fail \<comment> \<open>required for generic interface\<close>
@ -352,7 +352,7 @@ crunches
and device_state_inv[wp]: "\<lambda>ms. P (device_state ms)"
and irq_masks[wp]: "\<lambda>s. P (irq_masks s)"
and underlying_memory_inv[wp]: "\<lambda>s. P (underlying_memory s)"
(wp: no_irq_bind ignore: empty_fail NonDetMonad.bind)
(wp: no_irq_bind ignore: empty_fail Nondet_Monad.bind)
crunches getFPUState, getRegister, getRestartPC, setNextPC, ackInterrupt, maskInterrupt
for (no_fail) no_fail[intro!, wp, simp]

2
proof/invariant-abstract/ARM/ArchAcc_AI.thy
View File

@ -3148,7 +3148,7 @@ lemma cap_refs_respects_device_region_dmo:
lemma machine_op_lift_device_state[wp]:
"\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>"
by (clarsimp simp: machine_op_lift_def NonDetMonadVCG.valid_def bind_def
by (clarsimp simp: machine_op_lift_def Nondet_VCG.valid_def bind_def
machine_rest_lift_def gets_def simpler_modify_def get_def return_def
select_def ignore_failure_def select_f_def
split: if_splits)

2
proof/invariant-abstract/ARM/Machine_AI.thy
View File

@ -56,7 +56,7 @@ setup \<open>
\<close>
crunch_ignore (no_irq) (add:
NonDetMonad.bind return "when" get gets fail
Nondet_Monad.bind return "when" get gets fail
assert put modify unless select
alternative assert_opt gets_the
returnOk throwError lift bindE

2
proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy
View File

@ -3134,7 +3134,7 @@ lemma cap_refs_respects_device_region_dmo:
lemma machine_op_lift_device_state[wp]:
"\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>"
by (clarsimp simp: machine_op_lift_def NonDetMonadVCG.valid_def bind_def
by (clarsimp simp: machine_op_lift_def Nondet_VCG.valid_def bind_def
machine_rest_lift_def gets_def simpler_modify_def get_def return_def
select_def ignore_failure_def select_f_def
split: if_splits)

2
proof/invariant-abstract/ARM_HYP/Machine_AI.thy
View File

@ -56,7 +56,7 @@ setup \<open>
\<close>
crunch_ignore (no_irq) (add:
NonDetMonad.bind return "when" get gets fail
Nondet_Monad.bind return "when" get gets fail
assert put modify unless select
alternative assert_opt gets_the
returnOk throwError lift bindE

2
proof/invariant-abstract/BCorres_AI.thy
View File

@ -50,7 +50,7 @@ lemma OR_choiceE_bcorres[wp]:
done
crunch_ignore (bcorres)
(add: NonDetMonad.bind gets modify get put do_extended_op empty_slot_ext mapM_x "when"
(add: Nondet_Monad.bind gets modify get put do_extended_op empty_slot_ext mapM_x "when"
select unless mapM catch bindE liftE whenE alternative cap_swap_ext
cap_insert_ext cap_move_ext liftM create_cap_ext
possible_switch_to reschedule_required set_priority

2
proof/invariant-abstract/DetSchedSchedule_AI.thy
View File

@ -1350,7 +1350,7 @@ lemma append_thread_queued:
(* having is_highest_prio match gets_wp makes it very hard to stop and drop imps etc. *)
definition
"wrap_is_highest_prio cur_dom target_prio \<equiv> NonDetMonad.gets (is_highest_prio cur_dom target_prio)"
"wrap_is_highest_prio cur_dom target_prio \<equiv> Nondet_Monad.gets (is_highest_prio cur_dom target_prio)"
lemma schedule_choose_new_thread_valid_sched:
"\<lbrace> valid_idle and valid_etcbs and valid_idle_etcb and valid_queues and valid_blocked

2
proof/invariant-abstract/EmptyFail_AI.thy
View File

@ -57,7 +57,7 @@ lemma without_preemption_empty_fail[wp]:
by simp
crunch_ignore (empty_fail)
(add: NonDetMonad.bind bindE lift liftE liftM "when" whenE unless unlessE return fail
(add: Nondet_Monad.bind bindE lift liftE liftM "when" whenE unless unlessE return fail
assert_opt mapM mapM_x sequence_x catch handleE do_extended_op returnOk throwError
cap_insert_ext empty_slot_ext create_cap_ext cap_swap_ext cap_move_ext
reschedule_required possible_switch_to set_thread_state_ext

4
proof/invariant-abstract/Include_AI.thy
View File

@ -9,7 +9,7 @@ imports
Lib.Lib
ArchCrunchSetup_AI
Monads.Eisbach_WP
Monads.Strengthen_Setup
Monads.Nondet_Strengthen_Setup
ASpec.Syscall_A
Lib.LemmaBucket
Lib.ListLibLemmas
@ -25,7 +25,7 @@ unbundle l4v_word_context
(* Clagged from Bits_R *)
crunch_ignore (add: NonDetMonad.bind return "when" get gets fail assert put modify
crunch_ignore (add: Nondet_Monad.bind return "when" get gets fail assert put modify
unless select alternative assert_opt gets_the returnOk throwError lift
bindE liftE whenE unlessE throw_opt assertE liftM liftME sequence_x
zipWithM_x mapM_x sequence mapM sequenceE_x sequenceE mapME mapME_x

2
proof/invariant-abstract/README.md
View File

@ -9,7 +9,7 @@ Abstract Spec Invariant Proof
This proof defines and proves the global invariants of seL4's
[abstract specification](../../spec/abstract/). The invariants are
phrased and proved using a [monadic Hoare logic](../../lib/Monads/NonDetMonad.thy)
phrased and proved using a [monadic Hoare logic](../../lib/Monads/nondet/Nondet_Monad.thy)
described in a TPHOLS '08 [paper][1].
[1]: https://trustworthy.systems/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement"

2
proof/invariant-abstract/RISCV64/ArchAcc_AI.thy
View File

@ -2879,7 +2879,7 @@ lemma cap_refs_respects_device_region_dmo:
lemma machine_op_lift_device_state[wp]:
"machine_op_lift f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>"
by (clarsimp simp: machine_op_lift_def NonDetMonadVCG.valid_def bind_def
by (clarsimp simp: machine_op_lift_def Nondet_VCG.valid_def bind_def
machine_rest_lift_def gets_def simpler_modify_def get_def return_def
select_def ignore_failure_def select_f_def
split: if_splits)

2
proof/invariant-abstract/RISCV64/Machine_AI.thy
View File

@ -56,7 +56,7 @@ setup \<open>
\<close>
crunch_ignore (no_irq) (add:
NonDetMonad.bind return "when" get gets fail
Nondet_Monad.bind return "when" get gets fail
assert put modify unless select
alternative assert_opt gets_the
returnOk throwError lift bindE

2
proof/invariant-abstract/Syscall_AI.thy
View File

@ -898,7 +898,7 @@ lemma lookup_extra_caps_eq [wp]:
by (wpsimp wp: mapME_set simp: lookup_extra_caps_def)
(*FIXME: move to NonDetMonadVCG.valid_validE_R *)
(*FIXME: move to Nondet_VCG.valid_validE_R *)
lemma valid_validE_R_gen:
"\<lbrakk>\<And>rv s. Q' (Inr rv) s \<Longrightarrow> Q rv s; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -"
by (fastforce simp: validE_R_def validE_def valid_def split_def)

2
proof/invariant-abstract/X64/ArchAcc_AI.thy
View File

@ -2800,7 +2800,7 @@ lemma cap_refs_respects_device_region_dmo:
lemma machine_op_lift_device_state[wp]:
"\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>"
by (clarsimp simp: machine_op_lift_def NonDetMonadVCG.valid_def bind_def
by (clarsimp simp: machine_op_lift_def Nondet_VCG.valid_def bind_def
machine_rest_lift_def gets_def simpler_modify_def get_def return_def
select_def ignore_failure_def select_f_def
split: if_splits)

2
proof/invariant-abstract/X64/Machine_AI.thy
View File

@ -56,7 +56,7 @@ setup \<open>
\<close>
crunch_ignore (no_irq) (add:
NonDetMonad.bind return "when" get gets fail
Nondet_Monad.bind return "when" get gets fail
assert put modify unless select
alternative assert_opt gets_the
returnOk throwError lift bindE

2
proof/refine/AARCH64/Retype_R.thy
View File

@ -1546,7 +1546,7 @@ lemma retype_region_ext_modify_kheap_futz:
apply (simp add: modify_def[symmetric])
done
lemmas retype_region_ext_modify_kheap_futz' = fun_cong[OF arg_cong[where f=NonDetMonad.bind, OF retype_region_ext_modify_kheap_futz[symmetric]], simplified bind_assoc]
lemmas retype_region_ext_modify_kheap_futz' = fun_cong[OF arg_cong[where f=Nondet_Monad.bind, OF retype_region_ext_modify_kheap_futz[symmetric]], simplified bind_assoc]
lemma foldr_upd_app_if_eta_futz:
"foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as = (\<lambda>g x. if x \<in> set as then Some (f x) else g x)"

2
proof/refine/AARCH64/TcbAcc_R.thy
View File

@ -51,7 +51,7 @@ lemma isHighestPrio_def':
"isHighestPrio d p = gets (\<lambda>s. ksReadyQueuesL1Bitmap s d = 0 \<or> lookupBitmapPriority d s \<le> p)"
unfolding isHighestPrio_def bitmap_fun_defs getHighestPrio_def'
apply (rule ext)
apply (clarsimp simp: gets_def bind_assoc return_def NonDetMonad.bind_def get_def
apply (clarsimp simp: gets_def bind_assoc return_def Nondet_Monad.bind_def get_def
split: if_splits)
done

2
proof/refine/AARCH64/Tcb_R.thy
View File

@ -2068,7 +2068,7 @@ lemma checkPrio_wp:
checkPrio prio auth
\<lbrace> \<lambda>rv. P \<rbrace>,-"
apply (simp add: checkPrio_def)
apply (wp NonDetMonadVCG.whenE_throwError_wp getMCP_wp)
apply (wp Nondet_VCG.whenE_throwError_wp getMCP_wp)
by (auto simp add: pred_tcb_at'_def obj_at'_def)
lemma checkPrio_lt_ct:

Some files were not shown because too many files have changed in this diff Show More