Challenge 2 (partial): safety contracts + verification for 15 of 20 raw-pointer core::intrinsics

[ivmat]

Challenge 2 (partial): safety contracts and verification for 15 of 20 raw-pointer core::intrinsics

Tracking issue: #16. This PR does not close that issue.
Scope: 14 safety contracts checked by #[kani::proof_for_contract] at bounded finite instantiations,
plus arith_offset's unbounded no-UB proof. No generic theorem over all types and sizes is claimed.
Contracts use forwarding wrappers because kani#3325 blocks contracts on bodyless intrinsics (kani#3345).

Covered: typed_swap (typed_swap_nonoverlapping) · vtable_size · vtable_align · copy · copy_nonoverlapping ·
write_bytes · size_of_val · arith_offset · volatile_load · volatile_store · ptr_offset_from ·
ptr_offset_from_unsigned · compare_bytes · read_via_copy · write_via_move. Not covered: the five volatile
intrinsics under Residuals.

Response to the 2026-08-16 review

Blocking items, in review order:

1. vtable_size_coerced_wrapper / vtable_align_coerced_wrapper: unsize *const T and compare with size_of::<T>() / align_of::<T>().
   Checked at seven types through Debug, relative to compiler layout; raw *const () probes are excluded from the count.
2. size_of_val_wrapper: no #[requires] for sized pointers; separate dyn and symbolic-length slice wrappers.
   Slices require only size * len <= isize::MAX; composite unsized tails and extern type remain residuals.
3. compare_bytes_wrapper: requires only both regions readable for bytes. COMPARE_BYTES_CAP is a harness assume;
   covers witness non-zero length and the exact cap boundary.
4. volatile_load_wrapper / volatile_store_wrapper: scope is Rust-allocation-backed memory only.
   Documented aligned, non-trapping external-memory/MMIO access remains unverified.
5. arith_offset_bounded_probe / check_arith_offset_bounded_probe: excluded from the contract count.
   Safety rests on check_arith_offset_unconditional_safety, with a fully symbolic isize offset.

Non-blocking items:

• check_copy_untyped: pairs src.add(elem) with dst.add(elem); copy_wrapper captures the source using old(...).
  check_copy_wrapper_overlapping_nonuniform_contract checks the pre-state oracle on an overlapping non-uniform fixture.
• Pointer-distance preconditions: check_ptr_offset_from_u32_wrapper_contract, check_ptr_offset_from_unsigned_u32_wrapper_contract, and
  check_ptr_offset_u32_fixture_partitions exercise same/cross-allocation, forward/reverse order, and divisible/non-divisible distances; controls below.
• Fallback duplication: typed_swap_nonoverlapping_fallback is shared by the production fallback and verification wrapper.

Evidence

Targeted/module runs: c35c201b46a8be04daaef874defa438c8a5e945c; the later
cf5fd23c45cb38273a314d6229a9b214a16ebf3c changes comments only. Repository-suite run: cf5fd23c.

Tool / setting	Value
Kani	d4df833c8f8f18e632e7b0a7945bb2161f708990 (tool_config/kani-version.toml)
CBMC	6.8.0
rustc	1.93.0-nightly (c871d09 2025-11-24), nightly-2025-11-25
Flags	-Z unstable-options, -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing, --cbmc-args --object-bits 12

Run	Result
Targeted, both dependency-contract modes	55/55; every declared kani::cover satisfied in both modes
intrinsics::verify, CI mode (--no-assert-contracts)	374/374, 0 failures, exit 0
intrinsics::verify, dependency contracts asserted	372/374, 2 failures, exit 1
Repository suite, four Linux shards, cf5fd23c, --no-assert-contracts	1436 harnesses, 359 per shard, 0 failures

The asserting-mode failures, check_transmute_slice_metadata and check_transmute_unchecked_slice_metadata,
stop at --object-bits 12: “too many addressed objects” (4096 objects), CBMC status 6, not a property violation.
The stop reproduces on the untouched base for check_transmute_slice_metadata and on the prior PR head for both;
the base _unchecked run timed out without a verdict. This revision does not introduce the capacity stop.
A larger object budget is untested.

All five added/renamed harnesses named in the review response appear in kani list, used for sharding.
macOS was not run outside CI. The PR's CI run remains authoritative; no CI outcome is claimed here.

Controls

Control	Change	Observed
Copy implementation	copy_wrapper call replaced by write_bytes(dst, 0, count)	Only the ensures postcondition fails, both modes
Copy readable-source precondition	Conjunct deleted	Memory-safety failures including pre-state source read, both modes
Copy writable-destination precondition	Conjunct deleted	Destination write, modifies validity, and postcondition destination read fail, both modes
Copy count-size overflow precondition	Conjunct deleted	Survived. Subsumed by other conjuncts in this fixture; independence unestablished
Pointer-distance preconditions (five)	Same-allocation, divisibility, unsigned-ordering conjuncts individually ablated across signed/unsigned u32 wrappers	Each fails its named Kani model check, both modes
mem::swap drop detector	Harness epilogue's forget replaced by drop	Fixture's Drop panic; tests the detector, not the implementation

Reversing each ablation restores success. The two copy memory-precondition ablations also hit an unsupported
same_allocation check and leave checks undetermined; only their separate memory-safety failures count as evidence.

Criterion by criterion

#	Criterion	Scope / gap
1	Safety contracts for all listed intrinsics	15/20: 14 contract-form, plus arith_offset safety proof. Not satisfied for all 20.
2	Verify fallback implementations	The sole fallback, typed_swap_nonoverlapping, shares the helper symbolically executed through a wrapper. Equivalence to Kani's built-in model is not shown.
3	Explain model/definition correspondence	Value/pointer results use independently computed expectations; vtable correspondence is documented in source. Connection to bodyless intrinsic backend codegen remains open.
4	State assumptions and guarantees	Finite scope and assumptions below.
5	Documented conditions suffice for safety	Documented requires; caps in harnesses. Carve-outs: volatile MMIO is unverified; arith_offset uses the no-UB proof. Open for the five tool-blocked intrinsics.

Assumptions and bounds

• CI mode assumes dependency contracts (--no-assert-contracts); asserting-mode results are listed separately above.
• Copy byte-value postcondition: initialized T = u32, N = 4, SHIFT = 1, COUNT = 3, four distinct non-zero words;
  every element in 0..3 and byte in 0..4. No generic T or count result.
