[v3risec]

Summary

This PR adds Kani-based verification artifacts for Rc/Weak safety in library/alloc/src/rcs/rc.rs for Challenge 26.

The change introduces:

• proof harness modules under #[cfg(kani)] for all 12 required unsafe functions and all 54 listed safe functions;
• contracts for unsafe pointer and reference-count operations;
• semantic result assertions for safe functions, followed by kani::cover properties to demonstrate that the checked paths are reachable;
• shared helper-based construction for nondeterministic unsized slice inputs, so Rc<[T]>/Weak<[T]> paths can be exercised in a reusable way.

No non-verification runtime behavior is changed in normal builds.

Verification Coverage Report

Unsafe functions (required by Challenge 26)

Coverage: 12 / 12 (100%)

Verified set includes:

• Rc<mem::MaybeUninit<T>,A>::assume_init
• Rc<[mem::MaybeUninit<T>],A>::assume_init
• Rc<T:?Sized>::from_raw
• Rc<T:?Sized>::increment_strong_count
• Rc<T:?Sized>::decrement_strong_count
• Rc<T:?Sized,A:Allocator>::from_raw_in
• Rc<T:?Sized,A:Allocator>::increment_strong_count_in
• Rc<T:?Sized,A:Allocator>::decrement_strong_count_in
• Rc<T:?Sized,A:Allocator>::get_mut_unchecked
• Rc<dyn Any,A:Allocator>::downcast_unchecked
• Weak<T:?Sized>::from_raw
• Weak<T:?Sized,A:Allocator>::from_raw_in

Safe functions (Challenge 26 list)

Coverage: 54 / 54 (100%)

This exceeds the challenge threshold (>= 75%).

Covered safe functions (54/54), grouped by API category:

Allocation

• Rc<T>::new
• Rc<T>::new_uninit
• Rc<T>::new_zeroed
• Rc<T>::try_new
• Rc<T>::try_new_uninit
• Rc<T>::try_new_zeroed
• Rc<T>::pin
• Rc<T,A:Allocator>::new_uninit_in
• Rc<T,A:Allocator>::new_zeroed_in
• Rc<T,A:Allocator>::new_cyclic_in
• Rc<T,A:Allocator>::try_new_in
• Rc<T,A:Allocator>::try_new_uninit_in
• Rc<T,A:Allocator>::try_new_zeroed_in
• Rc<T,A:Allocator>::pin_in

Slice

• Rc<[T]>::new_uninit_slice
• Rc<[T]>::new_zeroed_slice
• Rc<[T]>::into_array
• Rc<[T],A:Allocator>::new_uninit_slice_in
• Rc<[T],A:Allocator>::new_zeroed_slice_in
• RcFromSlice<T: Copy>::from_slice
• RcFromSlice<T: Clone>::from_slice
• ToRcSlice<T, I>::to_rc_slice

Conversion and pointer

• Rc<T:?Sized, A:Allocator>::inner
• Rc<T:?Sized, A:Allocator>::into_inner_with_allocator
• Rc<T,A:Allocator>::try_unwrap
• Rc<T:?Sized,A:Allocator>::into_raw_with_allocator
• Rc<T:?Sized,A:Allocator>::as_ptr
• Rc<T:?Sized,A:Allocator>::get_mut
• Rc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut
• Rc<T:?Sized,A:Allocator>::from_box_in
• Rc<dyn Any,A:Allocator>::downcast

Trait implementations (Rc)

• Clone<T: ?Sized, A:Allocator>::clone for Rc
• Drop<T: ?Sized, A:Allocator>::drop for Rc
• Default<T:Default>::default
• Default<str>::default
• From<&str>::from
• From<Vec<T,A:Allocator>>::from
• From<Rc<str>>::from
• TryFrom<Rc<[T],A:Allocator>>::try_from

Weak and traits

• Weak<T:?Sized,A:Allocator>::as_ptr
• Weak<T:?Sized,A:Allocator>::into_raw_with_allocator
• Weak<T:?Sized,A:Allocator>::upgrade
• Weak<T:?Sized,A:Allocator>::inner
• Drop<T:?Sized, A:Allocator>::drop for Weak

UniqueRc and traits

