From 8c935c8be7362386d15136e8869661ea86246c4f Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 23 Sep 2025 14:07:26 +0200 Subject: [PATCH 01/13] First type-checking state. --- Cargo.lock | 9 +++------ tls_codec/Cargo.toml | 2 +- tls_codec/src/arrays.rs | 8 ++------ tls_codec/src/lib.rs | 16 +++++++++++++++- tls_codec/src/primitives.rs | 26 +++++++++++++++++++++++--- tls_codec/src/quic_vec.rs | 16 ++++++++++++++++ tls_codec/src/tls_vec.rs | 20 +++++++++++++++++++- 7 files changed, 79 insertions(+), 18 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e4151a471..51ea5134a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -739,8 +739,7 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" [[package]] name = "hax-lib" -version = "0.3.1" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-lib#89146496aa29fff2137635020f58a03a1ffb7caa" +version = "0.3.4" dependencies = [ "hax-lib-macros", "num-bigint", @@ -749,8 +748,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.3.1" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-lib#89146496aa29fff2137635020f58a03a1ffb7caa" +version = "0.3.4" dependencies = [ "hax-lib-macros-types", "proc-macro-error2", @@ -761,8 +759,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.3.1" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-lib#89146496aa29fff2137635020f58a03a1ffb7caa" +version = "0.3.4" dependencies = [ "proc-macro2", "quote", diff --git a/tls_codec/Cargo.toml b/tls_codec/Cargo.toml index 672892caf..2319540c8 100644 --- a/tls_codec/Cargo.toml +++ b/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 = {path = "../../hax/hax-lib"} # optional dependencies arbitrary = { version = "1.4", features = ["derive"], optional = true } diff --git a/tls_codec/src/arrays.rs b/tls_codec/src/arrays.rs index 3e6200896..52fa3339f 100644 --- a/tls_codec/src/arrays.rs +++ b/tls_codec/src/arrays.rs @@ -35,12 +35,8 @@ impl Deserialize for [u8; LEN] { impl 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)) } } diff --git a/tls_codec/src/lib.rs b/tls_codec/src/lib.rs index a6e61e0bc..4b25fd213 100644 --- a/tls_codec/src/lib.rs +++ b/tls_codec/src/lib.rs @@ -107,7 +107,9 @@ 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; } @@ -115,8 +117,10 @@ mod serialize_bytes { /// /// 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, Error>; } } @@ -146,10 +150,12 @@ impl From 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(&self, writer: &mut W) -> Result; /// Serialize `self` and return it as a byte vector. @@ -164,6 +170,7 @@ pub trait Serialize: Size { fn tls_serialize_detached_default(s: &T) -> Result, 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(s: &T) -> Result(bytes: &mut R) -> Result where Self: Sized; @@ -226,6 +235,7 @@ fn tls_deserialize_exact_default(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. @@ -233,6 +243,7 @@ pub trait DeserializeBytes: Size { /// 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; @@ -276,10 +287,12 @@ impl U24 { } } +#[hax_lib::fstar::options("--z3rlimit 00")] impl From for usize { fn from(value: U24) -> usize { const LEN: usize = core::mem::size_of::(); 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 +301,14 @@ impl From for usize { impl TryFrom for U24 { type Error = Error; - fn try_from(value: usize) -> Result { + fn try_from(value: usize) -> Result { const LEN: usize = core::mem::size_of::(); // In practice, our usages of this conversion should never be invalid, as the values // have to come from `TryFrom 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()?)) } } diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs index 5fac21b1d..90eae9b19 100644 --- a/tls_codec/src/primitives.rs +++ b/tls_codec/src/primitives.rs @@ -13,6 +13,7 @@ use std::io::{Read, Write}; impl Size for Option { #[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 Serialize for Option { match self { Some(e) => { let written = writer.write(&[1])?; + #[cfg(not(hax))] debug_assert_eq!(written, 1); - e.tls_serialize(writer).map(|l| l + 1) + e.tls_serialize(writer).map(|l| { + hax_lib::assume!(l <= 1000); + l + 1 + }) } None => { writer.write_all(&[0])?; @@ -49,6 +54,7 @@ impl SerializeBytes for Option { fn tls_serialize(&self) -> Result, Error> { match self { Some(e) => { + hax_lib::assume!(e.tls_serialized_len() <= 1000); 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(&self, writer: &mut W) -> Result { 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(&self, writer: &mut W) -> Result { 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::assume!(l < 1000 && written < 1000); + l + written + }) } } @@ -247,6 +257,7 @@ where { #[inline(always)] fn tls_serialized_len(&self) -> usize { + hax_lib::assume!(self.0.tls_serialized_len() < 1000 && self.1.tls_serialized_len() < 1000); self.0.tls_serialized_len() + self.1.tls_serialized_len() } } @@ -293,8 +304,12 @@ where #[inline(always)] fn tls_serialize(&self, writer: &mut W) -> Result { 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) + self.2.tls_serialize(writer).map(|l| { + hax_lib::assume!(l < 1000 && written < 1000); + l + written + }) } } @@ -306,6 +321,11 @@ where { #[inline(always)] fn tls_serialized_len(&self) -> usize { + hax_lib::assume!( + self.0.tls_serialized_len() < 1000 + && self.1.tls_serialized_len() < 1000 + && self.2.tls_serialized_len() < 1000 + ); self.0.tls_serialized_len() + self.1.tls_serialized_len() + self.2.tls_serialized_len() } } diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs index 194c8ec14..6f071d55b 100644 --- a/tls_codec/src/quic_vec.rs +++ b/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 { 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, 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 DeserializeBytes for Vec { 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::assume!(read < 1000 && element.tls_serialized_len() < 1000); // overflow read += element.tls_serialized_len(); result.push(element); } @@ -180,6 +186,8 @@ impl 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 SerializeBytes for Vec { impl 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 } @@ -347,6 +357,7 @@ impl Size for VLBytes { impl DeserializeBytes for VLBytes { #[inline(always)] fn tls_deserialize_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error> { + hax_lib::fstar!("admit ()"); let ((length, _), remainder) = read_variable_length_bytes(bytes)?; if length == 0 { return Ok((Self::new(vec![]), remainder)); @@ -469,6 +480,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 +514,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)?; @@ -542,6 +555,8 @@ mod rw_bytes { // large and write it out. let content_length = bytes.len(); + hax_lib::fstar!("admit ()"); + if !cfg!(fuzzing) { debug_assert!( content_length as u64 <= MAX_LEN, @@ -578,6 +593,7 @@ mod rw_bytes { impl Deserialize for VLBytes { fn tls_deserialize(bytes: &mut R) -> Result { + hax_lib::fstar!("admit ()"); let (length, _) = rw::read_length(bytes)?; if length == 0 { return Ok(Self::new(vec![])); diff --git a/tls_codec/src/tls_vec.rs b/tls_codec/src/tls_vec.rs index 3b0f9c55d..815208a76 100644 --- a/tls_codec/src/tls_vec.rs +++ b/tls_codec/src/tls_vec.rs @@ -20,6 +20,7 @@ macro_rules! impl_size { /// The serialized len #[inline(always)] fn tls_serialized_length(&$self) -> usize { + hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700 $self.as_slice() .iter() .fold($len_len, |acc, e| acc + e.tls_serialized_len()) @@ -32,6 +33,7 @@ macro_rules! impl_byte_size { /// The serialized len #[inline(always)] fn tls_serialized_byte_length(&$self) -> usize { + hax_lib::fstar!("admit ()"); // overflow $self.as_slice().len() + $len_len } } @@ -74,6 +76,7 @@ macro_rules! impl_byte_deserialize { u16::MAX ))); } + hax_lib::fstar!("admit ()"); // overflow let vec = bytes .get($len_len..len + $len_len) .ok_or(Error::EndOfStream)?; @@ -93,7 +96,9 @@ macro_rules! impl_deserialize { let mut read = len.tls_serialized_len(); let len_len = read; while (read - len_len) < len.try_into().unwrap() { + hax_lib::loop_invariant!(read >= len_len); let element = T::tls_deserialize(bytes)?; + hax_lib::assume!(read < 1000 && element.tls_serialized_len() < 1000); // overflow read += element.tls_serialized_len(); result.push(element); } @@ -111,8 +116,10 @@ macro_rules! impl_deserialize_bytes { let mut read = len.tls_serialized_len(); let len_len = read; while (read - len_len) < len.try_into().unwrap() { + hax_lib::loop_invariant!(read >= len_len); let (element, next_remainder) = T::tls_deserialize_bytes(remainder)?; remainder = next_remainder; + hax_lib::assume!(read < 1000 && element.tls_serialized_len() < 1000); // overflow read += element.tls_serialized_len(); result.push(element); } @@ -130,8 +137,11 @@ macro_rules! impl_serialize { // large and write it out. let (tls_serialized_len, byte_length) = $self.get_content_lengths()?; + hax_lib::fstar!("admit ()"); // Need to prove unwrap for usize to U24 let mut written = <$size as Serialize>::tls_serialize(&<$size>::try_from(byte_length).unwrap(), writer)?; + + hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700 // Now serialize the elements for e in $self.as_slice().iter() { written += e.tls_serialize(writer)?; @@ -152,8 +162,10 @@ macro_rules! impl_byte_serialize { // large and write it out. let (tls_serialized_len, byte_length) = $self.get_content_lengths()?; + hax_lib::fstar!("admit ()"); // Need to prove unwrap for usize to U24 let mut written = <$size as Serialize>::tls_serialize(&<$size>::try_from(byte_length).unwrap(), writer)?; + hax_lib::fstar!("admit ()"); // overflow // Now serialize the elements written += writer.write($self.as_slice())?; @@ -168,9 +180,10 @@ macro_rules! impl_serialize_common { $(#[$std_enabled])? fn get_content_lengths(&$self) -> Result<(usize, usize), Error> { let tls_serialized_len = $self.tls_serialized_len(); + hax_lib::assume!(tls_serialized_len > $len_len); let byte_length = tls_serialized_len - $len_len; - let max_len = <$size>::MAX.try_into().unwrap(); + #[cfg(not(hax))] debug_assert!( byte_length <= max_len, "Vector length can't be encoded in the vector length a {} >= {}", @@ -185,6 +198,7 @@ macro_rules! impl_serialize_common { $(#[$std_enabled])? fn assert_written_bytes(&$self, tls_serialized_len: usize, written: usize) -> Result<(), Error> { + #[cfg(not(hax))] debug_assert_eq!( written, tls_serialized_len, "{} bytes should have been serialized but {} were written", @@ -207,6 +221,7 @@ macro_rules! impl_serialize_bytes_bytes { let (tls_serialized_len, byte_length) = $self.get_content_lengths()?; let mut vec = Vec::::with_capacity(tls_serialized_len); + hax_lib::fstar!("admit ()"); // Need to prove unwrap for usize to U24 let length_vec = <$size as SerializeBytes>::tls_serialize(&byte_length.try_into().unwrap())?; let mut written = length_vec.len(); vec.extend_from_slice(&length_vec); @@ -434,6 +449,7 @@ macro_rules! impl_tls_vec_generic { } } + #[hax_lib::opaque] // index precondition impl core::ops::Index for $name { type Output = T; @@ -443,6 +459,7 @@ macro_rules! impl_tls_vec_generic { } } + #[hax_lib::opaque] // translation uses =., why? impl core::cmp::PartialEq for $name { fn eq(&self, other: &Self) -> bool { self.vec.eq(&other.vec) @@ -638,6 +655,7 @@ macro_rules! impl_tls_vec { #[inline] fn index(&self, i: usize) -> &u8 { + hax_lib::fstar!("admit ()"); // index precondition self.vec.index(i) } } From 56fe9a71914f48db4fd7f1c8a98baeb5a3bdf6d6 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 25 Sep 2025 10:29:42 +0200 Subject: [PATCH 02/13] Document all admits in hax proofs. --- Cargo.lock | 3 +++ tls_codec/Cargo.toml | 2 +- tls_codec/src/lib.rs | 3 +-- tls_codec/src/primitives.rs | 19 ++++++------------- tls_codec/src/quic_vec.rs | 16 +++++++++------- tls_codec/src/tls_vec.rs | 10 +++++----- 6 files changed, 25 insertions(+), 28 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 51ea5134a..d98c5998b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -740,6 +740,7 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" [[package]] name = "hax-lib" version = "0.3.4" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#dece8bb8e811c747639f7c7595978fb00b726fa9" dependencies = [ "hax-lib-macros", "num-bigint", @@ -749,6 +750,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" version = "0.3.4" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#dece8bb8e811c747639f7c7595978fb00b726fa9" dependencies = [ "hax-lib-macros-types", "proc-macro-error2", @@ -760,6 +762,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" version = "0.3.4" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#dece8bb8e811c747639f7c7595978fb00b726fa9" dependencies = [ "proc-macro2", "quote", diff --git a/tls_codec/Cargo.toml b/tls_codec/Cargo.toml index 2319540c8..50dd14128 100644 --- a/tls_codec/Cargo.toml +++ b/tls_codec/Cargo.toml @@ -16,7 +16,7 @@ zeroize = { version = "1.8", default-features = false, features = [ "alloc", "zeroize_derive", ] } -hax-lib = {path = "../../hax/hax-lib"} +hax-lib = {git = "https://github.com/cryspen/hax", branch = "tls-codec-panic-freedom"} # optional dependencies arbitrary = { version = "1.4", features = ["derive"], optional = true } diff --git a/tls_codec/src/lib.rs b/tls_codec/src/lib.rs index 4b25fd213..f46e3b725 100644 --- a/tls_codec/src/lib.rs +++ b/tls_codec/src/lib.rs @@ -287,7 +287,6 @@ impl U24 { } } -#[hax_lib::fstar::options("--z3rlimit 00")] impl From for usize { fn from(value: U24) -> usize { const LEN: usize = core::mem::size_of::(); @@ -308,7 +307,7 @@ impl TryFrom for U24 { if value > (1 << 24) - 1 { Err(Error::LibraryError) } else { - hax_lib::assume!(LEN == 8); // https://github.com/cryspen/hax/issues/1702 + hax_lib::assume!(LEN == 8); // https://github.com/cryspen/hax/issues/1702 Ok(U24(value.to_be_bytes()[LEN - 3..].try_into()?)) } } diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs index 90eae9b19..64c47ec08 100644 --- a/tls_codec/src/primitives.rs +++ b/tls_codec/src/primitives.rs @@ -37,7 +37,7 @@ impl Serialize for Option { #[cfg(not(hax))] debug_assert_eq!(written, 1); e.tls_serialize(writer).map(|l| { - hax_lib::assume!(l <= 1000); + hax_lib::fstar!("admit ()"); // overflow l + 1 }) } @@ -54,7 +54,7 @@ impl SerializeBytes for Option { fn tls_serialize(&self) -> Result, Error> { match self { Some(e) => { - hax_lib::assume!(e.tls_serialized_len() <= 1000); + 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 @@ -244,7 +244,7 @@ where fn tls_serialize(&self, writer: &mut W) -> Result { let written = self.0.tls_serialize(writer)?; self.1.tls_serialize(writer).map(|l| { - hax_lib::assume!(l < 1000 && written < 1000); + hax_lib::fstar!("admit ()"); // overflow l + written }) } @@ -257,7 +257,7 @@ where { #[inline(always)] fn tls_serialized_len(&self) -> usize { - hax_lib::assume!(self.0.tls_serialized_len() < 1000 && self.1.tls_serialized_len() < 1000); + hax_lib::fstar!("admit ()"); // overflow self.0.tls_serialized_len() + self.1.tls_serialized_len() } } @@ -306,10 +306,7 @@ where 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| { - hax_lib::assume!(l < 1000 && written < 1000); - l + written - }) + self.2.tls_serialize(writer).map(|l| l + written) } } @@ -321,11 +318,7 @@ where { #[inline(always)] fn tls_serialized_len(&self) -> usize { - hax_lib::assume!( - self.0.tls_serialized_len() < 1000 - && self.1.tls_serialized_len() < 1000 - && self.2.tls_serialized_len() < 1000 - ); + hax_lib::fstar!("admit ()"); // overflow self.0.tls_serialized_len() + self.1.tls_serialized_len() + self.2.tls_serialized_len() } } diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs index 6f071d55b..333d396b1 100644 --- a/tls_codec/src/quic_vec.rs +++ b/tls_codec/src/quic_vec.rs @@ -172,7 +172,7 @@ impl DeserializeBytes for Vec { hax_lib::loop_invariant!(read >= len_len); let (element, next_remainder) = T::tls_deserialize_bytes(remainder)?; remainder = next_remainder; - hax_lib::assume!(read < 1000 && element.tls_serialized_len() < 1000); // overflow + hax_lib::fstar!("admit ()"); // overflow read += element.tls_serialized_len(); result.push(element); } @@ -357,13 +357,13 @@ impl Size for VLBytes { impl DeserializeBytes for VLBytes { #[inline(always)] fn tls_deserialize_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error> { - hax_lib::fstar!("admit ()"); let ((length, _), remainder) = read_variable_length_bytes(bytes)?; if length == 0 { return Ok((Self::new(vec![]), remainder)); } if !cfg!(fuzzing) { + #[cfg(not(hax))] debug_assert!( length <= MAX_LEN as usize, "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.", @@ -374,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.", @@ -555,9 +556,8 @@ mod rw_bytes { // large and write it out. let content_length = bytes.len(); - hax_lib::fstar!("admit ()"); - 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}", @@ -574,6 +574,8 @@ mod rw_bytes { // Now serialize the elements writer.write_all(bytes)?; + hax_lib::fstar!("admit ()"); // overflow + Ok(content_length + len_len) } @@ -593,13 +595,13 @@ mod rw_bytes { impl Deserialize for VLBytes { fn tls_deserialize(bytes: &mut R) -> Result { - hax_lib::fstar!("admit ()"); let (length, _) = rw::read_length(bytes)?; if length == 0 { return Ok(Self::new(vec![])); } if !cfg!(fuzzing) { + #[cfg(not(hax))] debug_assert!( length <= MAX_LEN as usize, "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.", diff --git a/tls_codec/src/tls_vec.rs b/tls_codec/src/tls_vec.rs index 815208a76..1ea952790 100644 --- a/tls_codec/src/tls_vec.rs +++ b/tls_codec/src/tls_vec.rs @@ -98,7 +98,7 @@ macro_rules! impl_deserialize { while (read - len_len) < len.try_into().unwrap() { hax_lib::loop_invariant!(read >= len_len); let element = T::tls_deserialize(bytes)?; - hax_lib::assume!(read < 1000 && element.tls_serialized_len() < 1000); // overflow + hax_lib::fstar!("admit ()"); // overflow read += element.tls_serialized_len(); result.push(element); } @@ -119,7 +119,7 @@ macro_rules! impl_deserialize_bytes { hax_lib::loop_invariant!(read >= len_len); let (element, next_remainder) = T::tls_deserialize_bytes(remainder)?; remainder = next_remainder; - hax_lib::assume!(read < 1000 && element.tls_serialized_len() < 1000); // overflow + hax_lib::fstar!("admit ()"); // overflow read += element.tls_serialized_len(); result.push(element); } @@ -180,7 +180,7 @@ macro_rules! impl_serialize_common { $(#[$std_enabled])? fn get_content_lengths(&$self) -> Result<(usize, usize), Error> { let tls_serialized_len = $self.tls_serialized_len(); - hax_lib::assume!(tls_serialized_len > $len_len); + hax_lib::assume!(tls_serialized_len > $len_len); // underflow let byte_length = tls_serialized_len - $len_len; let max_len = <$size>::MAX.try_into().unwrap(); #[cfg(not(hax))] @@ -449,19 +449,19 @@ macro_rules! impl_tls_vec_generic { } } - #[hax_lib::opaque] // index precondition impl core::ops::Index for $name { type Output = T; #[inline] fn index(&self, i: usize) -> &T { + hax_lib::fstar!("admit ()"); // index precondition self.vec.index(i) } } - #[hax_lib::opaque] // translation uses =., why? impl core::cmp::PartialEq for $name { fn eq(&self, other: &Self) -> bool { + hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1704 self.vec.eq(&other.vec) } } From 8bdf96fa2d95b09188190c6746240093dc1518dc Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 25 Sep 2025 11:14:19 +0200 Subject: [PATCH 03/13] Avoid unused variable for hax. --- tls_codec/src/primitives.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs index 64c47ec08..fbef1fd53 100644 --- a/tls_codec/src/primitives.rs +++ b/tls_codec/src/primitives.rs @@ -34,7 +34,7 @@ impl Serialize for Option { match self { Some(e) => { let written = writer.write(&[1])?; - #[cfg(not(hax))] + hax_lib::assume!(written == 1); debug_assert_eq!(written, 1); e.tls_serialize(writer).map(|l| { hax_lib::fstar!("admit ()"); // overflow From b37c3e04a295e6109ac1d80eb6dd42a4e901674d Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 25 Sep 2025 11:35:25 +0200 Subject: [PATCH 04/13] Use right hax version, and type check F*. --- .github/workflows/tls_codec.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/tls_codec.yml b/.github/workflows/tls_codec.yml index d41e20d14..b047eafe2 100644 --- a/.github/workflows/tls_codec.yml +++ b/.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/ \ No newline at end of file + run: make -C proofs/fstar/extraction/ \ No newline at end of file From bb2cc8a8c1c1820f467807447e2138173a08f76d Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 25 Sep 2025 16:01:02 +0200 Subject: [PATCH 05/13] Use checked_add wherever possible to prove absence of overflows. --- Cargo.lock | 6 +++--- tls_codec/src/primitives.rs | 34 ++++++++++++++++++++-------------- tls_codec/src/quic_vec.rs | 13 +++++++------ tls_codec/src/tls_vec.rs | 24 +++++++++++------------- 4 files changed, 41 insertions(+), 36 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index d98c5998b..070242aa6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -740,7 +740,7 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" [[package]] name = "hax-lib" version = "0.3.4" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#dece8bb8e811c747639f7c7595978fb00b726fa9" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#a06153e29dd8eaab49ccda66a6b9e482980360e0" dependencies = [ "hax-lib-macros", "num-bigint", @@ -750,7 +750,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" version = "0.3.4" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#dece8bb8e811c747639f7c7595978fb00b726fa9" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#a06153e29dd8eaab49ccda66a6b9e482980360e0" dependencies = [ "hax-lib-macros-types", "proc-macro-error2", @@ -762,7 +762,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" version = "0.3.4" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#dece8bb8e811c747639f7c7595978fb00b726fa9" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#a06153e29dd8eaab49ccda66a6b9e482980360e0" dependencies = [ "proc-macro2", "quote", diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs index fbef1fd53..830fbcb41 100644 --- a/tls_codec/src/primitives.rs +++ b/tls_codec/src/primitives.rs @@ -36,10 +36,9 @@ impl Serialize for Option { let written = writer.write(&[1])?; hax_lib::assume!(written == 1); debug_assert_eq!(written, 1); - e.tls_serialize(writer).map(|l| { - hax_lib::fstar!("admit ()"); // overflow - l + 1 - }) + e.tls_serialize(writer)? + .checked_add(1) + .ok_or(Error::LibraryError) } None => { writer.write_all(&[0])?; @@ -54,8 +53,11 @@ impl SerializeBytes for Option { fn tls_serialize(&self) -> Result, Error> { match self { Some(e) => { - hax_lib::fstar!("admit ()"); // overflow - let mut out = Vec::with_capacity(e.tls_serialized_len() + 1); + let mut out = Vec::with_capacity( + e.tls_serialized_len() + .checked_add(1) + .ok_or(Error::LibraryError)?, + ); out.push(1); // Not inlining serialized_e is a workaround for // https://github.com/cryspen/hax/issues/1584 @@ -243,10 +245,10 @@ where #[inline(always)] fn tls_serialize(&self, writer: &mut W) -> Result { let written = self.0.tls_serialize(writer)?; - self.1.tls_serialize(writer).map(|l| { - hax_lib::fstar!("admit ()"); // overflow - l + written - }) + self.1 + .tls_serialize(writer)? + .checked_add(written) + .ok_or(Error::LibraryError) } } @@ -303,10 +305,14 @@ where #[cfg(feature = "std")] #[inline(always)] fn tls_serialize(&self, writer: &mut W) -> Result { - 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) + let written = self.0.tls_serialize(writer)?; + let written = written + .checked_add(self.1.tls_serialize(writer)?) + .ok_or(Error::LibraryError)?; + self.2 + .tls_serialize(writer)? + .checked_add(written) + .ok_or(Error::LibraryError) } } diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs index 333d396b1..c20eb3d72 100644 --- a/tls_codec/src/quic_vec.rs +++ b/tls_codec/src/quic_vec.rs @@ -132,8 +132,8 @@ pub fn write_variable_length(content_length: usize) -> Result, Error> { } let mut len = content_length; let l = length_bytes.len(); - hax_lib::fstar!("admit ()"); // underflows for i in 0..l { + hax_lib::loop_invariant!(|_: usize| length_bytes.len() == 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); len >>= 8; @@ -172,8 +172,9 @@ impl DeserializeBytes for Vec { 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(); + read = read + .checked_add(element.tls_serialized_len()) + .ok_or(Error::LibraryError)?; result.push(element); } Ok((result, remainder)) @@ -574,9 +575,9 @@ mod rw_bytes { // Now serialize the elements writer.write_all(bytes)?; - hax_lib::fstar!("admit ()"); // overflow - - Ok(content_length + len_len) + content_length + .checked_add(len_len) + .ok_or(Error::LibraryError) } impl Serialize for VLBytes { diff --git a/tls_codec/src/tls_vec.rs b/tls_codec/src/tls_vec.rs index 1ea952790..242a45683 100644 --- a/tls_codec/src/tls_vec.rs +++ b/tls_codec/src/tls_vec.rs @@ -65,7 +65,7 @@ macro_rules! impl_byte_deserialize { #[inline(always)] fn deserialize_bytes_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error> { let (type_len, remainder) = <$size>::tls_deserialize_bytes(bytes)?; - let len = type_len.try_into().unwrap(); + let len: usize = type_len.try_into().unwrap(); // When fuzzing we limit the maximum size to allocate. // XXX: We should think about a configurable limit for the allocation // here. @@ -76,10 +76,8 @@ macro_rules! impl_byte_deserialize { u16::MAX ))); } - hax_lib::fstar!("admit ()"); // overflow - let vec = bytes - .get($len_len..len + $len_len) - .ok_or(Error::EndOfStream)?; + let end = len.checked_add($len_len).ok_or(Error::LibraryError)?; + let vec = bytes.get($len_len..end).ok_or(Error::EndOfStream)?; let result = Self { vec: vec.to_vec() }; Ok((result, &remainder.get(len..).ok_or(Error::EndOfStream)?)) } @@ -98,8 +96,9 @@ macro_rules! impl_deserialize { while (read - len_len) < len.try_into().unwrap() { hax_lib::loop_invariant!(read >= len_len); let element = T::tls_deserialize(bytes)?; - hax_lib::fstar!("admit ()"); // overflow - read += element.tls_serialized_len(); + read = read + .checked_add(element.tls_serialized_len()) + .ok_or(Error::LibraryError)?; result.push(element); } Ok(result) @@ -119,8 +118,9 @@ macro_rules! impl_deserialize_bytes { 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(); + read = read + .checked_add(element.tls_serialized_len()) + .ok_or(Error::LibraryError)?; result.push(element); } Ok((result, remainder)) @@ -165,9 +165,8 @@ macro_rules! impl_byte_serialize { hax_lib::fstar!("admit ()"); // Need to prove unwrap for usize to U24 let mut written = <$size as Serialize>::tls_serialize(&<$size>::try_from(byte_length).unwrap(), writer)?; - hax_lib::fstar!("admit ()"); // overflow // Now serialize the elements - written += writer.write($self.as_slice())?; + written = written.checked_add(writer.write($self.as_slice())?).ok_or(Error::LibraryError)?; $self.assert_written_bytes(tls_serialized_len, written)?; Ok(written) @@ -180,8 +179,7 @@ macro_rules! impl_serialize_common { $(#[$std_enabled])? fn get_content_lengths(&$self) -> Result<(usize, usize), Error> { let tls_serialized_len = $self.tls_serialized_len(); - hax_lib::assume!(tls_serialized_len > $len_len); // underflow - let byte_length = tls_serialized_len - $len_len; + let byte_length = tls_serialized_len.checked_sub($len_len).ok_or(Error::InvalidVectorLength)?; let max_len = <$size>::MAX.try_into().unwrap(); #[cfg(not(hax))] debug_assert!( From babaf7c6b8266655d00ea96f46361413daecb678 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 25 Sep 2025 16:11:46 +0200 Subject: [PATCH 06/13] Add preconditions for 'index' methods panic freedom. --- tls_codec/src/quic_vec.rs | 6 ++++-- tls_codec/src/tls_vec.rs | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs index c20eb3d72..e6f1bbded 100644 --- a/tls_codec/src/quic_vec.rs +++ b/tls_codec/src/quic_vec.rs @@ -482,10 +482,12 @@ pub mod rw { let mut result = Vec::new(); let mut read = len_len; - hax_lib::fstar!("admit ()"); // underflow while (read - len_len) < length { + hax_lib::loop_invariant!(read >= len_len); let element = T::tls_deserialize(bytes)?; - read += element.tls_serialized_len(); + read = read + .checked_add(element.tls_serialized_len()) + .ok_or(Error::LibraryError)?; result.push(element); } Ok(result) diff --git a/tls_codec/src/tls_vec.rs b/tls_codec/src/tls_vec.rs index 242a45683..f2ce3c2de 100644 --- a/tls_codec/src/tls_vec.rs +++ b/tls_codec/src/tls_vec.rs @@ -447,12 +447,13 @@ macro_rules! impl_tls_vec_generic { } } + #[hax_lib::attributes] impl core::ops::Index for $name { type Output = T; #[inline] + #[hax_lib::requires(i < self.vec.len())] fn index(&self, i: usize) -> &T { - hax_lib::fstar!("admit ()"); // index precondition self.vec.index(i) } } @@ -648,12 +649,13 @@ macro_rules! impl_tls_vec { } } + #[hax_lib::attributes] impl core::ops::Index for $name { type Output = u8; #[inline] + #[hax_lib::requires(i < self.vec.len())] fn index(&self, i: usize) -> &u8 { - hax_lib::fstar!("admit ()"); // index precondition self.vec.index(i) } } From 244dacc02a505926173319cd21b9c9783f64b5b6 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 15 Oct 2025 16:51:59 +0200 Subject: [PATCH 07/13] Make more future proof assumption about LEN. --- tls_codec/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tls_codec/src/lib.rs b/tls_codec/src/lib.rs index f46e3b725..b533f9061 100644 --- a/tls_codec/src/lib.rs +++ b/tls_codec/src/lib.rs @@ -291,7 +291,7 @@ impl From for usize { fn from(value: U24) -> usize { const LEN: usize = core::mem::size_of::(); let mut usize_bytes = [0u8; LEN]; - hax_lib::assume!(LEN == 8); // https://github.com/cryspen/hax/issues/1702 + 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) } @@ -307,7 +307,7 @@ impl TryFrom for U24 { if value > (1 << 24) - 1 { Err(Error::LibraryError) } else { - hax_lib::assume!(LEN == 8); // https://github.com/cryspen/hax/issues/1702 + 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()?)) } } From 4dad4572de93ef00293caf6cddb1888d64780729 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 15 Oct 2025 16:52:08 +0200 Subject: [PATCH 08/13] Update hax-lib. --- Cargo.lock | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 070242aa6..d777d20a3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -739,8 +739,8 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" [[package]] name = "hax-lib" -version = "0.3.4" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#a06153e29dd8eaab49ccda66a6b9e482980360e0" +version = "0.3.5" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747" dependencies = [ "hax-lib-macros", "num-bigint", @@ -749,8 +749,8 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.3.4" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#a06153e29dd8eaab49ccda66a6b9e482980360e0" +version = "0.3.5" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747" dependencies = [ "hax-lib-macros-types", "proc-macro-error2", @@ -761,8 +761,8 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.3.4" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#a06153e29dd8eaab49ccda66a6b9e482980360e0" +version = "0.3.5" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747" dependencies = [ "proc-macro2", "quote", From ef5bf15590e8b4f968d350bd642fc8ea65ced867 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 15 Oct 2025 18:04:25 +0200 Subject: [PATCH 09/13] First try for checked version of tls_serialized_len. --- tls_codec/derive/src/lib.rs | 23 +++++++++ tls_codec/derive/tests/decode.rs | 8 +++ tls_codec/derive/tests/decode_bytes.rs | 4 ++ tls_codec/derive/tests/encode.rs | 4 ++ tls_codec/derive/tests/encode_bytes.rs | 4 ++ tls_codec/src/arrays.rs | 4 ++ tls_codec/src/lib.rs | 2 + tls_codec/src/primitives.rs | 69 ++++++++++++++++++++++---- tls_codec/src/quic_vec.rs | 61 +++++++++++++++++------ tls_codec/src/tls_vec.rs | 52 +++++++++++++++---- 10 files changed, 195 insertions(+), 36 deletions(-) diff --git a/tls_codec/derive/src/lib.rs b/tls_codec/derive/src/lib.rs index f132943a2..2f38c8410 100644 --- 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 { +//! TlsByteSliceU32(v).tls_serialized_len_checked() +//! } +//! //! pub fn tls_serialize(v: &[u8], writer: &mut W) -> Result { //! TlsByteSliceU32(v).tls_serialize(writer) //! } @@ -787,6 +791,10 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 { #(#prefixes::tls_serialized_len(&self.#members) + )* 0 } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + Some(0usize#(.checked_add(#prefixes::tls_serialized_len_checked(&self.#members)?)?)*) + } } impl #impl_generics tls_codec::Size for &#ident #ty_generics #where_clause { @@ -794,6 +802,10 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 { fn tls_serialized_len(&self) -> usize { tls_codec::Size::tls_serialized_len(*self) } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + tls_codec::Size::tls_serialized_len_checked(*self) + } } } } @@ -827,6 +839,13 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 { }; core::mem::size_of::<#repr>() + field_len } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + 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 { @@ -834,6 +853,10 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 { fn tls_serialized_len(&self) -> usize { tls_codec::Size::tls_serialized_len(*self) } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + tls_codec::Size::tls_serialized_len_checked(*self) + } } } } diff --git a/tls_codec/derive/tests/decode.rs b/tls_codec/derive/tests/decode.rs index 0238cf4a6..a3135ffe6 100644 --- 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 { + TlsByteSliceU32(v).tls_serialized_len_checked() + } + pub fn tls_serialize(v: &[u8], writer: &mut W) -> Result { 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 { + TlsByteSliceU32(v).tls_serialized_len_checked() + } + pub fn tls_serialize(v: &[u8], writer: &mut W) -> Result { TlsByteSliceU32(v).tls_serialize(writer) } diff --git a/tls_codec/derive/tests/decode_bytes.rs b/tls_codec/derive/tests/decode_bytes.rs index 2c42f0638..e78fe9801 100644 --- 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 { + v.tls_serialized_len_checked() + } + pub fn tls_serialize(v: &[u8]) -> Result, tls_codec::Error> { v.tls_serialize() } diff --git a/tls_codec/derive/tests/encode.rs b/tls_codec/derive/tests/encode.rs index 4830e99a9..7cd6f31f2 100644 --- 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 { + TlsByteSliceU32(v).tls_serialized_len_checked() + } + pub fn tls_serialize(v: &[u8], writer: &mut W) -> Result { TlsByteSliceU32(v).tls_serialize(writer) } diff --git a/tls_codec/derive/tests/encode_bytes.rs b/tls_codec/derive/tests/encode_bytes.rs index 089549f99..4052e249b 100644 --- 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 { + v.tls_serialized_len_checked() + } + pub fn tls_serialize(v: &[u8]) -> Result, tls_codec::Error> { v.tls_serialize() } diff --git a/tls_codec/src/arrays.rs b/tls_codec/src/arrays.rs index 52fa3339f..b974778c1 100644 --- a/tls_codec/src/arrays.rs +++ b/tls_codec/src/arrays.rs @@ -51,4 +51,8 @@ impl Size for [u8; LEN] { fn tls_serialized_len(&self) -> usize { LEN } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + Some(LEN) + } } diff --git a/tls_codec/src/lib.rs b/tls_codec/src/lib.rs index b533f9061..27bb85679 100644 --- 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; #[hax_lib::requires(true)] fn tls_serialized_len(&self) -> usize; } diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs index 830fbcb41..17b17e0a3 100644 --- a/tls_codec/src/primitives.rs +++ b/tls_codec/src/primitives.rs @@ -12,12 +12,20 @@ use std::io::{Read, Write}; impl Size for Option { #[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 { + 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 Size for &Option { fn tls_serialized_len(&self) -> usize { (*self).tls_serialized_len() } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + (*self).tls_serialized_len_checked() + } } impl Serialize for Option { @@ -187,6 +199,10 @@ macro_rules! impl_unsigned { fn tls_serialized_len(&self) -> usize { $bytes } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + Some($bytes) + } } impl Size for &$t { @@ -194,6 +210,10 @@ macro_rules! impl_unsigned { fn tls_serialized_len(&self) -> usize { (*self).tls_serialized_len() } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { + (*self).tls_serialized_len_checked() + } } }; } @@ -257,10 +277,18 @@ where T: Size, U: Size, { + #[inline(always)] + fn tls_serialized_len_checked(&self) -> Option { + 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 { + 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 { + Some(0) + } } impl Deserialize for () { @@ -363,6 +406,10 @@ impl Size for PhantomData { fn tls_serialized_len(&self) -> usize { 0 } + #[inline(always)] + fn tls_serialized_len_checked(&self) -> Option { + Some(0) + } } impl Deserialize for PhantomData { @@ -400,6 +447,10 @@ impl Size for Box { fn tls_serialized_len(&self) -> usize { self.as_ref().tls_serialized_len() } + #[inline(always)] + fn tls_serialized_len_checked(&self) -> Option { + self.as_ref().tls_serialized_len_checked() + } } impl Serialize for Box { diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs index e6f1bbded..e66d7a51d 100644 --- a/tls_codec/src/quic_vec.rs +++ b/tls_codec/src/quic_vec.rs @@ -147,6 +147,10 @@ impl Size for Vec { fn tls_serialized_len(&self) -> usize { self.as_slice().tls_serialized_len() } + #[inline(always)] + fn tls_serialized_len_checked(&self) -> Option { + self.as_slice().tls_serialized_len_checked() + } } impl Size for &Vec { @@ -154,6 +158,10 @@ impl Size for &Vec { fn tls_serialized_len(&self) -> usize { (*self).tls_serialized_len() } + #[inline(always)] + fn tls_serialized_len_checked(&self) -> Option { + (*self).tls_serialized_len_checked() + } } impl DeserializeBytes for Vec { @@ -225,17 +233,23 @@ impl SerializeBytes for Vec { } } +fn serialized_len_checked_slice(s: &[T]) -> Option { + 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 Size for &[T] { + #[inline(always)] + fn tls_serialized_len_checked(&self) -> Option { + 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 for Vec { } #[inline(always)] -fn tls_serialize_bytes_len(bytes: &[u8]) -> usize { +fn tls_serialize_bytes_len(bytes: &[u8]) -> Option { 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 { 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 { + (*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 { tls_serialize_bytes_len(self.0) } } impl Size for VLByteSlice<'_> { #[inline] - fn tls_serialized_len(&self) -> usize { + fn tls_serialized_len_checked(&self) -> Option { 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 { + 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 index f2ce3c2de..17a5dd123 100644 --- a/tls_codec/src/tls_vec.rs +++ b/tls_codec/src/tls_vec.rs @@ -19,11 +19,11 @@ macro_rules! impl_size { ($self:ident, $size:ty, $name:ident, $len_len:literal) => { /// The serialized len #[inline(always)] - fn tls_serialized_length(&$self) -> usize { + fn tls_serialized_length(&$self) -> Option { hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700 $self.as_slice() .iter() - .fold($len_len, |acc, e| acc + e.tls_serialized_len()) + .fold(Some($len_len), |acc, e| acc?.checked_add(e.tls_serialized_len_checked()?)) } } } @@ -32,9 +32,8 @@ macro_rules! impl_byte_size { ($self:ident, $size:ty, $name:ident, $len_len:literal) => { /// The serialized len #[inline(always)] - fn tls_serialized_byte_length(&$self) -> usize { - hax_lib::fstar!("admit ()"); // overflow - $self.as_slice().len() + $len_len + fn tls_serialized_byte_length(&$self) -> Option { + $self.as_slice().len().checked_add($len_len) } } } @@ -247,6 +246,10 @@ macro_rules! impl_tls_vec_codec_generic { impl Size for $name { #[inline] fn tls_serialized_len(&self) -> usize { + self.tls_serialized_length().unwrap_or(0) + } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_length() } } @@ -261,6 +264,10 @@ macro_rules! impl_tls_vec_codec_generic { impl Size for &$name { #[inline] fn tls_serialized_len(&self) -> usize { + self.tls_serialized_length().unwrap_or(0) + } + #[inline] + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_length() } } @@ -291,9 +298,12 @@ macro_rules! impl_tls_vec_codec_bytes { impl Size for $name { #[inline] - fn tls_serialized_len(&self) -> usize { + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_byte_length() } + fn tls_serialized_len(&self) -> usize { + self.tls_serialized_byte_length().unwrap_or(0) + } } impl Serialize for &$name { @@ -305,9 +315,13 @@ macro_rules! impl_tls_vec_codec_bytes { impl Size for &$name { #[inline] - fn tls_serialized_len(&self) -> usize { + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_byte_length() } + #[inline] + fn tls_serialized_len(&self) -> usize { + self.tls_serialized_byte_length().unwrap_or(0) + } } impl Deserialize for $name { @@ -956,16 +970,24 @@ macro_rules! impl_tls_byte_slice { impl<'a> Size for &$name<'a> { #[inline] - fn tls_serialized_len(&self) -> usize { + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_byte_length() } + #[inline] + fn tls_serialized_len(&self) -> usize { + self.tls_serialized_byte_length().unwrap_or(0) + } } impl<'a> Size for $name<'a> { #[inline] - fn tls_serialized_len(&self) -> usize { + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_byte_length() } + #[inline] + fn tls_serialized_len(&self) -> usize { + self.tls_serialized_byte_length().unwrap_or(0) + } } }; } @@ -1012,16 +1034,24 @@ macro_rules! impl_tls_slice { impl<'a, T: Size> Size for &$name<'a, T> { #[inline] - fn tls_serialized_len(&self) -> usize { + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_length() } + #[inline] + fn tls_serialized_len(&self) -> usize { + self.tls_serialized_length().unwrap_or(0) + } } impl<'a, T: Size> Size for $name<'a, T> { #[inline] - fn tls_serialized_len(&self) -> usize { + fn tls_serialized_len_checked(&self) -> Option { self.tls_serialized_length() } + #[inline] + fn tls_serialized_len(&self) -> usize { + self.tls_serialized_length().unwrap_or(0) + } } }; } From 252449d864b64e1d981dad6f3c2b00f992db27fd Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 16 Oct 2025 11:03:17 +0200 Subject: [PATCH 10/13] Fix clippy warnings. --- tls_codec/derive/src/lib.rs | 1 + tls_codec/src/quic_vec.rs | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/tls_codec/derive/src/lib.rs b/tls_codec/derive/src/lib.rs index 2f38c8410..c3925a1c0 100644 --- a/tls_codec/derive/src/lib.rs +++ b/tls_codec/derive/src/lib.rs @@ -792,6 +792,7 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 { 0 } #[inline] + #[allow(clippy::needless_question_mark)] fn tls_serialized_len_checked(&self) -> Option { Some(0usize#(.checked_add(#prefixes::tls_serialized_len_checked(&self.#members)?)?)*) } diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs index e66d7a51d..8a667788e 100644 --- a/tls_codec/src/quic_vec.rs +++ b/tls_codec/src/quic_vec.rs @@ -235,8 +235,8 @@ impl SerializeBytes for Vec { fn serialized_len_checked_slice(s: &[T]) -> Option { 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 content_length = s.iter().try_fold(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) From 4ef85151b0aa6a17fe3b2640cee9b9d2c4c661ef Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 16 Oct 2025 11:22:04 +0200 Subject: [PATCH 11/13] Remove try_fold which is not supported by hax. --- tls_codec/src/quic_vec.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs index 8a667788e..2ede8f221 100644 --- a/tls_codec/src/quic_vec.rs +++ b/tls_codec/src/quic_vec.rs @@ -233,10 +233,11 @@ impl SerializeBytes for Vec { } } +#[allow(clippy::manual_try_fold)] fn serialized_len_checked_slice(s: &[T]) -> Option { hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700 - let content_length = s.iter().try_fold(0usize, |acc, e| { - acc.checked_add(e.tls_serialized_len_checked()?) + 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) From 26c59bcb489215add190635065acba01b17f355a Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 16 Oct 2025 11:23:10 +0200 Subject: [PATCH 12/13] rename f* type checking step. --- .github/workflows/tls_codec.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/tls_codec.yml b/.github/workflows/tls_codec.yml index b047eafe2..09ce78329 100644 --- a/.github/workflows/tls_codec.yml +++ b/.github/workflows/tls_codec.yml @@ -89,5 +89,5 @@ jobs: hax_reference: tls-codec-panic-freedom - name: 🏃 Extract F* run: cargo hax into fstar - - name: 🏃 Lax-check extracted F* + - name: 🏃 Type-check extracted F* run: make -C proofs/fstar/extraction/ \ No newline at end of file From 5c7f5c227876e285f78761de2a359a482e005fde Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 11 Dec 2025 10:51:39 +0100 Subject: [PATCH 13/13] First correctness proofs. --- Cargo.lock | 6 ++--- tls_codec/proofs/fstar/models/Zeroize.fsti | 2 +- tls_codec/src/lib.rs | 7 ++++++ tls_codec/src/primitives.rs | 29 ++++++++++++++++++++++ tls_codec/src/tls_vec.rs | 1 + 5 files changed, 41 insertions(+), 4 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index d777d20a3..52b4d2dc5 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -740,7 +740,7 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" [[package]] name = "hax-lib" version = "0.3.5" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#ec426c36e8cdfaf68cdc4d6e44206288e4029d21" dependencies = [ "hax-lib-macros", "num-bigint", @@ -750,7 +750,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" version = "0.3.5" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#ec426c36e8cdfaf68cdc4d6e44206288e4029d21" dependencies = [ "hax-lib-macros-types", "proc-macro-error2", @@ -762,7 +762,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" version = "0.3.5" -source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747" +source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#ec426c36e8cdfaf68cdc4d6e44206288e4029d21" dependencies = [ "proc-macro2", "quote", diff --git a/tls_codec/proofs/fstar/models/Zeroize.fsti b/tls_codec/proofs/fstar/models/Zeroize.fsti index 6f98281fa..91452775e 100644 --- a/tls_codec/proofs/fstar/models/Zeroize.fsti +++ b/tls_codec/proofs/fstar/models/Zeroize.fsti @@ -1,6 +1,6 @@ module Zeroize #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core +open Core_models open FStar.Mul class t_Zeroize (v_Self: Type0) = { diff --git a/tls_codec/src/lib.rs b/tls_codec/src/lib.rs index 27bb85679..26c733b97 100644 --- a/tls_codec/src/lib.rs +++ b/tls_codec/src/lib.rs @@ -276,19 +276,26 @@ pub trait DeserializeBytes: Size { #[derive(Copy, Clone, Debug, Default, PartialEq)] pub struct U24([u8; 3]); +#[hax_lib::attributes] impl U24 { pub const MAX: Self = Self([255u8; 3]); pub const MIN: Self = Self([0u8; 3]); + #[hax_lib::ensures(|res| res == U24(bytes))] pub fn from_be_bytes(bytes: [u8; 3]) -> Self { U24(bytes) } + #[hax_lib::ensures(|res| self.0 == res)] pub fn to_be_bytes(self) -> [u8; 3] { self.0 } } +#[hax_lib::lemma] +#[hax_lib::opaque] +fn size_of_u24_lemma() -> Proof<{core::mem::size_of::() == 3}> {} + impl From for usize { fn from(value: U24) -> usize { const LEN: usize = core::mem::size_of::(); diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs index 17b17e0a3..758232b44 100644 --- a/tls_codec/src/primitives.rs +++ b/tls_codec/src/primitives.rs @@ -74,6 +74,7 @@ impl SerializeBytes for Option { // Not inlining serialized_e is a workaround for // https://github.com/cryspen/hax/issues/1584 let mut serialized_e = e.tls_serialize()?; + hax_lib::assume!(serialized_e.len() == e.tls_serialized_len()); out.append(&mut serialized_e); Ok(out) } @@ -145,10 +146,19 @@ macro_rules! impl_unsigned { } } + #[hax_lib::attributes] impl DeserializeBytes for $t { #[inline] + #[hax_lib::ensures(|res| { + let len = core::mem::size_of::<$t>(); + hax_lib::assume!(core::mem::size_of::() == 3); + hax_lib::implies( + bytes.len() >= len, + res == Ok((<$t>::from_be_bytes(bytes[..len].try_into().unwrap()), &bytes[len..])) + )})] fn tls_deserialize_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error> { let len = core::mem::size_of::<$t>(); + hax_lib::assume!(core::mem::size_of::() == 3); let out = bytes .get(..len) .ok_or(Error::EndOfStream)? @@ -161,15 +171,34 @@ macro_rules! impl_unsigned { } } + #[hax_lib::attributes] impl SerializeBytes for &$t { #[inline] + #[hax_lib::ensures(|res| { + if let Ok(serialized) = res { + if let Ok((deserialized, stream)) = $t::tls_deserialize_bytes(&serialized) { + return **self == deserialized && stream.is_empty() + } + } + false + })] fn tls_serialize(&self) -> Result, Error> { + hax_lib::assume!(core::mem::size_of::() == 3); Ok(self.to_be_bytes().to_vec()) } } + #[hax_lib::attributes] impl SerializeBytes for $t { #[inline] + #[hax_lib::ensures(|res| { + if let Ok(serialized) = res { + if let Ok((deserialized, stream)) = $t::tls_deserialize_bytes(&serialized) { + return *self == deserialized && stream.is_empty() + } + } + false + })] fn tls_serialize(&self) -> Result, Error> { <&Self as SerializeBytes>::tls_serialize(&self) } diff --git a/tls_codec/src/tls_vec.rs b/tls_codec/src/tls_vec.rs index 17a5dd123..25372e9cf 100644 --- a/tls_codec/src/tls_vec.rs +++ b/tls_codec/src/tls_vec.rs @@ -403,6 +403,7 @@ macro_rules! impl_vec_members { /// Remove the element at `index`. #[inline] pub fn remove(&mut self, index: usize) -> $element_type { + hax_lib::assume!(self.vec.len() > index); self.vec.remove(index) }