copilot-theorem 4.2 → 4.3

raw patch · 9 files changed

+641/−143 lines, 9 filesdep +HUnitdep ~copilot-coredep ~copilot-prettyprinterPVP ok

version bump matches the API change (PVP)

Dependencies added: HUnit

Dependency ranges changed: copilot-core, copilot-prettyprinter

API changes (from Hackage documentation)

Files

• CHANGELOG +7/−0
• README.md +74/−73
• copilot-theorem.cabal +4/−3
• src/Copilot/Theorem/IL/Translate.hs +7/−2
• src/Copilot/Theorem/Misc/SExpr.hs +1/−1
• src/Copilot/Theorem/TransSys/Translate.hs +1/−1
• src/Copilot/Theorem/What4.hs +347/−30
• src/Copilot/Theorem/What4/Translate.hs +36/−21
• tests/Test/Copilot/Theorem/What4.hs +164/−12

@@ -1,3 +1,10 @@+2025-03-07+        * Version bump (4.3). (#604)+        * Fix multiple typos in README. (#560)+        * Fix typo in documentation. (#587)+        * Add function to produce counterexamples for invalid properties. (#589)+        * Reject existentially quantified properties in What4 backend. (#254)+ 2025-01-07         * Version bump (4.2). (#577)         * Remove uses of Copilot.Core.Expr.UExpr.uExprType,uExprExpr. (#565)

@@ -4,7 +4,7 @@  Highly automated proof techniques are a necessary step for the widespread adoption of formal methods in the software industry. Moreover, it could provide-a partial answer to one of its main issue which is scalability.+a partial answer to one of its main issues, which is scalability.  *copilot-theorem* is a Copilot library aimed at checking automatically some safety properties on Copilot programs. It includes:@@ -17,9 +17,9 @@   proving basic k-inductive properties and for pedagogical purposes.  * A prover producing native inputs for the *Kind2* model checker, developed at-  University of Iowa. The latter uses both the *k-induction algorithm* extended-  with *path compression* and *structural abstraction* [2] and the **IC3-  algorithm** with counterexample generalization based on *approximate+  the University of Iowa. The latter uses both the *k-induction algorithm*+  extended with *path compression* and *structural abstraction* [2] and the+  **IC3 algorithm** with counterexample generalization based on *approximate   quantifier elimination* [3].  ## A Tutorial@@ -39,12 +39,12 @@ ### First steps  *copilot-theorem* is aimed at checking **safety properties** on Copilot programs.-Intuitively, a safety property is a property which express the idea that+Intuitively, a safety property is a property that expresses the idea that *nothing bad can happen*. In particular, any invalid safety property can be disproved by a finite execution trace of the program called a **counterexample**. Safety properties are often opposed to **liveness** properties, which express the idea that *something good will eventually-happen*. The latters are out of the scope of *copilot-theorem*.+happen*. The latter is out of the scope of *copilot-theorem*.  Safety properties are simply expressed with standard boolean streams. In addition to triggers and observers declarations, it is possible to bind a@@ -70,7 +70,7 @@ * The name of the proposition we want to check. * A strategy to prove the proposition. -In this case the proposition is simple enough so that we can check it directly+In this case, the proposition is simple enough so that we can check it directly by k-induction using `kind2Prover`. Therefore we can just write:  ```haskell@@ -79,14 +79,15 @@   prove spec' "gt0" (tell [Check $ kind2Prover def]) ``` -where `kind2Prover def` stands for the *Kind2 prover* with default+where `kind2Prover def` stands for the *Kind2 prover* with the default configuration.  #### The Kind2 prover -The *Kind2* prover uses the model checker with the same name, from Iowa-university. It translates the Copilot specification into a *modular transition-system* (the Kind2 native format) and then calls the `kind2` executable.+The *Kind2* prover uses the model checker with the same name, from the+University of Iowa. It translates the Copilot specification into a *modular+transition system* (the Kind2 native format) and then calls the `kind2`+executable.  It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prover :: Options -> Prover` where the `Options` type is defined as@@ -117,7 +118,7 @@ ### An introduction to SMT-based model checking  An introduction to the model-checking techniques used by *copilot-theorem* can be-found in the `doc` folder of this repository. It consists in a self sufficient+found in the `doc` folder of this repository. It consists of a self-sufficient set of slides. You can find some additional readings in the *References* section. @@ -216,16 +217,16 @@ #### Types  In these three formats, GADTs are used to statically ensure a part of the-type-corectness of the specification, in the same spirit it is done in the-other Copilot libraries. *copilot-theorem* handles only three types which are-`Integer`, `Real` and `Bool` and which are handled by the SMTLib standard.+type-correctness of the specification, in the same spirit as in+other Copilot libraries. *copilot-theorem* works with only three types,+`Integer`, `Real` and `Bool`, all of which SMT-Lib can handle. *copilot-theorem* works with *pure* reals and integers. Thus, it is unsafe in the sense it ignores integer overflow problems and the loss of precision due to floating point arithmetic.  #### The Kind2 prover -The *Kind2 prover* first translates the copilot specification into a *modular+The *Kind2 prover* first translates the Copilot specification into a *modular transition system*. Then, a chain of transformations is applied to this system (for instance, in order to remove dependency cycles among nodes). After this, the system is translated into the *Kind2 native format* and the `kind2`@@ -234,7 +235,7 @@  ##### Modular transition systems -Let's look at the definition of a *modular transition systems*, in the+Let's look at the definition of a *modular transition system*, in the `TransSys.Spec` module:  ```haskell@@ -295,10 +296,10 @@  ##### The translation process -First, a copilot specification is translated into a modular transition system.+First, a Copilot specification is translated into a modular transition system. This process is defined in the `TransSys.Translate` module. Each stream is-associated to a node. The most significant task of this translation process is-to *flatten* the copilot specification so the value of all streams at time *n*+associated with a node. The most significant task of this translation process is+to *flatten* the Copilot specification so the value of all streams at time *n* only depends on the values of all the streams at time *n - 1*, which is not the case in the `Fib` example shown earlier. This is done by a simple program transformation which turns this:@@ -337,13 +338,13 @@ file format*. Indeed, it is natural to bind each node to a predicate but the Kind2 file format requires that each predicate only uses previously defined predicates. However, some nodes in our transition system could be mutually-recursive. Therefore, the goal of the `removeCycles :: Spec -> Spec` function-defined in `TransSys.Transform` is to remove such dependency cycles.+recursive. Therefore, the goal of the `removeCycles :: Spec -> Spec` function,+defined in `TransSys.Transform`, is to remove such dependency cycles. -This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function-which signature is self-explicit. The latter solves name conflicts by using the-`Misc.Renaming` monad. Some code complexity has been added so the variable-names remains as clear as possible after merging two nodes.+This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function,+whose signature is self-explicit. The latter solves name conflicts by using the+`Misc.Renaming` monad. Some code complexity has been added so variable names+remain as clear as possible after merging two nodes.  The function `removeCycles` computes the strongly connected components of the dependency graph and merge each one into a single node. The complexity of this@@ -354,7 +355,7 @@ After the cycles have been removed, it is useful to apply another transformation which makes the translation from `TransSys.Spec` to `Kind2.AST` easier. This transformation is implemented in the `complete` function. In a-nutshell, it transforms a system such that+nutshell, it transforms a system such that:  * If a node depends on another, it imports *all* its variables. * The dependency graph is transitive, that is if *A* depends of *B* which@@ -374,7 +375,7 @@  which discards all the structure of a *modular transition system* and turns it into a *non-modular transition system* with only one node. In fact, when-translating a copilot specification to a kind2 file, two styles are available:+translating a Copilot specification to a Kind2 file, two styles are available: the `Kind2.toKind2` function takes a `Style` argument which can take the value `Inlined` or `Modular`. The only difference is that in the first case, a call to `removeCycles` is replaced by a call to `inline`.@@ -382,17 +383,17 @@ ### Limitations of copilot-theorem  Now, we will discuss some limitations of the *copilot-theorem* tool. These-limitations are organized in two categories: the limitations related to the-Copilot language itself and its implementation, and the limitations related to-the model-checking techniques we are using.+limitations are split into two categories: limitations related to the Copilot+language itself and its implementation, and limitations related to the+model-checking techniques we are using.  #### Limitations related to Copilot implementation -The reification process used to build the `Core.Spec` object looses many-informations about the structure of the original Copilot program. In fact, a-stream is kept in the reified program only if it is recursively defined.-Otherwise, all its occurences will be inlined. Moreover, let's look at the-`intCounter` function defined in the example `Grey.hs`:+The reification process used to build the `Core.Spec` object loses information+about the structure of the original Copilot program. In fact, a stream is kept+in the reified program only if it is recursively defined.  Otherwise, all its+occurrences will be inlined. Moreover, let's look at the `intCounter` function+defined in the example `Grey.hs`:  ```haskell intCounter :: Stream Bool -> Stream Word64@@ -413,8 +414,8 @@ * It makes the inputs given to the SMT solvers larger and repetitive.  We can't rewrite the Copilot reification process in order to avoid these-inconvenients as these informations are lost by GHC itself before it occurs.-The only solution we can see would be to use *Template Haskell* to generate+inconveniences as this information is lost by GHC itself before it occurs. The+only solution we can see would be to use *Template Haskell* to generate automatically some structural annotations, which might not be worth the dirt introduced. @@ -423,7 +424,7 @@ ##### Limitations of the IC3 algorithm  The IC3 algorithm was shown to be a very powerful tool for hardware-certification. However, the problems encountered when verifying softwares are+certification. However, the problems encountered when verifying software are much more complex. For now, very few non-inductive properties can be proved by *Kind2* when basic integer arithmetic is involved. @@ -433,32 +434,32 @@ lemma discarding it which is general enough so that all CTIs can be discarded in a finite number of steps. -The lemmas found by the current version fo *Kind2* are often too weak. Some+The lemmas found by the current version of *Kind2* are often too weak. Some suggestions to enhance this are presented in [1]. We hope some progress will be-made in this area in a near future.+made in this area in the near future. -A workaround to this problem would be to write kind of an interactive mode-where the user is invited to provide some additional lemmas when automatic-techniques fail. Another solution would be to make the properties being checked+A workaround to this problem would be to write an interactive mode where the+user is invited to provide some additional lemmas when automatic techniques+fail. Another solution would be to make the properties being checked quasi-inductive by hand. In this case, *copilot-theorem* is still a useful tool (especially for finding bugs) but the verification of a program can be long and-requires a high level of technicity.+requires a high level of technical knowledge.  ##### Limitations related to the SMT solvers -The use of SMT solvers introduces two kind of limitations:+The use of SMT solvers introduces two kinds of limitations:  1. We are limited by the computing power needed by the SMT solvers 2. SMT solvers can't handle quantifiers efficiently  Let's consider the first point. SMT solving is costly and its performances are sometimes unpredictable. For instance, when running the `SerialBoyerMoore`-example with the *k-induction prover*, Yices2 does not terminate. However, the *z3*+example with the *k-induction prover*, Yices2 does not terminate. However, the *Z3* SMT solver used by *Kind2* solves the problem instantaneously. Note that this performance gap is not due to the use of the IC3 algorithm because the property to check is inductive. It could be related to the fact the SMT problem produced by the *k-induction prover* uses uninterpreted functions for encoding streams instead-of simple integer variables, which is the case when the copilot program is+of simple integer variables, which is the case when the Copilot program is translated into a transition system. However, this wouldn't explain why the *k-induction prover* still terminates instantaneously on the `BoyerMoore` example, which seems not simpler by far.@@ -472,10 +473,10 @@ *Future work* section). However, this trick is not always possible. For instance, in the `SerialBoyerMoore` example, the property being checked should be quantified over all integer constants. Here, we can't just introduce an-arbitrary constant stream because it is the quantified property which is+arbitrary constant stream because it is the quantified property that is inductive and not the property specialized for a given constant stream. That's-why we have no other solution than replacing universal quantification by-*bounded* universal quantification by assuming all the elements of the input+why we have no other solution than replacing universal quantification with+*bounded* universal quantification, assuming all the elements of the input stream are in the finite list `allowed` and using the function `forAllCst`:  ```haskell@@ -487,13 +488,13 @@ ```  However, this solution isn't completely satisfying because the size of the-property generated is proportionnal to the cardinal of `allowed`.+property generated is proportional to the length of `allowed`.  #### Some scalability issues -A standard way to prove large programs is to rely on its logical structure by-writing a specification for each of its functions. This very natural approach-is hard to follow in our case because of+A standard way to prove large programs is to rely on their logical structure,+by writing a specification for each of their functions. This very natural+approach is hard to follow in our case due to:  * The difficulty to deal with universal quantification. * The lack of *true* functions in Copilot: the latter offers metaprogramming@@ -503,7 +504,7 @@  Once again, *copilot-theorem* is still a very useful tool, especially for debugging purposes. However, we don't think it is adapted to write and check a-complete specification for large scale programs.+complete specification for large-scale programs.  ## Future work @@ -512,19 +513,19 @@ These features are not currently provided due to the lack of important features in the Kind2 SMT solver. -#### Counterexamples displaying+#### Displaying counterexamples  Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't support XML output of counterexamples. If the last feature is provided, it-should be easy to implement counterexamples displaying in *copilot-theorem*. For-this, we recommend to keep some informations about *observers* in+should be easy to implement displaying of counterexamples in *copilot-theorem*.+For this, we recommend keeping some information about *observers* in `TransSys.Spec` and to add one variable per observer in the Kind2 output file.  #### Bad handling of non-linear operators and external functions  Non-linear Copilot operators and external functions are poorly handled because-of the lack of support of uninterpreted functions in the Kind2 native format. A-good way to handle these would be to use uninterpreted functions. With this+of the lack of support for uninterpreted functions in the Kind2 native format.+A good way to handle these would be to use uninterpreted functions. With this solution, properties like ```haskell 2 * sin x + 1 <= 3@@ -533,7 +534,7 @@ ```haskell let y = x in sin x == sin y ```-Currently, the *Kind2 prover* fail with the last example, as the results of+Currently, the *Kind2 prover* fails with the last example, as the results of unknown functions are turned into fresh unconstrained variables.  ### Simple extensions@@ -542,7 +543,7 @@ architecture of Kind2.  + If inductive proving of a property fails, giving the user a concrete CTI-  (*Counterexample To The Inductiveness*, see the [1]).+  (*Counterexample To The Inductiveness*, see [1]).  + Use Template Haskell to declare automatically some observers with the same   names used in the original program.@@ -559,29 +560,29 @@    - Declare assumptions and invariants next to the associated code instead of     gathering all properties in a single place.-  - Declare a frequent code pattern which should be factorized in the-    transition problem (see the section about Copilot limitations)+  - Declare a frequent code pattern that can be factorized in the transition+    problem (see the section about Copilot limitations)  ## FAQ -### Why does the code related to transition systems look so complex ?+### Why does the code related to transition systems look so complex? -It is true the code of `TransSys` is quite complex. In fact, it would be really-straightforward to produce a flattened transition system and then a Kind2 file-with just a single *top* predicate. In fact, It would be as easy as producing-an *IL* specification.+It is true that the code of `TransSys` is quite complex. In fact, it would be+really straightforward to produce a flattened transition system and then a+Kind2 file with just a single *top* predicate. In fact, It would be as easy as+producing an *IL* specification.  To be honest, I'm not sure producing a modular *Kind2* output is worth the complexity added. It's especially true at the time I write this in the sense that:  * Each predicate introduced is used only one time (which is true because-  copilot doesn't handle functions or parametrized streams like Lustre does and-  everything is inlined during the reification process).+  Copilot doesn't handle functions or parameterized streams like Lustre does+  and everything is inlined during the reification process). * A similar form of structure could be obtained from a flattened Kind2 native   input file with some basic static analysis by producing a dependency graph   between variables.-* For now, the *Kind2* model-checker ignores these structure informations.+* For now, the *Kind2* model-checker ignores these structures.  However, the current code offers some nice transformation tools (node merging, `Renaming` monad...) which could be useful if you intend to write a tool for

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 4.2+version                   : 4.3 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -63,8 +63,8 @@                           , xml                   >= 1.3 && < 1.4                           , what4                 >= 1.3 && < 1.7 -                          , copilot-core          >= 4.2 && < 4.3-                          , copilot-prettyprinter >= 4.2 && < 4.3+                          , copilot-core          >= 4.3 && < 4.4+                          , copilot-prettyprinter >= 4.3 && < 4.4    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove@@ -121,6 +121,7 @@    build-depends:       base+    , HUnit     , QuickCheck     , test-framework     , test-framework-quickcheck2

@@ -63,8 +63,13 @@   localConstraints <- popLocalConstraints   properties <- Map.fromList <$>     forM specProperties-      (\(C.Property {C.propertyName, C.propertyExpr}) -> do-        e' <- expr propertyExpr+      (\(C.Property {C.propertyName, C.propertyProp}) -> do+        -- Soundness note: it is OK to call `extractProp` here to drop the+        -- quantifier from the proposition `propertyProp`. This is because we+        -- IL translation always occurs within the context of a function that+        -- returns a `Proof`, and these `Proof` functions are always careful to+        -- use `Prover`s that respect the propositions's quantifier.+        e' <- expr (C.extractProp propertyProp)         propConds <- popLocalConstraints         return (propertyName, (propConds, e'))) 

