diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,10 @@ +2025-03-07 + * Version bump (4.3). (#604) + * Include missing dependencies in installation instructions. (#591) + * Update version of GHC in README. (#590) + * Add example of how to use proveWithCounterExample. (#589) + * List all Copilot packages in installation command in README. (#597) + 2025-01-07 * Version bump (4.2). (#577) * Bump upper version constraint on filepath. (#570) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -100,19 +100,20 @@ On other Linux distributions or older Debian-based distributions, to use Copilot you must install a Haskell compiler (GHC) and the package manager Cabal. We currently support all versions of GHC from 8.6.5 to modern versions -(9.8 as of this writing). You can install the toolchain using +(9.10 as of this writing). You can install the toolchain using [ghcup](https://www.haskell.org/ghcup/) or, if you are on Debian/Ubuntu, -directly with `apt-get`: +you can use `apt-get` to install all dependencies as follows: ```sh -$ sudo apt-get install ghc cabal-install +$ sudo apt-get install ghc cabal-install alex happy pkg-config libz-dev ``` Once the compiler is installed, install Copilot from [Hackage](https://hackage.haskell.org/package/copilot) with: ```sh -cabal v2-install --lib copilot +cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language \ + copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter ``` To test that Copilot is available, execute the following: @@ -141,7 +142,8 @@ [Hackage](https://hackage.haskell.org/package/copilot) with: ```sh -$ cabal v2-install --lib copilot +$ cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language \ + copilot-theorem copilot-libraries copilot-interpreter copilot-prettyprinter ``` To test that Copilot is available, execute the following: diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.2 +version: 4.3 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -52,12 +52,12 @@ , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.6 - , copilot-core >= 4.2 && < 4.3 - , copilot-theorem >= 4.2 && < 4.3 - , copilot-language >= 4.2 && < 4.3 - , copilot-libraries >= 4.2 && < 4.3 - , copilot-c99 >= 4.2 && < 4.3 - , copilot-prettyprinter >= 4.2 && < 4.3 + , copilot-core >= 4.3 && < 4.4 + , copilot-theorem >= 4.3 && < 4.4 + , copilot-language >= 4.3 && < 4.4 + , copilot-libraries >= 4.3 && < 4.4 + , copilot-c99 >= 4.3 && < 4.4 + , copilot-prettyprinter >= 4.3 && < 4.4 exposed-modules: Language.Copilot, Language.Copilot.Main @@ -78,6 +78,19 @@ main-is: Arithmetic.hs hs-source-dirs: examples/what4 build-depends: base + , copilot + , copilot-theorem + default-language: Haskell2010 + if flag(examples) + buildable: True + else + buildable: False + +executable what4-arithmetic-counterexamples + main-is: ArithmeticCounterExamples.hs + hs-source-dirs: examples/what4 + build-depends: base + , containers , copilot , copilot-theorem default-language: Haskell2010 diff --git a/examples/what4/ArithmeticCounterExamples.hs b/examples/what4/ArithmeticCounterExamples.hs new file mode 100644 --- /dev/null +++ b/examples/what4/ArithmeticCounterExamples.hs @@ -0,0 +1,110 @@ +-- | An example showing the usage of the What4 backend in copilot-theorem for +-- simple arithmetic. This example uses the 'proveWithCounterExamples' function +-- to demonstrate counterexamples in the event of invalid properties. + +module Main where + +import qualified Prelude as P +import Control.Monad (void, forM_) +import qualified Data.Map as Map + +import Language.Copilot +import Copilot.Theorem.What4 + +spec :: Spec +spec = do + -- Define some external streams. Their values are not important, so external + -- streams suffice. + let eint8 :: Stream Int8 + eint8 = extern "eint8" Nothing + eword8 :: Stream Word8 + eword8 = extern "eword8" Nothing + efloat :: Stream Float + efloat = extern "efloat" Nothing + + -- The simplest example involving numbers: equality on constant values. + void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1))) + + -- Testing "a < a + 1". This should fail, because it isn't true. + void $ prop "Example 2" (forAll (eint8 < (eint8 + 1))) + + -- Adding another condition to the above property to make it true. + void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127))) + + -- Just like the previous example, but with words. + void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255))) + + -- An example with floats. + void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat))) + + -- Another example with floats. This fails, because it isn't true. + void $ prop "Example 6" (forAll ((efloat + 1) /= efloat)) + +main :: IO () +main = do + spec' <- reify spec + + -- Use Z3 to prove the properties. + results <- proveWithCounterExample Z3 spec' + + -- Print the results. + forM_ results $ \(nm, res) -> do + putStr $ nm <> ": " + case res of + ValidCex -> putStrLn "valid" + InvalidCex cex -> do + putStrLn "invalid" + putStrLn $ ppCounterExample cex + UnknownCex -> putStrLn "unknown" + +-- | Pretty-print a counterexample for user display. +ppCounterExample :: CounterExample -> String +ppCounterExample cex + | any P.not (baseCases cex) + = if Map.null baseCaseVals + then + " All possible extern values during the base case(s) " P.++ + "constitute a counterexample." + else + unlines $ + " The base cases failed with the following extern values:" : + map + (\((name, _), val) -> " " P.++ name P.++ ": " P.++ show val) + (Map.toList baseCaseVals) + + | P.not (inductionStep cex) + = if Map.null inductionStepVals + then + " All possible extern values during the induction step " P.++ + "constitute a counterexample." + else + unlines $ + " The induction step failed with the following extern values:" : + map + (\((name, _), val) -> " " P.++ name P.++ ": " P.++ show val) + (Map.toList inductionStepVals) + + | otherwise + = error $ + "ppCounterExample: " P.++ + "Counterexample without failing base cases or induction step" + where + allExternVals = concreteExternValues cex + + baseCaseVals = + Map.filterWithKey + (\(_, offset) _ -> + case offset of + AbsoluteOffset {} -> True + RelativeOffset {} -> False + ) + allExternVals + + inductionStepVals = + Map.filterWithKey + (\(_, offset) _ -> + case offset of + AbsoluteOffset {} -> False + RelativeOffset {} -> True + ) + allExternVals