Merge branch 'develop-test-what4'. Close #474.

**Description**

As part of the requirements for Class D (NPR7150.2C), we need unit tests
for all of copilot.

A natural next step is to introduce the testing infrastructure for
`copilot-theorem`.

**Type**

- Management: conformance with new requirement.

**Additional context**

None.

**Requester**

- Ivan Perez

**Method to check presence of bug**

The following Dockerfile checks that copilot-theorem's tests can be
executed, in which case it prints the message Success:
```
FROM ubuntu:focal

RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc make libgmp3-dev g++

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.4.7
RUN ghcup install cabal 3.8
RUN ghcup set ghc 9.4.7
RUN cabal update

RUN apt-get install --yes z3

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd copilot-theorem && \
    cabal test copilot-theorem:unit-tests && \
    echo Success
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-474
```

**Expected result**

The library `copilot-theorem` includes tests for `what4`. Introducing
(some classes of) errors in the implementation of `copilot-theorem`
makes the tests detect those errors.

Running the docker file above prints the message success, indicating
that copilot-theorem now declares a unit-tests component.

**Proposed solution**

Add tests for `copilot-theorem` that test basic properties whose result
is known with one of the existing solver.

The tests focus on What4, the Z3 solver, and only 3 properties. The goal
is to introduce enough infrastructure that testing the What4 connection
more thoroughly should be reduced to adding more properties to the
now-existing test module.

**Further notes**

Due to the magnitude of this change, we decide to simplify the issue in
three ways:
- Focus only on `what4`, which is likely going to replace other ways of
  connecting to SMT solvers provided by `copilot-theorem`.
- Focus only on one of the SMT solvers.
- Focus only on the core of the infrastructure, leaving it to a future
  issue to have a more comprehensive list of properties.

Author: ivanperez-keera

.travis.yml

@@ -15,6 +15,11 @@ before_install:
   - travis_retry sudo add-apt-repository -y ppa:hvr/ghc
   - travis_retry sudo apt-get update
   - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER # see note about happy/alex
+
+  # We install z3 only for the tests, since it is not needed for normal
+  # compilation.
+  - if [ "${GHCVER}" == "8.10.4" ]; then travis_retry sudo apt-get install --yes z3; fi
+
   - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
   - cabal --version
   - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
@@ -27,4 +32,7 @@ script:
   # Run tests only on GHC 8.10.4
   #
   # Only libraries with tests are listed below or the v2-test command fails.
-  - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99; fi
+  #
+  # Testing copilot-theorem requires z3. See above conditional installation,
+  # and keep GHC version numbers in both places in sync.
+  - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99 copilot-theorem; fi

copilot-theorem/CHANGELOG

