prove: arch::pci (x86) & io

[Marsman1996]

• Add Verus specifications and proofs for x86 PCI configuration-space access.
• Model MMIO and PIO allocation, ownership, and recycling across the OSTD I/O APIs.
• Centralize external IdAlloc, x86 port-I/O, and little-endian integer specifications in vstd_extra::external.
• Replace the MMIO containment assumption with an explicit boot-window model connected to the concrete allocators by type invariants.

---

Maybe wait until the following PRs are merged:

• prove: id-alloc #742, which proves the id-alloc instead of adding assume

[Marsman1996]

Update ostd/src/io/io_port to 0.18.1 to solve the port overflow problem

[rikosellic]

OnceImpl is our own definition of Once. Is it able to assume the specification for Once? It is a bit tricky because you may need to add a Tracked object to indicate whether an Once has been created.

[Marsman1996]

OnceImpl::new is verified and its tracked initialization state is stored internally, so the static initializer can derive IO_MEM_ALLOCATOR.wf() from its specification without an additional Tracked creation token.