@@ -31,7 +31,7 @@ list = List                 -- (ss)  -- | Sequence of expressions with a root or main note, and a series of--- additional expressions or arguments..+-- additional expressions or arguments. node a l = List (Atom a : l)    -- (s ss)  -- A straightforward string representation for 'SExpr's of Strings that

@@ -139,7 +139,7 @@ streamOfProp prop =   C.Stream { C.streamId = 42            , C.streamBuffer = []-           , C.streamExpr = C.propertyExpr prop+           , C.streamExpr = C.extractProp (C.propertyProp prop)            , C.streamExprType = C.Bool }  stream :: C.Stream -> Trans Node

@@ -32,22 +32,35 @@ -- We perform @k@-induction on all the properties in a given specification where -- @k@ is chosen to be the maximum amount of delay on any of the involved -- streams. This is a heuristic choice, but often effective.+--+-- The functions in this module are only designed to prove universally+-- quantified propositions (i.e., propositions that use @forAll@). Attempting to+-- prove an existentially quantified proposition (i.e., propositions that use+-- @exists@) will cause a 'UnexpectedExistentialProposition' exception to be+-- thrown. module Copilot.Theorem.What4   ( -- * Proving properties about Copilot specifications     prove   , Solver(..)   , SatResult(..)+  , proveWithCounterExample+  , SatResultCex(..)+  , CounterExample(..)+  , ProveException(..)     -- * Bisimulation proofs about @copilot-c99@ code   , computeBisimulationProofBundle   , BisimulationProofBundle(..)   , BisimulationProofState(..)     -- * What4 representations of Copilot expressions   , XExpr(..)+  , CopilotValue(..)+  , StreamOffset(..)   ) where -import qualified Copilot.Core.Expr as CE-import qualified Copilot.Core.Spec as CS-import qualified Copilot.Core.Type as CT+import qualified Copilot.Core.Expr       as CE+import qualified Copilot.Core.Spec       as CS+import qualified Copilot.Core.Type       as CT+import qualified Copilot.Core.Type.Array as CTA  import qualified What4.Config                   as WC import qualified What4.Expr.Builder             as WB@@ -57,15 +70,18 @@ import qualified What4.Solver                   as WS import qualified What4.Solver.DReal             as WS +import Control.Exception (Exception, throw) import Control.Monad (forM) import Control.Monad.State import qualified Data.BitVector.Sized as BV import Data.Foldable (foldrM) import Data.List (genericLength) import qualified Data.Map as Map+import Data.Parameterized.Classes (ShowF) import Data.Parameterized.NatRepr import Data.Parameterized.Nonce import Data.Parameterized.Some+import qualified Data.Parameterized.Vector as V import GHC.Float (castWord32ToFloat, castWord64ToDouble) import LibBF (BigFloat, bfToDouble, pattern NearEven) import qualified Panic as Panic@@ -89,17 +105,256 @@ data SatResult = Valid | Invalid | Unknown   deriving Show -type CounterExample = [(String, Some CopilotValue)]+-- | The 'proveWithCounterExample' function returns results of this form for+-- each property in a spec. This is largely the same as 'SatResult', except that+-- 'InvalidCex' also records a 'CounterExample'.+data SatResultCex = ValidCex | InvalidCex CounterExample | UnknownCex+  deriving Show +-- | Concrete values that cause a property in a Copilot specification to be+-- invalid. As a simple example, consider the following spec:+--+-- @+-- spec :: Spec+-- spec = do+--   let s :: Stream Bool+--       s = [False] ++ constant True+--   void $ prop "should be invalid" (forAll s)+-- @+--+-- This defines a stream @s@ where the first value is @False@, but all+-- subsequent values are @True@'. This is used in a property that asserts that+-- the values in @s@ will be @True@ at all possible time steps. This is clearly+-- not true, given that @s@'s first value is @False@. As such, we would expect+-- that proving this property would yield an 'InvalidCex' result, where one of+-- the base cases would state that the @s@ stream contains a @False@ value.+--+-- We can use the 'proveWithCounterExample' function to query an SMT solver to+-- compute a counterexample:+--+-- @+-- CounterExample+--   { 'baseCases' =+--       [False]+--   , 'inductionStep' =+--       True+--   , 'concreteExternVars' =+--       fromList []+--   , 'concreteStreamValues' =+--       fromList+--         [ ( (0, 'AbsoluteOffset' 0), False )+--         , ( (0, 'RelativeOffset' 0), False )+--         , ( (0, 'RelativeOffset' 1), True )+--         ]+--   }+-- @+--+-- Let's go over what this counterexample is saying:+--+-- * The 'inductionStep' of the proof is 'True', so that part of the proof was+--   successful. On the other hand, the 'baseCases' contain a 'False', so the+--   proof was falsified when proving the base cases. (In this case, the list+--   has only one element, so there is only a single base case.)+--+-- * 'concreteStreamValues' reports the SMT solver's concrete values for each+--   stream during relevant parts of the proof as a 'Map.Map'.+--+--   The keys of the map are pairs. The first element of the pair is the stream+--   'CE.Id', and in this example, the only 'CE.Id' is @0@, corresponding to the+--   stream @s@. The second element is the time offset. An 'AbsoluteOffset'+--   indicates an offset starting from the initial time step, and a+--   'RelativeOffset' indicates an offset from an arbitrary point in time.+--   'AbsoluteOffset's are used in the base cases of the proof, and+--   'RelativeOffset's are used in the induction step of the proof.+--+--   The part of the map that is most interesting to us is the+--   @( (0, 'AbsoluteOffset' 0), False )@ entry, which represents a base case+--   where there is a value of @False@ in the stream @s@ during the initial time+--   step. Sure enough, this is enough to falsify the property @forAll s@.+--+-- * There are no extern streams in this example, so 'concreteExternVars' is+--   empty.+--+-- We can also see an example of where a proof succeeds in the base cases, but+-- fails during the induction step:+--+-- @+-- spec :: Spec+-- spec = do+--   let t :: Stream Bool+--       t = [True] ++ constant False+--   void $ prop "should also be invalid" (forAll t)+-- @+--+-- With the @t@ stream above, the base cases will succeed+-- ('proveWithCounterExample' uses @k@-induction with a value of @k == 1@ in+-- this example, so there will only be a single base case). On the other hand,+-- the induction step will fail, as later values in the stream will be @False@.+-- If we try to 'proveWithCounterExample' this property, then it will fail with:+--+-- @+-- CounterExample+--   { 'baseCases' =+--       [True]+--   , 'inductionStep' =+--       False+--   , 'concreteExternVars' =+--       fromList []+--   , 'concreteStreamValues' =+--       fromList+--         [ ( (0, 'AbsoluteOffset' 0), True )+--         , ( (0, 'RelativeOffset' 0), True )+--         , ( (0, 'RelativeOffset' 1), False )+--         ]+--   }+-- @+--+-- This time, the 'inductionStep' is 'False'. If we look at the+-- 'concreteStreamValues', we see the values at @'RelativeOffset' 0@ and+-- @'RelativeOffset' 1@ (which are relevant to the induction step) are @True@+-- and @False@, respectively. Since this is a proof by @k@-induction where+-- @k == 1@, the fact that the value at @'RelativeOffset 1@ is @False@ indicates+-- that the induction step was falsified.+--+-- Note that this proof does not say /when/ exactly the time steps at+-- @'RelativeOffset' 0@ or @'RelativeOffset' 1@ occur, only that that will occur+-- relative to some arbitrary point in time. In this example, they occur+-- relative to the initial time step, so @'RelativeOffset' 1@ would occur at the+-- second time step overall. In general, however, these time steps may occur far+-- in the future, so it is possible that one would need to step through the+-- execution of the streams for quite some time before finding the+-- counterexample.+--+-- Be aware that counterexamples involving struct values are not currently+-- supported.+data CounterExample = CounterExample+    { -- | A list of base cases in the proof, where each entry in the list+      -- corresponds to a particular time step. For instance, the first element+      -- in the list corresponds to the initial time step, the second element+      -- in the list corresponds to the second time step, and so on. A 'False'+      -- entry anywhere in this list will cause the overall proof to be+      -- 'InvalidCex'.+      --+      -- Because the proof uses @k@-induction, the number of base cases (i.e.,+      -- the number of entries in this list) is equal to the value of @k@,+      -- which is chosen using heuristics.+      baseCases :: [Bool]+      -- | Whether the induction step of the proof was valid or not. That is,+      -- given an arbitrary time step @n@, if the property is assumed to hold+      -- at time steps @n@, @n+1@, ..., @n+k@, then this will be @True@ is the+      -- property can the be proven to hold at time step @n+k+1@ (and 'False'+      -- otherwise). If this is 'False', then the overall proof will be+      -- 'InvalidCex'.+    , inductionStep :: Bool+      -- | The concrete values in the Copilot specification's extern streams+      -- that lead to the property being invalid.+      --+      -- Each key in the 'Map.Map' is the 'CE.Name' of an extern stream paired+      -- with a 'StreamOffset' representing the time step. The key's+      -- corresponding value is the concrete value of the extern stream at that+      -- time step.+    , concreteExternValues ::+        Map.Map (CE.Name, StreamOffset) (Some CopilotValue)+      -- | The concrete values in the Copilot specification's streams+      -- (excluding extern streams) that lead to the property being invalid.+      --+      -- Each key in the 'Map.Map' is the 'CE.Id' of a stream paired with a+      -- 'StreamOffset' representing the time step. The key's corresponding+      -- value is the concrete value of the extern stream at that time step.+    , concreteStreamValues :: Map.Map (CE.Id, StreamOffset) (Some CopilotValue)+    }+  deriving Show++-- | Exceptions that can arise when attempting a proof.+data ProveException+  = UnexpectedExistentialProposition+    -- ^ The functions in "Copilot.Theorem.What4" can only prove properties with+    -- universally quantified propositions. The functions in+    -- "Copilot.Theorem.What4" will throw this exception if they encounter an+    -- existentially quantified proposition.+  deriving Show++instance Exception ProveException+ -- | Attempt to prove all of the properties in a spec via an SMT solver (which -- must be installed locally on the host). Return an association list mapping -- the names of each property to the result returned by the solver.+--+-- PRE: All of the properties in the 'CS.Spec' use universally quantified+-- propositions. Attempting to supply an existentially quantified proposition+-- will cause a 'UnexpectedExistentialProposition' exception to be thrown. prove :: Solver       -- ^ Solver to use       -> CS.Spec       -- ^ Spec       -> IO [(CE.Name, SatResult)]-prove solver spec = do+prove solver spec = proveInternal solver spec $ \_ _ _ satRes ->+  case satRes of+    WS.Sat _   -> pure Invalid+    WS.Unsat _ -> pure Valid+    WS.Unknown -> pure Unknown++-- | Attempt to prove all of the properties in a spec via an SMT solver (which+-- must be installed locally on the host). Return an association list mapping+-- the names of each property to the result returned by the solver.+--+-- Unlike 'prove', 'proveWithCounterExample' returns a 'SatResultCex'. This+-- means that if a result is invalid, then it will include a 'CounterExample'+-- which describes the circumstances under which the property was falsified. See+-- the Haddocks for 'CounterExample' for more details.+--+-- Note that this function does not currently support creating counterexamples+-- involving struct values, so attempting to call 'proveWithCounterExample' on a+-- specification that uses structs will raise an error.+proveWithCounterExample :: Solver+                        -- ^ Solver to use+                        -> CS.Spec+                        -- ^ Spec+                        -> IO [(CE.Name, SatResultCex)]+proveWithCounterExample solver spec =+  proveInternal solver spec $ \baseCases indStep st satRes ->+    case satRes of+      WS.Sat ge -> do+        gBaseCases <- traverse (WG.groundEval ge) baseCases+        gIndStep <- WG.groundEval ge indStep+        gExternValues <- traverse (valFromExpr ge) (externVars st)+        gStreamValues <- traverse (valFromExpr ge) (streamValues st)+        let cex = CounterExample+              { baseCases            = gBaseCases+              , inductionStep        = gIndStep+              , concreteExternValues = gExternValues+              , concreteStreamValues = gStreamValues+              }+        pure (InvalidCex cex)+      WS.Unsat _ -> pure ValidCex+      WS.Unknown -> pure UnknownCex++-- | Attempt to prove all of the properties in a spec via an SMT solver (which+-- must be installed locally on the host). For each 'WS.SatResult' returned by+-- the solver, pass it to a continuation along with the relevant parts of the+-- proof-related state.+--+-- This is an internal-only function that is used to power 'prove' and+-- 'proveWithCounterExample'.+proveInternal :: Solver+              -- ^ Solver to use+              -> CS.Spec+              -- ^ Spec+              -> (forall sym t st fm+                   . ( sym ~ WB.ExprBuilder t st (WB.Flags fm)+                     , WI.KnownRepr WB.FloatModeRepr fm )+                  => [WI.Pred sym]+                     -- The proof's base cases+                  -> WI.Pred sym+                     -- The proof's induction step+                  -> TransState sym+                     -- The proof state+                  -> WS.SatResult (WG.GroundEvalFn t) ()+                     -- The overall result of the proof+                  -> IO a)+              -- ^ Continuation to call on each solver result+              -> IO [(CE.Name, a)]+proveInternal solver spec k = do   -- Setup symbolic backend   Some ng <- newIONonceGenerator   sym <- WB.newExprBuilder WB.FloatIEEERepr EmptyState ng@@ -118,9 +373,15 @@   -- This process performs k-induction where we use @k = maxBufLen@.   -- The choice for @k@ is heuristic, but often effective.   let proveProperties = forM (CS.specProperties spec) $ \pr -> do+        -- This function only supports universally quantified propositions, so+        -- throw an exception if we encounter an existentially quantified+        -- proposition.+        let prop = case CS.propertyProp pr of+                     CS.Forall p  -> p+                     CS.Exists {} -> throw UnexpectedExistentialProposition         -- State the base cases for k induction.         base_cases <- forM [0 .. maxBufLen - 1] $ \i -> do-          xe <- translateExpr sym mempty (CS.propertyExpr pr) (AbsoluteOffset i)+          xe <- translateExpr sym mempty prop (AbsoluteOffset i)           case xe of             XBool p -> return p             _ -> expectedBool "Property" xe@@ -128,7 +389,7 @@         -- Translate the induction hypothesis for all values up to maxBufLen in         -- the past         ind_hyps <- forM [0 .. maxBufLen-1] $ \i -> do-          xe <- translateExpr sym mempty (CS.propertyExpr pr) (RelativeOffset i)+          xe <- translateExpr sym mempty prop (RelativeOffset i)           case xe of             XBool hyp -> return hyp             _ -> expectedBool "Property" xe@@ -137,7 +398,7 @@         ind_goal <- do           xe <- translateExpr sym                               mempty-                              (CS.propertyExpr pr)+                              prop                               (RelativeOffset maxBufLen)           case xe of             XBool p -> return p@@ -153,24 +414,31 @@         not_p <- liftIO $ WI.notPred sym p         let clauses = [not_p] -        case solver of-          CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case-            WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)-            WS.Unsat _ -> return (CS.propertyName pr, Valid)-            WS.Unknown -> return (CS.propertyName pr, Unknown)-          DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case-            WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)-            WS.Unsat _ -> return (CS.propertyName pr, Valid)-            WS.Unknown -> return (CS.propertyName pr, Unknown)-          Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case-            WS.Sat _ge -> return (CS.propertyName pr, Invalid)-            WS.Unsat _ -> return (CS.propertyName pr, Valid)-            WS.Unknown -> return (CS.propertyName pr, Unknown)-          Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case-            WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)-            WS.Unsat _ -> return (CS.propertyName pr, Valid)-            WS.Unknown -> return (CS.propertyName pr, Unknown)+        st <- get+        let k' = k base_cases ind_case st+        satRes <-+          case solver of+            CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case+              WS.Sat (ge, _) -> k' (WS.Sat ge)+              WS.Unsat x -> k' (WS.Unsat x)+              WS.Unknown -> k' WS.Unknown+            DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case+              WS.Sat (c, m) -> do+                ge <- WS.getAvgBindings c m+                k' (WS.Sat ge)+              WS.Unsat x -> k' (WS.Unsat x)+              WS.Unknown -> k' WS.Unknown+            Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case+              WS.Sat ge -> k' (WS.Sat ge)+              WS.Unsat x -> k' (WS.Unsat x)+              WS.Unknown -> k' WS.Unknown+            Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case+              WS.Sat (ge, _) -> k' (WS.Sat ge)+              WS.Unsat x -> k' (WS.Unsat x)+              WS.Unknown -> k' WS.Unknown +        pure (CS.propertyName pr, satRes)+   -- Execute the action and return the results for each property   runTransM spec proveProperties @@ -180,6 +448,10 @@ -- to carry out a bisimulation proof that establishes a correspondence between -- the states of the Copilot stream program and the C code that @copilot-c99@ -- would generate for that Copilot program.+--+-- PRE: All of the properties in the 'CS.Spec' use universally quantified+-- propositions. Attempting to supply an existentially quantified proposition+-- will cause a 'UnexpectedExistentialProposition' exception to be thrown. computeBisimulationProofBundle ::      WFP.IsInterpretedFloatSymExprBuilder sym   => sym@@ -341,6 +613,10 @@     return (nm, Some tp, v)  -- | Compute the user-provided property assumptions in a Copilot program.+--+-- PRE: All of the properties in the 'CS.Spec' use universally quantified+-- propositions. Attempting to supply an existentially quantified proposition+-- will cause a 'UnexpectedExistentialProposition' exception to be thrown. computeAssumptions ::      forall sym.      WFP.IsInterpretedFloatSymExprBuilder sym@@ -360,9 +636,12 @@     -- user-provided property assumptions.     specPropertyExprs :: [CE.Expr Bool]     specPropertyExprs =-      [ CS.propertyExpr p+      [ CS.extractProp (CS.propertyProp p)       | p <- CS.specProperties spec       , elem (CS.propertyName p) properties+      , let prop = case CS.propertyProp p of+                     CS.Forall pr -> pr+                     CS.Exists {} -> throw UnexpectedExistentialProposition       ]      -- Compute all of the what4 predicates corresponding to each user-provided@@ -387,10 +666,32 @@ expectedBool what xe =   panic [what ++ " expected to have boolean result", show xe] -data CopilotValue a = CopilotValue { cvType :: CT.Type a-                                   , cvVal :: a-                                   }+-- | A Copilot value paired with its 'CT.Type'.+data CopilotValue a where+  CopilotValue :: CT.Typed a => CT.Type a -> a -> CopilotValue a +instance Show (CopilotValue a) where+  showsPrec p (CopilotValue ty val) =+    case ty of+      CT.Bool      -> showsPrec p val+      CT.Int8      -> showsPrec p val+      CT.Int16     -> showsPrec p val+      CT.Int32     -> showsPrec p val+      CT.Int64     -> showsPrec p val+      CT.Word8     -> showsPrec p val+      CT.Word16    -> showsPrec p val+      CT.Word32    -> showsPrec p val+      CT.Word64    -> showsPrec p val+      CT.Float     -> showsPrec p val+      CT.Double    -> showsPrec p val+      CT.Array {}  -> showsPrec p val+      CT.Struct {} -> showsPrec p val+instance ShowF CopilotValue++-- | Convert a symbolic 'XExpr' into a concrete 'CopilotValue'.+--+-- Struct values are not currently supported, so attempting to convert an+-- 'XStruct' value will raise an error. valFromExpr :: forall sym t st fm.                ( sym ~ WB.ExprBuilder t st (WB.Flags fm)                , WI.KnownRepr WB.FloatModeRepr fm@@ -420,7 +721,23 @@                        (fst . bfToDouble NearEven)                        fromRational                        (castWord64ToDouble . fromInteger . BV.asUnsigned)-  _ -> error "valFromExpr unhandled case"+  XEmptyArray tp ->+    pure $ Some $ CopilotValue (CT.Array @0 tp) (CTA.array [])+  XArray es -> do+    (someCVs :: V.Vector n (Some CopilotValue)) <- traverse (valFromExpr ge) es+    (Some (CopilotValue headTp _headVal), _) <- pure $ V.uncons someCVs+    cvs <-+      traverse+        (\(Some (CopilotValue tp val)) ->+          case tp `testEquality` headTp of+            Just Refl -> pure val+            Nothing -> panic [ "XArray with mismatched element types"+                             , show tp+                             , show headTp+                             ])+        someCVs+    pure $ Some $ CopilotValue (CT.Array @n headTp) (CTA.array (V.toList cvs))+  XStruct _ -> error "valFromExpr: Structs not currently handled"   where     fromBV :: forall a w . Num a => BV.BV w -> a     fromBV = fromInteger . BV.asUnsigned

@@ -56,7 +56,7 @@                                                  intValue, isZeroOrGT1,                                                  knownNat, minusPlusCancel,                                                  mkNatRepr, testNatCases,-                                                 testStrictLeq)+                                                 testStrictLeq, withKnownNat) import           Data.Parameterized.Some        (Some (..)) import           Data.Parameterized.SymbolRepr  (SymbolRepr, knownSymbol) import qualified Data.Parameterized.Vector      as V@@ -370,10 +370,10 @@     elts <- traverse (translateConstExpr sym tp) (CT.arrayElems a)     Some n <- return $ mkNatRepr (genericLength elts)     case isZeroOrGT1 n of-      Left Refl -> return XEmptyArray+      Left Refl -> return $ XEmptyArray tp       Right LeqProof -> do         let Just v = V.fromList n elts-        return $ XArray v+        return $ withKnownNat n $ XArray v   CT.Struct _ -> do     elts <- forM (CT.toValues a) $ \(CT.Value tp (CT.Field a)) ->       translateConstExpr sym tp a@@ -409,7 +409,7 @@   atp@(CT.Array itp) -> do     let n = arrayLen atp     case isZeroOrGT1 n of-      Left Refl -> return XEmptyArray+      Left Refl -> return $ XEmptyArray itp       Right LeqProof -> do         Refl <- return $ minusPlusCancel n (knownNat @1)         elts :: V.Vector n (XExpr t) <-@@ -1281,7 +1281,13 @@     XDouble <$> WFP.iFloatIte @_ @WFP.DoubleFloat sym pred e1 e2   (XStruct xes1, XStruct xes2) ->     XStruct <$> zipWithM (mkIte sym pred) xes1 xes2-  (XEmptyArray, XEmptyArray) -> return XEmptyArray+  (XEmptyArray tp1, XEmptyArray tp2) ->+    case tp1 `testEquality` tp2 of+      Just Refl -> return (XEmptyArray tp1)+      Nothing -> panic [ "Element type mismatch in ite"+                       , show tp1+                       , show tp2+                       ]   (XArray xes1, XArray xes2) ->     case V.length xes1 `testEquality` V.length xes2 of       Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2@@ -1438,25 +1444,34 @@                    sym                    (WFP.SymInterpretedFloatType sym WFP.DoubleFloat)               -> XExpr sym-  XEmptyArray :: XExpr sym-  XArray      :: 1 <= n => V.Vector n (XExpr sym) -> XExpr sym++  -- | An empty array. The 'CT.Typed' constraint and accompanying 'CT.Type'+  -- field are necessary in order to record evidence that the array type can be+  -- used in a context where 'CT.Typed' is required.+  XEmptyArray :: CT.Typed t => CT.Type t -> XExpr sym++  -- | A non-empty array. The 'KnownNat' constraint is necessary in order to+  -- record evidence that the array type can be used in a context for 'CT.Typed'+  -- is required.+  XArray      :: (KnownNat n, 1 <= n) => V.Vector n (XExpr sym) -> XExpr sym+   XStruct     :: [XExpr sym] -> XExpr sym  instance WI.IsExprBuilder sym => Show (XExpr sym) where-  show (XBool e)    = "XBool " ++ show (WI.printSymExpr e)-  show (XInt8 e)    = "XInt8 " ++ show (WI.printSymExpr e)-  show (XInt16 e)   = "XInt16 " ++ show (WI.printSymExpr e)-  show (XInt32 e)   = "XInt32 " ++ show (WI.printSymExpr e)-  show (XInt64 e)   = "XInt64 " ++ show (WI.printSymExpr e)-  show (XWord8 e)   = "XWord8 " ++ show (WI.printSymExpr e)-  show (XWord16 e)  = "XWord16 " ++ show (WI.printSymExpr e)-  show (XWord32 e)  = "XWord32 " ++ show (WI.printSymExpr e)-  show (XWord64 e)  = "XWord64 " ++ show (WI.printSymExpr e)-  show (XFloat e)   = "XFloat " ++ show (WI.printSymExpr e)-  show (XDouble e)  = "XDouble " ++ show (WI.printSymExpr e)-  show XEmptyArray  = "[]"-  show (XArray vs)  = showList (V.toList vs) ""-  show (XStruct xs) = "XStruct " ++ showList xs ""+  show (XBool e)       = "XBool " ++ show (WI.printSymExpr e)+  show (XInt8 e)       = "XInt8 " ++ show (WI.printSymExpr e)+  show (XInt16 e)      = "XInt16 " ++ show (WI.printSymExpr e)+  show (XInt32 e)      = "XInt32 " ++ show (WI.printSymExpr e)+  show (XInt64 e)      = "XInt64 " ++ show (WI.printSymExpr e)+  show (XWord8 e)      = "XWord8 " ++ show (WI.printSymExpr e)+  show (XWord16 e)     = "XWord16 " ++ show (WI.printSymExpr e)+  show (XWord32 e)     = "XWord32 " ++ show (WI.printSymExpr e)+  show (XWord64 e)     = "XWord64 " ++ show (WI.printSymExpr e)+  show (XFloat e)      = "XFloat " ++ show (WI.printSymExpr e)+  show (XDouble e)     = "XDouble " ++ show (WI.printSymExpr e)+  show (XEmptyArray _) = "[]"+  show (XArray vs)     = showList (V.toList vs) ""+  show (XStruct xs)    = "XStruct " ++ showList xs ""  -- * Stream offsets 

