Ipv6Addr

tautschnig · tautschnig · commit 07490e9decbf · 2025-07-10T17:40:34.000Z
diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs
@@ -645,13 +645,15 @@ impl Step for Ipv6Addr {
         u128::backward_checked(start.to_bits(), count).map(Ipv6Addr::from_bits)
     }
 
+    #[requires(start.to_bits().checked_add(count as u128).is_some())]
     #[inline]
     unsafe fn forward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {
         // SAFETY: Since u128 and Ipv6Addr are losslessly convertible,
         //   this is as safe as the u128 version.
         Ipv6Addr::from_bits(unsafe { u128::forward_unchecked(start.to_bits(), count) })
     }
 
+    #[requires(start.to_bits().checked_sub(count as u128).is_some())]
     #[inline]
     unsafe fn backward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {
         // SAFETY: Since u128 and Ipv6Addr are losslessly convertible,

Original file line number	Diff line number	Diff line change
`@@ -645,13 +645,15 @@ impl Step for Ipv6Addr {`
`645`	`645`	`u128::backward_checked(start.to_bits(), count).map(Ipv6Addr::from_bits)`
`646`	`646`	`}`
`647`	`647`
	`648`	`+ #[requires(start.to_bits().checked_add(count as u128).is_some())]`
`648`	`649`	`#[inline]`
`649`	`650`	`unsafe fn forward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {`
`650`	`651`	`// SAFETY: Since u128 and Ipv6Addr are losslessly convertible,`
`651`	`652`	`// this is as safe as the u128 version.`
`652`	`653`	`Ipv6Addr::from_bits(unsafe { u128::forward_unchecked(start.to_bits(), count) })`
`653`	`654`	`}`
`654`	`655`
	`656`	`+ #[requires(start.to_bits().checked_sub(count as u128).is_some())]`
`655`	`657`	`#[inline]`
`656`	`658`	`unsafe fn backward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {`
`657`	`659`	`// SAFETY: Since u128 and Ipv6Addr are losslessly convertible,`