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

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.

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

Thank you, @RyanGlScott .

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.

Change Manager: Confirmed that the bug exists.

Technical Lead: Confirmed that the issue should be addressed.

Technical Lead: Issue scheduled for fixing in Copilot 3.20.

Fix assigned to: @RyanGlScott .

Implementor: Solution implemented, review requested.

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 <#495 (comment)>, 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

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

Change Manager: Implementation ready to be merged.

	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