Weird issue with seq.fsi / FStar.Seq.fst

[msprotz]

It seems like FStar.Seq.fst cannot be verified alone, and needs seq.fsi prepended to it... this is sending the auto-deps analysis off the rails. Any way we can get rid of seq.fsi?

[msprotz]

There seems to be a similar issue with ordset.fsi:

protz@Joprotze-Z420:~/Code/fstar/examples/algorithms (master) $ fstar --explicit_deps --admit_fsi FStar.Set --admit_fsi FStar.OrdSet --admit_fsi FStar.OrdSetPropsFStar.FunctionalExtensionality.fst FStar.Set.fsi FStar.Heap.fst FStar.ST.fst FStar.All.fst FStar.List.Tot.fst ordset.fsi FStar.OrdSetProps.fst unification.fst 
Verifying module: FStar.Heap
Verifying module: FStar.ST
Verifying module: FStar.All
Verifying module: FStar.List.Tot
Verifying module: FStar.OrdSetProps
Verifying module: Unification
All verification conditions discharged successfully
protz@Joprotze-Z420:~/Code/fstar/examples/algorithms (master) $ fstar --dep nubuild !$
fstar --dep nubuild unification.fst
D:\cygwin\home\protz\Code\fstar\lib\prims.fst
D:\cygwin\home\protz\Code\fstar\lib\FStar.Set.fsi
D:\cygwin\home\protz\Code\fstar\lib\FStar.Heap.fst
D:\cygwin\home\protz\Code\fstar\lib\FStar.ST.fst
D:\cygwin\home\protz\Code\fstar\lib\FStar.All.fst
D:\cygwin\home\protz\Code\fstar\lib\FStar.List.Tot.fst
D:\cygwin\home\protz\Code\fstar\lib\FStar.List.fst
D:\cygwin\home\protz\Code\fstar\lib\FStar.OrdSet.fst
unification.fst
protz@Joprotze-Z420:~/Code/fstar/examples/algorithms (master) $ fstar unification.fst 
D:\cygwin\home\protz\Code\fstar\lib\FStar.OrdSet.fst(58,6-58,46) : Error
(D:\cygwin\home\protz\Code\fstar\lib\FStar.OrdSet.fst(58,6-58,46)) Failed to solve the sub-problem
    (U18905 a f s1 s2 hd tl) (Typ_app(Typ_uvar, [6 args])) 
        =(TOP)
    l:(ordset a f){((is_Cons l) /\ (((hd l) = x) \/ ((is_Cons s) /\ ((hd l) = (hd s)))))} (Typ_refine) (guard (U18906 a f s1 s2 hd tl))
Which arose because:
    TOP
Failed because:free-variable check failed on a non-redex

[jkzinzindohoue]

You can merge seq.fsi into FStar.Seq.fst and rename seq.fsi into FStar.Seq.fsi. I do not know why Set was renamed but not Seq.

[catalin-hritcu]

You can merge seq.fsi into FStar.Seq.fst and rename seq.fsi into FStar.Seq.fsi. I do not know what Set was renamed but not Seq.

Too many typos in this comment? Makes little sense to me.

[jkzinzindohoue]

Fixed one typo, if it helps.

[catalin-hritcu]

@jkzinzindohoue So you want seq.fsi to be both merged into the new fst and renamed into the new fsi?

[jkzinzindohoue]

Well if I understand the way things are going, with the merge of the auto-deps branch we will not be able to use .fst files as implementations for .fsi. I may be wrong, all this is not very clear to me. In any case, the current FStar.Seq.fst file contains only implementation, it has no types, no function declarations. So if one wants to prove something relying on the FStar.Seq module she has to either import both seq.fsi and FStar.Seq.fst (which works fine now, I am doing that), or if that it no longer available, all the specs have to be ported to FStar.Seq.fst so that the module is self-contained. Additionally I was thinking that to make the context lighter, people may want to keep the .fsi file, and admit it when extraction is not needed for example. In which case renaming it under the current FStar.Module convention would probably be more appropriate.

[catalin-hritcu]

@jkzinzindohoue Makes more sense now, thank you :)

[beurdouche]

So, I have those changes locally where all the specs from the .fsi file are merged in the .fst file (exactly and without any changes). This type-check without error ...

Should I push this change and remove seq.fsi ?

[catalin-hritcu]

+1

[beurdouche]

Done in https://github.com/FStarLang/FStar/commit/f70393b69f7d793128e8023ad0de2f8fc72a257f I'll fix the Makefile ... etc...

[msprotz]

Excellent. If you see any Makefiles that use --explicit_deps just for the purpose of passing seq.fsi before FStar.Seq.fst, chances are they might work without --explicit_deps and without any other arguments except for the last file.

[fournet]

Still confused by this... How to fix the Makefile in mitls to get something to typecheck again?

[beurdouche]

remove the --admit_fsi FStar.Seq replace seq.fsi by FStar.Seq.fst if it was not already there

[ad-l]

Just fixed the mitls-fstar Makefile

[beurdouche]

Can someone please check if make -C examples go through. (I often have z3 timeouts on OSX...)

[msprotz]

Running that right now

[msprotz]

The four steps after make theory in examples/wysteria/Makefile are broken; everything else is good.

[beurdouche]

Ok I'll have a look at it, thanks.

[beurdouche]

I think we are almost ok for FStar.Seq.fst now... Also, I fixed --auto-deps issues in forgotten targets for verification in wysteria except for a codegen target that won't go through because of ordset.fsi. Probably @aseemr should have a look at the target to make it work before we attempt to merge ordset.fsi with FStar.OrdSet.fst

[beurdouche]

Closing, feel free to reopen if there are problems with FStar.Seq

[nikswamy]

Removing 'seq.fsi' probably broke several clients, or at least slowed down their verification greatly.

The reason is that without the .fsi, every client program will have been verified against the concrete definition of sequences, rather than their more abstract, axiomatic interface. This will slow down the SMT solver a LOT.

Discussing with Jonathan, the plan to solve this is to replicate in the master branch the functionality for the 'abstract' qualifier currently available in the universes branch. I will do this ASAP (some time this week, probably)

[nikswamy]

It would be good to have some non-functional tests also, e.g., checking that verification time didn't blow up because of nuking seq.fsi.

[beurdouche]

Yes, it would be a good idea. I probably didn't see the verification time increase because some parts of examples/metatheory and examples/wysteria where already blowing up very often on my machine because of z3 timeouts. Do you get problems except for eventually those ?