First try for checked version of tls_serialized_len.

maximebuyse · maximebuyse · commit ef5bf15590e8 · 2025-10-15T18:04:25.000+02:00
diff --git a/tls_codec/derive/src/lib.rs b/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,21 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {
                         #(#prefixes::tls_serialized_len(&self.#members) + )*
                         0
                     }
+                    #[inline]
+                    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 +839,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)
+                    }
                 }
             }
         }
diff --git a/tls_codec/derive/tests/decode.rs b/tls_codec/derive/tests/decode.rs
@@ -273,6 +273,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)
     }
@@ -297,6 +301,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)
     }
diff --git a/tls_codec/derive/tests/decode_bytes.rs b/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()
     }
diff --git a/tls_codec/derive/tests/encode.rs b/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)
     }
diff --git a/tls_codec/derive/tests/encode_bytes.rs b/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()
     }
diff --git a/tls_codec/src/arrays.rs b/tls_codec/src/arrays.rs
@@ -51,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)
+    }
 }
diff --git a/tls_codec/src/lib.rs b/tls_codec/src/lib.rs
@@ -109,6 +109,8 @@ mod serialize_bytes {
     /// 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;
     }
diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs
@@ -12,12 +12,20 @@ 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(),
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        1usize.checked_add(match self {
+            Some(v) => v.tls_serialized_len_checked()?,
             None => 0,
-        }
+        })
+    }
+    #[inline]
+    fn tls_serialized_len(&self) -> usize {
+        1usize
+            .checked_add(match self {
+                Some(v) => v.tls_serialized_len(),
+                None => 0,
+            })
+            .unwrap_or(0)
     }
 }
 
@@ -26,6 +34,10 @@ impl<T: Size> Size for &Option<T> {
     fn tls_serialized_len(&self) -> usize {
         (*self).tls_serialized_len()
     }
+    #[inline]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        (*self).tls_serialized_len_checked()
+    }
 }
 
 impl<T: Serialize> Serialize for Option<T> {
@@ -187,13 +199,21 @@ macro_rules! impl_unsigned {
             fn tls_serialized_len(&self) -> usize {
                 $bytes
             }
+            #[inline]
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
+                Some($bytes)
+            }
         }
 
         impl Size for &$t {
             #[inline]
             fn tls_serialized_len(&self) -> usize {
                 (*self).tls_serialized_len()
             }
+            #[inline]
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
+                (*self).tls_serialized_len_checked()
+            }
         }
     };
 }
@@ -257,10 +277,18 @@ where
     T: Size,
     U: Size,
 {
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.0
+            .tls_serialized_len_checked()?
+            .checked_add(self.1.tls_serialized_len_checked()?)
+    }
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
-        hax_lib::fstar!("admit ()"); // overflow
-        self.0.tls_serialized_len() + self.1.tls_serialized_len()
+        self.0
+            .tls_serialized_len()
+            .checked_add(self.1.tls_serialized_len())
+            .unwrap_or(0)
     }
 }
 
@@ -322,10 +350,21 @@ where
     U: Size,
     V: Size,
 {
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.0
+            .tls_serialized_len_checked()?
+            .checked_add(self.1.tls_serialized_len_checked()?)?
+            .checked_add(self.2.tls_serialized_len_checked()?)
+    }
     #[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()
+        self.0
+            .tls_serialized_len()
+            .checked_add(self.1.tls_serialized_len())
+            .unwrap_or(0)
+            .checked_add(self.2.tls_serialized_len())
+            .unwrap_or(0)
     }
 }
 
