update hax extraction

libcrux-ml-kem/hax.py

@@ -101,11 +101,17 @@ def __call__(self, parser, args, values, option_string=None) -> None:
  )
 
  # Extract ml-kem
- include_str = "+** -libcrux_ml_kem::types::index_impls::**"
+ include_str = (
+ "+** -libcrux_ml_kem::types::index_impls::** -libcrux_ml_kem::kem::**"
+ )
  interface_include = "+**"
  cargo_hax_into = [
  "cargo",
  "hax",
+ "-C",
+ "--features",
+ "pre-verification",
+ ";",
  "into",
  "-i",
  include_str,

libcrux-ml-kem/src/mlkem1024.rs

@@ -47,7 +47,8 @@ pub type MlKem1024KeyPair = MlKemKeyPair<SECRET_KEY_SIZE_1024, CPA_PKE_PUBLIC_KE
 
 // Instantiate the different functions.
 macro_rules! instantiate {
- ($modp:ident, $p:path) => {
+ ($modp:ident, $p:path, $doc:expr) => {
+ #[doc = $doc]
  pub mod $modp {
  use super::*;
  use $p as p;
@@ -200,11 +201,11 @@ macro_rules! instantiate {
 
 // Instantiations
 
-instantiate! {portable, ind_cca::instantiations::portable}
+instantiate! {portable, ind_cca::instantiations::portable, "Portable ML-KEM 1024"}
 #[cfg(feature = "simd256")]
-instantiate! {avx2, ind_cca::instantiations::avx2}
+instantiate! {avx2, ind_cca::instantiations::avx2, "AVX2 Optimised ML-KEM 1024"}
 #[cfg(feature = "simd128")]
-instantiate! {neon, ind_cca::instantiations::neon}
+instantiate! {neon, ind_cca::instantiations::neon, "Neon Optimised ML-KEM 1024"}
 
 /// Validate a public key.
 ///

libcrux-ml-kem/src/mlkem512.rs

@@ -45,7 +45,8 @@ pub type MlKem512KeyPair = MlKemKeyPair<SECRET_KEY_SIZE_512, CPA_PKE_PUBLIC_KEY_
 
 // Instantiate the different functions.
 macro_rules! instantiate {
- ($modp:ident, $p:path) => {
+ ($modp:ident, $p:path, $doc:expr) => {
+ #[doc = $doc]
  pub mod $modp {
  use super::*;
  use $p as p;
@@ -196,11 +197,11 @@ macro_rules! instantiate {
 
 // Instantiations
 
-instantiate! {portable, ind_cca::instantiations::portable}
+instantiate! {portable, ind_cca::instantiations::portable, "Portable ML-KEM 512"}
 #[cfg(feature = "simd256")]
-instantiate! {avx2, ind_cca::instantiations::avx2}
+instantiate! {avx2, ind_cca::instantiations::avx2, "AVX2 Optimised ML-KEM 512"}
 #[cfg(feature = "simd128")]
-instantiate! {neon, ind_cca::instantiations::neon}
+instantiate! {neon, ind_cca::instantiations::neon, "Neon Optimised ML-KEM 512"}
 
 /// Validate a public key.
 ///

libcrux-ml-kem/src/mlkem768.rs

@@ -46,7 +46,8 @@ pub type MlKem768KeyPair = MlKemKeyPair<SECRET_KEY_SIZE_768, CPA_PKE_PUBLIC_KEY_
 
 // Instantiate the different functions.
 macro_rules! instantiate {
- ($modp:ident, $p:path) => {
+ ($modp:ident, $p:path, $doc:expr) => {
+ #[doc = $doc]
  pub mod $modp {
  use super::*;
  use $p as p;
@@ -196,11 +197,11 @@ macro_rules! instantiate {
 
 // Instantiations
 
-instantiate! {portable, ind_cca::instantiations::portable}
+instantiate! {portable, ind_cca::instantiations::portable, "Portable ML-KEM 768"}
 #[cfg(feature = "simd256")]
-instantiate! {avx2, ind_cca::instantiations::avx2}
+instantiate! {avx2, ind_cca::instantiations::avx2, "AVX2 Optimised ML-KEM 768"}
 #[cfg(feature = "simd128")]
-instantiate! {neon, ind_cca::instantiations::neon}
+instantiate! {neon, ind_cca::instantiations::neon, "Neon Optimised ML-KEM 768"}
 
 /// Validate a public key.
 ///

libcrux-sha3/proofs/fstar/extraction/Libcrux_sha3.Avx2.X4.Incremental.fsti

@@ -3,42 +3,46 @@ module Libcrux_sha3.Avx2.X4.Incremental
 open Core
 open FStar.Mul
 
-type t_KeccakState4 = { f_state:t_Array Libcrux_sha3.Neon.X2.Incremental.t_KeccakState2 (sz 2) }
+/// The Keccak state for the incremental API.
+type t_KeccakState = { f_state:t_Array Libcrux_sha3.Neon.X2.Incremental.t_KeccakState (sz 2) }
 
 /// Initialise the state and perform up to 4 absorbs at the same time,
 /// using two [`KeccakState4`].
 /// **PANICS** when `N` is not 2, 3, or 4.
 val v__shake128_absorb_finalxN (v_N: usize) (input: t_Array (t_Array u8 (sz 34)) v_N)
- : Prims.Pure t_KeccakState4 Prims.l_True (fun _ -> Prims.l_True)
+ : Prims.Pure t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
 
 /// Squeeze up to 3 x 4 (N) blocks in parallel, using two [`KeccakState4`].
 /// Each block is of size `LEN`.
 /// **PANICS** when `N` is not 2, 3, or 4.
-val v__shake128_squeeze3xN (v_LEN v_N: usize) (state: t_KeccakState4)
- : Prims.Pure (t_KeccakState4 & t_Array (t_Array u8 v_LEN) v_N)
+val v__shake128_squeeze3xN (v_LEN v_N: usize) (state: t_KeccakState)
+ : Prims.Pure (t_KeccakState & t_Array (t_Array u8 v_LEN) v_N)
  Prims.l_True
  (fun _ -> Prims.l_True)
 
 /// Squeeze up to 4 (N) blocks in parallel, using two [`KeccakState4`].
 /// Each block is of size `LEN`.
 /// **PANICS** when `N` is not 2, 3, or 4.
-val v__shake128_squeezexN (v_LEN v_N: usize) (state: t_KeccakState4)
- : Prims.Pure (t_KeccakState4 & t_Array (t_Array u8 v_LEN) v_N)
+val v__shake128_squeezexN (v_LEN v_N: usize) (state: t_KeccakState)
+ : Prims.Pure (t_KeccakState & t_Array (t_Array u8 v_LEN) v_N)
  Prims.l_True
  (fun _ -> Prims.l_True)
 
-val shake128_absorb_final (s: t_KeccakState4) (data0 data1 data2 data3: t_Slice u8)
- : Prims.Pure t_KeccakState4 Prims.l_True (fun _ -> Prims.l_True)
+/// Absorb
+val shake128_absorb_final (s: t_KeccakState) (data0 data1 data2 data3: t_Slice u8)
+ : Prims.Pure t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
 
-/// Initialise the [`KeccakState4`].
-val shake128_init: Prims.unit -> Prims.Pure t_KeccakState4 Prims.l_True (fun _ -> Prims.l_True)
+/// Initialise the [`KeccakState`].
+val shake128_init: Prims.unit -> Prims.Pure t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
 
-val shake128_squeeze_first_three_blocks (s: t_KeccakState4) (out0 out1 out2 out3: t_Slice u8)
- : Prims.Pure (t_KeccakState4 & t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8)
+/// Squeeze three blocks
+val shake128_squeeze_first_three_blocks (s: t_KeccakState) (out0 out1 out2 out3: t_Slice u8)
+ : Prims.Pure (t_KeccakState & t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8)
  Prims.l_True
  (fun _ -> Prims.l_True)
 
-val shake128_squeeze_next_block (s: t_KeccakState4) (out0 out1 out2 out3: t_Slice u8)
- : Prims.Pure (t_KeccakState4 & t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8)
+/// Squeeze another block
+val shake128_squeeze_next_block (s: t_KeccakState) (out0 out1 out2 out3: t_Slice u8)
+ : Prims.Pure (t_KeccakState & t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8)
  Prims.l_True
  (fun _ -> Prims.l_True)

libcrux-sha3/proofs/fstar/extraction/Libcrux_sha3.Neon.X2.Incremental.fsti

@@ -3,11 +3,8 @@ module Libcrux_sha3.Neon.X2.Incremental
 open Core
 open FStar.Mul
 
-unfold
-let t_KeccakState2Internal =
- Libcrux_sha3.Generic_keccak.t_KeccakState (sz 2) Core.Core_arch.Arm_shared.Neon.t_uint64x2_t
-
-type t_KeccakState2 = {
+/// The Keccak state for the incremental API.
+type t_KeccakState = {
  f_state:Libcrux_sha3.Generic_keccak.t_KeccakState (sz 2)
  Core.Core_arch.Arm_shared.Neon.t_uint64x2_t
 }
@@ -16,32 +13,37 @@ type t_KeccakState2 = {
 /// using two [`KeccakState2`].
 /// **PANICS** when `N` is not 2, 3, or 4.
 val v__shake128_absorb_finalxN (v_N: usize) (input: t_Array (t_Array u8 (sz 34)) v_N)
- : Prims.Pure (t_Array t_KeccakState2 (sz 2)) Prims.l_True (fun _ -> Prims.l_True)
+ : Prims.Pure (t_Array t_KeccakState (sz 2)) Prims.l_True (fun _ -> Prims.l_True)
 
 /// Squeeze up to 3 x 4 (N) blocks in parallel, using two [`KeccakState2`].
 /// Each block is of size `LEN`.
 /// **PANICS** when `N` is not 2, 3, or 4.
-val v__shake128_squeeze3xN (v_LEN v_N: usize) (state: t_Array t_KeccakState2 (sz 2))
- : Prims.Pure (t_Array t_KeccakState2 (sz 2) & t_Array (t_Array u8 v_LEN) v_N)
+val v__shake128_squeeze3xN (v_LEN v_N: usize) (state: t_Array t_KeccakState (sz 2))
+ : Prims.Pure (t_Array t_KeccakState (sz 2) & t_Array (t_Array u8 v_LEN) v_N)
  Prims.l_True
  (fun _ -> Prims.l_True)
 
 /// Squeeze up to 4 (N) blocks in parallel, using two [`KeccakState2`].
 /// Each block is of size `LEN`.
 /// **PANICS** when `N` is not 2, 3, or 4.
-val v__shake128_squeezexN (v_LEN v_N: usize) (state: t_Array t_KeccakState2 (sz 2))
- : Prims.Pure (t_Array t_KeccakState2 (sz 2) & t_Array (t_Array u8 v_LEN) v_N)
+val v__shake128_squeezexN (v_LEN v_N: usize) (state: t_Array t_KeccakState (sz 2))
+ : Prims.Pure (t_Array t_KeccakState (sz 2) & t_Array (t_Array u8 v_LEN) v_N)
  Prims.l_True
  (fun _ -> Prims.l_True)
 
-val shake128_absorb_final (s: t_KeccakState2) (data0 data1: t_Slice u8)
- : Prims.Pure t_KeccakState2 Prims.l_True (fun _ -> Prims.l_True)
+/// Shake128 absorb `data0` and `data1` in the [`KeccakState`] `s`.
+val shake128_absorb_final (s: t_KeccakState) (data0 data1: t_Slice u8)
+ : Prims.Pure t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
 
 /// Initialise the `KeccakState2`.
-val shake128_init: Prims.unit -> Prims.Pure t_KeccakState2 Prims.l_True (fun _ -> Prims.l_True)
+val shake128_init: Prims.unit -> Prims.Pure t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
 
-val shake128_squeeze_first_three_blocks (s: t_KeccakState2) (out0 out1: t_Slice u8)
- : Prims.Pure (t_KeccakState2 & t_Slice u8 & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
+/// Squeeze 2 times the first three blocks in parallel in the
+/// [`KeccakState`] and return the output in `out0` and `out1`.
+val shake128_squeeze_first_three_blocks (s: t_KeccakState) (out0 out1: t_Slice u8)
+ : Prims.Pure (t_KeccakState & t_Slice u8 & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
 
-val shake128_squeeze_next_block (s: t_KeccakState2) (out0 out1: t_Slice u8)
- : Prims.Pure (t_KeccakState2 & t_Slice u8 & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
+/// Squeeze 2 times the next block in parallel in the
+/// [`KeccakState`] and return the output in `out0` and `out1`.
+val shake128_squeeze_next_block (s: t_KeccakState) (out0 out1: t_Slice u8)
+ : Prims.Pure (t_KeccakState & t_Slice u8 & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

libcrux-sha3/proofs/fstar/extraction/Libcrux_sha3.Portable.Incremental.fsti

@@ -4,27 +4,27 @@ open Core
 open FStar.Mul
 
 /// Absorb
-val shake128_absorb_final (s: Libcrux_sha3.Portable.t_KeccakState1) (data0: t_Slice u8)
- : Prims.Pure Libcrux_sha3.Portable.t_KeccakState1 Prims.l_True (fun _ -> Prims.l_True)
+val shake128_absorb_final (s: Libcrux_sha3.Portable.t_KeccakState) (data0: t_Slice u8)
+ : Prims.Pure Libcrux_sha3.Portable.t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
 
 /// Initialise the SHAKE state.
 val shake128_init: Prims.unit
- -> Prims.Pure Libcrux_sha3.Portable.t_KeccakState1 Prims.l_True (fun _ -> Prims.l_True)
+ -> Prims.Pure Libcrux_sha3.Portable.t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
 
 /// Squeeze five blocks
-val shake128_squeeze_first_five_blocks (s: Libcrux_sha3.Portable.t_KeccakState1) (out0: t_Slice u8)
- : Prims.Pure (Libcrux_sha3.Portable.t_KeccakState1 & t_Slice u8)
+val shake128_squeeze_first_five_blocks (s: Libcrux_sha3.Portable.t_KeccakState) (out0: t_Slice u8)
+ : Prims.Pure (Libcrux_sha3.Portable.t_KeccakState & t_Slice u8)
  Prims.l_True
  (fun _ -> Prims.l_True)
 
 /// Squeeze three blocks
-val shake128_squeeze_first_three_blocks (s: Libcrux_sha3.Portable.t_KeccakState1) (out0: t_Slice u8)
- : Prims.Pure (Libcrux_sha3.Portable.t_KeccakState1 & t_Slice u8)
+val shake128_squeeze_first_three_blocks (s: Libcrux_sha3.Portable.t_KeccakState) (out0: t_Slice u8)
+ : Prims.Pure (Libcrux_sha3.Portable.t_KeccakState & t_Slice u8)
  Prims.l_True
  (fun _ -> Prims.l_True)
 
 /// Squeeze another block
-val shake128_squeeze_next_block (s: Libcrux_sha3.Portable.t_KeccakState1) (out0: t_Slice u8)
- : Prims.Pure (Libcrux_sha3.Portable.t_KeccakState1 & t_Slice u8)
+val shake128_squeeze_next_block (s: Libcrux_sha3.Portable.t_KeccakState) (out0: t_Slice u8)
+ : Prims.Pure (Libcrux_sha3.Portable.t_KeccakState & t_Slice u8)
  Prims.l_True
  (fun _ -> Prims.l_True)

libcrux-sha3/proofs/fstar/extraction/Libcrux_sha3.Portable.fsti

@@ -23,4 +23,5 @@ val shake128 (digest data: t_Slice u8)
 val shake256 (digest data: t_Slice u8)
  : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
 
-type t_KeccakState1 = { f_state:Libcrux_sha3.Generic_keccak.t_KeccakState (sz 1) u64 }
+/// The Keccak state for the incremental API.
+type t_KeccakState = { f_state:Libcrux_sha3.Generic_keccak.t_KeccakState (sz 1) u64 }

libcrux-sha3/proofs/fstar/extraction/Libcrux_sha3.Traits.fsti

@@ -11,8 +11,8 @@ let _ =
 
 /// A Keccak Item
 /// This holds the internal state and depends on the architecture.
-class t_KeccakStateItem (v_Self: Type0) (v_N: usize) = {
- [@@@ FStar.Tactics.Typeclasses.no_method]_super_7919791445461910775:Libcrux_sha3.Traits.Internal.t_KeccakItem
+class t_KeccakStateItem (#v_Self: Type0) (v_N: usize) = {
+ [@@@ FStar.Tactics.Typeclasses.no_method]_super_1179490486619621168:Libcrux_sha3.Traits.Internal.t_KeccakItem
  v_Self v_N
 }
 
@@ -23,5 +23,4 @@ let impl
  (#[FStar.Tactics.Typeclasses.tcresolve ()]
  i1:
  Libcrux_sha3.Traits.Internal.t_KeccakItem v_T v_N)
- : t_KeccakStateItem v_T v_N =
- { _super_7919791445461910775 = FStar.Tactics.Typeclasses.solve; __marker_trait = () }
+ : t_KeccakStateItem #v_T v_N = { _super_1179490486619621168 = FStar.Tactics.Typeclasses.solve }

libcrux-sha3/proofs/fstar/extraction/Libcrux_sha3.fsti

@@ -17,7 +17,7 @@ type t_Algorithm =
  | Algorithm_Sha512 : t_Algorithm
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Convert.t_From u32 t_Algorithm =
+let impl_1: Core.Convert.t_From #u32 #t_Algorithm =
  {
  f_from_pre = (fun (v: t_Algorithm) -> true);
  f_from_post = (fun (v: t_Algorithm) (out: u32) -> true);
@@ -35,21 +35,8 @@ let discriminant_Algorithm_Sha512: u32 = 4ul
 
 val t_Algorithm_cast_to_repr (x: t_Algorithm) : Prims.Pure u32 Prims.l_True (fun _ -> Prims.l_True)
 
-/// A SHA3 224 Digest
-unfold
-let t_Sha3_224Digest = t_Array u8 (sz 28)
-
-/// A SHA3 256 Digest
-unfold
-let t_Sha3_256Digest = t_Array u8 (sz 32)
-
-/// A SHA3 384 Digest
-unfold
-let t_Sha3_384Digest = t_Array u8 (sz 48)
-
-/// A SHA3 512 Digest
-unfold
-let t_Sha3_512Digest = t_Array u8 (sz 64)
+val from__panic_cold_explicit: Prims.unit
+ -> Prims.Pure Rust_primitives.Hax.t_Never Prims.l_True (fun _ -> Prims.l_True)
 
 /// Returns the output size of a digest.
 val digest_size (mode: t_Algorithm) : Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
@@ -99,7 +86,7 @@ val shake256 (v_BYTES: usize) (data: t_Slice u8)
  : Prims.Pure (t_Array u8 v_BYTES) Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Convert.t_From t_Algorithm u32 =
+let impl: Core.Convert.t_From #t_Algorithm #u32 =
  {
  f_from_pre = (fun (v: u32) -> true);
  f_from_post = (fun (v: u32) (out: t_Algorithm) -> true);
@@ -112,7 +99,7 @@ let impl: Core.Convert.t_From t_Algorithm u32 =
  | 3ul -> Algorithm_Sha384 <: t_Algorithm
  | 4ul -> Algorithm_Sha512 <: t_Algorithm
  | _ ->
- Rust_primitives.Hax.never_to_any (Core.Panicking.panic "explicit panic"
+ Rust_primitives.Hax.never_to_any (from__panic_cold_explicit ()
  <:
  Rust_primitives.Hax.t_Never)
  }