Opaque extensions

[maximebuyse]

Fixes #1119

We implement this design. The attribute opaque is introduced and allows to drop the content (erase) of functions, types, trait impls, consts, etc. to make them abstract. In this case we produce a type signature and an abstract definition (using assume in fstar). The interface-only include flag (cargo hax into -i '+:.....) allows to erase easily many items. It relies on default rules that say if a selected item should be erased or not (see design doc).

[maximebuyse]

Adding a note here that I noticed while reviewing the test result for tests/cli/interface-only. This previously produced only an fsti file, it now produces only an fst file. This makes sense because it uses the -i '+:' flag but no --interfaces flag for the fstar backend. As we now provide definitions for erased items we get them in an fst file. The definitions can still be discarded using --interfaces +!**. Maybe it would be worth documenting this but I am not sure where (I started with updating the documentation of the -i flag).

[W95Psp]

Thanks, I'm reviewing now.
Some snapshots are conflicting though: can you update them?

[maximebuyse]

Thanks, I'm reviewing now. Some snapshots are conflicting though: can you update them?

Done. I also pushed a small commit to allow making a single method opaque inside an impl (regular non-trait impl).

[W95Psp]

Thanks, that looks good to me :)
I have some minor comments.

I still need to test the PR on snippets of code.

[W95Psp]

Thanks, I'm reviewing now. Some snapshots are conflicting though: can you update them?

Done. I also pushed a small commit to allow making a single method opaque inside an impl (regular non-trait impl).

Oh great, that's a nice addition!

[W95Psp]

We also need the opaque attribute to work on traits I think. We forgot that case in the design document.

#[hax_lib::opaque]
trait Foo<X, Y> {
  ...
}

Should be translated to:

assume type foo: Type -> Type -> Type

(and for fsti val foo: Type -> Type -> Type)

[W95Psp]

#[hax_lib::opaque]
fn opaque_function(){}

fn regular_function(){}

Open this code snippet in the playground

Gets translated to:

val opaque_function: Prims.unit -> Prims.unit
assume val opaque_function': Prims.unit -> Prims.unit
let opaque_function = opaque_function'

let regular_function (_: Prims.unit): Prims.unit = ()

I don't think we want the val opaque_function, do we?

[maximebuyse]

#[hax_lib::opaque]
fn opaque_function(){}

fn regular_function(){}

Open this code snippet in the playground

Gets translated to:

val opaque_function: Prims.unit -> Prims.unit
assume val opaque_function': Prims.unit -> Prims.unit
let opaque_function = opaque_function'

let regular_function (_: Prims.unit): Prims.unit = ()

I don't think we want the val opaque_function, do we?

We want it in the fsti (if we have an fsti). I can generate it only in interface mode.

[maximebuyse]

We also need the opaque attribute to work on traits I think. We forgot that case in the design document.

#[hax_lib::opaque]
trait Foo<X, Y> {
  ...
}

Should be translated to:

assume type foo: Type -> Type -> Type

(and for fsti val foo: Type -> Type -> Type)