@@ -334,6 +373,10 @@ impl Size for () {
     fn tls_serialized_len(&self) -> usize {
         0
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        Some(0)
+    }
 }
 
 impl Deserialize for () {
@@ -363,6 +406,10 @@ impl<T> Size for PhantomData<T> {
     fn tls_serialized_len(&self) -> usize {
         0
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        Some(0)
+    }
 }
 
 impl<T> Deserialize for PhantomData<T> {
@@ -400,6 +447,10 @@ impl<T: Size> Size for Box<T> {
     fn tls_serialized_len(&self) -> usize {
         self.as_ref().tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.as_ref().tls_serialized_len_checked()
+    }
 }
 
 impl<T: Serialize> Serialize for Box<T> {
diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs
@@ -147,13 +147,21 @@ impl<T: Size> Size for Vec<T> {
     fn tls_serialized_len(&self) -> usize {
         self.as_slice().tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.as_slice().tls_serialized_len_checked()
+    }
 }
 
 impl<T: Size> Size for &Vec<T> {
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
         (*self).tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        (*self).tls_serialized_len_checked()
+    }
 }
 
 impl<T: DeserializeBytes> DeserializeBytes for Vec<T> {
@@ -225,17 +233,23 @@ impl<T: SerializeBytes> SerializeBytes for Vec<T> {
     }
 }
 
+fn serialized_len_checked_slice<T: Size>(s: &[T]) -> Option<usize> {
+    hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
+    let content_length = s.iter().fold(Some(0usize), |acc, e| {
+        acc?.checked_add(e.tls_serialized_len_checked()?)
+    })?;
+    let len_len = length_encoding_bytes(content_length as u64).ok()?;
+    content_length.checked_add(len_len)
+}
+
 impl<T: Size> Size for &[T] {
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        serialized_len_checked_slice(self)
+    }
     #[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.
-            // Let's say there's no content for now.
-            0
-        });
-        content_length + len_len
+        serialized_len_checked_slice(self).unwrap_or(0)
     }
 }
 
@@ -338,19 +352,19 @@ impl From<VLBytes> for Vec<u8> {
 }
 
 #[inline(always)]
-fn tls_serialize_bytes_len(bytes: &[u8]) -> usize {
+fn tls_serialize_bytes_len(bytes: &[u8]) -> Option<usize> {
     let content_length = bytes.len();
-    let len_len = length_encoding_bytes(content_length as u64).unwrap_or({
-        // 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
+    let len_len = length_encoding_bytes(content_length as u64).ok()?;
+    content_length.checked_add(len_len)
 }
 
 impl Size for VLBytes {
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
+        tls_serialize_bytes_len(self.as_slice()).unwrap_or(0)
+    }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
         tls_serialize_bytes_len(self.as_slice())
     }
 }
@@ -399,6 +413,10 @@ impl Size for &VLBytes {
     fn tls_serialized_len(&self) -> usize {
         (*self).tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        (*self).tls_serialized_len_checked()
+    }
 }
 
 pub struct VLByteSlice<'a>(pub &'a [u8]);
@@ -423,15 +441,23 @@ impl VLByteSlice<'_> {
 impl Size for &VLByteSlice<'_> {
     #[inline]
     fn tls_serialized_len(&self) -> usize {
+        tls_serialize_bytes_len(self.0).unwrap_or(0)
+    }
+    #[inline]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
         tls_serialize_bytes_len(self.0)
     }
 }
 
 impl Size for VLByteSlice<'_> {
     #[inline]
-    fn tls_serialized_len(&self) -> usize {
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
         tls_serialize_bytes_len(self.0)
     }
+    #[inline]
+    fn tls_serialized_len(&self) -> usize {
+        tls_serialize_bytes_len(self.0).unwrap_or(0)
+    }
 }
 
 #[cfg(feature = "std")]
