search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

Refactor SBV to provide separate low-level and high-level APIs #124

Closed brianhuffman closed 9 years ago

brianhuffman commented 9 years ago

The high-level interface would be the current Data.SBV API, unchanged.

The low-level interface would be available by e.g. import Data.SBV.Dynamic; it would provide an unparameterized SBV type, a full selection of (non-overloaded) operations on it, and none of the fancy SBV type classes. The high-level SBV a type would be a newtype wrapper around the unparameterized type.

The low-level interface would be a much better fit for applications like Cryptol and the SAW tools where we are dynamically generating terms at runtime. Currently we abuse SBV's interface, making bogus instances for classes like SymWord with some undefined methods, and carefully try to avoid triggering the undefined behavior. Having a low-level API would be much cleaner.

If you're supportive of the idea, I'm more than happy to do all the implementation work.

LeventErkok commented 9 years ago

@brianhuffman Wouldn't it be better to work towards supporting SBV n for arbitrary n? Will GHC 7.10 have enough support for type-literals to become a reality? @yav might provide some input.

I'm not against the idea (especially since you'll do the work), but if "SBV n" is within reach, sticking to that might be the better option here.

yav commented 9 years ago

I really think we should add the dynamic interface. In types like SBV n, n is still a type and needs to be known at compile time, so it is no use to programs that want to generate SBV terms at run-time. One could try to wrap everything in existentials, but this seems like just more hoops to jump through, for little benefit.

The core GHC 7.10 will not be any better at numbers than 7.8.3. One could use my solver, which is now implemented as a compiler plug-in (it is over here https://github.com/yav/type-nat-solver). This would be cool for the "high-level" users of SBV (i.e., when SBV is used as an EDSL in Haskell), but it wouldn't help with Cryptol.

In summary: I think it'd be great if Brian has the time to implement the dynamic interface, and we can wrap the safe EDSL version around that.

LeventErkok commented 9 years ago

Fair enough.. I'd still like the dynamic API to be "discouraged," i.e., just importing Data.SBV shouldn't make it available. Someone should be explicitly importing a module to get this stuff. And eventually we'll have proper support for "SBV n" when GHC is ready for that.

How about we create a new directory, Data/SBV/Internal; move the current module Data.SBV.Internals to that directory, and then create Data.SBV.Internal.Dynamic etc., and put all the modules you need under that directory. Would that work for you Brian? You can still access the under-the-hood stuff by merely importing Data.SBV.Internals.Internal or some such name. Feel free to choose what you think is the best.

yav commented 9 years ago

I agree that the Dynamic API should not be exported by Data.SBV. I'd advocate for exporting the dynamic functionality through Data.SBV.Dynamic though.

I don't like the Internal name much, because the convention followed by other Haskell libraries is that stuff under Internal should not be used, and is very much "may change at any time; use at your own risk".

I don't think that the dynamic API falls in this category: we should view it as a stable (well, eventually) low-level interface, which is to be used by other code that needs to generate terms at run-time.

LeventErkok commented 9 years ago

OK; I'll leave it to you and Brian's judgment, as you guys are the only user of that feature anyhow. Feel free to get rid of Data.SBV.Internals for a better place as well; I'm always in favor of better code organization.

brianhuffman commented 9 years ago

OK, this project is now well underway: I am working on a new branch at https://github.com/brianhuffman/sbv/tree/dynamic

Only a subset of the required functions are available so far; I'll submit a proper pull request once I have something worth merging.

LeventErkok commented 9 years ago

@brianhuffman Are we good to release 4.3? Or do you need some more time?

I think we've enough changes to warrant a release; but if you want to sneak in a few more things let's do that and release by the end of the week?

brianhuffman commented 9 years ago

I think I'd like to sneak in a few more things: Cryptol still relies on a few things exported from Data.SBV and does some casting between SVal and SBool. I want to get wrappers for those functions into Data.SBV.Dynamic before the next release.

brianhuffman commented 9 years ago

With pull request #149 I'm ready for a 4.3 release.

LeventErkok commented 9 years ago

OK; cleaning up some floating-point code. Will release shortly.