Repository navigation
Conversation
|
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 |
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
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.
|
Thanks for the detailed review, @feliperodri. On your two notes:
|
d9684c5 to
ddd07e8
Compare
|
@feliperodri the width-duplicate trim from your second note is in:
|
Thanks for merging it. Done on the Kani side (model-checking/kani#4778). Converting the three here needs this repo's pinned Kani ( The width-duplicate trim from (2) already went in (74→68 harnesses). |
…odule (model-checking#4778) Resolves model-checking#4777. `last_two_items_of_path_match` compares the user's turbofish against `def_path_str`'s rendering of each candidate. Impls living outside their type's home module render as `<impl Type<Args>>`, which no user-spellable path can equal — so multi-candidate methods in that position (e.g. the three `Box<dyn Any(+Send)(+Sync), A>::downcast_unchecked` impls in alloc's `boxed/convert.rs`) fail to resolve under every spelling, while single-candidate methods skip refinement and work. This is the out-of-module half of model-checking#3773 (whose fix and `multiple_inherent_impls.rs` test cover the same-module rendering). It adds a fallback that unwraps the `<impl SELF_TYPE>` form, extracts SELF_TYPE's generic arguments, strips the disambiguation parentheses `def_path_str` adds around trait-object bounds (tuple-type parentheses are semantic and preserved), and retries the comparison. Scope: this keeps the existing string-comparison approach and only unblocks the out-of-module rendering; the milder same-module symptom (concrete turbofish arguments not matching a structured self-type such as `MaybeUninit<u32>` vs the impl's `MaybeUninit<T>` — the generic-parameter spelling works there) is unchanged, and a semantic-resolution rewrite would subsume both. Two smaller spelling asymmetries are also known and left to that same follow-up: a trait-object bound nested inside another generic argument still requires def_path_str's parenthesized spelling (normalization is not recursive), and same-module dyn-argument candidates still require it too (the primary comparison does no paren normalization). Happy to take direction if the deeper rewrite is preferred. Tests: eight unit tests in the existing `simple_last_two_items_of_path_match` module (dyn-args match + mismatch, dyn in second argument position, tuple parens preserved, non-generic no-fallback, fn-pointer renderings decline cleanly, arrow-bearing lists skip normalization, spaced turbofish matches on the primary path) and a new end-to-end regression test `tests/kani/FunctionContracts/cross_module_multiple_impls.rs` with tuple and trait-object candidate pairs (fails to resolve without the fix, verifies with it; the dyn pair fails if the paren-strip is disabled). Also validated on the motivating case: all three `Box<dyn Any…>::downcast_unchecked` contracts in verify-rust-std resolve and verify as `proof_for_contract` targets under the patched resolver. Applies cleanly on current `main` (`last_two_items_of_path_match` is unchanged there). One call-out: candidates whose rendered path contains `->` (fn-pointer / `Fn`-sugar types) are not unwrapped by the fallback — the top-level `::` split already leaves such paths unmatchable, and the helpers additionally decline anything their bracket counting cannot parse — so these keep the existing failed-to-resolve behavior rather than matching a different candidate (unit-tested). Motivating case: model-checking/verify-rust-std#669 — the three `Box<dyn Any…>::downcast_unchecked` contract targets there. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>
@feliperodri: Following up here as requested above. Done: Our kani#4778 is now in the repo's pin, so the three One new wrinkle from the toolchain bump: I reported it as kani#4984 and filed a fix in kani#4985, and it reverts to |
This branch has not been deployed
2 participants
Towards #526. Solves Challenge 29: Safety of boxed.
Summary
unsafefunctionsproof_for_contract; the scalarassume_initby construction (const-fn limit; see Scope).Box::into_uniquewas removed fromstdupstream, so its harness is dropped.Tat primitive types,Globalallocator67 Kani harnesses, one
mod verifyper file, all passing at the current toolchain pin viascripts/run-kani.sh; purely additive across three files (boxed.rs,boxed/convert.rs,boxed/thin.rs). Counts: 10proof_for_contract, 108kani::cover, 6should_panic, 0kani::assume. Two Kani limitations this work surfaced were addressed upstream and authored here (kani#4778 merged, kani#4985 filed; see Upstream Kani contributions).Kani's check classes cover the challenge's UB list where a check exists: dangling or misaligned access via the
pointer_dereferenceclass, intrinsic misuse via the arithmetic-overflow and pointer-offset checks, invalid-value production via the typed-read checks. "Mutating immutable bytes" has no Kani check class (repo-wide tool scope, surfaced on #582; committee policy pending).The 9 unsafe functions
The four raw-pointer constructors (
from_raw,from_non_null, and their_invariants) verify withproof_for_contractat a sized instantiation, plus an unsized[u8]instantiation for the_inpair. The sliceassume_initverifies the same way; its target is spelled through the impl's generic parameters (Box::<[MaybeUninit<T>], A>::assume_init), since a concrete turbofish does not resolve against the impl's structured self type but the generic-parameter form does.The three
downcast_uncheckeds onBox<dyn Any (+ Send)(+ Sync), A>verify withproof_for_contract, the target again spelled through each impl's generic parameters (resolver fix in the Upstream note). Each#[requires]fixes the erased type withis::<T>(); each#[ensures]asserts pointer identity across the cast.The scalar
assume_initverifies by construction. The current toolchain makes it aconst fn, and a contract on aconst fnwith an ownedselffails const-evaluation (E0493) at this pin. Its harnesscheck_assume_init_u32runs the real body on a symbolic payload and asserts the postcondition (value read-back and pointer identity), with an in-code note. It reverts toproof_for_contractonce the fix lands and the pin bumps.The challenge table lists
<dyn Error>::downcast_uncheckedthree times, but no such method exists:impl dyn Errorexposes only the safedowncast. The three realdowncast_uncheckeds are onBox<dyn Any (+ Send)(+ Sync), A>, contracted here.Upstream Kani contributions
Both authored here:
proof_for_contracttarget whose impl block lives outside the type's module (the threedowncast_uncheckeds). Reported in kani#4777, fixed in kani#4778 (merged 2026-09-24, in this pin). This is what lets the three verify asproof_for_contract.const fnwith an ownedselffails const-evaluation (E0493), which blocksproof_for_contracton the scalarassume_init. Reported in kani#4984; the fix is kani#4985 (filed).The 46 safe functions
Most are heap round-trips (allocate, write, hand out a pointer, reconstruct); the harness checks that the value and its allocation return intact. A few carry a property verified on its own terms, and the
ThinBox/WithHeaderfamily is new work with noBoxanalog.new_in/try_new_*,write,into_boxed_slice,into_raw/into_non_null/leak,into_pin)Layout::arrayacceptsinto_array,from_slice,From<&str>,From<Box<str>>, bothTryFroms)into_arrayreturnsResult; both arms asserted. The spec'sTryFrom<Box<T>>row has no impl in the tree, so the two realTryFromsources stand in for it.downcastonBox<dyn Any…>anddyn Error…Drop,Default,CloneBox<str>clone: a fresh allocation for a non-empty string, the shared dangling pointer for an empty oneThinBox/WithHeadernew_unsize_zstproven with no assumptions on a slice-metadata instantiationTwo habits keep the proofs non-vacuous. Each input-bearing harness carries a
kani::coverconfirming it reaches the operation under test, and both arms are covered where a function has two reachable outcomes. No harness constrains inputs withkani::assume; every restriction is a visibleany_wheredomain. Panics are proven, not assumed away:should_panicharnesses send a panicking-drop sentinel throughBox<T>andBox<[T]>drop glue, and drive all four non-tryslice constructors pastisize::MAXinto the capacity-overflow guard.Scope: what this pin cannot reach
Three behaviors sit outside the model here, each noted in-code. Allocation never fails in Kani, so the
Errarm of everytry_new*is unreachable; those harnesses verify the success arm and mark the dead branch.new_unsize_zst'sdyn Anyform fails inside itsconst-allocated metadata block (a missingdrop_in_place::<dyn Any>and pointer-liveness checks on the const pointer), so that function is proven on its slice-metadata route. The lastWithHeaderlayout-overflow guard is reachable only by a near-isize::MAXtype, so no harness reaches it.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.