Allow `@`-binders in outputs about flux HOT 12 CLOSED

There's one neat use of requires that you can't do with constrained types, you can define unreachable as:

fn unreachable()
requires false

instead of

fn unreachable(_: {() : false})

which makes it more comfortable to use.

Other than that it's not strictly necessary, but I do find it sometimes clearer to specify the relationships between inputs in a requires clause.

I don't hate nor love #. In the interest of experimenting with the feature, I would go for it since it seems to have a clearer meaning.

from flux.

@ranjitjhala do you have a specific example in mind that requires this?

While the semantics of existentials in return position is clear to me, I'm a bit hesitant about whether we should abuse the @n syntax. Maybe this is an advance enough (uncommon) use case to require an explicit exists for clarity over conciseness.

Additionally, the particular example you posted could also be expressed with a "dependent pair". Strictly speaking, I think we only need existentials in position (...) -> exists n. ... if n is going to be mentioned both in the return type and ensures clauses.

from flux.

The "use-case" I have in mind was motivated by the kani/firecracker post

https://github.com/model-checking/kani/blob/main/tests/cargo-kani/firecracker-block-example/src/main.rs

but also the pattern in the motivating example for the "implicit refinement types" paper.

in essence, you have an api call that does some internal computation and returns:

• some value N and
• some other associated value that "depends on" N

So you want to give the output type the signature something like:

foo (p: &strg Thing) -> exists N. i32{v: ... depends on N ... } ensures p: Thing[N]

or the other way around the i32[N] and the p: Thing[... depends on N...]

from flux.

Not exactly the same thing, but I believe we should be able to support a general type exists n. T for any type T, provided that n appears in a proper position. I believe this could be used to desugars various syntaxes, e.g., dependent pairs as in the example in the original post. If the binder can be mentioned both in the return type and the ensures clauses, then the problem is different because we cannot simply desugar it as a type, but it is a related problem.

In anticipation, I already started some related work here https://github.com/liquid-rust/flux/tree/evars. It refactors the way we infer parameters at function calls. So, instead of inferring parameters first and then checking subtyping, we first generate fresh evars and then unify them during subtyping. I believe this will be useful to support existentials in more positions.

from flux.

Another use-case that shows up in wave (AFAICT) -- you have a method that takes in two &mut RVec of equal size and then pushes stuff into both (or pops from both) -- so simpler version is:

fn foo(x: &mut i32, y: &mut i32) {
  while random() > 10 {
     *x += 1;
     *y += 1;
  }
}  

So you'd want a signature like:

fn (x: &strg i32[@n], y: &strg i32[n]) ensures x: i32[#m], y: i32[m]

(using #m to denote the "output" or "existential" instead of the input @n)

from flux.

If we decide on the surface syntax this should be easy to implement after #281

from flux.

Some choices (am not particularly wedded to anything)

// Use explicit exists
fn (x: &strg i32[@n], y: &strg i32[n]) ensures exists m. x: i32[m], y: i32[m]

// Use `@` in the output
fn (x: &strg i32[@n], y: &strg i32[n]) ensures x: i32[@m], y: i32[m]

// Use some other symbol in the output eg
fn (x: &strg i32[@n], y: &strg i32[n]) ensures x: i32[#m], y: i32[m]

My suggestion would be to start with "explicit exists" and then if it gets too tedious/important enough, it will probably be easy to modify desugar to support
either of the other options?

from flux.

The problem with exists is that I don't really know where to put it to make clear what's the scope. Ideally, it should range over the ensures clauses and the return type, but it is weird when combined with requires

fn() -> exists x. R
requires p
ensures q

I want the exists to be over the return type R and the ensure predicate q.

from flux.

Do we really need a requires anymore?

from flux.

Or maybe then we should use the # to distinguish output binders (which WF will check cannot appear in the requires...)

from flux.

The # would also address the odd asymmetry of using exists (when we don't use a forall)...

from flux.

agree on all points!

from flux.