• check_copy: T = char, two PointerGenerator<100> allocations, symbolic pointers/count;
  Dangling and DeadObject excluded by assumption.
• -Z uninit-checks is off; can_dereference's initialization conjunct is inert. Copy checks are model-relative byte-value checks,
  with no Rust-semantic initialization claim or mixed-initialization relation.
• The overlap cover's overlap conjunct is constant; only its two value conjuncts are witnessed. No pointer-derived overlap predicate.
• check_copy_overlapping_shift_no_ub: SHIFT = 1, COUNT = 3, symbolic index; no exhaustive overlap sweep.
• Pointer distance: u8, one 8-byte allocation (divisibility unexercised); u32, two 16-byte allocations, offsets 0..16; no generic T result.
• mem::swap: T = u8 and a panic-on-Drop ADT; only kani::modifies(x) / modifies(y), no requires or ensures.
  No value exchange proved; the ADT fixture witnesses no operand drop.
• Small concrete fixtures, symbolic contents; compare_bytes cap 4, unwind 5, cap assumed in harness.
• Vtables: seven erased types, only Debug; expected/result share compiler layout. Includes [u8; 8], zero-sized, mixed-alignment, over-aligned types.
• size_of_val: sized u32 (null, dangling, non-deterministic-address, real pointers), four dyn erased types, four slice element types.
• arith_offset_bounded_probe: 0..=8; its unbounded safety proof is separate.
• --object-bits 12 fails loudly on overflow; no silent cap.
• No Challenge-2 harness uses kani::stub or stub_verified, or compiles out a shipped body; -Z stubbing serves pre-existing transmute harnesses.
• Only the copy family has an implementation mutation. No control mutates Kani codegen; lowering defects are not excluded.

Residuals

Five intrinsics are unsupported at the pin: volatile_copy_memory, volatile_copy_nonoverlapping_memory,
volatile_set_memory, unaligned_volatile_load, unaligned_volatile_store. Their harnesses remain under #[cfg(not(kani))].
Fixes are merged in kani#4672 (first three) and kani#4673 (last two), but the repository still pins d4df833: 15/20 remains.
A stand-in would omit volatile semantics and bypass codegen; kani#4672's investigation found (dst, src) reversed in the sketched volatile_copy_memory implementation.

Other open items:

• Copy mixed initialization and count-size overflow precondition independence.
• Wrapper-contract correspondence to backend codegen.
• Value-exchange oracles and implementation mutants for mem::swap / typed_swap;
  implementation mutants for volatile, vtable, size_of_val, and compare_bytes oracles.
• size_of_val: composite unsized tails and extern type metadata; volatile external memory/MMIO.
• Vtables: traits other than Debug, and final emitted vtables independently of compiler layout.
• Asserting-mode transmute failures at the object budget; larger budget untested.
• kani#90 remains open; its specific trigger is witnessed reachable here.
• macOS verification at this commit.

Usage and exposing tables

The challenge's five usage sites and five exposing functions are separate from the 15/20 count.

Row	Status here
[T]::copy_from_slice	Bounded real-caller proof exists elsewhere, not integrated; residual.
core::mem::swap	Two production-function contract harnesses; no value-exchange proof, row not counted.
core::mem::align_of_val	Bounded sized-u32 real-caller probe; documented T: ?Sized domain remains residual.
MaybeUninit::zeroed	Bounded u32 real-body probe exists elsewhere, not integrated; residual.
parse_u64_into	Absent; maintainer note below.
Five std::ptr::* exposing rows	Only std::ptr::swap resolves; all five residual pending intended targets.

Claim ledger

A machine-checkable manifest of the claims above — one entry per intrinsic with its harnesses, bounds,
assumptions, and an assurance band that says whether the claim's oracle was ever watched to fail — is at
https://github.com/ivmat/acceptance-format/tree/main/examples/verify-rust-std-pr618 (revision 2, for
cf5fd23c). Why it is there: this description states scope in prose; the manifest states the same
scope per claim in a fixed shape a reader can audit line by line and re-validate with the checker in
that repository, including the claims that have no control (all 15 per-intrinsic claims sit at the lowest band for
that reason; the one claim above it is the copy_wrapper byte-value oracle, which carries the observed-red
implementation mutation listed under Controls). It is hand-authored, is not part of this PR, and implies nothing about
acceptance.

Notes for the maintainers

parse_u64_into: removed by 26d30a058104fe049a8b1d6d10d18ddf8c04864a (nightly-2025-06-17 subtree update).
The current formatting path is not a one-to-one rename; the usage row needs an agreed disposition.

std::ptr targets: copy_from_slice, parse_u64_into, align_of_val, and zeroed do not resolve there.
Please clarify intended targets: MaybeUninit::zeroed and mem::zeroed, for example, have different safety boundaries.
No proof is transferred from another row.

The removed write_bytes kani#90 FIXME can be restored if preferred until upstream closure;
its guarded configuration verifies here with a cover witnessing the trigger.

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

[Copilot]

Pull request overview

Adds partial Kani verification for Challenge 2, targeting 15 raw-pointer intrinsics while preserving five unsupported harnesses.

Changes:

• Adds safety-contract wrappers and Kani proofs.
• Adds independent-oracle and non-vacuity checks.
• Documents unsupported volatile intrinsic residuals.

Suppressed comments (3)

library/core/src/intrinsics/mod.rs:3576

• This postcondition has the same indexing defect in check_copy_untyped: the selected destination element is compared with src[0], not the corresponding src[elem] (lines 2963-2966). Mixed initialized/uninitialized source elements can make a correct copy fail the contract, so the helper must offset both pointers by elem.

    #[ensures(|_| check_copy_untyped(src, dst, count))]

library/core/src/intrinsics/mod.rs:4556

• This excludes the documented MMIO use case: write_volatile permits aligned, non-trapping writes outside Rust allocations, but can_write and the ordinary-dereference postcondition only describe Rust-backed memory. Add a model for external volatile memory or list this as an unverified residual instead of treating this as the complete volatile_store safety contract.

    #[requires(ub_checks::can_write(dst))]
    #[ensures(|_| unsafe { *dst } == val)]

library/core/src/intrinsics/mod.rs:4594