• UniqueRc<T:?Sized,A:Allocator>::into_rc
• UniqueRc<T:?Sized,A:Allocator+Clone>::downgrade
• Deref<T:?Sized,A:Allocator>::deref
• DerefMut<T:?Sized,A:Allocator>::deref_mut
• Drop<T:?Sized, A:Allocator>::drop for UniqueRc
• UniqueRcUninit<T:?Sized, A:Allocator>::new
• UniqueRcUninit<T:?Sized, A:Allocator>::data_ptr
• Drop<T:?Sized, A:Allocator>::drop for UniqueRcUninit

Refcount internals

• RcInnerPtr::inc_strong
• RcInnerPtr::inc_weak

Note

• Verify the default RcFromSlice<T: Clone>::from_slice implementation with a manually implemented non-trivial Clone type, ensuring that the harness does not dispatch to the TrivialClone specialization.
• Verify ToRcSlice<T, I>::to_rc_slice through the FromIterator and exact-size TrustedLen path.
• Both harnesses execute the real Rc::from_iter_exact implementation and its original element-writing loop. The target implementation is not replaced with a cfg(kani)-specific loop.
• These two harnesses use symbolic inputs bounded to at most four elements and unwind the real loop. This is a verification tractability bound: current Kani loop contracts cannot soundly and tractably summarize the iterator's private pointer state, pointer provenance, and yielded values.

Three Criteria Met (Challenge 26)

• Required unsafe functions covered: All 12/12 required unsafe functions in Challenge 26 are annotated with contracts and verified.
• Safe-function threshold met: 54/54 safe functions are covered (100%), which exceeds the Challenge 26 requirement of at least 75%.
• Challenge scope allowances respected: Generic T is instantiated with allowed representative concrete types, and allocator-focused proofs are limited to standard-library allocator scope (Global).

Approach

The verification strategy combines contracts for unsafe entry points with executable proof harnesses:

1. Contract for unsafe functions

• Attach requires preconditions for pointer validity, alignment soundness, same-allocation checks, and refcount well-formedness.
• Attach postconditions where appropriate (ensures) and mutation footprints (kani::modifies) for refcount-changing operations.

2. Harness-backed behavioral checks

• Use #[kani::proof_for_contract(...)] harnesses for all required unsafe functions, and regular #[kani::proof] harnesses for the covered safe functions.
• Check safe functions' results including ownership changes, reference counts, pointer identity, slice length, and initialized payload.
• Place kani::cover properties after the corresponding assertions to show that the verified paths are not vacuous.

3. Helper-based unbounded input generalization

• Introduce shared helper functions for nondeterministic and unbounded vector/slice setup and reuse them across harnesses that target ?Sized slice-based functions.
• Use the helpers to exercise unsized slice cases through Rc<[T]>/Weak<[T]> constructions without duplicating per-harness setup logic.

4. Challenge alignment

• Keep all verification code under cfg(kani) so normal std behavior is unchanged.
• Target Challenge 26 success criteria directly: full required unsafe coverage + safe coverage above threshold.

Scope assumptions (per challenge allowance)

• Harnesses instantiate representative concrete types, including signed/unsigned widths (i8..i128, u8..u128), bool, (), arrays, vectors, slices, str, and trait objects (dyn Any).
• Allocator coverage is limited to Global (both explicit Rc<_, Global> / Weak<_, Global> and default Rc/Weak aliases).

Verification

All harnesses in this PR pass locally with Kani.

Platform-specific CI tractability note

The shared nondeterministic vector helper now bounds the symbolic length to <= 100 for CI resource stability. This is only a verification-time tractability bound for shared CI runners; it is not a safety condition or a function-behavior assumption.

Resolves #382

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

[feliperodri]

You should use macros to reduce code duplication. It'll also make review easier.

[Copilot]

Copilot wasn't able to review any files in this pull request.

[Copilot]

Copilot wasn't able to review any files in this pull request.

[Copilot]

Pull request overview

Copilot reviewed 1 out of 3 changed files in this pull request and generated 5 comments.

[v3risec]

Thanks for the thoughtful review. We have addressed all 5 comments and pushed 3 follow-up commits with the requested changes. The PR should now be ready for another round of CI and review. Could you please re-run the CI checks when possible?

[v3risec]

Hi, I would like to report what appears to be a CI resource / environment issue rather than a reproducible proof failure.
In my latest commit f6716a99a6b05a4f298cc83f62aff10ab8c3fad3, I observed two CBMC out-of-memory failures in CI:

1. In Kani / Verify std library (partition 1) (pull_request),
   rc::verify_3051::harness_from_vec_i32 failed with:
   CBMC appears to have run out of memory.

