copilot-theorem: Make What4 backend refuse to prove existentially quantified properties

Looking at the datatypes involved in the high-level and low-level Spec datatypes (e.g. SpecItem), it seems to me that properties and theorems are both represented as a bare stream of booleans. It strikes me as odd that we don't retain information about which quantifier was used to state the property, as it makes it impossible later to determine what semantics where intended; in particular, the quantifier for the property is not passed to the askProver method of Copilot.Theorem.Prove.prove, which strikes me as very strange. Am I missing something here?

I'm with you. I was also confused.

But I don't see how Spec could have a quantifier to give theorems a stream-based interpretation that also has operational meaning in online RV.

What do you suggest?

I think the current stream-based interpretation is fine, as long as we also remember the associated quantifier. I don't know that I would necessarily expect a run-time interpretation of these properties, but they are certainly an important distinction when proving properties about a spec. It's important not to assume an existential property as though it is universal (which is unsound); and the proof techniques one can use for universal properties are different than for existential (induction vs model checking).

In principle, one could interpret a universal property as a safety property and monitor it, but the trigger mechanism already basically does that.

Here is a test case that demonstrates the issue:

{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Data.Foldable
import Data.Functor

import Copilot.Theorem.What4
import Language.Copilot

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False

spec :: Spec
spec = do
  void $ prop "forAll trueThenFalses (should be invalid)" (forAll trueThenFalses)
  void $ prop "exists trueThenFalses (should be valid)" (exists trueThenFalses)

main :: IO ()
main = do
  spec' <- reify spec
  results <- prove Z3 spec'
  forM_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"

As its name suggests, exists trueThenFalses (should be valid) should yield valid, but it instead yields invalid. I suspect this is happening because Copilot is dropping the existential quantifier and incorrectly treating the underlying stream as though it were universally quantified.

Here is the Kind2 equivalent of the program above:

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

$ PATH=~/Software/kind2-0.7.2/bin:$PATH runghc Bug.hs
(define-pred top
  ((prop-t1.out Bool)
   (prop-t2.out Bool)
   (s0.out Bool)
   (s0.out.1 Bool))
  (init
    (and
      (= prop-t1.out s0.out)
      (= prop-t2.out s0.out)
      (= s0.out true)
      (= s0.out.1 false)))
  (trans
    (and
      (= (prime prop-t1.out) (prime s0.out))
      (= (prime prop-t2.out) (prime s0.out))
      (= (prime s0.out) s0.out.1)
      (= (prime s0.out.1) false))))

(check-prop
  ((t2 prop-t2.out)))
t2: invalid ()
Finished: t2: proof failed
(define-pred top
  ((prop-t1.out Bool)
   (prop-t2.out Bool)
   (s0.out Bool)
   (s0.out.1 Bool))
  (init
    (and
      (= prop-t1.out s0.out)
      (= prop-t2.out s0.out)
      (= s0.out true)
      (= s0.out.1 false)))
  (trans
    (and
      (= (prime prop-t1.out) (prime s0.out))
      (= (prime prop-t2.out) (prime s0.out))
      (= (prime s0.out) s0.out.1)
      (= (prime s0.out.1) false))))

(check-prop
  ((t1 prop-t1.out)))
t1: invalid ()
Finished: t1: proof failed
Warning: failed to check some proofs.

Both the t1 and t2 proofs fail, but t2 ought to succeed.

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. Because this information is not retained when later using Copilot.Theorem.Prove.prove to check the properties, the results returned by the SMT solvers may be incorrect.

Type

Bug: Information is lost, leading to unexpected results .

Additional context

None.

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.Foldable
import Data.Functor

import Copilot.Theorem.What4
import Language.Copilot

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False

spec :: Spec
spec = do
  void $ prop "forAll trueThenFalses (should be invalid)" (forAll trueThenFalses)
  void $ prop "exists trueThenFalses (should be valid)" (exists trueThenFalses)

main :: IO ()
main = do
  spec' <- reify spec
  results <- prove Z3 spec'
  forM_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"

Expected result

Running the specs above or a similar variant via What4 should yield valid when the property is indeed valid (the second property above), indicating that respects the quantifier is being respected.

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

Desired result

Running the specs above or a similar variant via What4 should yield valid when the property is indeed valid (the second property above), indicating that respects the quantifier is being respected.

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

Proposed solution

Modify copilot-language:Copilot.Language.Spec to carry enough information about the quantifier used, and either use the information to ensure a proper encoding of the property when connecting to the SMT-solver, or have the backend refuse to prove the property when the result would be incorrect.

Further notes

None.

Preserve proposition quantifiers in copilot-core. Refs Copilot-Langua…

copilot-theorem: Reject existentially quantified propositions in What…

copilot-core: Document changes in CHANGELOG. Refs Copilot-Language#254.

copilot-language: Document changes in CHANGELOG. Refs Copilot-Languag…

copilot-prettyprinter: Document changes in CHANGELOG. Refs Copilot-La…

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

copilot-language: Document changes in CHANGELOG. Refs Copilot-Languag…

copilot-prettyprinter: Document changes in CHANGELOG. Refs Copilot-La…

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

copilot-theorem: Reject existentially quantified propositions in What…

copilot-core: Document changes in CHANGELOG. Refs Copilot-Language#254.

copilot-language: Document changes in CHANGELOG. Refs Copilot-Languag…

copilot-prettyprinter: Document changes in CHANGELOG. Refs Copilot-La…

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://github.com/Copilot-Language/copilot/runs/38305999192

The solution proposed produces the expected result. Details:
The following Dockerfile runs the prover on a Copilot spec that proves an existential, which produces an exception caught by the program (as expected), after which it prints the message "Success". If an exception is not caught, the program exits with an error code.

--- Dockerfile-verify-254
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config \
      z3

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.10.1
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.10.1
RUN cabal update

ADD What4Existential.hs /tmp/What4Existential.hs

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install $NAME/copilot**/ \
  && cabal v1-exec -- runhaskell /tmp/What4Existential.hs \
  && echo "Success"

--- What4Existential.hs
{-# LANGUAGE NoImplicitPrelude   #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main (main) where

import Control.Exception ( SomeException, handle )
import Data.Foldable     ( forM_ )
import Data.Functor      ( void )
import System.Exit       ( exitFailure, exitSuccess )

import Copilot.Theorem.What4
import Language.Copilot

main :: IO ()
main = do
  handle (\(_ :: SomeException) -> exitSuccess) $ do
    proveSpec specF
    proveSpec specE
    putStrLn "The What4 backend tried to prove an existential proposition"
  exitFailure

proveSpec :: Spec -> IO ()
proveSpec spec = do
  spec' <- reify spec
  results <- prove Z3 spec'
  forM_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"

specF :: Spec
specF = void $
  prop "forAll trueThenFalses (should be invalid)" (forAll trueThenFalses)

specE :: Spec
specE = void $
  prop
    "exists trueThenFalses (shouldn't have a known result)"
    (exists trueThenFalses)

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False

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=700508abfcefea5c59517e0bdc3087735fdaa692 copilot-verify-254

Implementation is documented. Details:
All new top-level constructs include documentation, modules document the expected result when proving an existential, and new code includes additional comments.
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 needed; the prove function can now produce an exception.

Change Manager: Implementation ready to be merged.

Merge branch 'develop-what4-respect-quantifiers-T254'. Close Copilot-…

Merge branch 'develop-kind2-respect-quantifiers-T594'. Close #594.

Navigation Menu

Repository navigation

`copilot-theorem`: Make What4 backend refuse to prove existentially quantified properties #254

50 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

copilot-theorem: Make What4 backend refuse to prove existentially quantified properties #254

Description

Activity

ivanperez-keera commented on Sep 21, 2021

robdockins commented on Sep 21, 2021

RyanGlScott commented on Jan 8, 2024

RyanGlScott commented on Nov 15, 2024

ivanperez-keera commented on Jan 29, 2025

50 remaining items

ivanperez-keera commented on Mar 7, 2025

ivanperez-keera commented on Mar 7, 2025

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copilot-theorem`: Make What4 backend refuse to prove existentially quantified properties #254