Help with a verified implementation of a queue (really #580)

[nikswamy]

Simon Sini asks on fstar-club:

" Hi there, my name is Simon and im an undergraduate student at the university of Milan, Italy. I've just approached fstar in last few weeks and i've followed the tutorial, even though, i have to admit, I found the second part of it pretty tough. In order to practice and get a little bit more familiar with the language i decided to write a verified Queue module, using the usual functional implementation with 2 lists: one for the front and the other for the back. I know that's probabaly very basic but unfortunately i found myself in trouble with some part of the code, expecially with the remove function. So I was wondering if, posting my code or giving a link of the file on GitHub (better i guess), someone could help me out with it. Let me know if that's ok please and i will give the code. Thank's everyone in advance. Wish you all a nice day. Regards. Simon "

And

"Hello there, hope all is good with everyone of you!! My name is Simon, As I mentioned in a previous mail, I'm a bit struggling with a verified implementation of a queue. This is the link to my code : https://github.com/simosini/FStar/blob/master/Queues.fst Problems and doubts I'm having are fully explained in the comments. Any help or suggestion will be much appreciated. Many thanks in advance. Regards. Simon "

[nikswamy]

About this question in the code https://github.com/simosini/FStar/blob/master/Queues.fst

If I change this to:
type queue 'a =
  | Q : #n1:nat -> #n2:nat{n2 <= n1} -> front:sList 'a n1 -> back:sList 'a n2 -> queue 'a
that is I just moved the refinment from the back list to #n2, it does accept the emptyQ
declaration but it wont verify the makeQ function (written later)

This is an unfortunate, but known issue. See #580 and our plan to fix it by moving to a 2-phase type-checker: https://github.com/FStarLang/FStar/wiki/A-roadmap-for-F*

[nikswamy]

Indeed, the troubles you're facing in this file are all due to this annoying #580 issue.

Here's an edited version of your file that verifies.

module Queues

(* Queue implementation Okasaki's style: 2 lists,
   the front list which represents the front of the queue where to retrieve elements,
   the back list, kept reversed, which represents the back of the queue.
   As suggested by Okasaki I impose the invariant on the size of the 2 lists :
   the front size must not be smaller than the back one.
   http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp95queue.pdf
*)

(* As implemented in fstar/example/data_structures/Vector.fst *)
type sList 'a : nat -> Type =
  | Nil  : sList 'a 0
  | Cons : hd:'a -> #n:nat ->  sList 'a n -> sList 'a (n+1)

(* Im trying to provide examples all over the file to double-check im doing right *)

let okSl1 = Cons 2 Nil
let okSl2 = Nil 
let okSl3 = Cons 1 okSl1

(* A function to retrieve the carried size of the list *)

val size : #a:Type -> #n:nat -> sList a n -> Tot nat
let size #a #n _ = n 

let okSize   = assert (size okSl1 = 1) //accepted
//let badSize  = assert (size okSl3 = 3) should be 2 so not accepted (OK)
let okSize2 = assert (size okSl3 = 2) //accepted

(* We now need a couple of functions to retrieve the elements of the list. *)

(* n must be pos cause we dont allow the call of hd and tl on empty lists *)

val hd : #a:Type -> #n:nat -> sl:sList a n{n > 0} -> Tot a
let hd #a #n sl = match sl with
  | Cons h _ -> h

//let el1 = hd Nil not accepted (OK)
let el2 = hd okSl1 //accepted

val tl : #a:Type -> #n:nat -> sl:sList a n{n > 0} -> Tot (sList a (n-1))
let tl #a #n sl = match sl with
  | Cons _ rest -> rest

// let badTl = tl Nil not accepted (OK)
let okTl  = tl okSl1 //accepted

(* reverse and append needed for the remove and insert operations on the queue *)

val append : #a:Type -> #n1:nat -> #n2:nat -> 
             sList a n1 -> sList a n2 ->
             Tot(sList a (n1+n2))
let rec append #a #n1 #n2 sl1 sl2 = match sl1 with
  | Nil         -> sl2
  | Cons h rest -> Cons h (append rest sl2)

val reverse : #a:Type -> #n:nat -> sList a n -> 
              Tot(sList a n)
let rec reverse #a #n sl = match sl with
  | Nil         -> Nil 
  | Cons h rest -> append (reverse rest) (Cons h Nil)

let okReverse = assert (reverse okSl3 = Cons 2 (Cons 1 Nil)) //accepted
//let badReverse = assert (reverse okSl1 = Nil) not accepted (OK)

(* Let's now give a queue type made up of 2 sized Lists imposing that the size of the
first list (the front of the queue) is never smaller than the second one (the back) *)

(* Important Note!!! The type given  after this comment  doesn't accept the binding
let emptyQ = Q Nil Nil 
but verifies the makeQ function.
If I change this to:
type queue 'a =
  | Q : #n1:nat -> #n2:nat{n2 <= n1} -> front:sList 'a n1 -> back:sList 'a n2 -> queue 'a
that is I just moved the refinment from the back list to #n2, it does accept the emptyQ
declaration but it wont verify the makeQ function (written later)
*)
type queue 'a =
  | Q : #n1:nat -> #n2:nat -> front:sList 'a n1 -> back:sList 'a n2{n2 <= n1} -> queue 'a

//let emptyQ = Q Nil Nil not accepted but it should
let okQ = Q okSl1 Nil //accepted
// let badQ = Q Nil okSl1 not accepted the first list is shorter (OK)

(* In order to transfer the element from the back to the front we give a rotate function.
Mind that this function is only called when the front list is one element smaller than the
back so as the re-balance them. The refinment {n2 > n1 ==> n2 = n1 + 1} is needed for the 
makeQ function and it's explained in the next comment. What i actually need though is proving
that rotate is actually called only when size back = size front + 1, but with this refinment
the makeQ function wouldn't work.

****************************Question: How can I do that???? **********************)

val rotate : #a:Type -> #n1:nat -> #n2:nat ->
             f:sList a n1 -> b:sList a n2{n2 > n1 ==> n2 = n1 + 1} -> Tot (sList a (n1 + n2))
let rotate #a #n1 #n2 f b = append f (reverse b)

(* Let's now implement a queue constructor in charge of preserving the invariant.
The makeQ function is called after every operation on the queue.
Note that by using n2:nat{n2 > n1 ==> n2 = n1 + 1} what I would like to say is : 
IF the back list is bigger the front than it can only have 1 element more than it.
Otherwise ,that is if n1 happens to be bigger or equal to n2,  then n1 and n2 can have any nat value.
****************** Question: Is that true? How can I impose that otherwise? **************)

val qSize : queue 'a -> Tot nat
let qSize (Q f b) = size f + size b 

let okqSize = assert (qSize okQ = 1) // accepted
// let badqSize = assert (qSize okQ = 2) not accepted (OK)

val makeQ : #a:Type -> #n1:nat -> #n2:nat ->
            f:sList a n1 -> b:sList a n2{n2 > n1 ==> n2 = n1 + 1} -> Tot (q:queue a{qSize q = n1 + n2})
let makeQ #a #n1 #n2 f b =
  if n1 < n2  then Q (rotate f b) Nil
  else Q f b

(* recall that : okSl1 = [2] ; okSl3 = [1;2] ; okSl2 = [] *)
let okMakeQ1 = assert (Q (Cons 2(Cons 2(Cons 1 Nil))) Nil = makeQ okSl1 okSl3) 
let okMakeQ2 = assert (Q (Cons 1(Cons 2 Nil)) (Cons 2 Nil) = makeQ okSl3 okSl1) 
// let okMakeQ3 = assert (Q Nil Nil = makeQ okSl2 okSl2) //not accepted but it should 

(* Ok now the 2 main operations on the queue : insert and remove. 
To insert an element we just Cons it to be back list *)

val insert : #a:Type -> el:a -> q1:queue a -> Tot (q2:queue a{qSize q2 = qSize q1 + 1})
let insert #a el q = match q with
  | Q f b -> makeQ f (Cons el b)

(* If the queues is not empty than the front list must at least have one element because of the invariant *)

val notEmpty : queue 'a -> Tot bool
let notEmpty (Q f _) = size f > 0

(* To remove an element we just 'unCons' it from the front list *)

(* This function cannot be verified as it is, because hd and tl have a subtype error :
they expect a pos sList but they got a nat sList. For this reason I imposed q1 not to be empty
which means size f > 0 that is f has pos size. Despite this, the check does not work.
I understand that, maybe, a Lemma is needed to prove that.
Something like :
if the queue is not empty than the call of hd and tl on the front list is safe.
*************************** Question : How can i do that?? ********************************
*)

val remove : #a:Type -> q1:queue a{notEmpty q1} -> Tot (el:a * q2:queue a{qSize q2 = qSize q1 - 1})
let remove #a q = match q with
  | Q f b -> hd f, makeQ #_ #(size f - 1) (tl f) b

[nikswamy]

Let me explain how #580 is manifested here.

Say you have

val f : #n:nat -> slist bool n -> Tot unit
val k : nat
val l : slist bool k

Now, when you write

f l

F* tries to infer t the instantiation of #n by introducing a new unification variable ?u and solving it by unifying slist bool ?u with slist bool k, i.e., picking ?u = k. It then has to check that the solution is well-typed, i.e., in this case it has to check that k has type nat, which it does, so everything is ok.

Now, say you had:

val g : #n:nat{n > 0} -> slist bool n -> Tot unit

and you wrote

if k > 0 then g l else ()

Again, F tries to instantiate #n by solving a unification constraint as before, and finding the solution to be k. Now, it checks whether k has the type expected by g, i.e., whether k:nat{k > 0}. This time, the check fails, because of a limitation in how this check is implemented in F. In particular, in the case of checking the solutions to unification constraints, F does not make use of the control flow of the program. So, despite the test of k>0 in this context, F in this setting cannot prove that k is greater than zero.

Now, if instead you had written:

val g : #n:nat -> l:slist bool n{n > 0} -> Tot unit

Just moving the refinement away from the implicit argument (as you did in the type of Q) then the problem goes away.

This is clearly undesirable behavior that we're working hard on fixing. Meanwhile, one rule of thumb is to not refine your implicit arguments, instead placing those refinements in semantically equivalent contexts, but attaching them to explicit arguments. This is what I've done in a few places in your code.

Another option (usually less pleasant) is the style I used in the last remove function. In that case, you can explicitly instantiate your implicit arguments using the # notation. Note, the implicit arguments are positional. So, in this case, by writing makeQ #_ #(size f - 1) (tl f) b, I have instantiated the first implicit argument to an unspecified term, provided an explicit instantiation for the second one, and the third one is left implicit.

Sorry for this rather troublesome and confusing issue.

[nikswamy]

Finally, you might also consider a different style altogether for your example, relying less on indexed types in favor of refinement types and total functions.

For example, just use the regular list type in F* and the FStar.List.Tot library, i.e., something like:

module Queues
open FStar.List.Tot
type queue a = 
 | Q  : front:list a -> back:list a {length back <= length front} -> queue a

let rotate (#a:Type) (f:list a) (b:list a{length b > length a ==> length b = length a + 1})  : l:list a{length l = length a + length b} = append f (reverse b)

You may find some of the lemmas proven in ulib/FStar.ListProperties helpful, although I notice now that not all the lemmas you will need for your example are present, e.g., lemmas about the length of rev are missing, but should be easily provable.

[simosini]

@nikswamy First of all many thanks for your clear and very helpful explanation. I do understand now where I was wrong, and I really appreciate the fact that you guys are working hard on that issue. The only other question I have, probably due to my lack of knowledge (as I told you I'm just a beginner), is that I don't understand why this let binding about an empty queue, it's not accepted : let empQ = Q Nil Nil In fact whenever I try to verify this I got this weird (to me) error message : Error: Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. Failure("Universe variable not found").

[A-Manning]

If you go with NikSwamy's implementation above, let empQ = Q Nil Nil works just fine. The error looks like F# is unable to infer what universe empQ is in, perhaps annotating these explicitly will help for now? https://github.com/FStarLang/FStar/wiki/Explicit-universes may be relevant. Mixing implicits declared as #a and 'a seems to cause a lot of problems, so perhaps a refactor to avoid that would help.

[simosini]

Sorry to bother you again with this example, but that's still one thing I can't figure out. The remove function returns a tuple (el,newQ), that is the element removed plus the new queue. Anyway if I write :

let (el,newQ) = remove someOtherNotEmptyQ

I got Error : unexpected pattern at top-level If i write this instead :

let aTuple = remove someOtherNotEmptyQ
it works fine and, indeed, it accepts : 
let assertion = assert (aTuple = (el,newQ))

My question is : why the first let is not accepted?? Am I doing something wrong?? Thanks everyone

[kyoDralliam]

The error is a shortcoming of the current implementation of F. Basically any toplevel* declaration must be either a variable or a function. However, you can very well write let (el,newQ) = remove someOtherNotEmptyQ if it is not a toplevel let-binding.

I don't remember why we are not handling that. @nikswamy might be able to tell you more about this issue. AFAIK we could as well elaborate

let (el,newQ) = remove someOtherNotEmptyQ

to

let tmp_el_newQ = remove someOtherNotEmptyQ

let el = match tmp_el_newQ with | (el, newQ) -> el
let newQ = match tmp_el_newQ with | (el, newQ) -> newQ

[kyoDralliam]

Closing the thread since toplevel pattern have been implemented since then. So your code shoudl be working as is now @simosini