copilot-theorem: Reject existentially quantified propositions in What4 backend. Refs #254.

[RyanGlScott]

The functions in Copilot.Theorem.What4 (e.g., prove) take a proposition and attempt to prove that it is valid at all possible time steps. Currently, these functions do this regardless of whether the proposition is universally quantified
or existentially quantified, which is unsound. The reason that this happens is because the functions call extractProp on the proposition being proven, causing the proposition's quantifier not to be taken into account.

This commit removes the unsound uses of extractProp and instead checks if the proposition was actually quantified universally (i.e., with a Forall), which is the intended use case for Copilot.Theorem.What4. If the proposition was instead quantified existentially (i.e., with an Exists), then a ProveException will be thrown. Warnings have been added to Haddocks of the relevant functions that can potentially throw a ProveException.

Fixes #254.

[ivanperez-keera]

Change Manager: CI job fails. Please check.

[RyanGlScott]

Sigh, newer GHCs appear not to require the GADTs extension for code that older GHCs do require it for. Let me try again...

[RyanGlScott]

This is quite bizarre. The GHC 8.10.4 CI build fails with the following:

Linking /home/travis/build/Copilot-Language/copilot/dist-newstyle/build/x86_64-linux/ghc-8.10.4/copilot-core-4.2/t/unit-tests/build/unit-tests/unit-tests ...
Running 1 test suites...
Test suite unit-tests: RUNNING...
Copilot.Core.Type:
  <snip>
  transitivity of equality of simple types: [Failed]
<snip>

         Properties  Total 
 Passed  32          32    
 Failed  1           1     
 Total   33          33    
Test suite unit-tests: FAIL
Test suite logged to:
/home/travis/build/Copilot-Language/copilot/dist-newstyle/build/x86_64-linux/ghc-8.10.4/copilot-core-4.2/t/unit-tests/test/copilot-core-4.2-unit-tests.log
0 of 1 test suites (0 of 1 test cases) passed.
cabal: Tests failed for test:unit-tests from copilot-core-4.2.

The output does not give me any indication of why the transitivity of equality of simple types test failed, nor does it give me a seed to pass to QuickCheck to allow me to reproduce the failure. What's more, if I try running the copilot-core unit tests locally, then all of the tests pass. I'm not sure what to make of this, as it seems very unlikely that my changes would have impacted this part of copilot-core.

[ivanperez-keera]

Change Manager: Please rebase on top of the latest commit on master.

[RyanGlScott]

Thankfully, restarting the CI appears to have fixed the test suite issues observed earlier.

[RyanGlScott]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Please see the reviews and comments above.

[RyanGlScott]

Please see the reviews and comments above.

Which review comments in particular are you referring to?

[ivanperez-keera]

Change Manager: Please address the change requests / comments below.

[RyanGlScott]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: @RyanGlScott Please rebase on top of the latest master, review the new comments, split the commit that affects multiple libraries into one commit per library with the appropriate summary line indicating the library affected, and rephrase the commit messages to avoid the use of Previously.

[RyanGlScott]

Implementor: Fix implemented, review requested.

[RyanGlScott]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    Build log: https://github.com/Copilot-Language/copilot/runs/38305999192
  • The solution proposed produces the expected result. Details:
    The following Dockerfile runs the prover on a Copilot spec that proves an existential, which produces an exception caught by the program (as expected), after which it prints the message "Success". If an exception is not caught, the program exits with an error code.

    --- Dockerfile-verify-254
    FROM ubuntu:focal
    
    ENV DEBIAN_FRONTEND=noninteractive
    RUN apt-get update
    
    RUN apt-get install --yes \
          libz-dev \
          git \
          curl \
          gcc \
          g++ \
          make \
          libgmp3-dev  \
          pkg-config \
          z3
    
    RUN mkdir -p $HOME/.ghcup/bin
    RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -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/
    
    SHELL ["/bin/bash", "-c"]
    
    RUN ghcup install ghc 9.10.1
    RUN ghcup install cabal 3.2
    RUN ghcup set ghc 9.10.1
    RUN cabal update
    
    ADD What4Existential.hs /tmp/What4Existential.hs
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
      && cabal v1-sandbox init \
      && cabal v1-install alex happy --constraint='happy <= 2' \
      && cabal v1-install $NAME/copilot**/ \
      && cabal v1-exec -- runhaskell /tmp/What4Existential.hs \
      && echo "Success"
    
    --- What4Existential.hs
    {-# LANGUAGE NoImplicitPrelude   #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    module Main (main) where
    
    import Control.Exception ( SomeException, handle )
    import Data.Foldable     ( forM_ )
    import Data.Functor      ( void )
    import System.Exit       ( exitFailure, exitSuccess )
    
    import Copilot.Theorem.What4
    import Language.Copilot
    
    main :: IO ()
    main = do
      handle (\(_ :: SomeException) -> exitSuccess) $ do
        proveSpec specF
        proveSpec specE
        putStrLn "The What4 backend tried to prove an existential proposition"
      exitFailure
    
    proveSpec :: Spec -> IO ()
    proveSpec spec = do
      spec' <- reify spec
      results <- prove Z3 spec'
      forM_ results $ \(nm, res) -> do
        putStr $ nm <> ": "
        case res of
          Valid   -> putStrLn "valid"
          Invalid -> putStrLn "invalid"
          Unknown -> putStrLn "unknown"
    
    specF :: Spec
    specF = void $
      prop "forAll trueThenFalses (should be invalid)" (forAll trueThenFalses)
    
    specE :: Spec
    specE = void $
      prop
        "exists trueThenFalses (shouldn't have a known result)"
        (exists trueThenFalses)
    
    trueThenFalses :: Stream Bool
    trueThenFalses = [True] ++ constant False
    

    Command (substitute variables based on new path after merge):

    $ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=700508abfcefea5c59517e0bdc3087735fdaa692 copilot-verify-254
    

• Implementation is documented. Details:
  All new top-level constructs include documentation, modules document the expected result when proving an existential, and new code includes additional comments.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No updates needed.
• Required version bumps are evaluated. Details:
  Bump needed; the prove function can now produce an exception.