Liquid Fixpoint

This package implements a Horn-Clause/Logical Implication constraint solver used for various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar to:

Requirements

In addition to the .cabal dependencies you require an SMTLIB2 compatible solver binary:

If on Windows, please make sure to place the binary and any associated DLLs somewhere in your path.

How To Build and Install

Simply do:

git clone https://github.com/ucsd-progsys/liquid-fixpoint.git
cd liquid-fixpoint
stack install

or (cabal instead of stack if you prefer.)

Using SMTLIB-based SMT Solvers

You can use one of several SMTLIB2 compliant solvers, by:

fixpoint --smtsolver=z3 path/to/file.hs

Currently, we support

* Z3
* CVC4
* MathSat

Configuration Management

It is very important that the version of Liquid Fixpoint be maintained properly.

Suppose that the current version of Liquid Haskell is A.B.C.D:

After a release to hackage is made, if any of the components B, C, or D are missing, they shall be added and set to 0. Then the D component of Liquid Fixpoint shall be incremented by 1. The version of Liquid Fixpoint is now A.B.C.(D + 1)
The first time a new function or type is exported from Liquid Fixpoint, if any of the components B, or C are missing, they shall be added and set to 0. Then the C component shall be incremented by 1, and the D component shall stripped. The version of Liquid Fixpoint is now A.B.(C + 1)
The first time the signature of an exported function or type is changed, or an exported function or type is removed (this includes functions or types that Liquid Fixpoint re-exports from its own dependencies), if the B component is missing, it shall be added and set to 0. Then the B component shall be incremented by 1, and the C and D components shall be stripped. The version of Liquid Fixpoint is now A.(B + 1)
The A component shall be updated at the sole discretion of the project owners.

It is recommended to use the Bumper utility to manage the versioning of Liquid Fixpoint. Bumper will automatically do the correct update to the cabal file. Additionally, it will update any packages that you have the source for that depend on Liquid Fixpoint.

To update Liquid Fixpoint and Liquid Haskell, first clone Liquid Haskell and Liquid Fixpoint to a common location:

git clone https://github.com/ucsd-progsys/liquidhaskell.git
git clone https://github.com/ucsd-progsys/liquid-fixpoint.git

To increment the D component of Liquid Fixpoint:

./path/to/bumper -3 liquid-fixpoint

This will update the D component of Liquid Fixpoint. If necessary, this will update the Build-Depends of Liquid Haskell. If the Build-Depends was updated, Liquid Haskell's D component will be incremented.

To increment the C component of Liquid Fixpoint, and strip the D component:

./path/to/bumper --minor liquid-fixpoint

As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell.

To increment the B component of Liquid Fixpoint, and strip the D and C components:

./path/to/bumper --major liquid-fixpoint

As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell

SMTLIB2 Interface

There is a new SMTLIB2 interface directly from Haskell:

Language.Fixpoint.SmtLib2

See tests/smt2/{Smt.hs, foo.smt2} for an example of how to use it.

Options

--higherorder allows higher order binders into the environment

--extsolver runs the deprecated external solver.

--parts Partitions an FInfo into a [FInfo] and emits a bunch of files. So:

$ fixpoint -n -p path/to/foo.fq

will now emit files:

path/to/.liquid/foo.1.fq
path/to/.liquid/foo.2.fq
. . .
path/to/.liquid/foo.k.fq

and also a dot file with the constraint dependency graph:

path/to/.liquid/foo.fq.dot

FInfo Invariants

Binders

This is the field

     , bs       :: !BindEnv         -- ^ Bind  |-> (Symbol, SortedReft)

or in the .fq files as

bind 1 x : ...
bind 2 y : ...

Each BindId must be a distinct Int,
Each BindId that appears in a constraint environment i.e. inside any IBindEnv must appear inside the bs

Environments

Each constraint's environment is a set of BindId which must be defined in the bindInfo. Furthermore
Each constraint should not have duplicate names in its environment, that is if you have two binders

  bind 1 x : ...
  bind 12 x : ...

