proof of concept: hax by cfm · Pull Request #131 · freedomofpress/securedrop-protocol

cfm · 2025-12-04T01:01:28Z

https://hax.cryspen.com/manual/fstar/quick_start/

Per <https://hax.cryspen.com/manual/fstar/quick_start/>.

cfm · 2025-12-04T01:04:20Z

user@dev:~/securedrop-protocol/securedrop-protocol$ cargo build >/dev/null 2>&1
user@dev:~/securedrop-protocol/securedrop-protocol$ echo $?
0

hax itself seems to choke on some upstream incompatibilities.

user@dev:~/securedrop-protocol/securedrop-protocol$ cargo hax into fstar
    Checking libcrux-p256 v0.0.4
    Checking libcrux-curve25519 v0.0.4
    Checking libcrux-chacha20poly1305 v0.0.4
    Checking libcrux-aesgcm v0.0.4
error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 32]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-curve25519-0.0.4/src/ecdh_api.rs:19:22
   |
19 |         clamp(secret.declassify_ref_mut());
   |                      ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
19 -         clamp(secret.declassify_ref_mut());
19 +         clamp(secret.declassify_ref());
   |

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 32]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-curve25519-0.0.4/src/ecdh_api.rs:38:21
   |
38 |             derived.declassify_ref_mut().as_mut_slice(),
   |                     ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
38 -             derived.declassify_ref_mut().as_mut_slice(),
38 +             derived.declassify_ref().as_mut_slice(),
   |

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 32]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-curve25519-0.0.4/src/lib.rs:45:18
   |
45 |         clamp(dk.declassify_ref_mut());
   |                  ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
45 -         clamp(dk.declassify_ref_mut());
45 +         clamp(dk.declassify_ref());
   |

