Panic freedom

.github/workflows/tls_codec.yml

@@ -86,7 +86,8 @@ jobs:
         uses: hacspec/hax-actions@main
         with:
           fstar: v2025.08.07
+          hax_reference: tls-codec-panic-freedom
       - name: 🏃 Extract F*
         run: cargo hax into fstar
-      - name: 🏃 Lax-check extracted F*
-        run: OTHERFLAGS="--admit_smt_queries true" make -C proofs/fstar/extraction/
+      - name: 🏃 Type-check extracted F*
+        run: make -C proofs/fstar/extraction/

tls_codec/Cargo.toml

@@ -16,7 +16,7 @@ zeroize = { version = "1.8", default-features = false, features = [
     "alloc",
     "zeroize_derive",
 ] }
-hax-lib = {git = "https://github.com/cryspen/hax", branch = "tls-codec-lib"}
+hax-lib = {git = "https://github.com/cryspen/hax", branch = "tls-codec-panic-freedom"}
 
 # optional dependencies
 arbitrary = { version = "1.4", features = ["derive"], optional = true }

tls_codec/derive/src/lib.rs

@@ -90,6 +90,10 @@
 //!         TlsByteSliceU32(v).tls_serialized_len()
 //!     }
 //!
+//!     pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+//!         TlsByteSliceU32(v).tls_serialized_len_checked()
+//!     }
+//!
 //!     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
 //!         TlsByteSliceU32(v).tls_serialize(writer)
 //!     }
@@ -787,13 +791,22 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {
                         #(#prefixes::tls_serialized_len(&self.#members) + )*
                         0
                     }
+                    #[inline]
+                    #[allow(clippy::needless_question_mark)]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        Some(0usize#(.checked_add(#prefixes::tls_serialized_len_checked(&self.#members)?)?)*)
+                    }
                 }
 
                 impl #impl_generics tls_codec::Size for &#ident #ty_generics #where_clause {
                     #[inline]
                     fn tls_serialized_len(&self) -> usize {
                         tls_codec::Size::tls_serialized_len(*self)
                     }
+                    #[inline]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        tls_codec::Size::tls_serialized_len_checked(*self)
+                    }
                 }
             }
         }
@@ -827,13 +840,24 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {
                         };
                         core::mem::size_of::<#repr>() + field_len
                     }
+                    #[inline]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        let field_len = match self {
+                            #(#field_arms)*
+                        };
+                        core::mem::size_of::<#repr>().checked_add(field_len)
+                    }
                 }
 
                 impl #impl_generics tls_codec::Size for &#ident #ty_generics #where_clause {
                     #[inline]
                     fn tls_serialized_len(&self) -> usize {
                         tls_codec::Size::tls_serialized_len(*self)
                     }
+                    #[inline]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        tls_codec::Size::tls_serialized_len_checked(*self)
+                    }
                 }
             }
         }

tls_codec/derive/tests/decode.rs

@@ -269,6 +269,10 @@ mod custom {
         TlsByteSliceU32(v).tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        TlsByteSliceU32(v).tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
         TlsByteSliceU32(v).tls_serialize(writer)
     }
@@ -293,6 +297,10 @@ mod custom_bytes {
         TlsByteSliceU32(v).tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        TlsByteSliceU32(v).tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
         TlsByteSliceU32(v).tls_serialize(writer)
     }

tls_codec/derive/tests/decode_bytes.rs