• This contract is false for valid vtables whose erased type is not aligned like u32; a dyn Debug vtable for [u8; 8], for example, meets the readable-memory precondition but reports alignment 1 rather than 4. Readability also does not prove that the pointer is a vtable. Preserve the erased type's expected alignment in the wrapper/fixture and encode genuine vtable validity, or do not count this monomorphic probe as the intrinsic contract.

    #[requires(ub_checks::can_dereference(ptr as *const [usize; 3]))]
    #[ensures(|result| *result == core::mem::align_of::<u32>())]

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Kani-verification review — PR #618 (Challenge 2, partial: 15/20 raw-pointer intrinsics)

Bottom line

The engineering is careful and unusually honest, the wrapper-around-#[rustc_intrinsic] pattern is the right workaround for kani#3325/rust-lang#3345 (already blessed in-tree via transmute_unchecked_wrapper), and the #[cfg(not(kani))] gates are legitimate — not the fatal body-swap pattern. I'm requesting changes only on contract faithfulness / over-constraint grounds against success criterion 5, which several contracts do not meet as written. Nothing here makes an unsafe operation look safe (all deviations are conservative), so this is a fixable faithfulness bar, not a vacuity/soundness collapse.

What is sound (no action needed)

• All 5 #[cfg(not(kani))] gates are legitimate. They sit on disabled #[kani::proof] harnesses for intrinsics Kani reports as unsupported — check_volatile_set_memory_no_ub (618.diff L833), check_volatile_copy_nonoverlapping_memory_no_ub (L851), check_volatile_copy_memory_no_ub (L873), check_unaligned_volatile_load_no_ub (L929), check_unaligned_volatile_store_no_ub (L947). None compiles out a verified std function body behind an assume-the-conclusion stub. This is the same idiom as the pre-existing removed write_bytes gate (L199). No fatal vacuity.
• Contract-liveness is complete: 20 #[kani::proof_for_contract] targets, each paired to a contracted wrapper; the 42 requires / 31 ensures are multi-clause contracts on those 20 functions, so the raw "53 vs 20" is consistent, not decorative.
• typed_swap_fallback_wrapper (L77), copy_wrapper/copy_nonoverlapping_wrapper/write_bytes_wrapper (L112–134) use the correct can_dereference/can_write/maybe_is_nonoverlapping/alignment preconditions — exactly the right contract shape for raw-pointer memory intrinsics.
• Bounded fixtures ([u8;8], [u32;4], COMPARE_BYTES_CAP=4) are acceptable; the challenge does not mandate unbounded, and the added kani::cover non-vacuity witnesses are a nice touch.

Blocking: contracts that don't faithfully capture the documented safety condition (criterion 5)

1. vtable_size_wrapper / vtable_align_wrapper (L550–561). #[ensures(*result == size_of::<u32>())] / align_of::<u32>() is hard-coded to the fixture type; it is false for any non-u32 vtable (e.g. dyn Debug over u64/[u8;8]) that equally satisfies can_dereference(ptr as *const [usize;3]). The precondition also doesn't establish "ptr is actually a vtable." As written this is a monomorphic probe, not the intrinsic's contract. The author's own scoping note concedes this. Either encode the erased type's expected layout generically or don't count these two as verified for the challenge table.

2. size_of_val_wrapper (L486). #[requires(can_dereference(ptr))] is stronger than documented: mem::size_of_val_raw is safe for any T: Sized including null/dangling data pointers, which can_dereference rejects. So "meeting the documented condition is enough" (criterion 5) is not demonstrated — a stronger condition is. Only T = u32 (Sized) is covered; the ?Sized metadata cases are absent.

3. compare_bytes_wrapper (L417). bytes <= COMPARE_BYTES_CAP is a tractability bound placed in #[requires], so the contract rejects valid calls over larger readable regions. Keep the cap as a harness assume only; state the contract purely as "both regions readable for bytes."

4. volatile_load_wrapper / volatile_store_wrapper (L503/L519). can_dereference/can_write + an ordinary-deref postcondition cover only Rust-backed allocations and exclude the documented MMIO case (read/write_volatile permit aligned non-trapping access outside any Rust allocation). Over-constrains valid callers; list the external-memory case as an unverified residual rather than presenting this as the full contract.

5. arith_offset_wrapper (L258). #[requires(offset >= 0 && offset <= 8)] on the contract-form wrapper is not a documented precondition (arith_offset has none). The author's mitigation is real and appreciated — check_arith_offset_unconditional_safety (L280) proves safety unbounded — so the safety property is genuinely covered. But the bounded wrapper should be presented as a behavioral/pointer-model probe, not "the intrinsic contract."

Non-blocking but worth addressing

• check_copy_untyped oracle asymmetry (pre-existing helper, mod.rs:2954, now depended on by copy_wrapper/copy_nonoverlapping_wrapper ensures at diff L109/L119). It offsets dst by elem but leaves src at element 0 (src_data.add(byte) vs dst.add(elem)...add(byte)), so it compares dst[elem]'s init state against src[0]'s. For sources with per-element init differences this oracle is checking the wrong pair. It's not introduced by this PR, but since the PR newly relies on it for the copy/copy_nonoverlapping postconditions, it should be fixed to offset src by elem too (or confirmed harmless for these fixtures).
• ptr_offset_from_wrapper / ptr_offset_from_unsigned_wrapper (L301/L338). The author honestly discloses that dropping the #[requires] "all the way to true still verifies SUCCESSFUL" because the fixture only ever derives both pointers from one [u8;8] array. The contract text is doc-faithful, but the harness does not exercise the precondition (no cross-allocation / reversed-order pointers), so the proof is near-vacuous w.r.t. that precondition. Strengthen the fixture or note it as a known ablation gap in the PR body.
• typed_swap_fallback_wrapper: verifying a verbatim copy of the fallback body (not the shared implementation) satisfies criterion 2's letter but not Kani-entry into typed_swap_nonoverlapping; the author documents this scope limit clearly. Consider extracting a shared helper.

Partial submission

Partial (15/20) is acceptable for this open challenge, and the 5 uncovered intrinsics (the volatile/unaligned-volatile family) are genuinely Kani-unsupported and honestly documented. The blocker is not the missing 5 — it's that several of the claimed 15 have contracts that over-constrain or hard-code fixture specifics and so don't yet satisfy criterion 5 ("meeting the documented conditions is enough to guarantee safe usage"). Tighten items 1–5 (or relabel the affected ones as bounded probes / residuals) and this becomes approvable.

[ivmat]

Implemented the changes and scope relabelling at 9dc6083, and the shared-helper extraction you
suggested at e7b1bc1. CI is green. Walking your numbering:

