From d3b7763e7b6bb79389d94a78f19892a9370c62e3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 09:19:24 +0000 Subject: [PATCH] Fix num::nonzero::NonZero::<*>::rotate_{left,right} contracts The result of a rotate operation is always non-zero, which could still be less than zero in case of signed types. Proofs were failing with the prior contract, but this still passed CI as we haven't yet picked up the Kani version where autoharness exits with a non-zero exit code in case of proof failure. --- library/core/src/num/nonzero.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 83ebd7fbe1922..97e7d68f63b11 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -755,7 +755,7 @@ macro_rules! nonzero_integer { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline(always)] - #[ensures(|result| result.get() > 0)] + #[ensures(|result| result.get() != 0)] #[ensures(|result| result.rotate_right(n).get() == old(self).get())] pub const fn rotate_left(self, n: u32) -> Self { let result = self.get().rotate_left(n); @@ -790,7 +790,7 @@ macro_rules! nonzero_integer { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline(always)] - #[ensures(|result| result.get() > 0)] + #[ensures(|result| result.get() != 0)] #[ensures(|result| result.rotate_left(n).get() == old(self).get())] pub const fn rotate_right(self, n: u32) -> Self { let result = self.get().rotate_right(n);