Challenge 2: Verify safety of raw-pointer intrinsics with Kani

[v3risec]

Summary

This PR adds a Kani-based verification plan for Challenge 2.

The changes are organized into four layers:

• safety contracts for intrinsic wrappers and public APIs;
• a shared implementation proof for the typed_swap_nonoverlapping fallback;
• concrete usage harnesses for standard-library APIs;
• explicit documentation of model limitations, assumptions, and residuals.

The typed_swap_nonoverlapping fallback is extracted into a shared helper so the production path and the verification wrapper execute the same fallback body.

Current Source Mapping

Some names and locations in the challenge table do not match the current source tree:

• <[T]>::copy_from_slice is a safe method in library/core/src/slice/mod.rs; there is no separate std::ptr::copy_from_slice implementation.
• mem::align_of_val is the current implementation. The deprecated min_align_of_val function forwards to it.
• mem::zeroed<T> is implemented in library/core/src/mem/mod.rs.
• MaybeUninit::zeroed is a separate safe constructor in library/core/src/mem/maybe_uninit.rs.
• parse_u64_into is not present in the current source tree, so no proof is claimed for it.
• The current intrinsic symbol is typed_swap_nonoverlapping; the challenge table refers to the corresponding typed swap operation as typed_swap.

Part 1: Intrinsic Coverage

Intrinsic or operation	Current evidence
typed_swap_nonoverlapping	Active safety contract, shared fallback helper, fallback contract harnesses, and independent value-exchange proofs
vtable_size	Wrapper contract and compiler-generated-vtable harnesses
vtable_align	Wrapper contract and compiler-generated-vtable harnesses
copy_nonoverlapping	Wrapper contract, bounded allocation-backed harnesses, and initialization-state oracle
copy	Wrapper contract, distinct-range harnesses, forward/backward overlap harnesses, and initialization-state oracle
write_bytes	Wrapper contract, bounded writable-range harnesses, complete requested scalar/type coverage, and a dedicated ZST harness
size_of_val	Sized, slice, and dyn Debug wrapper harnesses using checked raw-layout predicates
arith_offset	Wrapper postconditions for wrapping pointer arithmetic
volatile_load	Allocation-backed contract and representative non-ZST harnesses
volatile_store	Allocation-backed contract and representative harnesses
compare_bytes	Readability contract and bounded harness
ptr_offset_from	Shared signed precondition predicate, two-allocation contract harnesses, and predicate-only negative-path audits
ptr_offset_from_unsigned	Independent unsigned predicate, reverse-order audit, and bounded contract harnesses
read_via_copy	Readability contract and representative harnesses
write_via_move	Writability contract and representative harnesses
Five unsupported volatile intrinsics	Not covered with the pinned Kani revision: volatile_copy_memory, volatile_copy_nonoverlapping_memory, volatile_set_memory, unaligned_volatile_load, and unaligned_volatile_store

