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

[ivmat]

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

Closes a substantial part of Challenge 2, and states plainly what it does not close. Per criterion 4, the assumptions are listed rather than implied.

Criterion 1 requires all 20; this PR delivers 15 and documents precisely why the rest are not counted. The challenge sets no partial threshold — whether to land partial progress is the maintainers' call.

Headline: 15 of the 20 mandated intrinsics are verified — 14 in the mandated contract form (including vtable_size/vtable_align, upgraded from monomorphic probes to coercion-based contracts (no #[requires]) per review), plus arith_offset (which has no documented safety precondition) via an unbounded no-UB proof (see ¹). The remaining 5 are not verifiable by official Kani at the pinned commit (d4df833) — Kani emits an explicit "not currently supported" diagnostic for each. That is a tool gap, not a proof failure: the upstream fix is merged (kani#4672, kani#4673), and all five verify under a build carrying those merges (see Residuals).

What is verified

15 of the 20 mandated intrinsics — 14 with a doc-derived safety contract verified via #[kani::proof_for_contract], plus arith_offset¹ (no documented precondition) closed by an unbounded no-UB proof:

typed_swap (in-tree today as 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

¹ arith_offset has no documented preconditions; its safety claim is check_arith_offset_unconditional_safety — a plain #[kani::proof] over a fully-symbolic (unbounded) offset, with the base pointer a single representative 8-byte allocation. It is not a #[kani::proof_for_contract]. The bounded contract-form wrapper alongside it is a behavioral/pointer-model probe, not the intrinsic's contract, and is not counted.

² vtable_size/vtable_align are counted via wrappers that take *const T and perform the unsize coercion inside the wrapper, so the pointer handed to the intrinsic is a vtable for T by construction — "ptr is a vtable" is established, not assumed — with the generic postcondition size_of::<T>()/align_of::<T>(). Verified at 7 erased types with independent size/align (incl. [u8;8], a ZST, mixed-align and over-aligned structs). The earlier raw-*const () monomorphic wrappers are kept in-tree, labelled probes, uncounted. Residuals: the monomorphization set is finite (as for every generic contract here), and the coercion fixes one trait (Debug); both stated in Assumptions.

³ size_of_val is verified on three paths: T: Sized (requires nothing — matching the documentation — with null/dangling/nondet-address witnesses), trait objects (dyn-metadata wrapper, 4 erased types), and slices with symbolic length, whose single #[requires] is the documented size * len ≤ isize::MAX condition (its ablation observed failing inside Kani's own size model). The extern type metadata case does not exist on stable and is a named residual.

Whole-module run on the currently pinned toolchain:

Complete - 370 successfully verified harnesses, 0 failures, 370 total.

Toolchain identity captured at run time rather than inferred, because the version string 0.67.0 is
identical for the 0.67.0 release and the pinned dev commit:

Kani	d4df833c8f8f18e632e7b0a7945bb2161f708990 (the commit tool_config/kani-version.toml pins)
CBMC	6.8.0 — the version that Kani commit's kani-dependencies declares
Flags	--no-assert-contracts, --object-bits 12

Non-vacuity is machine-checked, not asserted: every harness authored for this work carries kani::cover witnesses, all satisfied on the run above. None is unsatisfied — which matters, because Kani reports a harness whose cover is unsatisfiable as VERIFICATION: SUCCESSFUL, so an uninspected cover count can hide a vacuous proof. These covers witness that a scenario is reachable; they are not all adversarial, and which #[requires] clauses are actually load-bearing is tracked separately under Assumptions → precondition exercise status.

Preconditions are exercised, not just stated, where the fixture permits it: the same-allocation requires on ptr_offset_from(_unsigned) were ablation-tested — weakening them to true makes the harnesses FAIL (two-allocation nondet fixtures) — and the slice-size requires on size_of_val fails the same ablation test inside Kani's size model. Load-bearing clauses, demonstrated.

Every counted intrinsic except arith_offset carries doc-derived #[requires]/#[ensures], verified with #[kani::proof_for_contract]; arith_offset (no documented precondition) is closed by an unbounded no-UB proof instead (see ¹).

Because kani#3325 blocks contracts directly on bodyless #[rustc_intrinsic] declarations, contracts sit on a thin unsafe fn <name>_wrapper — the same pattern already used in-tree for transmute_unchecked_wrapper (PR #185), and the workaround recorded in kani#3345. For the vtable pair the wrapper additionally constructs the vtable by unsize coercion rather than assuming its validity — the same by-construction technique already in-tree in the NonNull::from_raw_parts harnesses (PR #127), which build a genuine dyn-trait vtable via coercion and read its metadata.

Each proof uses an independent reference check: the property is checked against a separately-computed expected value (for the vtable pair: the compiler's own size_of/align_of), never by re-calling the intrinsic under test. Honest bound, stated so a reviewer meets it head-on: for the layout intrinsics that expected value and the intrinsic's result both ultimately descend from rustc's layout_of, so the check is relative to the layout model — as is every size/align contract in this repo (e.g. Layout::new's size() == size_of::<T>(), PR #43). What it still falsifies end to end: the coercion wiring the right vtable, the model reading the right slot (the fixture set is chosen so size and align are mutually discriminating), and rustc's constant agreeing with CBMC's __CPROVER_OBJECT_SIZE — two independent sources of truth. See Criterion 3 below for the slot-level detail.

Criterion-by-criterion

#	Criterion	Status
1	All listed intrinsics annotated with safety contracts	15/20. 14 in contract form; the 15th (arith_offset, no documented precondition) via an unbounded no-UB proof — see ¹. The 5 residuals are not annotated, because pinned Kani cannot codegen them (support merged upstream, unreleased).
2	Any fallback intrinsic implementation must be verified	Closed. Of the 21 listed names, min_align_of_val is a non-intrinsic core::mem wrapper, so criterion 2 does not range over it; it resolves to the bodyless align_of_val intrinsic. Of the 20 intrinsics, 19 are declared with no body — nothing for the criterion to range over — and exactly one, typed_swap_nonoverlapping, carries a fallback body (unsafe { ptr::swap_nonoverlapping(x, y, 1) }), verified against the intrinsic's own contract via a wrapper that forces symbolic execution of the body rather than Kani's built-in model. The fallback body is factored into a shared private helper (typed_swap_nonoverlapping_fallback) that both the intrinsic and the verification wrapper call, so the proof covers the production fallback path itself and the two cannot drift apart. This shows the fallback satisfies the contract, not that Kani's model and the fallback are equivalent — a claim criterion 2 does not make.
3	Explain how modelled intrinsics match their definition	Stated per intrinsic: the independent-reference-check construction, plus the contracts themselves as the machine-checked correspondence. For the vtable pair — the one place the model is non-obvious — see the Criterion 3 subsection below.
4	State assumptions, auditability, guaranteed properties	See Assumptions and bounds below — deliberately explicit.
5	Documented conditions are sufficient for safe use	Satisfied for the counted contracts (requires = the documented conditions, no more — tractability caps live in harnesses, not contracts; size_of_val requires nothing for T: Sized and only the documented size bound for slices). Two carve-outs, stated plainly: volatile_load/volatile_store use can_dereference/can_write, which are proven for Rust-allocation-backed memory only — the documented MMIO case (aligned, non-trapping access outside any Rust allocation) is a named unverified residual (see Assumptions); and arith_offset's documented condition set is empty, so its sufficiency is shown by the unbounded no-UB proof, not a contract (see ¹). Open for the 5 tool-blocked residuals.

Criterion 3 — how the vtable_size/vtable_align model is matched

For the value/pointer intrinsics the contract is the correspondence. The vtable pair is the one place the model deserves spelling out, because the intrinsic reads a compiler-emitted structure:

• What the coercion binds. let dyn_ptr: *const dyn Debug = ptr; makes rustc emit the unique vtable for (T, dyn Debug) — under Kani's codegen the global vtable_impl_for_T (codegen_cast_to_fat_pointer → codegen_vtable). No fixture choice can substitute a vtable for a different erased type: the metadata is a function of T alone, so size_of::<T>() is the correct oracle for every T.
• What the intrinsic reads. Kani's vtable_info casts a per-trait vtable struct to the type-erased Kani::CommonVTable and reads the size/align slots by field name — a real layout-agreement obligation between two distinct struct types, not a no-op.
• The cross-check. check_vtable_size asserts the rustc constant equals CBMC's __CPROVER_OBJECT_SIZE — two independently derived sizes agreeing.
• What it cannot detect (named, not hidden): rustc's layout_of disagreeing with the vtable LLVM finally emits. That limit is relative to the model and is shared by every contract in this challenge.

The counted form is the coerced *const T wrapper: validity is established by construction for the (T, dyn Debug) pair, not asserted over arbitrary *const () inputs. So this is a generic, by-construction contract on the vtable path — not a reusable specification over the intrinsic's raw erased-pointer domain, nor over all traits/DSTs (those bounds are named under Assumptions). The raw *const () probes are kept in-tree, labelled, and excluded from the count; if a reviewer holds that a *const T wrapper is "a different function's contract," the probes stand as the monomorphic evidence they are, and the count is unaffected either way.

These two intrinsics are, additionally, already reached by merged maintainer-authored work: PR #43 (Layout::for_value/for_value_raw, tautschnig) verifies the dyn Debug case, which exercises vtable_size/vtable_align through Kani's model — to date the only merged verification that touches the vtable pair at all. That is the public-caller precedent that these intrinsics are legitimately verified via a real caller's contract; the coerced wrapper here is the complementary form that additionally pins the returned size/align to size_of::<T>()/align_of::<T>(), which the layout-only Layout::for_value postcondition does not state.

Residuals — what is NOT covered, at the headline

5 intrinsics official Kani cannot verify at the pinned commit:
volatile_copy_memory, volatile_copy_nonoverlapping_memory, volatile_set_memory, unaligned_volatile_load, unaligned_volatile_store.

These are not proof failures. Running each harness produces Kani's own diagnostic, e.g.:

volatile_set_memory is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose

The harnesses are written and kept in-tree under #[cfg(not(kani))], so the exact attempted proof is preserved and can be un-gated the moment support lands.

The upstream fix is merged — kani#4672 (volatile_copy_memory, volatile_copy_nonoverlapping_memory, volatile_set_memory) and kani#4673 (unaligned_volatile_load, unaligned_volatile_store). What the investigation behind those PRs found, all checkable by reading Kani's tree: the placeholders were never compiled (unstable_codegen! never expands its tokens), so the gated bodies had bit-rotted; the sketched implementation had (dst, src) reversed relative to Kani's codegen_copy; and adding the missing volatile_set_memory variant ICEs the points-to analysis unless handled.

Complete-picture check, run on a build of the pinned commit with both merges applied: contracts + harnesses for all five (same faithfulness treatment as the 15: MMIO residual named, no undocumented preconditions, ablation controls), and the full 20-intrinsic target set verifies whole-module with zero failures. This PR does not claim those five: the count stays 15/20 until Kani releases the merged support and this repo's kani-version.toml moves — at which point the additional commits are ready to land. Reported so the residuals are visibly tool-gated rather than quietly failing proofs.

One caveat preserved from that work, for whoever un-gates these later: check_volatile_copy_memory_no_ub as originally written combined a symbolic shift with for i in 0..(N - shift), putting a symbolic trip count in the formula (40 minutes, no convergence). Rewritten to the fixed-representative-SHIFT pattern check_copy_overlapping_shift_no_ub already uses, it verifies in 0.13s. That is a real weakening, identical to the one copy's own overlap harness carries, and it is flagged here rather than buried.

Why these five are gated rather than modeled behind a stand-in. A tempting shortcut is to give each unsupported volatile intrinsic a wrapper whose body calls an ordinary supported operation — copy, copy_nonoverlapping, write_bytes, read_unaligned/write_unaligned — and verify that. This PR deliberately does not do that. A #[kani::proof_for_contract] over a body that never calls the real intrinsic verifies the stand-in, not the intrinsic's own codegen; the volatile semantics (the flag that stops the optimizer reordering the access) are exactly what such a model drops. And the upstream investigation behind kani#4672/rust-lang#4673 found the sketched volatile_copy_memory implementation had (dst, src) reversed — precisely the class of defect a stand-in hides. So the five stay under #[cfg(not(kani))] with the real attempted proof preserved, and the honest count is 15/20 until the tool supports them — at which point the additional commits land as a genuine 20/20, each intrinsic verified against its own codegen rather than a substitute.

Assumptions and bounds (criterion 4)

These are the honest limits of what the proofs establish.

• Bounded, not unbounded. Proofs use small concrete sizes (typically N = 4) with symbolic contents. Tractability caps (e.g. compare_bytes' byte cap) live in the harness as assumes — the contracts state only documented conditions.
• Type coverage is finite, not generic. Each harness instantiates fixed concrete types. For the vtable pair this deserves its own sentence, since it was the review's core finding: the coerced wrappers are verified at 7 erased types with adversarially independent size/align, which establishes the generic contract per-instantiation — not ∀T — and the unsize coercion fixes one trait (Debug); the vtable layout Kani models is trait-independent. The arbitrary-pointer harnesses additionally exclude Dangling/DeadObject allocation states, which Kani's memory predicates cannot currently model.
• Overlap coverage is representative, not exhaustive. The copy overlap harness uses a fixed representative SHIFT with a symbolic index. This applies to copy, one of the 15 claimed above.
• No harness in this module is stub-mediated. The -Z stubbing flag in the reproduction command is required only because the module also contains pre-existing upstream transmute harnesses using #[kani::stub_verified]. No challenge-2 harness uses kani::stub or stub_verified.
• --no-assert-contracts. Dependency contracts are assumed, not asserted. The contracts under proof_for_contract are themselves fully checked.
• --object-bits 12. Fails loudly if exceeded — a sound bound, not a silent cap.
• Precondition exercise status, clause by clause. ptr_offset_from(_unsigned)'s same_allocation clause and size_of_val (slice)'s size-bound requires are ablation-tested load-bearing (observed FAILING when weakened). Because both ptr_offset_from wrappers are instantiated at T = u8, their byte-distance-divisibility clause reduces to % 1 == 0 and is not exercised (a named gap; a u32 instantiation with misaligned pointer pairs would exercise it). copy_nonoverlapping's non-overlap requires remains doc-correct but not falsifiable by its single-array fixture. For overlapping copy, the initialization oracle check_copy_untyped compares post-state source against post-state destination; a kani::cover in check_copy records whether the non-trivial mixed-initialization-overlap domain is reachable, and the post-state (rather than pre-state) comparison is a named limit on that domain.
• write_bytes value check. The write_bytes_wrapper contract constrains only UB and initialization, not the written value. A separate plain proof check_write_bytes_sets_value reads each written byte back and requires it to equal val, so the written value is independently checked.
• volatile_load/volatile_store cover Rust-allocation-backed memory only. The documented MMIO case (aligned, non-trapping access outside any Rust allocation) is an unverified residual; can_dereference/can_write do not model it.
• Non-vacuity is machine-witnessed where this PR adds harnesses. Every harness authored for this work carries a satisfied post-state kani::cover. The pre-existing typed_swap harnesses predate this discipline and carry none.
• Table-2 "usage sites" are argued by code inspection, not machine-checked. swap, copy_from_slice and the align_of_val site each delegate to the named intrinsic; zeroed delegates to write_bytes, which is verified here. The fifth, parse_u64_into, is the naming finding below.

Existing code this PR replaces (called out deliberately)

The diff touches one file, library/core/src/intrinsics/mod.rs. Pieces removed or corrected rather than left alongside:

• The commented-out check_copy and check_copy_nonoverlapping sketches — superseded by working proof_for_contract harnesses on the wrapper pattern that resolves their own noted blocker.
• The #[cfg(not(kani))]-disabled write_bytes harness and its kani#90 FIXME. kani#90 remains open upstream; the specific configuration this FIXME guarded verifies here (all 296 checks pass), with a kani::cover witnessing the exact kani#90 trigger as reachable. If maintainers would rather keep the FIXME until kani#90 is formally closed, say so and I'll restore it.
• The check_copy_untyped helper's element pairing (pre-existing) compared dst[elem] against src[0]; per review it now pairs src[elem] with dst[elem]. Both dependent harnesses stayed green after the fix, and a planted mutation in the corrected comparison was observed failing.
• typed_swap_nonoverlapping's fallback body is factored into a shared private helper, typed_swap_nonoverlapping_fallback (the same one-line ptr::swap_nonoverlapping(x, y, 1) call, semantically unchanged, marked rustc_const_stable_indirect), per review — so the verification wrapper executes the same code the intrinsic falls back to, rather than a copy of it.

No other upstream code is modified, and nothing outside this file is touched.

One finding for the maintainers

The challenge's mandated table lists parse_u64_into, which git grep parse_u64_into across library/ at this branch's HEAD does not find (this subtree mirrors rust-lang/rust, so a rename would have happened there). It may be renamed or removed upstream. Flagging it rather than silently dropping it — happy to open a separate issue if useful.

Reproducing

kani verify-std -Z unstable-options ./library \
    -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi \
    -Z loop-contracts -Z quantifiers -Z stubbing \
    --no-assert-contracts \
    --harness intrinsics::verify:: \
    --cbmc-args --object-bits 12

All harnesses live in library/core/src/intrinsics/mod.rs under mod verify. To reproduce the complete-picture check: build Kani at d4df833 with the merged kani#4672/rust-lang#4673 commits applied, and run the same command against this branch plus the five un-gated volatile harness commits (available on request).

[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