2. In Kani / Verify std library using autoharness (macos-latest) (pull_request),
   rc::verify_1650::harness_rc_from_raw_in_vec_u64 failed with:
   CBMC appears to have run out of memory.

What I want to emphasize is that both of these harnesses verify successfully in my local environment, and I do not see any CBMC appears to have run out of memory failure locally.

They also succeeded in the earlier commit e189a7d8a8b06cee7eb6a33c32ea024639702ebe. The harness definitions themselves were unchanged between the two commits, although shared helper code used by them did change (ptr::write_bytes added), so I cannot claim the proof inputs were fully identical across revisions. Still, the local-vs-CI discrepancy suggests that these proofs may be close to the CI resource boundary.

For reference, my local verification environment is:

• CPU: 2 x Intel(R) Xeon(R) Gold 6230R CPU @ 2.10GHz
• Cores / threads: 52 physical cores / 104 logical CPUs
• Memory: 125 GiB RAM
• OS: Ubuntu 24.04.1-based system
• Kernel: Linux 6.11.0-26-generic
• Kani: repo-pinned version from tool_config/kani-version.toml, commit 415ca503aea80fd4c4c4819ad4770b744f1bc3a1
• CBMC: 6.8.0 (cbmc-6.8.0)
• Rust: rustc 1.92.0-nightly (b6f0945e4 2025-10-08)
• Host: x86_64-unknown-linux-gnu
• LLVM: 21.1.2

So these do not appear to be stable. Given that these harnesses pass locally without any CBMC out-of-memory issue, would it make sense to investigate whether the CI runners are hitting memory limits, and if so, whether the memory budget or other CI resource constraints for these Kani jobs should be adjusted?

[v3risec]

Update on the CI resource issue:

The recent changes add a macOS-only bound to the nondeterministic slice/vector length used by the shared Rc<[T]> / Weak<[T]> helper code. This was added because some of these harnesses were hitting CBMC resource limits in GitHub Actions, while the same harnesses verified successfully in my local Ubuntu environment.

The bound is guarded by #[cfg(target_os = "macos")], so it only applies to the macOS CI configuration. Ubuntu/Linux verification keeps the original unbounded path with respect to this additional platform-specific assumption.

The intent is to keep the macOS CI jobs within their time/memory budget, not to change normal std behavior or the Linux verification setup.

[feliperodri]

Challenge 26 (Rc/Weak) — verification-soundness review

This is genuine, substantial verification work: 112 #[kani::proof] + 20 #[kani::proof_for_contract] (the macros expand these across ~13 primitive/slice instantiations each, yielding the full 132/24 harness counts). Both success criteria are met and the work is sound. I'm landing on COMMENT for a few non-blocking issues a maintainer should weigh before merge.

Soundness checklist — all clear

1. cfg-swap vacuity — BENIGN. The only #[cfg(not(kani))] (library/alloc/src/rc.rs, diff line 434) rewrites the from_slice for (i,item) in iter.enumerate() loop into an equivalent while let Some(item) = iter.next() under #[cfg(kani)], purely to attach #[kani::loop_invariant(i == guard.n_elems)] and loop_modifies. Runtime path keeps the upstream body; the Kani body performs identical ptr::write + n_elems bookkeeping. This is the accepted for→while rewrite pattern, not a fatal body swap. The other cfg(not(...)) are no_global_oom_handling (upstream) and target_os="macos" harness disables (resource limits) — benign.
2. No assume-the-conclusion. proof_for_contract harnesses construct a valid Rc/Weak from kani::any() and derive the raw pointer via into_raw/into_raw_with_allocator, so the precondition holds by construction rather than by assuming the conclusion.
3. No trivial invariants. Only loop_invariant(i == guard.n_elems) — meaningful. No invariant(true), requires(true), or assume(false).
4. Contract-liveness (T7) — real & faithful. All 10 proof_for_contract-verified unsafe fns target contracts newly added in this diff. Contracts encode provenance/refcount preconditions with the correct predicates: from_raw/from_raw_in (diff ~1333, ~1630) require ptr::addr_eq to the rebuilt inner pointer, kani::mem::checked_size_of_raw/checked_align_of_raw match, and strong >= 1; get_mut_unchecked (~1955) requires can_write and ensures result aliases the value; downcast_unchecked (~2204) requires (*self).is::<T>() (exactly the documented precondition); Weak::from_raw{,_in} (~3317/~3534) correctly special-case the is_dangling sentinel plus weak > 0 and same_allocation. These are faithful, not decorative, not over-constrained.
5. Symbolic, not concrete. Values are kani::any(); pointers are symbolic in Kani's model. Slice lengths are symbolic within a bound.
6. Bounded vs unbounded. Slice harnesses bound length (kani::assume(len <= 1024) / sz <= 1024 in verifier_nondet_vec). Acceptable for tractability; challenge permits primitive types only.
7. Success criteria — MET. (a) All 12 required unsafe fns have contracts: 10 verified via proof_for_contract; the two assume_init variants carry contracts (requires can_dereference, ensures strong_count >= 1) verified via #[kani::proof] with an explicit postcondition assertion — justified by both the Kani 0.65 MaybeUninit-impl path-resolution limitation and the challenge's own note that "showing something is initialized … may be impossible to express." (b) Safe-fn coverage spans essentially the entire ~53-entry list (new/new_uninit/new_zeroed/try_* families, pin/pin_in, into_array, get_mut, make_mut, downcast, from_box_in, From impls, Drop/Clone/Default, UniqueRc/UniqueRcUninit, Weak::{as_ptr,upgrade,inner,into_raw_with_allocator}, RcInnerPtr::inc_*), well above 75%. Branch-split harnesses (unique/shared/weak-present; success/failure; live/strong_zero/dangling) show real thought.

