copilot-theorem: Translate quantifiers correctly in Kind2 backend. Refs #594.

[RyanGlScott]

copilot-theorem's Kind2 backend takes a proposition and attempts to prove that it is valid at all possible time steps. Currently, this happens regardless of whether the proposition is universally or existentially quantified. This is unsound, and it can lead to valid, existentially quantified properties being incorrectly labeled as invalid.

This commit fixes the translations of propositions to Kind2 (via Kind2's TransSys backend) such that the translated properties respect quantifier information. Specifically, this replaces an unsound use of the extractProp function with an analysis that translates the property differently depending on whether it is universally or existentially quantified. Because all TransSys propositions use universal quantification, we convert an existentially quantified property ∃x.P(x) as ¬(∀x.¬(P(x))) during the translation to TransSys.

Fixes #594.

[ivanperez-keera]

Change Manager: Please see the comments above regarding alignment.

[RyanGlScott]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Please rebase branch wrt. the latest master.

[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://app.travis-ci.com/github/Copilot-Language/copilot/builds/274932248
  • The solution proposed produces the expected result. Details:
    The following Dockerfile uses the kind2 backend to Copilot spec to try to prove a universal and an existential property, and checks that the result reported by copilot-theorem matches the expectation, after which it prints the message "Success":

    --- Dockerfile-verify-594
    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 repository add archive git+https://github.com/ocaml/opam-repository-archive \
     && 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 -e "t1: proof failed" -e "t2: proof checked successfully") \
      && echo "Success"
    
    --- Spec.hs
    {-# LANGUAGE NoImplicitPrelude #-}
    module Main (main) where
    
    import Data.Functor
    
    import Copilot.Theorem.Kind2
    import Copilot.Theorem.Prove
    import Language.Copilot
    
    trueThenFalses :: Stream Bool
    trueThenFalses = [True] ++ constant False
    
    spec :: Spec
    spec = do
      void $ theorem "t1" (forAll trueThenFalses) (check (kind2Prover def))
      void $ theorem "t2" (exists trueThenFalses) (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=3b51c969d863755431cb628de80bc02e0c243a8d copilot-verify-594
    

• Implementation is documented. Details:
  The code is documented and changes to top-level definitions are adjusted where 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 required; change fixes a bug but does not affect public API.