prove: arch::pci (x86)

[Marsman1996]

The remaining code cannot be verified locally without a significantly larger dependency and ownership-modeling effort:

• IoMem::new calls KVirtArea::map_untracked_frames, whose verified API requires page-table ownership, root guards, metadata-region ownership, and locking guards. The existing IoMem API does not carry these tracked tokens, so they would need to be threaded through allocators, initialization code, and device drivers.
• The existing IoMem implementation targets the old VmIo interface. The current verified VmIo<P> trait requires explicit tracked ownership arguments, so the implementation and its callers need a new MMIO ownership model.
• The I/O-port allocator depends on id-alloc, bitvec, spin::Once, linker-defined section symbols, and cleanup through Drop. These dependencies currently lack the required Verus specifications.
• Verus also does not support some constructs used by the original code, including continue in for loops and Range::len() as an ExactSizeIterator provided method.

Completing the verification therefore requires either introducing trusted specifications for these external dependencies or performing a broader proof-only API migration that propagates ownership tokens beyond ostd/src/io. Both are outside the scope of a localized I/O proof change.