error[E0599]: no method named `declassify_ref_mut` found for array `[u8; 32]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-curve25519-0.0.4/src/lib.rs:57:22
   |
57 |         clamp(eph_dk.declassify_ref_mut());
   |                      ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
57 -         clamp(eph_dk.declassify_ref_mut());
57 +         clamp(eph_dk.declassify_ref());
   |

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 32]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-curve25519-0.0.4/src/lib.rs:60:17
   |
60 |         ecdh(ss.declassify_ref_mut(), ek, eph_dk.declassify_ref())
   |                 ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
60 -         ecdh(ss.declassify_ref_mut(), ek, eph_dk.declassify_ref())
60 +         ecdh(ss.declassify_ref(), ek, eph_dk.declassify_ref())
   |

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 32]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-curve25519-0.0.4/src/lib.rs:69:17
   |
69 |         ecdh(ss.declassify_ref_mut(), ct, dk.declassify_ref())
   |                 ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
69 -         ecdh(ss.declassify_ref_mut(), ct, dk.declassify_ref())
69 +         ecdh(ss.declassify_ref(), ct, dk.declassify_ref())
   |

For more information about this error, try `rustc --explain E0599`.
error: could not compile `libcrux-curve25519` (lib) due to 6 previous errors
warning: build failed, waiting for other jobs to finish...
error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 16]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-chacha20poly1305-0.0.4/src/impl_aead_trait.rs:56:21
   |
56 |                 tag.declassify_ref_mut(),
   |                     ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
56 -                 tag.declassify_ref_mut(),
56 +                 tag.declassify_ref(),
   |

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-chacha20poly1305-0.0.4/src/impl_aead_trait.rs:88:27
   |
88 |                 plaintext.declassify_ref_mut(),
   |                           ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
88 -                 plaintext.declassify_ref_mut(),
88 +                 plaintext.declassify_ref(),
   |

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:13:5
   |
12 | fn new_state() -> State {
   |                   ----- expected `core::arch::x86_64::__m128i` because of return type
13 |     mm_setzero_si128()
   |     ^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
13 |     mm_setzero_si128().into()
   |                       +++++++

error[E0599]: no method named `declassify_ref_mut` found for array `[u8; 32]` in the current scope
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-chacha20poly1305-0.0.4/src/impl_aead_trait.rs:155:24
    |
155 |                 subkey.declassify_ref_mut(),
    |                        ^^^^^^^^^^^^^^^^^^
    |
help: there is a method `declassify_ref` with a similar name
    |
155 -                 subkey.declassify_ref_mut(),
155 +                 subkey.declassify_ref(),
    |

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:18:11
    |
 18 |     *st = mm_xor_si128(*st, *k);
    |           ^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:18:24
    |
 18 |     *st = mm_xor_si128(*st, *k);
    |                        ^^^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:18:29
    |
 18 |     *st = mm_xor_si128(*st, *k);
    |                             ^^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:459:8
    |
459 | pub fn mm_xor_si128(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 18 |     *st = mm_xor_si128((*st).into(), *k);
    |                        +   ++++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 18 |     *st = mm_xor_si128(*st, (*k).into());
    |                             +  ++++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:18:11
   |
18 |     *st = mm_xor_si128(*st, *k);
   |     ---   ^^^^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |     |
   |     expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
18 |     *st = mm_xor_si128(*st, *k).into();
   |                                +++++++

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:23:11
    |
 23 |     *st = mm_aesenc_si128(*st, *key);
    |           ^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:23:27
    |
 23 |     *st = mm_aesenc_si128(*st, *key);
    |                           ^^^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:23:32
    |
 23 |     *st = mm_aesenc_si128(*st, *key);
    |                                ^^^^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:775:8
    |
775 | pub fn mm_aesenc_si128(a: Vec128, b: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 23 |     *st = mm_aesenc_si128((*st).into(), *key);
    |                           +   ++++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 23 |     *st = mm_aesenc_si128(*st, (*key).into());
    |                                +    ++++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:23:11
   |
23 |     *st = mm_aesenc_si128(*st, *key);
   |     ---   ^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |     |
   |     expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
23 |     *st = mm_aesenc_si128(*st, *key).into();
   |                                     +++++++

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 64]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-p256-0.0.4/src/ecdh_api.rs:39:21
   |
39 |             derived.declassify_ref_mut().as_mut_slice(),
   |                     ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
39 -             derived.declassify_ref_mut().as_mut_slice(),
39 +             derived.declassify_ref().as_mut_slice(),
   |

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:28:11
    |
 28 |     *st = mm_aesenclast_si128(*st, *key);
    |           ^^^^^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:28:31
    |
 28 |     *st = mm_aesenclast_si128(*st, *key);
    |                               ^^^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:28:36
    |
 28 |     *st = mm_aesenclast_si128(*st, *key);
    |                                    ^^^^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:781:8
    |
781 | pub fn mm_aesenclast_si128(a: Vec128, b: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 28 |     *st = mm_aesenclast_si128((*st).into(), *key);
    |                               +   ++++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 28 |     *st = mm_aesenclast_si128(*st, (*key).into());
    |                                    +    ++++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:28:11
   |
28 |     *st = mm_aesenclast_si128(*st, *key);
   |     ---   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |     |
   |     expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
28 |     *st = mm_aesenclast_si128(*st, *key).into();
   |                                         +++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:33:46
    |
 33 |     *next = mm_aeskeygenassist_si128::<RCON>(*prev);
    |             -------------------------------- ^^^^^ expected `BitVec<128>`, found `__m128i`
    |             |
    |             arguments to this function are incorrect
    |
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:787:8
    |
787 | pub fn mm_aeskeygenassist_si128<const RCON: i32>(a: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 33 |     *next = mm_aeskeygenassist_si128::<RCON>((*prev).into());
    |                                              +     ++++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:33:13
   |
33 |     *next = mm_aeskeygenassist_si128::<RCON>(*prev);
   |     -----   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |     |
   |     expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
33 |     *next = mm_aeskeygenassist_si128::<RCON>(*prev).into();
   |                                                    +++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:39:38
    |
 39 |     *next = mm_shuffle_epi32::<0xff>(*next);
    |             ------------------------ ^^^^^ expected `BitVec<128>`, found `__m128i`
    |             |
    |             arguments to this function are incorrect
    |
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:566:8
    |
566 | pub fn mm_shuffle_epi32<const CONTROL: i32>(vector: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 39 |     *next = mm_shuffle_epi32::<0xff>((*next).into());
    |                                      +     ++++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:39:13
   |
39 |     *next = mm_shuffle_epi32::<0xff>(*next);
   |     -----   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |     |
   |     expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
39 |     *next = mm_shuffle_epi32::<0xff>(*next).into();
   |                                            +++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:45:38
    |
 45 |     *next = mm_shuffle_epi32::<0xaa>(*next);
    |             ------------------------ ^^^^^ expected `BitVec<128>`, found `__m128i`
    |             |
    |             arguments to this function are incorrect
    |
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:566:8
    |
566 | pub fn mm_shuffle_epi32<const CONTROL: i32>(vector: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 45 |     *next = mm_shuffle_epi32::<0xaa>((*next).into());
    |                                      +     ++++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:45:13
   |
45 |     *next = mm_shuffle_epi32::<0xaa>(*next);
   |     -----   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |     |
   |     expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
45 |     *next = mm_shuffle_epi32::<0xaa>(*next).into();
   |                                            +++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:50:53
    |
 50 |     let p0 = mm_xor_si128(*prev, mm_slli_si128::<4>(*prev));
    |                                  ------------------ ^^^^^ expected `BitVec<128>`, found `__m128i`
    |                                  |
    |                                  arguments to this function are incorrect
    |
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:530:8
    |
530 | pub fn mm_slli_si128<const SHIFT_BY: i32>(vector: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 50 |     let p0 = mm_xor_si128(*prev, mm_slli_si128::<4>((*prev).into()));
    |                                                     +     ++++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:50:27
    |
 50 |     let p0 = mm_xor_si128(*prev, mm_slli_si128::<4>(*prev));
    |              ------------ ^^^^^ expected `BitVec<128>`, found `__m128i`
    |              |
    |              arguments to this function are incorrect
    |
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:459:8
    |
459 | pub fn mm_xor_si128(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 50 |     let p0 = mm_xor_si128((*prev).into(), mm_slli_si128::<4>(*prev));
    |                           +     ++++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:53:26
    |
 53 |     *next = mm_xor_si128(*next, p2);
    |             ------------ ^^^^^ expected `BitVec<128>`, found `__m128i`
    |             |
    |             arguments to this function are incorrect
    |
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:459:8
    |
459 | pub fn mm_xor_si128(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 53 |     *next = mm_xor_si128((*next).into(), p2);
    |                          +     ++++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:53:13
   |
53 |     *next = mm_xor_si128(*next, p2);
   |     -----   ^^^^^^^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |     |
   |     expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
53 |     *next = mm_xor_si128(*next, p2).into();
   |                                    +++++++

error[E0599]: no method named `declassify_ref_mut` found for array `[u8; 12]` in the current scope
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-chacha20poly1305-0.0.4/src/impl_aead_trait.rs:156:27
    |
156 |                 new_nonce.declassify_ref_mut(),
    |                           ^^^^^^^^^^^^^^^^^^
    |
help: there is a method `declassify_ref` with a similar name
    |
156 -                 new_nonce.declassify_ref_mut(),
156 +                 new_nonce.declassify_ref(),
    |

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:66:17
   |
66 |         *self = mm_loadu_si128(b);
   |         -----   ^^^^^^^^^^^^^^^^^ expected `__m128i`, found `BitVec<128>`
   |         |
   |         expected due to the type of this binding
   |
   = note: expected struct `core::arch::x86_64::__m128i`
              found struct `core_models::abstractions::bitvec::BitVec<128>`
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
   |
66 |         *self = mm_loadu_si128(b).into();
   |                                  +++++++

error[E0308]: mismatched types
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:73:33
   |
73 |         mm_storeu_si128_u8(out, *self);
   |         ------------------      ^^^^^ expected `BitVec<128>`, found `__m128i`
   |         |
   |         arguments to this function are incorrect
   |
   = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
              found struct `core::arch::x86_64::__m128i`
note: function defined here
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:62:8
   |
62 | pub fn mm_storeu_si128_u8(output: &mut [u8], vector: Vec128) {
   |        ^^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
   |
73 |         mm_storeu_si128_u8(out, (*self).into());
   |                                 +     ++++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/aes_core.rs:85:45
    |
 85 |         let out_vec = mm_xor_si128(inp_vec, *self);
    |                       ------------          ^^^^^ expected `BitVec<128>`, found `__m128i`
    |                       |
    |                       arguments to this function are incorrect
    |
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:459:8
    |
459 | pub fn mm_xor_si128(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 85 |         let out_vec = mm_xor_si128(inp_vec, (*self).into());
    |                                             +     ++++++++

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:77:16
    |
 77 |     let p_lo = mm_clmulepi64_si128::<0x00>(a, b);
    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:77:44
    |
 77 |     let p_lo = mm_clmulepi64_si128::<0x00>(a, b);
    |                                            ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:77:47
    |
 77 |     let p_lo = mm_clmulepi64_si128::<0x00>(a, b);
    |                                               ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:769:8
    |
769 | pub fn mm_clmulepi64_si128<const IMM8: i32>(a: Vec128, b: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 77 |     let p_lo = mm_clmulepi64_si128::<0x00>(a.into(), b);
    |                                             +++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 77 |     let p_lo = mm_clmulepi64_si128::<0x00>(a, b.into());
    |                                                +++++++

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:79:16
    |
 79 |     let p_hi = mm_clmulepi64_si128::<0x11>(a, b);
    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:79:44
    |
 79 |     let p_hi = mm_clmulepi64_si128::<0x11>(a, b);
    |                                            ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:79:47
    |
 79 |     let p_hi = mm_clmulepi64_si128::<0x11>(a, b);
    |                                               ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:769:8
    |
769 | pub fn mm_clmulepi64_si128<const IMM8: i32>(a: Vec128, b: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 79 |     let p_hi = mm_clmulepi64_si128::<0x11>(a.into(), b);
    |                                             +++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 79 |     let p_hi = mm_clmulepi64_si128::<0x11>(a, b.into());
    |                                                +++++++

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:84:30
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a, a));
    |                              ^^^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:84:48
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a, a));
    |                                                ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:84:51
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a, a));
    |                                                   ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:588:8
    |
588 | pub fn mm_unpackhi_epi64(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a.into(), a), mm_unpacklo_epi64(a, a));
    |                                                 +++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a.into()), mm_unpacklo_epi64(a, a));
    |                                                    +++++++

error[E0599]: no method named `declassify_ref_mut` found for array `[u8; 32]` in the current scope
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-chacha20poly1305-0.0.4/src/impl_aead_trait.rs:175:29
    |
175 |                 &mut subkey.declassify_ref_mut(),
    |                             ^^^^^^^^^^^^^^^^^^
    |
help: there is a method `declassify_ref` with a similar name
    |
175 -                 &mut subkey.declassify_ref_mut(),
175 +                 &mut subkey.declassify_ref(),
    |

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:84:55
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a, a));
    |                                                       ^^^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:84:73
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a, a));
    |                                                                         ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:84:76
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a, a));
    |                                                                            ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:757:8
    |
757 | pub fn mm_unpacklo_epi64(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a.into(), a));
    |                                                                          +++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 84 |     let a_xor = mm_xor_si128(mm_unpackhi_epi64(a, a), mm_unpacklo_epi64(a, a.into()));
    |                                                                             +++++++

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:85:30
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b, b));
    |                              ^^^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:85:48
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b, b));
    |                                                ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:85:51
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b, b));
    |                                                   ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:588:8
    |
588 | pub fn mm_unpackhi_epi64(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b.into(), b), mm_unpacklo_epi64(b, b));
    |                                                 +++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b.into()), mm_unpacklo_epi64(b, b));
    |                                                    +++++++

error[E0308]: arguments to this function are incorrect
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:85:55
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b, b));
    |                                                       ^^^^^^^^^^^^^^^^^
    |
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:85:73
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b, b));
    |                                                                         ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: expected `BitVec<128>`, found `__m128i`
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:85:76
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b, b));
    |                                                                            ^
    = note: expected struct `core_models::abstractions::bitvec::BitVec<128>`
               found struct `core::arch::x86_64::__m128i`
note: function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-intrinsics-0.0.4/src/avx2.rs:757:8
    |
757 | pub fn mm_unpacklo_epi64(lhs: Vec128, rhs: Vec128) -> Vec128 {
    |        ^^^^^^^^^^^^^^^^^
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b.into(), b));
    |                                                                          +++++++
help: call `Into::into` on this expression to convert `core::arch::x86_64::__m128i` into `core_models::abstractions::bitvec::BitVec<128>`
    |
 85 |     let b_xor = mm_xor_si128(mm_unpackhi_epi64(b, b), mm_unpacklo_epi64(b, b.into()));
    |                                                                             +++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:103:35
    |
103 |         FieldElement::from_vec128(res_high),
    |         ------------------------- ^^^^^^^^ expected `__m128i`, found `BitVec<128>`
    |         |
    |         arguments to this function are incorrect
    |
    = note: expected struct `core::arch::x86_64::__m128i`
               found struct `core_models::abstractions::bitvec::BitVec<128>`
note: associated function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:26:8
    |
 26 |     fn from_vec128(vec: __m128i) -> Self {
    |        ^^^^^^^^^^^ ------------
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
    |
103 |         FieldElement::from_vec128(res_high.into()),
    |                                           +++++++

error[E0308]: mismatched types
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:104:35
    |
104 |         FieldElement::from_vec128(res_low),
    |         ------------------------- ^^^^^^^ expected `__m128i`, found `BitVec<128>`
    |         |
    |         arguments to this function are incorrect
    |
    = note: expected struct `core::arch::x86_64::__m128i`
               found struct `core_models::abstractions::bitvec::BitVec<128>`
note: associated function defined here
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-aesgcm-0.0.4/src/platform/x64/gf128_core.rs:26:8
    |
 26 |     fn from_vec128(vec: __m128i) -> Self {
    |        ^^^^^^^^^^^ ------------
help: call `Into::into` on this expression to convert `core_models::abstractions::bitvec::BitVec<128>` into `core::arch::x86_64::__m128i`
    |
104 |         FieldElement::from_vec128(res_low.into()),
    |                                          +++++++

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 32]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-p256-0.0.4/src/impl_kem.rs:26:46
   |
26 |         if !super::p256::dh_initiator(ek, dk.declassify_ref_mut()) {
   |                                              ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
26 -         if !super::p256::dh_initiator(ek, dk.declassify_ref_mut()) {
26 +         if !super::p256::dh_initiator(ek, dk.declassify_ref()) {
   |

error[E0599]: no method named `declassify_ref_mut` found for array `[u8; 12]` in the current scope
   --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-chacha20poly1305-0.0.4/src/impl_aead_trait.rs:176:32
    |
176 |                 &mut new_nonce.declassify_ref_mut(),
    |                                ^^^^^^^^^^^^^^^^^^
    |
help: there is a method `declassify_ref` with a similar name
    |
176 -                 &mut new_nonce.declassify_ref_mut(),
176 +                 &mut new_nonce.declassify_ref(),
    |

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 64]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-p256-0.0.4/src/impl_kem.rs:47:42
   |
47 |         if !super::p256::dh_responder(ss.declassify_ref_mut(), ek, rand.declassify_ref()) {
   |                                          ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
47 -         if !super::p256::dh_responder(ss.declassify_ref_mut(), ek, rand.declassify_ref()) {
47 +         if !super::p256::dh_responder(ss.declassify_ref(), ek, rand.declassify_ref()) {
   |

error[E0599]: no method named `declassify_ref_mut` found for mutable reference `&mut [u8; 64]` in the current scope
  --> /home/user/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/libcrux-p256-0.0.4/src/impl_kem.rs:71:42
   |
71 |         if !super::p256::dh_responder(ss.declassify_ref_mut(), ct, dk.declassify_ref()) {
   |                                          ^^^^^^^^^^^^^^^^^^
   |
help: there is a method `declassify_ref` with a similar name
   |
71 -         if !super::p256::dh_responder(ss.declassify_ref_mut(), ct, dk.declassify_ref()) {
71 +         if !super::p256::dh_responder(ss.declassify_ref(), ct, dk.declassify_ref()) {
   |

For more information about this error, try `rustc --explain E0308`.
error: could not compile `libcrux-aesgcm` (lib) due to 28 previous errors
error: could not compile `libcrux-chacha20poly1305` (lib) due to 6 previous errors
error: could not compile `libcrux-p256` (lib) due to 4 previous errors
warning: hax: running `cargo build` was not successful, continuing anyway.

securedrop-protocol/Cargo.toml

cfm · 2025-12-06T00:32:42Z

.github/workflows/hax.yml

+      packages: read
+
+    env:
+      HAX_IMAGE: ghcr.io/cfm/hax@sha256:9200676dcc475677fb18b8f07ea1da1aeb63680eedec8a78c26a760343b0d6a4


I've built this from https://github.com/cryspen/hax/blob/4019185e9c96836c51081519bb6b7e51edee1f4c/README.md?plain=1#L159-L170 just to have something reproducible in CI, but we'll probably want to pin an image that we build and publish ourselves.

Or use https://github.com/hacspec/hax-actions. It should be as fast or faster than this with caching, but it didn't immediately work for me during #125, and I wound up needing able to build with a specific (newer) Rust toolchain anyway.

If that can help you make a decision, we always use https://github.com/hacspec/hax-actions. We can help you debugging if you have problems with this method (I am less familiar with the docker method so I am not sure I can help with it). We can also help if you need a specific hax toolchain (although this doesn't work well with caching so you'll experience longer CI times).

Thanks, @maximebuyse! We'll take you up on that offer before this lands in main. :-)

<https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3> via <https://hax.cryspen.com/manual/fstar/quick_start/>.

cfm · 2025-12-10T00:26:13Z

This worked in 44c3158 with pins in 2d320b7 to cryspen/libcrux#1263, thanks to @maximebuyse. There's an unrelated Rust error that I'm looking into via hacspec/hax-actions or a new Docker image built from the Rust nightly channel.

cfm · 2025-12-11T01:34:53Z

As of 3a6b438, this now fails usefully, pointing to changes we'll need to make in the implementation to make it hax-friendly:

error: [HAX0011] The support in hax of function with one or more inputs of type `&mut _` is limited.
Only trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected.

This is discussed in issue https://github.com/hacspec/hax/issues/1405.
Please upvote or comment this issue if you see this error message.
Note: the error was labeled with context `AndMutDefsite`.

  --> src/sign.rs:31:16
   |
31 |     pub fn new(mut rng: &mut impl CryptoRng) -> Result<SigningKey, Error> {
   |                ^^^^^^^
   |
error: [HAX0003] The mutation of this &mut is not allowed here.

rocodes · 2026-01-19T21:31:08Z

@cfm based on this so far, any pointers that make it easier (or harder) to integrate hax in terms of code style are welcome. I'm working on #140, and while I'm at it, if I'm refactoring I might as well do it in a hax-friendly way. (For later we might also think of adding some custom lint rules if we discover there are patterns to follow/avoid).

cfm · 2026-01-31T01:44:03Z

@rocodes, the big one is going to be avoiding muts. But we can deal with all of it incrementally by tuning what we extract for verification, working inside-out from #154. So I say full steam ahead on #140!

cfm added 2 commits December 3, 2025 16:42

chore: update all libcrux crates to published v0.0.4

0e932aa

chore: add "cfg(hax)" target

b75fb3c

Per <https://hax.cryspen.com/manual/fstar/quick_start/>.

cfm added the proof of concept label Dec 4, 2025

redshiftzero reviewed Dec 4, 2025

View reviewed changes

securedrop-protocol/Cargo.toml Show resolved Hide resolved

cfm commented Dec 6, 2025

View reviewed changes

cfm added 4 commits December 9, 2025 15:24

ci(hax): extract hax → F*

ac7be3f

build: pin to cryspen/libcrux#1263

2d320b7

build(hax): import recommended Makefile for hax → F*

72dd991

<https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3> via <https://hax.cryspen.com/manual/fstar/quick_start/>.

ci(hax): diff extracted F*

f2f97aa

cfm force-pushed the hax branch from c15496c to f2f97aa Compare December 9, 2025 23:24

chore: "cargo hax into fstar"

44c3158

ci(hax): use $HAX_IMAGE built with latest nightly Rust

3a6b438

cfm force-pushed the hax branch from dcfbb5b to 3a6b438 Compare December 11, 2025 01:15

This was referenced Dec 15, 2025

research spike on verification tools (to inform implementation plan) #125

Closed

chore: update all libcrux crates to published v0.0.4 #134

Merged

cfm added the verification label Jan 13, 2026

cfm mentioned this pull request Jan 13, 2026

first minimal target for end-to-end proof coverage #154

Open

4 tasks

maximebuyse mentioned this pull request Feb 4, 2026

Fix hax extraction of crates depending on some libcrux crates. cryspen/libcrux#1263

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

proof of concept: hax#131

proof of concept: hax#131
cfm wants to merge 8 commits intomainfrom
hax

cfm commented Dec 4, 2025 •

edited

Loading

Uh oh!

cfm commented Dec 4, 2025

Uh oh!

Uh oh!

cfm Dec 6, 2025

Uh oh!

cfm Dec 17, 2025

Uh oh!

maximebuyse Dec 18, 2025

Uh oh!

cfm Dec 20, 2025

Uh oh!

cfm commented Dec 10, 2025

Uh oh!

cfm commented Dec 11, 2025

Uh oh!

rocodes commented Jan 19, 2026

Uh oh!

cfm commented Jan 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

cfm commented Dec 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

cfm commented Dec 4, 2025

Uh oh!

Uh oh!

cfm Dec 6, 2025

Choose a reason for hiding this comment

Uh oh!

cfm Dec 17, 2025

Choose a reason for hiding this comment

Uh oh!

maximebuyse Dec 18, 2025

Choose a reason for hiding this comment

Uh oh!

cfm Dec 20, 2025

Choose a reason for hiding this comment

Uh oh!

cfm commented Dec 10, 2025

Uh oh!

cfm commented Dec 11, 2025

Uh oh!

rocodes commented Jan 19, 2026

Uh oh!

cfm commented Jan 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

cfm commented Dec 4, 2025 •

edited

Loading