Proposal: get rid of wrapper packages

[facundominguez]

Problem

Verifying a program with liquid haskell requires one to state the assumptions about how dependencies work. The notable exception is when a dependency is also verified with LH, in which case it will contain specifications that can be used to verify the program.

The current mechanism to manage assumptions is to create a Haskell package that states the assumptions (e.g. liquid-base) and then have the program use it instead of the actual package (e.g. base). In order to state the assumptions, Liquid Haskell requires the liquid-base to redefine all the modules of base on which assumptions are needed and reexport all of the other modules. This is a hassle because users need to:

1. change the cabal configuration to replace dependencies by others which are only needed for verification.
2. create wrapper liquid-* packages for every dependency they intend to make assumptions about.
3. keep the wrapper packages up-to-date as new releases of the dependencies pop up.

A solution

I propose that we introduce some changes to LH so we don't need wrapper packages anymore.

A first change is to give LH a mechanism to state reusable assumptions about dependencies without having to redefine Haskell modules only for that sake. In this way, if we want to throw all of the assumptions about a dependency into a single module, we can do it, and moreover, we can do it without having to change the dependency of the program. Making the assumptions reusable means that we can somehow point LH to the module containing the assumptions, and LH will be able to use them in other places.

A second change is to pack inside the LH plugin all of the essential assumptions made for the boot libraries. These libraries depend on the GHC version used, and there is no reason to ask the user to manage the assumptions about boot libraries separately from enabling the LH plugin.

A last change is to allow to configure the LH plugin so it knows where to find the assumptions about dependencies when they are not boot libraries. There are a few options here:

• Use a directive that brings the assumptions from a module and its imports: e.g. {-@ import My.Liquid.Assumptions @-}
• Have LH implicitly load assumptions from a module like Liquid_Dependency_Assumptions and its imports.
• Define some overrideable convention so LH knows to look for assumptions for functions in module M in some other module Liquid.Assumptions.M.

It would be helpful to collect others thoughts on this matter as I'm finding tricky to navigate the design space. Also, I'm not too knowledgeable on how the current LH works, so perhaps there are already solutions which are similar to the proposed changes.

[facundominguez]

@kosmikus @adinapoli if you have any thoughts, they will be appreciated.

[ranjitjhala]

Thanks @facundominguez - I think this is very important! A couple of things

1. (Minor) we use “embed” for something quite different already (to tell fixpoint to interpret certain Haskell types as certain “sorts”).
2. @kosmikus points out that one nice benefit of the wrappers is we get to use cabal directly for managing dependencies; whatever mechanism we want should preserve this property imo.

CURRENTLY in LH we have a way to retroactively slap on specs to package- and module- external functions using the “assume” pragma

module Moo where LJ

assume foo :: T

which says, (if foo is not defined in the module Moo where the above appears), to use T as the signature for foo in that module Moo (only).

IIRC (we can check the code or maybe @adinapoli can recall) these assume are NOT serialized with the module annotations and hence NOT exported by Moo.

Perhaps the solution is to have an

module Moo where

export foo :: T

such that also tells any client of Moo to assume foo :: T

If we do so, then the current liquid-X, packages could be refactored so they only “export” the relevant signature instead of “assume” ing it?

[facundominguez]

If we do so, then the current liquid-X, packages could be refactored so they only “export” the relevant signature instead of “assume” ing it?

If the refactoring implies that liquid-X package doesn't need to redefine the modules in the original package X, it looks like a step forward.

Now we would need to define how a program does bring the exported assumptions into scope. These could be by importing the module with a regular import declaration:

import My.Assumptions.Module()

or by using an import directive,

{-@ import My.Assumptions.Module @-}

when we want to state that a module import is only needed for verification.

Then we need to decide on whether to add a mechanism to reexport assumptions from imports.

(Minor) we use “embed” for something quite different already

👍 I edited this in the description.

... one nice benefit of the wrappers is we get to use cabal directly for managing dependencies; whatever mechanism we want should preserve this property imo.

This makes sense to me, so the user continues to use only one tool to express dependencies between packages.

[nikivazou]

I also agree with @facundominguez's suggestion to get rid of the wrapper packages, for three reasons:

• as a user I prefer my code to depend on base than on liquid-base,
• maintenance and release updates of the liquid-* wrappers ended up being not trivial, and
• I have seen some build problems that refer to these wrappers.

My understanding is that the current solution is close to what we had before, i.e.,

Define and export .spec packages for the libraries.

I believe this seems cleaner.

[nikivazou]

If we do use .spec instead of .hs files for specifications, I believe, we do not need to import-reexport functions.
But I cannot remember if there were other reasons we replaced the .spec files.

So, currently, my suggestion is to 1) define the type signatures in spec files and 2) use annotations to import them.
I am happy to discuss this more.

[facundominguez]

But I cannot remember if there were other reasons we replaced the .spec files.

In that case, perhaps we can use .spec files for boot libraries. However, I think spec files won't solve the problem for other libraries.

For instance, suppose we have LH assumptions about functions in package vector and we put them in spec files. Where would these spec files reside? We can't put them in a liquid-vector package, because we are trying to get rid of this package to begin with.

