"detached" vs "attached" Flux specifications?

[ranjitjhala]

Hi @tautschnig and @carolynzech,

@nilehmann and I were working on a second PR to add flux specifications to verify underflows and slice-index-bounds more modules in core, namely -- pat, bstr, hash and time.

As you might have seen in the first PR, flux specifications are attached as attributes to the corresponding piece of Rust source code, but this has the effect of adding tool-specific annotations to the source. To simplify possible upstreaming we implemented a second style where specifications are detached and live in a separate file, leaving the source itself unchanged.

Here is a comparison of the two approaches

https://github.com/flux-rs/verify-rust-std/compare/c1e89cc88935110013543a1080bf8b9ea6655e3d..flux-submission2-detached

The left is "attached" and the right is "detached".

Do you all have any thoughts on which one you would prefer for a PR?

(The main advantage of the attached is that the spec is "right there", of course.)

Any thoughts would be most welcome!

[tautschnig]

Given that Rust has adopted (although experimental) a notion of contracts already with rust-lang#128044, which are in the "attached" style I'd lean towards that.

It actually makes me ask: do you think there is a path for Flux to eventually adopt Rust contract syntax?

I should note that I may be biased in that Kani also uses that "attached" style.

[ranjitjhala]

Ok, thanks! We'll try to keep things that are useful as contracts "attached" and other flux-specific stuff separate.

I think it is plausible that flux might adopt something like the contract syntax, but there are a few non-trivial challenges.

1. Flux lets you refine type definitions themselves (e.g. pack invariants into structs / enums) which can be quite handy
   as shown here

2. The refinements inside flux specifications are "pure", this means we can only support some subset of contracts which have to somehow be guaranteed to be pure (flux has various syntactic restrictions that enforce this requirement on specifications)

3. On the other hand, flux lets you write things like Vec<i32{v:v > 0}> which means a vector where all elements are strictly positive, which requires some sort of quantification with plain contracts.

4. Finally, flux lets you write specifications for closures in rather natural manner e.g. see this; I'm not quite sure what the best way to do that with contracts is -- the solutions I've seen in e.g. prusti and verus and dafny seem a bit more heavyweight...

[tautschnig]

Thank you for all the input! It think it is good that, for now, we have a range of specification grammars that each demonstrate some advantages (and possibly disadvantages). By rolling them out more widely (e.g., across a large fraction of the standard library) we will see what works best. Let's keep exploring!

Also, Rust's attributes and configurations mean that all of our approaches can safely co-exist. It would actually be nice to see some functions annotated with several shapes of contracts to have the different approaches side-by-side.