Input File Format Specification

[MichaReiser]

Hy everyone

I'm trying to create a simple liquid haskell implementation for the simple lambda calculus as a student project (to explain refinement types to other). As I' unfamiliar with SMT solvers I want to delegate the constraint solving to liquid-fixpoint.

Exists there any documentation how an input file needs to be build up that liquid fixpoint can solve fit?

Thanks... Micha

[ranjitjhala]

@Hi @DatenMetzgerX,

This is an excellent idea! I have been wanting to create such a tutorial for a while.

The main entry is in Liquid.Fixpoint.Solver which exports:

1. solve which solves a query given as an FInfo (defined in Liquid.Fixpoint.Types),
2. solveFQ which runs the fixpoint binary on a .fq file.

For now, I recommend you use the second option solveFQ. You can also just run the fixpoint binary directly on a .fq file, this is easiest as you don't have to understand all the invariants needed to build an FInfo.

To see what an .fq file looks like, take a look at the tests directory

For example, in tests/pos/test1.fq we have

1. one k-variable $k0 that must be given a refinement that is well-formed with respect to the empty environment (i.e. can only contain the free variable v).
2. three subtyping constraints involving $k0

// This qualifier saves the day; solve constraints WITHOUT IT
qualif Zog(v:a) : (10 <= v)

bind 0 x : {v : int | v = 10}
bind 1 y : {v : int | v = 20}
bind 2 a : {v : int | $k0    }

constraint:
  env [0]
  lhs {v : int | v = x}
  rhs {v : int | $k0   }
  id 1 tag []

constraint:
  env [1]
  lhs {v : int | v = y}
  rhs {v : int | $k0   }
  id 2 tag []

constraint:
  env [2]
  lhs {v : int | v = a  }
  rhs {v : int | 10 <= v}
  id 3 tag []

wf:
  env [ ]
  reft {v : int | $k0}

If you run

$ stack exec --  fixpoint test1.fq --save

then you get:

Safe
rjhala@borscht ~/r/s/l/t/pos (develop)> more .liquid/test1.fq.fqout 

Solution:
$k0 := 10 <= v

If instead, you change the "binding" (definition) for x to:

bind 0 x : {v : int | v = 9}

see tests/neg/test1.fq

then you get:

Unsafe:
WARNING: 3
rjhala@borscht ~/r/s/l/t/neg (develop) [1]> more .liquid/test1.fq.fqout 

Solution:
$k0 := true

Does this help?

Please let me know what other things are unclear -- I've been wanting to put together a tutorial of the sort you describe, and so this will be a great forcing function!

Thanks!

[MichaReiser]

Thanks @ranjitjhala I will take a look on Wednesday. My writing will mostly be based on your excellent liquid types paper and your talk at Microsoft Research in July, 2008. My goal is to create something less formal then your liquid types paper that is easier to understand by non type system experts like me.

So if I understand this correct. wf stands for the Well Formedness Constraints. Bindings are created for each variable / expression. This already looks amazing... now I can verify if I have generated the right constraints (and understood your paper.)

[MichaReiser]

Hy Ranjit

Actually, I still have some further questions. Overall, I think I have a good understanding but as soon as I start with the implementation, the little details start to creep out.. To start, I want to shortly summarize the basics to ensure that I have no misunderstanding with these basic concepts.

Symbols As I understand, there are two kind of symbols. At one hand, there are the symbols from the lexical scope (variables). At the other hand, there are the liquid type variables. However, Liquid Type variables can correspond with symbols defined in the lexical scope (and even have to).

Template According to my understanding, a template consists of a base type (Shape S) and a predicate (e).

Constraint / Predicate A constraint is just a logical expression that is only using qualifiers defined by liquid haskell.

Substitution Substituting [e/x] means that x is replaced by e. Here it is unclear to me what substitution in this context means. Does this actually mean that the (constraint) expression of x is replaced by e or is just the liquid variabe x renamed to e?

I started with a simple lambda calculus parser, HM Type Checker and Liquid type inference / type checking. The application (written in Java) uses the fixpoint binary for constraint solving. My current goal is to verify a quite simple program for a start

test = let x = 0 in 10 / x

that maps to the following program in the simple lambda calculus (assume infix operators are supported)

let x = 0 in 10 / x

I used liquid haskell to generated the expected fq file for the given program. The relevant constraints and bindings for the given program are (quite many, I hope I did not truncate any other essential constraints)

