Usability issues with interfaces

[fournet]

I wrote down a bunch of issues while writing Handshake.Log.fsti and Handshake.fsti; I don't have smaller repros, sorry.

• rewriting val/let to a single annotated let to migrate it to an interface.
• maintaining the same ordering between interfaces and implementations (goes against local code clarity)
• refreshing the state of the implementation buffer while editing both files.
• restarting verification in the implementation buffer after it crashes, e.g. on a typing error when reading its interface, aka Found the interface Handshake.fsti but could not parse it first!
• adding intermediate let bindings in implementations of abstract types.
• fixing proofs that used to go through in a single file, e.g. adding annotations (see e.g. eT and next_fragment in Handshake.fsti).
• In interactive mode, I am getting early terminations from F* and some Failure("Bound term variable not found (after unmangling)").
• In interactive mode for the interface, some errors are poorly localized, e.g. a failing assert reports F* reported issues in other files: [([cl-struct-fstar-issue error "C:\\cygwin64\\home\\fournet\\everest\\FStar\\ulib\\prims.fst" 633 633 4 11 "assertion failed"])]

[fournet]

Another interface/interactive problem: when loading the fst, fstar crashes with Found the interface Foo.fsti but could not parse it first!. This is hard to debug and seems to cover other errors, e.g. .\StAE.fsti(81,0-81,29) : (Error) Interface contains an abstract 'type' declaration; use 'val' instead that are not detected while verifying the fsti (even on the command line). In some cases, both fst and fsti pass verification on the command line.

[fournet]

Overall, working with interfaces currently involves 4 windows: two in emacs, and two for getting command-line errors.

[msprotz]

@cpitclaudel would you know which of these are still valid?

[cpitclaudel]

rewriting val/let to a single annotated let to migrate it to an interface.

Does this mean that you have a let succ: (x: int) : int = x + 1 and you want to extract val succ: x:int -> int?
I don't think we have tools to do that ATM. But I'd prefer just having keywords and generating the full fsti from those over generating these vals one by one and migrating them to the fsti by hand.

maintaining the same ordering between interfaces and implementations (goes against local code clarity)

I think this is a core principle of F* interfaces.

refreshing the state of the implementation buffer while editing both files.

I think this works nicely now.

restarting verification in the implementation buffer after it crashes, e.g. on a typing error when reading its interface, aka Found the interface Handshake.fsti but could not parse it first!

That too.

adding intermediate let bindings in implementations of abstract types.

Not sure what this refers to.

fixing proofs that used to go through in a single file, e.g. adding annotations (see e.g. eT and next_fragment in Handshake.fsti).

Same here

In interactive mode, I am getting early terminations from F* and some Failure("Bound term variable not found (after unmangling)").

#933, #1091

In interactive mode for the interface, some errors are poorly localized, e.g. a failing assert reports F* reported issues in other files: [([cl-struct-fstar-issue error "C:\cygwin64\home\fournet\everest\FStar\ulib\prims.fst" 633 633 4 11 "assertion failed"])]

I think this is better now (we report the error in the main file, and use the alternate location field to point to the other file). There may still be cases where the whole error is reported on the other file, though.

[nikswamy]

Interfaces without interleaving

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:

1. Typecheck A.fsti file
2. Typecheck A.fst, assuming all the symbols from A.fsti are in scope
3. 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.