Generic Types and Comparison

[aa-luna]

NonZero Link
Initially we tried to implement a comparison in requires/ensure so that :

#[requires(n != T::Zero())]
#[ensures(|result: Self| result.get() == n)]

Seems like the issue is Zero or .get() is not associated with T, generic type. We are also unable to compare variables and recommended to add PartialEq, but we see it already exists in line 172:

impl<T> PartialEq for NonZero<T>
where
T: ZeroablePrimitive + PartialEq,

Maybe we are calling it incorrectly? We also added PartialEq to the implementation block for new_unchecked but also received errors.

Would it be better to just use kani::proof with assume / asset for this type of harness?

[celinval]

Yeah, I understand the problem. The implementation for some of the NonZero<T> methods only requires T: ZeroablePrimitive, which doesn't provide any method to inspect or compare the T value.

In that case, I believe we'll have to work on a byte basis. For example, in order to check if a value is zero, you could get the address of the value, and create a *const [u8] where the len of the slice is the size of T. Then, you assume that it is safe to read from this slice, and check if any of the bytes is different than zero.

The same idea can be applied to compare values using byte comparison.

Please let me know if that makes sense or if anyone has any other solution.

[celinval]

Note that this solution assumes that T has no padding byte, which is definitely the case today.

I believe this is how the existing implementation guarantees that we can safely transmute between Self::NonZeroInner and Option<Self::NonZeroInner> (by ensuring there is only one invalid value that will be used in the niche optimization). But this is not future proof, and the trait itself does not explicitly states that T has no padding bytes.

Maybe it's something that we can bring to the library team later to confirm this assumption.

[feliperodri]

@aa-luna does the answer above answers your question? If yes, could you "mark as answer"?