Contracts and harnesses for dangling, from_raw_parts, slice_from_raw_parts, to_raw_parts in NonNull

[QinyuanWu]

Towards #53

Contracts and harnesses for dangling, from_raw_parts, slice_from_raw_parts, to_raw_parts in NonNull

Discussion

1. NonNull::slice_from_raw_parts: requested new Kani API to compare byte by byte
2. NonNull::to_raw_parts: unstable vtable comparison 'Eq'

Verification Result

SUMMARY:
** 0 of 141 failed
VERIFICATION:- SUCCESSFUL
Verification Time: 0.17378491s
Complete - 6 successfully verified harnesses, 0 failures, 6 total.

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

[QinyuanWu]

@zhassan-aws I just starting to get compiler errors when I run kani on this branch:

Kani Rust Verifier 0.56.0 (standalone)
error: cannot find a built-in macro with name `SmartPointer`
--> /Users/owo/Desktop/verify-rust-std/library/core/src/marker.rs:1068:1
|
1068 | / pub macro SmartPointer($item:item) {
1069 | | /* compiler built-in */
1070 | | }
| |_^
error: attributes starting with `rustc` are reserved for use by the `rustc` compiler
--> /Users/owo/Desktop/verify-rust-std/library/core/src/marker.rs:1095:12
|
1095 | impl<#[rustc_runtime] const RUNTIME: bool> Compat<RUNT...
| ^^^^^^^^^^^^^
......

I just pulled the latest kani changes and re-built it but the error persists. Latest kani git log:

commit abd68b963c6e4a9508ce9f6950f3d26134631eba
Author: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Date: Mon Nov 11 17:13:34 2024 -0600
Bump tests/perf/s2n-quic from `65d55a4` to `cb41b35` (#3706)
Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`65d55a4` to `cb41b35`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/cb41b35a9bc0412435b70b5038df0681a881e414"><code>cb41b35</code></a>
feat(s2n-quic-dc): mtu probing event subscriber (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2374">#2374</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/56ce95a48db7dd2ed31110d9d408775793bbcb3a"><code>56ce95a</code></a>
test(s2n-quic-core): add metric snapshot registry (<a

@danielhumanmode also reproduced this error on his local environment and found that Kani compiled the code successfully on commit 13e6695(before the latest merge from main).

[carolynzech]

@zhassan-aws I just starting to get compiler errors when I run kani on this branch:
I just pulled the latest kani changes and re-built it but the error persists. Latest kani git log:

commit abd68b963c6e4a9508ce9f6950f3d26134631eba
Author: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Date: Mon Nov 11 17:13:34 2024 -0600
Bump tests/perf/s2n-quic from `65d55a4` to `cb41b35` (#3706)
Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`65d55a4` to `cb41b35`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/cb41b35a9bc0412435b70b5038df0681a881e414"><code>cb41b35</code></a>
feat(s2n-quic-dc): mtu probing event subscriber (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2374">#2374</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/56ce95a48db7dd2ed31110d9d408775793bbcb3a"><code>56ce95a</code></a>
test(s2n-quic-core): add metric snapshot registry (<a

@danielhumanmode also reproduced this error on his local environment and found that Kani compiled the code successfully on commit 13e6695(before the latest merge from main).

@QinyuanWu Is there a reason why you're running on Kani's main branch instead of the features/verify-rust-std branch? If not, please try running Kani from the features/verify-rust-std branch instead.

[QinyuanWu]

eatures/verify-rust-std br

@carolynzech This resolved the compiler errors in PR #105 but not this one ;-;
@zhassan-aws I tried running ./scripts/run-kani.sh but the cbmc-viewer error still persists:

For the script, I pulled the latest changes from main and it seems like cbmc-viewer is still being installed/upgraded:
==> Upgrading aws/tap/cbmc-viewer
3.9 -> 3.10 Error: Your Command Line Tools are too outdated.
Update them from Software Update in System Settings.

[zhassan-aws]

Did you merge the latest commits (including at least 6aa2661)?

[zhassan-aws]

If you have the up-to-date changes, these should be the contents of tool_config/kani-version.toml:

$ cat tool_config/kani-version.toml # This version should be updated whenever there is a change that makes this version of kani# incompatible with the verify-std repo.
[kani]
commit = "26c078e097025499baf6e360210a21989d3605e0"

[QinyuanWu]

@zhassan-aws Thank you the compiler issue is resolved after running the script and executing kani from /verify-rust-std/kani_build/scripts/kani. I then tried the kani I built before(/kani/scripts/kani) and it surprisingly worked again. Not sure what happened lol(maybe because some commits from main were not merged in?). Previous comments are addressed.

[qinheping]

LGTM.

[zhassan-aws]

Almost there. Can you also resolve the conflict?

[QinyuanWu]

@zhassan-aws Resolved comments and conflicts:

SUMMARY:
** 0 of 141 failed
VERIFICATION:- SUCCESSFUL
Verification Time: 0.17723987s
Complete - 24 successfully verified harnesses, 0 failures, 24 total.

[zhassan-aws]

Please re-resolve the conflicts, and I'll merge it.

[QinyuanWu]

@zhassan-aws Resolved conflicts. Thank you so much!

SUMMARY:
** 0 of 141 failed
VERIFICATION:- SUCCESSFUL
Verification Time: 0.17861353s
Complete - 28 successfully verified harnesses, 0 failures, 28 total.