[sankalpsthakur]

Resolves #526 (Challenge 29: Box, convert and ThinBox).

Add safety contracts and Kani harnesses using the repository's safety::{requires, ensures} annotations. Runtime stdlib logic is unchanged.

Coverage includes assume-init methods, raw/non-null reconstructors, ThinBox operations, slice constructors, downcast paths and pinning. Slice harnesses use bounded symbolic lengths. Reconstructor contracts check dereferenceability and layout bounds; allocator provenance remains a caller obligation that these contracts cannot express.

The challenge's unchecked dyn Error methods do not exist in this tree. The actual Box<dyn Any> downcast_unchecked variants carry contracts and are proved with proof_for_contract, which needs model-checking/kani#4778 (in the pinned Kani). The listed TryFrom<Box<T>> implementation also does not exist; TryFrom<Vec<T>> is covered separately.

Validation

On the current head 4712f513d5, all 27 completed GitHub checks pass (2 skipped). The earlier run 32560286046 at 4da62f00d5 reported 1,447 (Ubuntu) and 1,446 (macOS) verified autoharness harnesses with zero failures. These are run-level results, not counts of new harnesses in this PR.

AI coding tools assisted with the contracts, harnesses and this description.

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

[sankalpsthakur]

Ready for committee FCFS review of Challenge 29 (in-window, end 2026-12-31).

Head 5d8f0ee99218643bc7eb62fe39aa70b6c43508cb:

• Kani partitions 1–4 SUCCESS
• Autoharness ubuntu: 1445 harnesses, 0 failures
• Autoharness macos: 1444 harnesses, 0 failures
• Flux, GOTO, VeriFast, upstream_test SUCCESS
• Contracts use repo-standard safety::{requires, ensures}

Tracking Fixes #526. No second solution PR.

[feliperodri]

Approving — leading solution for Challenge 29

Thanks @sankalpsthakur. After reviewing all three open Challenge 29 (boxed) solutions with our vacuity tooling and local Kani (pinned 0.67.0 / CBMC 6.8.0), this is complete, sound, and the most concise. Prioritizing it.

Coverage against Ch29 criteria:

