diff --git a/lib/Monad_WP/Datatype_Schematic.thy b/lib/Monads/Datatype_Schematic.thy similarity index 100% rename from lib/Monad_WP/Datatype_Schematic.thy rename to lib/Monads/Datatype_Schematic.thy diff --git a/lib/Monad_WP/Less_Monad_Syntax.thy b/lib/Monads/Less_Monad_Syntax.thy similarity index 100% rename from lib/Monad_WP/Less_Monad_Syntax.thy rename to lib/Monads/Less_Monad_Syntax.thy diff --git a/lib/Monad_WP/NonDetMonad.thy b/lib/Monads/NonDetMonad.thy similarity index 100% rename from lib/Monad_WP/NonDetMonad.thy rename to lib/Monads/NonDetMonad.thy diff --git a/lib/Monad_WP/NonDetMonadLemmas.thy b/lib/Monads/NonDetMonadLemmas.thy similarity index 100% rename from lib/Monad_WP/NonDetMonadLemmas.thy rename to lib/Monads/NonDetMonadLemmas.thy diff --git a/lib/Monad_WP/NonDetMonadVCG.thy b/lib/Monads/NonDetMonadVCG.thy similarity index 100% rename from lib/Monad_WP/NonDetMonadVCG.thy rename to lib/Monads/NonDetMonadVCG.thy diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monads/OptionMonad.thy similarity index 100% rename from lib/Monad_WP/OptionMonad.thy rename to lib/Monads/OptionMonad.thy diff --git a/lib/Monad_WP/OptionMonadND.thy b/lib/Monads/OptionMonadND.thy similarity index 100% rename from lib/Monad_WP/OptionMonadND.thy rename to lib/Monads/OptionMonadND.thy diff --git a/lib/Monad_WP/OptionMonadWP.thy b/lib/Monads/OptionMonadWP.thy similarity index 100% rename from lib/Monad_WP/OptionMonadWP.thy rename to lib/Monads/OptionMonadWP.thy diff --git a/lib/Monad_WP/Strengthen.thy b/lib/Monads/Strengthen.thy similarity index 100% rename from lib/Monad_WP/Strengthen.thy rename to lib/Monads/Strengthen.thy diff --git a/lib/Monad_WP/Strengthen_Demo.thy b/lib/Monads/Strengthen_Demo.thy similarity index 100% rename from lib/Monad_WP/Strengthen_Demo.thy rename to lib/Monads/Strengthen_Demo.thy diff --git a/lib/Monad_WP/TraceMonad.thy b/lib/Monads/TraceMonad.thy similarity index 100% rename from lib/Monad_WP/TraceMonad.thy rename to lib/Monads/TraceMonad.thy diff --git a/lib/Monad_WP/TraceMonadLemmas.thy b/lib/Monads/TraceMonadLemmas.thy similarity index 100% rename from lib/Monad_WP/TraceMonadLemmas.thy rename to lib/Monads/TraceMonadLemmas.thy diff --git a/lib/Monad_WP/TraceMonadVCG.thy b/lib/Monads/TraceMonadVCG.thy similarity index 100% rename from lib/Monad_WP/TraceMonadVCG.thy rename to lib/Monads/TraceMonadVCG.thy diff --git a/lib/Monad_WP/WhileLoopRules.thy b/lib/Monads/WhileLoopRules.thy similarity index 100% rename from lib/Monad_WP/WhileLoopRules.thy rename to lib/Monads/WhileLoopRules.thy diff --git a/lib/Monad_WP/WhileLoopRulesCompleteness.thy b/lib/Monads/WhileLoopRulesCompleteness.thy similarity index 100% rename from lib/Monad_WP/WhileLoopRulesCompleteness.thy rename to lib/Monads/WhileLoopRulesCompleteness.thy diff --git a/lib/Monad_WP/wp/Eisbach_WP.thy b/lib/Monads/wp/Eisbach_WP.thy similarity index 100% rename from lib/Monad_WP/wp/Eisbach_WP.thy rename to lib/Monads/wp/Eisbach_WP.thy diff --git a/lib/Monad_WP/wp/WP-method.ML b/lib/Monads/wp/WP-method.ML similarity index 100% rename from lib/Monad_WP/wp/WP-method.ML rename to lib/Monads/wp/WP-method.ML diff --git a/lib/Monad_WP/wp/WP.thy b/lib/Monads/wp/WP.thy similarity index 100% rename from lib/Monad_WP/wp/WP.thy rename to lib/Monads/wp/WP.thy diff --git a/lib/Monad_WP/wp/WPBang.thy b/lib/Monads/wp/WPBang.thy similarity index 100% rename from lib/Monad_WP/wp/WPBang.thy rename to lib/Monads/wp/WPBang.thy diff --git a/lib/Monad_WP/wp/WPC.thy b/lib/Monads/wp/WPC.thy similarity index 100% rename from lib/Monad_WP/wp/WPC.thy rename to lib/Monads/wp/WPC.thy diff --git a/lib/Monad_WP/wp/WPEx.thy b/lib/Monads/wp/WPEx.thy similarity index 100% rename from lib/Monad_WP/wp/WPEx.thy rename to lib/Monads/wp/WPEx.thy diff --git a/lib/Monad_WP/wp/WPFix.thy b/lib/Monads/wp/WPFix.thy similarity index 100% rename from lib/Monad_WP/wp/WPFix.thy rename to lib/Monads/wp/WPFix.thy diff --git a/lib/Monad_WP/wp/WPI.thy b/lib/Monads/wp/WPI.thy similarity index 100% rename from lib/Monad_WP/wp/WPI.thy rename to lib/Monads/wp/WPI.thy diff --git a/lib/Monad_WP/wp/WPSimp.thy b/lib/Monads/wp/WPSimp.thy similarity index 100% rename from lib/Monad_WP/wp/WPSimp.thy rename to lib/Monads/wp/WPSimp.thy diff --git a/lib/Monad_WP/wp/WP_Pre.thy b/lib/Monads/wp/WP_Pre.thy similarity index 100% rename from lib/Monad_WP/wp/WP_Pre.thy rename to lib/Monads/wp/WP_Pre.thy diff --git a/lib/ROOT b/lib/ROOT index de7a27539..b77b55b3b 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -12,8 +12,8 @@ session Lib (lib) = Word_Lib + Eisbach_Tools ML_Utils directories - "Monad_WP" - "Monad_WP/wp" + "Monads" + "Monads/wp" theories Lib AddUpdSimps @@ -74,27 +74,27 @@ session Lib (lib) = Word_Lib + (* 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/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" + "Monads/WhileLoopRules" + "Monads/TraceMonad" + "Monads/OptionMonadND" + "Monads/OptionMonadWP" + "Monads/Strengthen_Demo" + "Monads/TraceMonadLemmas" + "Monads/wp/WPBang" + "Monads/wp/WPFix" + "Monads/wp/Eisbach_WP" + "Monads/wp/WPI" + "Monads/wp/WPC" + "Monads/wp/WP_Pre" + "Monads/wp/WP" + "Monads/Datatype_Schematic" + "Monads/WhileLoopRulesCompleteness" + "Monads/Strengthen" + "Monads/OptionMonad" + "Monads/TraceMonadVCG" + "Monads/NonDetMonadVCG" + "Monads/NonDetMonad" + "Monads/NonDetMonadLemmas" session CLib (lib) in clib = CParser + sessions diff --git a/proof/invariant-abstract/README.md b/proof/invariant-abstract/README.md index 4515a4d50..736889ae3 100644 --- a/proof/invariant-abstract/README.md +++ b/proof/invariant-abstract/README.md @@ -9,7 +9,7 @@ Abstract Spec Invariant Proof This proof defines and proves the global invariants of seL4's [abstract specification](../../spec/abstract/). The invariants are -phrased and proved using a [monadic Hoare logic](../../lib/Monad_WP/NonDetMonad.thy) +phrased and proved using a [monadic Hoare logic](../../lib/Monads/NonDetMonad.thy) described in a TPHOLS '08 [paper][1]. [1]: https://trustworthy.systems/publications/nictaabstracts/Cock_KS_08.abstract "Secure Microkernels, State Monads and Scalable Refinement" diff --git a/spec/abstract/README.md b/spec/abstract/README.md index 2f076ba45..2046d88c8 100644 --- a/spec/abstract/README.md +++ b/spec/abstract/README.md @@ -14,7 +14,7 @@ specification. The specification draws in additional interface files from `design` and `machine`. The specification is written in monadic style. See -`l4v/lib/Monad_WP/NonDetMonad` for the definition of this monad. +`l4v/lib/Monads/NonDetMonad` for the definition of this monad. Top-Level Theory ----------------