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

No rewriting of $ names in fstar! macro with bundling #1196

Open
maximebuyse opened this issue Dec 18, 2024 · 0 comments · May be fixed by #1206
Open

No rewriting of $ names in fstar! macro with bundling #1196

maximebuyse opened this issue Dec 18, 2024 · 0 comments · May be fixed by #1206

Comments

@maximebuyse
Copy link
Contributor

mod a {
    #[hax_lib::requires(fstar!("$super::b::cond()"))]
    pub fn f(){super::b::g()}
}
mod b {
    pub fn g(){super::a::f()}
    pub fn cond() -> bool {true}
}

Open this code snippet in the playground

The example above has the following code in its fstar bundle:

let cond (_: Prims.unit) : bool = true

let rec f (_: Prims.unit)
    : Prims.Pure Prims.unit
      (requires Playground.B.cond ())
      (fun _ -> Prims.l_True) = g ()

Here we find Playground.B.cond in the precondition which should be transformed to just cond to avoid a cyclic dependency. I suspect the macro does something at the string level which will make it hard to fix.

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

Successfully merging a pull request may close this issue.

1 participant