Add a few intrinsics contracts

[celinval]

Here are a few limitations:

1. Harness forwrite_bytes was disabled due to:
   • Issue Spurious failure when calling vec! with a size of zero kani#90.
2. The harnesses explicitly disable cases where a pointer is dangling.
   • Kani cannot make assumptions on pointer allocation for dead or dangling pointers (Add support for non-deterministic pointer kani#2300).
3. Actual intrinsics are very hard to verify with Kani. The cases we can verify are those that have wrappers around the actual intrinsic.
   • Issue Add contract support to intrinsics kani#3345

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

[rahulku]

is this waiting for something?

[celinval]

Yes, I need to update the branch and tests.

[celinval]

FYI, this is blocked until we merge the PointerGenerator into Kani: model-checking/kani#3538

[celinval]

Just an update. I haven't been able to figure out yet why the copy_nonoverlapping harness is failing yet. The error is:

Checking harness intrinsics::verify::check_copy_nonoverlapping...

VERIFICATION RESULT:
 ** 1 of 856 failed (3 unreachable)
Failed Checks: Only a single top-level call to function _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_ when checking contract _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_
2024-11-02T01:43:52.2508870Z  File: "/Users/runner/work/verify-rust-std/verify-rust-std/head/library/core/src/intrinsics.rs", line 3311, in _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_

VERIFICATION:- FAILED

which doesn't make sense to me. The harness structure is exactly the same as copy, and so is the function implementation. 🤷‍♀️

[qinheping]

LGTM, thank you!

[tautschnig]

Just an update. I haven't been able to figure out yet why the copy_nonoverlapping harness is failing yet. The error is:

Checking harness intrinsics::verify::check_copy_nonoverlapping...

VERIFICATION RESULT:
 ** 1 of 856 failed (3 unreachable)
Failed Checks: Only a single top-level call to function _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_ when checking contract _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_
2024-11-02T01:43:52.2508870Z  File: "/Users/runner/work/verify-rust-std/verify-rust-std/head/library/core/src/intrinsics.rs", line 3311, in _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_

VERIFICATION:- FAILED

which doesn't make sense to me. The harness structure is exactly the same as copy, and so is the function implementation. 🤷‍♀️

I have seen the very same problem on #120, and I haven't yet managed to understand why.

[tautschnig]

Here are a few problems that I bumped into: [...]

Before merning, would you mind adding to the PR description also what actually does work?

[celinval]

@tautschnig can you please see my answer to your comments? Is it OK if I move ahead and merge these changes?

[celinval]

I need to solve the new conflicts. After that, I'll merge this PR

[celinval]

I updated this PR to account to the fact that the intrinsics.rs file was moved to intrinsics/mod.rs. I have also disabled the write_bytes harness because of model-checking/kani#90.

@tautschnig can you please take a look and see if this is good to go?