1. vtable_size / vtable_align hard-coded to u32. Added vtable_size_coerced_wrapper<T: Debug>
and vtable_align_coerced_wrapper<T: Debug>, which take *const T and unsize-coerce inside the
wrapper, so they carry no #[requires] at all.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 4636 to 4834 in e7b1bc1

	// General `vtable_size` and `vtable_align` contracts.
	// Taking `*const T` and unsizing inside the wrapper binds the vtable to `T`.
	// Kani emits its `codegen_vtable`, so callers cannot substitute another type's vtable.
	// The wrapper establishes the documented vtable precondition and needs no `#[requires]`.
	// Residual: rustc's `layout_of` supplies both the vtable constant and `size_of::<T>()`.
	// The proof still checks vtable selection, `Kani::CommonVTable` slot layout, and rustc's value
	// against CBMC's independent `__CPROVER_OBJECT_SIZE` value.
	// It cannot detect `layout_of` disagreeing with the final LLVM vtable.
	// Residual: the wrappers use only `core::fmt::Debug`. Rustc fixes size, align, and drop as the
	// first three slots for every trait, but this does not prove all traits.
	// Keep the raw `*const ()` wrappers above as monomorphic probes of the intrinsic's exact form.
	// Only these typed contracts count as general contracts.
	#[ensures(|result| *result == core::mem::size_of::<T>())]
	#[allow(dead_code)]
	unsafe fn vtable_size_coerced_wrapper<T: core::fmt::Debug>(ptr: *const T) -> usize {
	// The unsize coercion binds the vtable to `T`.
	let dyn_ptr: *const dyn core::fmt::Debug = ptr;
	let vtable_ptr = vtable_ptr_of(crate::ptr::metadata(dyn_ptr));
	unsafe { vtable_size(vtable_ptr) }
	}
	#[ensures(|result| *result == core::mem::align_of::<T>())]
	#[allow(dead_code)]
	unsafe fn vtable_align_coerced_wrapper<T: core::fmt::Debug>(ptr: *const T) -> usize {
	// The unsize coercion binds the vtable to `T`.
	let dyn_ptr: *const dyn core::fmt::Debug = ptr;
	let vtable_ptr = vtable_ptr_of(crate::ptr::metadata(dyn_ptr));
	unsafe { vtable_align(vtable_ptr) }
	}
	// Trivial `Debug` impls avoid unused formatting code in the vtables.
	struct VtableZst;
	impl core::fmt::Debug for VtableZst {
	fn fmt(&self, _f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
	Ok(())
	}
	}
	// Size 16, alignment 8.
	#[repr(C)]
	struct MixedAlign {
	a: u8,
	b: u64,
	}
	impl core::fmt::Debug for MixedAlign {
	fn fmt(&self, _f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
	Ok(())
	}
	}
	// Size 16, alignment 16.
	#[repr(align(16))]
	struct OverAligned16(#[allow(dead_code)] u8);
	impl core::fmt::Debug for OverAligned16 {
	fn fmt(&self, _f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
	Ok(())
	}
	}
	#[kani::proof_for_contract(vtable_size_coerced_wrapper)]
	pub fn check_vtable_size_coerced_wrapper_contract_u8() {
	let val: u8 = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u8 = if real { &val } else { addr as *const u8 };
	kani::cover(!real, "vtable_size coerced u8: nondet-address pointer case reached");
	let _ = unsafe { vtable_size_coerced_wrapper::<u8>(ptr) };
	}
	#[kani::proof_for_contract(vtable_align_coerced_wrapper)]
	pub fn check_vtable_align_coerced_wrapper_contract_u8() {
	let val: u8 = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u8 = if real { &val } else { addr as *const u8 };
	kani::cover(!real, "vtable_align coerced u8: nondet-address pointer case reached");
	let _ = unsafe { vtable_align_coerced_wrapper::<u8>(ptr) };
	}
	#[kani::proof_for_contract(vtable_size_coerced_wrapper)]
	pub fn check_vtable_size_coerced_wrapper_contract_u32() {
	let val: u32 = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u32 = if real { &val } else { addr as *const u32 };
	kani::cover(!real, "vtable_size coerced u32: nondet-address pointer case reached");
	let _ = unsafe { vtable_size_coerced_wrapper::<u32>(ptr) };
	}
	#[kani::proof_for_contract(vtable_align_coerced_wrapper)]
	pub fn check_vtable_align_coerced_wrapper_contract_u32() {
	let val: u32 = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u32 = if real { &val } else { addr as *const u32 };
	kani::cover(!real, "vtable_align coerced u32: nondet-address pointer case reached");
	let _ = unsafe { vtable_align_coerced_wrapper::<u32>(ptr) };
	}
	#[kani::proof_for_contract(vtable_size_coerced_wrapper)]
	pub fn check_vtable_size_coerced_wrapper_contract_u64() {
	let val: u64 = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u64 = if real { &val } else { addr as *const u64 };
	kani::cover(!real, "vtable_size coerced u64: nondet-address pointer case reached");
	let _ = unsafe { vtable_size_coerced_wrapper::<u64>(ptr) };
	}
	#[kani::proof_for_contract(vtable_align_coerced_wrapper)]
	pub fn check_vtable_align_coerced_wrapper_contract_u64() {
	let val: u64 = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u64 = if real { &val } else { addr as *const u64 };
	kani::cover(!real, "vtable_align coerced u64: nondet-address pointer case reached");
	let _ = unsafe { vtable_align_coerced_wrapper::<u64>(ptr) };
	}
	// Size 8, alignment 1 rejects a `T = u32` monomorphic claim.
	#[kani::proof_for_contract(vtable_size_coerced_wrapper)]
	pub fn check_vtable_size_coerced_wrapper_contract_arr_u8_8() {
	let val: [u8; 8] = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const [u8; 8] = if real { &val } else { addr as *const [u8; 8] };
	kani::cover(!real, "vtable_size coerced [u8; 8]: nondet-address pointer case reached");
	let _ = unsafe { vtable_size_coerced_wrapper::<[u8; 8]>(ptr) };
	}
	#[kani::proof_for_contract(vtable_align_coerced_wrapper)]
	pub fn check_vtable_align_coerced_wrapper_contract_arr_u8_8() {
	let val: [u8; 8] = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const [u8; 8] = if real { &val } else { addr as *const [u8; 8] };
	kani::cover(!real, "vtable_align coerced [u8; 8]: nondet-address pointer case reached");
	let _ = unsafe { vtable_align_coerced_wrapper::<[u8; 8]>(ptr) };
	}
	#[kani::proof_for_contract(vtable_size_coerced_wrapper)]
	pub fn check_vtable_size_coerced_wrapper_contract_zst() {
	let val = VtableZst;
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const VtableZst = if real { &val } else { addr as *const VtableZst };
	kani::cover(!real, "vtable_size coerced ZST: nondet-address pointer case reached");
	let _ = unsafe { vtable_size_coerced_wrapper::<VtableZst>(ptr) };
	}
	#[kani::proof_for_contract(vtable_align_coerced_wrapper)]
	pub fn check_vtable_align_coerced_wrapper_contract_zst() {
	let val = VtableZst;
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const VtableZst = if real { &val } else { addr as *const VtableZst };
	kani::cover(!real, "vtable_align coerced ZST: nondet-address pointer case reached");
	let _ = unsafe { vtable_align_coerced_wrapper::<VtableZst>(ptr) };
	}
	#[kani::proof_for_contract(vtable_size_coerced_wrapper)]
	pub fn check_vtable_size_coerced_wrapper_contract_mixed_align() {
	let val = MixedAlign { a: kani::any(), b: kani::any() };
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const MixedAlign = if real { &val } else { addr as *const MixedAlign };
	kani::cover(!real, "vtable_size coerced MixedAlign: nondet-address pointer case reached");
	let _ = unsafe { vtable_size_coerced_wrapper::<MixedAlign>(ptr) };
	}
	#[kani::proof_for_contract(vtable_align_coerced_wrapper)]
	pub fn check_vtable_align_coerced_wrapper_contract_mixed_align() {
	let val = MixedAlign { a: kani::any(), b: kani::any() };
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const MixedAlign = if real { &val } else { addr as *const MixedAlign };
	kani::cover(!real, "vtable_align coerced MixedAlign: nondet-address pointer case reached");
	let _ = unsafe { vtable_align_coerced_wrapper::<MixedAlign>(ptr) };
	}
	#[kani::proof_for_contract(vtable_size_coerced_wrapper)]
	pub fn check_vtable_size_coerced_wrapper_contract_over_aligned() {
	let val = OverAligned16(kani::any());
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const OverAligned16 = if real { &val } else { addr as *const OverAligned16 };
	kani::cover(!real, "vtable_size coerced OverAligned16: nondet-address case reached");
	let _ = unsafe { vtable_size_coerced_wrapper::<OverAligned16>(ptr) };
	}
	#[kani::proof_for_contract(vtable_align_coerced_wrapper)]
	pub fn check_vtable_align_coerced_wrapper_contract_over_aligned() {
	let val = OverAligned16(kani::any());
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const OverAligned16 = if real { &val } else { addr as *const OverAligned16 };
	kani::cover(!real, "vtable_align coerced OverAligned16: nondet-address case reached");
	let _ = unsafe { vtable_align_coerced_wrapper::<OverAligned16>(ptr) };
	}

The harnesses include your u64 counterexample and six further size/alignment cases, among them
[u8; 8] (size 8, align 1), a ZST, and an over-aligned type. The raw *const () wrappers remain as
u32/u64 probes, labelled as such and excluded from the verified count. One residual stated
in-code: rustc's layout_of supplies both sides of the comparison.

2. size_of_val_wrapper precondition stronger than documented. can_dereference is removed; the
Sized contract is unconditional. The harness selects symbolically between null, dangling, a nondet
address and a real reference, with covers witnessing the first three are reached. For ?Sized, added
size_of_val_dyn_wrapper and size_of_val_slice_wrapper, the latter carrying the documented
size_of::<T>() == 0 || len <= isize::MAX / size_of::<T>() bound and nothing else.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 4393 to 4537 in e7b1bc1

	// For sized `T`, `size_of_val` reads no memory and accepts any pointer.
	// `size_of::<T>()` is the independent oracle. The harness covers null, dangling, and raw cases.
	// Residual: this wrapper excludes `?Sized`, whose metadata must be valid. Later wrappers cover
	// trait objects and slices.
	#[ensures(|result| *result == core::mem::size_of::<T>())]
	#[allow(dead_code)]
	unsafe fn size_of_val_wrapper<T>(ptr: *const T) -> usize {
	unsafe { size_of_val(ptr) }
	}
	#[kani::proof_for_contract(size_of_val_wrapper)]
	pub fn check_size_of_val_wrapper_contract() {
	let val: u32 = kani::any();
	let raw_addr: usize = kani::any();
	let case: u8 = kani::any();
	kani::assume(case < 4);
	let ptr: *const u32 = match case {
	0 => core::ptr::null(),
	1 => core::ptr::NonNull::<u32>::dangling().as_ptr() as *const u32,
	2 => raw_addr as *const u32,
	_ => &val as *const u32,
	};
	kani::cover(case == 0, "size_of_val: null pointer case reached");
	kani::cover(case == 1, "size_of_val: dangling pointer case reached");
	kani::cover(case == 2, "size_of_val: nondet-address pointer case reached");
	let _ = unsafe { size_of_val_wrapper::<u32>(ptr) };
	}
	// `size_of_val` for `?Sized` uses metadata. These wrappers establish its documented conditions.
	// The trait-object wrapper creates the vtable by unsizing. `size_of::<T>()` is its oracle.
	// The slice wrapper requires initialized `len` metadata whose byte size fits in `isize`.
	// Its oracle is `size_of::<T>() * len`; the ZST branch avoids division by zero.
	// Residual: composite unsized tails are not instantiated. Kani models them, so this is only
	// untested scope. Extern types are excluded because Kani's model panics on them.
	#[ensures(|result| *result == core::mem::size_of::<T>())]
	#[allow(dead_code)]
	unsafe fn size_of_val_dyn_wrapper<T: core::fmt::Debug>(ptr: *const T) -> usize {
	// The unsize coercion creates a valid vtable bound to `T`.
	let dyn_ptr: *const dyn core::fmt::Debug = ptr;
	unsafe { size_of_val(dyn_ptr) }
	}
	#[requires(
	core::mem::size_of::<T>() == 0
	|| len <= (isize::MAX as usize) / core::mem::size_of::<T>()
	)]
	#[ensures(|result| *result == core::mem::size_of::<T>() * len)]
	#[allow(dead_code)]
	unsafe fn size_of_val_slice_wrapper<T>(ptr: *const T, len: usize) -> usize {
	let slice_ptr: *const [T] = crate::ptr::slice_from_raw_parts(ptr, len);
	unsafe { size_of_val(slice_ptr) }
	}
	#[kani::proof_for_contract(size_of_val_dyn_wrapper)]
	pub fn check_size_of_val_dyn_wrapper_contract_u32() {
	let val: u32 = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u32 = if real { &val } else { addr as *const u32 };
	kani::cover(!real, "size_of_val dyn u32: nondet-address pointer case reached");
	let _ = unsafe { size_of_val_dyn_wrapper::<u32>(ptr) };
	}
	// Distinguish the size slot from alignment with an 8-byte, 1-aligned type.
	#[kani::proof_for_contract(size_of_val_dyn_wrapper)]
	pub fn check_size_of_val_dyn_wrapper_contract_arr_u8_8() {
	let val: [u8; 8] = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const [u8; 8] = if real { &val } else { addr as *const [u8; 8] };
	kani::cover(!real, "size_of_val dyn [u8; 8]: nondet-address pointer case reached");
	let _ = unsafe { size_of_val_dyn_wrapper::<[u8; 8]>(ptr) };
	}
	// Add an independent `(size, align) = (16, 16)` case.
	// Residual: only a composite unsized tail can exercise non-trivial alignment rounding.
	#[kani::proof_for_contract(size_of_val_dyn_wrapper)]
	pub fn check_size_of_val_dyn_wrapper_contract_over_aligned() {
	let val = OverAligned16(kani::any());
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const OverAligned16 = if real { &val } else { addr as *const OverAligned16 };
	kani::cover(!real, "size_of_val dyn OverAligned16: nondet-address case reached");
	let _ = unsafe { size_of_val_dyn_wrapper::<OverAligned16>(ptr) };
	}
	#[kani::proof_for_contract(size_of_val_dyn_wrapper)]
	pub fn check_size_of_val_dyn_wrapper_contract_zst() {
	let val = VtableZst;
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const VtableZst = if real { &val } else { addr as *const VtableZst };
	kani::cover(!real, "size_of_val dyn ZST: nondet-address pointer case reached");
	let _ = unsafe { size_of_val_dyn_wrapper::<VtableZst>(ptr) };
	}
	// Check every contract-valid symbolic `len`. `size_of_val` reads only slice metadata.
	#[kani::proof_for_contract(size_of_val_slice_wrapper)]
	pub fn check_size_of_val_slice_wrapper_contract_u8() {
	let val: [u8; 4] = kani::any();
	let len: usize = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u8 = if real { val.as_ptr() } else { addr as *const u8 };
	kani::cover(len == 0, "size_of_val slice u8: zero-length case reached");
	kani::cover(len > 1, "size_of_val slice u8: multi-element case reached");
	let _ = unsafe { size_of_val_slice_wrapper::<u8>(ptr, len) };
	}
	#[kani::proof_for_contract(size_of_val_slice_wrapper)]
	pub fn check_size_of_val_slice_wrapper_contract_u32() {
	let val: [u32; 4] = kani::any();
	let len: usize = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const u32 = if real { val.as_ptr() } else { addr as *const u32 };
	kani::cover(len == 0, "size_of_val slice u32: zero-length case reached");
	kani::cover(len > 1, "size_of_val slice u32: multi-element case reached");
	let _ = unsafe { size_of_val_slice_wrapper::<u32>(ptr, len) };
	}
	// A 16-byte element reaches the `isize::MAX` bound earliest.
	#[kani::proof_for_contract(size_of_val_slice_wrapper)]
	pub fn check_size_of_val_slice_wrapper_contract_over_aligned() {
	let val = OverAligned16(kani::any());
	let len: usize = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const OverAligned16 = if real { &val } else { addr as *const OverAligned16 };
	kani::cover(len == 0, "size_of_val slice OverAligned16: zero-length case reached");
	kani::cover(len > 1, "size_of_val slice OverAligned16: multi-element case reached");
	let _ = unsafe { size_of_val_slice_wrapper::<OverAligned16>(ptr, len) };
	}
	// Exercise the ZST branch for every `len`, including `usize::MAX`.
	#[kani::proof_for_contract(size_of_val_slice_wrapper)]
	pub fn check_size_of_val_slice_wrapper_contract_zst_elem() {
	let val = VtableZst;
	let len: usize = kani::any();
	let addr: usize = kani::any();
	let real: bool = kani::any();
	let ptr: *const VtableZst = if real { &val } else { addr as *const VtableZst };
	kani::cover(len == usize::MAX, "size_of_val slice ZST elem: usize::MAX length reached");
	let _ = unsafe { size_of_val_slice_wrapper::<VtableZst>(ptr, len) };
	}

