copilot `copilot-theorem`: `kind2Prover` gives parse error when disproving a property

(In order to reproduce this bug, you'll need to install Kind2-0.7.2, which is (as far as I can tell) the latest version of Kind2 that copilot-theorem currently supports. Note that Kind2-0.7.2 doesn't offer binary distributions, so you'll have to build it from source.)

copilot-theorem's kind2Prover is able to prove properties that are true. For instance, running this program:

module Main (main) where

import Data.Functor

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

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

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

Will yield:

(define-pred top
  ((prop-true.out Bool))
  (init
    (= prop-true.out true))
  (trans
    (= (prime prop-true.out) true)))

(check-prop
  ((true prop-true.out)))
true: valid ()
Finished: true: proof checked successfully

On the other hand, if kind2Prover attempts to disprove a property that is false, then it will crash with a parse error. This can be seen when running this program:

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

(define-pred top
  ((prop-false.out Bool))
  (init
    (= prop-false.out false))
  (trans
    (= (prime prop-false.out) false)))

(check-prop
  ((false prop-false.out)))
Main.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.135</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.18.1-inplace:Copilot.Theorem.Misc.Error

The problem lies in this code:

https://github.com/Copilot-Language/copilot/blob/835deafa4727c60741337a84cf7b8dce705f6e41/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs#L19-L24

This expects Kind2's XML output to have an <Answer>...</Answer> tag whose content is the string invalid. As can be seen in the XML output that is dumped in the error message above, however, the actual content of the <Answer> tag is falsifiable.

Resolving this issue would be helpful in an eventual resolution for #254. In order to check an existentially quantified property with Kind2, it would be convenient to take a universally quantified property and negate it, checking if Kind2 returns falsifiable as the answer. This won't be possible unless we first fix this issue.

Jan 12 '24 15:01 RyanGlScott

The following Dockerfile checks that theorem correctly reports that a property is unsatisfiable using the Kind2 backend:

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

Run the Dockerfile like so:

$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=f8239019b9c83315a78e2a92221b862945aa3b7c" -it copilot-theorem-495

This fails as of commit f8239019b9c83315a78e2a92221b862945aa3b7c:

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

Apr 22 '24 22:04 RyanGlScott

Thank you, @RyanGlScott .

Apr 23 '24 08:04 ivanperez-keera

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:

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

Expected result

Running the spec above should complete correctly, and produce an output that contains the text "false: proof failed", since the property we are attempting to prove is falsifiable.

Desired result

Running the spec above should complete correctly, and produce an output that contains the text "false: proof failed", since the property we are attempting to prove is falsifiable.

Proposed solution

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

Further notes

None.

Apr 24 '24 15:04 ivanperez-keera

Change Manager: Confirmed that the bug exists.

Apr 24 '24 17:04 ivanperez-keera

Technical Lead: Confirmed that the issue should be addressed.

Apr 24 '24 17:04 ivanperez-keera

Technical Lead: Issue scheduled for fixing in Copilot 3.20.

Fix assigned to: @RyanGlScott .

Apr 24 '24 17:04 ivanperez-keera

Implementor: Solution implemented, review requested.

Apr 24 '24 17:04 RyanGlScott

In the past, we sometimes involved George Hagan with Kind2 issues. He created Kind and is still in touch with the Iowa guys.

On Wed, Apr 24, 2024 at 1:14 PM Ryan Scott @.***> wrote:

Implementor: Solution implemented, review requested.

— Reply to this email directly, view it on GitHub https://github.com/Copilot-Language/copilot/issues/495#issuecomment-2075449433, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAONILT3MZWEAEDGVNOZRCDY67R7ZAVCNFSM6AAAAABBYKG5OKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANZVGQ2DSNBTGM . You are receiving this because you are subscribed to this thread.Message ID: @.***>

-- Alwyn E. Goodloe, Ph.D. @.***

Research Computer Engineer NASA Langley Research Center

Apr 24 '24 20:04 agoodloe

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).

May 07 '24 14:05 ivanperez-keera

Change Manager: Implementation ready to be merged.

May 07 '24 14:05 ivanperez-keera