NonZero (unchecked_mul & unchecked_add) Proof for Contracts (Init)

[SahithiMV]

Working on #71 (Safety of NonZero)

We are looking for feedback on our proof_for_contracts for unchecked_mul and unchecked_add.
This is the initial logic; we will add a macro to extrapolate for data types.

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

[SahithiMV]

@carolynzech Can you please review the changes?

[carolynzech]

Suggested change

	#[kani::proof_for_contract(<$t>::unchecked_add)]
	#[kani::proof_for_contract(<$nonzero_type>::unchecked_add)]

[carolynzech]

Suggested change

	let x: $nonzero_type = kani::any();
	let y: $nonzero_type = kani::any();
	unsafe {
	x.get().unchecked_add(y.get());
	let x: $nonzero_type = kani::any();
	let y: $t = kani::any();
	unsafe {
	x.unchecked_add(y);

See the documentation for unchecked_add -- self (x, in this case) should be a NonZero, and other (y) should be a primitive type. (Calling get on x gets its primitive type, so this harness as of now calls the primitive type's unchecked_add instead of the NonZero version.

[carolynzech]

Hi @SahithiMV,

I did some debugging to figure out why Kani was failing on these new versions of the contracts. Turns out it's a Kani bug. See this issue: model-checking/kani#3773. This happens because of the phenomenon I described in the issue: Kani picks the first implementation that it finds when it resolves the function name inside the proof_for_contract attribute. In the case of your unchecked_add harness, for example, it happens to find the one for u8, so when you actually invoke the unchecked_add macro on u8, everything works fine, but it doesn't work for the other types.

In other words, you can think about it as Kani replacing this:

#[kani::proof_for_contract(NonZero::unchecked_add)]

with this:

#[kani::proof_for_contract(NonZero::<u8>::unchecked_add)]

every time, which of course only makes sense if your harness happens to call unchecked_add on u8s.

So in terms of what this means for you: you should still be able to write the contracts, even if they won't successfully verify because of this issue. So please get your harnesses to a place where they only fail because of this issue. That way, we can merge your contracts unchanged once we fix the issue on our end. (You can tell if it's the same issue by seeing if the error message is the same).

Please let me know if there's anything I can clarify, or if I can help further writing the harnesses.