• A: 9/9 unsafe fns with contracts + verified. assume_init (sized+slice), from_raw, from_non_null, from_raw_in, from_non_null_in are verified via #[kani::proof_for_contract] (6). The 3 downcast_unchecked methods carry contracts and are exercised via plain #[kani::proof] with the precondition mirrored by kani::assume — Kani cannot resolve proof_for_contract on a trait-object generic method (Box<dyn Any>::downcast_unchecked::<T>), the documented/accepted workaround. Note the 3 challenge-listed <dyn Error>::downcast_unchecked don't exist in std — the real methods are Box<dyn Any(+Send)(+Sync)>::downcast_unchecked, which you correctly verified (disclosed in the PR).
• B: 45/46 safe abstractions (97.8%, ≥ 75%). Only <Box<[T;N]> as TryFrom<Box<T>>>::try_from (which doesn't exist in-tree) is uncovered.

Soundness (all clean):

• T1: no cfg body swaps — 906 lines pure additions, no - lines; the only cfg-gated code is the box_ptr_fits_box_layout helper used in requires clauses.
• T2: no trivial invariants, no loop_invariant(true); slice iteration uses unwind(4) for len ≤ 2 (non-vacuous).
• T7: 6/9 unsafe fns + boxed_slice_as_array_unchecked have proof_for_contract; the 3 downcast_unchecked + WithHeader::drop are assume-mirror (Kani trait-object limitation, disclosed). Autoharness allowlist unchanged.
• Not assume-the-conclusion — downcast harnesses build Box::new(concrete) then downcast to the same type; the is::<T>() witness is real, not assumed.
• Inputs symbolic (kani::any()); primitive-mono is challenge-allowed; no unbounded clause. No runtime std logic changed.

Local Kani sample (CBMC 6.8.0): 4/4 VERIFICATION SUCCESSFUL — check_assume_init_i32 (proof_for_contract), check_from_raw_i32 (proof_for_contract), check_downcast_unchecked_any, check_leak.

Minor note (non-blocking): the 3 Box<dyn Any>::downcast_unchecked contracts and WithHeader::drop rely on assume-mirror rather than proof_for_contract (Kani limitation) — worth a tracking note so they can be upgraded if kani gains trait-object contract resolution. Complete and sound as-is.

[sankalpsthakur]

Merged current main in c454b54 and resolved the boxed conversion import conflict. The alloc crate compiles on nightly-2026-02-05 and the three changed files pass rustfmt with the pinned upstream configuration. The contracts and harnesses are unchanged; full Kani verification on this updated base remains pending.

[sankalpsthakur]

CI caught two harnesses still referencing BoxFromSlice, which current main removed. Updated them to use Box::from in cdfeac6, preserving the inputs and assertions. The full proof checks are rerunning; no proof pass is claimed yet.

[sankalpsthakur]

At cdfeac6, all four Ubuntu proof partitions, Ubuntu autoharness and GOTO pass. The Ubuntu metrics job received a runner shutdown signal and exited 143: log. Could a maintainer rerun that job? GitHub denied my rerun request for lack of admin rights. macOS jobs remain queued.

[sankalpsthakur]

At cdfeac6, all five macOS proof jobs stop before verification: Kani setup fails when Homebrew rejects the diffblue/cbmc tap as untrusted (log). Ubuntu proof partitions and autoharness pass. The runner setup needs repair before macOS can rerun; no harness change is indicated by these failures.

[sankalpsthakur]

@feliperodri Current main made Box::assume_init a const fn. With our #[requires] contract on it, the alloc build fails under Kani with E0493 (the owned receiver's destructor can't be evaluated in a const fn), so the merge with main doesn't compile yet: log. Would you prefer moving that contract into an assume-mirror harness like the downcast_unchecked ones, or waiting for Kani to handle owned receivers in const contracts? Main also removed into_unique, so that harness would be retired either way.

[sankalpsthakur]

at e5c65ce, the now-const Box::assume_init contract is a commented todo; three plain proofs mirror its pre/postconditions to avoid E0493. into_array follows Result; the removed into_unique harness is gone. kani proof partitions and autoharness pass; metrics remain red. @feliperodri, does the mirrored contract still satisfy criterion a, or should i use a contracted wrapper?

[sankalpsthakur]

kani metrics red is the typ.rs:777 crash in stdarch sve, same on main since oct 6, unrelated to this pr

[feliperodri]

@sankalpsthakur, re-reviewing the changes since my approval: all 71 harnesses verify locally with the pinned Kani. One request: none of them has a kani::cover, so a passing run doesn't show that the paths they're meant to check are reached. Could you add covers for the cases each harness targets, for example kani::cover!(len == N) and kani::cover!(len != N) in check_into_array and check_try_from_boxed_slice, the Ok and Err arms of the downcast harnesses, and an empty and non-empty slice in the slice constructors? Kani reports a cover as SATISFIED only if some execution reaches it, which guards against harnesses whose assumptions rule out the interesting inputs.

[feliperodri]

Requesting changes on the commits since my approval. Two harnesses can't reach the case they're meant to rule out, and nothing in the suite shows which paths are reached.

What I checked locally with the pinned Kani (6ce55b9): all 71 harnesses verify. Criterion 1: 8 of the 9 unsafe functions have contracts verified with proof_for_contract (from_raw, from_non_null, from_raw_in and from_non_null_in for i32 and [u8], the slice assume_init, and the three downcast_unchecked). Moving downcast_unchecked to proof_for_contract is an improvement. Criterion 2: every listed function except the removed into_unique has a harness, well above 75%. The diff is additive (+774/−0).

Mutation testing:

Mutant	Result
Box::write skips the write	killed by check_write
ThinBox drop frees ptr - value_offset - 1	killed by 10 harnesses
into_array accepts len >= N	survives
TryFrom<Box<[T]>> accepts len >= N	survives

The two survivors are the inline comments below. With no kani::cover anywhere (see my earlier comment), this kind of gap doesn't show up in the results.

On the sized assume_init: I put the commented-out contract back and Kani fails with error[E0493]: destructor of Box<MaybeUninit<T>, A> cannot be evaluated at compile-time, so the TODO is right that this is a Kani limitation, and the mirror harnesses are the best available. Could you open a Kani issue for it and link it from the TODO, so the contract comes back when that's fixed?

What would flip this to approval: the two harnesses below reaching len > N, and covers on the cases the harnesses target.

[feliperodri]

@sankalpsthakur any news?

[sankalpsthakur]

working on it. check_into_array, check_try_from_boxed_slice and check_try_from_vec (same gap) now draw the slice from an [i32; N + 1] array, so len > N is reached, and they cover len < N, len == N and len > N. the other harnesses cover their cases: empty and full slices, the Ok and Err results of the downcasts, and a reachability cover after each contract call and assumed precondition. for the assume_init TODO, model-checking/kani#4984 already tracks this E0493 case, so i link that one. it's running on my fork's CI now, together with your two mutants, and i'll push here once it's green.

[sankalpsthakur]

pushed 4e2719b and 5f0e638:

• check_into_array, check_try_from_boxed_slice and check_try_from_vec draw from an [i32; N + 1] array and cover len < N, len == N and len > N.
• the slice constructors and the slice assume_init, from_raw, from_non_null, from_raw_in and from_non_null_in harnesses cover an empty and a full slice, the downcast harnesses cover their Ok and Err results, and the contract harnesses and the sized assume_init mirrors cover that they are reached with the precondition assumed.
• the assume_init TODO links Cannot annotate a const fn taking self by value with a contract (E0493) kani#4984, which already tracks this E0493 case.

on my fork, with main merged (Kani cd355b0) and only the boxed:: harnesses:

• all 71 verify, and all 64 cover properties are satisfied, in 38 harnesses: https://github.com/sankalpsthakur/verify-rust-std/actions/runs/41581793208
• with your two mutants, plus the same one in TryFrom<Vec<T>>, the three array harnesses fail and the other 68 verify: https://github.com/sankalpsthakur/verify-rust-std/actions/runs/41581796149. check_into_array fails on assert!(len == SLICE_CAP), and the two TryFrom harnesses on the debug_assert_eq! in boxed_slice_as_array_unchecked.

the other 33 harnesses have no length, result or precondition that picks a path, so they have no case to cover.

a heads-up: on my fork ubuntu-latest is now ubuntu 26.04, and the Kani setup then fails to install CBMC because there's no ubuntu-26.04-cbmc-6.11.0-Linux.deb, so these runs pin ubuntu-24.04.

[feliperodri]

Re-verified on 5f0e638 with the pinned Kani: all 71 harnesses pass, all 64 covers are satisfied, and both mutants from my last review (into_array and TryFrom<Box<[T]>> accepting len >= N) now fail. Thanks for the quick turnaround.

Approving. The one remaining gap is the contract on the sized Box<MaybeUninit<T>>::assume_init, which Kani can't attach today (E0493, model-checking/kani#4984); the mirror harnesses cover it in the meantime. We'll add the contract back once kani#4984 is fixed.

[feliperodri]

@sankalpsthakur would you be willing to write a blog post about this proof for https://model-checking.github.io/kani-verifier-blog/?

[sankalpsthakur]

thanks for the careful review, the mutation run made the harnesses better. yes, i'd be glad to write it. i'll send you a draft

[rajath-mk]

Ran all 71 harnesses at the pinned Kani: all verify and all 64 covers are reached. I also re-ran the len >= N mutants for into_array, TryFrom<Box<[T]>> and TryFrom<Vec<T>>, and each is killed by its own harness. One thing about this contract: can_dereference only checks initialization under -Z uninit-checks (otherwise Kani treats is_initialized as true), and CI doesn't pass that flag. So in CI this requires doesn't rule out uninitialized elements: a proof_for_contract calling Box::<[MaybeUninit<u8>]>::new_uninit_slice(len).assume_init() without writing anything still verifies. With -Z uninit-checks, Kani reports [MaybeUninit<u8>] as unsupported (union layout), so neither setup checks it today. Not blocking, since it's a Kani limitation, but could you reword "encodes that for Kani" here and "covers aligned/initialized" on box_ptr_fits_box_layout (line 213) to say initialization stays the caller's obligation?