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).

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

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).

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!

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)

#[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?

#[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.

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.

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 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.

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

#[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

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

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.