copilot-theorem: Make the kind2 connection handle both existentially and universally quantified properties correctly

Description

Copilot.Language.Spec.prop and Copilot.Language.Spec.theorem are both reified into as a bare stream of booleans, and do not retain information about whether the Prop passed as argument was a Forall or an Exists. This makes the use of the Kind2 connection in copilot-theorem render incorrect results.

Type

Bug: Information is lost, leading to unexpected results .

Additional context

Issue copilot-theorem: Make What4 backend refuse to prove existentially quantified properties #254 will introduce enough information in streams to know which quantifier has been used, and adjust the What4 connection to use the information accordingly and refuse to prove properties that it cannot prove. The scope of this ticket is how to use that information, once available, to ensure that copilot-theorem produces correct results when Kind2 is used.

Requester

Rob Dockins.

Method to check presence of bug

The issue can be detected with the following sample programs:

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

Expected result

Running the specs above or a similar variant via Kind2 should print proof checked successfully as part of its output if it can prove a theorem true, and proof failed otherwise, indicating that respects the quantifier is being respected. For the cases above, t1 should be falsified, but t2 should succeed.

If the prover is not able to prove a property of a given type, a suitable error message should be printed.

Desired result

Running the specs above or a similar variant via Kind2 should print proof checked successfully as part of its output if it can prove a theorem true, and proof failed otherwise, indicating that respects the quantifier is being respected. For the cases above, t1 should be falsified, but t2 should succeed.

If the prover is not able to prove a property of a given type, a suitable error message should be printed.

Proposed solution

Modify copilot-theorem to properly use the information about the which quantifier was used, and translate it appropriately before sending it to Kind2.

Further notes

None.

Now that the groundwork has been laid in #596 (the fix for #254), I'd like to work on fixing this issue.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

@RyanGlScott

Technical Lead: Issue scheduled for fixing in Copilot 4.4.

Fix assigned to: @RyanGlScott .

Implementor: Solution implemented, review requested.

copilot-theorem: Add Props to specProps. Refs Copilot-Language#594.

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

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

copilot-theorem: Add Props to specProps. Refs Copilot-Language#594.

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

copilot-theorem: Document changes in CHANGELOG. Refs Copilot-Language…

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.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-kind2-respect-quantifiers-T594'. Close Copilot-…

Navigation Menu

Repository navigation

`copilot-theorem`: Make the kind2 connection handle both existentially and universally quantified properties correctly #594

5 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-theorem: Make the kind2 connection handle both existentially and universally quantified properties correctly #594

Description

Activity

RyanGlScott commented on Mar 7, 2025

ivanperez-keera commented on Mar 26, 2025

ivanperez-keera commented on Mar 26, 2025

ivanperez-keera commented on Mar 26, 2025

5 remaining items

RyanGlScott commented on Mar 27, 2025

ivanperez-keera commented on Apr 19, 2025

ivanperez-keera commented on Apr 19, 2025

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-theorem`: Make the kind2 connection handle both existentially and universally quantified properties correctly #594