Challenge 2: memory safety of raw-pointer intrinsics

[stefanzetzsche]

Towards #16. Solves Challenge 2: Verify the memory safety of core intrinsics using raw pointers: safety contracts and Kani harnesses for the raw-pointer intrinsics (Part 1), proofs that the std library's uses of them are safe (Part 2), and contracts on the raw-pointer functions exposing them (Part 3). All 146 harnesses added by this PR pass in a single kani verify-std invocation at the pinned Kani commit.

Changes

File	Change
intrinsics/mod.rs	Contracts + proof_for_contract harnesses for 20 intrinsics, via thin wrappers (Kani cannot attach contracts to body-less #[rustc_intrinsic]s, model-checking/kani#3325; same pattern as the in-tree transmute_unchecked_wrapper); also fixes the pre-existing check_copy_untyped spec helper, which compared src[0]'s initialization state against dst[elem]'s instead of src[elem]'s
mem/mod.rs	Usage proofs for swap and align_of_val; contract + harnesses for align_of_val_raw (Part 3)
mem/maybe_uninit.rs	Usage proof for zeroed (reaches write_bytes), byte-level ensures
fmt/num.rs	Contract + harnesses for u64::_fmt, the successor of the challenge-listed parse_u64_into (Part 2)
ptr/mod.rs	Contracts + harnesses for ptr::swap and ptr::write_bytes (Part 3)
slice/mod.rs	Contract + harnesses for copy_from_slice (Parts 2/3)

Part 1: the intrinsics

All 21 listed intrinsics are contracted and verified: 20 by this PR, and the 21st, typed_swap, already carries a verified in-tree contract with passing harnesses (added by #37, before this challenge was tackled), so re-verifying it here would only duplicate upstream code. This PR still exercises that existing contract as part of the mem::swap usage proof (Part 2). Two findings for the committee: parse_u64_into no longer exists anywhere in the tree, and five intrinsics (volatile_copy_memory, volatile_copy_nonoverlapping_memory, volatile_set_memory, unaligned_volatile_load, unaligned_volatile_store) are reported unsupported by Kani and have no fallback body. For those five, the contract is verified on a *_model function whose body is the non-volatile equivalent: the two forms differ only in LLVM's volatile flag, an optimization barrier with no effect on the abstract memory state CBMC reasons about, and the docs state their safety requirements match the non-volatile counterparts. model-checking/kani#4672 and model-checking/kani#4673 (merged 2026-08-01/02, after the January pin) add support for these five; once the pin bumps past them, the models should be swapped for the real intrinsics.

Contracts state exactly the documented # Safety conditions. Where the documented condition is per-case, so is the contract: size_of_val/align_of_val get a Sized wrapper with no precondition (documented "always safe", proven with dangling pointers) and a slice wrapper requiring only that the total size fits isize. All remaining intrinsics are Kani-modeled; each harness pins the model with a concrete assertion (e.g. vtable_size returns exactly size_of::<T>(), store harnesses read the value back).

Intrinsics	Approach
copy, copy_nonoverlapping, write_bytes, volatile/unaligned family	Readable/writable-range + alignment + (where documented) non-overlap requires; untyped-copy ensures; byte-granular pointer offsets so misaligned inputs are generated, not avoided
vtable_size, vtable_align, size_of_val, align_of_val	Metadata-only models; generic ensures (size fits isize, alignment is a power of two); per-type fidelity asserts in harnesses; the layout queries cover all three documented cases (Sized, slice tail, trait-object tail via real compiler-produced vtables)
ptr_offset_from, ptr_offset_from_unsigned, arith_offset	Same-allocation / ordering requires; arith_offset checked over a mid-range address window (CBMC does not model the address-space edges)
compare_bytes	Whole-range readability requires (docs stress chunked reads); checked instances bounded to 8 bytes (unwind(9)) — the bound lives in the harness, not the contract
read_via_copy, write_via_move	Read/write validity; write_via_move ensures dereferenceability post-state (the moved value cannot be re-read for generic T)

For the trait-object case, Kani has no "is a vtable" predicate, so (as for vtable_size/vtable_align) dereferenceability of the three metadata words is the stated approximation of the documented condition; the harnesses supply real compiler-produced vtables, so the precondition is discharged non-vacuously.

Part 2: std usage sites

Usage site	Proof
mem::swap	proof_for_contract(swap) + stub_verified(typed_swap_nonoverlapping), so the intrinsic's requires become explicit call-site obligations
<[T]>::copy_from_slice	Contract on the function; symbolic lengths 0..=32 across 5 element types, element equality asserted per type
mem::align_of_val	8 harnesses (Sized + slice tails); the precondition holds structurally for &T
MaybeUninit::zeroed	10 harnesses: the reached write_bytes is safe and all backing bytes are 0
fmt::parse_u64_into	Does not exist in the tree (finding above); its successor u64::_fmt is contracted and verified instead — the documented buffer-size safety condition as requires, digits-only/length ensures, plus a bounded value-fidelity harness. The contract lives on a #[cfg(kani)] wrapper because _fmt is macro-generated for every integer type; annotating it directly would touch them all

Part 3: raw-pointer functions

Contracts + harnesses for ptr::swap (overlap-permitted path exercised), ptr::write_bytes, and mem::align_of_val_raw (including dangling-pointer harnesses for the documented always-safe Sized case). copy_from_slice doubles as its own Part 3 item.

Wherever a harness restricts inputs with kani::assume, a kani::cover check confirms some input satisfies the restriction, so no proof passes vacuously; value-level properties that cannot be generic ensures clauses (no PartialEq bound) are asserted per concrete type.

Relation to other work on this challenge

#37 (merged) contributed the typed_swap contract this PR builds on and exercises via the mem::swap usage proof.

#618 is an open partial solution covering 15 Part 1 intrinsics. This PR was developed independently and additionally covers the five Kani-unsupported intrinsics (via the models above), Part 2, and Part 3. Its review thread shaped two of this PR's contracts (per-case preconditions instead of a blanket can_dereference), and its author's now-merged Kani fixes (model-checking/kani#4672, model-checking/kani#4673) are what will let the five models be replaced with real-intrinsic proofs once the pin bumps past them.

#643 is another open full-table attempt, developed independently on the same wrapper pattern; this PR adopts its correct fix to the pre-existing check_copy_untyped spec helper (src_data was never offset by the chosen element), with all affected harnesses re-verified. Beyond that, this PR goes further on three fronts:

• Adversarial inputs. Copy-family harnesses here generate byte-granular pointer offsets across several element types, so misaligned and overlapping inputs are produced by the solver rather than avoided; Challenge 2: Kani contracts for raw-pointer core::intrinsics #643's are u8-only (alignment trivially 1) with a single fixed overlap shift, so its alignment precondition is never non-trivially exercised.
• Part 2 depth. Both PRs touch all five usage sites; this PR proves each more deeply: 10 byte-level zeroed harnesses (Challenge 2: Kani contracts for raw-pointer core::intrinsics #643 has 2, integer-only), copy_from_slice at symbolic lengths 0..=32 across 5 element types (Challenge 2: Kani contracts for raw-pointer core::intrinsics #643: one u8 harness at fixed length 4), and a mem::swap proof that stub_verifieds the intrinsic contract so its requires become explicit call-site obligations (Challenge 2: Kani contracts for raw-pointer core::intrinsics #643 asserts value exchange only).
• Part 3 coverage. This PR contracts and verifies the exposing functions — ptr::swap (overlap-permitted path), ptr::write_bytes, mem::align_of_val_raw — as the challenge asks; in Challenge 2: Kani contracts for raw-pointer core::intrinsics #643 this part is essentially absent (plain fixed-size harnesses without contracts, align_of_val_raw not covered).

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