Residuals: composite unsized tails are not instantiated, and extern type is excluded because
Kani's model panics on it.

3. compare_bytes_wrapper tractability cap in #[requires]. Done as asked. #[requires] now
carries readability of both regions and nothing else; bytes <= CAP is a kani::assume in the
harness. The #[ensures] comparison oracle is unchanged.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 4351 to 4391 in e7b1bc1

	// `compare_bytes` requires both regions to be readable for `bytes` bytes.
	// An independent loop checks every symbolic `bytes` value.
	// `COMPARE_BYTES_CAP` bounds only the harness, not the contract.
	const COMPARE_BYTES_CAP: usize = 4;
	#[requires(ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(left, bytes))
	&& ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(right, bytes)))]
	#[ensures(|result| {
	// Independently compare the first `bytes` bytes.
	let mut idx = 0;
	let mut verdict: i32 = 0;
	let mut decided = false;
	while idx < bytes {
	let lb = unsafe { *left.add(idx) };
	let rb = unsafe { *right.add(idx) };
	if !decided && lb != rb {
	verdict = if lb < rb { -1 } else { 1 };
	decided = true;
	}
	idx += 1;
	}
	if decided {
	(verdict < 0 && *result < 0) || (verdict > 0 && *result > 0)
	} else {
	*result == 0
	}
	})]
	#[allow(dead_code)]
	unsafe fn compare_bytes_wrapper(left: *const u8, right: *const u8, bytes: usize) -> i32 {
	unsafe { compare_bytes(left, right, bytes) }
	}
	#[kani::unwind(5)] // CAP (4) + 1
	#[kani::proof_for_contract(compare_bytes_wrapper)]
	pub fn check_compare_bytes_wrapper_contract() {
	const CAP: usize = COMPARE_BYTES_CAP;
	let left: [u8; CAP] = kani::any();
	let right: [u8; CAP] = kani::any();
	let bytes: usize = kani::any();
	kani::assume(bytes <= CAP);
	let _ = unsafe { compare_bytes_wrapper(left.as_ptr(), right.as_ptr(), bytes) };
	}

