Move hax-lib-macros dependency to a feature

Cargo.toml

@@ -18,14 +18,15 @@ rand = "0.8.0"
 hex = "0.4.3"
 tracing = "0.1"
 libcrux = { version = "0.0.2-pre.2", features = ["rand"] }
-hax-lib-macros = { git = "https://github.com/hacspec/hax" }
+hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true }
 
 
 [features]
 default = ["api"]
 test_utils = []
 secret_integers = []
 api = []             # The streaming Rust API that everyone should use but is not hacspec.
+hax-pv = ["dep:hax-lib-macros"]
 
 [dev-dependencies]
 bertie = { path = ".", features = ["test_utils"] }

src/tls13cert.rs

@@ -15,8 +15,7 @@
 //!     }
 //!     BitString // 0x03
 //! }
-//! ```
-
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
 #[cfg(not(feature = "secret_integers"))]
@@ -283,7 +282,7 @@ fn read_spki(cert: &Bytes, mut offset: usize) -> Result<Spki, Asn1Error> {
 /// certificate.
 ///
 /// Returns the start offset within the `cert` bytes and length of the key.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn verification_key_from_cert(cert: &Bytes) -> Result<Spki, Asn1Error> {
     // An x509 cert is an ASN.1 sequence of [Certificate, SignatureAlgorithm, Signature].
     // Take the first sequence inside the outer because we're interested in the
@@ -304,7 +303,7 @@ pub(crate) fn verification_key_from_cert(cert: &Bytes) -> Result<Spki, Asn1Error
 }
 
 /// Read the EC PK from the cert as uncompressed point.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn ecdsa_public_key(
     cert: &Bytes,
     indices: CertificateKey,
