leventerkok / sbvplugin Goto Github PK

Rewrite sbvPlugin (https://hackage.haskell.org/package/sbvPlugin) using Conal's lambda-ccc (https://github.com/conal/lambda-ccc).

If you can do that, and assuming it works, I think sbvPlugin would become a viable project for people to use in "real life." See this talk by Conal for details: https://www.youtube.com/watch?v=vzLK_xE9Zy8 where he talks about a "Z3" embedding towards the end.

I'd be interested in collaborating on this, if someone takes the charge.

Currently we're not handling newtype casts correctly, the following chokes:

-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module T14 where

import Data.SBV.Plugin

newtype Age = Age Int deriving Eq

{-# ANN f theorem {options = [Verbose, Names ["age"]]} #-}
f :: Age -> Bool
f age@(Age i) = i == i

Yields:

** Starting symbolic simulation..
[SBV] Impossible happened. Got an application with mismatched types: ["== @ Int $fEqInt","age `cast` (NTCo:Age[0] :: Age ~R# Int)"]

This is because we simply "trust" the type of the expression in a cast, instead of actually accepting the new type; we need to thread that through

It appears that the plugins do not see any bindings that are not "exported" from the module; so if you have a theorem binding which is there just for the sake of writing that property (which is usually the case!) then it's not even seen when the plugin runs.

Not usually a problem with GHCi as it "loads" everything in the module (I think), but definitely an issue in compilation.

Need to check with the experts to see if there's a way to reach those names; or otherwise establish a BKM.

Once SBV 7.0 is released, we'll need to upgrade the plugin. Minor changes will be needed, and test outputs will surely differ. But shouldn't be a big deal.

Problem: The default mode for theorem is to find a counterexample of some equation, i.e. a set of inputs to which the result is False.

But I want to find satisfying assignments, i.e. a set of inputs for which the result is True.

Workaround: The easiest way to do this is to invert the clause; that is, if I want to find if any inputs x and y, such that f x y = ... is True, I can write f' x y = not (f x y) and prove that.

Suggestion: It would be nice to have a sat API utility as well as theorem. There are two API points I can think of, regarding what it would look like:

• Should you return the first satisfying assignment, N-many, or all of them?
• What about multiple theorem provers? Do you race all of them until one gives a single satisfying assignment? What if I want every satisfying assignment from every theorem prover?

I'm not sure exactly how you'd like to approach that, but it'd be great to have this!

Following program chokes badly:

{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module T36 where

import Data.SBV.Plugin

{-# ANN f theorem {options = [Verbose,Debug]}#-}
f :: (Int, Int) -> Bool
f (a, b) = (b, a) == (a, b)

The reason is that we have an implicit assumption that the "top-level" entry either has base-types; or they go uninterpreted; with no understanding of tuples there. (Tuples are internally supported, but not at this level.)

Shouldn't be too hard to fix?

A type like [Char] gets properly uninterpred. But String gets uninterpreted in a different way. This is not OK; we should be able to expand type-synonyms somehow. Here's an example program that currently chokes:

{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module T19 where

import Data.SBV.Plugin

{-# ANN f theorem {options=[Verbose]} #-}
f :: String -> Bool
f s = reverse (reverse s) == s

This is trickier; but perhaps we can ask the user to provide a "size" argument as a hint.

Haddock generation is failing again with a bizarre error. (Reminiscent of older issues we had regarding haddock):

 100% ( 11 / 11) in 'Data.SBV.Plugin'

<no location info>: error:
    expectJust getLinkDeps
CallStack (from HasCallStack):
  error, called at compiler/GHC/Data/Maybe.hs:71:27 in ghc:GHC.Data.Maybe
  expectJust, called at compiler/GHC/Linker/Loader.hs:847:28 in ghc:GHC.Linker.Loader

<no location info>: error:
    expectJust getLinkDeps
CallStack (from HasCallStack):
  error, called at compiler/GHC/Data/Maybe.hs:71:27 in ghc:GHC.Data.Maybe
  expectJust, called at compiler/GHC/Linker/Loader.hs:847:28 in ghc:GHC.Linker.Loader

I suspect this is again something to do with Template Haskell; but I'm at a loss ass to what's going on.

Due to nick8325/quickcheck#113; SBV <= 5.13 could be installed with a version of QuickCheck that makes SBV's quick-check only run 1 test in certain cases; which in turn impacts SBVPlugin.

The solution is to bump up version of SBV the plugin depends on to >=5.14; but that cannot really happen till that version of SBV is released. So, this is just a note to do that!

Latest code (modified to "compile" with GHC 9.4.4) has test failures, that I was unable to resolve. For instance tests/T45.hs fails with:

panic! (the 'impossible' happened)
  GHC version 9.4.4:
        lookupIdSubst

foldValid
InScope {}
Call stack:
    CallStack (from HasCallStack):
      callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in ghc:GHC.Utils.Panic
      pprPanic, called at compiler/GHC/Core/Subst.hs:260:17 in ghc:GHC.Core.Subst

Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

I doubt this is a real GHC issue; but rather something I'm doing wrong in the plugin. If you've expertise in how these things work, please help!

For starters, simply let it loop. This is more consistent with how we treat top-level bindings.

The plugin, while it can be useful as is, doesn't really scale in practice. Main problems:

1. Definitions in other modules are not visible
2. It gets utterly confused even with simple uses of polymorphism. Dictionaries in core are hard to track and process correctly. Note that the issue here isn't that we want to support polymorphism: We're completely happy with monomorphic code, but the core we get from GHC has dictionary applications still lying around, which makes the analyzer really complicated. A monomorphising GHC core pass would be most welcome at this point. (And would potentially be useful to other plugins, not just sbv.)
3. It's extremely slow, even when the user is willing to code in a style that avoids the first two problems above. Symbolically simulating the core is tricky due to lots of traversals.

If the plugin is going to see more usage, these problems need to be addressed. Hopefully by someone who is well versed in GHC-core.

Currently, any definition that's not in the current module is simply "uninterpreted" when sbvPlugin runs. This is arguably the right behavior as we're not really targeting a whole-program-analysis tool, but rather small local proofs.

But that stops a little short, since even the prelude isn't there. Basic functions such as take, drop etc. are completely gone; even if we can perfectly reason with (at least some) of these.

Of course, the ramifications can be large: Consider filter: If the predicate is symbolic, then we'll choke soon as we merge: There's just no way to handle that currently. But perhaps a happy medium exists?

Need an example where uninterpreted constant causes proof failure; and so we properly issue a message that this might be the case

Stop simulation at a certain depth (user-specified) if we're that deep into a functions body. Default should be something like 256 perhaps; to support Int/Word8 out of the box without crapping out?

In GHC 9.4 series, integers are represented differently compared to previous versions. It's been hard to decipher exactly how to recognize them. The following is the code I ended up with, which is clearly duck-tape:

We should figure out how to do this properly.

Due to: LeventErkok/sbv#205

fix test T32.hs once the above is fixed in SBV.

I am wondering if it is possible to run this as a doctest tool instead of a GHC plugin? What is the reason for hooking into the GHC pipeline?

The following pgm currently fails:

{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module T24 where

import Data.SBV.Plugin

{-# ANN f theorem {options = [Verbose]} #-}
f :: Int -> Bool
f x =  foo x == x*(x+1) `div` 2
  where -- foo :: Int -> Int
        foo 0 = 0
        foo n = n + foo (n-1)

We get:

[SBV] Counter-example might be bogus due to uninterpreted constants:
  [T24.hs:11:9-11] foo :: Num Int => Int -> Int

Surely, we must recognize Num Int as an available dictionary and do the right thing here. (Not quite sure how though.)

$ cabal new-haddock --haddock-option=--hyperlinked-source --haddock-option=--no-warnings

Haddock coverage:
 100% (  6 /  6) in 'Data.SBV.Plugin.Data'
 100% ( 11 / 11) in 'Data.SBV.Plugin'
haddock: ^^ Could not load '_sbvPluginzm9zi0zi1zminplace_DataziSBVziPluginziPlugin_plugin_closure', dependency unresolved. See top entry above.


GHC.Runtime.Linker.getHValue
During interactive linking, GHCi couldn't find the following symbol:
  sbvPluginzm9zi0zi1zminplace_DataziSBVziPluginziPlugin_plugin_closure
This may be due to you not asking GHCi to load extra object files,
archives or DLLs needed by your current session.  Restart GHCi, specifying
the missing library using the -L/path/to/object/dir and -lmissinglibname
flags, or simply by naming the relevant files on the GHCi command line.
Alternatively, this link failure might indicate a bug in GHCi.
If you suspect the latter, please report this as a GHC bug:
  https://www.haskell.org/ghc/reportabug

cabal: Failed to build documentation for sbvPlugin-9.0.1.

Filed: https://gitlab.haskell.org/ghc/ghc/-/issues/19578, but GHC folks blamed haddock. Then filed haskell/haddock#1369 at the haddock tracker.

We currently only support uninterpreted "Base" values. Need to extend to functions, though it's not clear to me how to go about that ala SBV.. Here's a simple example that currently chokes:

{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module T14 where

import Data.SBV.Plugin

newtype Age = Age Int deriving Eq

{-# ANN f theorem {options = [Verbose]} #-}
f :: Age -> Age -> Bool
f a@(Age i) b@(Age j) = a == b

Gives:

[SBV] bug2.hs:11:1 Skipping proof. Uninterpreted function application:
                      == @ Age $fEqAge
                      a

If the type-signature on foo below is commented out, as we have here, then we end up uninterpreting foo. Is there a way to avoid that?

{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module T24 where

import Data.SBV.Plugin

{-# ANN f theorem {options = [Debug]} #-}
f :: Int -> Bool
f x =  foo x == x
  where -- foo :: Int -> Int
        foo x = x+1