4. volatile_load / volatile_store exclude the MMIO case. No code change. Taking your second
option: these are now labelled unverified residuals in the source and in the PR body, rather than
presented as the full contract. The u32 wrappers verify round trips through ordinary Rust-backed
memory; the documented external-memory case remains unverified.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 4539 to 4571 in e7b1bc1

	// Check `volatile_load` and `volatile_store` by value-preserving round trips.
	// Residual: `can_dereference` and `can_write` cover only Rust-backed allocations. Kani's
	// pointer model cannot represent the documented external-memory MMIO case.
	#[requires(ub_checks::can_dereference(src))]
	#[ensures(|result| *result == unsafe { *src })]
	#[allow(dead_code)]
	unsafe fn volatile_load_wrapper(src: *const u32) -> u32 {
	unsafe { volatile_load(src) }
	}
	#[kani::proof_for_contract(volatile_load_wrapper)]
	pub fn check_volatile_load_wrapper_contract() {
	let val: u32 = kani::any();
	let local = val;
	let ptr: *const u32 = &local;
	let _ = unsafe { volatile_load_wrapper(ptr) };
	}
	#[cfg_attr(kani, kani::modifies(dst))]
	#[requires(ub_checks::can_write(dst))]
	#[ensures(|_| unsafe { *dst } == val)]
	#[allow(dead_code)]
	unsafe fn volatile_store_wrapper(dst: *mut u32, val: u32) {
	unsafe { volatile_store(dst, val) }
	}
	#[kani::proof_for_contract(volatile_store_wrapper)]
	pub fn check_volatile_store_wrapper_contract() {
	let val: u32 = kani::any();
	let mut local: u32 = kani::any();
	let ptr: *mut u32 = &mut local;
	unsafe { volatile_store_wrapper(ptr, val) };
	}

