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:

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

  • 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
  

• Implementation is documented. Details:
  No updates needed.
• 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 not needed (bug fix).