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/
+        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/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))
     }
 }
 

tls_codec/src/lib.rs

@@ -107,16 +107,20 @@ 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(&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 +150,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 +170,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 +191,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 +200,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 +235,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 +291,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!(LEN == 8); // https://github.com/cryspen/hax/issues/1702
         usize_bytes[LEN - 3..].copy_from_slice(&value.0);
         usize::from_be_bytes(usize_bytes)
     }
@@ -288,13 +300,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!(LEN == 8); // https://github.com/cryspen/hax/issues/1702
             Ok(U24(value.to_be_bytes()[LEN - 3..].try_into()?))
         }
     }

tls_codec/src/primitives.rs

@@ -13,6 +13,7 @@ use std::io::{Read, Write};
 impl<T: Size> Size for Option<T> {
     #[inline]
     fn tls_serialized_len(&self) -> usize {
+        hax_lib::fstar!("admit ()"); // overflow
         1 + match self {
             Some(v) => v.tls_serialized_len(),
             None => 0,
@@ -33,8 +34,12 @@ impl<T: Serialize> Serialize for Option<T> {
         match self {
             Some(e) => {
                 let written = writer.write(&[1])?;
+                hax_lib::assume!(written == 1);
                 debug_assert_eq!(written, 1);
-                e.tls_serialize(writer).map(|l| l + 1)
+                e.tls_serialize(writer).map(|l| {
+                    hax_lib::fstar!("admit ()"); // overflow
+                    l + 1
+                })
             }
             None => {
                 writer.write_all(&[0])?;
@@ -49,6 +54,7 @@ impl<T: SerializeBytes> SerializeBytes for Option<T> {
     fn tls_serialize(&self) -> Result<Vec<u8>, Error> {
         match self {
             Some(e) => {
+                hax_lib::fstar!("admit ()"); // overflow
                 let mut out = Vec::with_capacity(e.tls_serialized_len() + 1);
                 out.push(1);
                 // Not inlining serialized_e is a workaround for
@@ -160,6 +166,7 @@ macro_rules! impl_unsigned {
             #[inline]
             fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error> {
                 let written = writer.write(&self.to_be_bytes())?;
+                #[cfg(not(hax))]
                 debug_assert_eq!(written, $bytes);
                 Ok(written)
             }
@@ -236,7 +243,10 @@ where
     #[inline(always)]
     fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error> {
         let written = self.0.tls_serialize(writer)?;
-        self.1.tls_serialize(writer).map(|l| l + written)
+        self.1.tls_serialize(writer).map(|l| {
+            hax_lib::fstar!("admit ()"); // overflow
+            l + written
+        })
     }
 }
 
@@ -247,6 +257,7 @@ where
 {
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
+        hax_lib::fstar!("admit ()"); // overflow
         self.0.tls_serialized_len() + self.1.tls_serialized_len()
     }
 }
@@ -293,6 +304,7 @@ where
     #[inline(always)]
     fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error> {
         let mut written = self.0.tls_serialize(writer)?;
+        hax_lib::fstar!("admit ()"); // overflow
         written += self.1.tls_serialize(writer)?;
         self.2.tls_serialize(writer).map(|l| l + written)
     }
@@ -306,6 +318,7 @@ where
 {
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
+        hax_lib::fstar!("admit ()"); // overflow
         self.0.tls_serialized_len() + self.1.tls_serialized_len() + self.2.tls_serialized_len()
     }
 }

tls_codec/src/quic_vec.rs

@@ -25,6 +25,7 @@ use serde::{Deserialize as SerdeDeserialize, Serialize as SerdeSerialize};
 use crate::{DeserializeBytes, Error, SerializeBytes, Size};
 
 #[cfg(not(feature = "mls"))]
+#[hax_lib::fstar::verification_status(lax)] // Need lemma for (1 << 62) >= 1
 const MAX_LEN: u64 = (1 << 62) - 1;
 #[cfg(not(feature = "mls"))]
 const MAX_LEN_LEN_LOG: usize = 3;
@@ -50,6 +51,7 @@ fn calculate_length(len_len_byte: u8) -> Result<(usize, usize), Error> {
     let length: usize = (len_len_byte & 0x3F).into();
     let len_len_log = (len_len_byte >> 6).into();
     if !cfg!(fuzzing) {
+        #[cfg(not(hax))]
         debug_assert!(len_len_log <= MAX_LEN_LEN_LOG);
     }
     if len_len_log > MAX_LEN_LEN_LOG {
@@ -87,6 +89,7 @@ fn read_variable_length_bytes(bytes: &[u8]) -> Result<((usize, usize), &[u8]), E
 #[inline(always)]
 fn length_encoding_bytes(length: u64) -> Result<usize, Error> {
     if !cfg!(fuzzing) {
+        #[cfg(not(hax))]
         debug_assert!(length <= MAX_LEN);
     }
     if length > MAX_LEN {
@@ -129,6 +132,7 @@ pub fn write_variable_length(content_length: usize) -> Result<Vec<u8>, Error> {
     }
     let mut len = content_length;
     let l = length_bytes.len();
+    hax_lib::fstar!("admit ()"); // underflows
     for i in 0..l {
         // Not using |= is a workaround for https://github.com/cryspen/hax/issues/1512
         length_bytes[l - i - 1] = length_bytes[l - i - 1] | ((len & 0xFF) as u8);
@@ -165,8 +169,10 @@ impl<T: DeserializeBytes> DeserializeBytes for Vec<T> {
         let mut result = Vec::new();
         let mut read = len_len;
         while (read - len_len) < length {
+            hax_lib::loop_invariant!(read >= len_len);
             let (element, next_remainder) = T::tls_deserialize_bytes(remainder)?;
             remainder = next_remainder;
+            hax_lib::fstar!("admit ()"); // overflow
             read += element.tls_serialized_len();
             result.push(element);
         }
@@ -180,6 +186,8 @@ impl<T: SerializeBytes> SerializeBytes for &[T] {
         // We need to pre-compute the length of the content.
         // This requires more computations but the other option would be to buffer
         // the entire content, which can end up requiring a lot of memory.
+
+        hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
         let content_length = self.iter().fold(0, |acc, e| acc + e.tls_serialized_len());
         let mut length = write_variable_length(content_length)?;
         let len_len = length.len();
@@ -219,6 +227,7 @@ impl<T: SerializeBytes> SerializeBytes for Vec<T> {
 impl<T: Size> Size for &[T] {
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
+        hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
         let content_length = self.iter().fold(0, |acc, e| acc + e.tls_serialized_len());
         let len_len = length_encoding_bytes(content_length as u64).unwrap_or({
             // We can't do anything about the error unless we change the trait.
@@ -334,6 +343,7 @@ fn tls_serialize_bytes_len(bytes: &[u8]) -> usize {
         // We can't do anything about the error. Let's say there's no content.
         0
     });
+    hax_lib::fstar!("admit ()"); // overflow
     content_length + len_len
 }
 
@@ -353,6 +363,7 @@ impl DeserializeBytes for VLBytes {
         }
 
         if !cfg!(fuzzing) {
+            #[cfg(not(hax))]
             debug_assert!(
                 length <= MAX_LEN as usize,
                 "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.",
@@ -363,11 +374,12 @@ impl DeserializeBytes for VLBytes {
                 "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.",
             )));
         }
-        match remainder.get(..length).ok_or(Error::EndOfStream) {
-            Ok(vec) => Ok((Self { vec: vec.to_vec() }, &remainder[length..])),
+        match remainder.split_at_checked(length).ok_or(Error::EndOfStream) {
+            Ok((vec, remainder)) => Ok((Self { vec: vec.to_vec() }, remainder)),
             Err(_e) => {
                 let remaining_len = remainder.len();
                 if !cfg!(fuzzing) {
+                    #[cfg(not(hax))]
                     debug_assert_eq!(
                         remaining_len, length,
                         "Expected to read {length} bytes but {remaining_len} were read.",
@@ -469,6 +481,7 @@ pub mod rw {
 
             let mut result = Vec::new();
             let mut read = len_len;
+            hax_lib::fstar!("admit ()"); // underflow
             while (read - len_len) < length {
                 let element = T::tls_deserialize(bytes)?;
                 read += element.tls_serialized_len();
@@ -502,6 +515,7 @@ pub mod rw {
             // We need to pre-compute the length of the content.
             // This requires more computations but the other option would be to buffer
             // the entire content, which can end up requiring a lot of memory.
+            hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
             let content_length = self.iter().fold(0, |acc, e| acc + e.tls_serialized_len());
             let len_len = write_length(writer, content_length)?;
 
@@ -543,6 +557,7 @@ mod rw_bytes {
         let content_length = bytes.len();
 
         if !cfg!(fuzzing) {
+            #[cfg(not(hax))]
             debug_assert!(
                 content_length as u64 <= MAX_LEN,
                 "Vector can't be encoded. It's too large. {content_length} >= {MAX_LEN}",
@@ -559,6 +574,8 @@ mod rw_bytes {
         // Now serialize the elements
         writer.write_all(bytes)?;
 
+        hax_lib::fstar!("admit ()"); // overflow
+
         Ok(content_length + len_len)
     }
 
@@ -584,6 +601,7 @@ mod rw_bytes {
             }
 
             if !cfg!(fuzzing) {
+                #[cfg(not(hax))]
                 debug_assert!(
                     length <= MAX_LEN as usize,
                     "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.",