5. arith_offset_wrapper's undocumented 0..=8 bound. No contract change. Taking your framing: the
bounded wrapper is labelled a pointer-model probe in the source and the body, and is no longer
counted in contract form. The unbounded safety property stays in
check_arith_offset_unconditional_safety, over a fully symbolic offset.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 4228 to 4257 in e7b1bc1

	// `arith_offset` has no safety precondition. See `ptr/const_ptr.rs`.
	// `check_arith_offset_unconditional_safety` checks all offsets without dereferencing them.
	// Probe only: the bounded wrapper checks behavior in Kani's pointer model, not the intrinsic's
	// general contract. CBMC preserves the address identity only within the fixture object.
	#[requires(offset >= 0 && offset <= 8)]
	#[ensures(|result| *result as usize == (dst as usize).wrapping_add(offset as usize))]
	#[allow(dead_code)]
	unsafe fn arith_offset_wrapper(dst: *const u8, offset: isize) -> *const u8 {
	unsafe { arith_offset(dst, offset) }
	}
	#[kani::proof_for_contract(arith_offset_wrapper)]
	pub fn check_arith_offset_wrapper_contract() {
	let arr: [u8; 8] = kani::any();
	let base = arr.as_ptr();
	// The bound scopes only the pointer-model probe, not safety.
	let offset: isize = kani::any();
	let _ = unsafe { arith_offset_wrapper(base, offset) };
	}
	// Check unconditional `arith_offset` safety for every `offset: isize`.
	// The cover witnesses a non-null result.
	#[kani::proof]
	pub fn check_arith_offset_unconditional_safety() {
	let arr: [u8; 8] = kani::any();
	let base = arr.as_ptr();
	let offset: isize = kani::any();
	let r = unsafe { arith_offset(base, offset) };
	kani::cover(!r.is_null(), "arith_offset result observed with unbounded offset (no UB)");
	}

Non-blocking:

check_copy_untyped oracle asymmetry. Fixed at the helper — src is now offset by elem, so the
oracle compares the matching pair, and check_copy gained a cover witnessing that an overlapping
copy from a source not fully valid at the destination type is reachable. One residual I should state
rather than let you find: the oracle runs as #[ensures], so for an overlapping copy it reads the
source after the copy may have overwritten it. The indexing asymmetry you reported is fixed; that
weakness is not, and I can follow up on it if you want it closed here.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 2963 to 2981 in e7b1bc1

	fn check_copy_untyped<T>(src: *const T, dst: *mut T, count: usize) -> bool {
	#[cfg(kani)]
	if count > 0 {
	// Inspect a non-deterministically chosen byte in the copy.
	let byte = kani::any_where(|sz: &usize| *sz < size_of::<T>());
	// Instead of checking every one of the `count` copies, this picks one
	// non-deterministically and inspects it. Quantifiers add no value here: the solver already
	// picks an uninitialized element if one exists.
	let elem = kani::any_where(|val: &usize| *val < count);
	let src_data = unsafe { src.add(elem) } as *const u8;
	let dst_data = unsafe { dst.add(elem) } as *const u8;
	ub_checks::can_dereference(unsafe { src_data.add(byte) })
	== ub_checks::can_dereference(unsafe { dst_data.add(byte) })
	} else {
	true
	}
	#[cfg(not(kani))]
	false
	}

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 3580 to 3610 in e7b1bc1

	#[kani::proof_for_contract(copy_wrapper)]
	fn check_copy() {
	run_with_arbitrary_ptrs::<char>(|src, dst| {
	let count: usize = kani::any();
	// Witness a valid overlap. The same overflow, `can_dereference`, and `can_write`
	// conditions guard the contract call.
	let sz = core::mem::size_of::<char>();
	let s = src as usize;
	let d = dst as usize;
	let requires_hold = !count.overflowing_mul(sz).1
	&& ub_checks::can_dereference(core::ptr::slice_from_raw_parts(
	src as *const MaybeUninit<char>,
	count,
	))
	&& ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count));
	let overlap = count > 0
	&& s < d.wrapping_add(count.wrapping_mul(sz))
	&& d < s.wrapping_add(count.wrapping_mul(sz));
	kani::cover(
	requires_hold && overlap,
	"copy: contract-admissible overlapping src/dst (count>0) is reachable",
	);
	// Witness valid overlap with a source not fully initialized as `char`.
	// This makes the `check_copy_untyped` initialization oracle non-trivial.
	kani::cover(
	requires_hold && overlap && !ub_checks::can_dereference(src as *const char),
	"copy: overlapping call with a non-fully-initialized source is reachable",
	);
	unsafe { copy_wrapper(src, dst, count) }
	});
	}

