CompCert treats all registers the same, allocating an entire 64-bit pair for 32-bit values. This cuts the number of available registers in half and requires fix-up outside the formally verified compiler to comply with calling conventions. We introduce CompCert${}^p$, an extension to the CompCert compiler, which faithfully models register pairs, thereby reducing the TCB. We adapt the proofs for all CompCert-supported architectures and demonstrate that, despite a slight increase in compile time, CompCert${}^p$ generates code that is either smaller or comparable in size to that produced by the original CompCert.