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 Expr
s 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}