Because Kani cannot currently attach contracts directly to several body-less intrinsic declarations (Kani rust-lang#3325), the copy, layout, arithmetic, volatile, comparison, read, and write proofs use ordinary wrapper functions. These wrappers provide verification evidence but should not be described as declaration-level production contracts.

Pending volatile intrinsic coverage

The following five intrinsic targets are not covered by this change:

• volatile_copy_nonoverlapping_memory
• volatile_copy_memory
• volatile_set_memory
• unaligned_volatile_load
• unaligned_volatile_store

This is a limitation of the Kani version currently pinned by verify-rust-std, rather than a remaining limitation of upstream Kani. The repository pins Kani commit d4df833c8f8f18e632e7b0a7945bb2161f708990 from January 18, 2026.

Upstream support for these intrinsics has since been implemented and merged:

• model-checking/kani#4672, merged August 1, 2026, added support for volatile_copy_memory, volatile_copy_nonoverlapping_memory, and volatile_set_memory.
• model-checking/kani#4673, merged August 2, 2026, added support for unaligned_volatile_load and unaligned_volatile_store.

Once verify-rust-std updates its pinned Kani revision to include these changes, contracts and proof harnesses for the five remaining targets can be added and verified using the same approach as the intrinsics covered here.

Part 2: Standard-Library Usage

API	Current evidence
<[T]>::copy_from_slice	Safe usage harnesses with equal-length slices, bounded lengths, and a non-empty reachability cover. The current harness does not independently assert element-value preservation.
mem::swap	Plain usage proofs with pre-state snapshots and value-exchange assertions across the representative type matrix
mem::align_of_val	Sized and slice usage proofs comparing the result with align_of::<T>()
MaybeUninit::zeroed	Byte-level proofs that inspect initialized bytes without constructing an invalid T
parse_u64_into	Not present in the current source tree; no usage proof is claimed

Part 3: Public APIs Exposing Intrinsics

API	Current evidence
ptr::swap	Safety contract and contract harnesses for integer, scalar, array, validity-sensitive, and ZST types
ptr::write_bytes	Safety contract, bounded writable-range harnesses, scalar/type coverage, and a separate ZST allocation workaround
mem::align_of_val_raw	Metadata-validity contract with sized, slice, and dyn Debug harnesses
mem::zeroed	Safety contract with zero-valid scalar, array, and unit instantiations; the unit instance currently fails in Kani's ZST memset model and is not claimed as successfully verified

Model Correspondence

• copy and copy_nonoverlapping are modeled at byte level. The oracle checks preservation of initialization state, including the corresponding source and destination element offsets. It is not a universal byte-value oracle for arbitrary T.
• write_bytes is modeled as a writable byte-range operation. The current harnesses check contract reachability and memory conditions, but do not independently assert the resulting fill byte.
• vtable_size, vtable_align, size_of_val, and align_of_val_raw use compiler-generated metadata and Kani's checked raw-layout predicates. This establishes consistency for the instantiated types, not a complete proof of every rustc layout.
• arith_offset is checked against wrapping pointer arithmetic postconditions.
• Pointer-offset wrappers share the same pure predicates used by the audit harnesses. Invalid candidates are checked without calling the unsafe intrinsic.
• volatile_load and volatile_store currently model ordinary Rust-allocation-backed memory only.
• compare_bytes, read_via_copy, write_via_move, and the volatile wrappers currently establish memory-safety conditions, not complete independent value semantics.

Harness Audit

• Generic proofs use concrete monomorphizations.
• Symbolic lengths, counts, and indices are bounded by fixed backing arrays.
• The fallback value proofs cover signed and unsigned integer widths, isize/usize, floating-point values, bool, char, arrays, NonZeroI32, and unit.
• align_of_val_raw covers the full sized scalar matrix, u8 through u128 slices, and representative dyn Debug values.
• The pointer-offset audit covers cross-allocation candidates, non-element byte distances, unsigned reverse order, and valid same-allocation distances. Same-address/different-provenance is not separately audited.
• The ptr::write_bytes::<()> harness uses a real byte allocation because Kani cannot represent a writable zero-sized memset destination. This is a harness-only workaround and does not change production code.

Verification

All added Challenge 2 harnesses pass locally with Kani.

Resolves #16

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

[feliperodri]

Thanks @v3risec — this is a solid, sound submission. It's clean on our vacuity checks (no cfg(kani) body swaps, no decorative contracts — every contracted fn has a matching proof_for_contract, no assume-the-conclusion), inputs are symbolic, and it even fixes a real bug in the base check_copy_untyped oracle (comparing src[0] vs the corresponding src.add(elem) byte, with a ZST guard). The shared typed_swap_nonoverlapping_fallback helper to keep production and verification bodies from drifting is a nice touch.

Where it fell short of closing Challenge 2 — it's incomplete relative to the criteria:

• Group A: ~15 of 21 intrinsics. The 5 volatile/unaligned-volatile intrinsics (volatile_copy_memory, volatile_copy_nonoverlapping_memory, volatile_set_memory, unaligned_volatile_load, unaligned_volatile_store) have no wrapper/harness.
• Group B: 4 of 5 (parse_u64_into — absent from the current tree, understood).
• Group C: 3 of 5 literal std::ptr/wrapper functions (copy_from_slice/parse_u64_into not covered as wrappers).

For transparency: we reviewed all three open Challenge 2 solutions together and are prioritizing #649 in the review process, which covers all 21 intrinsics + 5/5 usages + 5/5 wrappers. Your bug fix and the fallback-sharing pattern are genuinely valuable — worth surfacing to that PR/upstream regardless. One thing to watch: adding #[safety::requires] to widely-used ptr::swap/ptr::write_bytes/mem::zeroed/align_of_val_raw turns those into proof obligations at every in-repo call site and can surface unrelated CI failures.