@@ -90,6 +90,10 @@ mod custom {
         v.tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        v.tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize(v: &[u8]) -> Result<Vec<u8>, tls_codec::Error> {
         v.tls_serialize()
     }

tls_codec/derive/tests/encode.rs

@@ -131,6 +131,10 @@ mod custom {
         TlsByteSliceU32(v).tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        TlsByteSliceU32(v).tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
         TlsByteSliceU32(v).tls_serialize(writer)
     }

tls_codec/derive/tests/encode_bytes.rs

@@ -107,6 +107,10 @@ mod custom {
         v.tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        v.tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize(v: &[u8]) -> Result<Vec<u8>, tls_codec::Error> {
         v.tls_serialize()
     }

tls_codec/src/arrays.rs

@@ -35,12 +35,8 @@ impl<const LEN: usize> Deserialize for [u8; LEN] {
 impl<const LEN: usize> DeserializeBytes for [u8; LEN] {
     #[inline]
     fn tls_deserialize_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error> {
-        let out = bytes
-            .get(..LEN)
-            .ok_or(Error::EndOfStream)?
-            .try_into()
-            .map_err(|_| Error::EndOfStream)?;
-        Ok((out, &bytes[LEN..]))
+        let (out, remainder) = bytes.split_at_checked(LEN).ok_or(Error::EndOfStream)?;
+        Ok((out.try_into().map_err(|_| Error::EndOfStream)?, remainder))
     }
 }
 
@@ -55,4 +51,8 @@ impl<const LEN: usize> Size for [u8; LEN] {
     fn tls_serialized_len(&self) -> usize {
         LEN
     }
+    #[inline]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        Some(LEN)
+    }
 }

tls_codec/src/lib.rs

@@ -107,16 +107,22 @@ mod serialize_bytes {
     /// efficiently serialized.
     /// This allows to collect the length of a serialized structure before allocating
     /// memory.
+    #[hax_lib::attributes]
     pub trait Size {
+        #[hax_lib::requires(true)]
+        fn tls_serialized_len_checked(&self) -> Option<usize>;
+        #[hax_lib::requires(true)]
         fn tls_serialized_len(&self) -> usize;
     }
 
     /// The `SerializeBytes` trait provides a function to serialize a struct or enum.
     ///
     /// The trait provides one function:
     /// * `tls_serialize` that returns a byte vector
+    #[hax_lib::attributes]
     pub trait SerializeBytes: Size {
         /// Serialize `self` and return it as a byte vector.
+        #[hax_lib::requires(true)]
         fn tls_serialize(&self) -> Result<Vec<u8>, Error>;
     }
 }
@@ -146,10 +152,12 @@ impl From<std::io::Error> for Error {
 /// The trait provides two functions:
 /// * `tls_serialize` that takes a buffer to write the serialization to
 /// * `tls_serialize_detached` that returns a byte vector
+#[hax_lib::attributes]
 pub trait Serialize: Size {
     /// Serialize `self` and write it to the `writer`.
     /// The function returns the number of bytes written to `writer`.
     #[cfg(feature = "std")]
+    #[hax_lib::requires(true)]
     fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error>;
 
     /// Serialize `self` and return it as a byte vector.
@@ -164,6 +172,7 @@ pub trait Serialize: Size {
 fn tls_serialize_detached_default<T: ?Sized + Serialize>(s: &T) -> Result<Vec<u8>, Error> {
     let mut buffer = Vec::with_capacity(s.tls_serialized_len());
     let written = s.tls_serialize(&mut buffer)?;
+    #[cfg(not(hax))]
     debug_assert_eq!(
         written,
         buffer.len(),
@@ -184,6 +193,7 @@ fn tls_serialize_detached_default<T: ?Sized + Serialize>(s: &T) -> Result<Vec<u8
 
 /// The `Deserialize` trait defines functions to deserialize a byte slice to a
 /// struct or enum.
+#[hax_lib::attributes]
 pub trait Deserialize: Size {
     /// This function deserializes the `bytes` from the provided a [`std::io::Read`]
     /// and returns the populated struct.
@@ -192,6 +202,7 @@ pub trait Deserialize: Size {
     ///
     /// Returns an error if one occurs during deserialization.
     #[cfg(feature = "std")]
+    #[hax_lib::requires(true)]
     fn tls_deserialize<R: Read>(bytes: &mut R) -> Result<Self, Error>
     where
         Self: Sized;
@@ -226,13 +237,15 @@ fn tls_deserialize_exact_default<T: Deserialize>(bytes: impl AsRef<[u8]>) -> Res
 /// The `DeserializeBytes` trait defines functions to deserialize a byte slice
 /// to a struct or enum. In contrast to [`Deserialize`], this trait operates
 /// directly on byte slices and can return any remaining bytes.
+#[hax_lib::attributes]
 pub trait DeserializeBytes: Size {
     /// This function deserializes the `bytes` from the provided a `&[u8]`
     /// and returns the populated struct, as well as the remaining slice.
     ///
     /// In order to get the amount of bytes read, use [`Size::tls_serialized_len`].
     ///
     /// Returns an error if one occurs during deserialization.
+    #[hax_lib::requires(true)]
     fn tls_deserialize_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error>
     where
         Self: Sized;
@@ -280,6 +293,7 @@ impl From<U24> for usize {
     fn from(value: U24) -> usize {
         const LEN: usize = core::mem::size_of::<usize>();
         let mut usize_bytes = [0u8; LEN];
+        hax_lib::assume!(usize_bytes.len() == LEN); // https://github.com/cryspen/hax/issues/1702
         usize_bytes[LEN - 3..].copy_from_slice(&value.0);
         usize::from_be_bytes(usize_bytes)
     }
@@ -288,13 +302,14 @@ impl From<U24> for usize {
 impl TryFrom<usize> for U24 {
     type Error = Error;
 
-    fn try_from(value: usize) -> Result<Self, Self::Error> {
+    fn try_from(value: usize) -> Result<Self, Error> {
         const LEN: usize = core::mem::size_of::<usize>();
         // In practice, our usages of this conversion should never be invalid, as the values
         // have to come from `TryFrom<U24> for usize`.
         if value > (1 << 24) - 1 {
             Err(Error::LibraryError)
         } else {
+            hax_lib::assume!(value.to_be_bytes().len() == LEN); // https://github.com/cryspen/hax/issues/1702
             Ok(U24(value.to_be_bytes()[LEN - 3..].try_into()?))
         }
     }