@@ -317,7 +316,7 @@ pub(crate) fn ecdsa_public_key(
     Ok(cert.slice(offset + 1, len - 1)) // Drop the 0x04 here.
 }
 
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn rsa_public_key(
     cert: &Bytes,
     indices: CertificateKey,
@@ -392,7 +391,7 @@ pub(crate) fn rsa_private_key(key: &Bytes) -> Result<Bytes, Asn1Error> {
 ///
 /// On input of a `certificate` and `spki`, return a [`PublicVerificationKey`]
 /// if successful, or an [`Asn1Error`] otherwise.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn cert_public_key(
     certificate: &Bytes,
     spki: &Spki,

src/tls13crypto.rs

@@ -1,12 +1,12 @@
-use std::fmt::Display;
-
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 use libcrux::{
     kem::{Ct, PrivateKey, PublicKey},
     signature::rsa_pss::{RsaPssKeySize, RsaPssPrivateKey, RsaPssPublicKey},
     *,
 };
 use rand::{CryptoRng, RngCore};
+use std::fmt::Display;
 
 use crate::tls13utils::{
     check_mem, eq, length_u16_encoded, tlserr, Bytes, Error, TLSError, CRYPTO_ERROR,
@@ -109,7 +109,7 @@ impl HashAlgorithm {
     /// Hash `data` with the given `algorithm`.
     ///
     /// Returns the digest or an [`TLSError`].
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn hash(&self, data: &Bytes) -> Result<Bytes, TLSError> {
         Ok(digest::hash(self.libcrux_algorithm()?, &data.declassify()).into())
     }
@@ -141,7 +141,7 @@ impl HashAlgorithm {
 /// Compute the HMAC tag.
 ///
 /// Returns the tag [`Hmac`] or a [`TLSError`].
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn hmac_tag(alg: &HashAlgorithm, mk: &MacKey, input: &Bytes) -> Result<Hmac, TLSError> {
     Ok(hmac::hmac(
         alg.hmac_algorithm()?,
@@ -155,7 +155,7 @@ pub(crate) fn hmac_tag(alg: &HashAlgorithm, mk: &MacKey, input: &Bytes) -> Resul
 /// Verify a given HMAC `tag`.
 ///
 /// Returns `()` if successful or a [`TLSError`].
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn hmac_verify(
     alg: &HashAlgorithm,
     mk: &MacKey,
@@ -186,7 +186,7 @@ fn hkdf_algorithm(alg: &HashAlgorithm) -> Result<hkdf::Algorithm, TLSError> {
 /// HKDF Extract.
 ///
 /// Returns the result as [`Bytes`] or a [`TLSError`].
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn hkdf_extract(
     alg: &HashAlgorithm,
     ikm: &Bytes,
@@ -198,7 +198,7 @@ pub(crate) fn hkdf_extract(
 /// HKDF Expand.
 ///
 /// Returns the result as [`Bytes`] or a [`TLSError`].
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn hkdf_expand(
     alg: &HashAlgorithm,
     prk: &Bytes,
@@ -316,7 +316,7 @@ impl SignatureScheme {
 }
 
 /// Sign the `input` with the provided RSA key.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn sign_rsa(
     sk: &Bytes,
     pk_modulus: &Bytes,
@@ -350,7 +350,7 @@ pub(crate) fn sign_rsa(
 }
 
 /// Sign the bytes in `input` with the signature key `sk` and `algorithm`.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn sign(
     algorithm: &SignatureScheme,
     sk: &Bytes,
@@ -388,7 +388,7 @@ pub(crate) fn sign(
 /// Verify the `input` bytes against the provided `signature`.
 ///
 /// Return `Ok(())` if the verification succeeds, and a [`TLSError`] otherwise.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn verify(
     alg: &SignatureScheme,
     pk: &PublicVerificationKey,
@@ -497,7 +497,7 @@ impl KemScheme {
 }
 
 /// Generate a new KEM key pair.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn kem_keygen(
     alg: KemScheme,
     rng: &mut (impl CryptoRng + RngCore),
@@ -541,7 +541,7 @@ fn into_raw(alg: KemScheme, point: Bytes) -> Bytes {
 }
 
 /// KEM encapsulation
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn kem_encap(
     alg: KemScheme,
     pk: &Bytes,
@@ -576,7 +576,7 @@ fn to_shared_secret(alg: KemScheme, shared_secret: Bytes) -> Bytes {
 }
 
 /// KEM decapsulation
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn kem_decap(alg: KemScheme, ct: &Bytes, sk: &Bytes) -> Result<Bytes, TLSError> {
     // event!(Level::DEBUG, "KEM Decaps with {alg:?}");
     // event!(Level::TRACE, "  with ciphertext: {}", ct.as_hex());

src/tls13formats.rs

@@ -24,6 +24,8 @@ pub(crate) mod handshake_data;
 use handshake_data::{HandshakeData, HandshakeType};
 #[cfg(bench)]
 pub use handshake_data::{HandshakeData, HandshakeType};
+
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
 // Well Known Constants
@@ -493,7 +495,7 @@ pub fn bench_client_hello(
 }
 
 /// Build a ClientHello message.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn client_hello(
     algorithms: &Algorithms,
     client_random: Random,
@@ -545,7 +547,7 @@ pub(crate) fn client_hello(
     Ok((client_hello, trunc_len))
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn set_client_hello_binder(
     ciphersuite: &Algorithms,
     binder: &Option<Hmac>,
@@ -593,7 +595,7 @@ pub fn bench_parse_client_hello(
 
 /// Parse the provided `client_hello` with the given `ciphersuite`.
 #[allow(clippy::type_complexity)]
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(super) fn parse_client_hello(
     ciphersuite: &Algorithms,
     client_hello: &HandshakeData,
@@ -691,7 +693,7 @@ pub(super) fn parse_client_hello(
 }
 
 /// Build the server hello message.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn server_hello(
     algs: &Algorithms,
     sr: Random,
@@ -733,7 +735,7 @@ pub fn bench_parse_server_hello(
     parse_server_hello(algs, server_hello)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_server_hello(
     algs: &Algorithms,
     server_hello: &HandshakeData,
@@ -773,15 +775,15 @@ pub(crate) fn parse_server_hello(
     }
 }
 
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn encrypted_extensions(_algs: &Algorithms) -> Result<HandshakeData, TLSError> {
     let handshake_type = bytes1(HandshakeType::EncryptedExtensions as u8);
     Ok(HandshakeData(handshake_type.concat(encode_length_u24(
         &encode_length_u16(Bytes::new())?,
     )?)))
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_encrypted_extensions(
     _algs: &Algorithms,
     encrypted_extensions: &HandshakeData,
@@ -796,7 +798,7 @@ pub(crate) fn parse_encrypted_extensions(
         encrypted_extension_bytes.raw_slice(1..encrypted_extension_bytes.len()),
     )
 }
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn server_certificate(
     _algs: &Algorithms,
     cert: &Bytes,
@@ -813,7 +815,7 @@ pub fn bench_parse_server_certificate(certificate: &HandshakeData) -> Result<Byt
     parse_server_certificate(certificate)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_server_certificate(certificate: &HandshakeData) -> Result<Bytes, TLSError> {
     let HandshakeData(sc) = certificate.as_handshake_message(HandshakeType::Certificate)?;
     let mut next = 0;
@@ -882,7 +884,7 @@ fn parse_ecdsa_signature(sig: Bytes) -> Result<Bytes, TLSError> {
         }
     }
 }
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn certificate_verify(algs: &Algorithms, cv: &Bytes) -> Result<HandshakeData, TLSError> {
     let sv = match algs.signature {
         SignatureScheme::RsaPssRsaSha256 => cv.clone(),
@@ -902,7 +904,7 @@ pub(crate) fn certificate_verify(algs: &Algorithms, cv: &Bytes) -> Result<Handsh
     HandshakeData::from_bytes(HandshakeType::CertificateVerify, &sig)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_certificate_verify(
     algs: &Algorithms,
     certificate_verify: &HandshakeData,
@@ -925,12 +927,12 @@ pub(crate) fn parse_certificate_verify(
     }
 }
 
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn finished(vd: &Bytes) -> Result<HandshakeData, TLSError> {
     HandshakeData::from_bytes(HandshakeType::Finished, vd)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_finished(finished: &HandshakeData) -> Result<Bytes, TLSError> {
     let HandshakeData(fin) = finished.as_handshake_message(HandshakeType::Finished)?;
     Ok(fin)
@@ -1058,7 +1060,7 @@ impl Transcript {
     }
 
     /// Add the [`HandshakeData`] `msg` to this transcript.
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn add(mut self, msg: &HandshakeData) -> Self {
         self.transcript = self.transcript.concat(msg);
         self
@@ -1071,7 +1073,7 @@ impl Transcript {
     }
 
     /// Get the hash of this transcript without the client hello
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn transcript_hash_without_client_hello(
         &self,
         client_hello: &HandshakeData,

src/tls13formats/handshake_data.rs

@@ -1,3 +1,4 @@
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
 use crate::tls13utils::{
@@ -80,7 +81,7 @@ impl HandshakeData {
 
     /// Returns a new [`HandshakeData`] that contains the bytes of
     /// `other` appended to the bytes of `self`.
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn concat(self, other: &HandshakeData) -> HandshakeData {
         let mut message1 = self.to_bytes();
         let message2 = other.to_bytes();
@@ -134,7 +135,7 @@ impl HandshakeData {
     /// If successful, returns the parsed handshake messages. Returns a [TLSError]
     /// if parsing of either message fails or if the payload is not fully consumed
     /// by parsing two messages.
-    #[pv_handwritten]
+    #[cfg_attr(feature = "hax-pv", pv_handwritten)]
     pub(crate) fn to_two(&self) -> Result<(HandshakeData, HandshakeData), TLSError> {
         let (message1, payload_rest) = self.next_handshake_message()?;
         let (message2, payload_rest) = payload_rest.next_handshake_message()?;
@@ -150,7 +151,7 @@ impl HandshakeData {
     /// If successful, returns the parsed handshake messages. Returns a [TLSError]
     /// if parsing of any message fails or if the payload is not fully consumed
     /// by parsing four messages.
-    #[pv_handwritten]
+    #[cfg_attr(feature = "hax-pv", pv_handwritten)]
     pub(crate) fn to_four(
         &self,
     ) -> Result<(HandshakeData, HandshakeData, HandshakeData, HandshakeData), TLSError> {