Challenge 29: Verify the safety of Box and ThinBox in alloc::boxed

[kasimte]

Towards #526. Solves Challenge 29: Safety of boxed.

The challenge asks for safety contracts on 9 unsafe functions and verification of at least 75% of the 46 safe functions; this covers all 9 and all 46, including the ThinBox/WithHeader family that has no Box analog. Generics are instantiated at primitive types, which the challenge allows, with the Global allocator. The work is 74 Kani harnesses in one mod verify per file, all passing via scripts/run-kani.sh, as a purely additive change to three files. On every one, Kani also checks the challenge's four listed undefined behaviors — access through a dangling or misaligned pointer, misuse of intrinsics, mutation of immutable bytes, and production of an invalid value.

The 9 unsafe functions

All nine carry safety contracts, and all nine are verified — six with proof_for_contract, three by construction. The four raw-pointer constructors — from_raw, from_non_null, and their _in variants — are discharged at a sized instantiation and, for the _in pair, an unsized [u8] one. Both assume_inits are discharged as well, with the target spelled through the impl's own generic parameters (Box::<MaybeUninit<T>, A>::assume_init): concrete turbofish arguments do not resolve against that impl's structured self-type, but the generic-parameter form does.

The remaining three — the downcast_uncheckeds — are verified by running the real function body on symbolic inputs and asserting the whole postcondition, the returned value and its pointer identity: at this repository's Kani pin, proof_for_contract resolves none of the three same-named dyn-self impls, across five path spellings including the resolver's own printed implementation forms. Their contracts are annotated and checked in the harness rather than machine-linked, with an in-code note at each site. The root cause is that those impl blocks live in a different module than Box, so the resolver renders them in an <impl …> path form no spelling can match; a resolver fix developed alongside this work (model-checking/kani#4777, fix in model-checking/kani#4778) verifies all three as proof_for_contract targets under a patched Kani, and each note marks the mechanical upgrade for a pin that includes it.

The challenge's function table also lists <dyn Error>::downcast_unchecked three times, but no such method exists: impl dyn Error exposes only the safe downcast. The three real downcast_uncheckeds are on Box<dyn Any (+ Send)(+ Sync), A>, and those are the ones contracted here.

The 46 safe functions

Most are heap round-trips — allocate, write, hand out a pointer, reconstruct — where the harness checks that the value and its allocation come back intact. A few carry a property worth verifying on its own terms, and the ThinBox/WithHeader family is the genuinely new work.

Group	What the harnesses establish
Constructors and ownership handoffs — new_in/try_new_*, write, into_boxed_slice, into_raw/into_non_null/into_unique/leak, into_pin	the value and its allocation survive the round-trip
Slice constructors	the same, at a fully symbolic length bounded only by what Layout::array will accept
Conversions — into_array, from_slice, From<&str>, From<Box<str>>, and both TryFroms	content preserved, or both the matching- and mismatched-length arms; the spec's TryFrom<Box<T>> row has no impl in the tree, so the two real TryFrom sources stand in for it
downcast on Box<dyn Any…> and dyn Error…	the success and the failure arm, with pointer identity on success
Drop, Default, Clone	including the Box<str> clone, which asserts a fresh allocation for a non-empty string and the shared dangling pointer for an empty one
ThinBox / WithHeader	the full family; new_unsize_zst is proven with no assumptions on a slice-metadata instantiation

Two habits keep the proofs honest. First, covers: each input-bearing harness carries a kani::cover confirming it reaches the operation under test rather than passing on a setup that silently failed, and where a function has two reachable outcomes, both arms are covered — so no proof passes while checking a dead or unreachable path. No harness constrains its inputs with kani::assume; every input restriction is a visible any_where domain. Second, panics are proven rather than assumed away: should_panic harnesses send a panicking-drop sentinel through Box<T> and Box<[T]> drop glue, and drive all four non-try slice constructors past isize::MAX into their capacity-overflow guard.

What this Kani pin can't reach

Two behaviors sit outside the model here, both noted in-code where they occur. Allocation never fails in Kani, so the Err arm of every try_new* is unreachable — those harnesses verify the success arm and mark the dead branch rather than covering it. And new_unsize_zst's dyn Any form fails inside its const-allocated metadata block, on a missing drop_in_place::<dyn Any> and pointer-liveness checks on the const pointer, so that function is proven on its slice-metadata route instead. The last overflow guard, in WithHeader layout arithmetic, is reachable only by a near-isize::MAX type and is covered through the slice constructors above.

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

[kasimte]

Hi @feliperodri — thanks for working through the Challenge 29 reviews; I was wondering if #669 might have been missed? Would you be open to taking a look when you have a chance? It's a purely additive solution — all 9 unsafe fns carry contracts, and the safe functions are well past the challenge's 75% bar. It also surfaced (and I filed a fix for) a Kani resolver limitation that blocks proof_for_contract on these trait-object methods (kani#4778). Happy to rebase to clear the merge conflict whenever that's useful. Thanks!

[feliperodri]

Thanks @kasimte, and apologies — you were right that this was missed in the Challenge 29 round (it was created after the snapshot our triage list was built from). I've now reviewed it fully.

This is a genuinely strong, sound solution: 9/9 unsafe fns with contracts (6 via #[kani::proof_for_contract], 3 Box<dyn Any>::downcast_unchecked verified by-construction on symbolic payloads — the same Kani trait-object resolver limitation, which you've helpfully filed kani#4778 to fix) and 46/46 safe abstractions (~100%, slightly ahead of the other solution's 45/46). Clean on all our vacuity checks — no cfg body swaps, no trivial/loop invariants, no kani::assume anywhere (all restrictions are visible any_where domains), uncapped symbolic slice lengths, per-harness kani::cover non-vacuity witnesses, should_panic twins for the overflow/drop-glue-panic paths, and you even recorded a real Kani counterexample that corrected an over-strong !addr_eq claim. Excellent verification hygiene.

Requesting changes only on the prioritization: we reviewed all four open Challenge 29 solutions together and approved #639 as the accepted solution — it achieves the same 9/9 (6 proof_for_contract + 3 by-construction) + 45/46 coverage more concisely (+765 vs +1200 here), which matters for upstreamability. This PR is equally sound and marginally more complete, so we're keeping it as the strong alternative rather than displacing an already-approved equivalent. If #639 stalls, this is our fallback.

Two things that would make this the stronger of the two: (1) your kani#4778 fix landing so the 3 downcast_unchecked contracts become real proof_for_contracts (a genuine edge over #639) — please link the kani PR here; (2) trimming the width-duplicate harnesses to tighten the diff. Really appreciate the work and the upstream Kani fix.