Trait implementation has extra _super variable

[parrot7483]

I am working on making the extracted F* from the libcrux-sha3 type-check using my fork of hax.

Currently I am facing an error which is probably a bug in HAX.

The Squeeze1 Trait in src/traits.rs gets extracted to this F*:

class t_Squeeze1 (v_Self: Type0) (v_T: Type0) = {
  f_squeeze_pre:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> Type0;
  f_squeeze_post:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> t_Slice u8 -> Type0;
  f_squeeze:v_RATE: usize -> x0: v_Self -> x1: t_Slice u8 -> x2: usize -> x3: usize
    -> Prims.Pure (t_Slice u8)
        (f_squeeze_pre v_RATE x0 x1 x2 x3)
        (fun result -> f_squeeze_post v_RATE x0 x1 x2 x3 result)
}

The implementation of the trait in src/simd/portable.rs gets extracted to this in F*:

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_2: Libcrux_sha3.Traits.t_Squeeze1
  (Libcrux_sha3.Generic_keccak.t_KeccakState (mk_usize 1) u64) u64 =
  {
    _super_18390613159176269294 = FStar.Tactics.Typeclasses.solve;
    f_squeeze_pre
    =
    (fun
        (v_RATE: usize)
        (self: Libcrux_sha3.Generic_keccak.t_KeccakState (mk_usize 1) u64)
        (out: t_Slice u8)
        (start: usize)
        (len: usize)
        ->
        true);
    f_squeeze_post
    =
    (fun
        (v_RATE: usize)
        (self: Libcrux_sha3.Generic_keccak.t_KeccakState (mk_usize 1) u64)
        (out: t_Slice u8)
        (start: usize)
        (len: usize)
        (out1: t_Slice u8)
        ->
        true);
    f_squeeze
    =
    fun
      (v_RATE: usize)
      (self: Libcrux_sha3.Generic_keccak.t_KeccakState (mk_usize 1) u64)
      (out: t_Slice u8)
      (start: usize)
      (len: usize)
      ->
      let out:t_Slice u8 = store_block v_RATE self.Libcrux_sha3.Generic_keccak.f_st out start len in
      out
  }

The _super variable in line 5 prevents the module from lax checking. Removing the line fixes the error.

In libcrux-sha3 run $ ./hax extract --portable to get the F* extraction

[W95Psp]

Thanks for the report!

Seems like I can't reproduce a standalone example easily:

trait KeccakItem<const I: usize> {}

pub(crate) trait Squeeze1<T: KeccakItem<1>> {
    fn squeeze<const RATE: usize>(&self, out: &mut [u8], start: usize, len: usize);
}

Open this code snippet in the playground

I will look at libcrux-sha3.

[W95Psp]

Looking at libcrux-sha3/10fbd6f06ad9ba52138e0 on hax main, ./hax.py extract gives me a Libcrux_sha3.Traits.fsti that contains:

/// Trait to squeeze bytes out of the state.
/// Note that this is implemented for each platform (1, 2, 4) because hax can't
/// handle the mutability required for a generic implementation.
/// Store blocks `N = 1`
class t_Squeeze1 (v_Self: Type0) (v_T: Type0) = {
  [@@@ FStar.Tactics.Typeclasses.no_method]_super_18390613159176269294:t_KeccakItem v_T (mk_usize 1);
  f_squeeze_pre:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> Type0;
  f_squeeze_post:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> t_Slice u8 -> Type0;
  f_squeeze:v_RATE: usize -> x0: v_Self -> x1: t_Slice u8 -> x2: usize -> x3: usize
    -> Prims.Pure (t_Slice u8)
        (f_squeeze_pre v_RATE x0 x1 x2 x3)
        (fun result -> f_squeeze_post v_RATE x0 x1 x2 x3 result)
}

So it seems I can't reproduce. I tried with your fork of hax, but got the same extraction. Can you try to minimize? e.g. if you take the piece of code I posted earlier and try to extract it in a new crate, do you hit the same bug?

[parrot7483]

I rebased my branch on latest libcrux main and used it together with latest HAX main.

Now its the other way around.

The extraction of src/traits.rs has the super variable:

/// Trait to squeeze bytes out of the state.
/// Note that this is implemented for each platform (1, 2, 4) because hax can't
/// handle the mutability required for a generic implementation.
/// Store blocks `N = 1`
class t_Squeeze1 (v_Self: Type0) (v_T: Type0) = {
  [@@@ FStar.Tactics.Typeclasses.no_method]_super_18390613159176269294:t_KeccakItem v_T (mk_usize 1);
  f_squeeze_pre:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> Type0;
  f_squeeze_post:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> t_Slice u8 -> Type0;
  f_squeeze:v_RATE: usize -> x0: v_Self -> x1: t_Slice u8 -> x2: usize -> x3: usize
    -> Prims.Pure (t_Slice u8)
        (f_squeeze_pre v_RATE x0 x1 x2 x3)
        (fun result -> f_squeeze_post v_RATE x0 x1 x2 x3 result)
}

but the implementation in src/simd/portable.rs is missing it

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_2: Libcrux_sha3.Traits.t_Squeeze1
  (Libcrux_sha3.Generic_keccak.t_KeccakState (mk_usize 1) u64) u64 =
  {
    f_squeeze_pre
    =
    (fun
        (v_RATE: usize)
        (self: Libcrux_sha3.Generic_keccak.t_KeccakState (mk_usize 1) u64)
        (out: t_Slice u8)
        (start: usize)
        (len: usize)
        ->
        true);

...

[W95Psp]

@Parrot7483, do you think this issue is still relevant? If so, could you write a Rust reproducer for it?

[parrot7483]

It is still a problem. I will try to reproduce.

[parrot7483]

I tried again to produce this error this in the playground. I could not reproduce it. I will start from the code in libcrux-sha3 and then simplify it step by step.