From ace125d9da7f35b67aa15f4c3a7b6dfb4908ebd9 Mon Sep 17 00:00:00 2001 From: ultrabear Date: Mon, 28 Jul 2025 19:02:35 -0700 Subject: [PATCH 1/3] implement perfect addition of two SizeHint's --- http-body/src/size_hint.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/http-body/src/size_hint.rs b/http-body/src/size_hint.rs index 2cad79d..d30b9c2 100644 --- a/http-body/src/size_hint.rs +++ b/http-body/src/size_hint.rs @@ -82,3 +82,17 @@ impl SizeHint { self.upper = Some(value); } } + +/// Perfectly adds two `SizeHint'`s +impl core::ops::Add for SizeHint { + type Output = SizeHint; + + fn add(self, rhs: Self) -> Self::Output { + SizeHint { + lower: self.lower() + rhs.lower(), + upper: self + .upper() + .and_then(|this| rhs.upper().map(|rhs| this + rhs)), + } + } +} From 34e8e34edc213ee968d34438a8e2d2bcedb9c115 Mon Sep 17 00:00:00 2001 From: ultrabear Date: Tue, 29 Jul 2025 09:16:05 -0700 Subject: [PATCH 2/3] add some basic tests --- http-body/src/size_hint.rs | 109 +++++++++++++++++++++++++++++++++++++ 1 file changed, 109 insertions(+) diff --git a/http-body/src/size_hint.rs b/http-body/src/size_hint.rs index d30b9c2..cd7b2bd 100644 --- a/http-body/src/size_hint.rs +++ b/http-body/src/size_hint.rs @@ -96,3 +96,112 @@ impl core::ops::Add for SizeHint { } } } + +/// Asserts that SizeHint addition is perfect with a basic proof +#[test] +fn size_hint_addition_proof() { + /// Converts a SizeHint to a tuple for equality checks and matching + fn to_parts(s: SizeHint) -> (u64, Option) { + (s.lower(), s.upper()) + } + + // assuming addition itself is perfect, there are 3 distinct states: + // (_, Some(_)) + (_, Some(_)) => (_ + _, Some(_ + _)) + // (_, Some(_)) + (_, None) => (_ + _, None) + // (_, None) + (_, None) => (_ + _, None) + // + // we can assert this in the typesystem! (and name them for our tests) + match (to_parts(SizeHint::new()), to_parts(SizeHint::new())) { + ((_, Some(_)), (_, Some(_))) => {} // 1 + ((_, None), (_, None)) => {} // 2 + + // note that these cases are identical if we can prove lhs + rhs is equivalent to rhs + lhs + // see below, we do prove that! + ((_, Some(_)), (_, None)) => {} // 3 + ((_, None), (_, Some(_))) => {} + } + // + // Additionally, we assert a with_exact remains intact if we add two with_exact's together + // + // Additionally, we assert that all operations are equivalent if we do a + b vs b + a + + // asserts a + b == b + a == eq + macro_rules! reciprocal_add_eq { + ($a:expr, $b:expr, $eq:expr) => { + assert_eq!(to_parts(($a.clone() + $b.clone())), $eq); + assert_eq!(to_parts(($b.clone() + $a.clone())), $eq); + }; + } + + // note that we use increasing powers of two every time we fetch a number, this ensures all + // numbers will add uniquely + + let exact_1 = SizeHint::with_exact(1); + let exact_2 = SizeHint::with_exact(2); + + // with_exact + reciprocal_add_eq!(exact_1, exact_2, to_parts(SizeHint::with_exact(3))); + + let some_lhs = SizeHint { + lower: 4, + upper: Some(8), + }; + + let some_rhs = SizeHint { + lower: 16, + upper: Some(32), + }; + + // case 1 + reciprocal_add_eq!(some_lhs, some_rhs, (4 + 16, Some(8 + 32))); + + let none_lhs = SizeHint { + lower: 64, + upper: None, + }; + + let none_rhs = SizeHint { + lower: 128, + upper: None, + }; + + // case 2 + reciprocal_add_eq!(none_lhs, none_rhs, (64 + 128, None)); + + // case 3 + reciprocal_add_eq!(some_lhs, none_rhs, (4 + 128, None)); +} + +/// Asserts that some "real data" gets passed through without issue +#[test] +fn size_hint_addition_basic() { + let exact_l = SizeHint::with_exact(20); + let exact_r = SizeHint::with_exact(5); + + assert_eq!(Some(25), (exact_l.clone() + exact_r).exact()); + + let inexact_l = SizeHint { + lower: 25, + upper: None, + }; + let inexact_r = SizeHint { + lower: 10, + upper: Some(50), + }; + + let inexact = inexact_l + inexact_r.clone(); + + assert_eq!(inexact.lower(), 35); + assert_eq!(inexact.upper(), None); + + let exact_inexact = exact_l.clone() + inexact_r.clone(); + + assert_eq!(exact_inexact.lower(), 30); + assert_eq!(exact_inexact.upper(), Some(70)); + + // same as previous but reversed operation order + let inexact_exact = inexact_r + exact_l; + + assert_eq!(inexact_exact.lower(), 30); + assert_eq!(inexact_exact.upper(), Some(70)); +} From 8f8962dc18ac62fb887d07568d2c82eb2e2f03e3 Mon Sep 17 00:00:00 2001 From: ultrabear Date: Tue, 29 Jul 2025 09:20:33 -0700 Subject: [PATCH 3/3] change to 1 + 2 for consistency --- http-body/src/size_hint.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/http-body/src/size_hint.rs b/http-body/src/size_hint.rs index cd7b2bd..4b477fc 100644 --- a/http-body/src/size_hint.rs +++ b/http-body/src/size_hint.rs @@ -140,7 +140,7 @@ fn size_hint_addition_proof() { let exact_2 = SizeHint::with_exact(2); // with_exact - reciprocal_add_eq!(exact_1, exact_2, to_parts(SizeHint::with_exact(3))); + reciprocal_add_eq!(exact_1, exact_2, to_parts(SizeHint::with_exact(1 + 2))); let some_lhs = SizeHint { lower: 4,