The options are either putting the assumptions in the vector package itself, or putting them elsewhere to be defined. Assuming we sometimes will want to put assumptions elsewhere, we would need to spell out how does Liquid Haskell find them.

[facundominguez]

2. use annotations to import them.

Import annotations can tell which spec file is needed, but I don't think they can say where in the system the file is located.

[facundominguez]

The following assumption about A.f seems to be exported.

module A where
f :: Int
f = 1

module B where
import A(f)
{-@ assume A.f :: { z:Int | z > 0 } @-}
{-@ g :: { z:Int | z > 0 } @-}
g :: Int
g = f

module C where
import A
import B() -- needed only for the assumption about A.f
{-@ h :: { z:Int | z > 0 } @-}
h :: Int
h = f

Importing B in module C is necessary for verification to succeed. I couldn't find any differences in behavior when putting the assumption in a .spec file. The key change determining if the assumption is exported or not, is whether the identifier in the assume directive appears qualified or not. Thus, it looks like we already have some of the behavior that we need.

If I introduce conflicting assumptions about f, then the prevailing assumption varies, but perhaps we could deal with this in a separate issue.

[nikivazou]

I agree that the problem is where to put the annotations. Ideally we want them in the package (e.g., vector) but that is not totally up to us :) In the past, we had them in Liquid Haskell's include directory, which looked ok to me. The final option is the current liquid-* package, which in theory seems more modular.

[facundominguez]

While investigating solutions, I realized that there is a design choice to make.

The problem is to bring assumptions into scope that are not provided in the imports of the module being verified.

1. Implicit assumptions We can go for bringing assumptions implicitly into scope. This can be done by looking at import declarations to decide what assumptions to bring. Say, if the module imports Prelude or Data.List, these imported modules are from base which doesn't provide assumptions, but LH would automatically bring into scope from elsewhere the assumptions about list functions. Because the assumptions may not be useful in all situations, we also need to have a mechanism to override them or stop them from being brought implicitly; or

2. Explicit assumptions We ask the user to be explicit about which assumptions to bring. Imagine that liquid-base only offers modules that bring assumptions, like Prelude_LHAssumptions and Data.List_LHAssumptions and the user of liquid Haskell must explicitly import any of those modules in order to bring their assumptions into scope.

The answer to this question could be different depending on whether we are talking about boot libraries, or whether we are talking about other libraries of which LH is unaware at build time.

---

I like option (2) the most because it gives the user the most control with the simplest means. We still will need to have liquid-* packages to hold assumptions, but they hold no tight connection to the module hierarchy of the wrapped packages.
The downside is that LH users need to care about manually bringing the assumptions, but I think this is a modest verification cost to pay when using libraries that don't use the LH plugin.

Option (1) doesn't require manually importing assumptions, but it has the risk of bloating the environment with unnecessary assumptions and measures, and it could introduce disrupting assumptions too. Moreover, any mechanism to import assumptions implicitly seems to impose some burden on authors of assumptions as in the following explanation.

In order to decide which assumptions to bring into scope, LH would look at the import declarations of the module being verified. Suppose there is an import declaration like import A.B.C where module A.B.C is provided by a Haskell library abc. The assumptions to bring depend on the version of abc in use, as different version might provide different functions and types. Moreover, the modules of abc might be renamed on different version, and the author of implicit assumptions would have to keep up with it. Also, as in the case of Prelude, definitions might come from transitively imported modules, the user could import either top-level or specialized modules, and therefore the author of implicit assumptions also needs to keep up with changes in the transitive imports of a library.

---

With respect to the current situation, both options save the trouble of editing the cabal configuration to replace base with liquid-base and similarly for other packages. Both options avoid the trouble of reexporting modules that don't need assumptions in wrapped packages.

Only option (2) saves the trouble of dealing with changes in the module hierarchy across versions of a dependency that needs assumptions.

Any preferences?

[ranjitjhala]

I prefer (1) at least for the "prelude" and similar because without implicitly loading the assumptions for stuff like + and head and such, all the existing LH code will break (as in will "trivially" typecheck, as there will be no contracts to check them against :-)) That is, a user will not know which assumptions to implicitly include to get some meaningful checking on their code.

Perhaps the solution is some mixture. So

• some modules (e.g. those in the LH prelude/current liquid-* get loaded implicitly
• other modules can be explicitly opt-in (and maybe if they prove very useful, they can be "upgraded" to implicit?

[facundominguez]

I started moving spec files from liquid-ghc-prim and liquid-base to the data files of the package liquidhaskell. While this is likely to work in the end, it does require maintaining a separate mechanism for processing these spec files.

Today I was struck by another approach: merge the assumptions of the liquid-* packages into a single package, that also rexports the plugin. Let's call this package liquidhaskell-final.

Users of lh need only depend on liquidhaskell-final, and LH will know to load the assumptions in the interface files of the appropriate modules in liquidhaskell-final based on the imports needed by the module being verified. Suppose a module imports Data.List, LH will look for assumptions in the interface file of liquidhaskell-final:Data.List_LHAssumptions.

The advantage of this approach is that it could be reused for boot and non-boot libraries. Whenever a module imports module M, LH can look for assumptions in some module M_LH in the direct dependencies of the current package.

Thoughts welcome.
🤔

[facundominguez]

After #2166 and #2170, I think we can consider this issue addressed.