bind 4 x##aly : {lq_tmp$x##36 : real | [(lq_tmp$x##36 = 0.0)]}
bind 5 lq_anf$##1677724084##dE4 : {lq_tmp$x##42 : real | [(lq_tmp$x##42 = 10.0)]}
bind 6 Main.test##rjG : {VV##60 : real | []}
bind 7 VV##61 : {VV##61 : real | [(VV##61 = (lq_anf$##1677724084##dE4 / x##aly));
                                  (VV##61 = (lq_anf$##1677724084##dE4 / x##aly))]}
bind 8 VV##63 : {VV##63 : real | [(VV##63 = 0.0);
                                  (VV##63 = x##aly)]}
bind 9 VV##65 : {VV##65 : real | [(VV##65 = 10.0);
                                  (VV##65 = lq_anf$##1677724084##dE4)]}
bind 10 VV##67 : {VV##67 : real | [(VV##67 = 10.0)]}
bind 11 VV##69 : {VV##69 : real | [(VV##69 = 0.0)]}

constraint:
  env [0; 1; 2; 3; 4; 5]
  lhs {VV##F##1 : real | [(VV##F##1 = 0.0); (VV##F##1 = x##aly)]}
  rhs {VV##F##1 : real | [(VV##F##1 != 0); (VV##F##1 != 0.0)]}
  id 1 tag [1]
  // META constraint id 1 : ()

Here I noticed that I need some further details about the file and maybe even have some missunderstanding with the concepts.

1. I expected that each template is over the liquid type variable v. But in the given output, all bindings seem to have there own instance of v. Why are the predicates not just over v?
2. Why is there a need for generating bindings for sub expressions. Is there a way to avoid these. I expect that explaining the behavior might be simpler if the constraints of the sub expressions are directly inlined?
3. [(VV##F##1 = 0.0); (VV##F##1 = x##aly)]: Is the semantics of ; defined as and? Why does it not refer to binding 8 and instead inlines the constraint?
4. The output for the given example is RESULT: Unsafe [Just 1]. How is the result to be interpreted. Unsafe makes sense. But What information holds Just 1? Refers the 1 to the constraint with the tag 1?
5. Why are no wf constraints generated. According to the liquid types paper, let in generates one wf and one subtyping constraint.

Some further, but example independent questions

1. Is there a possibility to define a constraint whose rhs is something like {v: int | true }. Right now i have to eliminate such subtyping constraints, but it might be helpful for understanding to see that these constraints are actually generated (even if they are obvious to solve).
2. What would the program of the original program of tests/pos/test1.fq look like?
3. One last question to your original Liquid Types paper: In figure 4 (Liquid Type Inference Algorithm) for the case of a variable / an identifier. There is a distinction whatever the inferred type of HM equals B. When should this not be the case? As I understand it, a new Template is created when the variable x is not yet in the type environment, otherwise the template from the type environment is returned. However, when should x not be in the type environment? If it is declared, then the abstraction or let in rule ensure that the variable is defined, otherwise HM should fail as a not declared variable is used?
4. For branch specific Type Environments: Is the branch specific condition just encoded as AND condition into the lhs of a constraint?

Sorry for those many questions. The concept seems easy to understand at a first glance but there are many details when looked into in more detail. If you do not have the time to answer the question, don't bother. I can switch my paper topic to just explain liquid types and what the great benefits of it are. However, I'm personally more interested in why is it working, because there are already many great tutorials from you explaining how refinement types can be used.

Anyway, thank you a lot and I'm very interested in seeing where liquid types are going in the future (maybe even supporting imperative languages)!

Micha

PS:

What my program currently generates for the given program is

bind 0 x : {v: int | v = 0 }

bind 1 temp0 : {v: int | v = 10 }

constraint:
  env [1; 0]
  lhs {v : int | v = 0}
  rhs {v : int | x /= 0}
  id 0 tag []

constraint:
  env [1; 0]
  lhs {v : int | v = temp0 / x}
  rhs {v : int | $k1}
  id 1 tag []

wf:
  env []
  reft {v : int | $k1}

I'm not sure if the constraint 0 is valid, shouldn't it be v /= 0.

[MichaReiser]

Hy Ranjit

I think I'm a little bit further. I tried to analyze the max function:

let max = x -> y -> if > x y then x else y in max 12 23

The generated constraints are (without wf constraints)

bind 0 x : {v: int | $k2 }

bind 1 y : {v: int | $k3 }

bind 2 max : {v: (func(1, [(int (func(1, [(int int)])))])) | $k1 }

constraint:
  env [0; 1]
  lhs {v : int | [$k2 ; x > y]}
  rhs {v : int | $k1}
  id 0 tag []

constraint:
  env [0; 1]
  lhs {v : int | [$k3 ; (not x > y)]}
  rhs {v : int | $k1}
  id 1 tag []

constraint:
  env [0; 1]
  lhs {v : int | $k1}
  rhs {v : int | $k1}
  id 2 tag []

constraint:
  env [0]
  lhs {v : int | $k3}
  rhs {v : (func(1, [(int int)])) | $k1}
  id 3 tag []

constraint:
  env [2]
  lhs {v : int | v = 10}
  rhs {v : int | $k2}
  id 4 tag []

constraint:
  env [2]
  lhs {v : int | v = 12}
  rhs {v : int | $k3}
  id 5 tag []

constraint:
  env [2]
  lhs {v : int | $k1}
  rhs {v : int | $k1}
  id 6 tag []

The result is, as expected, safe. However, Liquid-Fixpiont doesn't give me any solutions for $k1. Why not?

[ranjitjhala]

Hi (sorry for the delay!),

there are a couple of things.

1. You need to define "wellformedness" constraints that essentially define the "scope" of each $k, for example, you need something like:

wf:
  env [] 
  reft {v:int | $k1}

wf:
  env [] 
  reft {v:int | $k2}

wf:
  env [] 
  reft {v:int | $k3}

1. Even after that you will get "SAFE" and no output, because the constraints are "trivially" safe, as there is no constraint with a "rhs" that is a predicate. Consequently, the system just computes the trivial solution "TRUE" for all the $k. Suppose your code was instead:

let max = x -> y -> if x > y then x else y in 
  assert (max 12 23 > 0)

then you should get the above plus the extra constraint:

constraint: 
  env []
  lhs {v: int | $k1 } 
  rhs {v: int | v > 0 }
  id 7

If you run it now, you will get the output:

Unsafe:
WARNING: 7

meaning that the constraint 7 is UNSAT using the strongest solution over the qualifiers.

This is because the set of qualifiers is empty (none have been given in the file) so the computed solution is (saved in .liquid/file.fq.fqout run with --save to get it)

rjhala@borscht ~/r/s/l/t/pos (develop) [1]> more .liquid/bob.fq.fqout 

Solution:
$k3 := true

$k2 := true

$k1 := true

To address this, lets add some qualifiers to the file, for example:

qualif Gt0(v:int): v >= 0
qualif Gt10(v:int):  v >= 10
qualif Gt12(v:int): v >= 12

After this, you get:

$ stack exec -- fixpoint bob.fq --save 
...

Safe

and furthermore, you can look at the solution:

$ more .liquid/bob.fq.fqout 

Solution:
$k3 := v >= 12
       && v >= 10
       && v >= 0

$k2 := v >= 0
       && v >= 10

$k1 := v >= 0
       && v >= 10

Does this help?

[MichaReiser]

This may actually help a lot. I never was sure for what the qualifiers are in liquid-fixpoint. So if I understand this correctly, there are no built in qualifiers Q. I need to define those myself. And instead of * (star) constraint, i can just define an arbitrary symbol, e.g. x, like it is done in the Cmp qualifier. So if I want to build up on your paper I can just define all qualifiers of Q.

qualif Cmp(v : @(0), x : @(0)): ((v != x))

[ranjitjhala]

That is correct! In the paper we write * but in the tool we just use named parameters, so exactly as you say above. (x instead of *).

[MichaReiser]

Hy Ranjit

I'm actually making progress and was capable to create all needed constraints for

let avgspeed = s t => s / t in avgspeed 100 2

qualif CmpZ(v:a): (0 <= v)
qualif CmpZ(v:a): (v != 0)
qualif Cmp(v:a, x:a): (x < v)
qualif Cmp(v:a, x:a): (v <= x)

bind 0 s : {v: int | $ks }
bind 1 t : {v: int | $kt }
bind 2 res: {v: int | $kres}
bind 3 let: {v: int| $klet}

wf:
  env []
  reft {v : int | $ks}

wf:
  env [0]
  reft {v : int | $kt}

wf:
  env [0; 1]
  reft {v : int | $kres}

wf:
  env []
  reft {v : int | $klet}

constraint:
  env [0; 1]
  lhs {v : int | v = s/t}
  rhs {v : int | $kres}
  id 1 tag []

constraint:
  env [0; 1]
  lhs {v : int | $kt}
  rhs {v : int | v != 0}
  id 2 tag []

constraint:
  env []
  lhs {v : int | v = 100}
  rhs {v : int | $ks}
  id 3 tag []

constraint:
  env []
  lhs {v : int | v = 2}
  rhs {v : int | $kt}
  id 4 tag []

constraint:
  env [2]
  lhs {v : int | $kres[s:=100][t:=2]}
  rhs {v : int | $klet}
  id 5 tag []

$kres = return value of the avgspeed function.$klet type of the let body.

If i run fixpoint against the given file I get the desired solution for $ks and $kt

Safe

Solution:
$kt := v /= 0
       && 0 <= v

$ks := v /= 0
       && 0 <= v

However, I never get a type for $klet or $kres?

I also tried to solve the constraints by hand --- actually I did quite well --- however the following embeddings are unclear to me:

avgspeed:Fspeed |- {v:int | v = 2} <: {v:int | $kt}

The type of avgspeed is a template-function over $ks -> $kt -> $kres. What is the correct embedding assuming that A($ks)=0<=v, v!=0 and A($kt)=0<=v, v!=0, v<=s, s<v

(0<=s ^ s!=0 ^ 0<=t ^ t!=0 ^ t<=s ^ s< t ^ v=2) => q

or do neither embed $ks nor $kt since they are not explicitly in the environment

v=2 => q

For the later case it is unclear to me how to verify if the qualifiers containing s are evaluated. In this case no constraints exists for s and Z3 can pick an arbitrary value for s (than the qualifier q is always true and the implication always holds).

A similar question arises for the embedding of

s:Fs; t:Ft |- {v:int|$kt} <: {v:int|v!=0}

As t is in the environment, the current solution needs to be added to the embedding

(0<=s ^ s!=0 ^ 0<=t ^ t!=0 ^ t<=s ^ s< t ^ q) => v!=0 

However, q itself is again one of the qualifiers from t. And besides, the embedding of the type environment contains a contradiction (t<=s ^ s < t) and therefore is never true (implication holds for all qualifiers).

Should the embedding instead be

(0<=s ^ s!=0 ^ q) => v!=0 

In this case the qualifiers 0<=v, v!=0 and s<v hold. However, s<v is not a valid qualifier in the solution of liquid fixpoint (and therefore should not be SAT?)

If i know how to test if the qualifiers are satisfying a given constraint i may actually complete my paper (that will still need a lot of rework but I should have the content after all).

Again, Thank you very much. Micha

[ranjitjhala]

Hi @DatenMetzgerX,

1. The reason that $klet and $kres get "no solution" is that they are "sliced away" since they do not appear in any left-hand-side (actually, anywhere), consequently, you can pretty much assign them ANY refinement and it doesn't affect the solution.
2. Re: avgspeed since it is a function and as it does not appear in any solution (unless I missed something) you can "embed" it either as:

bind 4 avgspeed: {v: func(0, [int; int; int] | [] }

and then add the bind 4 to your env in the constraint id 4.

Func(0, [int; int; int]) which means a monomorphic function 0 type variables that takes two int and returns an int OR better, just don't put it in anywhere since you can't actually use functions in refinements (unless they are "measures" -- see our ICFP 2014 paper for an explanation of that.)

Thus, the way you would embed

avgspeed:Fspeed |- {v:int | v = 2} <: {v:int | $kt}

is via a constraint id 4 exactly as you have done right now...

Does that make sense?

[MichaReiser]

Ok thank you. Good that I got it write... Than only the other two questions about the embedding (when solving by hand) are still open

1. The embedding of avgspeed:Fspeed |- {v:int | v = 2} <: {v:int | $kt} is

v = 2 => q

where q is a qualifier that should be tested from A($kt). Is the reason for throwing the qualifier v<=s away that s is not in the environment?

1. Testing the qualifiers for s:Fs; t:Ft |- {v:int|$kt} <: {v:int|v!=0}: Is the current solution for $kt$ embedded into implication or only the qualifiers one by one.

E.g. To we test for

(0<=s ^ s!=0 ^ 0<=t ^ t!=0 ^ t<=s ^ s< t ^ q) => v!=0 
|------------|-------------------------|
        s                               t

Or simply

(0<=s ^ s!=0 ^ q) => v!=0 
|------------|
        s      

where t is not embedded into the test as we trying to find the qualifiers for t.

I just want to be sure that I get this write and explain the reason for throwing a qualifier away is correct.

Thank you Ranjit

My resolving looks like this

[MichaReiser]

Thanks Ranjit for your Feedback.

I think that I now understand the input format.