Summary
Rc::<T, A>::get_mut_unchecked's Kani contract encodes only that the pointee is writable, not the aliasing condition its documentation actually requires. The same gap applies to the Arc counterpart.
The contract added in #582 (library/alloc/src/rc.rs, around line 2065) is:
#[requires({
let inner = this.ptr.as_ptr();
let value = unsafe { &raw mut (*inner).value };
kani::mem::can_write(value)
})]The documented safety condition is stronger: no other Rc or Weak pointer to the same allocation may be dereferenced (or have a live reference derived from it) for the lifetime of the returned &mut T. can_write(value) is essentially always true given a valid &mut Rc, so the precondition does not constrain what the caller must prove — a caller that violates uniqueness still satisfies the contract.
Why it was not fixed in #582
Uniqueness / absence of aliasing is not expressible in Kani today — there is no predicate over the set of live references to an allocation. The author flags the limitation in a source comment above the contract:
// `can_write` models writable storage; aliasing, active borrows, and exact
// pointee-type obligations are caller guarantees beyond this contract model.
This is the same class of limitation the challenge itself already carves out under "Assumptions" (e.g. assume_init's initialization requirement), so it did not block the solution. Filing it so the gap is tracked rather than lost in a code comment.
Impact
The proof_for_contract harnesses for get_mut_unchecked are sound as written — the harnesses construct uniquely-owned Rcs, so they never exercise an aliasing violation. The limitation is that the contract is not usable as a caller obligation: if get_mut_unchecked is later used as a contract-based abstraction at call sites, satisfying its requires will not establish the safety property callers actually need.
Possible directions
- A Kani predicate for "this allocation has no other live reference" (likely needs borrow-tracking Kani does not have).
- An
Rc-specific weaker-but-real proxy, e.g. requiring strong_count == 1 && weak_count == 0. That is sufficient but not necessary, so it would over-constrain callers who legitimately hold aliases they never dereference — worth discussing whether over-constraining is preferable to the current near-vacuous precondition.
- Leave as-is and document the gap in the challenge's Assumptions section, so it is a recorded limitation rather than an apparent contract.
References
Summary
Rc::<T, A>::get_mut_unchecked's Kani contract encodes only that the pointee is writable, not the aliasing condition its documentation actually requires. The same gap applies to theArccounterpart.The contract added in #582 (
library/alloc/src/rc.rs, around line 2065) is:The documented safety condition is stronger: no other
RcorWeakpointer to the same allocation may be dereferenced (or have a live reference derived from it) for the lifetime of the returned&mut T.can_write(value)is essentially always true given a valid&mut Rc, so the precondition does not constrain what the caller must prove — a caller that violates uniqueness still satisfies the contract.Why it was not fixed in #582
Uniqueness / absence of aliasing is not expressible in Kani today — there is no predicate over the set of live references to an allocation. The author flags the limitation in a source comment above the contract:
This is the same class of limitation the challenge itself already carves out under "Assumptions" (e.g.
assume_init's initialization requirement), so it did not block the solution. Filing it so the gap is tracked rather than lost in a code comment.Impact
The
proof_for_contractharnesses forget_mut_uncheckedare sound as written — the harnesses construct uniquely-ownedRcs, so they never exercise an aliasing violation. The limitation is that the contract is not usable as a caller obligation: ifget_mut_uncheckedis later used as a contract-based abstraction at call sites, satisfying itsrequireswill not establish the safety property callers actually need.Possible directions
Rc-specific weaker-but-real proxy, e.g. requiringstrong_count == 1 && weak_count == 0. That is sufficient but not necessary, so it would over-constrain callers who legitimately hold aliases they never dereference — worth discussing whether over-constraining is preferable to the current near-vacuous precondition.References