Contracts & Harnesses for byte_add, byte_offset, and byte_offset_from

[danielhumanmod]

Description:

This PR introduces function contracts and proof harness for the NonNull pointer in the Rust core library. Specifically, it verifies three new APIs—byte_offset, byte_add, and byte_offset_from with Kani. These changes enhance the functionality of pointer arithmetic and verification for NonNull pointers.

Changes Overview:

Covered APIs:

1. NonNull::byte_add: Adds a specified byte offset to a pointer.
2. NonNull::byte_offset: Allows calculating an offset from a pointer in bytes.
3. NonNull::byte_offset_from: Calculates the distance between two pointers in bytes.

Proof harness:

1. non_null_byte_add_proof
2. non_null_byte_offset_proof
3. non_null_byte_offset_from_proof

Towards #53

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

[danielhumanmod]

Thanks for your suggestion @zhassan-aws! I've updated the code in the latest commit based on your comments. I’d appreciate it if you could take a look when you have a chance.

[danielhumanmod]

Hi @zhassan-aws , thanks for the review and suggestions. I have updated the code based on the comments, fix the unnecessary assume proof harness, using addr, and add unchecked_add to avoid overflow, appreciate if any further suggestion!

[zhassan-aws]

Nice. Thanks!

[celinval]

Please replace kani::requires and kani::ensures by safety::requires and safety::ensures. Thanks!

[celinval]

Looks good. Can you please add harnesses for the dangling pointers cases?

[feliperodri]

@danielhumanmod could you resolve the conflicts?

[danielhumanmod]

@danielhumanmod could you resolve the conflicts?

Hi @feliperodri , I have solved the conflicts in latest commit, thanks for reminding that

[danielhumanmod]

Thanks for the clarification @zhassan-aws ! I have updated the code based on the comments, appreciate any further or review that might need @zhassan-aws @celinval

[zhassan-aws]

Thanks!