Yes that can be nice when we have unallowed &mut in method signatures. I implemented that but maybe we should be careful about an opaque trait that has non-opaque impls. I think it could be nice to somehow enforce this (but maybe it is not a priority.

[W95Psp]

Yes that can be nice when we have unallowed &mut in method signatures. I implemented that but maybe we should be careful about an opaque trait that has non-opaque impls. I think it could be nice to somehow enforce this (but maybe it is not a priority.

Indeed, let's file an issue with a good description then. I think we don't care for this PR.

[maximebuyse]

Yes that can be nice when we have unallowed &mut in method signatures. I implemented that but maybe we should be careful about an opaque trait that has non-opaque impls. I think it could be nice to somehow enforce this (but maybe it is not a priority.

Indeed, let's file an issue with a good description then. I think we don't care for this PR.

Yes, let's do that. I am not sure what you described worked by the way. With:

val t_T (v_Self v_U: Type0) : Type0

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl:t_T u8 u8

fstar complains with:

Instances must define instances of `class` types.
  - Type
    Opaque_impl.t_T Rust_primitives.Integers.u8 Rust_primitives.Integers.u8
    is not a class.

[W95Psp]

Ah, you are right, there's a catch, you need an attribute to mark the val (or assume val) as a typeclass, as follows:

[@@ FStar.Tactics.Typeclasses.tcclass]
val t_T (v_Self v_U: Type0) : Type0

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl:t_T u8 u8

[maximebuyse]

#[hax_lib::opaque]
fn opaque_function(){}

fn regular_function(){}

Open this code snippet in the playground

Gets translated to:

val opaque_function: Prims.unit -> Prims.unit
assume val opaque_function': Prims.unit -> Prims.unit
let opaque_function = opaque_function'

let regular_function (_: Prims.unit): Prims.unit = ()

I don't think we want the val opaque_function, do we?

@W95Psp This is fixed now

[W95Psp]

We chatted quickly about this with @maximebuyse, the opaque traits are not implemented yet, either we implement that here or we open a follow up issue.
It's unlikely I will have time to do more review here by the end of the day, I will do that Monday morning

[maximebuyse]

We just noticed a few problems here:

• For the case of types we should generate something similar as other cases in the fst (assume val with a let alias)
• The let alias should take and pass the generic arguments otherwise fstar fails.
• We should have tests for all of that, also with trait bounds.

[maximebuyse]

We just noticed a few problems here:

* For the case of types we should generate something similar as other cases in the fst (`assume val` with a let alias)

* The let alias should take and pass the generic arguments otherwise fstar fails.

* We should have tests for all of that, also with trait bounds.

All of this is now fixed. @W95Psp You can review.

[W95Psp]

I've spawned a ML-KEM job for this PR: https://github.com/cryspen/libcrux/actions/runs/12292989138

That looks good to me. I think we can improve a bit the tests. Can you add:

• an associated type in trait T
• an associated constant in T
• an associated method (with a self) in T, with a precondition (say, a method that takes a self and a u8, with a precondiotion on the u8)
• in the impl of T for u8, add the same precondition and a postcondition
• an inherent impl

This way I think we will have all the possible items kind covered :)

[W95Psp]

The Ci above failed: after chatting with @maximebuyse, we found out the issue. This PR is a breaking change for haxlib, thus we need to update the pin in libcrux.

Running the CI again with pinning hax in libcrux to the right branch (libcrux/follow-up-pr-hax-1134): https://github.com/cryspen/libcrux/actions/runs/12293570150

This failed because of dependencies being duplicated, new run here:
https://github.com/cryspen/libcrux/actions/runs/12293872143/job/34307457260

[W95Psp]

We found a small regression: when extracting an impl without associated type in F* interface mode, we used to expose a single opaque val for the impl. This is not the case any more, but @maximebuyse is taking care of fixing that.
After that, we will re-trigger a libcrux job, if this job is green, we merge.

[maximebuyse]

We found a small regression: when extracting an impl without associated type in F* interface mode, we used to expose a single opaque val for the impl. This is not the case any more, but @maximebuyse is taking care of fixing that. After that, we will re-trigger a libcrux job, if this job is green, we merge.

We found a small regression: when extracting an impl without associated type in F* interface mode, we used to expose a single opaque val for the impl. This is not the case any more, but @maximebuyse is taking care of fixing that. After that, we will re-trigger a libcrux job, if this job is green, we merge.

I worked on a fix, I think it does what we want. It would be nice to add a test for that but it affects the interface mode (not interface-only) and I don't think we have a test that does that. Anyway I restarted the libcrux job: https://github.com/cryspen/libcrux/actions/runs/12296788479/job/34316515254

[W95Psp]

Libcrux CI is green, let's merge!