Update the rustc pin

[Nadrieril]

This updates the rustc pin to a nightly from a few days ago. I did it like this to avoid the many developments of the attribute handling rework.

Other relevant changes:

• TypingMode rust-lang/types-team#128
• #t-compiler/help > Change in THIR of anonymous constants?

I'm leaving it as draft while I propagate the change to charon.

[Nadrieril]

Alright, everything is ready!

[W95Psp]

Thanks you, that's great! 😃
Let's merge!

[karthikbhargavan]

We need to also test this on libcrux, bertie, and pq11, both of which are somewhat critical right now. Let's please not merge in a rush if the proofs there break.

• libcrux (fix(F*): rename instance ids, following cryspen/hax#1391 libcrux#916)
• bertie
• pq11

[W95Psp]

I'm looking at bertie. @maximebuyse can you try this version of hax on PQ11? I don't really know what branch to test there.

[maximebuyse]

I'm looking at bertie. @maximebuyse can you try this version of hax on PQ11? I don't really know what branch to test there.

I have a few problems. One is that some names have changed in the core lib. I can push fixes for that. But there is something else which is more concerning:

mod Err1 {
    pub struct Error();
}

struct Error();

impl From<Err1::Error> for Error {
    fn from(value: Err1::Error) -> Self {
        Error()
    }
}

fn f(x: Result<i32, Err1::Error>) -> Result<i32, Error> {
    Ok(x?)
}

Open this code snippet in the playground
In this situation, with current hax main, we have the error conversion in the extracted F* (it is implicit in Rust with the ?). With the changes in this PR, there is no conversion, so the extracted F* doesn't lax-check.

[Nadrieril]

I diffed the THIR json for this example between main and this PR, and there are virtually zero differences except two tiny changes because attributes changed their representation. I am confused, because I can indeed reproduce the difference in the F* output.

[Nadrieril]

Ah wait, this PR is a week out of date with latest hax, let me update. EDIT: nope, no change.

[maximebuyse]

I diffed the THIR json for this example between main and this PR, and there are virtually zero differences except two tiny changes because attributes changed their representation. I am confused, because I can indeed reproduce the difference in the F* output.

This is fixed now, the question marks phase in the engine was relying on a hardcoded impl number which has changed with the rustc pin. With the fix we should be more robust. I also pushed the naming changes for the core lib so everything is good for pq11. I think we can merge! 🥳