Need to refer to $self_ instead of $self in ensures
#1276
Labels
lib
Lib-related issue (e.g. annotations lib)
Comments
struct Test(u8);
#[hax_lib::attributes]
impl Test {
#[hax_lib::ensures(|result| fstar!("${self_}._0 = $result"))]
fn f(&self) -> u8 {self.0}
}Open this code snippet in the playground Here is a reproducer for an inherent impl, where things seem to be just broken. |
Workaround: struct Test(u8);
#[hax_lib::attributes]
impl Test {
#[hax_lib::ensures(|result| fstar!("let ${self_} = self in ${self_.0} = $result"))]
fn f(&self) -> u8 {self.0}
} |
|
We hit this again in Bertie. It would be great to prioritize this. |
|
Note that this is not just an See: struct Test(pub u8);
#[hax_lib::attributes]
impl Test {
#[hax_lib::ensures(|result| self.0 == result)]
fn f(&self) -> u8 {self.0}
} |
This was referenced Mar 10, 2025
W95Psp
added a commit
that referenced
this issue
Mar 11, 2025
Consider the following piece of code:
```rust
struct S(pub u8);
impl S {
#[hax_lib::requires(self.0 == 0)]
fn f(&self) {}
}
```
The `requires` annotation produces a standalone function that looks like the following:
```rust
fn requires(self_: S) -> bool {
self_.0 == 0
}
```
Here, we can't use `self`: this is a reserved keyword in Rust, and we are not in a `impl` context.
Thus, the macro renames `self` into `self_`.
The bug described in #1276 comes from this renaming not being reverted in the engine.
With this commit, when the F* backend inteprets
such clauses, if the function on which a clause
exists have a `self` as first argument, we now
substitute the first argument of the clause
function to replace it with the first argument of
the original function.
In the example above, we replace `self_` with `self`.
W95Psp
added a commit
that referenced
this issue
Mar 11, 2025
Consider the following piece of code:
```rust
struct S(pub u8);
impl S {
#[hax_lib::requires(self.0 == 0)]
fn f(&self) {}
}
```
The `requires` annotation produces a standalone function that looks like the following:
```rust
fn requires(self_: S) -> bool {
self_.0 == 0
}
```
Here, we can't use `self`: this is a reserved keyword in Rust, and we are not in a `impl` context.
Thus, the macro renames `self` into `self_`.
The bug described in #1276 comes from this renaming not being reverted in the engine.
With this commit, when the F* backend inteprets
such clauses, if the function on which a clause
exists have a `self` as first argument, we now
substitute the first argument of the clause
function to replace it with the first argument of
the original function.
In the example above, we replace `self_` with `self`.
This PR also improves the macro to always pick a fresh name, not always `self_`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Open this code snippet in the playground
As in the example above, when using
fstar!inside anensuresfor a method inside a trait implementation, we need to refer to self as$self_instead of$selfwhich is confusing. Note that this seems not to work at all for a non-trait impl.The text was updated successfully, but these errors were encountered: