Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make desugaring of for loops more hygienic #1240

Open
Lysxia opened this issue Nov 18, 2024 · 6 comments
Open

Make desugaring of for loops more hygienic #1240

Lysxia opened this issue Nov 18, 2024 · 6 comments

Comments

@Lysxia
Copy link
Collaborator

Lysxia commented Nov 18, 2024

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
Copy link
Collaborator

xldenis commented Nov 18, 2024

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
Copy link
Collaborator

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
Copy link
Collaborator Author

Lysxia commented Nov 18, 2024

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
Copy link
Collaborator

xldenis commented Nov 18, 2024

Yes your first snippet is undesirable.

@jhjourdan
Copy link
Collaborator

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
Copy link
Collaborator

xldenis commented Nov 19, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants