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

[robdockins]

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?

[ivanperez-keera]

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?

[robdockins]

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.

[RyanGlScott]

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.

[RyanGlScott]

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.

[ivanperez-keera]

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.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.3.

Fix assigned to: @RyanGlScott .

[RyanGlScott]

Implementor: Solution implemented, review requested.