Merge remote-tracking branch 'galois/develop-issue495-kind2Prover-falsifiable'. Close #495.

**Description**

`copilot-theorem` crashes when trying to disprove a property that is
false using `kind2Prover`.

`kind2Prover` expects the word used in kind2's XML output to be
`invalid`, but the keyword used is `falsifiable`, leading to a parse
error.

**Type**

- Bug: crash when passing valid input to function.

**Additional context**

None.

**Requester**

- Ryan Scott (Galois)

**Method to check presence of bug**

Attempting to run the following spec with kind2-0.7.2:

```haskell
module Main (main) where

import Data.Functor

import Copilot.Theorem.Kind2
import Copilot.Theorem.Prove
import Language.Copilot

spec :: Spec
spec =
  void $ theorem "false" (forAll false) (check (kind2Prover def))

main :: IO ()
main = void $ reify spec
```

leads to a crash due to a parse error:

```
Spec.hs: Parse error while reading the Kind2 XML output :
Unrecognized status : falsifiable

<?xml version="1.0"?>
<Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<Log class="info" source="parser">kind2 v0.7.2</Log>
<Property name="false">
  <Runtime unit="sec" timeout="false">0.122</Runtime>
  <K>1</K>
  <Answer source="bmc">falsifiable</Answer>
  <Counterexample></Counterexample>
</Property>

</Results>

CallStack (from HasCallStack):
  error, called at src/Copilot/Theorem/Misc/Error.hs:32:9 in copilot-theorem-3.19-CUYLKPoYpZX7ZyknpdGomd:Copilot.Theorem.Misc.Error
```

The following Dockerfile checks that running the above Spec completes
successfully, in which case it prints the message "Success":

```
--- Dockerfile
FROM ubuntu:focal

RUN apt-get update

RUN apt-get install --yes software-properties-common
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update

RUN apt-get install --yes \
  ghc-8.6.5 cabal-install-2.4 \
  libtool-bin libz-dev libzmq5 opam z3

 # Install Kind2's OCaml dependencies
RUN opam init --auto-setup --yes --bare --disable-sandboxing \
 && opam switch create default 4.01.0 \
 && opam install -y -j "$(nproc)" camlp4 menhir \
 && opam clean -a -c -s --logs

 # Install Kind2-0.7.2
ENV KIND2_VER="0.7.2"
RUN wget https://github.com/kind2-mc/kind2/archive/refs/tags/v${KIND2_VER}.zip \
 && unzip v${KIND2_VER}.zip
WORKDIR kind2-${KIND2_VER}
RUN sed -i.bak -e 's/-pedantic -Werror -Wall/-pedantic -Wall/' ocamlczmq/czmq/configure.ac
RUN eval $(opam env) \
 && ./autogen.sh \
 && ./build.sh \
 && make install
WORKDIR /

 # Install GHC and Cabal
ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH

RUN cabal update
RUN cabal v1-sandbox init
RUN apt-get install --yes git

ADD Spec.hs /tmp/Spec.hs

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-install alex happy \
  && cabal v1-install $NAME/copilot**/ \
  && (cabal v1-exec -- runhaskell /tmp/Spec.hs | grep "false: proof failed") \
  && echo "Success"

--- Spec.hs
module Main (main) where

import Data.Functor

import Copilot.Theorem.Kind2
import Copilot.Theorem.Prove
import Language.Copilot

spec :: Spec
spec =
  void $ theorem "false" (forAll false) (check (kind2Prover def))

main :: IO ()
main = void $ reify spec
```

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-495
```

**Expected result**

Running the Dockerfile above prints the message "Success", indicating
that the spec was proven falsifiable using kind2, and that the output
from Copilot contained the text "false: proof failed" (as expected).

**Solution implemented**

Modify `copilot-theorem:Copilot.Theorem.Kind2.Output.parseOutput` to
expect the word `falsifiable`, rather than `invalid`.

**Further notes**

None.

Author: ivanperez-keera

copilot-theorem/CHANGELOG

@@ -1,3 +1,6 @@
+2024-05-05
+        * Fix handling of unsatisfiable properties with Kind2. (#495)
+
 2024-03-07
         * Version bump (3.19). (#504)
 

copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs

@@ -19,9 +19,9 @@ parseOutput :: String    -- ^ Property whose validity is being checked.
 parseOutput prop xml = fromJust $ do
   root <- parseXMLDoc xml
   case findAnswer . findPropTag $ root of
-    "valid"   -> return (Output Valid   [])
-    "invalid" -> return (Output Invalid [])
-    s         -> err $ "Unrecognized status : " ++ s
+    "valid"       -> return (Output Valid   [])
+    "falsifiable" -> return (Output Invalid [])
+    s             -> err $ "Unrecognized status : " ++ s
 
   where