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

[RyanGlScott]

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

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

Lines 19 to 24 in 835deaf

	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

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.

[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 f823901:

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

[ivanperez-keera]

Thank you, @RyanGlScott .

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

[ivanperez-keera]

Change Manager: Confirmed that the bug exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 3.20.

Fix assigned to: @RyanGlScott .