globally use session-qualified imports; add Lib session
Session-qualified imports will be required for Isabelle2018 and help clarify the structure of sessions in the build tree. This commit mainly adds a new set of sessions for lib/, including a Lib session that includes most theories in lib/ and a few separate sessions for parts that have dependencies beyond CParser or are separate AFP sessions. The group "lib" collects all lib/ sessions. As a consequence, other theories should use lib/ theories by session name, not by path, which in turns means spec and proof sessions should also refer to each other by session name, not path, to avoid duplicate theory errors in theory merges later.
This commit is contained in:
parent
c1a0f3be1c
commit
b5cdf4703f
1
ROOTS
1
ROOTS
|
@ -6,5 +6,6 @@ proof
|
||||||
tools
|
tools
|
||||||
camkes
|
camkes
|
||||||
sys-init
|
sys-init
|
||||||
|
lib
|
||||||
lib/Word_Lib
|
lib/Word_Lib
|
||||||
lib/sep_algebra
|
lib/sep_algebra
|
15
camkes/ROOT
15
camkes/ROOT
|
@ -35,14 +35,15 @@ session CamkesAdlSpec (Camkes) in "adl-spec" = HOL +
|
||||||
* of CamkesAdlSpec and DSpec, and is defined because we can't easily depend on both.
|
* of CamkesAdlSpec and DSpec, and is defined because we can't easily depend on both.
|
||||||
*)
|
*)
|
||||||
session CamkesCdlBase (Camkes) in "adl-spec" = DPolicy +
|
session CamkesCdlBase (Camkes) in "adl-spec" = DPolicy +
|
||||||
|
sessions
|
||||||
|
DSpec
|
||||||
|
CamkesAdlSpec
|
||||||
|
Lib
|
||||||
theories
|
theories
|
||||||
(* DSpec *)
|
"DSpec.Syscall_D"
|
||||||
"../spec/capDL/Syscall_D"
|
"CamkesAdlSpec.Wellformed_CAMKES"
|
||||||
(* CamkesAdlSpec *)
|
"CamkesAdlSpec.Examples_CAMKES"
|
||||||
"Wellformed_CAMKES"
|
"Lib.LemmaBucket"
|
||||||
"Examples_CAMKES"
|
|
||||||
(* Lemma buckets *)
|
|
||||||
"../../lib/LemmaBucket"
|
|
||||||
|
|
||||||
(* CAmkES<->CapDL reasoning. *)
|
(* CAmkES<->CapDL reasoning. *)
|
||||||
session CamkesCdlRefine (Camkes) in "cdl-refine" = CamkesCdlBase +
|
session CamkesCdlRefine (Camkes) in "cdl-refine" = CamkesCdlBase +
|
||||||
|
|
|
@ -11,9 +11,9 @@
|
||||||
theory Generator_CAMKES_CDL imports
|
theory Generator_CAMKES_CDL imports
|
||||||
"../adl-spec/Types_CAMKES"
|
"../adl-spec/Types_CAMKES"
|
||||||
"../adl-spec/Library_CAMKES"
|
"../adl-spec/Library_CAMKES"
|
||||||
"../../spec/capDL/Syscall_D"
|
"DSpec.Syscall_D"
|
||||||
Types_CAMKES_CDL
|
Types_CAMKES_CDL
|
||||||
"../../proof/access-control/Dpolicy"
|
"DPolicy.Dpolicy"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory Types_CAMKES_CDL imports
|
theory Types_CAMKES_CDL imports
|
||||||
"../adl-spec/Types_CAMKES"
|
"../adl-spec/Types_CAMKES"
|
||||||
"../adl-spec/Library_CAMKES"
|
"../adl-spec/Library_CAMKES"
|
||||||
"../../spec/capDL/Syscall_D"
|
"DSpec.Syscall_D"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* placeholder for things to fill in *)
|
(* placeholder for things to fill in *)
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
chapter {* Shared Memory *}
|
chapter {* Shared Memory *}
|
||||||
(*<*)
|
(*<*)
|
||||||
theory DataIn imports
|
theory DataIn imports
|
||||||
"../../tools/c-parser/CTranslation"
|
"CParser.CTranslation"
|
||||||
"../../tools/autocorres/AutoCorres"
|
"AutoCorres.AutoCorres"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
||||||
|
|
|
@ -11,8 +11,8 @@
|
||||||
chapter {* Event Send *}
|
chapter {* Event Send *}
|
||||||
(*<*)
|
(*<*)
|
||||||
theory EventFrom imports
|
theory EventFrom imports
|
||||||
"../../tools/c-parser/CTranslation"
|
"CParser.CTranslation"
|
||||||
"../../tools/autocorres/AutoCorres"
|
"AutoCorres.AutoCorres"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
chapter {* Event Receive *}
|
chapter {* Event Receive *}
|
||||||
(*<*)
|
(*<*)
|
||||||
theory EventTo imports
|
theory EventTo imports
|
||||||
"../../tools/c-parser/CTranslation"
|
"CParser.CTranslation"
|
||||||
"../../tools/autocorres/AutoCorres"
|
"AutoCorres.AutoCorres"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
||||||
|
|
|
@ -9,8 +9,8 @@
|
||||||
*)
|
*)
|
||||||
(*<*)
|
(*<*)
|
||||||
theory RPCFrom imports
|
theory RPCFrom imports
|
||||||
"../../tools/c-parser/CTranslation"
|
"CParser.CTranslation"
|
||||||
"../../tools/autocorres/AutoCorres"
|
"AutoCorres.AutoCorres"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
chapter {* RPC Receive *}
|
chapter {* RPC Receive *}
|
||||||
(*<*)
|
(*<*)
|
||||||
theory RPCTo imports
|
theory RPCTo imports
|
||||||
"../../tools/c-parser/CTranslation"
|
"CParser.CTranslation"
|
||||||
"../../tools/autocorres/AutoCorres"
|
"AutoCorres.AutoCorres"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
(* THIS THEORY IS GENERATED. DO NOT EDIT. *)
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
chapter {* Syntax *}
|
chapter {* Syntax *}
|
||||||
(*<*)
|
(*<*)
|
||||||
theory Syntax imports
|
theory Syntax imports
|
||||||
"../../tools/c-parser/CTranslation"
|
"CParser.CTranslation"
|
||||||
"../../tools/autocorres/AutoCorres"
|
"AutoCorres.AutoCorres"
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory AdjustSchematic (* FIXME: bitrotted *)
|
theory AdjustSchematic (* FIXME: bitrotted *)
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
lemma meta_arg_cong:
|
lemma meta_arg_cong:
|
||||||
|
|
|
@ -10,8 +10,11 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Apply_Debug
|
theory Apply_Debug
|
||||||
imports Apply_Trace "~~/src/HOL/Eisbach/Eisbach_Tools"
|
imports
|
||||||
keywords "apply_debug" :: "prf_script" % "proof" and
|
Apply_Trace
|
||||||
|
"HOL-Eisbach.Eisbach_Tools"
|
||||||
|
keywords
|
||||||
|
"apply_debug" :: "prf_script" % "proof" and
|
||||||
"continue" :: prf_script % "proof" and "finish" :: prf_script % "proof"
|
"continue" :: prf_script % "proof" and "finish" :: prf_script % "proof"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -11,7 +11,10 @@
|
||||||
|
|
||||||
|
|
||||||
theory CorresK_Lemmas
|
theory CorresK_Lemmas
|
||||||
imports Corres_Method "../spec/design/Syscall_H" "../spec/abstract/Syscall_A"
|
imports
|
||||||
|
Corres_Method
|
||||||
|
"ExecSpec.Syscall_H"
|
||||||
|
"ASpec.Syscall_A"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
lemma corres_throwError_str [corres_concrete_rER]:
|
lemma corres_throwError_str [corres_concrete_rER]:
|
||||||
|
|
|
@ -14,7 +14,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Corres_Test
|
theory Corres_Test
|
||||||
imports "../proof/refine/ARM/VSpace_R" Corres_Method
|
imports "Refine.VSpace_R" Corres_Method
|
||||||
begin
|
begin
|
||||||
|
|
||||||
chapter \<open>The Corres Method\<close>
|
chapter \<open>The Corres Method\<close>
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory DataMap
|
theory DataMap
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
type_synonym ('k, 'a) map = "'k \<rightharpoonup> 'a"
|
type_synonym ('k, 'a) map = "'k \<rightharpoonup> 'a"
|
||||||
|
|
|
@ -13,8 +13,9 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Eisbach_Methods
|
theory Eisbach_Methods
|
||||||
imports "subgoal_focus/Subgoal_Methods"
|
imports
|
||||||
"~~/src/HOL/Eisbach/Eisbach_Tools"
|
"subgoal_focus/Subgoal_Methods"
|
||||||
|
"HOL-Eisbach.Eisbach_Tools"
|
||||||
Rule_By_Method
|
Rule_By_Method
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory ExpandAll (* FIXME: bitrotted *)
|
theory ExpandAll (* FIXME: bitrotted *)
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
lemma expand_forall:
|
lemma expand_forall:
|
||||||
|
|
|
@ -1,18 +0,0 @@
|
||||||
(*
|
|
||||||
* Copyright 2014, NICTA
|
|
||||||
*
|
|
||||||
* This software may be distributed and modified according to the terms of
|
|
||||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
|
||||||
* See "LICENSE_BSD2.txt" for details.
|
|
||||||
*
|
|
||||||
* @TAG(NICTA_BSD)
|
|
||||||
*)
|
|
||||||
|
|
||||||
theory GenericLib_C
|
|
||||||
imports HaskellLemmaBucket
|
|
||||||
begin
|
|
||||||
|
|
||||||
(* Legacy interface file. *)
|
|
||||||
|
|
||||||
|
|
||||||
end
|
|
|
@ -16,7 +16,7 @@
|
||||||
theory HaskellLib_H
|
theory HaskellLib_H
|
||||||
imports
|
imports
|
||||||
Lib
|
Lib
|
||||||
"$L4V_ARCH/WordSetup"
|
"Word_Lib.WordSetup"
|
||||||
"Monad_WP/NonDetMonadVCG"
|
"Monad_WP/NonDetMonadVCG"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
|
|
||||||
theory Hoare_Sep_Tactics
|
theory Hoare_Sep_Tactics
|
||||||
imports
|
imports
|
||||||
"../Monad_WP/NonDetMonadVCG"
|
"Lib.NonDetMonadVCG"
|
||||||
"../sep_algebra/Sep_Algebra_L4v"
|
"Sep_Algebra.Sep_Algebra_L4v"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* FIXME: needs cleanup *)
|
(* FIXME: needs cleanup *)
|
||||||
|
|
|
@ -49,7 +49,8 @@
|
||||||
* - Naive algorithm, takes \<approx>quadratic time.
|
* - Naive algorithm, takes \<approx>quadratic time.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Insulin imports HOL
|
theory Insulin
|
||||||
|
imports Main
|
||||||
keywords "desugar_term" "desugar_thm" "desugar_goal" :: diag
|
keywords "desugar_term" "desugar_thm" "desugar_goal" :: diag
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -22,7 +22,7 @@ imports
|
||||||
Extract_Conjunct
|
Extract_Conjunct
|
||||||
Eval_Bool
|
Eval_Bool
|
||||||
NICTATools
|
NICTATools
|
||||||
"~~/src/HOL/Library/Prefix_Order"
|
"HOL-Library.Prefix_Order"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* FIXME: eliminate *)
|
(* FIXME: eliminate *)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
chapter "List Manipulation Functions"
|
chapter "List Manipulation Functions"
|
||||||
|
|
||||||
theory List_Lib
|
theory List_Lib
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
definition list_replace :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where
|
definition list_replace :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
|
|
||||||
theory WP_Pre
|
theory WP_Pre
|
||||||
imports
|
imports
|
||||||
"~~/src/HOL/Main"
|
Main
|
||||||
"~~/src/HOL/Eisbach/Eisbach_Tools"
|
"HOL-Eisbach.Eisbach_Tools"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
named_theorems wp_pre
|
named_theorems wp_pre
|
||||||
|
|
|
@ -13,8 +13,8 @@ imports
|
||||||
"Monad_WP/NonDetMonadVCG"
|
"Monad_WP/NonDetMonadVCG"
|
||||||
"MonadEq"
|
"MonadEq"
|
||||||
"Monad_WP/WhileLoopRulesCompleteness"
|
"Monad_WP/WhileLoopRulesCompleteness"
|
||||||
Distinct_Prop
|
"Word_Lib.Distinct_Prop"
|
||||||
"~~/src/HOL/Word/Word_Miscellaneous"
|
"HOL-Word.Word_Miscellaneous"
|
||||||
begin
|
begin
|
||||||
setup \<open>AutoLevity_Base.add_attribute_test "wp" WeakestPre.is_wp_rule\<close>
|
setup \<open>AutoLevity_Base.add_attribute_test "wp" WeakestPre.is_wp_rule\<close>
|
||||||
|
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
|
||||||
theory WordSetup
|
theory WordSetup (* part of non-AFP Word_Lib *)
|
||||||
imports
|
imports
|
||||||
"../Distinct_Prop"
|
"../Distinct_Prop"
|
||||||
"../Word_Lib/Word_Lemmas_64"
|
"../Word_Lib/Word_Lemmas_64"
|
||||||
|
|
|
@ -0,0 +1,175 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2018, Data61/CSIRO
|
||||||
|
*
|
||||||
|
* This software may be distributed and modified according to the terms of
|
||||||
|
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||||
|
* See "LICENSE_BSD2.txt" for details.
|
||||||
|
*
|
||||||
|
* @TAG(DATA61_BSD)
|
||||||
|
*)
|
||||||
|
|
||||||
|
chapter Lib
|
||||||
|
|
||||||
|
session Lib (lib) = Word_Lib +
|
||||||
|
sessions
|
||||||
|
"HOL-Library"
|
||||||
|
"HOL-Eisbach"
|
||||||
|
theories
|
||||||
|
Lib
|
||||||
|
Apply_Trace_Cmd
|
||||||
|
AddUpdSimps
|
||||||
|
EmptyFailLib
|
||||||
|
List_Lib
|
||||||
|
Crunch_Test_NonDet
|
||||||
|
Crunch_Test_Qualified_NonDet
|
||||||
|
Crunch_Test_Qualified_Trace
|
||||||
|
Crunch_Test_Trace
|
||||||
|
SubMonadLib
|
||||||
|
Simulation
|
||||||
|
MonadEq
|
||||||
|
SimpStrategy
|
||||||
|
Extract_Conjunct
|
||||||
|
Apply_Debug_Test
|
||||||
|
GenericLib
|
||||||
|
ProvePart
|
||||||
|
Corres_Adjust_Preconds
|
||||||
|
AutoLevity_Base
|
||||||
|
Requalify
|
||||||
|
Value_Abbreviation
|
||||||
|
Eisbach_Methods
|
||||||
|
HaskellLib_H
|
||||||
|
AutoLevity_Test
|
||||||
|
Eval_Bool
|
||||||
|
Bisim_UL
|
||||||
|
Extend_Locale
|
||||||
|
Solves_Tac
|
||||||
|
Crunch
|
||||||
|
Crunch_Instances_NonDet
|
||||||
|
Crunch_Instances_Trace
|
||||||
|
StateMonad
|
||||||
|
Corres_UL
|
||||||
|
Find_Names
|
||||||
|
LemmaBucket
|
||||||
|
Try_Methods
|
||||||
|
ListLibLemmas
|
||||||
|
Time_Methods_Cmd
|
||||||
|
Apply_Debug
|
||||||
|
Match_Abbreviation_Test
|
||||||
|
MonadicRewrite
|
||||||
|
HaskellLemmaBucket
|
||||||
|
"ml-helpers/TermPatternAntiquote"
|
||||||
|
"subgoal_focus/Subgoal_Methods"
|
||||||
|
Insulin
|
||||||
|
ExtraCorres
|
||||||
|
NICTATools
|
||||||
|
BCorres_UL
|
||||||
|
Qualify
|
||||||
|
LexordList
|
||||||
|
Rule_By_Method
|
||||||
|
Defs
|
||||||
|
AutoLevity_Hooks
|
||||||
|
Distinct_Cmd
|
||||||
|
Match_Abbreviation
|
||||||
|
ShowTypes
|
||||||
|
SpecValid_R
|
||||||
|
EquivValid
|
||||||
|
SplitRule
|
||||||
|
Time_Methods_Cmd_Test
|
||||||
|
DataMap
|
||||||
|
Corres_Method
|
||||||
|
Conjuncts
|
||||||
|
|
||||||
|
(* should really be a separate session, but too entangled atm: *)
|
||||||
|
NonDetMonadLemmaBucket
|
||||||
|
"Monad_WP/WhileLoopRules"
|
||||||
|
"Monad_WP/TraceMonad"
|
||||||
|
"Monad_WP/OptionMonadND"
|
||||||
|
"Monad_WP/OptionMonadWP"
|
||||||
|
"Monad_WP/Strengthen_Demo"
|
||||||
|
"Monad_WP/TraceMonadLemmas"
|
||||||
|
"Monad_WP/wp/WPBang"
|
||||||
|
"Monad_WP/wp/WPFix"
|
||||||
|
"Monad_WP/wp/Eisbach_WP"
|
||||||
|
"Monad_WP/wp/WPI"
|
||||||
|
"Monad_WP/wp/WPC"
|
||||||
|
"Monad_WP/wp/WPEx"
|
||||||
|
"Monad_WP/wp/WP_Pre"
|
||||||
|
"Monad_WP/wp/WP"
|
||||||
|
"Monad_WP/Datatype_Schematic"
|
||||||
|
"Monad_WP/WhileLoopRulesCompleteness"
|
||||||
|
"Monad_WP/Strengthen"
|
||||||
|
"Monad_WP/OptionMonad"
|
||||||
|
"Monad_WP/TraceMonadVCG"
|
||||||
|
"Monad_WP/NonDetMonadVCG"
|
||||||
|
"Monad_WP/NonDetMonad"
|
||||||
|
"Monad_WP/NonDetMonadLemmas"
|
||||||
|
|
||||||
|
(* bitrotted:
|
||||||
|
AdjustSchematic
|
||||||
|
ExpandAll
|
||||||
|
TSubst
|
||||||
|
Trace_Attribs
|
||||||
|
StringOrd
|
||||||
|
"ml-helpers/TacticAPI"
|
||||||
|
*)
|
||||||
|
|
||||||
|
session CLib (lib) in clib = CParser +
|
||||||
|
sessions
|
||||||
|
"HOL-Library"
|
||||||
|
"HOL-Statespace"
|
||||||
|
"HOL-Eisbach"
|
||||||
|
"Simpl-VCG"
|
||||||
|
Lib
|
||||||
|
theories
|
||||||
|
Corres_UL_C
|
||||||
|
CCorresLemmas
|
||||||
|
CCorres_Rewrite
|
||||||
|
Simpl_Rewrite
|
||||||
|
MonadicRewrite_C
|
||||||
|
DetWPLib
|
||||||
|
CTranslationNICTA
|
||||||
|
LemmaBucket_C
|
||||||
|
SIMPL_Lemmas
|
||||||
|
SimplRewrite
|
||||||
|
TypHeapLib
|
||||||
|
BitFieldProofsLib
|
||||||
|
XPres
|
||||||
|
|
||||||
|
session CorresK = Lib +
|
||||||
|
sessions
|
||||||
|
ASpec
|
||||||
|
ExecSpec
|
||||||
|
theories
|
||||||
|
CorresK_Lemmas
|
||||||
|
|
||||||
|
session LibTest (lib) = Refine +
|
||||||
|
sessions
|
||||||
|
Lib
|
||||||
|
CLib
|
||||||
|
ASpec
|
||||||
|
ExecSpec
|
||||||
|
theories
|
||||||
|
Corres_Test
|
||||||
|
WPTutorial
|
||||||
|
|
||||||
|
session SepTactics (lib) in Hoare_Sep_Tactics = Sep_Algebra +
|
||||||
|
theories
|
||||||
|
Hoare_Sep_Tactics
|
||||||
|
|
||||||
|
(* FIXME: in proof
|
||||||
|
session AutoLevity (lib) = HOL +
|
||||||
|
theories
|
||||||
|
AutoLevity
|
||||||
|
AutoLevity_Run
|
||||||
|
AutoLevity_Theory_Report
|
||||||
|
*)
|
||||||
|
|
||||||
|
session Concurrency (lib) in concurrency = HOL +
|
||||||
|
sessions
|
||||||
|
Lib
|
||||||
|
theories
|
||||||
|
Atomicity_Lib
|
||||||
|
Triv_Refinement
|
||||||
|
Prefix_Refinement
|
||||||
|
"examples/Peterson_Atomicity"
|
||||||
|
"examples/Plus2_Prefix"
|
|
@ -11,7 +11,7 @@
|
||||||
theory Rule_By_Method
|
theory Rule_By_Method
|
||||||
imports
|
imports
|
||||||
Main
|
Main
|
||||||
"~~/src/HOL/Eisbach/Eisbach_Tools"
|
"HOL-Eisbach.Eisbach_Tools"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
ML \<open>
|
ML \<open>
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory SimpStrategy
|
theory SimpStrategy
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
|
|
@ -15,7 +15,7 @@
|
||||||
chapter "Refinement"
|
chapter "Refinement"
|
||||||
|
|
||||||
theory Simulation
|
theory Simulation
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory SplitRule
|
theory SplitRule
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
ML {*
|
ML {*
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory StringOrd
|
theory StringOrd
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
datatype anotherBL =
|
datatype anotherBL =
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory Time_Methods_Cmd_Test imports
|
theory Time_Methods_Cmd_Test imports
|
||||||
Time_Methods_Cmd
|
Time_Methods_Cmd
|
||||||
Eisbach_Methods
|
Eisbach_Methods
|
||||||
"~~/src/HOL/Library/Sublist"
|
"HOL-Library.Sublist"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text \<open>
|
text \<open>
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory WPTutorial
|
theory WPTutorial
|
||||||
imports "../proof/refine/$L4V_ARCH/Bits_R"
|
imports "Refine.Bits_R"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
|
|
@ -9,9 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory AutoCorresCRefine
|
theory AutoCorresCRefine
|
||||||
|
imports Ctac LegacyAutoCorres
|
||||||
imports Ctac "../../tools/autocorres/LegacyAutoCorres"
|
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context kernel begin
|
context kernel begin
|
||||||
|
|
|
@ -10,7 +10,7 @@
|
||||||
|
|
||||||
theory BitFieldProofsLib
|
theory BitFieldProofsLib
|
||||||
imports
|
imports
|
||||||
Eisbach_Methods
|
"Lib.Eisbach_Methods"
|
||||||
TypHeapLib
|
TypHeapLib
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -11,9 +11,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory CCorres_Rewrite
|
theory CCorres_Rewrite
|
||||||
imports
|
imports Corres_UL_C Simpl_Rewrite
|
||||||
"Corres_UL_C"
|
|
||||||
"Simpl_Rewrite"
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text \<open>A simple proof method for rewriting Simpl programs under @{term ccorres_underlying}.\<close>
|
text \<open>A simple proof method for rewriting Simpl programs under @{term ccorres_underlying}.\<close>
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
|
|
||||||
theory CTranslationNICTA
|
theory CTranslationNICTA
|
||||||
imports
|
imports
|
||||||
"../tools/c-parser/CTranslation"
|
"CParser.CTranslation"
|
||||||
"Word_Lib/Word_Lib"
|
"Word_Lib.Word_Lib"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
declare len_of_numeral_defs [simp del]
|
declare len_of_numeral_defs [simp del]
|
|
@ -15,9 +15,9 @@
|
||||||
|
|
||||||
theory Corres_UL_C
|
theory Corres_UL_C
|
||||||
imports
|
imports
|
||||||
"../LemmaBucket_C"
|
"LemmaBucket_C"
|
||||||
"../LemmaBucket"
|
"Lib.LemmaBucket"
|
||||||
"../SIMPL_Lemmas"
|
"SIMPL_Lemmas"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
declare word_neq_0_conv [simp del]
|
declare word_neq_0_conv [simp del]
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory DetWPLib
|
theory DetWPLib
|
||||||
imports "../GenericLib_C"
|
imports "Lib.HaskellLemmaBucket"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
definition
|
definition
|
||||||
|
|
|
@ -10,7 +10,7 @@
|
||||||
|
|
||||||
theory LegacyAutoCorres
|
theory LegacyAutoCorres
|
||||||
|
|
||||||
imports AutoCorres "../../lib/clib/Corres_UL_C"
|
imports "AutoCorres.AutoCorres" "Corres_UL_C"
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -10,10 +10,10 @@
|
||||||
|
|
||||||
theory LemmaBucket_C
|
theory LemmaBucket_C
|
||||||
imports
|
imports
|
||||||
Lib
|
"Lib.Lib"
|
||||||
"$L4V_ARCH/WordSetup"
|
"Word_Lib.WordSetup"
|
||||||
TypHeapLib
|
TypHeapLib
|
||||||
"../tools/c-parser/umm_heap/ArrayAssertion"
|
"CParser.ArrayAssertion"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
declare word_neq_0_conv [simp del]
|
declare word_neq_0_conv [simp del]
|
|
@ -12,7 +12,7 @@
|
||||||
|
|
||||||
theory MonadicRewrite_C
|
theory MonadicRewrite_C
|
||||||
imports
|
imports
|
||||||
"../MonadicRewrite"
|
"Lib.MonadicRewrite"
|
||||||
Corres_UL_C
|
Corres_UL_C
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -10,7 +10,7 @@
|
||||||
|
|
||||||
theory SIMPL_Lemmas
|
theory SIMPL_Lemmas
|
||||||
imports
|
imports
|
||||||
"GenericLib_C"
|
"Lib.HaskellLemmaBucket"
|
||||||
"CTranslationNICTA"
|
"CTranslationNICTA"
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -11,8 +11,8 @@
|
||||||
theory SimplRewrite
|
theory SimplRewrite
|
||||||
imports
|
imports
|
||||||
"CTranslationNICTA"
|
"CTranslationNICTA"
|
||||||
"SplitRule"
|
"Lib.SplitRule"
|
||||||
"~~/src/HOL/Eisbach/Eisbach"
|
"HOL-Eisbach.Eisbach"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
primrec
|
primrec
|
|
@ -15,9 +15,9 @@ text \<open>A simple proof method for rewriting Simpl programs under a predicate
|
||||||
|
|
||||||
theory Simpl_Rewrite
|
theory Simpl_Rewrite
|
||||||
imports
|
imports
|
||||||
"../../tools/c-parser/Simpl/Vcg"
|
"Simpl-VCG.Vcg"
|
||||||
"../Eisbach_Methods"
|
"Lib.Eisbach_Methods"
|
||||||
"../Apply_Debug"
|
"Lib.Apply_Debug"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text \<open>Definitions and lemmas for reasoning about equivalence of Simpl programs.\<close>
|
text \<open>Definitions and lemmas for reasoning about equivalence of Simpl programs.\<close>
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory TypHeapLib
|
theory TypHeapLib
|
||||||
imports "../tools/c-parser/CTranslation"
|
imports "CParser.CTranslation"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* This file contains everything you need to know and use for the
|
(* This file contains everything you need to know and use for the
|
|
@ -11,7 +11,7 @@ theory Prefix_Refinement
|
||||||
|
|
||||||
imports
|
imports
|
||||||
Triv_Refinement
|
Triv_Refinement
|
||||||
"../Monad_WP/TraceMonadLemmas"
|
"Lib.TraceMonadLemmas"
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
theory Triv_Refinement
|
theory Triv_Refinement
|
||||||
|
|
||||||
imports
|
imports
|
||||||
"../Monad_WP/TraceMonadVCG"
|
"Lib.TraceMonadVCG"
|
||||||
"../Monad_WP/Strengthen"
|
"Lib.Strengthen"
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -16,7 +16,7 @@
|
||||||
chapter {* More properties of maps plus map disjuction. *}
|
chapter {* More properties of maps plus map disjuction. *}
|
||||||
|
|
||||||
theory Map_Extra
|
theory Map_Extra
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory MonadSep
|
theory MonadSep
|
||||||
imports
|
imports
|
||||||
Sep_Algebra_L4v
|
Sep_Algebra_L4v
|
||||||
"../LemmaBucket"
|
"Lib.LemmaBucket"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
locale sep_lifted =
|
locale sep_lifted =
|
||||||
|
|
|
@ -11,7 +11,11 @@
|
||||||
chapter Lib
|
chapter Lib
|
||||||
|
|
||||||
(* This is a testing session to make sure none of these are forgotten *)
|
(* This is a testing session to make sure none of these are forgotten *)
|
||||||
session Sep_Algebra = Word_Lib +
|
session Sep_Algebra (lib) = Word_Lib +
|
||||||
|
sessions
|
||||||
|
"HOL-Eisbach"
|
||||||
|
"HOL-Hoare"
|
||||||
|
Lib
|
||||||
theories
|
theories
|
||||||
"Generic_Separation_Algebras"
|
"Generic_Separation_Algebras"
|
||||||
"MonadSep"
|
"MonadSep"
|
||||||
|
|
|
@ -18,7 +18,7 @@ chapter "Abstract Separation Algebra"
|
||||||
theory Separation_Algebra
|
theory Separation_Algebra
|
||||||
imports
|
imports
|
||||||
Arbitrary_Comm_Monoid
|
Arbitrary_Comm_Monoid
|
||||||
"~~/src/Tools/Adhoc_Overloading"
|
"HOL-Library.Adhoc_Overloading"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {* This theory is the main abstract separation algebra development *}
|
text {* This theory is the main abstract separation algebra development *}
|
||||||
|
|
|
@ -16,7 +16,7 @@
|
||||||
chapter "Abstract Separation Logic, Alternative Definition"
|
chapter "Abstract Separation Logic, Alternative Definition"
|
||||||
|
|
||||||
theory Separation_Algebra_Alt
|
theory Separation_Algebra_Alt
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
|
|
@ -18,7 +18,7 @@ chapter "Example from HOL/Hoare/Separation"
|
||||||
|
|
||||||
theory Simple_Separation_Example
|
theory Simple_Separation_Example
|
||||||
imports
|
imports
|
||||||
"~~/src/HOL/Hoare/Hoare_Logic_Abort"
|
"HOL-Hoare.Hoare_Logic_Abort"
|
||||||
"../Sep_Heap_Instance"
|
"../Sep_Heap_Instance"
|
||||||
"../Sep_Tactics"
|
"../Sep_Tactics"
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -16,7 +16,7 @@
|
||||||
chapter "A simplified version of the actual capDL specification."
|
chapter "A simplified version of the actual capDL specification."
|
||||||
|
|
||||||
theory Types_D
|
theory Types_D
|
||||||
imports "~~/src/HOL/Word/Word"
|
imports "HOL-Word.Word"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(*
|
(*
|
||||||
|
|
38
proof/ROOT
38
proof/ROOT
|
@ -32,12 +32,22 @@ chapter "Proofs"
|
||||||
|
|
||||||
session Refine = BaseRefine +
|
session Refine = BaseRefine +
|
||||||
description {* Refinement between Haskell and Abstract spec. *}
|
description {* Refinement between Haskell and Abstract spec. *}
|
||||||
|
sessions
|
||||||
|
Lib
|
||||||
|
CorresK
|
||||||
|
AInvs
|
||||||
theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty]
|
theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty]
|
||||||
"refine/$L4V_ARCH/Refine"
|
"refine/$L4V_ARCH/Refine"
|
||||||
|
"refine/$L4V_ARCH/RAB_FN"
|
||||||
|
"refine/$L4V_ARCH/EmptyFail_H"
|
||||||
theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
|
theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
|
||||||
"refine/$L4V_ARCH/Refine"
|
"refine/$L4V_ARCH/Refine"
|
||||||
|
"refine/$L4V_ARCH/RAB_FN"
|
||||||
|
"refine/$L4V_ARCH/EmptyFail_H"
|
||||||
theories
|
theories
|
||||||
"refine/$L4V_ARCH/Refine"
|
"refine/$L4V_ARCH/Refine"
|
||||||
|
"refine/$L4V_ARCH/RAB_FN"
|
||||||
|
"refine/$L4V_ARCH/EmptyFail_H"
|
||||||
theories [condition = "L4V_ARCH_IS_ARM"]
|
theories [condition = "L4V_ARCH_IS_ARM"]
|
||||||
"refine/$L4V_ARCH/Orphanage"
|
"refine/$L4V_ARCH/Orphanage"
|
||||||
|
|
||||||
|
@ -83,12 +93,16 @@ session CRefine = CBaseRefine +
|
||||||
"crefine/$L4V_ARCH/Refine_C"
|
"crefine/$L4V_ARCH/Refine_C"
|
||||||
|
|
||||||
session CBaseRefine = CSpec +
|
session CBaseRefine = CSpec +
|
||||||
|
sessions
|
||||||
|
CLib
|
||||||
|
Refine
|
||||||
|
AutoCorres
|
||||||
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
|
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
|
||||||
(* ../lib/clib/AutoCorres_C explains why L4VerifiedLinks is included here. *)
|
(* ../lib/clib/AutoCorres_C explains why L4VerifiedLinks is included here. *)
|
||||||
"../tools/autocorres/L4VerifiedLinks"
|
"crefine/lib/L4VerifiedLinks"
|
||||||
"crefine/$L4V_ARCH/Include_C"
|
"crefine/$L4V_ARCH/Include_C"
|
||||||
theories
|
theories
|
||||||
"../tools/autocorres/L4VerifiedLinks"
|
"crefine/lib/L4VerifiedLinks"
|
||||||
"crefine/$L4V_ARCH/Include_C"
|
"crefine/$L4V_ARCH/Include_C"
|
||||||
|
|
||||||
session AutoCorresCRefine = CRefine +
|
session AutoCorresCRefine = CRefine +
|
||||||
|
@ -100,6 +114,8 @@ session AutoCorresCRefine = CRefine +
|
||||||
*)
|
*)
|
||||||
|
|
||||||
session DBaseRefine = Refine +
|
session DBaseRefine = Refine +
|
||||||
|
sessions
|
||||||
|
DSpec
|
||||||
theories
|
theories
|
||||||
"drefine/Include_D"
|
"drefine/Include_D"
|
||||||
|
|
||||||
|
@ -108,6 +124,8 @@ session DRefine = DBaseRefine +
|
||||||
"drefine/Refine_D"
|
"drefine/Refine_D"
|
||||||
|
|
||||||
session DPolicy = DRefine +
|
session DPolicy = DRefine +
|
||||||
|
sessions
|
||||||
|
Access
|
||||||
theories
|
theories
|
||||||
"access-control/Dpolicy"
|
"access-control/Dpolicy"
|
||||||
|
|
||||||
|
@ -117,6 +135,7 @@ session DPolicy = DRefine +
|
||||||
|
|
||||||
session Access in "access-control" = AInvs +
|
session Access in "access-control" = AInvs +
|
||||||
theories
|
theories
|
||||||
|
"ADT_AC"
|
||||||
"Syscall_AC"
|
"Syscall_AC"
|
||||||
"ExampleSystem"
|
"ExampleSystem"
|
||||||
|
|
||||||
|
@ -125,6 +144,10 @@ session InfoFlow in "infoflow" = Access +
|
||||||
"InfoFlow_Image_Toplevel"
|
"InfoFlow_Image_Toplevel"
|
||||||
|
|
||||||
session InfoFlowCBase = CRefine +
|
session InfoFlowCBase = CRefine +
|
||||||
|
sessions
|
||||||
|
Refine
|
||||||
|
Access
|
||||||
|
InfoFlow
|
||||||
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
|
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
|
||||||
"infoflow/Include_IF_C"
|
"infoflow/Include_IF_C"
|
||||||
theories
|
theories
|
||||||
|
@ -140,6 +163,9 @@ session InfoFlowC = InfoFlowCBase +
|
||||||
*)
|
*)
|
||||||
|
|
||||||
session SepDSpec = DSpec +
|
session SepDSpec = DSpec +
|
||||||
|
sessions
|
||||||
|
Sep_Algebra
|
||||||
|
SepTactics
|
||||||
theories
|
theories
|
||||||
"sep-capDL/Frame_SD"
|
"sep-capDL/Frame_SD"
|
||||||
|
|
||||||
|
@ -152,6 +178,8 @@ session DSpecProofs in "capDL-api" = SepDSpec +
|
||||||
*)
|
*)
|
||||||
|
|
||||||
session Bisim in bisim = AInvs +
|
session Bisim in bisim = AInvs +
|
||||||
|
sessions
|
||||||
|
ASepSpec
|
||||||
theories
|
theories
|
||||||
"Syscall_S"
|
"Syscall_S"
|
||||||
files
|
files
|
||||||
|
@ -163,11 +191,9 @@ session Bisim in bisim = AInvs +
|
||||||
* Separation Logic
|
* Separation Logic
|
||||||
*)
|
*)
|
||||||
|
|
||||||
session SepTactics = Word_Lib +
|
|
||||||
theories
|
|
||||||
"../lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics"
|
|
||||||
|
|
||||||
session SepTacticsExamples = SepTactics +
|
session SepTacticsExamples = SepTactics +
|
||||||
|
sessions
|
||||||
|
SepDSpec
|
||||||
theories [quick_and_dirty]
|
theories [quick_and_dirty]
|
||||||
"capDL-api/Sep_Tactic_Examples"
|
"capDL-api/Sep_Tactic_Examples"
|
||||||
|
|
||||||
|
|
|
@ -10,7 +10,7 @@
|
||||||
|
|
||||||
theory Deterministic_AC
|
theory Deterministic_AC
|
||||||
imports
|
imports
|
||||||
"../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI"
|
"AInvs.ArchDetSchedSchedule_AI"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(*This theory defines an abstract "integrity" property over
|
(*This theory defines an abstract "integrity" property over
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory DomainSepInv
|
theory DomainSepInv
|
||||||
imports
|
imports
|
||||||
"Ipc_AC" (* for transfer_caps_loop_pres_dest lec_valid_cap' set_simple_ko_get_tcb thread_set_tcb_fault_update_valid_mdb *)
|
"Ipc_AC" (* for transfer_caps_loop_pres_dest lec_valid_cap' set_simple_ko_get_tcb thread_set_tcb_fault_update_valid_mdb *)
|
||||||
"../../lib/Monad_WP/wp/WPBang"
|
"Lib.WPBang"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -11,8 +11,8 @@
|
||||||
theory Dpolicy
|
theory Dpolicy
|
||||||
imports
|
imports
|
||||||
Access
|
Access
|
||||||
"../drefine/Refine_D"
|
"DRefine.Refine_D"
|
||||||
"../drefine/Include_D"
|
"DBaseRefine.Include_D"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(*
|
(*
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Ipc_AC
|
theory Ipc_AC
|
||||||
imports Finalise_AC "../../lib/MonadicRewrite"
|
imports Finalise_AC "Lib.MonadicRewrite"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -13,7 +13,7 @@ theory SEL4GlobalsSwap
|
||||||
imports "../../tools/asmrefine/GlobalsSwap"
|
imports "../../tools/asmrefine/GlobalsSwap"
|
||||||
"../../tools/asmrefine/AsmSemanticsRespects"
|
"../../tools/asmrefine/AsmSemanticsRespects"
|
||||||
"../../tools/asmrefine/FieldAccessors"
|
"../../tools/asmrefine/FieldAccessors"
|
||||||
"../../spec/cspec/Substitute"
|
"CSpec.Substitute"
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory SEL4GraphRefine
|
theory SEL4GraphRefine
|
||||||
imports
|
imports
|
||||||
"../../tools/asmrefine/ProveGraphRefine"
|
"../../tools/asmrefine/ProveGraphRefine"
|
||||||
"../../spec/cspec/Substitute"
|
"CSpec.Substitute"
|
||||||
"SEL4GlobalsSwap"
|
"SEL4GlobalsSwap"
|
||||||
"SEL4SimplExport"
|
"SEL4SimplExport"
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -12,7 +12,7 @@ theory SEL4SimplExport
|
||||||
|
|
||||||
imports
|
imports
|
||||||
"../../tools/asmrefine/SimplExport"
|
"../../tools/asmrefine/SimplExport"
|
||||||
"../../spec/cspec/Substitute"
|
"CSpec.Substitute"
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory TestGraphRefine
|
theory TestGraphRefine
|
||||||
|
|
||||||
imports "../../tools/asmrefine/ProveGraphRefine"
|
imports "../../tools/asmrefine/ProveGraphRefine"
|
||||||
"../../spec/cspec/Substitute"
|
"CSpec.Substitute"
|
||||||
"SEL4GlobalsSwap" "SEL4SimplExport"
|
"SEL4GlobalsSwap" "SEL4SimplExport"
|
||||||
|
|
||||||
begin
|
begin
|
||||||
|
|
|
@ -12,10 +12,10 @@ chapter "Restricted capabilities in the Separation Kernel Abstract Specification
|
||||||
|
|
||||||
theory Separation
|
theory Separation
|
||||||
imports
|
imports
|
||||||
"../../spec/sep-abstract/Syscall_SA"
|
"ASepSpec.Syscall_SA"
|
||||||
"../invariant-abstract/AInvs"
|
"AInvs.AInvs"
|
||||||
"../../lib/Bisim_UL"
|
"Lib.Bisim_UL"
|
||||||
"../../lib/LemmaBucket"
|
"Lib.LemmaBucket"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {*
|
text {*
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
|
|
||||||
theory Kernel_DP
|
theory Kernel_DP
|
||||||
imports
|
imports
|
||||||
"../../spec/capDL/Syscall_D"
|
"DSpec.Syscall_D"
|
||||||
"../sep-capDL/Types_SD"
|
"SepDSpec.Types_SD"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* Bootinfo contructs *)
|
(* Bootinfo contructs *)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory ProofHelpers_DP
|
theory ProofHelpers_DP
|
||||||
imports
|
imports
|
||||||
Kernel_DP
|
Kernel_DP
|
||||||
"../sep-capDL/Frame_SD"
|
"SepDSpec.Frame_SD"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
crunch_ignore (add:
|
crunch_ignore (add:
|
||||||
|
|
|
@ -10,7 +10,7 @@
|
||||||
|
|
||||||
theory Sep_Tactic_Examples
|
theory Sep_Tactic_Examples
|
||||||
imports
|
imports
|
||||||
"../sep-capDL/Sep_Tactic_Helper"
|
"SepDSpec.Sep_Tactic_Helper"
|
||||||
KHeap_DP
|
KHeap_DP
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory ADT_C
|
theory ADT_C
|
||||||
imports
|
imports
|
||||||
Schedule_C Retype_C Recycle_C
|
Schedule_C Retype_C Recycle_C
|
||||||
"../../invariant-abstract/BCorres2_AI"
|
"AInvs.BCorres2_AI"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory BuildRefineCache_C (* FIXME: broken *)
|
theory BuildRefineCache_C (* FIXME: broken *)
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
ML {*
|
ML {*
|
||||||
|
|
|
@ -11,8 +11,8 @@
|
||||||
theory CLevityCatch
|
theory CLevityCatch
|
||||||
imports
|
imports
|
||||||
Include_C
|
Include_C
|
||||||
"../../../lib/LemmaBucket_C"
|
"CLib.LemmaBucket_C"
|
||||||
"../../../lib/LemmaBucket"
|
"Lib.LemmaBucket"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
(* collects lemmas common to the various CSpace branches *)
|
(* collects lemmas common to the various CSpace branches *)
|
||||||
|
|
||||||
theory CSpaceAcc_C
|
theory CSpaceAcc_C
|
||||||
imports "../../refine/$L4V_ARCH/EmptyFail" Ctac_lemmas_C
|
imports "Refine.EmptyFail" Ctac_lemmas_C
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* For resolving schematics *)
|
(* For resolving schematics *)
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory CSpace_RAB_C
|
theory CSpace_RAB_C
|
||||||
imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C"
|
imports CSpaceAcc_C "CLib.MonadicRewrite_C"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context kernel
|
context kernel
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Cache (* FIXME: broken *)
|
theory Cache (* FIXME: broken *)
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {* Enable the proof cache, both skipping from it
|
text {* Enable the proof cache, both skipping from it
|
||||||
|
|
|
@ -12,7 +12,7 @@
|
||||||
|
|
||||||
theory Ctac_lemmas_C
|
theory Ctac_lemmas_C
|
||||||
imports
|
imports
|
||||||
"../../../lib/clib/Ctac"
|
"../lib/Ctac"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context kernel
|
context kernel
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory DetWP
|
theory DetWP
|
||||||
imports "../../../lib/clib/DetWPLib" Include_C
|
imports "CLib.DetWPLib" Include_C
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -14,8 +14,8 @@ imports
|
||||||
SyscallArgs_C
|
SyscallArgs_C
|
||||||
Delete_C
|
Delete_C
|
||||||
Syscall_C
|
Syscall_C
|
||||||
"../../refine/$L4V_ARCH/RAB_FN"
|
"Refine.RAB_FN"
|
||||||
"../../../lib/clib/MonadicRewrite_C"
|
"CLib.MonadicRewrite_C"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
|
|
||||||
theory Include_C
|
theory Include_C
|
||||||
imports
|
imports
|
||||||
"../../../spec/cspec/KernelInc_C"
|
"CSpec.KernelInc_C"
|
||||||
"../../refine/$L4V_ARCH/Refine"
|
"Refine.Refine"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Invoke_C
|
theory Invoke_C
|
||||||
imports Recycle_C "../../../lib/clib/MonadicRewrite_C"
|
imports Recycle_C "CLib.MonadicRewrite_C"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context kernel_m
|
context kernel_m
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory IsolatedThreadAction
|
theory IsolatedThreadAction
|
||||||
imports "../../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
|
imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
|
||||||
begin
|
begin
|
||||||
|
|
||||||
datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
|
datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
(* things that should be moved into first refinement *)
|
(* things that should be moved into first refinement *)
|
||||||
|
|
||||||
theory Move
|
theory Move
|
||||||
imports "../../refine/$L4V_ARCH/Refine"
|
imports "Refine.Refine"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
lemma finaliseCap_Reply:
|
lemma finaliseCap_Reply:
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
chapter "Toplevel Refinement Statement"
|
chapter "Toplevel Refinement Statement"
|
||||||
|
|
||||||
theory Refine_C
|
theory Refine_C
|
||||||
imports Init_C Fastpath_C "../../../lib/clib/CToCRefine"
|
imports Init_C Fastpath_C "../lib/CToCRefine"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -13,7 +13,7 @@ header "Toplevel Refinement Statement for nondeterministic specification"
|
||||||
theory Refine_nondet_C (* FIXME: broken *)
|
theory Refine_nondet_C (* FIXME: broken *)
|
||||||
imports
|
imports
|
||||||
Refine_C
|
Refine_C
|
||||||
"../../invariant-abstract/BCorres2_AI"
|
"AInvs.BCorres2_AI"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
definition (in state_rel)
|
definition (in state_rel)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory SR_lemmas_C
|
theory SR_lemmas_C
|
||||||
imports
|
imports
|
||||||
StateRelation_C
|
StateRelation_C
|
||||||
"../../refine/$L4V_ARCH/Invariants_H"
|
"Refine.Invariants_H"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -13,9 +13,9 @@
|
||||||
|
|
||||||
theory Wellformed_C
|
theory Wellformed_C
|
||||||
imports
|
imports
|
||||||
"../../../lib/CTranslationNICTA"
|
"CLib.CTranslationNICTA"
|
||||||
CLevityCatch
|
CLevityCatch
|
||||||
"../../../spec/cspec/Substitute"
|
"CSpec.Substitute"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
theory ADT_C
|
theory ADT_C
|
||||||
imports
|
imports
|
||||||
Schedule_C Retype_C Recycle_C
|
Schedule_C Retype_C Recycle_C
|
||||||
"../../invariant-abstract/BCorres2_AI"
|
"AInvs.BCorres2_AI"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory BuildRefineCache_C (* FIXME: broken *)
|
theory BuildRefineCache_C (* FIXME: broken *)
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
ML {*
|
ML {*
|
||||||
|
|
|
@ -12,8 +12,8 @@ theory CLevityCatch
|
||||||
imports
|
imports
|
||||||
Include_C
|
Include_C
|
||||||
Move
|
Move
|
||||||
"../../../lib/LemmaBucket_C"
|
"CLib.LemmaBucket_C"
|
||||||
"../../../lib/LemmaBucket"
|
"Lib.LemmaBucket"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
(* collects lemmas common to the various CSpace branches *)
|
(* collects lemmas common to the various CSpace branches *)
|
||||||
|
|
||||||
theory CSpaceAcc_C
|
theory CSpaceAcc_C
|
||||||
imports "../../refine/$L4V_ARCH/EmptyFail" Ctac_lemmas_C
|
imports "Refine.EmptyFail" Ctac_lemmas_C
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* For resolving schematics *)
|
(* For resolving schematics *)
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory CSpace_RAB_C
|
theory CSpace_RAB_C
|
||||||
imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C"
|
imports CSpaceAcc_C "CLib.MonadicRewrite_C"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context kernel
|
context kernel
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Cache (* FIXME: broken *)
|
theory Cache (* FIXME: broken *)
|
||||||
imports "~~/src/HOL/Main"
|
imports Main
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text {* Enable the proof cache, both skipping from it
|
text {* Enable the proof cache, both skipping from it
|
||||||
|
|
|
@ -12,7 +12,7 @@
|
||||||
|
|
||||||
theory Ctac_lemmas_C
|
theory Ctac_lemmas_C
|
||||||
imports
|
imports
|
||||||
"../../../lib/clib/Ctac"
|
"../lib/Ctac"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context kernel
|
context kernel
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory DetWP
|
theory DetWP
|
||||||
imports "../../../lib/clib/DetWPLib" Include_C
|
imports "CLib.DetWPLib" Include_C
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* FIXME YUCK where did you come from *)
|
(* FIXME YUCK where did you come from *)
|
||||||
|
|
|
@ -14,8 +14,8 @@ imports
|
||||||
SyscallArgs_C
|
SyscallArgs_C
|
||||||
Delete_C
|
Delete_C
|
||||||
Syscall_C
|
Syscall_C
|
||||||
"../../refine/$L4V_ARCH/RAB_FN"
|
"Refine.RAB_FN"
|
||||||
"../../../lib/clib/MonadicRewrite_C"
|
"CLib.MonadicRewrite_C"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||||
|
|
|
@ -10,8 +10,8 @@
|
||||||
|
|
||||||
theory Include_C
|
theory Include_C
|
||||||
imports
|
imports
|
||||||
"../../../spec/cspec/KernelInc_C"
|
"CSpec.KernelInc_C"
|
||||||
"../../refine/$L4V_ARCH/Refine"
|
"Refine.Refine"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory Invoke_C
|
theory Invoke_C
|
||||||
imports Recycle_C "../../../lib/clib/MonadicRewrite_C"
|
imports Recycle_C "CLib.MonadicRewrite_C"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
context kernel_m
|
context kernel_m
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
*)
|
*)
|
||||||
|
|
||||||
theory IsolatedThreadAction
|
theory IsolatedThreadAction
|
||||||
imports "../../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
|
imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
|
||||||
begin
|
begin
|
||||||
|
|
||||||
datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
|
datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
(* things that should be moved into first refinement *)
|
(* things that should be moved into first refinement *)
|
||||||
|
|
||||||
theory Move
|
theory Move
|
||||||
imports "../../refine/$L4V_ARCH/Refine"
|
imports "Refine.Refine"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
(* FIXME move: need a theory on top of CSpec that arches can share *)
|
(* FIXME move: need a theory on top of CSpec that arches can share *)
|
||||||
|
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue