diff --git a/ROOTS b/ROOTS index e418c0c34..1610af891 100644 --- a/ROOTS +++ b/ROOTS @@ -6,5 +6,6 @@ proof tools camkes sys-init +lib lib/Word_Lib lib/sep_algebra \ No newline at end of file diff --git a/camkes/ROOT b/camkes/ROOT index 8949f1079..1de760108 100644 --- a/camkes/ROOT +++ b/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. *) session CamkesCdlBase (Camkes) in "adl-spec" = DPolicy + + sessions + DSpec + CamkesAdlSpec + Lib theories - (* DSpec *) - "../spec/capDL/Syscall_D" - (* CamkesAdlSpec *) - "Wellformed_CAMKES" - "Examples_CAMKES" - (* Lemma buckets *) - "../../lib/LemmaBucket" + "DSpec.Syscall_D" + "CamkesAdlSpec.Wellformed_CAMKES" + "CamkesAdlSpec.Examples_CAMKES" + "Lib.LemmaBucket" (* CAmkES<->CapDL reasoning. *) session CamkesCdlRefine (Camkes) in "cdl-refine" = CamkesCdlBase + diff --git a/camkes/cdl-refine/Generator_CAMKES_CDL.thy b/camkes/cdl-refine/Generator_CAMKES_CDL.thy index 94e9ed433..452e3b31b 100644 --- a/camkes/cdl-refine/Generator_CAMKES_CDL.thy +++ b/camkes/cdl-refine/Generator_CAMKES_CDL.thy @@ -11,9 +11,9 @@ theory Generator_CAMKES_CDL imports "../adl-spec/Types_CAMKES" "../adl-spec/Library_CAMKES" - "../../spec/capDL/Syscall_D" + "DSpec.Syscall_D" Types_CAMKES_CDL - "../../proof/access-control/Dpolicy" + "DPolicy.Dpolicy" begin text {* diff --git a/camkes/cdl-refine/Types_CAMKES_CDL.thy b/camkes/cdl-refine/Types_CAMKES_CDL.thy index 5aa697143..7f3b95916 100644 --- a/camkes/cdl-refine/Types_CAMKES_CDL.thy +++ b/camkes/cdl-refine/Types_CAMKES_CDL.thy @@ -11,7 +11,7 @@ theory Types_CAMKES_CDL imports "../adl-spec/Types_CAMKES" "../adl-spec/Library_CAMKES" - "../../spec/capDL/Syscall_D" + "DSpec.Syscall_D" begin (* placeholder for things to fill in *) diff --git a/camkes/glue-proofs/DataIn.thy b/camkes/glue-proofs/DataIn.thy index 96a47fd7c..ea782541f 100644 --- a/camkes/glue-proofs/DataIn.thy +++ b/camkes/glue-proofs/DataIn.thy @@ -10,8 +10,8 @@ chapter {* Shared Memory *} (*<*) theory DataIn imports - "../../tools/c-parser/CTranslation" - "../../tools/autocorres/AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin (* THIS THEORY IS GENERATED. DO NOT EDIT. *) diff --git a/camkes/glue-proofs/EventFrom.thy b/camkes/glue-proofs/EventFrom.thy index 01bb624c7..d90a6d330 100644 --- a/camkes/glue-proofs/EventFrom.thy +++ b/camkes/glue-proofs/EventFrom.thy @@ -11,8 +11,8 @@ chapter {* Event Send *} (*<*) theory EventFrom imports - "../../tools/c-parser/CTranslation" - "../../tools/autocorres/AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin (* THIS THEORY IS GENERATED. DO NOT EDIT. *) diff --git a/camkes/glue-proofs/EventTo.thy b/camkes/glue-proofs/EventTo.thy index bb382ca73..16a736b24 100644 --- a/camkes/glue-proofs/EventTo.thy +++ b/camkes/glue-proofs/EventTo.thy @@ -10,8 +10,8 @@ chapter {* Event Receive *} (*<*) theory EventTo imports - "../../tools/c-parser/CTranslation" - "../../tools/autocorres/AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin (* THIS THEORY IS GENERATED. DO NOT EDIT. *) diff --git a/camkes/glue-proofs/RPCFrom.thy b/camkes/glue-proofs/RPCFrom.thy index ce9af2ecb..6d747e71c 100644 --- a/camkes/glue-proofs/RPCFrom.thy +++ b/camkes/glue-proofs/RPCFrom.thy @@ -9,8 +9,8 @@ *) (*<*) theory RPCFrom imports - "../../tools/c-parser/CTranslation" - "../../tools/autocorres/AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin (* THIS THEORY IS GENERATED. DO NOT EDIT. *) diff --git a/camkes/glue-proofs/RPCTo.thy b/camkes/glue-proofs/RPCTo.thy index 8bc6c3453..7fead7d9e 100644 --- a/camkes/glue-proofs/RPCTo.thy +++ b/camkes/glue-proofs/RPCTo.thy @@ -10,8 +10,8 @@ chapter {* RPC Receive *} (*<*) theory RPCTo imports - "../../tools/c-parser/CTranslation" - "../../tools/autocorres/AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin (* THIS THEORY IS GENERATED. DO NOT EDIT. *) diff --git a/camkes/glue-proofs/Syntax.thy b/camkes/glue-proofs/Syntax.thy index 432fefb90..5393ef4bc 100644 --- a/camkes/glue-proofs/Syntax.thy +++ b/camkes/glue-proofs/Syntax.thy @@ -10,8 +10,8 @@ chapter {* Syntax *} (*<*) theory Syntax imports - "../../tools/c-parser/CTranslation" - "../../tools/autocorres/AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin (*>*) diff --git a/lib/AdjustSchematic.thy b/lib/AdjustSchematic.thy index 0ce0ed8ee..7a3e871fe 100644 --- a/lib/AdjustSchematic.thy +++ b/lib/AdjustSchematic.thy @@ -9,7 +9,7 @@ *) theory AdjustSchematic (* FIXME: bitrotted *) -imports "~~/src/HOL/Main" +imports Main begin lemma meta_arg_cong: diff --git a/lib/Apply_Debug.thy b/lib/Apply_Debug.thy index fff1c3d7e..fea9467fa 100644 --- a/lib/Apply_Debug.thy +++ b/lib/Apply_Debug.thy @@ -10,8 +10,11 @@ *) theory Apply_Debug - imports Apply_Trace "~~/src/HOL/Eisbach/Eisbach_Tools" - keywords "apply_debug" :: "prf_script" % "proof" and + imports + Apply_Trace + "HOL-Eisbach.Eisbach_Tools" + keywords + "apply_debug" :: "prf_script" % "proof" and "continue" :: prf_script % "proof" and "finish" :: prf_script % "proof" begin diff --git a/lib/CorresK_Lemmas.thy b/lib/CorresK_Lemmas.thy index 39b89f373..ff8a3e08e 100644 --- a/lib/CorresK_Lemmas.thy +++ b/lib/CorresK_Lemmas.thy @@ -11,7 +11,10 @@ theory CorresK_Lemmas -imports Corres_Method "../spec/design/Syscall_H" "../spec/abstract/Syscall_A" +imports + Corres_Method + "ExecSpec.Syscall_H" + "ASpec.Syscall_A" begin lemma corres_throwError_str [corres_concrete_rER]: diff --git a/lib/Corres_Test.thy b/lib/Corres_Test.thy index bd0bee124..0df6e5a49 100755 --- a/lib/Corres_Test.thy +++ b/lib/Corres_Test.thy @@ -14,7 +14,7 @@ *) theory Corres_Test -imports "../proof/refine/ARM/VSpace_R" Corres_Method +imports "Refine.VSpace_R" Corres_Method begin chapter \The Corres Method\ diff --git a/lib/DataMap.thy b/lib/DataMap.thy index 316ce165c..9fb7bd0af 100644 --- a/lib/DataMap.thy +++ b/lib/DataMap.thy @@ -9,7 +9,7 @@ *) theory DataMap -imports "~~/src/HOL/Main" +imports Main begin type_synonym ('k, 'a) map = "'k \ 'a" diff --git a/lib/Eisbach_Methods.thy b/lib/Eisbach_Methods.thy index e38de49b6..3e6c6cafc 100644 --- a/lib/Eisbach_Methods.thy +++ b/lib/Eisbach_Methods.thy @@ -13,9 +13,10 @@ *) theory Eisbach_Methods -imports "subgoal_focus/Subgoal_Methods" - "~~/src/HOL/Eisbach/Eisbach_Tools" - Rule_By_Method +imports + "subgoal_focus/Subgoal_Methods" + "HOL-Eisbach.Eisbach_Tools" + Rule_By_Method begin diff --git a/lib/ExpandAll.thy b/lib/ExpandAll.thy index 0109b4df5..f86151b27 100644 --- a/lib/ExpandAll.thy +++ b/lib/ExpandAll.thy @@ -9,7 +9,7 @@ *) theory ExpandAll (* FIXME: bitrotted *) -imports "~~/src/HOL/Main" +imports Main begin lemma expand_forall: diff --git a/lib/GenericLib_C.thy b/lib/GenericLib_C.thy deleted file mode 100644 index f3eacb045..000000000 --- a/lib/GenericLib_C.thy +++ /dev/null @@ -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 diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy index 82a2b1f4a..4e42a6476 100644 --- a/lib/HaskellLib_H.thy +++ b/lib/HaskellLib_H.thy @@ -16,7 +16,7 @@ theory HaskellLib_H imports Lib - "$L4V_ARCH/WordSetup" + "Word_Lib.WordSetup" "Monad_WP/NonDetMonadVCG" begin diff --git a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy index 3630cd619..1f8030f63 100644 --- a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy +++ b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy @@ -10,8 +10,8 @@ theory Hoare_Sep_Tactics imports - "../Monad_WP/NonDetMonadVCG" - "../sep_algebra/Sep_Algebra_L4v" + "Lib.NonDetMonadVCG" + "Sep_Algebra.Sep_Algebra_L4v" begin (* FIXME: needs cleanup *) diff --git a/lib/Insulin.thy b/lib/Insulin.thy index b20d62ad9..1ee90479f 100644 --- a/lib/Insulin.thy +++ b/lib/Insulin.thy @@ -49,7 +49,8 @@ * - Naive algorithm, takes \quadratic time. *) -theory Insulin imports HOL +theory Insulin + imports Main keywords "desugar_term" "desugar_thm" "desugar_goal" :: diag begin diff --git a/lib/Lib.thy b/lib/Lib.thy index 15c652c7a..1047928f5 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -22,7 +22,7 @@ imports Extract_Conjunct Eval_Bool NICTATools - "~~/src/HOL/Library/Prefix_Order" + "HOL-Library.Prefix_Order" begin (* FIXME: eliminate *) diff --git a/lib/List_Lib.thy b/lib/List_Lib.thy index 8430b2a02..edf82a524 100644 --- a/lib/List_Lib.thy +++ b/lib/List_Lib.thy @@ -11,7 +11,7 @@ chapter "List Manipulation Functions" theory List_Lib -imports "~~/src/HOL/Main" +imports Main begin definition list_replace :: "'a list \ 'a \ 'a \ 'a list" where diff --git a/lib/Monad_WP/wp/WP_Pre.thy b/lib/Monad_WP/wp/WP_Pre.thy index 7e513e209..abfeb7086 100644 --- a/lib/Monad_WP/wp/WP_Pre.thy +++ b/lib/Monad_WP/wp/WP_Pre.thy @@ -10,8 +10,8 @@ theory WP_Pre imports - "~~/src/HOL/Main" - "~~/src/HOL/Eisbach/Eisbach_Tools" + Main + "HOL-Eisbach.Eisbach_Tools" begin named_theorems wp_pre diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index 9d9e6ec4c..426aef546 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -13,8 +13,8 @@ imports "Monad_WP/NonDetMonadVCG" "MonadEq" "Monad_WP/WhileLoopRulesCompleteness" - Distinct_Prop - "~~/src/HOL/Word/Word_Miscellaneous" + "Word_Lib.Distinct_Prop" + "HOL-Word.Word_Miscellaneous" begin setup \AutoLevity_Base.add_attribute_test "wp" WeakestPre.is_wp_rule\ diff --git a/lib/RISCV64/WordSetup.thy b/lib/RISCV64/WordSetup.thy index 67ca62e0c..f3e64ac84 100644 --- a/lib/RISCV64/WordSetup.thy +++ b/lib/RISCV64/WordSetup.thy @@ -9,7 +9,7 @@ *) -theory WordSetup +theory WordSetup (* part of non-AFP Word_Lib *) imports "../Distinct_Prop" "../Word_Lib/Word_Lemmas_64" diff --git a/lib/ROOT b/lib/ROOT new file mode 100644 index 000000000..45715c189 --- /dev/null +++ b/lib/ROOT @@ -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" diff --git a/lib/Rule_By_Method.thy b/lib/Rule_By_Method.thy index 05fda6cc6..f32f8e54f 100644 --- a/lib/Rule_By_Method.thy +++ b/lib/Rule_By_Method.thy @@ -11,7 +11,7 @@ theory Rule_By_Method imports Main - "~~/src/HOL/Eisbach/Eisbach_Tools" + "HOL-Eisbach.Eisbach_Tools" begin ML \ diff --git a/lib/SimpStrategy.thy b/lib/SimpStrategy.thy index 1d81e1fe6..447ec18c8 100644 --- a/lib/SimpStrategy.thy +++ b/lib/SimpStrategy.thy @@ -9,7 +9,7 @@ *) theory SimpStrategy -imports "~~/src/HOL/Main" +imports Main begin text {* diff --git a/lib/Simulation.thy b/lib/Simulation.thy index 0bfe1e698..6f7ff0110 100644 --- a/lib/Simulation.thy +++ b/lib/Simulation.thy @@ -15,7 +15,7 @@ chapter "Refinement" theory Simulation -imports "~~/src/HOL/Main" +imports Main begin text {* diff --git a/lib/SplitRule.thy b/lib/SplitRule.thy index 4abdb1dd2..294ae5b5f 100644 --- a/lib/SplitRule.thy +++ b/lib/SplitRule.thy @@ -9,7 +9,7 @@ *) theory SplitRule -imports "~~/src/HOL/Main" +imports Main begin ML {* diff --git a/lib/StringOrd.thy b/lib/StringOrd.thy index d95445cb0..f2ce9ce0a 100644 --- a/lib/StringOrd.thy +++ b/lib/StringOrd.thy @@ -9,7 +9,7 @@ *) theory StringOrd -imports "~~/src/HOL/Main" +imports Main begin datatype anotherBL = diff --git a/lib/Time_Methods_Cmd_Test.thy b/lib/Time_Methods_Cmd_Test.thy index 8607567e4..8855c547b 100644 --- a/lib/Time_Methods_Cmd_Test.thy +++ b/lib/Time_Methods_Cmd_Test.thy @@ -11,7 +11,7 @@ theory Time_Methods_Cmd_Test imports Time_Methods_Cmd Eisbach_Methods - "~~/src/HOL/Library/Sublist" + "HOL-Library.Sublist" begin text \ diff --git a/lib/WPTutorial.thy b/lib/WPTutorial.thy index ded24e750..98b221c22 100644 --- a/lib/WPTutorial.thy +++ b/lib/WPTutorial.thy @@ -9,7 +9,7 @@ *) theory WPTutorial -imports "../proof/refine/$L4V_ARCH/Bits_R" +imports "Refine.Bits_R" begin text {* diff --git a/lib/clib/AutoCorresCRefine.thy b/lib/clib/AutoCorresCRefine.thy index 700ec60b9..00a848851 100644 --- a/lib/clib/AutoCorresCRefine.thy +++ b/lib/clib/AutoCorresCRefine.thy @@ -9,9 +9,7 @@ *) theory AutoCorresCRefine - -imports Ctac "../../tools/autocorres/LegacyAutoCorres" - +imports Ctac LegacyAutoCorres begin context kernel begin diff --git a/lib/BitFieldProofsLib.thy b/lib/clib/BitFieldProofsLib.thy similarity index 99% rename from lib/BitFieldProofsLib.thy rename to lib/clib/BitFieldProofsLib.thy index e5bb8d090..90726c41d 100644 --- a/lib/BitFieldProofsLib.thy +++ b/lib/clib/BitFieldProofsLib.thy @@ -10,7 +10,7 @@ theory BitFieldProofsLib imports - Eisbach_Methods + "Lib.Eisbach_Methods" TypHeapLib begin diff --git a/lib/clib/CCorres_Rewrite.thy b/lib/clib/CCorres_Rewrite.thy index d66baa815..c670f3869 100644 --- a/lib/clib/CCorres_Rewrite.thy +++ b/lib/clib/CCorres_Rewrite.thy @@ -11,9 +11,7 @@ *) theory CCorres_Rewrite -imports - "Corres_UL_C" - "Simpl_Rewrite" +imports Corres_UL_C Simpl_Rewrite begin text \A simple proof method for rewriting Simpl programs under @{term ccorres_underlying}.\ diff --git a/lib/CTranslationNICTA.thy b/lib/clib/CTranslationNICTA.thy similarity index 93% rename from lib/CTranslationNICTA.thy rename to lib/clib/CTranslationNICTA.thy index 9e44585a9..f10c33486 100644 --- a/lib/CTranslationNICTA.thy +++ b/lib/clib/CTranslationNICTA.thy @@ -10,8 +10,8 @@ theory CTranslationNICTA imports - "../tools/c-parser/CTranslation" - "Word_Lib/Word_Lib" + "CParser.CTranslation" + "Word_Lib.Word_Lib" begin declare len_of_numeral_defs [simp del] diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index bc863c353..b0b8d69fd 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -15,9 +15,9 @@ theory Corres_UL_C imports - "../LemmaBucket_C" - "../LemmaBucket" - "../SIMPL_Lemmas" + "LemmaBucket_C" + "Lib.LemmaBucket" + "SIMPL_Lemmas" begin declare word_neq_0_conv [simp del] diff --git a/lib/clib/DetWPLib.thy b/lib/clib/DetWPLib.thy index 48c974626..27de0e558 100644 --- a/lib/clib/DetWPLib.thy +++ b/lib/clib/DetWPLib.thy @@ -9,7 +9,7 @@ *) theory DetWPLib -imports "../GenericLib_C" +imports "Lib.HaskellLemmaBucket" begin definition diff --git a/tools/autocorres/LegacyAutoCorres.thy b/lib/clib/LegacyAutoCorres.thy similarity index 98% rename from tools/autocorres/LegacyAutoCorres.thy rename to lib/clib/LegacyAutoCorres.thy index 22b878165..c7812a343 100644 --- a/tools/autocorres/LegacyAutoCorres.thy +++ b/lib/clib/LegacyAutoCorres.thy @@ -10,7 +10,7 @@ theory LegacyAutoCorres -imports AutoCorres "../../lib/clib/Corres_UL_C" +imports "AutoCorres.AutoCorres" "Corres_UL_C" begin diff --git a/lib/LemmaBucket_C.thy b/lib/clib/LemmaBucket_C.thy similarity index 99% rename from lib/LemmaBucket_C.thy rename to lib/clib/LemmaBucket_C.thy index b6cc59bec..66b1c2f8d 100644 --- a/lib/LemmaBucket_C.thy +++ b/lib/clib/LemmaBucket_C.thy @@ -10,10 +10,10 @@ theory LemmaBucket_C imports - Lib - "$L4V_ARCH/WordSetup" + "Lib.Lib" + "Word_Lib.WordSetup" TypHeapLib - "../tools/c-parser/umm_heap/ArrayAssertion" + "CParser.ArrayAssertion" begin declare word_neq_0_conv [simp del] diff --git a/lib/clib/MonadicRewrite_C.thy b/lib/clib/MonadicRewrite_C.thy index 3dc99fd48..87b18a520 100644 --- a/lib/clib/MonadicRewrite_C.thy +++ b/lib/clib/MonadicRewrite_C.thy @@ -12,7 +12,7 @@ theory MonadicRewrite_C imports - "../MonadicRewrite" + "Lib.MonadicRewrite" Corres_UL_C begin diff --git a/lib/SIMPL_Lemmas.thy b/lib/clib/SIMPL_Lemmas.thy similarity index 99% rename from lib/SIMPL_Lemmas.thy rename to lib/clib/SIMPL_Lemmas.thy index be0d15d57..a16c0c238 100644 --- a/lib/SIMPL_Lemmas.thy +++ b/lib/clib/SIMPL_Lemmas.thy @@ -10,7 +10,7 @@ theory SIMPL_Lemmas imports - "GenericLib_C" + "Lib.HaskellLemmaBucket" "CTranslationNICTA" begin diff --git a/lib/SimplRewrite.thy b/lib/clib/SimplRewrite.thy similarity index 99% rename from lib/SimplRewrite.thy rename to lib/clib/SimplRewrite.thy index 86e245cfd..b438a9d82 100644 --- a/lib/SimplRewrite.thy +++ b/lib/clib/SimplRewrite.thy @@ -11,8 +11,8 @@ theory SimplRewrite imports "CTranslationNICTA" - "SplitRule" - "~~/src/HOL/Eisbach/Eisbach" + "Lib.SplitRule" + "HOL-Eisbach.Eisbach" begin primrec diff --git a/lib/clib/Simpl_Rewrite.thy b/lib/clib/Simpl_Rewrite.thy index 0f15d6e2f..67541b9be 100644 --- a/lib/clib/Simpl_Rewrite.thy +++ b/lib/clib/Simpl_Rewrite.thy @@ -15,9 +15,9 @@ text \A simple proof method for rewriting Simpl programs under a predicate theory Simpl_Rewrite imports - "../../tools/c-parser/Simpl/Vcg" - "../Eisbach_Methods" - "../Apply_Debug" + "Simpl-VCG.Vcg" + "Lib.Eisbach_Methods" + "Lib.Apply_Debug" begin text \Definitions and lemmas for reasoning about equivalence of Simpl programs.\ diff --git a/lib/TypHeapLib.thy b/lib/clib/TypHeapLib.thy similarity index 99% rename from lib/TypHeapLib.thy rename to lib/clib/TypHeapLib.thy index e4ae064ba..7629e880c 100644 --- a/lib/TypHeapLib.thy +++ b/lib/clib/TypHeapLib.thy @@ -9,7 +9,7 @@ *) theory TypHeapLib -imports "../tools/c-parser/CTranslation" +imports "CParser.CTranslation" begin (* This file contains everything you need to know and use for the diff --git a/lib/XPres.thy b/lib/clib/XPres.thy similarity index 100% rename from lib/XPres.thy rename to lib/clib/XPres.thy diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy index 0c9af7a4a..51b58e5d4 100644 --- a/lib/concurrency/Prefix_Refinement.thy +++ b/lib/concurrency/Prefix_Refinement.thy @@ -11,7 +11,7 @@ theory Prefix_Refinement imports Triv_Refinement - "../Monad_WP/TraceMonadLemmas" + "Lib.TraceMonadLemmas" begin diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy index 4ff76dd5b..191df4a72 100644 --- a/lib/concurrency/Triv_Refinement.thy +++ b/lib/concurrency/Triv_Refinement.thy @@ -10,8 +10,8 @@ theory Triv_Refinement imports - "../Monad_WP/TraceMonadVCG" - "../Monad_WP/Strengthen" + "Lib.TraceMonadVCG" + "Lib.Strengthen" begin diff --git a/lib/sep_algebra/Map_Extra.thy b/lib/sep_algebra/Map_Extra.thy index 886c39dde..e61002f5a 100644 --- a/lib/sep_algebra/Map_Extra.thy +++ b/lib/sep_algebra/Map_Extra.thy @@ -16,7 +16,7 @@ chapter {* More properties of maps plus map disjuction. *} theory Map_Extra -imports "~~/src/HOL/Main" +imports Main begin text {* diff --git a/lib/sep_algebra/MonadSep.thy b/lib/sep_algebra/MonadSep.thy index c92076520..b9304b2da 100644 --- a/lib/sep_algebra/MonadSep.thy +++ b/lib/sep_algebra/MonadSep.thy @@ -11,7 +11,7 @@ theory MonadSep imports Sep_Algebra_L4v - "../LemmaBucket" + "Lib.LemmaBucket" begin locale sep_lifted = diff --git a/lib/sep_algebra/ROOT b/lib/sep_algebra/ROOT index cbef0c0cb..ca898b865 100644 --- a/lib/sep_algebra/ROOT +++ b/lib/sep_algebra/ROOT @@ -11,7 +11,11 @@ chapter Lib (* 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 "Generic_Separation_Algebras" "MonadSep" diff --git a/lib/sep_algebra/Separation_Algebra.thy b/lib/sep_algebra/Separation_Algebra.thy index 0ff42b538..e125f28ce 100644 --- a/lib/sep_algebra/Separation_Algebra.thy +++ b/lib/sep_algebra/Separation_Algebra.thy @@ -18,7 +18,7 @@ chapter "Abstract Separation Algebra" theory Separation_Algebra imports Arbitrary_Comm_Monoid - "~~/src/Tools/Adhoc_Overloading" + "HOL-Library.Adhoc_Overloading" begin text {* This theory is the main abstract separation algebra development *} diff --git a/lib/sep_algebra/Separation_Algebra_Alt.thy b/lib/sep_algebra/Separation_Algebra_Alt.thy index 1bbbed43e..cb83f840d 100644 --- a/lib/sep_algebra/Separation_Algebra_Alt.thy +++ b/lib/sep_algebra/Separation_Algebra_Alt.thy @@ -16,7 +16,7 @@ chapter "Abstract Separation Logic, Alternative Definition" theory Separation_Algebra_Alt -imports "~~/src/HOL/Main" +imports Main begin text {* diff --git a/lib/sep_algebra/ex/Simple_Separation_Example.thy b/lib/sep_algebra/ex/Simple_Separation_Example.thy index 6f7ddf985..9f3f8768c 100644 --- a/lib/sep_algebra/ex/Simple_Separation_Example.thy +++ b/lib/sep_algebra/ex/Simple_Separation_Example.thy @@ -18,7 +18,7 @@ chapter "Example from HOL/Hoare/Separation" theory Simple_Separation_Example imports - "~~/src/HOL/Hoare/Hoare_Logic_Abort" + "HOL-Hoare.Hoare_Logic_Abort" "../Sep_Heap_Instance" "../Sep_Tactics" begin diff --git a/lib/sep_algebra/ex/capDL/Types_D.thy b/lib/sep_algebra/ex/capDL/Types_D.thy index a0aea3517..0d6d2c59d 100644 --- a/lib/sep_algebra/ex/capDL/Types_D.thy +++ b/lib/sep_algebra/ex/capDL/Types_D.thy @@ -16,7 +16,7 @@ chapter "A simplified version of the actual capDL specification." theory Types_D -imports "~~/src/HOL/Word/Word" +imports "HOL-Word.Word" begin (* diff --git a/proof/ROOT b/proof/ROOT index f4ab418eb..a91d94f72 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -32,12 +32,22 @@ chapter "Proofs" session Refine = BaseRefine + description {* Refinement between Haskell and Abstract spec. *} + sessions + Lib + CorresK + AInvs theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty] "refine/$L4V_ARCH/Refine" + "refine/$L4V_ARCH/RAB_FN" + "refine/$L4V_ARCH/EmptyFail_H" theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs] "refine/$L4V_ARCH/Refine" + "refine/$L4V_ARCH/RAB_FN" + "refine/$L4V_ARCH/EmptyFail_H" theories "refine/$L4V_ARCH/Refine" + "refine/$L4V_ARCH/RAB_FN" + "refine/$L4V_ARCH/EmptyFail_H" theories [condition = "L4V_ARCH_IS_ARM"] "refine/$L4V_ARCH/Orphanage" @@ -83,12 +93,16 @@ session CRefine = CBaseRefine + "crefine/$L4V_ARCH/Refine_C" session CBaseRefine = CSpec + + sessions + CLib + Refine + AutoCorres theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs] (* ../lib/clib/AutoCorres_C explains why L4VerifiedLinks is included here. *) - "../tools/autocorres/L4VerifiedLinks" + "crefine/lib/L4VerifiedLinks" "crefine/$L4V_ARCH/Include_C" theories - "../tools/autocorres/L4VerifiedLinks" + "crefine/lib/L4VerifiedLinks" "crefine/$L4V_ARCH/Include_C" session AutoCorresCRefine = CRefine + @@ -100,6 +114,8 @@ session AutoCorresCRefine = CRefine + *) session DBaseRefine = Refine + + sessions + DSpec theories "drefine/Include_D" @@ -108,6 +124,8 @@ session DRefine = DBaseRefine + "drefine/Refine_D" session DPolicy = DRefine + + sessions + Access theories "access-control/Dpolicy" @@ -117,6 +135,7 @@ session DPolicy = DRefine + session Access in "access-control" = AInvs + theories + "ADT_AC" "Syscall_AC" "ExampleSystem" @@ -125,6 +144,10 @@ session InfoFlow in "infoflow" = Access + "InfoFlow_Image_Toplevel" session InfoFlowCBase = CRefine + + sessions + Refine + Access + InfoFlow theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs] "infoflow/Include_IF_C" theories @@ -140,6 +163,9 @@ session InfoFlowC = InfoFlowCBase + *) session SepDSpec = DSpec + + sessions + Sep_Algebra + SepTactics theories "sep-capDL/Frame_SD" @@ -152,6 +178,8 @@ session DSpecProofs in "capDL-api" = SepDSpec + *) session Bisim in bisim = AInvs + + sessions + ASepSpec theories "Syscall_S" files @@ -163,11 +191,9 @@ session Bisim in bisim = AInvs + * Separation Logic *) -session SepTactics = Word_Lib + - theories - "../lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics" - session SepTacticsExamples = SepTactics + + sessions + SepDSpec theories [quick_and_dirty] "capDL-api/Sep_Tactic_Examples" diff --git a/proof/access-control/Deterministic_AC.thy b/proof/access-control/Deterministic_AC.thy index db6e59b7c..319bd5996 100644 --- a/proof/access-control/Deterministic_AC.thy +++ b/proof/access-control/Deterministic_AC.thy @@ -10,7 +10,7 @@ theory Deterministic_AC imports - "../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI" + "AInvs.ArchDetSchedSchedule_AI" begin (*This theory defines an abstract "integrity" property over diff --git a/proof/access-control/DomainSepInv.thy b/proof/access-control/DomainSepInv.thy index a3ff3d9e9..a7a39f517 100644 --- a/proof/access-control/DomainSepInv.thy +++ b/proof/access-control/DomainSepInv.thy @@ -11,7 +11,7 @@ theory DomainSepInv imports "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 context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/access-control/Dpolicy.thy b/proof/access-control/Dpolicy.thy index 17e86788c..52d885b16 100644 --- a/proof/access-control/Dpolicy.thy +++ b/proof/access-control/Dpolicy.thy @@ -11,8 +11,8 @@ theory Dpolicy imports Access - "../drefine/Refine_D" - "../drefine/Include_D" + "DRefine.Refine_D" + "DBaseRefine.Include_D" begin (* diff --git a/proof/access-control/Ipc_AC.thy b/proof/access-control/Ipc_AC.thy index 1958b449e..b75a000e8 100644 --- a/proof/access-control/Ipc_AC.thy +++ b/proof/access-control/Ipc_AC.thy @@ -9,7 +9,7 @@ *) theory Ipc_AC -imports Finalise_AC "../../lib/MonadicRewrite" +imports Finalise_AC "Lib.MonadicRewrite" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/asmrefine/SEL4GlobalsSwap.thy b/proof/asmrefine/SEL4GlobalsSwap.thy index 088a78be0..c8d476f18 100644 --- a/proof/asmrefine/SEL4GlobalsSwap.thy +++ b/proof/asmrefine/SEL4GlobalsSwap.thy @@ -13,7 +13,7 @@ theory SEL4GlobalsSwap imports "../../tools/asmrefine/GlobalsSwap" "../../tools/asmrefine/AsmSemanticsRespects" "../../tools/asmrefine/FieldAccessors" - "../../spec/cspec/Substitute" + "CSpec.Substitute" begin diff --git a/proof/asmrefine/SEL4GraphRefine.thy b/proof/asmrefine/SEL4GraphRefine.thy index 6794b8a4f..ed913ddba 100644 --- a/proof/asmrefine/SEL4GraphRefine.thy +++ b/proof/asmrefine/SEL4GraphRefine.thy @@ -11,7 +11,7 @@ theory SEL4GraphRefine imports "../../tools/asmrefine/ProveGraphRefine" - "../../spec/cspec/Substitute" + "CSpec.Substitute" "SEL4GlobalsSwap" "SEL4SimplExport" begin diff --git a/proof/asmrefine/SEL4SimplExport.thy b/proof/asmrefine/SEL4SimplExport.thy index b91d1a152..8ddd48eb1 100644 --- a/proof/asmrefine/SEL4SimplExport.thy +++ b/proof/asmrefine/SEL4SimplExport.thy @@ -12,7 +12,7 @@ theory SEL4SimplExport imports "../../tools/asmrefine/SimplExport" - "../../spec/cspec/Substitute" + "CSpec.Substitute" begin diff --git a/proof/asmrefine/TestGraphRefine.thy b/proof/asmrefine/TestGraphRefine.thy index d9e75dcfd..883286864 100644 --- a/proof/asmrefine/TestGraphRefine.thy +++ b/proof/asmrefine/TestGraphRefine.thy @@ -11,7 +11,7 @@ theory TestGraphRefine imports "../../tools/asmrefine/ProveGraphRefine" - "../../spec/cspec/Substitute" + "CSpec.Substitute" "SEL4GlobalsSwap" "SEL4SimplExport" begin diff --git a/proof/bisim/Separation.thy b/proof/bisim/Separation.thy index 6c26c6a3f..d51f7cb3d 100644 --- a/proof/bisim/Separation.thy +++ b/proof/bisim/Separation.thy @@ -12,10 +12,10 @@ chapter "Restricted capabilities in the Separation Kernel Abstract Specification theory Separation imports - "../../spec/sep-abstract/Syscall_SA" - "../invariant-abstract/AInvs" - "../../lib/Bisim_UL" - "../../lib/LemmaBucket" + "ASepSpec.Syscall_SA" + "AInvs.AInvs" + "Lib.Bisim_UL" + "Lib.LemmaBucket" begin text {* diff --git a/proof/capDL-api/Kernel_DP.thy b/proof/capDL-api/Kernel_DP.thy index 1780c74f2..3de47d9f0 100644 --- a/proof/capDL-api/Kernel_DP.thy +++ b/proof/capDL-api/Kernel_DP.thy @@ -10,8 +10,8 @@ theory Kernel_DP imports - "../../spec/capDL/Syscall_D" - "../sep-capDL/Types_SD" + "DSpec.Syscall_D" + "SepDSpec.Types_SD" begin (* Bootinfo contructs *) diff --git a/proof/capDL-api/ProofHelpers_DP.thy b/proof/capDL-api/ProofHelpers_DP.thy index 38de36250..a6e4c1b2f 100644 --- a/proof/capDL-api/ProofHelpers_DP.thy +++ b/proof/capDL-api/ProofHelpers_DP.thy @@ -11,7 +11,7 @@ theory ProofHelpers_DP imports Kernel_DP - "../sep-capDL/Frame_SD" + "SepDSpec.Frame_SD" begin crunch_ignore (add: diff --git a/proof/capDL-api/Sep_Tactic_Examples.thy b/proof/capDL-api/Sep_Tactic_Examples.thy index 0fd6b0b8b..6ffc16aca 100644 --- a/proof/capDL-api/Sep_Tactic_Examples.thy +++ b/proof/capDL-api/Sep_Tactic_Examples.thy @@ -10,7 +10,7 @@ theory Sep_Tactic_Examples imports - "../sep-capDL/Sep_Tactic_Helper" + "SepDSpec.Sep_Tactic_Helper" KHeap_DP begin diff --git a/proof/crefine/ARM/ADT_C.thy b/proof/crefine/ARM/ADT_C.thy index 5df3a88ca..c52d120b7 100644 --- a/proof/crefine/ARM/ADT_C.thy +++ b/proof/crefine/ARM/ADT_C.thy @@ -11,7 +11,7 @@ theory ADT_C imports Schedule_C Retype_C Recycle_C - "../../invariant-abstract/BCorres2_AI" + "AInvs.BCorres2_AI" begin diff --git a/proof/crefine/ARM/BuildRefineCache_C.thy b/proof/crefine/ARM/BuildRefineCache_C.thy index d2a73c408..2565f8d3e 100644 --- a/proof/crefine/ARM/BuildRefineCache_C.thy +++ b/proof/crefine/ARM/BuildRefineCache_C.thy @@ -9,7 +9,7 @@ *) theory BuildRefineCache_C (* FIXME: broken *) -imports "~~/src/HOL/Main" +imports Main begin ML {* diff --git a/proof/crefine/ARM/CLevityCatch.thy b/proof/crefine/ARM/CLevityCatch.thy index b0de967a6..4b19a18b8 100644 --- a/proof/crefine/ARM/CLevityCatch.thy +++ b/proof/crefine/ARM/CLevityCatch.thy @@ -11,8 +11,8 @@ theory CLevityCatch imports Include_C - "../../../lib/LemmaBucket_C" - "../../../lib/LemmaBucket" + "CLib.LemmaBucket_C" + "Lib.LemmaBucket" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM/CSpaceAcc_C.thy b/proof/crefine/ARM/CSpaceAcc_C.thy index 29401a103..e8ba70083 100644 --- a/proof/crefine/ARM/CSpaceAcc_C.thy +++ b/proof/crefine/ARM/CSpaceAcc_C.thy @@ -11,7 +11,7 @@ (* collects lemmas common to the various CSpace branches *) theory CSpaceAcc_C -imports "../../refine/$L4V_ARCH/EmptyFail" Ctac_lemmas_C +imports "Refine.EmptyFail" Ctac_lemmas_C begin (* For resolving schematics *) diff --git a/proof/crefine/ARM/CSpace_RAB_C.thy b/proof/crefine/ARM/CSpace_RAB_C.thy index 456ec6d4e..bc403c79a 100644 --- a/proof/crefine/ARM/CSpace_RAB_C.thy +++ b/proof/crefine/ARM/CSpace_RAB_C.thy @@ -9,7 +9,7 @@ *) theory CSpace_RAB_C -imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C" +imports CSpaceAcc_C "CLib.MonadicRewrite_C" begin context kernel diff --git a/proof/crefine/ARM/Cache.thy b/proof/crefine/ARM/Cache.thy index d3a219aa1..295247125 100644 --- a/proof/crefine/ARM/Cache.thy +++ b/proof/crefine/ARM/Cache.thy @@ -9,7 +9,7 @@ *) theory Cache (* FIXME: broken *) -imports "~~/src/HOL/Main" +imports Main begin text {* Enable the proof cache, both skipping from it diff --git a/proof/crefine/ARM/Ctac_lemmas_C.thy b/proof/crefine/ARM/Ctac_lemmas_C.thy index ca6d0559b..0bf2f0713 100644 --- a/proof/crefine/ARM/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM/Ctac_lemmas_C.thy @@ -12,7 +12,7 @@ theory Ctac_lemmas_C imports - "../../../lib/clib/Ctac" + "../lib/Ctac" begin context kernel diff --git a/proof/crefine/ARM/DetWP.thy b/proof/crefine/ARM/DetWP.thy index 2e1bca1a9..ac489d80b 100644 --- a/proof/crefine/ARM/DetWP.thy +++ b/proof/crefine/ARM/DetWP.thy @@ -9,7 +9,7 @@ *) theory DetWP -imports "../../../lib/clib/DetWPLib" Include_C +imports "CLib.DetWPLib" Include_C begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy index f40bf547f..e2c969280 100644 --- a/proof/crefine/ARM/Fastpath_C.thy +++ b/proof/crefine/ARM/Fastpath_C.thy @@ -14,8 +14,8 @@ imports SyscallArgs_C Delete_C Syscall_C - "../../refine/$L4V_ARCH/RAB_FN" - "../../../lib/clib/MonadicRewrite_C" + "Refine.RAB_FN" + "CLib.MonadicRewrite_C" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM/Include_C.thy b/proof/crefine/ARM/Include_C.thy index 942811468..7db17a442 100644 --- a/proof/crefine/ARM/Include_C.thy +++ b/proof/crefine/ARM/Include_C.thy @@ -10,8 +10,8 @@ theory Include_C imports - "../../../spec/cspec/KernelInc_C" - "../../refine/$L4V_ARCH/Refine" + "CSpec.KernelInc_C" + "Refine.Refine" begin end diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy index f8833d5c3..b33b463fa 100644 --- a/proof/crefine/ARM/Invoke_C.thy +++ b/proof/crefine/ARM/Invoke_C.thy @@ -9,7 +9,7 @@ *) theory Invoke_C -imports Recycle_C "../../../lib/clib/MonadicRewrite_C" +imports Recycle_C "CLib.MonadicRewrite_C" begin context kernel_m diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy index 536391dbb..db56c1b91 100644 --- a/proof/crefine/ARM/IsolatedThreadAction.thy +++ b/proof/crefine/ARM/IsolatedThreadAction.thy @@ -9,7 +9,7 @@ *) theory IsolatedThreadAction -imports "../../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C +imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C begin datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \ machine_word" diff --git a/proof/crefine/ARM/Move.thy b/proof/crefine/ARM/Move.thy index 3f568cb8e..44b69f788 100644 --- a/proof/crefine/ARM/Move.thy +++ b/proof/crefine/ARM/Move.thy @@ -11,7 +11,7 @@ (* things that should be moved into first refinement *) theory Move -imports "../../refine/$L4V_ARCH/Refine" +imports "Refine.Refine" begin lemma finaliseCap_Reply: diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index aa4a3ee9f..7198ce261 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -11,7 +11,7 @@ chapter "Toplevel Refinement Statement" theory Refine_C -imports Init_C Fastpath_C "../../../lib/clib/CToCRefine" +imports Init_C Fastpath_C "../lib/CToCRefine" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM/Refine_nondet_C.thy b/proof/crefine/ARM/Refine_nondet_C.thy index 65c9ffb6b..bca186552 100644 --- a/proof/crefine/ARM/Refine_nondet_C.thy +++ b/proof/crefine/ARM/Refine_nondet_C.thy @@ -13,7 +13,7 @@ header "Toplevel Refinement Statement for nondeterministic specification" theory Refine_nondet_C (* FIXME: broken *) imports Refine_C - "../../invariant-abstract/BCorres2_AI" + "AInvs.BCorres2_AI" begin definition (in state_rel) diff --git a/proof/crefine/ARM/SR_lemmas_C.thy b/proof/crefine/ARM/SR_lemmas_C.thy index 8b7a9d501..e22736f05 100644 --- a/proof/crefine/ARM/SR_lemmas_C.thy +++ b/proof/crefine/ARM/SR_lemmas_C.thy @@ -11,7 +11,7 @@ theory SR_lemmas_C imports StateRelation_C - "../../refine/$L4V_ARCH/Invariants_H" + "Refine.Invariants_H" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy index 99f84bf22..8123c8d6c 100644 --- a/proof/crefine/ARM/Wellformed_C.thy +++ b/proof/crefine/ARM/Wellformed_C.thy @@ -13,9 +13,9 @@ theory Wellformed_C imports - "../../../lib/CTranslationNICTA" + "CLib.CTranslationNICTA" CLevityCatch - "../../../spec/cspec/Substitute" + "CSpec.Substitute" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM_HYP/ADT_C.thy b/proof/crefine/ARM_HYP/ADT_C.thy index 56c10512a..6af590a93 100644 --- a/proof/crefine/ARM_HYP/ADT_C.thy +++ b/proof/crefine/ARM_HYP/ADT_C.thy @@ -11,7 +11,7 @@ theory ADT_C imports Schedule_C Retype_C Recycle_C - "../../invariant-abstract/BCorres2_AI" + "AInvs.BCorres2_AI" begin diff --git a/proof/crefine/ARM_HYP/BuildRefineCache_C.thy b/proof/crefine/ARM_HYP/BuildRefineCache_C.thy index d2a73c408..2565f8d3e 100644 --- a/proof/crefine/ARM_HYP/BuildRefineCache_C.thy +++ b/proof/crefine/ARM_HYP/BuildRefineCache_C.thy @@ -9,7 +9,7 @@ *) theory BuildRefineCache_C (* FIXME: broken *) -imports "~~/src/HOL/Main" +imports Main begin ML {* diff --git a/proof/crefine/ARM_HYP/CLevityCatch.thy b/proof/crefine/ARM_HYP/CLevityCatch.thy index 68350fd80..281b3ba0d 100644 --- a/proof/crefine/ARM_HYP/CLevityCatch.thy +++ b/proof/crefine/ARM_HYP/CLevityCatch.thy @@ -12,8 +12,8 @@ theory CLevityCatch imports Include_C Move - "../../../lib/LemmaBucket_C" - "../../../lib/LemmaBucket" + "CLib.LemmaBucket_C" + "Lib.LemmaBucket" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM_HYP/CSpaceAcc_C.thy b/proof/crefine/ARM_HYP/CSpaceAcc_C.thy index 29401a103..e8ba70083 100644 --- a/proof/crefine/ARM_HYP/CSpaceAcc_C.thy +++ b/proof/crefine/ARM_HYP/CSpaceAcc_C.thy @@ -11,7 +11,7 @@ (* collects lemmas common to the various CSpace branches *) theory CSpaceAcc_C -imports "../../refine/$L4V_ARCH/EmptyFail" Ctac_lemmas_C +imports "Refine.EmptyFail" Ctac_lemmas_C begin (* For resolving schematics *) diff --git a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy index 0f6c9ca5a..62d063543 100644 --- a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy +++ b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy @@ -9,7 +9,7 @@ *) theory CSpace_RAB_C -imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C" +imports CSpaceAcc_C "CLib.MonadicRewrite_C" begin context kernel diff --git a/proof/crefine/ARM_HYP/Cache.thy b/proof/crefine/ARM_HYP/Cache.thy index d3a219aa1..295247125 100644 --- a/proof/crefine/ARM_HYP/Cache.thy +++ b/proof/crefine/ARM_HYP/Cache.thy @@ -9,7 +9,7 @@ *) theory Cache (* FIXME: broken *) -imports "~~/src/HOL/Main" +imports Main begin text {* Enable the proof cache, both skipping from it diff --git a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy index bc6a5ffb2..555de99a5 100644 --- a/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy +++ b/proof/crefine/ARM_HYP/Ctac_lemmas_C.thy @@ -12,7 +12,7 @@ theory Ctac_lemmas_C imports - "../../../lib/clib/Ctac" + "../lib/Ctac" begin context kernel diff --git a/proof/crefine/ARM_HYP/DetWP.thy b/proof/crefine/ARM_HYP/DetWP.thy index 92a80295e..d8679db1b 100644 --- a/proof/crefine/ARM_HYP/DetWP.thy +++ b/proof/crefine/ARM_HYP/DetWP.thy @@ -9,7 +9,7 @@ *) theory DetWP -imports "../../../lib/clib/DetWPLib" Include_C +imports "CLib.DetWPLib" Include_C begin (* FIXME YUCK where did you come from *) diff --git a/proof/crefine/ARM_HYP/Fastpath_C.thy b/proof/crefine/ARM_HYP/Fastpath_C.thy index 67fa0851b..9969fd6d6 100644 --- a/proof/crefine/ARM_HYP/Fastpath_C.thy +++ b/proof/crefine/ARM_HYP/Fastpath_C.thy @@ -14,8 +14,8 @@ imports SyscallArgs_C Delete_C Syscall_C - "../../refine/$L4V_ARCH/RAB_FN" - "../../../lib/clib/MonadicRewrite_C" + "Refine.RAB_FN" + "CLib.MonadicRewrite_C" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM_HYP/Include_C.thy b/proof/crefine/ARM_HYP/Include_C.thy index 942811468..7db17a442 100644 --- a/proof/crefine/ARM_HYP/Include_C.thy +++ b/proof/crefine/ARM_HYP/Include_C.thy @@ -10,8 +10,8 @@ theory Include_C imports - "../../../spec/cspec/KernelInc_C" - "../../refine/$L4V_ARCH/Refine" + "CSpec.KernelInc_C" + "Refine.Refine" begin end diff --git a/proof/crefine/ARM_HYP/Invoke_C.thy b/proof/crefine/ARM_HYP/Invoke_C.thy index 676dcedc1..f66eb0e44 100644 --- a/proof/crefine/ARM_HYP/Invoke_C.thy +++ b/proof/crefine/ARM_HYP/Invoke_C.thy @@ -9,7 +9,7 @@ *) theory Invoke_C -imports Recycle_C "../../../lib/clib/MonadicRewrite_C" +imports Recycle_C "CLib.MonadicRewrite_C" begin context kernel_m diff --git a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy index 295084de8..787315ec5 100644 --- a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy +++ b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy @@ -9,7 +9,7 @@ *) theory IsolatedThreadAction -imports "../../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C +imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C begin datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \ machine_word" diff --git a/proof/crefine/ARM_HYP/Move.thy b/proof/crefine/ARM_HYP/Move.thy index 6af0d8523..acf0e863a 100644 --- a/proof/crefine/ARM_HYP/Move.thy +++ b/proof/crefine/ARM_HYP/Move.thy @@ -11,7 +11,7 @@ (* things that should be moved into first refinement *) theory Move -imports "../../refine/$L4V_ARCH/Refine" +imports "Refine.Refine" begin (* FIXME move: need a theory on top of CSpec that arches can share *) diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index 1d7fe98dc..460fc683d 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -11,7 +11,7 @@ chapter "Toplevel Refinement Statement" theory Refine_C -imports Init_C Fastpath_C "../../../lib/clib/CToCRefine" +imports Init_C Fastpath_C "../lib/CToCRefine" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM_HYP/Refine_nondet_C.thy b/proof/crefine/ARM_HYP/Refine_nondet_C.thy index 65c9ffb6b..bca186552 100644 --- a/proof/crefine/ARM_HYP/Refine_nondet_C.thy +++ b/proof/crefine/ARM_HYP/Refine_nondet_C.thy @@ -13,7 +13,7 @@ header "Toplevel Refinement Statement for nondeterministic specification" theory Refine_nondet_C (* FIXME: broken *) imports Refine_C - "../../invariant-abstract/BCorres2_AI" + "AInvs.BCorres2_AI" begin definition (in state_rel) diff --git a/proof/crefine/ARM_HYP/SR_lemmas_C.thy b/proof/crefine/ARM_HYP/SR_lemmas_C.thy index 5967d1bb7..0b6092cfa 100644 --- a/proof/crefine/ARM_HYP/SR_lemmas_C.thy +++ b/proof/crefine/ARM_HYP/SR_lemmas_C.thy @@ -11,7 +11,7 @@ theory SR_lemmas_C imports StateRelation_C - "../../refine/$L4V_ARCH/Invariants_H" + "Refine.Invariants_H" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy index c5fa61840..9bf43d5a9 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/proof/crefine/ARM_HYP/Wellformed_C.thy @@ -13,9 +13,9 @@ theory Wellformed_C imports - "../../../lib/CTranslationNICTA" + "CLib.CTranslationNICTA" CLevityCatch - "../../../spec/cspec/Substitute" + "CSpec.Substitute" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/X64/ADT_C.thy b/proof/crefine/X64/ADT_C.thy index 7788542e0..ebeaa6d16 100644 --- a/proof/crefine/X64/ADT_C.thy +++ b/proof/crefine/X64/ADT_C.thy @@ -11,7 +11,7 @@ theory ADT_C imports Schedule_C Retype_C Recycle_C - "../../invariant-abstract/BCorres2_AI" + "AInvs.BCorres2_AI" begin diff --git a/proof/crefine/X64/AutoCorresTest.thy b/proof/crefine/X64/AutoCorresTest.thy new file mode 100644 index 000000000..d87284203 --- /dev/null +++ b/proof/crefine/X64/AutoCorresTest.thy @@ -0,0 +1,17 @@ +(* + * Copyright 2018, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory AutoCorresTest +imports Refine_C +begin + +(* empty stub, currently tested for ARM and ARM_HYP only *) + +end diff --git a/proof/crefine/X64/CLevityCatch.thy b/proof/crefine/X64/CLevityCatch.thy index 39295d281..3adf6e5c3 100644 --- a/proof/crefine/X64/CLevityCatch.thy +++ b/proof/crefine/X64/CLevityCatch.thy @@ -12,8 +12,8 @@ theory CLevityCatch imports Include_C Move - "../../../lib/LemmaBucket_C" - "../../../lib/LemmaBucket" + "CLib.LemmaBucket_C" + "Lib.LemmaBucket" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/X64/CSpaceAcc_C.thy b/proof/crefine/X64/CSpaceAcc_C.thy index 20d4a5dc0..ae47b0e5c 100644 --- a/proof/crefine/X64/CSpaceAcc_C.thy +++ b/proof/crefine/X64/CSpaceAcc_C.thy @@ -11,7 +11,7 @@ (* collects lemmas common to the various CSpace branches *) theory CSpaceAcc_C -imports "../../refine/$L4V_ARCH/EmptyFail" Ctac_lemmas_C +imports "Refine.EmptyFail" Ctac_lemmas_C begin (* For resolving schematics *) diff --git a/proof/crefine/X64/CSpace_RAB_C.thy b/proof/crefine/X64/CSpace_RAB_C.thy index 88d70a1da..c11168ed7 100644 --- a/proof/crefine/X64/CSpace_RAB_C.thy +++ b/proof/crefine/X64/CSpace_RAB_C.thy @@ -9,7 +9,7 @@ *) theory CSpace_RAB_C -imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C" +imports CSpaceAcc_C "CLib.MonadicRewrite_C" begin context kernel diff --git a/proof/crefine/X64/Ctac_lemmas_C.thy b/proof/crefine/X64/Ctac_lemmas_C.thy index 09aa988ab..baded123f 100644 --- a/proof/crefine/X64/Ctac_lemmas_C.thy +++ b/proof/crefine/X64/Ctac_lemmas_C.thy @@ -12,7 +12,7 @@ theory Ctac_lemmas_C imports - "../../../lib/clib/Ctac" + "../lib/Ctac" begin context kernel diff --git a/proof/crefine/X64/DetWP.thy b/proof/crefine/X64/DetWP.thy index d6f2ba3c9..2134ad795 100644 --- a/proof/crefine/X64/DetWP.thy +++ b/proof/crefine/X64/DetWP.thy @@ -9,7 +9,7 @@ *) theory DetWP -imports "../../../lib/clib/DetWPLib" Include_C +imports "CLib.DetWPLib" Include_C begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/X64/Include_C.thy b/proof/crefine/X64/Include_C.thy index ed8ad8131..764edef8c 100644 --- a/proof/crefine/X64/Include_C.thy +++ b/proof/crefine/X64/Include_C.thy @@ -10,8 +10,8 @@ theory Include_C imports - "../../../spec/cspec/KernelInc_C" - "../../refine/$L4V_ARCH/Refine" + "CSpec.KernelInc_C" + "Refine.Refine" begin end diff --git a/proof/crefine/X64/Invoke_C.thy b/proof/crefine/X64/Invoke_C.thy index de38bd155..0466c1e68 100644 --- a/proof/crefine/X64/Invoke_C.thy +++ b/proof/crefine/X64/Invoke_C.thy @@ -9,7 +9,7 @@ *) theory Invoke_C -imports Recycle_C "../../../lib/clib/MonadicRewrite_C" +imports Recycle_C "CLib.MonadicRewrite_C" begin context kernel_m diff --git a/proof/crefine/X64/IsolatedThreadAction.thy b/proof/crefine/X64/IsolatedThreadAction.thy index 200a642fd..14cc32a4b 100644 --- a/proof/crefine/X64/IsolatedThreadAction.thy +++ b/proof/crefine/X64/IsolatedThreadAction.thy @@ -9,7 +9,7 @@ *) theory IsolatedThreadAction -imports "../../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C +imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C begin context begin interpretation Arch . diff --git a/proof/crefine/X64/Move.thy b/proof/crefine/X64/Move.thy index 49b781e5a..b29666771 100644 --- a/proof/crefine/X64/Move.thy +++ b/proof/crefine/X64/Move.thy @@ -11,7 +11,7 @@ (* things that should be moved into first refinement *) theory Move -imports "../../refine/$L4V_ARCH/Refine" +imports "Refine.Refine" begin lemma finaliseCap_Reply: diff --git a/proof/crefine/X64/Refine_C.thy b/proof/crefine/X64/Refine_C.thy index 69870cfa1..4ec14b73e 100644 --- a/proof/crefine/X64/Refine_C.thy +++ b/proof/crefine/X64/Refine_C.thy @@ -20,10 +20,10 @@ imports SyscallArgs_C Delete_C Syscall_C - "../../refine/$L4V_ARCH/RAB_FN" - "../../../lib/clib/MonadicRewrite_C" + "Refine.RAB_FN" + "CLib.MonadicRewrite_C" - "../../../lib/clib/CToCRefine" + "../lib/CToCRefine" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/X64/SR_lemmas_C.thy b/proof/crefine/X64/SR_lemmas_C.thy index 55fdf444a..282dae5bd 100644 --- a/proof/crefine/X64/SR_lemmas_C.thy +++ b/proof/crefine/X64/SR_lemmas_C.thy @@ -11,7 +11,7 @@ theory SR_lemmas_C imports StateRelation_C - "../../refine/$L4V_ARCH/Invariants_H" + "Refine.Invariants_H" begin (* FIXME: move to Word_Lib *) diff --git a/proof/crefine/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy index fab60db0d..bef055f04 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -13,9 +13,9 @@ theory Wellformed_C imports - "../../../lib/CTranslationNICTA" + "CLib.CTranslationNICTA" CLevityCatch - "../../../spec/cspec/Substitute" + "CSpec.Substitute" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/lib/clib/AutoCorresModifiesProofs.thy b/proof/crefine/lib/AutoCorresModifiesProofs.thy similarity index 99% rename from lib/clib/AutoCorresModifiesProofs.thy rename to proof/crefine/lib/AutoCorresModifiesProofs.thy index 6edd3d55a..bf1656d19 100644 --- a/lib/clib/AutoCorresModifiesProofs.thy +++ b/proof/crefine/lib/AutoCorresModifiesProofs.thy @@ -8,9 +8,10 @@ * @TAG(NICTA_GPL) *) -theory AutoCorresModifiesProofs imports - "../../tools/autocorres/L4VerifiedLinks" - "../../lib/SIMPL_Lemmas" +theory AutoCorresModifiesProofs +imports + "L4VerifiedLinks" + "CLib.SIMPL_Lemmas" begin text \ diff --git a/lib/clib/AutoCorres_C.thy b/proof/crefine/lib/AutoCorres_C.thy similarity index 100% rename from lib/clib/AutoCorres_C.thy rename to proof/crefine/lib/AutoCorres_C.thy diff --git a/lib/clib/CToCRefine.thy b/proof/crefine/lib/CToCRefine.thy similarity index 97% rename from lib/clib/CToCRefine.thy rename to proof/crefine/lib/CToCRefine.thy index ea6f853d4..71c56f9b4 100644 --- a/lib/clib/CToCRefine.thy +++ b/proof/crefine/lib/CToCRefine.thy @@ -11,9 +11,9 @@ theory CToCRefine imports - "../../spec/cspec/Substitute" - "../SimplRewrite" - "../TypHeapLib" + "CSpec.Substitute" + "CLib.SimplRewrite" + "CLib.TypHeapLib" begin lemma spec_statefn_simulates_lookup_tree_Node: diff --git a/lib/clib/Corres_C.thy b/proof/crefine/lib/Corres_C.thy similarity index 99% rename from lib/clib/Corres_C.thy rename to proof/crefine/lib/Corres_C.thy index 1fa55893b..5cf7db6ec 100644 --- a/lib/clib/Corres_C.thy +++ b/proof/crefine/lib/Corres_C.thy @@ -10,8 +10,8 @@ theory Corres_C imports - CCorresLemmas - "../../proof/crefine/$L4V_ARCH/SR_lemmas_C" + "CLib.CCorresLemmas" + "../$L4V_ARCH/SR_lemmas_C" begin abbreviation diff --git a/lib/clib/Ctac.thy b/proof/crefine/lib/Ctac.thy similarity index 99% rename from lib/clib/Ctac.thy rename to proof/crefine/lib/Ctac.thy index 02153b36a..53e4e4c69 100644 --- a/lib/clib/Ctac.thy +++ b/proof/crefine/lib/Ctac.thy @@ -13,7 +13,7 @@ theory Ctac imports AutoCorres_C - "../XPres" + "CLib.XPres" begin (* This file includes theorems associated with ctac and friends *) diff --git a/tools/autocorres/L4VerifiedLinks.thy b/proof/crefine/lib/L4VerifiedLinks.thy similarity index 98% rename from tools/autocorres/L4VerifiedLinks.thy rename to proof/crefine/lib/L4VerifiedLinks.thy index 21725bd21..c025bf198 100644 --- a/tools/autocorres/L4VerifiedLinks.thy +++ b/proof/crefine/lib/L4VerifiedLinks.thy @@ -16,8 +16,8 @@ theory L4VerifiedLinks imports - AutoCorres - "../../lib/clib/Corres_UL_C" + "AutoCorres.AutoCorres" + "CLib.Corres_UL_C" begin (* diff --git a/lib/clib/ctac-method.ML b/proof/crefine/lib/ctac-method.ML similarity index 100% rename from lib/clib/ctac-method.ML rename to proof/crefine/lib/ctac-method.ML diff --git a/proof/drefine/Finalise_DR.thy b/proof/drefine/Finalise_DR.thy index 66b108873..b6c692fb6 100644 --- a/proof/drefine/Finalise_DR.thy +++ b/proof/drefine/Finalise_DR.thy @@ -11,7 +11,7 @@ theory Finalise_DR imports KHeap_DR - "../invariant-abstract/VSpaceEntries_AI" + "AInvs.VSpaceEntries_AI" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/drefine/Include_D.thy b/proof/drefine/Include_D.thy index c3202eb90..bc04f83b9 100644 --- a/proof/drefine/Include_D.thy +++ b/proof/drefine/Include_D.thy @@ -16,9 +16,9 @@ theory Include_D imports - "../../spec/capDL/Syscall_D" - "../refine/$L4V_ARCH/Refine" - "../../lib/MonadicRewrite" + "DSpec.Syscall_D" + "Refine.Refine" + "Lib.MonadicRewrite" begin end diff --git a/proof/drefine/Lemmas_D.thy b/proof/drefine/Lemmas_D.thy index e974ba930..b4cfce903 100644 --- a/proof/drefine/Lemmas_D.thy +++ b/proof/drefine/Lemmas_D.thy @@ -20,9 +20,8 @@ imports Include_D MoreHOL MoreCorres - "../../spec/design/InvocationLabels_H" - "../../lib/MonadicRewrite" - "../refine/$L4V_ARCH/EmptyFail" + "ExecSpec.InvocationLabels_H" + "Refine.EmptyFail" begin no_notation bind_drop (infixl ">>" 60) diff --git a/proof/drefine/MoreCorres.thy b/proof/drefine/MoreCorres.thy index 0d9293f6d..02a00106b 100644 --- a/proof/drefine/MoreCorres.thy +++ b/proof/drefine/MoreCorres.thy @@ -9,7 +9,7 @@ *) theory MoreCorres -imports "../../lib/ExtraCorres" +imports "Lib.ExtraCorres" begin (* FIXME: move all of this into ExtraCorres *) diff --git a/proof/drefine/MoreHOL.thy b/proof/drefine/MoreHOL.thy index ab09fb771..916d4b895 100644 --- a/proof/drefine/MoreHOL.thy +++ b/proof/drefine/MoreHOL.thy @@ -9,7 +9,7 @@ *) theory MoreHOL -imports "~~/src/HOL/Main" +imports Main begin (* diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index da0a7c091..a3959d2cf 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -18,8 +18,8 @@ text {* theory ADT_IF imports Noninterference_Base - "../access-control/Syscall_AC" - "../access-control/ADT_AC" + "Access.Syscall_AC" + "Access.ADT_AC" IRQMasks_IF FinalCaps Scheduler_IF UserOp_IF begin diff --git a/proof/infoflow/ADT_IF_Refine.thy b/proof/infoflow/ADT_IF_Refine.thy index d2dae2453..600d5f95f 100644 --- a/proof/infoflow/ADT_IF_Refine.thy +++ b/proof/infoflow/ADT_IF_Refine.thy @@ -10,7 +10,7 @@ theory ADT_IF_Refine imports - "ADT_IF" "../refine/$L4V_ARCH/Refine" "../refine/$L4V_ARCH/EmptyFail_H" + "ADT_IF" "Refine.Refine" "Refine.EmptyFail_H" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/infoflow/ADT_IF_Refine_C.thy b/proof/infoflow/ADT_IF_Refine_C.thy index a9562fed0..a61a74fbb 100644 --- a/proof/infoflow/ADT_IF_Refine_C.thy +++ b/proof/infoflow/ADT_IF_Refine_C.thy @@ -10,7 +10,7 @@ theory ADT_IF_Refine_C imports - "ADT_IF_Refine" "../crefine/$L4V_ARCH/Refine_C" + "ADT_IF_Refine" "CRefine.Refine_C" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/infoflow/ExampleSystemPolicyFlows.thy b/proof/infoflow/ExampleSystemPolicyFlows.thy index 444f37ea3..46aa738d5 100644 --- a/proof/infoflow/ExampleSystemPolicyFlows.thy +++ b/proof/infoflow/ExampleSystemPolicyFlows.thy @@ -11,7 +11,7 @@ theory ExampleSystemPolicyFlows imports Noninterference - "../access-control/ExampleSystem" + "Access.ExampleSystem" begin subsection {* Example 1 -- similar to Sys1 in ../access-control/ExampleSystem.thy *} diff --git a/proof/infoflow/Example_Valid_State.thy b/proof/infoflow/Example_Valid_State.thy index 715aa5ecb..9f3ed872d 100644 --- a/proof/infoflow/Example_Valid_State.thy +++ b/proof/infoflow/Example_Valid_State.thy @@ -11,7 +11,7 @@ theory Example_Valid_State imports "Noninterference" - "../../lib/Distinct_Cmd" + "Lib.Distinct_Cmd" begin section {* Example *} diff --git a/proof/infoflow/IRQMasks_IF.thy b/proof/infoflow/IRQMasks_IF.thy index f9f174e96..9772297a9 100644 --- a/proof/infoflow/IRQMasks_IF.thy +++ b/proof/infoflow/IRQMasks_IF.thy @@ -9,7 +9,7 @@ *) theory IRQMasks_IF -imports "../access-control/DomainSepInv" +imports "Access.DomainSepInv" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/infoflow/Include_IF_C.thy b/proof/infoflow/Include_IF_C.thy index bc7a25992..d7b99c4df 100644 --- a/proof/infoflow/Include_IF_C.thy +++ b/proof/infoflow/Include_IF_C.thy @@ -10,9 +10,9 @@ theory Include_IF_C imports - "Noninterference" - "Noninterference_Base_Refinement" - "Example_Valid_State" + "InfoFlow.Noninterference" + "InfoFlow.Noninterference_Base_Refinement" + "InfoFlow.Example_Valid_State" begin end diff --git a/proof/infoflow/InfoFlow.thy b/proof/infoflow/InfoFlow.thy index e520da8d2..821e9b867 100644 --- a/proof/infoflow/InfoFlow.thy +++ b/proof/infoflow/InfoFlow.thy @@ -21,8 +21,8 @@ text {* theory InfoFlow imports - "../access-control/Syscall_AC" - "../../lib/EquivValid" + "Access.Syscall_AC" + "Lib.EquivValid" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index 0d0b3361f..bb5567dea 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -13,7 +13,7 @@ imports "Noninterference_Base" "Noninterference_Base_Alternatives" "Scheduler_IF" "ADT_IF" - "../access-control/ADT_AC" + "Access.ADT_AC" begin text {* diff --git a/proof/infoflow/Noninterference_Base.thy b/proof/infoflow/Noninterference_Base.thy index 1f13dad45..cae721791 100644 --- a/proof/infoflow/Noninterference_Base.thy +++ b/proof/infoflow/Noninterference_Base.thy @@ -9,7 +9,7 @@ *) theory Noninterference_Base -imports "../../lib/Simulation" +imports "Lib.Simulation" begin text {* diff --git a/proof/infoflow/Noninterference_Base_Alternatives.thy b/proof/infoflow/Noninterference_Base_Alternatives.thy index e9cfd62d0..c3e50a535 100644 --- a/proof/infoflow/Noninterference_Base_Alternatives.thy +++ b/proof/infoflow/Noninterference_Base_Alternatives.thy @@ -9,7 +9,7 @@ *) theory Noninterference_Base_Alternatives -imports Noninterference_Base "../../lib/Eisbach_Methods" +imports Noninterference_Base "Lib.Eisbach_Methods" begin diff --git a/proof/infoflow/Noninterference_Base_Enabledness_weak_asym.thy b/proof/infoflow/Noninterference_Base_Enabledness_weak_asym.thy index b2ff55057..ef12dde7c 100644 --- a/proof/infoflow/Noninterference_Base_Enabledness_weak_asym.thy +++ b/proof/infoflow/Noninterference_Base_Enabledness_weak_asym.thy @@ -9,7 +9,7 @@ *) theory Noninterference_Base_Enabledness_weak_asym -imports "../../lib/Simulation" +imports "Lib.Simulation" begin text {* diff --git a/proof/infoflow/PasUpdates.thy b/proof/infoflow/PasUpdates.thy index 4b0b48450..cc9be3724 100644 --- a/proof/infoflow/PasUpdates.thy +++ b/proof/infoflow/PasUpdates.thy @@ -16,8 +16,7 @@ theory PasUpdates imports "Arch_IF" "FinalCaps" - "../invariant-abstract/EmptyFail_AI" - + "AInvs.EmptyFail_AI" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/infoflow/PolicySystemSAC.thy b/proof/infoflow/PolicySystemSAC.thy index 7e25806d4..3187eae8f 100644 --- a/proof/infoflow/PolicySystemSAC.thy +++ b/proof/infoflow/PolicySystemSAC.thy @@ -11,7 +11,7 @@ theory PolicySystemSAC imports Noninterference - "../access-control/ExampleSystem" + "Access.ExampleSystem" begin text {* diff --git a/proof/infoflow/UserOp_IF.thy b/proof/infoflow/UserOp_IF.thy index 84bcbfe22..a8da30b6d 100644 --- a/proof/infoflow/UserOp_IF.thy +++ b/proof/infoflow/UserOp_IF.thy @@ -9,7 +9,7 @@ *) theory UserOp_IF -imports Syscall_IF "../access-control/ADT_AC" +imports Syscall_IF "Access.ADT_AC" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/invariant-abstract/ARM/ArchADT_AI.thy b/proof/invariant-abstract/ARM/ArchADT_AI.thy index 8b645246c..197ebde1d 100644 --- a/proof/invariant-abstract/ARM/ArchADT_AI.thy +++ b/proof/invariant-abstract/ARM/ArchADT_AI.thy @@ -12,7 +12,7 @@ chapter {* ARM-specific definitions for abstract datatype for the abstract speci theory ArchADT_AI imports - "../../../lib/Simulation" + "Lib.Simulation" "../Invariants_AI" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchAcc_AI.thy b/proof/invariant-abstract/ARM/ArchAcc_AI.thy index f74462a2d..57573d8a6 100644 --- a/proof/invariant-abstract/ARM/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchAcc_AI.thy @@ -14,7 +14,7 @@ Lemmas on arch get/set object etc theory ArchAcc_AI imports "../SubMonad_AI" - "../../../lib/Crunch_Instances_NonDet" + "Lib.Crunch_Instances_NonDet" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchCrunchSetup_AI.thy b/proof/invariant-abstract/ARM/ArchCrunchSetup_AI.thy index 3f48fd89b..275712120 100644 --- a/proof/invariant-abstract/ARM/ArchCrunchSetup_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCrunchSetup_AI.thy @@ -10,8 +10,8 @@ theory ArchCrunchSetup_AI imports - "../../../spec/abstract/Syscall_A" - "../../../lib/Crunch_Instances_NonDet" + "ASpec.Syscall_A" + "Lib.Crunch_Instances_NonDet" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy b/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy index d9703ff05..4197035cf 100644 --- a/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchLevityCatch_AI.thy @@ -11,8 +11,8 @@ theory ArchLevityCatch_AI imports "../BCorres_AI" - "../../../lib/LemmaBucket" - "../../../lib/SplitRule" + "Lib.LemmaBucket" + "Lib.SplitRule" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy index 6187f3a6f..37b8bcadb 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchADT_AI.thy @@ -12,7 +12,7 @@ chapter {* ARM-specific definitions for abstract datatype for the abstract speci theory ArchADT_AI imports - "../../../lib/Simulation" + "Lib.Simulation" "../Invariants_AI" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy index 8892815c1..190d416d8 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy @@ -14,7 +14,7 @@ Lemmas on arch get/set object etc theory ArchAcc_AI imports "../SubMonad_AI" - "../../../lib/Crunch_Instances_NonDet" + "Lib.Crunch_Instances_NonDet" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM_HYP/ArchCrunchSetup_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCrunchSetup_AI.thy index 7127ea9df..712906417 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchCrunchSetup_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchCrunchSetup_AI.thy @@ -10,8 +10,8 @@ theory ArchCrunchSetup_AI imports - "../../../spec/abstract/Syscall_A" - "../../../lib/Crunch_Instances_NonDet" + "ASpec.Syscall_A" + "Lib.Crunch_Instances_NonDet" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/ARM_HYP/ArchLevityCatch_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchLevityCatch_AI.thy index edec4026a..29bcc177f 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchLevityCatch_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchLevityCatch_AI.thy @@ -11,8 +11,8 @@ theory ArchLevityCatch_AI imports "../BCorres_AI" - "../../../lib/LemmaBucket" - "../../../lib/SplitRule" + "Lib.LemmaBucket" + "Lib.SplitRule" begin context Arch begin global_naming ARM diff --git a/proof/invariant-abstract/BCorres2_AI.thy b/proof/invariant-abstract/BCorres2_AI.thy index 4958a1356..28c1f9d7f 100644 --- a/proof/invariant-abstract/BCorres2_AI.thy +++ b/proof/invariant-abstract/BCorres2_AI.thy @@ -10,7 +10,7 @@ theory BCorres2_AI imports - "../../lib/BCorres_UL" + "Lib.BCorres_UL" "./$L4V_ARCH/ArchEmptyFail_AI" begin diff --git a/proof/invariant-abstract/BCorres_AI.thy b/proof/invariant-abstract/BCorres_AI.thy index 0dac3e828..7f5458efd 100644 --- a/proof/invariant-abstract/BCorres_AI.thy +++ b/proof/invariant-abstract/BCorres_AI.thy @@ -11,8 +11,8 @@ theory BCorres_AI imports Include_AI - "../../lib/BCorres_UL" - "../../spec/abstract/Syscall_A" + "Lib.BCorres_UL" + "ASpec.Syscall_A" begin abbreviation "bcorres \ bcorres_underlying truncate_state" diff --git a/proof/invariant-abstract/Include_AI.thy b/proof/invariant-abstract/Include_AI.thy index b0a67c6f1..46f56f7b5 100644 --- a/proof/invariant-abstract/Include_AI.thy +++ b/proof/invariant-abstract/Include_AI.thy @@ -11,10 +11,10 @@ theory Include_AI imports "./$L4V_ARCH/ArchCrunchSetup_AI" - "../../lib/Monad_WP/wp/Eisbach_WP" - "../../spec/abstract/Syscall_A" - "../../lib/LemmaBucket" - "../../lib/ListLibLemmas" + "Lib.Eisbach_WP" + "ASpec.Syscall_A" + "Lib.LemmaBucket" + "Lib.ListLibLemmas" begin no_notation bind_drop (infixl ">>" 60) diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index fc5986907..ae19b0585 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -10,7 +10,7 @@ theory Ipc_AI imports "./$L4V_ARCH/ArchFinalise_AI" - "../../lib/Monad_WP/wp/WPBang" + "Lib.WPBang" begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/KernelInitSepProofs_AI.thy b/proof/invariant-abstract/KernelInitSepProofs_AI.thy index 91506a7aa..ae1870ab8 100644 --- a/proof/invariant-abstract/KernelInitSepProofs_AI.thy +++ b/proof/invariant-abstract/KernelInitSepProofs_AI.thy @@ -12,7 +12,7 @@ theory KernelInitSepProofs_AI (* unused and broken, kept here for future referen imports KernelInitSep_AI CSpaceInv_AI - "../../spec/abstract/KernelInit_A" + "ASpec.KernelInit_A" begin lemma propagate_do_kernel_op: diff --git a/proof/invariant-abstract/KernelInitSep_AI.thy b/proof/invariant-abstract/KernelInitSep_AI.thy index 61a60bb83..ea5527d05 100644 --- a/proof/invariant-abstract/KernelInitSep_AI.thy +++ b/proof/invariant-abstract/KernelInitSep_AI.thy @@ -10,8 +10,8 @@ theory KernelInitSep_AI imports - "../../spec/abstract/KernelInit_A" - "../../lib/sep_algebra/Sep_Algebra_L4v" + "ASpec.KernelInit_A" + "Sep_Algebra.Sep_Algebra_L4v" Invariants_AI begin diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index 014715c46..7b35631a4 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -12,7 +12,7 @@ theory Untyped_AI imports "./$L4V_ARCH/ArchDetype_AI" - "../../lib/MonadicRewrite" + "Lib.MonadicRewrite" begin context begin interpretation Arch . diff --git a/proof/invariant-abstract/X64/ArchADT_AI.thy b/proof/invariant-abstract/X64/ArchADT_AI.thy index 45d4d4934..d61e0c91d 100644 --- a/proof/invariant-abstract/X64/ArchADT_AI.thy +++ b/proof/invariant-abstract/X64/ArchADT_AI.thy @@ -12,7 +12,7 @@ chapter {* X64-specific definitions for abstract datatype for the abstract speci theory ArchADT_AI imports - "../../../lib/Simulation" + "Lib.Simulation" "../Invariants_AI" begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchAcc_AI.thy b/proof/invariant-abstract/X64/ArchAcc_AI.thy index 10075ed55..d89bf2d47 100644 --- a/proof/invariant-abstract/X64/ArchAcc_AI.thy +++ b/proof/invariant-abstract/X64/ArchAcc_AI.thy @@ -13,8 +13,7 @@ Lemmas on arch get/set object etc *) theory ArchAcc_AI -imports "../SubMonad_AI" "ArchVSpaceLookup_AI" - "../../../lib/Crunch_Instances_NonDet" +imports "../SubMonad_AI" "ArchVSpaceLookup_AI" "Lib.Crunch_Instances_NonDet" begin diff --git a/proof/invariant-abstract/X64/ArchCrunchSetup_AI.thy b/proof/invariant-abstract/X64/ArchCrunchSetup_AI.thy index caf51403f..98c23c324 100644 --- a/proof/invariant-abstract/X64/ArchCrunchSetup_AI.thy +++ b/proof/invariant-abstract/X64/ArchCrunchSetup_AI.thy @@ -10,8 +10,8 @@ theory ArchCrunchSetup_AI imports - "../../../spec/abstract/Syscall_A" - "../../../lib/Crunch_Instances_NonDet" + "ASpec.Syscall_A" + "Lib.Crunch_Instances_NonDet" begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchInvariants_AI.thy b/proof/invariant-abstract/X64/ArchInvariants_AI.thy index 3632962f5..9bb73ea05 100644 --- a/proof/invariant-abstract/X64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/X64/ArchInvariants_AI.thy @@ -9,7 +9,7 @@ *) theory ArchInvariants_AI -imports "../InvariantsPre_AI" "../../../lib/Apply_Trace_Cmd" +imports "../InvariantsPre_AI" "Lib.Apply_Trace_Cmd" begin section "Move this up" diff --git a/proof/invariant-abstract/X64/ArchLevityCatch_AI.thy b/proof/invariant-abstract/X64/ArchLevityCatch_AI.thy index 4b0f27443..c69792eb8 100644 --- a/proof/invariant-abstract/X64/ArchLevityCatch_AI.thy +++ b/proof/invariant-abstract/X64/ArchLevityCatch_AI.thy @@ -11,8 +11,8 @@ theory ArchLevityCatch_AI imports "../BCorres_AI" - "../../../lib/LemmaBucket" - "../../../lib/SplitRule" + "Lib.LemmaBucket" + "Lib.SplitRule" begin context Arch begin global_naming X64 diff --git a/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy b/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy index c1d6f45c1..0ac8a0de6 100644 --- a/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpaceLookup_AI.thy @@ -10,7 +10,7 @@ theory ArchVSpaceLookup_AI imports "../SubMonad_AI" - "../../../lib/Crunch_Instances_NonDet" + "Lib.Crunch_Instances_NonDet" begin definition diff --git a/proof/refine/ARM/ADT_H.thy b/proof/refine/ARM/ADT_H.thy index 14ca04d7f..7604330ce 100644 --- a/proof/refine/ARM/ADT_H.thy +++ b/proof/refine/ARM/ADT_H.thy @@ -12,7 +12,7 @@ chapter {* Abstract datatype for the executable specification *} theory ADT_H imports - "../../invariant-abstract/ADT_AI" + "AInvs.ADT_AI" Syscall_R begin diff --git a/proof/refine/ARM/BuildRefineCache.thy b/proof/refine/ARM/BuildRefineCache.thy index dd5033b75..17eb42005 100644 --- a/proof/refine/ARM/BuildRefineCache.thy +++ b/proof/refine/ARM/BuildRefineCache.thy @@ -9,7 +9,7 @@ *) theory BuildRefineCache -imports "~~/src/HOL/Main" +imports Main begin ML {* diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy index 546723cb6..616deae2d 100644 --- a/proof/refine/ARM/CSpace1_R.thy +++ b/proof/refine/ARM/CSpace1_R.thy @@ -15,7 +15,7 @@ theory CSpace1_R imports CSpace_I - "../../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI" + "AInvs.ArchDetSchedSchedule_AI" begin context Arch begin global_naming ARM_A (*FIXME: arch_split*) diff --git a/proof/refine/ARM/Cache.thy b/proof/refine/ARM/Cache.thy index c800ed1d6..a4bc896f5 100644 --- a/proof/refine/ARM/Cache.thy +++ b/proof/refine/ARM/Cache.thy @@ -9,7 +9,7 @@ *) theory Cache -imports "~~/src/HOL/Main" +imports Main begin text {* Enable the proof cache, both skipping from it diff --git a/proof/refine/ARM/Corres.thy b/proof/refine/ARM/Corres.thy index 986404427..952d1d63b 100644 --- a/proof/refine/ARM/Corres.thy +++ b/proof/refine/ARM/Corres.thy @@ -9,7 +9,7 @@ *) theory Corres -imports StateRelation "../../../lib/CorresK_Lemmas" +imports StateRelation "CorresK.CorresK_Lemmas" begin text {* Instantiating the corres framework to this particular state relation. *} diff --git a/proof/refine/ARM/Include.thy b/proof/refine/ARM/Include.thy index 500aa3128..fd122988d 100644 --- a/proof/refine/ARM/Include.thy +++ b/proof/refine/ARM/Include.thy @@ -10,9 +10,9 @@ theory Include imports - "../../../spec/abstract/Syscall_A" - "../../../spec/design/API_H" - "../../../spec/design/$L4V_ARCH/ArchIntermediate_H" + "ASpec.Syscall_A" + "ExecSpec.API_H" + "ExecSpec.ArchIntermediate_H" begin no_notation bind_drop (infixl ">>" 60) diff --git a/proof/refine/ARM/Invariants_H.thy b/proof/refine/ARM/Invariants_H.thy index 0ed7fa4d8..1557d4623 100644 --- a/proof/refine/ARM/Invariants_H.thy +++ b/proof/refine/ARM/Invariants_H.thy @@ -11,9 +11,9 @@ theory Invariants_H imports LevityCatch - "../../invariant-abstract/Deterministic_AI" - "../../invariant-abstract/AInvs" - "../../../lib/AddUpdSimps" + "AInvs.Deterministic_AI" + "AInvs.AInvs" + "Lib.AddUpdSimps" begin context Arch begin diff --git a/proof/refine/ARM/IpcCancel_R.thy b/proof/refine/ARM/IpcCancel_R.thy index aff6878b0..8d9e25b16 100644 --- a/proof/refine/ARM/IpcCancel_R.thy +++ b/proof/refine/ARM/IpcCancel_R.thy @@ -11,7 +11,7 @@ theory IpcCancel_R imports Schedule_R - "../../../lib/SimpStrategy" + "Lib.SimpStrategy" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/refine/ARM/KHeap_R.thy b/proof/refine/ARM/KHeap_R.thy index d47e215fc..4d7576302 100644 --- a/proof/refine/ARM/KHeap_R.thy +++ b/proof/refine/ARM/KHeap_R.thy @@ -10,7 +10,7 @@ theory KHeap_R imports - "../../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI" + "AInvs.ArchDetSchedSchedule_AI" Machine_R begin diff --git a/proof/refine/ARM/KernelInit_R.thy b/proof/refine/ARM/KernelInit_R.thy index 69b7455d8..490e85162 100644 --- a/proof/refine/ARM/KernelInit_R.thy +++ b/proof/refine/ARM/KernelInit_R.thy @@ -14,7 +14,7 @@ theory KernelInit_R imports IncKernelInit - "../../invariant-abstract/KernelInit_AI" + "AInvs.KernelInit_AI" begin (* Axiomatisation of the rest of the initialisation code *) diff --git a/proof/refine/ARM/LevityCatch.thy b/proof/refine/ARM/LevityCatch.thy index 5d52d4767..4f88c8b49 100644 --- a/proof/refine/ARM/LevityCatch.thy +++ b/proof/refine/ARM/LevityCatch.thy @@ -11,7 +11,7 @@ theory LevityCatch imports Include - "../../../lib/LemmaBucket" + "Lib.LemmaBucket" begin (* Try again, clagged from Include *) diff --git a/proof/refine/ARM/RAB_FN.thy b/proof/refine/ARM/RAB_FN.thy index 7d69f32da..092c86e71 100644 --- a/proof/refine/ARM/RAB_FN.thy +++ b/proof/refine/ARM/RAB_FN.thy @@ -12,7 +12,7 @@ theory RAB_FN imports "CSpace1_R" - "../../../lib/MonadicRewrite" + "Lib.MonadicRewrite" begin diff --git a/proof/refine/ARM_HYP/ADT_H.thy b/proof/refine/ARM_HYP/ADT_H.thy index daf8099d1..8b4ddea88 100644 --- a/proof/refine/ARM_HYP/ADT_H.thy +++ b/proof/refine/ARM_HYP/ADT_H.thy @@ -12,7 +12,7 @@ chapter {* Abstract datatype for the executable specification *} theory ADT_H imports - "../../invariant-abstract/ADT_AI" + "AInvs.ADT_AI" Syscall_R begin diff --git a/proof/refine/ARM_HYP/BuildRefineCache.thy b/proof/refine/ARM_HYP/BuildRefineCache.thy index dd5033b75..17eb42005 100644 --- a/proof/refine/ARM_HYP/BuildRefineCache.thy +++ b/proof/refine/ARM_HYP/BuildRefineCache.thy @@ -9,7 +9,7 @@ *) theory BuildRefineCache -imports "~~/src/HOL/Main" +imports Main begin ML {* diff --git a/proof/refine/ARM_HYP/CSpace1_R.thy b/proof/refine/ARM_HYP/CSpace1_R.thy index cb10e7071..ee923bfee 100644 --- a/proof/refine/ARM_HYP/CSpace1_R.thy +++ b/proof/refine/ARM_HYP/CSpace1_R.thy @@ -15,7 +15,7 @@ theory CSpace1_R imports CSpace_I - "../../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI" + "AInvs.ArchDetSchedSchedule_AI" begin context Arch begin global_naming ARM_A (*FIXME: arch_split*) diff --git a/proof/refine/ARM_HYP/Cache.thy b/proof/refine/ARM_HYP/Cache.thy index c800ed1d6..a4bc896f5 100644 --- a/proof/refine/ARM_HYP/Cache.thy +++ b/proof/refine/ARM_HYP/Cache.thy @@ -9,7 +9,7 @@ *) theory Cache -imports "~~/src/HOL/Main" +imports Main begin text {* Enable the proof cache, both skipping from it diff --git a/proof/refine/ARM_HYP/Corres.thy b/proof/refine/ARM_HYP/Corres.thy index aba52e6ef..f2e6b048e 100644 --- a/proof/refine/ARM_HYP/Corres.thy +++ b/proof/refine/ARM_HYP/Corres.thy @@ -9,7 +9,7 @@ *) theory Corres -imports StateRelation "../../../lib/CorresK_Lemmas" +imports StateRelation "CorresK.CorresK_Lemmas" begin text {* Instantiating the corres framework to this particular state relation. *} diff --git a/proof/refine/ARM_HYP/Include.thy b/proof/refine/ARM_HYP/Include.thy index 500aa3128..fd122988d 100644 --- a/proof/refine/ARM_HYP/Include.thy +++ b/proof/refine/ARM_HYP/Include.thy @@ -10,9 +10,9 @@ theory Include imports - "../../../spec/abstract/Syscall_A" - "../../../spec/design/API_H" - "../../../spec/design/$L4V_ARCH/ArchIntermediate_H" + "ASpec.Syscall_A" + "ExecSpec.API_H" + "ExecSpec.ArchIntermediate_H" begin no_notation bind_drop (infixl ">>" 60) diff --git a/proof/refine/ARM_HYP/Invariants_H.thy b/proof/refine/ARM_HYP/Invariants_H.thy index 285eba326..53262b946 100644 --- a/proof/refine/ARM_HYP/Invariants_H.thy +++ b/proof/refine/ARM_HYP/Invariants_H.thy @@ -11,9 +11,9 @@ theory Invariants_H imports LevityCatch - "../../invariant-abstract/Deterministic_AI" - "../../invariant-abstract/AInvs" - "../../../lib/AddUpdSimps" + "AInvs.Deterministic_AI" + "AInvs.AInvs" + "Lib.AddUpdSimps" begin context Arch begin diff --git a/proof/refine/ARM_HYP/IpcCancel_R.thy b/proof/refine/ARM_HYP/IpcCancel_R.thy index 4a931386d..a35dd1d50 100644 --- a/proof/refine/ARM_HYP/IpcCancel_R.thy +++ b/proof/refine/ARM_HYP/IpcCancel_R.thy @@ -11,7 +11,7 @@ theory IpcCancel_R imports Schedule_R - "../../../lib/SimpStrategy" + "Lib.SimpStrategy" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/refine/ARM_HYP/KHeap_R.thy b/proof/refine/ARM_HYP/KHeap_R.thy index 6a559d814..dd3c38c93 100644 --- a/proof/refine/ARM_HYP/KHeap_R.thy +++ b/proof/refine/ARM_HYP/KHeap_R.thy @@ -10,7 +10,7 @@ theory KHeap_R imports - "../../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI" + "AInvs.ArchDetSchedSchedule_AI" Machine_R begin diff --git a/proof/refine/ARM_HYP/KernelInit_R.thy b/proof/refine/ARM_HYP/KernelInit_R.thy index 69b7455d8..490e85162 100644 --- a/proof/refine/ARM_HYP/KernelInit_R.thy +++ b/proof/refine/ARM_HYP/KernelInit_R.thy @@ -14,7 +14,7 @@ theory KernelInit_R imports IncKernelInit - "../../invariant-abstract/KernelInit_AI" + "AInvs.KernelInit_AI" begin (* Axiomatisation of the rest of the initialisation code *) diff --git a/proof/refine/ARM_HYP/LevityCatch.thy b/proof/refine/ARM_HYP/LevityCatch.thy index 30a243e99..4c0de9f34 100644 --- a/proof/refine/ARM_HYP/LevityCatch.thy +++ b/proof/refine/ARM_HYP/LevityCatch.thy @@ -11,7 +11,7 @@ theory LevityCatch imports Include - "../../../lib/LemmaBucket" + "Lib.LemmaBucket" begin (* Try again, clagged from Include *) diff --git a/proof/refine/ARM_HYP/RAB_FN.thy b/proof/refine/ARM_HYP/RAB_FN.thy index 7d69f32da..092c86e71 100644 --- a/proof/refine/ARM_HYP/RAB_FN.thy +++ b/proof/refine/ARM_HYP/RAB_FN.thy @@ -12,7 +12,7 @@ theory RAB_FN imports "CSpace1_R" - "../../../lib/MonadicRewrite" + "Lib.MonadicRewrite" begin diff --git a/proof/refine/X64/ADT_H.thy b/proof/refine/X64/ADT_H.thy index 331f3da5b..4fd4e1225 100644 --- a/proof/refine/X64/ADT_H.thy +++ b/proof/refine/X64/ADT_H.thy @@ -12,7 +12,7 @@ chapter {* Abstract datatype for the executable specification *} theory ADT_H imports - "../../invariant-abstract/ADT_AI" + "AInvs.ADT_AI" Syscall_R begin diff --git a/proof/refine/X64/BuildRefineCache.thy b/proof/refine/X64/BuildRefineCache.thy index dd5033b75..17eb42005 100644 --- a/proof/refine/X64/BuildRefineCache.thy +++ b/proof/refine/X64/BuildRefineCache.thy @@ -9,7 +9,7 @@ *) theory BuildRefineCache -imports "~~/src/HOL/Main" +imports Main begin ML {* diff --git a/proof/refine/X64/CSpace1_R.thy b/proof/refine/X64/CSpace1_R.thy index 5036c2524..aefa25f3f 100644 --- a/proof/refine/X64/CSpace1_R.thy +++ b/proof/refine/X64/CSpace1_R.thy @@ -15,7 +15,7 @@ theory CSpace1_R imports CSpace_I - "../../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI" + "AInvs.ArchDetSchedSchedule_AI" begin context Arch begin global_naming X64_A (*FIXME: arch_split*) diff --git a/proof/refine/X64/Cache.thy b/proof/refine/X64/Cache.thy index c800ed1d6..a4bc896f5 100644 --- a/proof/refine/X64/Cache.thy +++ b/proof/refine/X64/Cache.thy @@ -9,7 +9,7 @@ *) theory Cache -imports "~~/src/HOL/Main" +imports Main begin text {* Enable the proof cache, both skipping from it diff --git a/proof/refine/X64/Corres.thy b/proof/refine/X64/Corres.thy index b00aecc30..21f376822 100644 --- a/proof/refine/X64/Corres.thy +++ b/proof/refine/X64/Corres.thy @@ -9,7 +9,7 @@ *) theory Corres -imports StateRelation "../../../lib/CorresK_Lemmas" +imports StateRelation "CorresK.CorresK_Lemmas" begin text {* Instantiating the corres framework to this particular state relation. *} diff --git a/proof/refine/X64/Include.thy b/proof/refine/X64/Include.thy index 500aa3128..fd122988d 100644 --- a/proof/refine/X64/Include.thy +++ b/proof/refine/X64/Include.thy @@ -10,9 +10,9 @@ theory Include imports - "../../../spec/abstract/Syscall_A" - "../../../spec/design/API_H" - "../../../spec/design/$L4V_ARCH/ArchIntermediate_H" + "ASpec.Syscall_A" + "ExecSpec.API_H" + "ExecSpec.ArchIntermediate_H" begin no_notation bind_drop (infixl ">>" 60) diff --git a/proof/refine/X64/Invariants_H.thy b/proof/refine/X64/Invariants_H.thy index 478b45e64..6a58e06df 100644 --- a/proof/refine/X64/Invariants_H.thy +++ b/proof/refine/X64/Invariants_H.thy @@ -11,9 +11,9 @@ theory Invariants_H imports LevityCatch - "../../invariant-abstract/Deterministic_AI" - "../../invariant-abstract/AInvs" - "../../../lib/AddUpdSimps" + "AInvs.Deterministic_AI" + "AInvs.AInvs" + "Lib.AddUpdSimps" begin context Arch begin diff --git a/proof/refine/X64/IpcCancel_R.thy b/proof/refine/X64/IpcCancel_R.thy index 733d3a657..c3b66ee8f 100644 --- a/proof/refine/X64/IpcCancel_R.thy +++ b/proof/refine/X64/IpcCancel_R.thy @@ -11,7 +11,7 @@ theory IpcCancel_R imports Schedule_R - "../../../lib/SimpStrategy" + "Lib.SimpStrategy" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/refine/X64/KHeap_R.thy b/proof/refine/X64/KHeap_R.thy index 5b1e370fb..6b97c9e40 100644 --- a/proof/refine/X64/KHeap_R.thy +++ b/proof/refine/X64/KHeap_R.thy @@ -10,7 +10,7 @@ theory KHeap_R imports - "../../invariant-abstract/$L4V_ARCH/ArchDetSchedSchedule_AI" + "AInvs.ArchDetSchedSchedule_AI" Machine_R begin diff --git a/proof/refine/X64/KernelInit_R.thy b/proof/refine/X64/KernelInit_R.thy index e19976363..fdf174bf8 100644 --- a/proof/refine/X64/KernelInit_R.thy +++ b/proof/refine/X64/KernelInit_R.thy @@ -14,7 +14,7 @@ theory KernelInit_R imports IncKernelInit - "../../invariant-abstract/KernelInit_AI" + "AInvs.KernelInit_AI" begin (* Axiomatisation of the rest of the initialisation code *) diff --git a/proof/refine/X64/LevityCatch.thy b/proof/refine/X64/LevityCatch.thy index 3100e6499..035fd20d6 100644 --- a/proof/refine/X64/LevityCatch.thy +++ b/proof/refine/X64/LevityCatch.thy @@ -11,7 +11,7 @@ theory LevityCatch imports Include - "../../../lib/LemmaBucket" + "Lib.LemmaBucket" begin (* Try again, clagged from Include *) diff --git a/proof/refine/X64/RAB_FN.thy b/proof/refine/X64/RAB_FN.thy index 143d26334..325f8882a 100644 --- a/proof/refine/X64/RAB_FN.thy +++ b/proof/refine/X64/RAB_FN.thy @@ -12,7 +12,7 @@ theory RAB_FN imports "CSpace1_R" - "../../../lib/MonadicRewrite" + "Lib.MonadicRewrite" begin diff --git a/proof/sep-capDL/AbstractSeparationHelpers_SD.thy b/proof/sep-capDL/AbstractSeparationHelpers_SD.thy index 9989147f9..1cb3f1330 100644 --- a/proof/sep-capDL/AbstractSeparationHelpers_SD.thy +++ b/proof/sep-capDL/AbstractSeparationHelpers_SD.thy @@ -10,7 +10,7 @@ theory AbstractSeparationHelpers_SD imports - "../../lib/sep_algebra/Sep_Algebra_L4v" + "Sep_Algebra.Sep_Algebra_L4v" begin (* diff --git a/proof/sep-capDL/AbstractSeparation_SD.thy b/proof/sep-capDL/AbstractSeparation_SD.thy index 02d0f9beb..ec03af669 100644 --- a/proof/sep-capDL/AbstractSeparation_SD.thy +++ b/proof/sep-capDL/AbstractSeparation_SD.thy @@ -11,8 +11,8 @@ theory AbstractSeparation_SD imports AbstractSeparationHelpers_SD - "../../lib/sep_algebra/Map_Extra" - "../../spec/capDL/Types_D" + "Sep_Algebra.Map_Extra" + "DSpec.Types_D" begin datatype cdl_component_id = Fields | Slot nat diff --git a/proof/sep-capDL/Helpers_SD.thy b/proof/sep-capDL/Helpers_SD.thy index c48f14cb8..e11ebfea9 100644 --- a/proof/sep-capDL/Helpers_SD.thy +++ b/proof/sep-capDL/Helpers_SD.thy @@ -11,9 +11,9 @@ theory Helpers_SD imports "Lookups_D" - "../../lib/SimpStrategy" - "../../lib/LemmaBucket" - "../../lib/sep_algebra/Map_Extra" + "Lib.SimpStrategy" + "Lib.LemmaBucket" + "Sep_Algebra.Map_Extra" begin (* Functions we need from capDL, but can't have yet (until we change capDL). diff --git a/proof/sep-capDL/Lookups_D.thy b/proof/sep-capDL/Lookups_D.thy index c3d35ffec..084154ce5 100644 --- a/proof/sep-capDL/Lookups_D.thy +++ b/proof/sep-capDL/Lookups_D.thy @@ -10,8 +10,8 @@ theory Lookups_D imports - "../../spec/capDL/Syscall_D" - "../../lib/Monad_WP/OptionMonadND" + "DSpec.Syscall_D" + "Lib.OptionMonadND" begin type_synonym 'a lookup = "cdl_state \ 'a option" diff --git a/proof/sep-capDL/Sep_Tactic_Helper.thy b/proof/sep-capDL/Sep_Tactic_Helper.thy index acab12908..b5d2a193a 100644 --- a/proof/sep-capDL/Sep_Tactic_Helper.thy +++ b/proof/sep-capDL/Sep_Tactic_Helper.thy @@ -10,8 +10,8 @@ theory Sep_Tactic_Helper imports - "../../lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics" - "../../lib/sep_algebra/MonadSep" + "SepTactics.Hoare_Sep_Tactics" + "Sep_Algebra.MonadSep" begin lemma no_exception_conjE: diff --git a/spec/ROOT b/spec/ROOT index 20bb58263..da2b3c316 100644 --- a/spec/ROOT +++ b/spec/ROOT @@ -33,6 +33,10 @@ chapter "Specifications" (* Session on which most other sessions build. *) session ASpec in "abstract" = Word_Lib + options [document=false] + sessions + "HOL-Library" + Lib + ExecSpec theories "Syscall_A" @@ -41,16 +45,12 @@ session ASpec in "abstract" = Word_Lib + whenever the git commit ID changes. *) session ASpecDoc in "abstract" = Word_Lib + options [document=pdf] - theories [document = false] - "../../lib/Lib" - "../../lib/Defs" - "../../lib/List_Lib" - "../../lib/$L4V_ARCH/WordSetup" + sessions + "HOL-Library" + Lib + ExecSpec theories "Intro_Doc" - "../../lib/Monad_WP/NonDetMonad" - theories [document = false] - "../../lib/Monad_WP/NonDetMonadLemmas" theories "Syscall_A" "Glossary_Doc" @@ -77,6 +77,9 @@ session ASpecDoc in "abstract" = Word_Lib + session ExecSpec = Word_Lib + options [document = false] + sessions + Lib + "HOL-Eisbach" theories "design/API_H" "design/$L4V_ARCH/ArchIntermediate_H" @@ -96,6 +99,9 @@ session CSpec = CKernel + "cspec/KernelState_C" session CKernel = CParser + + sessions + "ExecSpec" + "CLib" theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty] "cspec/$L4V_ARCH/Kernel_C" theories @@ -104,23 +110,26 @@ session CKernel = CParser + "cspec/c/build/$L4V_ARCH/kernel_all.c_pp" session SimplExport = CSpec + - theories "cspec/SimplExport" + theories "../tools/asmrefine/SimplExport" (* * CapDL *) -session DSpec = Word_Lib + +session DSpec in capDL = Word_Lib + + sessions + ExecSpec + ASpec theories - "capDL/Syscall_D" + Syscall_D (* * Take-Grant. *) -session TakeGrant in "take-grant" = "HOL-Word" + +session TakeGrant in "take-grant" = Word_Lib + theories "System_S" "Isolation_S" diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy index 96757bfcf..0b127c80f 100644 --- a/spec/abstract/ARM/Arch_Structs_A.thy +++ b/spec/abstract/ARM/Arch_Structs_A.thy @@ -16,7 +16,7 @@ chapter "ARM-Specific Data Types" theory Arch_Structs_A imports - "../../design/$L4V_ARCH/Arch_Structs_B" + "ExecSpec.Arch_Structs_B" "../ExceptionTypes_A" "../VMRights_A" begin diff --git a/spec/abstract/ARM/Machine_A.thy b/spec/abstract/ARM/Machine_A.thy index 28482bdcc..1964a54c0 100644 --- a/spec/abstract/ARM/Machine_A.thy +++ b/spec/abstract/ARM/Machine_A.thy @@ -17,7 +17,7 @@ chapter "ARM Machine Instantiation" theory Machine_A imports - "../../machine/$L4V_ARCH/MachineTypes" + "ExecSpec.MachineTypes" begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/ARM_HYP/Arch_Structs_A.thy b/spec/abstract/ARM_HYP/Arch_Structs_A.thy index 766c50c51..e6fa1406e 100644 --- a/spec/abstract/ARM_HYP/Arch_Structs_A.thy +++ b/spec/abstract/ARM_HYP/Arch_Structs_A.thy @@ -16,7 +16,7 @@ chapter "ARM-Specific Data Types" theory Arch_Structs_A imports - "../../design/$L4V_ARCH/Arch_Structs_B" + "ExecSpec.Arch_Structs_B" "../ExceptionTypes_A" "../VMRights_A" begin diff --git a/spec/abstract/ARM_HYP/Machine_A.thy b/spec/abstract/ARM_HYP/Machine_A.thy index 12350960e..70c763f17 100644 --- a/spec/abstract/ARM_HYP/Machine_A.thy +++ b/spec/abstract/ARM_HYP/Machine_A.thy @@ -17,7 +17,7 @@ chapter "ARM Machine Instantiation" theory Machine_A imports - "../../machine/$L4V_ARCH/MachineTypes" + "ExecSpec.MachineTypes" begin context Arch begin global_naming ARM_A diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy index dbea799db..4ed0e19a4 100644 --- a/spec/abstract/CSpace_A.thy +++ b/spec/abstract/CSpace_A.thy @@ -19,8 +19,8 @@ imports "./$L4V_ARCH/ArchVSpace_A" IpcCancel_A "./$L4V_ARCH/ArchCSpace_A" - "../../lib/Monad_WP/NonDetMonadLemmas" - "~~/src/HOL/Library/Prefix_Order" + "Lib.NonDetMonadLemmas" + "HOL-Library.Prefix_Order" begin context begin interpretation Arch . diff --git a/spec/abstract/CapRights_A.thy b/spec/abstract/CapRights_A.thy index b5337d838..93e5ca574 100644 --- a/spec/abstract/CapRights_A.thy +++ b/spec/abstract/CapRights_A.thy @@ -15,7 +15,7 @@ Definition of access rights. chapter "Access Rights" theory CapRights_A -imports "~~/src/HOL/Main" +imports Main begin text {* The possible access-control rights that exist in the system. diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 9c59f7956..8ee5eb4df 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -18,7 +18,7 @@ theory Decode_A imports Interrupt_A "./$L4V_ARCH/ArchDecode_A" - "../design/InvocationLabels_H" + "ExecSpec.InvocationLabels_H" begin context begin interpretation Arch . diff --git a/spec/abstract/Deterministic_A.thy b/spec/abstract/Deterministic_A.thy index 20842ed4c..ed8e14cd7 100644 --- a/spec/abstract/Deterministic_A.thy +++ b/spec/abstract/Deterministic_A.thy @@ -13,7 +13,7 @@ chapter "Abstract Specification Instantiations" theory Deterministic_A imports Structures_A - "../../lib/List_Lib" + "Lib.List_Lib" begin diff --git a/spec/abstract/Intro_Doc.thy b/spec/abstract/Intro_Doc.thy index 964ece96f..d928a090e 100644 --- a/spec/abstract/Intro_Doc.thy +++ b/spec/abstract/Intro_Doc.thy @@ -16,7 +16,7 @@ chapter "Introduction" (*<*) theory Intro_Doc -imports "~~/src/HOL/Main" +imports Main begin (*>*) text {* diff --git a/spec/abstract/InvocationLabels_A.thy b/spec/abstract/InvocationLabels_A.thy index 39dc36def..6a3993454 100644 --- a/spec/abstract/InvocationLabels_A.thy +++ b/spec/abstract/InvocationLabels_A.thy @@ -17,7 +17,7 @@ chapter "Kernel Object Invocations" theory InvocationLabels_A imports MiscMachine_A - "../design/$L4V_ARCH/ArchLabelFuns_H" + "ExecSpec.ArchLabelFuns_H" begin definition diff --git a/spec/abstract/MiscMachine_A.thy b/spec/abstract/MiscMachine_A.thy index dec587e74..260a75b34 100644 --- a/spec/abstract/MiscMachine_A.thy +++ b/spec/abstract/MiscMachine_A.thy @@ -15,7 +15,7 @@ Utilities for the machine level which are not machine-dependent. chapter "Machine Accessor Functions" theory MiscMachine_A -imports "./$L4V_ARCH/Machine_A" "../machine/MachineExports" +imports "./$L4V_ARCH/Machine_A" "ExecSpec.MachineExports" begin context begin interpretation Arch . diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index a74b6ddec..f4cec2b99 100644 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -18,7 +18,7 @@ chapter "Basic Data Structures" theory Structures_A imports "./$L4V_ARCH/Arch_Structs_A" - "../machine/MachineExports" + "ExecSpec.MachineExports" begin diff --git a/spec/abstract/Syscall_A.thy b/spec/abstract/Syscall_A.thy index a8a61e347..8e94ca4dc 100644 --- a/spec/abstract/Syscall_A.thy +++ b/spec/abstract/Syscall_A.thy @@ -16,7 +16,7 @@ chapter "System Calls" theory Syscall_A imports - "../design/Event_H" + "ExecSpec.Event_H" Decode_A "./$L4V_ARCH/Init_A" "./$L4V_ARCH/Hypervisor_A" diff --git a/spec/abstract/X64/ArchDecode_A.thy b/spec/abstract/X64/ArchDecode_A.thy index 844f04816..3f2a96377 100644 --- a/spec/abstract/X64/ArchDecode_A.thy +++ b/spec/abstract/X64/ArchDecode_A.thy @@ -18,8 +18,8 @@ theory ArchDecode_A imports "../Interrupt_A" "../InvocationLabels_A" - "../../../lib/Word_Lib/Word_Lib" - "../../design/InvocationLabels_H" + "Word_Lib.Word_Lib" + "ExecSpec.InvocationLabels_H" begin context Arch begin global_naming X64_A diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy index d22cd232f..0ad216d16 100644 --- a/spec/abstract/X64/Arch_Structs_A.thy +++ b/spec/abstract/X64/Arch_Structs_A.thy @@ -12,7 +12,7 @@ chapter "x64-Specific Data Types" theory Arch_Structs_A imports - "../../design/$L4V_ARCH/Arch_Structs_B" + "ExecSpec.Arch_Structs_B" "../ExceptionTypes_A" "../VMRights_A" begin diff --git a/spec/abstract/X64/Machine_A.thy b/spec/abstract/X64/Machine_A.thy index 969366dac..84c276e9c 100644 --- a/spec/abstract/X64/Machine_A.thy +++ b/spec/abstract/X64/Machine_A.thy @@ -17,10 +17,10 @@ chapter "x64 Machine Instantiation" theory Machine_A imports - "../../../lib/$L4V_ARCH/WordSetup" - "../../../lib/Monad_WP/NonDetMonad" - "../../machine/$L4V_ARCH/MachineTypes" - "../../machine/$L4V_ARCH/MachineOps" + "Word_Lib.WordSetup" + "Lib.NonDetMonad" + "ExecSpec.MachineTypes" + "ExecSpec.MachineOps" begin context Arch begin global_naming X64_A diff --git a/spec/capDL/Intents_D.thy b/spec/capDL/Intents_D.thy index 6d9c244dc..e3f996fa4 100644 --- a/spec/capDL/Intents_D.thy +++ b/spec/capDL/Intents_D.thy @@ -28,8 +28,8 @@ theory Intents_D imports - "../../lib/$L4V_ARCH/WordSetup" - "../abstract/CapRights_A" + "Word_Lib.WordSetup" + "ASpec.CapRights_A" begin (* diff --git a/spec/capDL/Interrupt_D.thy b/spec/capDL/Interrupt_D.thy index efc4c4c70..75f00d1ad 100644 --- a/spec/capDL/Interrupt_D.thy +++ b/spec/capDL/Interrupt_D.thy @@ -13,7 +13,7 @@ *) theory Interrupt_D -imports Endpoint_D "../machine/$L4V_ARCH/Platform" +imports Endpoint_D "ExecSpec.Platform" begin context begin interpretation Arch . diff --git a/spec/capDL/Monads_D.thy b/spec/capDL/Monads_D.thy index 94f98b810..3ed1ed02a 100644 --- a/spec/capDL/Monads_D.thy +++ b/spec/capDL/Monads_D.thy @@ -15,7 +15,7 @@ theory Monads_D imports Types_D - "../../lib/Monad_WP/NonDetMonadVCG" + "Lib.NonDetMonadVCG" begin (* Kernel state monad *) diff --git a/spec/capDL/Syscall_D.thy b/spec/capDL/Syscall_D.thy index 3a7464612..a1e953a88 100644 --- a/spec/capDL/Syscall_D.thy +++ b/spec/capDL/Syscall_D.thy @@ -16,7 +16,7 @@ theory Syscall_D imports Schedule_D Decode_D - "../design/Event_H" + "ExecSpec.Event_H" begin (* diff --git a/spec/capDL/Types_D.thy b/spec/capDL/Types_D.thy index 41909c7b4..cc499990a 100644 --- a/spec/capDL/Types_D.thy +++ b/spec/capDL/Types_D.thy @@ -17,9 +17,9 @@ theory Types_D imports - "../abstract/VMRights_A" + "ASpec.VMRights_A" Intents_D - "../../lib/SplitRule" + "Lib.SplitRule" begin (* A hardware IRQ number. *) diff --git a/spec/cspec/ARM/Kernel_C.thy b/spec/cspec/ARM/Kernel_C.thy index 0339c9df3..fa41532df 100644 --- a/spec/cspec/ARM/Kernel_C.thy +++ b/spec/cspec/ARM/Kernel_C.thy @@ -10,8 +10,8 @@ theory Kernel_C imports - "../../machine/$L4V_ARCH/MachineTypes" - "../../../lib/CTranslationNICTA" + "ExecSpec.MachineTypes" + "CLib.CTranslationNICTA" "../../../tools/asmrefine/CommonOps" begin diff --git a/spec/cspec/ARM_HYP/Kernel_C.thy b/spec/cspec/ARM_HYP/Kernel_C.thy index 0339c9df3..fa41532df 100644 --- a/spec/cspec/ARM_HYP/Kernel_C.thy +++ b/spec/cspec/ARM_HYP/Kernel_C.thy @@ -10,8 +10,8 @@ theory Kernel_C imports - "../../machine/$L4V_ARCH/MachineTypes" - "../../../lib/CTranslationNICTA" + "ExecSpec.MachineTypes" + "CLib.CTranslationNICTA" "../../../tools/asmrefine/CommonOps" begin diff --git a/spec/cspec/KernelState_C.thy b/spec/cspec/KernelState_C.thy index 51240f7e9..644bb7d18 100644 --- a/spec/cspec/KernelState_C.thy +++ b/spec/cspec/KernelState_C.thy @@ -10,8 +10,8 @@ theory KernelState_C imports - "../../lib/$L4V_ARCH/WordSetup" - "../../lib/BitFieldProofsLib" + "Word_Lib.WordSetup" + "CLib.BitFieldProofsLib" "$L4V_ARCH/Kernel_C" "Substitute" begin diff --git a/spec/cspec/TypHeapLimits.thy b/spec/cspec/TypHeapLimits.thy index 5b0546b06..130e91e12 100644 --- a/spec/cspec/TypHeapLimits.thy +++ b/spec/cspec/TypHeapLimits.thy @@ -9,7 +9,7 @@ *) theory TypHeapLimits -imports "../../lib/TypHeapLib" +imports "CLib.TypHeapLib" begin definition diff --git a/spec/cspec/X64/Kernel_C.thy b/spec/cspec/X64/Kernel_C.thy index 2a4d79d77..498643ae6 100644 --- a/spec/cspec/X64/Kernel_C.thy +++ b/spec/cspec/X64/Kernel_C.thy @@ -10,8 +10,8 @@ theory Kernel_C imports - "../../machine/$L4V_ARCH/MachineTypes" - "../../../lib/CTranslationNICTA" + "ExecSpec.MachineTypes" + "CLib.CTranslationNICTA" "../../../tools/asmrefine/CommonOps" begin diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy index 66230c08c..4f6b24017 100644 --- a/spec/design/m-skel/ARM/MachineTypes.thy +++ b/spec/design/m-skel/ARM/MachineTypes.thy @@ -12,7 +12,7 @@ chapter "ARM Machine Types" theory MachineTypes imports - "../../../lib/Monad_WP/NonDetMonad" + "Lib.NonDetMonad" "../Setup_Locale" Platform begin diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy index 9ae443ab4..369f02ab1 100644 --- a/spec/design/m-skel/ARM_HYP/MachineTypes.thy +++ b/spec/design/m-skel/ARM_HYP/MachineTypes.thy @@ -12,7 +12,7 @@ chapter {* ARM\_HYP Machine Types *} theory MachineTypes imports - "../../../lib/Monad_WP/NonDetMonad" + "Lib.NonDetMonad" "../Setup_Locale" Platform begin diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy index 2ea9c49c1..24b38cbbf 100644 --- a/spec/design/m-skel/RISCV64/MachineTypes.thy +++ b/spec/design/m-skel/RISCV64/MachineTypes.thy @@ -12,10 +12,10 @@ chapter "RISCV 64bit Machine Types" theory MachineTypes imports - "../../../lib/Word_Lib/Enumeration" - "../../../lib/$L4V_ARCH/WordSetup" - "../../../lib/Monad_WP/NonDetMonad" - "../../../lib/HaskellLib_H" + "Word_Lib.Enumeration" + "Word_Lib.WordSetup" + "Lib.NonDetMonad" + "Lib.HaskellLib_H" Platform begin diff --git a/spec/design/m-skel/X64/MachineTypes.thy b/spec/design/m-skel/X64/MachineTypes.thy index b89257151..0417c8498 100644 --- a/spec/design/m-skel/X64/MachineTypes.thy +++ b/spec/design/m-skel/X64/MachineTypes.thy @@ -12,10 +12,9 @@ chapter "x86-64bit Machine Types" theory MachineTypes imports - "../../../lib/Word_Lib/Enumeration" - "../../../lib/$L4V_ARCH/WordSetup" - "../../../lib/Monad_WP/NonDetMonad" - "../../../lib/HaskellLib_H" + "Word_Lib.WordSetup" + "Lib.NonDetMonad" + "Lib.HaskellLib_H" Platform begin diff --git a/spec/design/skel/ARM/ArchInvocationLabels_H.thy b/spec/design/skel/ARM/ArchInvocationLabels_H.thy index c77448bad..3e8edd16a 100644 --- a/spec/design/skel/ARM/ArchInvocationLabels_H.thy +++ b/spec/design/skel/ARM/ArchInvocationLabels_H.thy @@ -12,7 +12,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports - "../../../lib/Word_Lib/Enumeration" + "Word_Lib.Enumeration" "../../machine/Setup_Locale" begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/ArchStructures_H.thy b/spec/design/skel/ARM/ArchStructures_H.thy index 6d1a60de7..d33068c39 100644 --- a/spec/design/skel/ARM/ArchStructures_H.thy +++ b/spec/design/skel/ARM/ArchStructures_H.thy @@ -10,7 +10,7 @@ theory ArchStructures_H imports - "../../../lib/Lib" + "Lib.Lib" "../Types_H" Hardware_H begin diff --git a/spec/design/skel/ARM/ArchTypes_H.thy b/spec/design/skel/ARM/ArchTypes_H.thy index afaccad86..774bcf397 100644 --- a/spec/design/skel/ARM/ArchTypes_H.thy +++ b/spec/design/skel/ARM/ArchTypes_H.thy @@ -18,7 +18,7 @@ theory ArchTypes_H imports State_H Hardware_H - "../../../lib/Lib" + "Lib.Lib" begin #INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits diff --git a/spec/design/skel/ARM/Arch_Structs_B.thy b/spec/design/skel/ARM/Arch_Structs_B.thy index a59576a9b..81b1b03d2 100644 --- a/spec/design/skel/ARM/Arch_Structs_B.thy +++ b/spec/design/skel/ARM/Arch_Structs_B.thy @@ -13,7 +13,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports "~~/src/HOL/Main" "../../../spec/machine/Setup_Locale" +imports Main "../../../spec/machine/Setup_Locale" begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/RegisterSet_H.thy b/spec/design/skel/ARM/RegisterSet_H.thy index 4dae930d8..ded3e63c9 100644 --- a/spec/design/skel/ARM/RegisterSet_H.thy +++ b/spec/design/skel/ARM/RegisterSet_H.thy @@ -12,7 +12,7 @@ chapter "Register Set" theory RegisterSet_H imports - "../../../lib/HaskellLib_H" + "Lib.HaskellLib_H" "../../machine/ARM/MachineTypes" begin context Arch begin global_naming ARM_H diff --git a/spec/design/skel/ARM/State_H.thy b/spec/design/skel/ARM/State_H.thy index 7801f9792..de0027adc 100644 --- a/spec/design/skel/ARM/State_H.thy +++ b/spec/design/skel/ARM/State_H.thy @@ -16,7 +16,7 @@ chapter "Machine State" theory State_H imports - "../../../lib/HaskellLib_H" + "Lib.HaskellLib_H" RegisterSet_H "../../machine/ARM/MachineOps" begin diff --git a/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy b/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy index c3fa34205..ed75ed714 100644 --- a/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy +++ b/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy @@ -12,7 +12,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports - "../../../lib/Word_Lib/Enumeration" + "Word_Lib.Enumeration" "../../machine/Setup_Locale" begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/ArchStructures_H.thy b/spec/design/skel/ARM_HYP/ArchStructures_H.thy index 82eaba5cf..305aed48c 100644 --- a/spec/design/skel/ARM_HYP/ArchStructures_H.thy +++ b/spec/design/skel/ARM_HYP/ArchStructures_H.thy @@ -10,7 +10,7 @@ theory ArchStructures_H imports - "../../../lib/Lib" + "Lib.Lib" "../Types_H" Hardware_H begin diff --git a/spec/design/skel/ARM_HYP/ArchTypes_H.thy b/spec/design/skel/ARM_HYP/ArchTypes_H.thy index 12079503d..51ba94a66 100644 --- a/spec/design/skel/ARM_HYP/ArchTypes_H.thy +++ b/spec/design/skel/ARM_HYP/ArchTypes_H.thy @@ -18,7 +18,7 @@ theory ArchTypes_H imports State_H Hardware_H - "../../../lib/Lib" + "Lib.Lib" begin #INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits diff --git a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy index b03aa7420..b58dcc46c 100644 --- a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy +++ b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy @@ -13,7 +13,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports "~~/src/HOL/Main" "../../machine/Setup_Locale" +imports Main "../../machine/Setup_Locale" begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/RegisterSet_H.thy b/spec/design/skel/ARM_HYP/RegisterSet_H.thy index a9be204aa..78024b182 100644 --- a/spec/design/skel/ARM_HYP/RegisterSet_H.thy +++ b/spec/design/skel/ARM_HYP/RegisterSet_H.thy @@ -12,7 +12,7 @@ chapter "Register Set" theory RegisterSet_H imports - "../../../lib/HaskellLib_H" + "Lib.HaskellLib_H" "../../machine/ARM_HYP/MachineTypes" begin context Arch begin global_naming ARM_HYP_H diff --git a/spec/design/skel/ARM_HYP/State_H.thy b/spec/design/skel/ARM_HYP/State_H.thy index 712f48d8d..d36371a36 100644 --- a/spec/design/skel/ARM_HYP/State_H.thy +++ b/spec/design/skel/ARM_HYP/State_H.thy @@ -16,7 +16,7 @@ chapter "Machine State" theory State_H imports - "../../../lib/HaskellLib_H" + "Lib.HaskellLib_H" RegisterSet_H "../../machine/ARM_HYP/MachineOps" begin diff --git a/spec/design/skel/PSpaceFuns_H.thy b/spec/design/skel/PSpaceFuns_H.thy index ef7b1d24a..d3c7f523b 100644 --- a/spec/design/skel/PSpaceFuns_H.thy +++ b/spec/design/skel/PSpaceFuns_H.thy @@ -14,7 +14,7 @@ theory PSpaceFuns_H imports ObjectInstances_H FaultMonad_H - "../../lib/DataMap" + "Lib.DataMap" begin context begin interpretation Arch . diff --git a/spec/design/skel/PSpaceStorable_H.thy b/spec/design/skel/PSpaceStorable_H.thy index 1ae8f08a9..9aab392f8 100644 --- a/spec/design/skel/PSpaceStorable_H.thy +++ b/spec/design/skel/PSpaceStorable_H.thy @@ -12,7 +12,7 @@ theory PSpaceStorable_H imports Structures_H KernelStateData_H - "../../lib/DataMap" + "Lib.DataMap" begin context begin interpretation Arch . diff --git a/spec/design/skel/PSpaceStruct_H.thy b/spec/design/skel/PSpaceStruct_H.thy index c21c05119..0c980937d 100644 --- a/spec/design/skel/PSpaceStruct_H.thy +++ b/spec/design/skel/PSpaceStruct_H.thy @@ -13,7 +13,7 @@ chapter "Physical Memory Structure" theory PSpaceStruct_H imports Structures_H - "../../lib/DataMap" + "Lib.DataMap" begin text {* Helper Functions *} diff --git a/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy b/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy index 52bcff5ad..526577152 100644 --- a/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy +++ b/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy @@ -12,7 +12,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports - "../../../lib/Word_Lib/Enumeration" + "Word_Lib.Enumeration" "../../machine/Setup_Locale" begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/RISCV64/ArchStructures_H.thy b/spec/design/skel/RISCV64/ArchStructures_H.thy index ec32e2088..218a59052 100644 --- a/spec/design/skel/RISCV64/ArchStructures_H.thy +++ b/spec/design/skel/RISCV64/ArchStructures_H.thy @@ -10,7 +10,7 @@ theory ArchStructures_H imports - "../../../lib/Lib" + "Lib.Lib" "../Types_H" Hardware_H begin diff --git a/spec/design/skel/RISCV64/ArchTypes_H.thy b/spec/design/skel/RISCV64/ArchTypes_H.thy index 6cf663945..0df0cc3c6 100644 --- a/spec/design/skel/RISCV64/ArchTypes_H.thy +++ b/spec/design/skel/RISCV64/ArchTypes_H.thy @@ -18,7 +18,7 @@ theory ArchTypes_H imports State_H Hardware_H - "../../../lib/Lib" + "Lib.Lib" begin #INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits diff --git a/spec/design/skel/RISCV64/Arch_Structs_B.thy b/spec/design/skel/RISCV64/Arch_Structs_B.thy index 9566bf47a..8d5866432 100644 --- a/spec/design/skel/RISCV64/Arch_Structs_B.thy +++ b/spec/design/skel/RISCV64/Arch_Structs_B.thy @@ -13,7 +13,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports "~~/src/HOL/Main" "../../../spec/machine/Setup_Locale" +imports "../../../spec/machine/Setup_Locale" begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/RISCV64/RegisterSet_H.thy b/spec/design/skel/RISCV64/RegisterSet_H.thy index 3fcfecfc4..fe070fc62 100644 --- a/spec/design/skel/RISCV64/RegisterSet_H.thy +++ b/spec/design/skel/RISCV64/RegisterSet_H.thy @@ -12,7 +12,7 @@ chapter "Register Set" theory RegisterSet_H imports - "../../../lib/HaskellLib_H" + "Lib.HaskellLib_H" "../../machine/RISCV64/MachineOps" begin context Arch begin global_naming RISCV64_H diff --git a/spec/design/skel/Types_H.thy b/spec/design/skel/Types_H.thy index 2fed89952..ca57624ec 100644 --- a/spec/design/skel/Types_H.thy +++ b/spec/design/skel/Types_H.thy @@ -17,7 +17,7 @@ chapter "Types visible in the API" theory Types_H imports "./$L4V_ARCH/State_H" - "../../lib/Lib" + "Lib.Lib" "./$L4V_ARCH/ArchTypes_H" begin diff --git a/spec/design/skel/X64/ArchInvocationLabels_H.thy b/spec/design/skel/X64/ArchInvocationLabels_H.thy index 8077dbbe4..2a01c2e2f 100644 --- a/spec/design/skel/X64/ArchInvocationLabels_H.thy +++ b/spec/design/skel/X64/ArchInvocationLabels_H.thy @@ -12,7 +12,7 @@ chapter "Architecture-specific Invocation Labels" theory ArchInvocationLabels_H imports - "../../../lib/Word_Lib/Enumeration" + "Word_Lib.Enumeration" "../../machine/Setup_Locale" begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/ArchStructures_H.thy b/spec/design/skel/X64/ArchStructures_H.thy index 031d8da2f..7348160e9 100644 --- a/spec/design/skel/X64/ArchStructures_H.thy +++ b/spec/design/skel/X64/ArchStructures_H.thy @@ -10,7 +10,7 @@ theory ArchStructures_H imports - "../../../lib/Lib" + "Lib.Lib" "../Types_H" Hardware_H begin diff --git a/spec/design/skel/X64/ArchTypes_H.thy b/spec/design/skel/X64/ArchTypes_H.thy index a80507d10..7f14ff46d 100644 --- a/spec/design/skel/X64/ArchTypes_H.thy +++ b/spec/design/skel/X64/ArchTypes_H.thy @@ -18,7 +18,7 @@ theory ArchTypes_H imports State_H Hardware_H - "../../../lib/Lib" + "Lib.Lib" begin #INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits diff --git a/spec/design/skel/X64/Arch_Structs_B.thy b/spec/design/skel/X64/Arch_Structs_B.thy index b1bf96d40..c775ac4ee 100644 --- a/spec/design/skel/X64/Arch_Structs_B.thy +++ b/spec/design/skel/X64/Arch_Structs_B.thy @@ -13,7 +13,7 @@ chapter "Common, Architecture-Specific Data Types" theory Arch_Structs_B -imports "~~/src/HOL/Main" "../../../spec/machine/Setup_Locale" +imports Main "../../../spec/machine/Setup_Locale" begin context Arch begin global_naming X64_H diff --git a/spec/design/skel/X64/RegisterSet_H.thy b/spec/design/skel/X64/RegisterSet_H.thy index 9979c648c..e546cfd5b 100644 --- a/spec/design/skel/X64/RegisterSet_H.thy +++ b/spec/design/skel/X64/RegisterSet_H.thy @@ -12,7 +12,7 @@ chapter "Register Set" theory RegisterSet_H imports - "../../../lib/HaskellLib_H" + "Lib.HaskellLib_H" "../../machine/X64/MachineOps" begin context Arch begin global_naming X64_H diff --git a/spec/machine/ARM/Platform.thy b/spec/machine/ARM/Platform.thy index 465d2bbd2..e33748ae1 100644 --- a/spec/machine/ARM/Platform.thy +++ b/spec/machine/ARM/Platform.thy @@ -12,9 +12,9 @@ chapter "Platform Definitions" theory Platform imports - "../../../lib/Defs" - "../../../lib/Lib" - "../../../lib/ARM/WordSetup" + "Lib.Defs" + "Lib.Lib" + "Word_Lib.WordSetup" "../Setup_Locale" begin diff --git a/spec/machine/ARM_HYP/Platform.thy b/spec/machine/ARM_HYP/Platform.thy index eb07a60a6..9bbd5668d 100644 --- a/spec/machine/ARM_HYP/Platform.thy +++ b/spec/machine/ARM_HYP/Platform.thy @@ -12,9 +12,9 @@ chapter "Platform Definitions" theory Platform imports - "../../../lib/Defs" - "../../../lib/Lib" - "../../../lib/ARM_HYP/WordSetup" + "Lib.Defs" + "Lib.Lib" + "Word_Lib.WordSetup" "../Setup_Locale" begin diff --git a/spec/machine/Setup_Locale.thy b/spec/machine/Setup_Locale.thy index b29bc1a53..e669957b9 100644 --- a/spec/machine/Setup_Locale.thy +++ b/spec/machine/Setup_Locale.thy @@ -10,7 +10,7 @@ theory Setup_Locale -imports "../../lib/Qualify" "../../lib/Requalify" "../../lib/Extend_Locale" +imports "Lib.Qualify" "Lib.Requalify" "Lib.Extend_Locale" begin (* diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy index 631056c65..88f5bc63e 100644 --- a/spec/machine/X64/MachineOps.thy +++ b/spec/machine/X64/MachineOps.thy @@ -12,8 +12,8 @@ chapter "Machine Operations" theory MachineOps imports - "../../../lib/$L4V_ARCH/WordSetup" - "../../../lib/Monad_WP/NonDetMonad" + "Word_Lib.WordSetup" + "Lib.NonDetMonad" "../MachineMonad" begin diff --git a/spec/machine/X64/Platform.thy b/spec/machine/X64/Platform.thy index 57fecae74..b265aaf55 100644 --- a/spec/machine/X64/Platform.thy +++ b/spec/machine/X64/Platform.thy @@ -12,9 +12,9 @@ chapter "Platform Definitions" theory Platform imports - "../../../lib/Lib" - "../../../lib/Word_Lib/Word_Enum" - "../../../lib/Defs" + "Lib.Lib" + "Word_Lib.Word_Enum" + "Lib.Defs" "../Setup_Locale" begin diff --git a/spec/sep-abstract/Ipc_SA.thy b/spec/sep-abstract/Ipc_SA.thy index a6c674d9b..cda935817 100644 --- a/spec/sep-abstract/Ipc_SA.thy +++ b/spec/sep-abstract/Ipc_SA.thy @@ -15,7 +15,7 @@ Specification of Inter-Process Communication. chapter "IPC" theory Ipc_SA -imports "../abstract/Syscall_A" +imports "ASpec.Syscall_A" begin diff --git a/spec/take-grant/System_S.thy b/spec/take-grant/System_S.thy index 4aa212fb7..913cc212a 100644 --- a/spec/take-grant/System_S.thy +++ b/spec/take-grant/System_S.thy @@ -20,7 +20,7 @@ *) theory System_S -imports "../../lib/$L4V_ARCH/WordSetup" +imports "Word_Lib.WordSetup" begin (* System entities: Definition of entities that constitute the system diff --git a/sys-init/CreateIRQCaps_SI.thy b/sys-init/CreateIRQCaps_SI.thy index 1e5f54725..ec3584afa 100644 --- a/sys-init/CreateIRQCaps_SI.thy +++ b/sys-init/CreateIRQCaps_SI.thy @@ -10,7 +10,7 @@ theory CreateIRQCaps_SI imports - "../proof/capDL-api/IRQ_DP" + "DSpecProofs.IRQ_DP" ObjectInitialised_SI RootTask_SI SysInit_SI diff --git a/sys-init/CreateObjects_SI.thy b/sys-init/CreateObjects_SI.thy index e8de7c2b2..c6aaa6287 100644 --- a/sys-init/CreateObjects_SI.thy +++ b/sys-init/CreateObjects_SI.thy @@ -10,7 +10,7 @@ theory CreateObjects_SI imports - "../proof/capDL-api/Retype_DP" + "DSpecProofs.Retype_DP" ObjectInitialised_SI RootTask_SI SysInit_SI diff --git a/sys-init/DuplicateCaps_SI.thy b/sys-init/DuplicateCaps_SI.thy index 32023acca..866dcf81c 100644 --- a/sys-init/DuplicateCaps_SI.thy +++ b/sys-init/DuplicateCaps_SI.thy @@ -10,7 +10,7 @@ theory DuplicateCaps_SI imports - "../proof/capDL-api/CNode_DP" + "DSpecProofs.CNode_DP" ObjectInitialised_SI RootTask_SI SysInit_SI diff --git a/sys-init/InitCSpace_SI.thy b/sys-init/InitCSpace_SI.thy index cd10069eb..f9e74909b 100644 --- a/sys-init/InitCSpace_SI.thy +++ b/sys-init/InitCSpace_SI.thy @@ -10,7 +10,7 @@ theory InitCSpace_SI imports - "../proof/capDL-api/CNode_DP" + "DSpecProofs.CNode_DP" ObjectInitialised_SI RootTask_SI SysInit_SI diff --git a/sys-init/InitIRQ_SI.thy b/sys-init/InitIRQ_SI.thy index 8c8884456..186c55f55 100644 --- a/sys-init/InitIRQ_SI.thy +++ b/sys-init/InitIRQ_SI.thy @@ -10,7 +10,7 @@ theory InitIRQ_SI imports - "../proof/capDL-api/IRQ_DP" + "DSpecProofs.IRQ_DP" ObjectInitialised_SI RootTask_SI SysInit_SI diff --git a/sys-init/InitTCB_SI.thy b/sys-init/InitTCB_SI.thy index d392b9fbd..f02761961 100644 --- a/sys-init/InitTCB_SI.thy +++ b/sys-init/InitTCB_SI.thy @@ -10,8 +10,8 @@ theory InitTCB_SI imports - "../proof/capDL-api/KHeap_DP" - "../proof/capDL-api/TCB_DP" + "DSpecProofs.KHeap_DP" + "DSpecProofs.TCB_DP" ObjectInitialised_SI RootTask_SI SysInit_SI diff --git a/sys-init/InitVSpace_SI.thy b/sys-init/InitVSpace_SI.thy index 2b372fd56..f2a78f4ee 100644 --- a/sys-init/InitVSpace_SI.thy +++ b/sys-init/InitVSpace_SI.thy @@ -11,8 +11,8 @@ theory InitVSpace_SI imports - "../proof/capDL-api/Invocation_DP" - "../proof/capDL-api/Arch_DP" + "DSpecProofs.Invocation_DP" + "DSpecProofs.Arch_DP" ObjectInitialised_SI RootTask_SI SysInit_SI diff --git a/sys-init/ROOT b/sys-init/ROOT index fad447ace..dbd1ba643 100644 --- a/sys-init/ROOT +++ b/sys-init/ROOT @@ -15,6 +15,10 @@ chapter "System-Initialisation" *) session SysInit = DSpecProofs + + sessions + Lib + SepDSpec + DSpecProofs theories "Proof_SI" diff --git a/sys-init/SysInit_SI.thy b/sys-init/SysInit_SI.thy index cb8f5be00..712204060 100644 --- a/sys-init/SysInit_SI.thy +++ b/sys-init/SysInit_SI.thy @@ -10,8 +10,8 @@ theory SysInit_SI imports - "../proof/capDL-api/Kernel_DP" - "../lib/NonDetMonadLemmaBucket" + "DSpecProofs.Kernel_DP" + "Lib.NonDetMonadLemmaBucket" begin definition diff --git a/sys-init/WellFormed_SI.thy b/sys-init/WellFormed_SI.thy index 53ec97811..0da8fd2f5 100644 --- a/sys-init/WellFormed_SI.thy +++ b/sys-init/WellFormed_SI.thy @@ -21,9 +21,9 @@ theory WellFormed_SI imports - "../proof/capDL-api/Kernel_DP" - "../proof/sep-capDL/Separation_SD" - "../lib/SimpStrategy" + "DSpecProofs.Kernel_DP" + "SepDSpec.Separation_SD" + "Lib.SimpStrategy" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/tools/asmrefine/CommonOps.thy b/tools/asmrefine/CommonOps.thy index 65676b5ba..9eb119792 100644 --- a/tools/asmrefine/CommonOps.thy +++ b/tools/asmrefine/CommonOps.thy @@ -10,7 +10,7 @@ theory CommonOps -imports "../../lib/CTranslationNICTA" +imports "CLib.CTranslationNICTA" "GlobalsSwap" begin diff --git a/tools/asmrefine/CommonOpsLemmas.thy b/tools/asmrefine/CommonOpsLemmas.thy index e1012d5e1..0d8d28460 100644 --- a/tools/asmrefine/CommonOpsLemmas.thy +++ b/tools/asmrefine/CommonOpsLemmas.thy @@ -12,7 +12,7 @@ theory CommonOpsLemmas imports "CommonOps" - "../../lib/$L4V_ARCH/WordSetup" + "Word_Lib.WordSetup" begin lemma fold_all_htd_updates': diff --git a/tools/asmrefine/ExtraSpecs.thy b/tools/asmrefine/ExtraSpecs.thy index 2981a4741..b9034d7c0 100644 --- a/tools/asmrefine/ExtraSpecs.thy +++ b/tools/asmrefine/ExtraSpecs.thy @@ -11,7 +11,7 @@ theory ExtraSpecs imports - "../../lib/TypHeapLib" + "CLib.TypHeapLib" begin diff --git a/tools/asmrefine/FieldAccessors.thy b/tools/asmrefine/FieldAccessors.thy index afaef2318..e08b61659 100644 --- a/tools/asmrefine/FieldAccessors.thy +++ b/tools/asmrefine/FieldAccessors.thy @@ -10,7 +10,7 @@ theory FieldAccessors -imports "../../lib/LemmaBucket_C" +imports "CLib.LemmaBucket_C" begin diff --git a/tools/asmrefine/GhostAssertions.thy b/tools/asmrefine/GhostAssertions.thy index 1ffa2fb3e..09aba1bce 100644 --- a/tools/asmrefine/GhostAssertions.thy +++ b/tools/asmrefine/GhostAssertions.thy @@ -10,7 +10,7 @@ theory GhostAssertions -imports "../c-parser/CTranslation" +imports "CParser.CTranslation" begin diff --git a/tools/asmrefine/GlobalsSwap.thy b/tools/asmrefine/GlobalsSwap.thy index 97d8097d0..8166b7e6c 100644 --- a/tools/asmrefine/GlobalsSwap.thy +++ b/tools/asmrefine/GlobalsSwap.thy @@ -10,9 +10,9 @@ theory GlobalsSwap imports - "../../lib/Lib" - "../c-parser/CTranslation" - "../c-parser/PackedTypes" + "Lib.Lib" + "CParser.CTranslation" + "CParser.PackedTypes" begin datatype 'g global_data = diff --git a/tools/asmrefine/GraphLang.thy b/tools/asmrefine/GraphLang.thy index 8731fac42..16987a397 100644 --- a/tools/asmrefine/GraphLang.thy +++ b/tools/asmrefine/GraphLang.thy @@ -11,8 +11,8 @@ theory GraphLang imports - "../../lib/TypHeapLib" - "../../lib/SplitRule" + "CLib.TypHeapLib" + "Lib.SplitRule" "CommonOps" begin diff --git a/tools/asmrefine/GraphProof.thy b/tools/asmrefine/GraphProof.thy index 187fe1126..32c1ee12f 100644 --- a/tools/asmrefine/GraphProof.thy +++ b/tools/asmrefine/GraphProof.thy @@ -10,7 +10,7 @@ theory GraphProof -imports TailrecPre GraphLangLemmas "../../lib/SplitRule" +imports TailrecPre GraphLangLemmas "Lib.SplitRule" begin diff --git a/tools/asmrefine/GraphRefine.thy b/tools/asmrefine/GraphRefine.thy index df7ff9a51..4220c475c 100644 --- a/tools/asmrefine/GraphRefine.thy +++ b/tools/asmrefine/GraphRefine.thy @@ -13,7 +13,7 @@ theory GraphRefine imports TailrecPre GraphLangLemmas - "../../lib/LemmaBucket_C" + "CLib.LemmaBucket_C" ExtraSpecs begin diff --git a/tools/asmrefine/TailrecPre.thy b/tools/asmrefine/TailrecPre.thy index 9c25f116f..ed75ebc5d 100644 --- a/tools/asmrefine/TailrecPre.thy +++ b/tools/asmrefine/TailrecPre.thy @@ -10,8 +10,8 @@ theory TailrecPre imports - "../../lib/$L4V_ARCH/WordSetup" - "../../lib/Lib" + "Word_Lib.WordSetup" + "Lib.Lib" begin definition diff --git a/tools/autocorres/AbstractArrays.thy b/tools/autocorres/AbstractArrays.thy index c024d1d2d..9b8d1ad3d 100644 --- a/tools/autocorres/AbstractArrays.thy +++ b/tools/autocorres/AbstractArrays.thy @@ -10,8 +10,8 @@ theory AbstractArrays imports - "../../lib/TypHeapLib" - "../../lib/$L4V_ARCH/WordSetup" + "CLib.TypHeapLib" + "Word_Lib.WordSetup" begin (* diff --git a/tools/autocorres/AutoCorres.thy b/tools/autocorres/AutoCorres.thy index 645b8e4cc..4244fa9ea 100644 --- a/tools/autocorres/AutoCorres.thy +++ b/tools/autocorres/AutoCorres.thy @@ -25,10 +25,10 @@ imports TypHeapSimple HeapLift WordAbstract - "../../lib/Monad_WP/OptionMonadWP" - "../../lib/Apply_Trace" + "Lib.OptionMonadWP" + "Lib.Apply_Trace" AutoCorresSimpset - "../../lib/ml-helpers/TermPatternAntiquote" + "Lib.TermPatternAntiquote" keywords "autocorres" :: thy_decl begin diff --git a/tools/autocorres/Auto_Separation_Algebra.thy b/tools/autocorres/Auto_Separation_Algebra.thy index 446ea591f..1dc9a7490 100644 --- a/tools/autocorres/Auto_Separation_Algebra.thy +++ b/tools/autocorres/Auto_Separation_Algebra.thy @@ -12,7 +12,7 @@ FIXME: this is not quite finished. There are some proof tactics missing (see getter_rewrite etc) *) theory Auto_Separation_Algebra -imports "AutoCorres" "../../lib/sep_algebra/Separation_Algebra" +imports "AutoCorres" "Sep_Algebra.Separation_Algebra" keywords "sep_instance" :: thy_goal begin diff --git a/tools/autocorres/DataStructures.thy b/tools/autocorres/DataStructures.thy index 2a4899e07..b138a269f 100644 --- a/tools/autocorres/DataStructures.thy +++ b/tools/autocorres/DataStructures.thy @@ -9,7 +9,7 @@ *) theory DataStructures -imports "~~/src/HOL/Main" +imports Main begin (* diff --git a/tools/autocorres/HeapLift.thy b/tools/autocorres/HeapLift.thy index 093db051e..ca53d5edc 100644 --- a/tools/autocorres/HeapLift.thy +++ b/tools/autocorres/HeapLift.thy @@ -15,7 +15,7 @@ imports L2Defs ExecConcrete AbstractArrays - "../../lib/LemmaBucket_C" + "CLib.LemmaBucket_C" begin definition "L2Tcorres st A C = corresXF st (\r _. r) (\r _. r) \ A C" diff --git a/tools/autocorres/MonadMono.thy b/tools/autocorres/MonadMono.thy index d18bd03f3..1c4baac4d 100644 --- a/tools/autocorres/MonadMono.thy +++ b/tools/autocorres/MonadMono.thy @@ -16,7 +16,7 @@ theory MonadMono imports NonDetMonadEx - "../../lib/Monad_WP/OptionMonadWP" + "Lib.OptionMonadWP" begin (* diff --git a/tools/autocorres/NonDetMonadEx.thy b/tools/autocorres/NonDetMonadEx.thy index 434b721d4..3a50a9c47 100644 --- a/tools/autocorres/NonDetMonadEx.thy +++ b/tools/autocorres/NonDetMonadEx.thy @@ -14,9 +14,9 @@ theory NonDetMonadEx imports - "../../lib/$L4V_ARCH/WordSetup" - "../../lib/NonDetMonadLemmaBucket" - "../../lib/Monad_WP/OptionMonadND" + "Word_Lib.WordSetup" + "Lib.NonDetMonadLemmaBucket" + "Lib.OptionMonadND" begin (* diff --git a/tools/autocorres/ROOT b/tools/autocorres/ROOT index 00f683532..32b30d1bd 100644 --- a/tools/autocorres/ROOT +++ b/tools/autocorres/ROOT @@ -13,10 +13,19 @@ *) session AutoCorres = CParser + + sessions + "HOL-Eisbach" + Lib + CLib theories "AutoCorres" session AutoCorresSEL4 = CBaseRefine + + sessions + "HOL-Library" + "HOL-Computational_Algebra" + Lib + CLib + CParser theories "TestSEL4" - diff --git a/tools/autocorres/SimplBucket.thy b/tools/autocorres/SimplBucket.thy index 2248b7189..884b65724 100644 --- a/tools/autocorres/SimplBucket.thy +++ b/tools/autocorres/SimplBucket.thy @@ -13,7 +13,7 @@ *) theory SimplBucket -imports "../c-parser/CTranslation" +imports "CParser.CTranslation" begin lemma Normal_resultE: diff --git a/tools/autocorres/TestSEL4.thy b/tools/autocorres/TestSEL4.thy index a5ad422d6..1bac56c69 100644 --- a/tools/autocorres/TestSEL4.thy +++ b/tools/autocorres/TestSEL4.thy @@ -11,7 +11,7 @@ theory TestSEL4 imports AutoCorres - "../../spec/cspec/KernelInc_C" + "CSpec.KernelInc_C" begin (* diff --git a/tools/autocorres/TypHeapSimple.thy b/tools/autocorres/TypHeapSimple.thy index 1222f13f2..fa3a1492f 100644 --- a/tools/autocorres/TypHeapSimple.thy +++ b/tools/autocorres/TypHeapSimple.thy @@ -19,7 +19,7 @@ theory TypHeapSimple imports - "../../lib/TypHeapLib" + "CLib.TypHeapLib" begin (* diff --git a/tools/autocorres/TypeStrengthen.thy b/tools/autocorres/TypeStrengthen.thy index 0984030d7..7a7249ee4 100644 --- a/tools/autocorres/TypeStrengthen.thy +++ b/tools/autocorres/TypeStrengthen.thy @@ -18,7 +18,7 @@ theory TypeStrengthen imports L2Defs - "../../lib/Monad_WP/OptionMonadND" + "Lib.OptionMonadND" ExecConcrete begin diff --git a/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy b/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy index 9ecc05db6..79800448e 100644 --- a/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy +++ b/tools/autocorres/doc/quickstart/Chapter1_MinMax.thy @@ -10,7 +10,7 @@ (*<*) theory Chapter1_MinMax -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin (*>*) diff --git a/tools/autocorres/doc/quickstart/Chapter2_HoareHeap.thy b/tools/autocorres/doc/quickstart/Chapter2_HoareHeap.thy index fbfc3d2cd..8a1d53862 100644 --- a/tools/autocorres/doc/quickstart/Chapter2_HoareHeap.thy +++ b/tools/autocorres/doc/quickstart/Chapter2_HoareHeap.thy @@ -10,7 +10,7 @@ (*<*) theory Chapter2_HoareHeap -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin (*>*) diff --git a/tools/autocorres/doc/quickstart/Chapter3_HoareHeap.thy b/tools/autocorres/doc/quickstart/Chapter3_HoareHeap.thy index ba3888f07..60e5c5a0f 100644 --- a/tools/autocorres/doc/quickstart/Chapter3_HoareHeap.thy +++ b/tools/autocorres/doc/quickstart/Chapter3_HoareHeap.thy @@ -10,7 +10,7 @@ (*<*) theory Chapter3_HoareHeap -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin (*>*) diff --git a/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy b/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy index 86563c1f1..1e72f5aa5 100644 --- a/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy +++ b/tools/autocorres/experiments/alloc-proof/Alloc_Lite.thy @@ -10,7 +10,7 @@ theory Alloc_Lite imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin (* Parse the input file. *) diff --git a/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy b/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy index dabc9023f..d176036f8 100644 --- a/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy +++ b/tools/autocorres/experiments/alloc-proof/Alloc_Simp.thy @@ -11,10 +11,10 @@ theory Alloc_Simp imports - "../../AutoCorres" - "../../../../lib/sep_algebra/Separation_Algebra" - "../../../../lib/sep_algebra/Sep_Algebra_L4v" - "../../../../lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics" + "AutoCorres.AutoCorres" + "Sep_Algebra.Separation_Algebra" + "Sep_Algebra.Sep_Algebra_L4v" + "Hoare_Sep_Tactics.Hoare_Sep_Tactics" begin (* Parse the input file. *) diff --git a/tools/autocorres/tests/examples/AC_Rename.thy b/tools/autocorres/tests/examples/AC_Rename.thy index 8aee61e8a..bb0133dfa 100644 --- a/tools/autocorres/tests/examples/AC_Rename.thy +++ b/tools/autocorres/tests/examples/AC_Rename.thy @@ -13,7 +13,7 @@ * functions and globals. *) theory AC_Rename imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin declare [[allow_underscore_idents]] diff --git a/tools/autocorres/tests/examples/Alloc.thy b/tools/autocorres/tests/examples/Alloc.thy index 4f8fa16cc..8008c72e8 100644 --- a/tools/autocorres/tests/examples/Alloc.thy +++ b/tools/autocorres/tests/examples/Alloc.thy @@ -10,7 +10,7 @@ theory Alloc imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin (* Parse the input file. *) diff --git a/tools/autocorres/tests/examples/BinarySearch.thy b/tools/autocorres/tests/examples/BinarySearch.thy index 675b4711a..c43a16d19 100644 --- a/tools/autocorres/tests/examples/BinarySearch.thy +++ b/tools/autocorres/tests/examples/BinarySearch.thy @@ -9,7 +9,7 @@ *) theory BinarySearch -imports "../../AutoCorres" "../../DataStructures" +imports "AutoCorres.AutoCorres" "../../DataStructures" begin install_C_file "binary_search.c" diff --git a/tools/autocorres/tests/examples/CList.thy b/tools/autocorres/tests/examples/CList.thy index e2e8fcc68..7ae442f79 100644 --- a/tools/autocorres/tests/examples/CList.thy +++ b/tools/autocorres/tests/examples/CList.thy @@ -36,7 +36,7 @@ *) theory CList imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin install_C_file "list.c" diff --git a/tools/autocorres/tests/examples/ConditionGuard.thy b/tools/autocorres/tests/examples/ConditionGuard.thy index f4babc612..a298dd225 100644 --- a/tools/autocorres/tests/examples/ConditionGuard.thy +++ b/tools/autocorres/tests/examples/ConditionGuard.thy @@ -9,7 +9,9 @@ *) (* See comment in condition_guard.c *) -theory ConditionGuard imports "../../AutoCorres" begin +theory ConditionGuard +imports "AutoCorres.AutoCorres" +begin install_C_file "condition_guard.c" autocorres "condition_guard.c" diff --git a/tools/autocorres/tests/examples/Factorial.thy b/tools/autocorres/tests/examples/Factorial.thy index 7f2fc0616..591fcd3ce 100644 --- a/tools/autocorres/tests/examples/Factorial.thy +++ b/tools/autocorres/tests/examples/Factorial.thy @@ -13,8 +13,8 @@ Termination for recursive functions. *) theory Factorial imports - "../../AutoCorres" - "../../../../lib/Monad_WP/OptionMonadWP" + "AutoCorres.AutoCorres" + "Lib.OptionMonadWP" begin (* Parse the input file. *) diff --git a/tools/autocorres/tests/examples/FibProof.thy b/tools/autocorres/tests/examples/FibProof.thy index 39fa2df55..6dc1c6f6c 100644 --- a/tools/autocorres/tests/examples/FibProof.thy +++ b/tools/autocorres/tests/examples/FibProof.thy @@ -20,7 +20,7 @@ To do: theory FibProof imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin (* diff --git a/tools/autocorres/tests/examples/FunctionInfoDemo.thy b/tools/autocorres/tests/examples/FunctionInfoDemo.thy index c80d04148..18dda8f13 100644 --- a/tools/autocorres/tests/examples/FunctionInfoDemo.thy +++ b/tools/autocorres/tests/examples/FunctionInfoDemo.thy @@ -16,7 +16,7 @@ text \ See also: TraceDemo \ theory FunctionInfoDemo imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin text \Process a source file to populate our data structures.\ diff --git a/tools/autocorres/tests/examples/HeapWrap.thy b/tools/autocorres/tests/examples/HeapWrap.thy index 92bfadf52..0c370afb1 100644 --- a/tools/autocorres/tests/examples/HeapWrap.thy +++ b/tools/autocorres/tests/examples/HeapWrap.thy @@ -13,7 +13,7 @@ * JIRA issue ID: VER-356 *) theory HeapWrap -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "heap_wrap.c" diff --git a/tools/autocorres/tests/examples/Incremental.thy b/tools/autocorres/tests/examples/Incremental.thy index 60a3d7f48..56da9b0c4 100644 --- a/tools/autocorres/tests/examples/Incremental.thy +++ b/tools/autocorres/tests/examples/Incremental.thy @@ -14,7 +14,7 @@ * to select different functions for each run. *) theory Incremental imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin install_C_file "type_strengthen.c" diff --git a/tools/autocorres/tests/examples/IsPrime.thy b/tools/autocorres/tests/examples/IsPrime.thy index 115a2fd94..6a7ac49ed 100644 --- a/tools/autocorres/tests/examples/IsPrime.thy +++ b/tools/autocorres/tests/examples/IsPrime.thy @@ -10,8 +10,8 @@ theory IsPrime imports - "../../AutoCorres" - "~~/src/HOL/Computational_Algebra/Primes" + "AutoCorres.AutoCorres" + "HOL-Computational_Algebra.Primes" begin (* Parse the input file. *) diff --git a/tools/autocorres/tests/examples/Kmalloc.thy b/tools/autocorres/tests/examples/Kmalloc.thy index 53f81bfa8..cee1ebe3e 100644 --- a/tools/autocorres/tests/examples/Kmalloc.thy +++ b/tools/autocorres/tests/examples/Kmalloc.thy @@ -9,7 +9,7 @@ *) theory Kmalloc -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin (* No proof here, just testing the parser. *) diff --git a/tools/autocorres/tests/examples/ListRev.thy b/tools/autocorres/tests/examples/ListRev.thy index 0c76a8ba6..acdc6c321 100644 --- a/tools/autocorres/tests/examples/ListRev.thy +++ b/tools/autocorres/tests/examples/ListRev.thy @@ -9,7 +9,7 @@ *) theory ListRev -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "list_rev.c" diff --git a/tools/autocorres/tests/examples/Memcpy.thy b/tools/autocorres/tests/examples/Memcpy.thy index 09c10378d..9cac2934b 100644 --- a/tools/autocorres/tests/examples/Memcpy.thy +++ b/tools/autocorres/tests/examples/Memcpy.thy @@ -10,8 +10,8 @@ theory Memcpy imports - "../../../c-parser/CTranslation" - "../../AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin abbreviation "ADDR_MAX \ UWORD_MAX TYPE(addr_bitsize)" diff --git a/tools/autocorres/tests/examples/Memset.thy b/tools/autocorres/tests/examples/Memset.thy index 1983ce7da..fb1fa57b9 100644 --- a/tools/autocorres/tests/examples/Memset.thy +++ b/tools/autocorres/tests/examples/Memset.thy @@ -9,7 +9,7 @@ *) theory Memset -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "memset.c" diff --git a/tools/autocorres/tests/examples/MultByAdd.thy b/tools/autocorres/tests/examples/MultByAdd.thy index 26bd7c559..0b68c14cc 100644 --- a/tools/autocorres/tests/examples/MultByAdd.thy +++ b/tools/autocorres/tests/examples/MultByAdd.thy @@ -10,7 +10,7 @@ theory MultByAdd imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin (* Parse the input file. *) diff --git a/tools/autocorres/tests/examples/Plus.thy b/tools/autocorres/tests/examples/Plus.thy index 30a8ee3ad..2733d17e4 100644 --- a/tools/autocorres/tests/examples/Plus.thy +++ b/tools/autocorres/tests/examples/Plus.thy @@ -10,7 +10,7 @@ theory Plus imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin install_C_file "plus.c" diff --git a/tools/autocorres/tests/examples/Quicksort.thy b/tools/autocorres/tests/examples/Quicksort.thy index 1004d0a2c..e2abe141a 100644 --- a/tools/autocorres/tests/examples/Quicksort.thy +++ b/tools/autocorres/tests/examples/Quicksort.thy @@ -13,8 +13,8 @@ *) theory Quicksort imports - "../../AutoCorres" - "~~/src/HOL/Library/Multiset" + "AutoCorres.AutoCorres" + "HOL-Library.Multiset" begin declare validNF_whileLoop_inv_measure_twosteps [wp] diff --git a/tools/autocorres/tests/examples/SchorrWaite.thy b/tools/autocorres/tests/examples/SchorrWaite.thy index 3b6b6d9ac..ab1cda28b 100644 --- a/tools/autocorres/tests/examples/SchorrWaite.thy +++ b/tools/autocorres/tests/examples/SchorrWaite.thy @@ -47,8 +47,8 @@ * the proof to show fault-avoidence and termination. *) theory SchorrWaite imports - "~~/src/HOL/Library/Product_Lexorder" - "../../AutoCorres" + "HOL-Library.Product_Lexorder" + "AutoCorres.AutoCorres" begin declare fun_upd_apply[simp del] diff --git a/tools/autocorres/tests/examples/Simple.thy b/tools/autocorres/tests/examples/Simple.thy index 525012471..feb3bbad5 100644 --- a/tools/autocorres/tests/examples/Simple.thy +++ b/tools/autocorres/tests/examples/Simple.thy @@ -10,7 +10,7 @@ theory Simple imports - "../../AutoCorres" + "AutoCorres.AutoCorres" GCD begin diff --git a/tools/autocorres/tests/examples/Str2Long.thy b/tools/autocorres/tests/examples/Str2Long.thy index 7a5aa7bfc..3e2194250 100644 --- a/tools/autocorres/tests/examples/Str2Long.thy +++ b/tools/autocorres/tests/examples/Str2Long.thy @@ -10,8 +10,8 @@ theory Str2Long imports - "../../../c-parser/CTranslation" - "../../AutoCorres" + "CParser.CTranslation" + "AutoCorres.AutoCorres" begin install_C_file "str2long.c" diff --git a/tools/autocorres/tests/examples/Suzuki.thy b/tools/autocorres/tests/examples/Suzuki.thy index 3b5bd3a00..2552bbdac 100644 --- a/tools/autocorres/tests/examples/Suzuki.thy +++ b/tools/autocorres/tests/examples/Suzuki.thy @@ -15,7 +15,7 @@ theory Suzuki imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin install_C_file "suzuki.c" diff --git a/tools/autocorres/tests/examples/Swap.thy b/tools/autocorres/tests/examples/Swap.thy index ab9ba01c2..24d74f871 100644 --- a/tools/autocorres/tests/examples/Swap.thy +++ b/tools/autocorres/tests/examples/Swap.thy @@ -10,8 +10,7 @@ theory Swap imports - "../../AutoCorres" - "../../TypHeapSimple" + "AutoCorres.AutoCorres" begin (* Parse the input file. *) diff --git a/tools/autocorres/tests/examples/TraceDemo.thy b/tools/autocorres/tests/examples/TraceDemo.thy index 3fcfdb17b..009483ce3 100644 --- a/tools/autocorres/tests/examples/TraceDemo.thy +++ b/tools/autocorres/tests/examples/TraceDemo.thy @@ -15,7 +15,7 @@ * translation phases. *) -theory TraceDemo imports "../../AutoCorres" begin +theory TraceDemo imports "AutoCorres.AutoCorres" begin install_C_file "trace_demo.c" diff --git a/tools/autocorres/tests/examples/WordAbs.thy b/tools/autocorres/tests/examples/WordAbs.thy index 2987744a1..5c04ae942 100644 --- a/tools/autocorres/tests/examples/WordAbs.thy +++ b/tools/autocorres/tests/examples/WordAbs.thy @@ -9,7 +9,7 @@ *) theory WordAbs -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "word_abs.c" diff --git a/tools/autocorres/tests/examples/type_strengthen_tricks.thy b/tools/autocorres/tests/examples/type_strengthen_tricks.thy index 791ae781f..25b805fb5 100644 --- a/tools/autocorres/tests/examples/type_strengthen_tricks.thy +++ b/tools/autocorres/tests/examples/type_strengthen_tricks.thy @@ -13,7 +13,7 @@ * Based on type_strengthen.thy. *) theory type_strengthen_tricks imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin install_C_file "type_strengthen.c" diff --git a/tools/autocorres/tests/failing/dirty_frees.thy b/tools/autocorres/tests/failing/dirty_frees.thy index 7e1d5b164..3add58316 100644 --- a/tools/autocorres/tests/failing/dirty_frees.thy +++ b/tools/autocorres/tests/failing/dirty_frees.thy @@ -11,7 +11,7 @@ (* * Tests for handling of names and free variables. *) -theory dirty_frees imports "../../AutoCorres" begin +theory dirty_frees imports "AutoCorres.AutoCorres" begin install_C_file "dirty_frees.c" diff --git a/tools/autocorres/tests/failing/jira_ver_591.thy b/tools/autocorres/tests/failing/jira_ver_591.thy index 5da3a242a..8c9470054 100644 --- a/tools/autocorres/tests/failing/jira_ver_591.thy +++ b/tools/autocorres/tests/failing/jira_ver_591.thy @@ -11,7 +11,7 @@ (* * Test for Jira issue VER-591. See the C file for more details. *) -theory jira_ver_591 imports "../../AutoCorres" begin +theory jira_ver_591 imports "AutoCorres.AutoCorres" begin install_C_file "jira_ver_591.c" diff --git a/tools/autocorres/tests/proof-tests/CustomWordAbs.thy b/tools/autocorres/tests/proof-tests/CustomWordAbs.thy index ed9b05fbb..912868a56 100644 --- a/tools/autocorres/tests/proof-tests/CustomWordAbs.thy +++ b/tools/autocorres/tests/proof-tests/CustomWordAbs.thy @@ -9,7 +9,7 @@ *) theory CustomWordAbs -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "custom_word_abs.c" diff --git a/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy b/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy index 791b88a7c..f1425b818 100644 --- a/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy +++ b/tools/autocorres/tests/proof-tests/Test_Spec_Translation.thy @@ -12,7 +12,7 @@ * Tests for handling Spec constructs emitted by the C parser. *) theory Test_Spec_Translation -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "test_spec_translation.c" diff --git a/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy b/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy index 83af0bc2d..b24e3aa70 100644 --- a/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy +++ b/tools/autocorres/tests/proof-tests/WhileLoopVarsPreserved.thy @@ -9,7 +9,7 @@ *) theory WhileLoopVarsPreserved imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin install_C_file "while_loop_vars_preserved.c" diff --git a/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy b/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy index 422243420..3e5d594c0 100644 --- a/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy +++ b/tools/autocorres/tests/proof-tests/WordAbsFnCall.thy @@ -9,7 +9,7 @@ *) theory WordAbsFnCall imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin install_C_file "word_abs_fn_call.c" diff --git a/tools/autocorres/tests/proof-tests/array_indirect_update.thy b/tools/autocorres/tests/proof-tests/array_indirect_update.thy index ff65af88b..6801072d2 100644 --- a/tools/autocorres/tests/proof-tests/array_indirect_update.thy +++ b/tools/autocorres/tests/proof-tests/array_indirect_update.thy @@ -13,7 +13,7 @@ * Here we prove that writing a pointer that points into an array * will update the array. *) -theory array_indirect_update imports "../../AutoCorres" begin +theory array_indirect_update imports "AutoCorres.AutoCorres" begin install_C_file "array_indirect_update.c" autocorres "array_indirect_update.c" diff --git a/tools/autocorres/tests/proof-tests/badnames.thy b/tools/autocorres/tests/proof-tests/badnames.thy index 9fe9c3d58..b0e8dbf6a 100644 --- a/tools/autocorres/tests/proof-tests/badnames.thy +++ b/tools/autocorres/tests/proof-tests/badnames.thy @@ -11,7 +11,7 @@ (* * Test handling of C idents that are unusual or at risk of conflicting with other names. *) -theory badnames imports "../../AutoCorres" begin +theory badnames imports "AutoCorres.AutoCorres" begin declare [[allow_underscore_idents]] install_C_file "badnames.c" diff --git a/tools/autocorres/tests/proof-tests/global_array_update.thy b/tools/autocorres/tests/proof-tests/global_array_update.thy index e26a13495..9e7c2f33b 100644 --- a/tools/autocorres/tests/proof-tests/global_array_update.thy +++ b/tools/autocorres/tests/proof-tests/global_array_update.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory global_array_update imports "../../AutoCorres" begin +theory global_array_update imports "AutoCorres.AutoCorres" begin install_C_file "global_array_update.c" autocorres "global_array_update.c" diff --git a/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy b/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy index 9706df8ae..6612c00ce 100644 --- a/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy +++ b/tools/autocorres/tests/proof-tests/heap_lift_force_prevent.thy @@ -13,7 +13,7 @@ *) theory heap_lift_force_prevent -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "heap_lift_force_prevent.c" diff --git a/tools/autocorres/tests/proof-tests/nested_struct.thy b/tools/autocorres/tests/proof-tests/nested_struct.thy index 0a6f514c8..567d982a2 100644 --- a/tools/autocorres/tests/proof-tests/nested_struct.thy +++ b/tools/autocorres/tests/proof-tests/nested_struct.thy @@ -12,7 +12,7 @@ * Accessing nested structs. * Testcase for bug VER-321. *) -theory nested_struct imports "../../AutoCorres" begin +theory nested_struct imports "AutoCorres.AutoCorres" begin install_C_file "nested_struct.c" (* Nested struct translation currently only works for packed_type types. *) diff --git a/tools/autocorres/tests/proof-tests/prototyped_functions.thy b/tools/autocorres/tests/proof-tests/prototyped_functions.thy index 346a802bc..ce08668f0 100644 --- a/tools/autocorres/tests/proof-tests/prototyped_functions.thy +++ b/tools/autocorres/tests/proof-tests/prototyped_functions.thy @@ -9,7 +9,7 @@ *) theory prototyped_functions -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "prototyped_functions.c" diff --git a/tools/autocorres/tests/proof-tests/skip_heap_abs.thy b/tools/autocorres/tests/proof-tests/skip_heap_abs.thy index 85c0e3e64..66ae4d978 100644 --- a/tools/autocorres/tests/proof-tests/skip_heap_abs.thy +++ b/tools/autocorres/tests/proof-tests/skip_heap_abs.thy @@ -11,7 +11,7 @@ (* * Simple test for skip_heap_abs. *) -theory skip_heap_abs imports "../../AutoCorres" begin +theory skip_heap_abs imports "AutoCorres.AutoCorres" begin install_C_file "skip_heap_abs.c" autocorres [skip_heap_abs] "skip_heap_abs.c" diff --git a/tools/autocorres/tests/proof-tests/struct.thy b/tools/autocorres/tests/proof-tests/struct.thy index 66095744d..8c58ccae8 100644 --- a/tools/autocorres/tests/proof-tests/struct.thy +++ b/tools/autocorres/tests/proof-tests/struct.thy @@ -9,7 +9,7 @@ *) theory struct -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "struct.c" diff --git a/tools/autocorres/tests/proof-tests/struct2.thy b/tools/autocorres/tests/proof-tests/struct2.thy index f63ece9bb..0b7da16b6 100644 --- a/tools/autocorres/tests/proof-tests/struct2.thy +++ b/tools/autocorres/tests/proof-tests/struct2.thy @@ -9,7 +9,7 @@ *) theory struct2 -imports "../../AutoCorres" +imports "AutoCorres.AutoCorres" begin install_C_file "struct2.c" diff --git a/tools/autocorres/tests/proof-tests/word_abs_cases.thy b/tools/autocorres/tests/proof-tests/word_abs_cases.thy index bb29dca2a..1390cea47 100644 --- a/tools/autocorres/tests/proof-tests/word_abs_cases.thy +++ b/tools/autocorres/tests/proof-tests/word_abs_cases.thy @@ -9,7 +9,7 @@ *) theory word_abs_cases imports - "../../AutoCorres" + "AutoCorres.AutoCorres" begin (* extra optimization for word_abs (currently does not work) *) diff --git a/tools/autocorres/tests/proof-tests/word_abs_options.thy b/tools/autocorres/tests/proof-tests/word_abs_options.thy index f56ad3dfe..32d2acd8a 100644 --- a/tools/autocorres/tests/proof-tests/word_abs_options.thy +++ b/tools/autocorres/tests/proof-tests/word_abs_options.thy @@ -8,7 +8,7 @@ * @TAG(NICTA_BSD) *) -theory word_abs_options imports "../../AutoCorres" begin +theory word_abs_options imports "AutoCorres.AutoCorres" begin install_C_file "word_abs_options.c" diff --git a/tools/c-parser/testfiles/RISCV64/imports/MachineWords.thy b/tools/c-parser/testfiles/RISCV64/imports/MachineWords.thy index c86f9a1c5..61ced4c05 100644 --- a/tools/c-parser/testfiles/RISCV64/imports/MachineWords.thy +++ b/tools/c-parser/testfiles/RISCV64/imports/MachineWords.thy @@ -9,7 +9,7 @@ *) theory MachineWords -imports "../../../CTranslation" +imports "CParser.CTranslation" begin type_synonym machine_word_len = "64"