Fix num::nonzero::NonZero::<*>::rotate_{left,right} contracts (model-checking#346)

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.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

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);