Then a single IBindEnv should only mention at most one of 1 or 12.

There is also a "tree-shape" property that its a bit hard to describe ... TODO

LHS

Each slhs of a constraint is a SortedReft.

Each SortredReft is basically a Reft -- a logical predicate. The important bit is that a KVar i.e. terms of the formalized

     $k1[x1:=y1][x2:=y2]...[xn:=yn]

That is represented in the Expr type as

  | PKVar  !KVar !Subst

must appear only at the top-level that is not under any other operators, i.e. not as a sub-Expr of other expressions.

This is basically a predicate that needs to be "well sorted" with respect to the BindId, intuitively

    x:int, y:int |- x + y : int

is well sorted. but

    x:int  |- x + y : int

is not, and

    x:int, y: list |- x + y : int

is not. The exact definition is formalized in Language.Fixpoint.SortCheck

RHS

Similarly each rhs of a SubC must either be a single $k[...] or an plain $k-free Expr.

Global vs. Distinct Literals

     , gLits    :: !(SEnv Sort)               -- ^ Global Constant symbols
     , dLits    :: !(SEnv Sort)

The global literals gLits are symbols that are in scope everywhere i.e. need not be separately defined in individual environments. These include things like

uninterpreted measure functions len, height,
uninterpreted data constructor literals True, False

Suppose you have an enumerated type like:

data Day = Sun | Mon | Tue | Wed | ... | Sat

You can model the above values in fixpoint as:

constant lit#Sun : Day
constant lit#Mon : Day
constant lit#Tue : Day
constant lit#Wed : Day

The distinct literals are a subset of the above where we want to tell the SMT solver that the values are distinct i.e. not equal to each other, for example, you can additionally specify this as:

distinct lit#Sun : Day
distinct lit#Mon : Day
distinct lit#Tue : Day
distinct lit#Wed : Day

The above two are represented programmatically by generating suitable Symbol values (for the literals see litSymbol) and Sort values as FTC FTycon and then making an SEnv from the [(Symbol, Sort)].

Sorts

What's the difference between an FTC and an FObj?

In early versions of fixpoint, there was support for three sorts for expressions (Expr) that were sent to the SMT solver:

int
bool
"other"

The FObj sort was introduced to represent essentially all non-int and non-bool values (e.g. tuples, lists, trees, pointers...)

However, we later realized that it is valuable to keep more precise information for Exprs and so we introduced the FTC (fixpoint type constructor), which lets us represent the above respectively as:

FTC "String" [] -- in Haskell String
FTC "Tuple" [FInt, Bool] -- in Haskell (Int, Bool)
FTC "List" [FTC "List" [FInt]] -- in Haskell [[Int]]

There is a comment that says FObj's are uninterpretted types; so probably a type the SMT solver doesn't know about? Does that then make FTC types that the SMT solver does know about (bools, ints, lists, sets, etc.)?

The SMT solver knows about bool, int and set (also bitvector and map) but all other types are currently represented as plain Int inside the SMT solver. However, we will be changing this to make use of SMT support for ADTs ...

To sum up: the FObj is there for historical reasons; it has been subsumed by FTC which is what I recomend you use. However FObj is there if you want a simple "unitype" / "any" type for terms that are not "interpreted".

Qualifier Patterns

λ> doParse' (qualParamP sortP) "" "z as (mon . $1) : int"
QP {qpSym = "z", qpPat = PatPrefix "mon" 1, qpSort = FInt}
λ> doParse' (qualParamP sortP) "" "z as ($1 . mon) : int"
QP {qpSym = "z", qpPat = PatSuffix 1 "mon", qpSort = FInt}
λ> doParse' (qualParamP sortP) "" "z as mon : int"
QP {qpSym = "z", qpPat = PatExact "mon", qpSort = FInt}
λ> doParse' (qualParamP sortP) "" "z : int"
QP {qpSym = "z", qpPat = PatNone, qpSort = FInt}

jprider63/liquid-fixpoint