ptr_offset_from precondition never exercised. Strengthened the fixture rather than noting the
gap. Both harnesses build two independent arrays and choose each pointer's provenance symbolically,
so cross-allocation and reversed-order pairs are reachable and the #[requires] filters.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 4259 to 4315 in e7b1bc1

	// Match `ptr_offset_from` in `ptr/const_ptr.rs`: no overflow, whole elements, same allocation.
	#[requires(
	(ptr as isize).checked_sub(base as isize).is_some()
	&& (ptr as isize - base as isize) % (size_of::<u8>() as isize) == 0
	&& (ptr as isize == base as isize || ub_checks::same_allocation(ptr, base))
	)]
	#[ensures(|result| *result == (ptr as isize - base as isize) / (size_of::<u8>() as isize))]
	#[allow(dead_code)]
	unsafe fn ptr_offset_from_wrapper(ptr: *const u8, base: *const u8) -> isize {
	unsafe { ptr_offset_from(ptr, base) }
	}
	#[kani::proof_for_contract(ptr_offset_from_wrapper)]
	pub fn check_ptr_offset_from_wrapper_contract() {
	let arr_a: [u8; 8] = kani::any();
	let arr_b: [u8; 8] = kani::any();
	let base_a = arr_a.as_ptr();
	let base_b = arr_b.as_ptr();
	let i: usize = kani::any();
	let j: usize = kani::any();
	kani::assume(i <= 8 && j <= 8);
	// Reach both same- and cross-allocation pairs. `#[requires]` filters them.
	let pi_from_a: bool = kani::any();
	let pj_from_a: bool = kani::any();
	let pi = if pi_from_a { unsafe { base_a.add(i) } } else { unsafe { base_b.add(i) } };
	let pj = if pj_from_a { unsafe { base_a.add(j) } } else { unsafe { base_b.add(j) } };
	let _ = unsafe { ptr_offset_from_wrapper(pi, pj) };
	}
	// `ptr_offset_from_unsigned` also requires `ptr >= base`. See `ptr/const_ptr.rs`.
	#[requires(
	(ptr as isize).checked_sub(base as isize).is_some()
	&& (ptr as isize - base as isize) % (size_of::<u8>() as isize) == 0
	&& (ptr as isize == base as isize || ub_checks::same_allocation(ptr, base))
	&& ptr as usize >= base as usize
	)]
	#[ensures(|result| *result == (ptr as usize - base as usize) / size_of::<u8>())]
	#[allow(dead_code)]
	unsafe fn ptr_offset_from_unsigned_wrapper(ptr: *const u8, base: *const u8) -> usize {
	unsafe { ptr_offset_from_unsigned(ptr, base) }
	}
	#[kani::proof_for_contract(ptr_offset_from_unsigned_wrapper)]
	pub fn check_ptr_offset_from_unsigned_wrapper_contract() {
	let arr_a: [u8; 8] = kani::any();
	let arr_b: [u8; 8] = kani::any();
	let base_a = arr_a.as_ptr();
	let base_b = arr_b.as_ptr();
	let i: usize = kani::any();
	let j: usize = kani::any();
	kani::assume(i <= 8 && j <= 8);
	let pi_from_a: bool = kani::any();
	let pj_from_a: bool = kani::any();
	let pi = if pi_from_a { unsafe { base_a.add(i) } } else { unsafe { base_b.add(i) } };
	let pj = if pj_from_a { unsafe { base_a.add(j) } } else { unsafe { base_b.add(j) } };
	let _ = unsafe { ptr_offset_from_unsigned_wrapper(pi, pj) };
	}

typed_swap_fallback_wrapper verifies a copied body. Took your suggestion and extracted the
shared helper: typed_swap_nonoverlapping_fallback now holds the one-line fallback body, and both
the intrinsic's fallback and the verification wrapper call it — so the proof covers the production
fallback path itself, and the two can no longer drift apart.

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 2558 to 2567 in e7b1bc1

	/// Shared fallback body of [`typed_swap_nonoverlapping`], factored out so the
	/// Kani verification wrapper can execute the same code the intrinsic falls back to.
	#[rustc_const_stable_indirect] // must follow stable const rules: reachable from the const-stable-indirect intrinsic below
	#[inline]
	const unsafe fn typed_swap_nonoverlapping_fallback<T>(x: *mut T, y: *mut T) {
	// SAFETY: The caller provided single non-overlapping items behind
	// pointers, so swapping them with `count: 1` is fine.
	unsafe { ptr::swap_nonoverlapping(x, y, 1) };
	}

verify-rust-std/library/core/src/intrinsics/mod.rs

Lines 3511 to 3528 in e7b1bc1

	// Kani models `typed_swap_nonoverlapping` itself with `codegen_swap`, so
	// `#[kani::proof_for_contract]` can never enter its fallback body directly. This wrapper
	// and the intrinsic's fallback body both call the same shared helper,
	// `typed_swap_nonoverlapping_fallback`, so proving this wrapper against the contract proves
	// the production fallback path too, and the two cannot drift apart.
	// `ptr::swap_nonoverlapping` reaches `copy_nonoverlapping`, never `typed_swap_nonoverlapping`.
	// The proof is therefore not circular.
	#[cfg_attr(kani, kani::modifies(x))]
	#[cfg_attr(kani, kani::modifies(y))]
	#[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
	#[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
	#[requires(x.addr() != y.addr() || core::mem::size_of::<T>() == 0)]
	#[requires(ub_checks::maybe_is_nonoverlapping(x as *const (), y as *const (), size_of::<T>(), 1))]
	#[ensures(|_| ub_checks::can_dereference(x) && ub_checks::can_dereference(y))]
	#[allow(dead_code)]
	unsafe fn typed_swap_fallback_wrapper<T>(x: *mut T, y: *mut T) {
	unsafe { typed_swap_nonoverlapping_fallback(x, y) }
	}

The PR body is updated to match the current scope.

Re-requesting review.

[ivmat]

if you are interested, you can check acceptance file for this PR based on acceptance format i've been developing.

[ivmat]

Not yet complete, found some issuea