@@ -1,3 +1,6 @@
+2023-12-18
+        * Introduce testing infrastructure for Copilot.Theorem.What4. (#474)
+
 2023-11-07
         * Version bump (3.17). (#466)
         * Relax version constraint on what4. (#461)

copilot-theorem/copilot-theorem.cabal

@@ -108,3 +108,31 @@ library
                           , Copilot.Theorem.TransSys.Type
 
                           , Copilot.Theorem.What4.Translate
+
+test-suite unit-tests
+  type:
+    exitcode-stdio-1.0
+
+  main-is:
+    Main.hs
+
+  other-modules:
+    Test.Copilot.Theorem.What4
+
+  build-depends:
+      base
+    , QuickCheck
+    , test-framework
+    , test-framework-quickcheck2
+
+    , copilot-core
+    , copilot-theorem
+
+  hs-source-dirs:
+    tests
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall

copilot-theorem/tests/Main.hs

@@ -0,0 +1,18 @@
+-- | Test copilot-theorem.
+module Main where
+
+-- External imports
+import Test.Framework (Test, defaultMain)
+
+-- Internal imports
+import qualified Test.Copilot.Theorem.What4
+
+-- | Run all unit tests on copilot-theorem.
+main :: IO ()
+main = defaultMain tests
+
+-- | All unit tests in copilot-theorem.
+tests :: [Test.Framework.Test]
+tests =
+  [ Test.Copilot.Theorem.What4.tests
+  ]

copilot-theorem/tests/Test/Copilot/Theorem/What4.hs

@@ -0,0 +1,108 @@
+-- The following warning is disabled due to a necessary instance of SatResult
+-- defined in this module.
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | Test copilot-theorem:Copilot.Theorem.What4.
+module Test.Copilot.Theorem.What4 where
+
+-- External imports
+import Data.Int                             (Int8)
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Property, arbitrary, forAll)
+import Test.QuickCheck.Monadic              (monadicIO, run)
+
+-- External imports: Copilot
+import           Copilot.Core.Expr      (Expr (Const, Op2))
+import           Copilot.Core.Operators (Op2 (..))
+import           Copilot.Core.Spec      (Spec (..))
+import qualified Copilot.Core.Spec      as Copilot
+import           Copilot.Core.Type      (Typed (typeOf))
+
+-- Internal imports: Modules being tested
+import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove)
+
+-- * Constants
+
+-- | Unit tests for copilot-theorem:Copilot.Theorem.What4.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Theorem.What4"
+    [ testProperty "Prove via Z3 that true is valid"    testProveZ3True
+    , testProperty "Prove via Z3 that false is invalid" testProveZ3False
+    , testProperty "Prove via Z3 that x == x is valid"  testProveZ3EqConst
+    ]
+
+-- * Individual tests
+
+-- | Test that Z3 is able to prove the following expression valid:
+-- @
+--   constant True
+-- @
+testProveZ3True :: Property
+testProveZ3True =
+    monadicIO $ run $ checkResult Z3 propName spec Valid
+  where
+    propName :: String
+    propName = "prop"
+
+    spec :: Spec
+    spec = propSpec propName $ Const typeOf True
+
+-- | Test that Z3 is able to prove the following expression invalid:
+-- @
+--   constant False
+-- @
+testProveZ3False :: Property
+testProveZ3False =
+    monadicIO $ run $ checkResult Z3 propName spec Invalid
+  where
+    propName :: String
+    propName = "prop"
+
+    spec :: Spec
+    spec = propSpec propName $ Const typeOf False
+
+-- | Test that Z3 is able to prove the following expresion valid:
+-- @
+--   for all (x :: Int8), constant x == constant x
+-- @
+testProveZ3EqConst :: Property
+testProveZ3EqConst = forAll arbitrary $ \x ->
+    monadicIO $ run $ checkResult Z3 propName (spec x) Valid
+  where
+    propName :: String
+    propName = "prop"
+
+    spec :: Int8 -> Spec
+    spec x = propSpec propName $
+      Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
+
+-- | Check that the solver's satisfiability result for the given property in
+-- the given spec matches the expectation.
+checkResult :: Solver -> String -> Spec -> SatResult -> IO Bool
+checkResult solver propName spec expectation = do
+  results <- prove solver spec
+
+  -- Find the satisfiability result for propName.
+  let propResult = lookup propName results
+
+  -- The following check also works for the case in which the property name
+  -- does not exist in the results, in which case the lookup returns 'Nothing'.
+  return $ propResult == Just expectation
+
+-- * 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]
+
+-- | Equality for 'SatResult'.
+--
+-- This is an orphan instance, so we suppress the warning that GHC would
+-- normally produce with a GHC option at the top.
+instance Eq SatResult where
+  Valid   == Valid   = True
+  Invalid == Invalid = True
+  Unknown == Unknown = True
+  _       == _       = False

copilot/CHANGELOG

@@ -1,3 +1,6 @@
+2023-12-18
+        * Enable tests for copilot-theorem in CI script. (#474)
+
 2023-11-07
         * Version bump (3.17). (#466)
         * Replace uses of deprecated functions. (#457)