`copilot-theorem`: Look for `falsifiable` (not `invalid`). Refs #495.

[RyanGlScott]

In Kind2-0.7.2, disproven properties are tagged with falsifiable in the XML output, but the code in copilot-theorem's Kind2 backend was instead searching for a tag named invalid. As a result, copilot-theorem would error when attempting to disprove properties that are false, as it fail to parse the XML output. This fixes the issue by replacing invalid with falsifiable.

Fixes #495.

[ivanperez-keera]

Change Manager:

• Could you please drop commit db60ae7? We'll review how to document that dependency separately.
• Could you please fix up df857e5 with 226a108 ?
• Could you please adjust the CHANGELOG and the commit messages to not include the specific version number of kind2?

[RyanGlScott]

I've implemented your suggestions—please take a look.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

  • [X] The code proposed compiles and passes all tests. Details: Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/270315105

  • [X] The solution proposed produces the expected result. Details: The following Dockerfile uses the kind2 backend to check that a false stream is falsifiable, 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/GaloisInc/copilot-1" -e "NAME=copilot-1" -e "COMMIT=b153fbc2231ad33862d2b7a94986f0a90bf501f9" -it copilot-verify-495

• [X] Implementation is documented. Details: No updates needed.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed.
• [X] Required version bumps are evaluated. Details: Bump not needed (bug fix).