Contracts and Harnesses for <*mut T>::add, sub and offset

[stogaru]

Towards #76

Changes

• Adds contracts for <*mut T>::add, <*mut T>::sub and <*mut T>::offset
• Adds proofs for contracts of the above functions verifying the pointee types:
  • All integer types
  • Tuples (composite type)
  • Unit Type
• Defines a macro for add and sub and another for offset.

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

[xsxszab]

@zhassan-aws Hi the proofs have been updated to use pointer generator, however after the update we encountered a strange test failure, probably a bug: the test case check_mut_add_u8 constantly fails with the following output:

SUMMARY:
 ** 1 of 293 failed (4 unreachable)
Failed Checks: Only a single top-level call to function _RNCNCNvMNtNtCs1YNGORL5zck_4core3ptr7mut_ptrOh3adds0_0s_0Ba_ when checking contract _RNCNCNvMNtNtCs1YNGORL5zck_4core3ptr7mut_ptrOh3adds0_0s_0Ba_
 File: "/Users/xsxsz/vscode-projects/verify-rust-std/library/core/src/ptr/mut_ptr.rs", line 1019, in _RNCNCNvMNtNtCs1YNGORL5zck_4core3ptr7mut_ptrOh3adds0_0s_0Ba_

VERIFICATION:- FAILED
Verification Time: 0.45757997s

All other proofs generated by the same macro work fine. Is there any possible cause for this problem? For now, we have to skip this test case by commenting it out.

Update: The const counterpart check_const_add_u8 in another PR (#166) works fine. This information might help locate the issue

[zhassan-aws]

@celinval encountered the same issue in #37 (comment). @celinval were you able to figure out what is causing the error and whether there's a workaround?

[celinval]

Yes, the problem is that the pointer generator code is likely using the API you are trying to verify. For the harness that is failing, you won't be able to use the generator as is today. Sorry!

[zhassan-aws]

Thanks