This is clearly superior to the competing #574 (zero contracts, concrete-only inputs).

Non-blocking issues to address

• Convention: uses raw kani:: attributes, not the tool-agnostic safety crate. All contracts are #[cfg_attr(kani, kani::requires(...))] / kani::ensures / kani::modifies with use core::kani. Per CLAUDE.md / library/contracts/safety, contracts are supposed to use use safety::{requires, ensures} so they are tool-agnostic and plausibly upstreamable. As written these contracts are Kani-only and diverge from every other merged challenge. Recommend porting to the safety attributes. (Note the Cargo.lock churn adding safety/proc-macro-error to core/alloc deps — reconcile with the branch's existing safety integration.)
• assume_init contracts are present but not proof_for_contract-enforced. The harnesses (verify_1198/verify_1239) run the real body on constructed-valid inputs and manually assert the postcondition, which is sound. But the code comment's claim that "the requires clause is still checked as an assertion at the call site" is imprecise — a contract on a normally-called (non-stubbed, non-target) function is inert in Kani; the requires is satisfied here only because the input is constructed valid, not independently checked. Reword the comment to avoid over-claiming.
• Roundtrip inside a requires clause. The increment_strong_count/increment_strong_count_in preconditions (diff ~1408, ~1760) build Rc::from_raw(ptr) and call into_raw inside the requires to compare addresses. It nets out refcount-neutral and evidently passes CI, but embedding construct/consume logic in a precondition is fragile; consider simplifying to the pure provenance/addr_eq checks used by the other contracts.

Net: sound, faithful, meets both criteria. The above are quality/convention items, not soundness defects.

[v3risec]

@feliperodri Thanks for the detailed review. I’ve addressed the three non-blocking points:

• Migrated all 13 requires and 6 ensures contracts in alloc::rc to the tool-agnostic safety::{requires, ensures} attributes. The four kani::modifies attributes remain Kani-specific frame conditions because the safety crate does not currently provide an equivalent modifies attribute.
• Reworked the comments for both assume_init harness groups. They now state explicitly that a regular #[kani::proof] executes the real function body but does not activate the callee’s requires or ensures contract.
• Explicitly mirrored the expressible assume_init contract conditions in the harnesses:
  • both scalar and slice harnesses assert kani::mem::can_dereference(Rc::as_ptr(&uninit)) before the call;
  • the scalar harness asserts Rc::strong_count(&init) >= 1 afterward;
  • the slice harness retains the stronger strong_count == 1 assertion;
  • the existing value, allocation-address, and slice-length assertions remain in place.
• Clarified that the initialization obligation is established constructively: scalar values are initialized with MaybeUninit::write, while slice backing storage is initialized before assume_init is called.
• Removed the Rc::from_raw/into_raw roundtrips from the affected requires clauses. The contracts now use only the direct pointer/address, dynamic size/alignment, and strong >= 1 checks, while retaining their existing frame conditions.

Please let me know if there are any other changes you would like me to make.

[v3risec]

@feliperodri All CI checks are green now, and I’ve addressed the non-blocking issues. This should be ready for another look. Thanks!

