copilot 4.2 → 4.3
raw patch · 4 files changed
+144/−12 lines, 4 filesdep +containersdep ~basedep ~copilot-c99dep ~copilot-corenew-component:exe:what4-arithmetic-counterexamplesPVP ok
version bump matches the API change (PVP)
Dependencies added: containers
Dependency ranges changed: base, copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem
API changes (from Hackage documentation)
Files
- CHANGELOG +7/−0
- README.md +7/−5
- copilot.cabal +20/−7
- examples/what4/ArithmeticCounterExamples.hs +110/−0
CHANGELOG view
@@ -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)
README.md view
@@ -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:
copilot.cabal view
@@ -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
+ examples/what4/ArithmeticCounterExamples.hs view
@@ -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