@@ -679,6 +705,9 @@ mod secret_bytes {
         fn tls_serialized_len(&self) -> usize {
             self.0.tls_serialized_len()
         }
+        fn tls_serialized_len_checked(&self) -> Option<usize> {
+            self.0.tls_serialized_len_checked()
+        }
     }
 
     impl DeserializeBytes for SecretVLBytes {
diff --git a/tls_codec/src/tls_vec.rs b/tls_codec/src/tls_vec.rs

Original file line number	Diff line number	Diff line change
`@@ -90,6 +90,10 @@`
`90`	`90`	`//! TlsByteSliceU32(v).tls_serialized_len()`
`91`	`91`	`//! }`
`92`	`92`	`//!`
	`93`	`+//! pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {`
	`94`	`+//! TlsByteSliceU32(v).tls_serialized_len_checked()`
	`95`	`+//! }`
	`96`	`+//!`
`93`	`97`	`//! pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {`
`94`	`98`	`//! TlsByteSliceU32(v).tls_serialize(writer)`
`95`	`99`	`//! }`
`@@ -787,13 +791,21 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {`
`787`	`791`	`#(#prefixes::tls_serialized_len(&self.#members) + )*`
`788`	`792`	`0`
`789`	`793`	`}`
	`794`	`+ #[inline]`
	`795`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`796`	`+ Some(0usize#(.checked_add(#prefixes::tls_serialized_len_checked(&self.#members)?)?)*)`
	`797`	`+ }`
`790`	`798`	`}`
`791`	`799`
`792`	`800`	`impl #impl_generics tls_codec::Size for &#ident #ty_generics #where_clause {`
`793`	`801`	`#[inline]`
`794`	`802`	`fn tls_serialized_len(&self) -> usize {`
`795`	`803`	`tls_codec::Size::tls_serialized_len(*self)`
`796`	`804`	`}`
	`805`	`+ #[inline]`
	`806`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`807`	`+ tls_codec::Size::tls_serialized_len_checked(*self)`
	`808`	`+ }`
`797`	`809`	`}`
`798`	`810`	`}`
`799`	`811`	`}`
`@@ -827,13 +839,24 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {`
`827`	`839`	`};`
`828`	`840`	`core::mem::size_of::<#repr>() + field_len`
`829`	`841`	`}`
	`842`	`+ #[inline]`
	`843`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`844`	`+ let field_len = match self {`
	`845`	`+ #(#field_arms)*`
	`846`	`+ };`
	`847`	`+ core::mem::size_of::<#repr>().checked_add(field_len)`
	`848`	`+ }`
`830`	`849`	`}`
`831`	`850`
`832`	`851`	`impl #impl_generics tls_codec::Size for &#ident #ty_generics #where_clause {`
`833`	`852`	`#[inline]`
`834`	`853`	`fn tls_serialized_len(&self) -> usize {`
`835`	`854`	`tls_codec::Size::tls_serialized_len(*self)`
`836`	`855`	`}`
	`856`	`+ #[inline]`
	`857`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`858`	`+ tls_codec::Size::tls_serialized_len_checked(*self)`
	`859`	`+ }`
`837`	`860`	`}`
`838`	`861`	`}`
`839`	`862`	`}`
Original file line number	Diff line number	Diff line change
`@@ -273,6 +273,10 @@ mod custom {`
`273`	`273`	`TlsByteSliceU32(v).tls_serialized_len()`
`274`	`274`	`}`
`275`	`275`
	`276`	`+ pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {`
	`277`	`+ TlsByteSliceU32(v).tls_serialized_len_checked()`
	`278`	`+ }`
	`279`	`+`
`276`	`280`	`pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {`
`277`	`281`	`TlsByteSliceU32(v).tls_serialize(writer)`
`278`	`282`	`}`
`@@ -297,6 +301,10 @@ mod custom_bytes {`
`297`	`301`	`TlsByteSliceU32(v).tls_serialized_len()`
`298`	`302`	`}`
`299`	`303`
	`304`	`+ pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {`
	`305`	`+ TlsByteSliceU32(v).tls_serialized_len_checked()`
	`306`	`+ }`
	`307`	`+`
`300`	`308`	`pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {`
`301`	`309`	`TlsByteSliceU32(v).tls_serialize(writer)`
`302`	`310`	`}`
Original file line number	Diff line number	Diff line change
`@@ -90,6 +90,10 @@ mod custom {`
`90`	`90`	`v.tls_serialized_len()`
`91`	`91`	`}`
`92`	`92`
	`93`	`+ pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {`
	`94`	`+ v.tls_serialized_len_checked()`
	`95`	`+ }`
	`96`	`+`
`93`	`97`	`pub fn tls_serialize(v: &[u8]) -> Result<Vec<u8>, tls_codec::Error> {`
`94`	`98`	`v.tls_serialize()`
`95`	`99`	`}`
Original file line number	Diff line number	Diff line change
`@@ -131,6 +131,10 @@ mod custom {`
`131`	`131`	`TlsByteSliceU32(v).tls_serialized_len()`
`132`	`132`	`}`
`133`	`133`
	`134`	`+ pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {`
	`135`	`+ TlsByteSliceU32(v).tls_serialized_len_checked()`
	`136`	`+ }`
	`137`	`+`
`134`	`138`	`pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {`
`135`	`139`	`TlsByteSliceU32(v).tls_serialize(writer)`
`136`	`140`	`}`
Original file line number	Diff line number	Diff line change
`@@ -107,6 +107,10 @@ mod custom {`
`107`	`107`	`v.tls_serialized_len()`
`108`	`108`	`}`
`109`	`109`
	`110`	`+ pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {`
	`111`	`+ v.tls_serialized_len_checked()`
	`112`	`+ }`
	`113`	`+`
`110`	`114`	`pub fn tls_serialize(v: &[u8]) -> Result<Vec<u8>, tls_codec::Error> {`
`111`	`115`	`v.tls_serialize()`
`112`	`116`	`}`
Original file line number	Diff line number	Diff line change
`@@ -51,4 +51,8 @@ impl<const LEN: usize> Size for [u8; LEN] {`
`51`	`51`	`fn tls_serialized_len(&self) -> usize {`
`52`	`52`	`LEN`
`53`	`53`	`}`
	`54`	`+ #[inline]`
	`55`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`56`	`+ Some(LEN)`
	`57`	`+ }`
`54`	`58`	`}`
Original file line number	Diff line number	Diff line change
`@@ -109,6 +109,8 @@ mod serialize_bytes {`
`109`	`109`	`/// memory.`
`110`	`110`	`#[hax_lib::attributes]`
`111`	`111`	`pub trait Size {`
	`112`	`+ #[hax_lib::requires(true)]`
	`113`	`+ fn tls_serialized_len_checked(&self) -> Option<usize>;`
`112`	`114`	`#[hax_lib::requires(true)]`
`113`	`115`	`fn tls_serialized_len(&self) -> usize;`
`114`	`116`	`}`
Original file line number	Diff line number	Diff line change
`@@ -12,12 +12,20 @@ use std::io::{Read, Write};`
`12`	`12`
`13`	`13`	`impl<T: Size> Size for Option<T> {`
`14`	`14`	`#[inline]`
`15`		`- fn tls_serialized_len(&self) -> usize {`
`16`		`- hax_lib::fstar!("admit ()"); // overflow`
`17`		`- 1 + match self {`
`18`		`- Some(v) => v.tls_serialized_len(),`
	`15`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`16`	`+ 1usize.checked_add(match self {`
	`17`	`+ Some(v) => v.tls_serialized_len_checked()?,`
`19`	`18`	`None => 0,`
`20`		`- }`
	`19`	`+ })`
	`20`	`+ }`
	`21`	`+ #[inline]`
	`22`	`+ fn tls_serialized_len(&self) -> usize {`
	`23`	`+ 1usize`
	`24`	`+ .checked_add(match self {`
	`25`	`+ Some(v) => v.tls_serialized_len(),`
	`26`	`+ None => 0,`
	`27`	`+ })`
	`28`	`+ .unwrap_or(0)`
`21`	`29`	`}`
`22`	`30`	`}`
`23`	`31`
`@@ -26,6 +34,10 @@ impl<T: Size> Size for &Option<T> {`
`26`	`34`	`fn tls_serialized_len(&self) -> usize {`
`27`	`35`	`(*self).tls_serialized_len()`
`28`	`36`	`}`
	`37`	`+ #[inline]`
	`38`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`39`	`+ (*self).tls_serialized_len_checked()`
	`40`	`+ }`
`29`	`41`	`}`
`30`	`42`
`31`	`43`	`impl<T: Serialize> Serialize for Option<T> {`
`@@ -187,13 +199,21 @@ macro_rules! impl_unsigned {`
`187`	`199`	`fn tls_serialized_len(&self) -> usize {`
`188`	`200`	`$bytes`
`189`	`201`	`}`
	`202`	`+ #[inline]`
	`203`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`204`	`+ Some($bytes)`
	`205`	`+ }`
`190`	`206`	`}`
`191`	`207`
`192`	`208`	`impl Size for &$t {`
`193`	`209`	`#[inline]`
`194`	`210`	`fn tls_serialized_len(&self) -> usize {`
`195`	`211`	`(*self).tls_serialized_len()`
`196`	`212`	`}`
	`213`	`+ #[inline]`
	`214`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`215`	`+ (*self).tls_serialized_len_checked()`
	`216`	`+ }`
`197`	`217`	`}`
`198`	`218`	`};`
`199`	`219`	`}`
`@@ -257,10 +277,18 @@ where`
`257`	`277`	`T: Size,`
`258`	`278`	`U: Size,`
`259`	`279`	`{`
	`280`	`+ #[inline(always)]`
	`281`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`282`	`+ self.0`
	`283`	`+ .tls_serialized_len_checked()?`
	`284`	`+ .checked_add(self.1.tls_serialized_len_checked()?)`
	`285`	`+ }`
`260`	`286`	`#[inline(always)]`
`261`	`287`	`fn tls_serialized_len(&self) -> usize {`
`262`		`- hax_lib::fstar!("admit ()"); // overflow`
`263`		`- self.0.tls_serialized_len() + self.1.tls_serialized_len()`
	`288`	`+ self.0`
	`289`	`+ .tls_serialized_len()`
	`290`	`+ .checked_add(self.1.tls_serialized_len())`
	`291`	`+ .unwrap_or(0)`
`264`	`292`	`}`
`265`	`293`	`}`
`266`	`294`
`@@ -322,10 +350,21 @@ where`
`322`	`350`	`U: Size,`
`323`	`351`	`V: Size,`
`324`	`352`	`{`
	`353`	`+ #[inline(always)]`
	`354`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`355`	`+ self.0`
	`356`	`+ .tls_serialized_len_checked()?`
	`357`	`+ .checked_add(self.1.tls_serialized_len_checked()?)?`
	`358`	`+ .checked_add(self.2.tls_serialized_len_checked()?)`
	`359`	`+ }`
`325`	`360`	`#[inline(always)]`
`326`	`361`	`fn tls_serialized_len(&self) -> usize {`
`327`		`- hax_lib::fstar!("admit ()"); // overflow`
`328`		`- self.0.tls_serialized_len() + self.1.tls_serialized_len() + self.2.tls_serialized_len()`
	`362`	`+ self.0`
	`363`	`+ .tls_serialized_len()`
	`364`	`+ .checked_add(self.1.tls_serialized_len())`
	`365`	`+ .unwrap_or(0)`
	`366`	`+ .checked_add(self.2.tls_serialized_len())`
	`367`	`+ .unwrap_or(0)`
`329`	`368`	`}`
`330`	`369`	`}`
`331`	`370`
`@@ -334,6 +373,10 @@ impl Size for () {`
`334`	`373`	`fn tls_serialized_len(&self) -> usize {`
`335`	`374`	`0`
`336`	`375`	`}`
	`376`	`+ #[inline(always)]`
	`377`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`378`	`+ Some(0)`
	`379`	`+ }`
`337`	`380`	`}`
`338`	`381`
`339`	`382`	`impl Deserialize for () {`
`@@ -363,6 +406,10 @@ impl<T> Size for PhantomData<T> {`
`363`	`406`	`fn tls_serialized_len(&self) -> usize {`
`364`	`407`	`0`
`365`	`408`	`}`
	`409`	`+ #[inline(always)]`
	`410`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`411`	`+ Some(0)`
	`412`	`+ }`
`366`	`413`	`}`
`367`	`414`
`368`	`415`	`impl<T> Deserialize for PhantomData<T> {`
`@@ -400,6 +447,10 @@ impl<T: Size> Size for Box<T> {`
`400`	`447`	`fn tls_serialized_len(&self) -> usize {`
`401`	`448`	`self.as_ref().tls_serialized_len()`
`402`	`449`	`}`
	`450`	`+ #[inline(always)]`
	`451`	`+ fn tls_serialized_len_checked(&self) -> Option<usize> {`
	`452`	`+ self.as_ref().tls_serialized_len_checked()`
	`453`	`+ }`
`403`	`454`	`}`
`404`	`455`
`405`	`456`	`impl<T: Serialize> Serialize for Box<T> {`