Make desugaring of for loops more hygienic

[Lysxia]

The desugaring of for loops introduces three local variables: produced, iter_old, and iter, which are currently accessible from the body of the loop:

for i in 0..10 {
  let x = iter; // iter is in scope here
}

What is the intended scope of these identifiers?

• We mean to use produced in invariants. Do we also want to to be able to refer to iter_old and iter? If not then at least it is easy to put those two out of scope from user-written code/specs.
• Is it intentional to be able to refer to produced in the loop body, in a proof_assert! or an inner loop invariant?

Should users be allowed/required to bind produced explicitly somehow?

• Maybe users should explicitly name the produced variable, with a special "produces binder":

  #[produces(my_produced)]
  #[invariant(blah(my_produced))]
  for i in 0..10 {
    ...
  }

  which desugars to a lambda applied to the macro-generated produced variable?

[xldenis]

Is it intentional to be able to refer to produced in the loop body, in a proof_assert! or an inner loop invariant?

No, but I think I wasn't able to get it to work with rustc name hygiene.

Should users be allowed/required to bind produced explicitly somehow?

I don't want that to be required, I could understand giving people the option, but I want a sensible default produced.

iter_old, iter should not be usable either.

[jhjourdan]

I think I have a different opinion: iter is the current state of the iterator, which the user may want to assert things about, so it should be available to the user.

In addition, I don't see why we would provide access to these variables in invariants, but not in e.g., assertions. After all, assertions may be useful to help the provers prove the invariant.

Should users be allowed/required to bind produced explicitly somehow?

I don't want that to be required, I could understand giving people the option, but I want a sensible default produced.

Agreed.

[Lysxia]

OK that's good to know (including the fact that there is no consensus on iter).

In any case, we only want to be able to refer to those names in specs, not in code, so for example the snippet in my first comment should be considered incorrect syntax, right? Allowing those names in assertions but not in executable code seems like an interesting challenge.

[xldenis]

Yes your first snippet is undesirable.

[jhjourdan]

Again, my opinion is somewhat different.

I agree that the content of these variables is only relevant in specifications. However, I don't think this is a justification for having two different environments at the same program point (the first environment for variables usable in the program, the second environment for variables usable in specifications). This adds yet another complication in the semantics, without a pragmatic justification: I don't think there is one use case where the program would be easier to write with that.

We could even imagine cases where the use would use produced, of type Snapshot<Seq<T>> to write snapshot to fields of a data structure.

[xldenis]

I agree that the content of these variables is only relevant in specifications. However, I don't think this is a justification for having two different environments at the same program point (the first environment for variables usable in the program, the second environment for variables usable in specifications). This adds yet another complication in the semantics, without a pragmatic justification: I don't think there is one use case where the program would be easier to write with that.

His first snippet modifies iter which is is a program variable. I would say that for our macro to be a faithful encoding of the rust equivalent we cannot allow that to be accessible.