Verify VecDeque (Challenge 25): contracts on the 13 unsafe fns and unbounded proofs for the 30 safe fns

Contracts (`safety::{requires, ensures}` + `kani::modifies`) with
`proof_for_contract` harnesses on the 13 unsafe functions of the
challenge plus `rotate_left_inner`/`rotate_right_inner`, and
`#[kani::proof]` harnesses on the 30 safe abstractions. Every harness
starts from `any_deque()`: a real allocation of symbolic capacity, a
symbolic head over every valid physical index and a symbolic length,
so no proof depends on a length constant or an unwind bound (the only
`#[kani::unwind]`s are in `verify::bounded_evidence`, which checks the
stubs, the `write_iter` transcription and the slice drop glue bounded).
Generic `T` is covered by representative element shapes over every
property the code observes (`size_of`/`align_of`, `IS_ZST`, validity
invariant, `needs_drop`).

Review items of 2026-09-13: representative shapes with the properties
they cover (shape matrix in the module doc); the shipped `for_each`
statement of `write_iter` compiled under Kani byte for byte as
`write_iter_for_each` and checked bounded against the same contract;
each stub's evidence harness in the stub table.

Rebased onto main at cd371e0 (toolchain nightly-2026-09-25, Kani
1640445, CBMC 6.11.0): contracts and harnesses adapted to the
`WrappedIndex` buffer offsets, `into_raw_parts_with_allocator`, and
upstream's new `debug_assert!` in `from_contiguous_raw_parts_in`
(the contract's clause). At this pin: `stub_verified(write_iter)`
compiles but never terminates for sized elements (the generated
replacement havocs the slice `modifies` target element by element), so
the hand-written replacement stays and `write_iter`'s ensures gains the
`size_hint` lower bound; `WithDrop`'s destructor no longer writes a
static (a `CountedDrop` counts destructors for the bounded drop-glue
evidence); `try_reserve*` harnesses exclude requests CBMC's object
model cannot represent; and `buffer_read`/`pop_front` carry no
validity-invariant shape (`bool` and `NonZero<u8>` make CBMC run out of
memory nondeterministically on exactly those two targets).

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MqLN2C9EzETaAMVsU7XsoC

Author: jrey8343