[v3risec]

Strengthen the Challenge 26 Kani safe functions' harnesses for Rc and related Weak, UniqueRc, and UniqueRcUninit paths.

The safe functions' harnesses now:

• add semantic result assertions with matching kani::cover properties;
• check strong and weak reference-count invariants across construction, cloning, conversion, raw-pointer roundtrips, and destruction;
• cover live, expired, and dangling weak-pointer states;
• exercise relevant ownership transitions, including unique, shared, and weak-present states;

[v3risec]

Added standalone verification coverage for the two previously uncovered safe functions:

• RcFromSlice<T: Clone>::from_slice
• ToRcSlice<T, I>::to_rc_slice

The RcFromSlice harness uses a type with a manual, non-trivial Clone implementation, which forces dispatch through the default clone-per-element implementation rather than the TrivialClone specialization.

The ToRcSlice harness exercises the exact-size TrustedLen path through FromIterator. Both harnesses call the real Rc::from_iter_exact implementation and unwind its original element-writing loop.

These two harnesses use nondeterministic inputs bounded to at most four elements with #[kani::unwind(6)]. The bound is needed because current Kani loop contracts cannot soundly and tractably summarize the iterator's private pointer state, pointer provenance, and yielded values.

With these additions, the PR now provides standalone coverage for all 54/54 safe functions listed in Challenge 26.

[feliperodri]

Approving — leading solution for Challenge 26

Thanks @v3risec. After reviewing both open Challenge 26 (Rc/Weak) solutions with our vacuity tooling and local Kani (pinned 0.67.0 / CBMC 6.8.0), this is complete and sound. Prioritizing it.

Coverage against Ch26 criteria:

• A: 12/12 unsafe pub fns with real #[requires]/#[ensures]/kani::modifies contracts backed by matching #[kani::proof_for_contract] harnesses, monomorphized across primitive T (i8..i128, u8..u128, bool, unit, [u8;4]) and unsized [T] as challenge-allowed.
• B: ~54/54 safe abstractions with unsafe (~100%, ≥ 75%). Complete coverage across new(_uninit/_zeroed/in), try*, pin/pin_in, into_array, get_mut/make_mut (with 3-state coverage), downcast (Ok+Err), from_box_in, RcFromSlice / ToRcSlice, Drop/Clone/Default, all From/TryFrom variants, Weak::{as_ptr,into_raw_with_allocator,upgrade,inner} (multi-path), inc_strong/inc_weak (+ should_panic overflow), UniqueRc + UniqueRcUninit.

Soundness (all clean):

• T1: no cfg body swaps — grep for cfg(not(kani)) in the diff returns 0 hits; harnesses run the real bodies.
• T2: no trivial invariants, no loop_invariant(true).
• T7: all 12 unsafe fns have explicit proof_for_contract; .github/workflows/kani.yml autoharness allowlist unchanged — no silent autoharness dependency.
• Not assume-the-conclusion — the only kani::assume(can_dereference(...)) is Vec::set_len's own precondition inside a helper, not the fn under proof.
• Inputs symbolic (kani::any::<T>()); slice length bounded ≤100 (documented CI-tractability budget); iterator loops unwind(6) for 4-element input (documented Kani loop-contract limitation).
• No runtime std logic changed.

Local Kani sample (CBMC 6.8.0): 4/4 VERIFICATION SUCCESSFUL — harness_rc_assume_init_i8 (proof_for_contract), harness_rc_downcast_unchecked_i8 (proof_for_contract), harness_inc_strong_overflow_should_panic, harness_rc_default_str.

Minor weaknesses to note for the record (non-blocking):

1. verifier_nondet_vec uses ptr::write_bytes(..., kani::any::<u8>(), size_of::<T>() * sz) — one symbolic byte pattern replicated across all elements, so a run over Rc<[u32]> only covers [0x00000000; n], [0x01010101; n], … Symbolic but coverage-limited for multi-byte T.
2. Rc::from_raw, Rc::increment_strong_count, and Weak::from_raw (non-_in variants) read (*ptr).get() inside unsafe without an explicit kani::mem::can_dereference in the requires, unlike the _in variants which do. Harmless for the roundtrip harnesses (pointers are always valid), but the exported contract is weaker than the _in variant for arbitrary callers — consider adding can_dereference to match.
3. Rc::get_mut_unchecked contract only requires can_write(value); the documented safety property (no other Rc/Weak may reference the inner value) is not encoded — the harness proves UB-freedom of the body but under-specifies the caller obligation.
4. Roundtrip-narrowed inputs (from_raw/increment/decrement use ptr obtained via into_raw) narrow the input universe vs a fully symbolic pointer meeting the precondition.

