Interfaces without interleaving

[s-zanella]

In #959 @fournet summarized a few usability issues with interface files.
In a comment, @nik made a good proposal to do away with the interleaving semantics that would make them much more usable. For visibility, I'm making this an independent feature request and copying Nik's comment below.

See also this outstanding PR that describes other usability issues with pragma directives and open namespaces in interfaces.

In conversations with @mtzguido, @aseemr @protz et al., we've been considering revising the way interfaces are typechecked by doing away with the interleaving semantics.

Instead, we'd like to see the following behavior:

Typecheck A.fsti file
Typecheck A.fst, assuming all the symbols from A.fsti are in scope
Implemented a cycle detection check to make sure that we do not allow using 
ill-founded definitions, e.g., The following should be forbidden

val x : t
val y : t
let y = x
let x = y

Put another way, we'd like to see the .fsti as just a prefix of the .fst and to relax the syntactic criterion on ordering of val/let that is currently imposed by the ToSyntax phase (desugaring).

This should solve the issues 1, 2, and 5 in @fournet's original post.

But, there are also some complications:

-- While allowing out-of-order definitions, we should be careful to ensure that we do not introduce circularities in the SMT encoding (it's probably okay, but we should double check)

-- Out of order definitions cannot be extracted to ML. So, after step 3 above (i.e., checking for the absence of cycles), it would be good to topologically sort the sigelts in a module so that they can be processed in order by the rest of the compiler pipeline.

[s-zanella]

Adding another usability issue with the current interleaving semantics.

When verifying the implementation of a module, the interface file is re-checked as part of the interleaving. This means that the recommended incremental-build style will effectively run queries for typechecking A.fsti twice:

1. When verifying A.fsti, generating A.fsti.checked
2. When verifying A.fst. These queries run in a larger context and often counterintuively fail or need a much larger Z3 rlimit than they do when verifying A.fsti.

[mtzguido]

Ambitiously tagging this for the V1 release.

[mtzguido]

Ran into this again today. Particularly the issue mentioned by Jonathan here #1142 (comment).

EDIT: Though actually in my case it was more like:

fsti:

val join : int -> ...

val something_else : ... -> Lemma (join 42 ....)

fst:

let join = ...

...
open FStar.Tactics
...

let something_else = ....

And the error was that join expects a unit argument (since it's being resolved to the tactics one), which happens only when checking the fst, but pointing to an fsti location. It's more annoying since one cannot refer to join via a fully qualified name since it is in the same module.

[nikswamy]

Is this really achievable in a few weeks?

[SECtim]

Is there any progress/planned work on this? We're running into issues with #push-option pragmas from the fsti being ignored when checking the fst/interleaved file (and apparently, this is on purpose: #1142 though I'd be interested in the reasoning behind this, it seems a bit weird to me).

[mtzguido]

We haven't started working on this so far, but it's pretty high in our to-do list.

I think the reason for that (bandaid) patch you mention was that if an interface has something like:

#set-options "--fuel 0 --ifuel 0"
val f : ...

Then the fuel setting can leak into the definition of f in the fst. Even with another set-options just before the let f, the set-options from the fsti could sneak in between them and make the definition fail, and it's pretty hard to see why. I was under the impression that one can just repeat the relevant pragmas in the fst to work around this, but I suppose you might be observing the opposite problem..? i.e. you cannot robustly place the pragmas in order to wrap the vals?

Maybe a bigger bandaid is to keep two pragma states, so fst and fsti won't affect each other, and just interleave everything.

[SECtim]

Thanks for the reply, I see the point in doing it like that. Plus it's good to hear that this will be tackled 👍

In our case, we were indeed able to work around the problem by setting higher (i)fuel and resources in the fst file. We have some lemmas proven in the fsti file (which I admit is probably not the best style) and these lemmas failing to verify when checking the fst after we were able to verify the fsti came as quite a surprise for us.