From c4419c04021548cc970b27b22863f2e5f9e65334 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Fri, 16 Feb 2024 12:33:25 +1100 Subject: [PATCH] lib/monads: add a nondet README and improves wp's Signed-off-by: Corey Lewis --- lib/Monads/README.md | 19 ++- lib/Monads/nondet/Nondet_README.thy | 142 ++++++++++++++++++ .../WPReadme.txt => Monads/wp/WP_README.thy} | 61 +++++--- 3 files changed, 196 insertions(+), 26 deletions(-) create mode 100644 lib/Monads/nondet/Nondet_README.thy rename lib/{doc/WPReadme.txt => Monads/wp/WP_README.thy} (64%) diff --git a/lib/Monads/README.md b/lib/Monads/README.md index 28d00f00e1..9d9dac4b56 100644 --- a/lib/Monads/README.md +++ b/lib/Monads/README.md @@ -26,14 +26,23 @@ In particular, this session defines: - for the nondeterministic state monad, additional concepts such as wellformedness with respect to failure (`empty_fail`), absence of failure - (`no_fail`), absence of exceptions (`no_throw`). See the respective theories - for more details. + (`no_fail`), absence of exceptions (`no_throw`). See its [README][nondet] and + the respective theories for more details. + +- the trace monad has similar concepts where applicable, and its theories follow + the same structure as that of the nondet monad. The directory [`wp/`](./wp/) contains proof methods to reason about these monads -in weakest-precondition style. +in weakest-precondition style. See its [README][wp] for more details. + +This session also introduces a [strengthen] method, which is useful for +performing rewriting steps within the complex conclusions that often appear when +working with these monads. [l4v]: https://github.com/seL4/l4v/ -[nondet]: ./nondet/Nondet_Monad.thy +[nondet]: ./nondet/Nondet_README.thy [option]: ./reader_option/Reader_Option_Monad.thy [trace]: ./trace/Trace_Monad.thy -[AutoCorres]: ../../tools/autocorres/ \ No newline at end of file +[AutoCorres]: ../../tools/autocorres/ +[wp]: ./wp/WP_README.thy +[strengthen]: ./Strengthen_Demo.thy diff --git a/lib/Monads/nondet/Nondet_README.thy b/lib/Monads/nondet/Nondet_README.thy new file mode 100644 index 0000000000..4cf9de4a1a --- /dev/null +++ b/lib/Monads/nondet/Nondet_README.thy @@ -0,0 +1,142 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Nondet_README + imports + Nondet_More_VCG + Nondet_Det + Nondet_No_Throw + Nondet_Monad_Equations + WP_README +begin + +\ \Nondeterministic State Monad with Failure\ + +text \ +The type of the nondeterministic monad, @{typ "('s, 'a) nondet_monad"}, can be found in +@{theory Monads.Nondet_Monad}, along with definitions of fundamental monad primitives and +Haskell-like do-syntax. + +The basic type of the nondeterministic state monad with failure is very similar to the +normal state monad. Instead of a pair consisting of result and new state, we return a set +of these pairs coupled with a failure flag. Each element in the set is a potential result +of the computation. The flag is @{const True} if there is an execution path in the +computation that may have failed. Conversely, if the flag is @{const False}, none of the +computations resulting in the returned set can have failed. + +The following lemmas are basic examples of those primitives and that syntax.\ + +lemma "do x \ return 1; + return (2::nat); + return x + od = + return 1 >>= + (\x. return (2::nat) >>= + K_bind (return x))" + by (rule refl) + +lemma "do x \ return 1; + return 2; + return x + od = return 1" + by simp + +text \ +We also provide a variant of the nondeterministic monad extended with exceptional return +values. This is available by using the type @{typ "('s, 'e + 'a) nondet_monad"}, with +primitives and syntax existing for it as well\ + +lemma "doE x \ returnOk 1; + returnOk (2::nat); + returnOk x + odE = + returnOk 1 >>=E + (\x. returnOk (2::nat) >>=E + K_bind (returnOk x))" + by (rule refl) + +text \ +A Hoare logic for partial correctness for the nondeterministic state monad and the +exception monad is introduced in @{theory Monads.Nondet_VCG}. This comes along with a +family of lemmas and tools which together perform the role of a VCG (verification +condition generator). + +The Hoare logic is defined by the @{const valid} predicate, which is a triple of +precondition, monadic function, and postcondition. A version is also provided for the +exception monad, in the form of @{const validE}. Instead of one postcondition it has two: +one for normal and one for exceptional results. + +@{theory Monads.Nondet_VCG} also proves a collection of rules about @{const valid}, in +particular lifting rules for the common operators and weakest precondition rules for the +monadic primitives. The @{method wp} tool automates the storage and use of this +collection of rules. For more details about @{method wp} see @{theory Monads.WP_README}. + +The following is an example of one of these operator lifting rules and an example of a +relatively trivial Hoare triple being solved by @{method wp}.\ + +lemma hoare_vcg_if_split: + "\P \ \Q\ f \S\; \P \ \R\ g \S\\ + \ \\s. (P \ Q s) \ (\P \ R s)\ if P then f else g \S\" + by simp + +lemma + "\\s. odd (value s)\ + do + x <- gets value; + return (3 * x) + od + \\rv s. odd rv\" + by wpsimp + +text \ +Lemmas directly about the monad primitives can be found in @{theory Monads.Nondet_Lemmas} +and @{theory Monads.Nondet_Monad_Equations}. Many of these lemmas use @{method monad_eq}, +which is a tactic for solving monadic equalities.\ + +lemma + "(do x \ gets f; + xa \ gets f; + m xa x + od) = + (do xa \ gets f; + m xa xa + od)" + by monad_eq + +lemma + "snd (gets_the X s) = (X s = None)" + by (monad_eq simp: gets_the_def gets_def get_def) + +text \ +While working with the monad primitives you sometimes end up needing to reason directly +on the states, with goals containing terms in the form of @{term "(v, s') \ fst (m s)"}. +Lemmas for handling these goals exist in @{theory Monads.Nondet_In_Monad}, with +@{thm in_monad} being particularly useful.\ + +lemma + "(r, s) \ fst (return r s)" + by (simp add: in_monad) + +text \ +There are additional properties of nondeterministic monadic functions that are often +useful. These include: + @{const no_fail} - a monad does not fail when starting in a state that satisfies a + given precondition. + @{const empty_fail} - if a monad returns an empty set of results then it must also have + the failure flag set. + @{const no_throw} - an exception monad does not throw an exception when starting in a + state that satisfies a given precondition. + @{const det} - a monad is deterministic and returns exactly one non-failing state.\ + +text \ +Variants of the basic validity definition are sometimes useful when working with the +nondeterministic monad. + @{const validNF} - a total correctness extension combining @{const valid} and + @{const no_fail}. + @{const exs_valid} - a dual to @{const valid} showing that after a monad executes there + exists at least one state that satisfies a given condition.\ + +end diff --git a/lib/doc/WPReadme.txt b/lib/Monads/wp/WP_README.thy similarity index 64% rename from lib/doc/WPReadme.txt rename to lib/Monads/wp/WP_README.thy index fec3734aed..ba14a06f94 100644 --- a/lib/doc/WPReadme.txt +++ b/lib/Monads/wp/WP_README.thy @@ -1,33 +1,40 @@ -# -# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) -# -# SPDX-License-Identifier: BSD-2-Clause -# +(* + * Copyright 2024, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause +*) -Readme for the 'WP' tool and friends +theory WP_README + imports + Nondet_More_VCG +begin -The nondeterministic monad framework comes with a collection of tools which +\ \The 'WP' tool and friends\ + +text\ +The monad framework comes with a collection of tools which together perform the role of a VCG (verification condition generator). The usual strategy for proving a Hoare triple is via backward propagation from the postcondition. The initial step is to replace the current precondition with an Isabelle schematic variable using a precondition weakening rule such as -'hoare_pre'. This schematic variable is progressively instantiated by applying +@{thm hoare_pre}. This schematic variable is progressively instantiated by applying weakest precondition rules as introduction rules. The implication between the assumed and generated preconditions must be solved by some other means. This approach requires a large family of weakest precondition rules, including one for each monadic combinator and operation, and further rules for -user-defined monadic operations. The 'wp' tool automates the storage and use of +user-defined monadic operations. The @{method wp} tool automates the storage and use of this collection of rules. Weakest precondition rules are marked with the 'wp' -attribute and will be automatically applied. +attribute and are then automatically applied. -The 'wp' tool also also handles the construction of variations of 'wp' rules +The 'wp' tool also handles the construction of variations of 'wp' rules via combinator rules. If the postcondition being proved is a conjunction and a weakest precondition rule is available for the first conjunct, progress can be -made by first applying the 'hoare_vcg_conj_lift' combinator rule and then the +made by first applying the @{thm hoare_vcg_conj_lift} combinator rule and then the rule of interest. The 'wp_comb' attribute given to such rules in -NonDetMonadVCG.thy specifies that they should be used in this way. +@{theory Monads.Nondet_VCG} specifies that they should be used in this way. The 'wp' tool's semantics are defined entirely by these sets of rules. It always either applies a 'wp' rule as an introduction rule, or applies a @@ -38,11 +45,10 @@ selected last-first. There is also a 'wp_split' rule set which are not combined with combinators and which are applied only if no 'wp' rules can be applied. Note that rules may be supplied which are not the actual weakest precondition. -This may cause the tool to produce unhelpfully weak conclusions. Perhaps the -tool should actually be named 'p'. The 'hoare_vcg_prop' rule supplied in -NonDetMonadVCG.thy is unsafe in this manner. It is convenient that -postconditions which ignore the results of the operation can be handled -immediately (especially when used with the combinator rules), however +This may cause the tool to produce unhelpfully weak conclusions. The +@{thm hoare_vcg_prop} rule supplied in @{theory Monads.Nondet_VCG} is unsafe in this manner. +It is convenient that postconditions which ignore the results of the operation can +be handled immediately (especially when used with the combinator rules), however information from assertions in the program may be discarded. Rules declared 'wp' do not have to match an unspecified postcondition. It was @@ -60,15 +66,19 @@ that case spliting cannot be done via Isabelle's normal mechanisms. Isabelle's implicitly doing case splits on meta-quantified tuples in a way that blocks unification. -The 'wpc' tool synthesises the needed case split rules for datatype case +The @{method wpc} tool synthesises the needed case split rules for datatype case statements in the function bodies in the Hoare triples. +There are several cases where unification of the schematic preconditions can cause +problems. The @{method wpfix} tool handles four of the most common of these cases. +See @{theory Monads.WPFix} and @{theory Monads.Datatype_Schematic} for more details. + A further caveat is that the 'wp' and 'wp_comb' rulesets provided are not necessarily ideal. Updating these rulesets would create difficult maintenance problems, and thus they are largely left as first defined. One issue that has not been addressed is the implicit precondition weakening done by combinator -rules 'hoare_post_comb_imp_conj' and 'hoare_vcg_precond_imp'. In hindsight it -would be better if 'hoare_pre' were always applied manually, or if the 'wp' +rules @{thm hoare_post_comb_imp_conj} and @{thm hoare_vcg_precond_imp}. In hindsight it +would be better if @{thm hoare_pre} were always applied manually, or if the 'wp' tool itself could decide when they ought be applied. Note that such weakening rules were not supplied for the error hoare triples/quadruple, which postdate this realisation. @@ -83,4 +93,13 @@ The 'wp' tool may be extended to new triples or other judgements by supplying an appropriate set of rules. A 'wp_trip' rule may be provided to accelerate rule lookup. +The `wp` tool can also be traced, either by invoking it with `wp (trace)` or by +setting the config value `wp_trace` to `true`. This will list the rules used by `wp`, +in the order that they were applied. It is occasionally helpful to see the specific +instantiations of the rules used, to see how their preconditions were unified. This +can be done by setting `wp_trace_instantiation` to `true`. + +For ease of use, @{method wpsimp} is available and wraps up the standard usage pattern +of '(wpfix|wp|wpc|clarsimp)+'.\ +end