These are contract-strength refinements, not soundness bugs; they can be addressed in a followup. Challenge 26 explicitly permits bounded + primitive-mono.

[feliperodri]

@lucasccordeiro @rajath-mk @patricklam @HuStmpHrrr could you review this propose solution for challenge 26?

[v3risec]

@feliperodri Thanks! I've rebased onto the latest main and resolved the conflicts. The force-push rewrote the commit history as part of the rebase, which explains the large number of updated commits.

A few updates:

• Updated the README.md link to the new rcs/rc.rs path.
• Temporarily removed the two overflow harnesses for inc_strong and inc_weak, since the pinned Kani doesn't support abort_immediate(). Added comments explaining the limitation.
• Cleaned up a duplicate Rc::new call and an outdated comment.

No worries about the delay, and thanks for the continued reviews!

[feliperodri]

@v3risec, an update after re-reviewing #587 (Ch27, Arc), so the two are judged the same way.

This PR has the same UB-list gaps as #587 (which also leaves out data races):

UB item in the spec	#582 (Rc)	#587 (Arc)
Mutating immutable bytes	Not covered. get_mut_unchecked's rule that no other Rc/Weak may be used while the &mut lives isn't in its contract	Same gap
Producing an invalid value	Not checked: -Z valid-value-checks isn't enabled in run-kani.sh	Same gap

#587 is now approved as sound proofs toward Ch27 that don't solve the challenge, and this PR should be treated the same way, so I'm no longer holding it on these items. You can address them in follow-up PRs. Whether solutions must cover the first one, which Kani can't check, is being discussed in #733.

[v3risec]

Update on -Z valid-value-checks and Challenge 26 coverage

@feliperodri To address the “Producing an invalid value” gap, I ran the Rc/Weak harnesses locally with -Z valid-value-checks using Kani 0.68.0 (6ce55b9) and CBMC 6.11.0.

This exposed several limitations in Kani's experimental checker:

• Unsupported validity checks for copy_nonoverlapping.

• Unsupported mutable pointer casts during raw-pointer reconstruction, byte offsets, and deallocation.

• Unsupported raw-pointer dereference validity checks involving RcInner<dyn Any>.

• False positives on valid RcInner<bool> initialization, including Box::new and partial field initialization.

These failures are verifier limitations or demonstrated false positives, not counterexamples establishing UB in Rc/Weak.

For unsized harnesses, the previous symbolic-length verifier_nondet_vec + Rc::from(Vec) setup triggered the unsupported copy_nonoverlapping check. Where possible, I replaced it with:

let array: [$elem; 1024] = kani::any();
let strong: Rc<[$elem]> = Rc::new(array);

This is a deliberate bounded verification approach: the elements remain symbolic, and the real unsized Rc<[T]> paths are still exercised, but the slice length is fixed. It is a workaround for the current tool limitation, not an attempt to hide a verification failure.

I temporarily commented out the blocked harnesses and paths, with TODOs explaining why they need to be restored. Counting a function as covered when at least one harness remains enabled, the current source-level coverage is:

• Unsafe: 11/12 (91.7%) — downcast_unchecked remains blocked by Kani.

• Safe: 49/54 (90.7%) — above the 75% threshold.

The remaining unsafe-function gap is explicitly acknowledged rather than counted as verified.

I have not enabled -Z valid-value-checks globally in run-kani.sh, since that would affect all verification harnesses, including those currently blocked by the experimental checker. The results above therefore describe local opt-in checking, not an additional CI-enforced check.

Would this local validation and the documented Kani limitations be sufficient to address the invalid-value gap, or would you require CI integration? If #733 accepts the Kani-only scope for “mutating immutable bytes,” and the remaining tool-blocked unsafe function can be accepted as an exception or resolved, could this PR be considered a complete Challenge 26 solution?

[feliperodri]

Re-approving on the current commit (fa0abd4). Criteria 1 and 2 are met and the proofs are sound. Challenge 26 doesn't list data races. The two UB items Kani can't establish here ("mutating immutable bytes" and "producing an invalid value") are with the committee in #733, so whether this resolves the challenge depends on that ruling.