@@ -1,4 +1,6 @@-{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-} -- The following warning is disabled due to a necessary instance of SatResult -- defined in this module. {-# OPTIONS_GHC -fno-warn-orphans #-}@@ -6,18 +8,23 @@ module Test.Copilot.Theorem.What4 where  -- External imports+import Control.Exception                    (Exception, try) import Data.Int                             (Int8)+import Data.Proxy                           (Proxy (..))+import Data.Typeable                        (typeRep) import Data.Word                            (Word32) import Test.Framework                       (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.HUnit                           (Assertion, assertBool,+                                             assertFailure) import Test.QuickCheck                      (Arbitrary (arbitrary), Property,                                              arbitrary, forAll) import Test.QuickCheck.Monadic              (monadicIO, run)  -- External imports: Copilot-import           Copilot.Core.Expr      (Expr (Const, Op1, Op2))+import           Copilot.Core.Expr      (Expr (Const, Drop, Op1, Op2), Id) import           Copilot.Core.Operators (Op1 (..), Op2 (..))-import           Copilot.Core.Spec      (Spec (..))+import           Copilot.Core.Spec      (Spec (..), Stream (..)) import qualified Copilot.Core.Spec      as Copilot import           Copilot.Core.Type      (Field (..),                                          Struct (toValues, typeName),@@ -25,7 +32,9 @@                                          Value (..))  -- Internal imports: Modules being tested-import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove)+import Copilot.Theorem.What4 (CounterExample (..), ProveException (..),+                              SatResult (..), SatResultCex (..), Solver (..),+                              prove, proveWithCounterExample)  -- * Constants @@ -37,6 +46,9 @@     , testProperty "Prove via Z3 that false is invalid" testProveZ3False     , testProperty "Prove via Z3 that x == x is valid"  testProveZ3EqConst     , testProperty "Prove via Z3 that a struct update is valid" testProveZ3StructUpdate+    , testProperty "Counterexample with invalid base case" testCounterExampleBaseCase+    , testProperty "Counterexample with invalid induction step" testCounterExampleInductionStep+    , testProperty "Check that the What4 backend rejects existential quantification" testWhat4ExistsException     ]  -- * Individual tests@@ -53,7 +65,7 @@     propName = "prop"      spec :: Spec-    spec = propSpec propName $ Const typeOf True+    spec = forallPropSpec propName [] $ Const typeOf True  -- | Test that Z3 is able to prove the following expression invalid: -- @@@ -67,7 +79,7 @@     propName = "prop"      spec :: Spec-    spec = propSpec propName $ Const typeOf False+    spec = forallPropSpec propName [] $ Const typeOf False  -- | Test that Z3 is able to prove the following expresion valid: -- @@@ -81,7 +93,7 @@     propName = "prop"      spec :: Int8 -> Spec-    spec x = propSpec propName $+    spec x = forallPropSpec propName [] $       Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)  -- | Test that Z3 is able to prove the following expresion valid:@@ -97,7 +109,7 @@     propName = "prop"      spec :: TestStruct -> Spec-    spec s = propSpec propName $+    spec s = forallPropSpec propName [] $       Op2         (Eq typeOf)         (getField@@ -116,6 +128,86 @@         add1 :: Expr Word32 -> Expr Word32         add1 x = Op2 (Add typeOf) x (Const typeOf 1) +-- | Test that Z3 is able to produce a counterexample to the following property,+-- where the base case is proved invalid:+--+-- @+--   let s :: Stream Bool+--       s = [False] ++ constant True+--   in forAll s+-- @+testCounterExampleBaseCase :: Property+testCounterExampleBaseCase =+    monadicIO $ run $+      checkCounterExample Z3 propName spec $ \cex ->+        pure $ not $ and $ baseCases cex+  where+    propName :: String+    propName = "prop"++    -- s = [False] ++ constant True+    s :: Stream+    s = Stream+      { streamId       = sId+      , streamBuffer   = [False]+      , streamExpr     = Const typeOf True+      , streamExprType = typeOf+      }++    sId :: Id+    sId = 0++    spec :: Spec+    spec = forallPropSpec propName [s] $ Drop typeOf 0 sId++-- | Test that Z3 is able to produce a counterexample to the following property,+-- where the induction step is proved invalid:+--+-- @+--   let s :: Stream Bool+--       s = [True] ++ constant False+--   in forAll s+-- @+testCounterExampleInductionStep :: Property+testCounterExampleInductionStep =+    monadicIO $ run $+      checkCounterExample Z3 propName spec $ \cex ->+        pure $ not $ inductionStep cex+  where+    propName :: String+    propName = "prop"++    -- s = [True] ++ constant False+    s :: Stream+    s = Stream+      { streamId       = sId+      , streamBuffer   = [True]+      , streamExpr     = Const typeOf False+      , streamExprType = typeOf+      }++    sId :: Id+    sId = 0++    spec :: Spec+    spec = forallPropSpec propName [s] $ Drop typeOf 0 sId++-- | Test that @copilot-theorem@'s @what4@ backend will throw an exception if it+-- attempts to prove an existentially quantified proposition.+testWhat4ExistsException :: Property+testWhat4ExistsException =+    monadicIO $ run $+      checkException (prove Z3 spec) isUnexpectedExistentialProposition+  where+    isUnexpectedExistentialProposition :: ProveException -> Bool+    isUnexpectedExistentialProposition UnexpectedExistentialProposition = True++    propName :: String+    propName = "prop"++    spec :: Spec+    spec = existsPropSpec propName [] $ Const typeOf True+ -- | A simple data type with a 'Struct' instance and a 'Field'. This is only -- used as part of 'testProveZ3StructUpdate'. newtype TestStruct = TestStruct { testField :: Field "testField" Word32 }@@ -145,12 +237,72 @@   -- does not exist in the results, in which case the lookup returns 'Nothing'.   return $ propResult == Just expectation +-- | Check that the solver produces an invalid result for the given property and+-- that the resulting 'CounterExample' satifies the given predicate.+checkCounterExample :: Solver+                    -> String+                    -> Spec+                    -> (CounterExample -> IO Bool)+                    -> IO Bool+checkCounterExample solver propName spec cexPred = do+  results <- proveWithCounterExample solver spec++  -- Find the satisfiability result for propName. If the property name does not+  -- exist in the results, raise an assertion failure.+  propResult <-+    case lookup propName results of+      Just propResult ->+        pure propResult+      Nothing ->+        assertFailure $+          "Could not find property in results: " ++ propName++  -- Assert that the solver returned an invalid result and pass the+  -- counterexample to the predicate. If the result is anything other than+  -- invalid, raise an assertion failure.+  case propResult of+    InvalidCex cex ->+      cexPred cex+    ValidCex {} ->+      assertFailure "Expected invalid result, but result was valid"+    UnknownCex {} ->+      assertFailure "Expected invalid result, but result was unknown"++-- | Check that the given 'IO' action throws a particular exception. This is+-- largely taken from the implementation of @shouldThrow@ in+-- @hspec-expectations@ (note that this test suite uses @test-framework@ instead+-- of @hspec@).+checkException :: forall e a. Exception e => IO a -> (e -> Bool) -> Assertion+checkException action p = do+    r <- try action+    case r of+      Right _ ->+        assertFailure $+          "did not get expected exception: " ++ exceptionType+      Left e ->+        assertBool+          ("predicate failed on expected exception: " ++ exceptionType +++           "\n" ++ show e)+          (p e)+  where+    -- String representation of the expected exception's type+    exceptionType = show $ typeRep $ Proxy @e+ -- * Auxiliary --- | Build a 'Spec' that contains one property with the given name and defined--- by the given boolean expression.-propSpec :: String -> Expr Bool -> Spec-propSpec propName propExpr = Spec [] [] [] [Copilot.Property propName propExpr]+-- | Build a 'Spec' that contains one property with the given name, which+-- contains the given streams, and is defined by the given boolean expression,+-- which is universally quantified.+forallPropSpec :: String -> [Stream] -> Expr Bool -> Spec+forallPropSpec propName propStreams propExpr =+  Spec propStreams [] [] [Copilot.Property propName (Copilot.Forall propExpr)]++-- | Build a 'Spec' that contains one property with the given name, which+-- contains the given streams, and is defined by the given boolean expression,+-- which is existentially quantified.+existsPropSpec :: String -> [Stream] -> Expr Bool -> Spec+existsPropSpec propName propStreams propExpr =+  Spec propStreams [] [] [Copilot.Property propName (Copilot.Exists propExpr)]  -- | Equality for 'SatResult'. --