Step-indexing, handled through the \emph{later modality} $\triangleright P$, plays a key role in many techniques for program verification. A key challenge in proofs is the \emph{later elimination problem}, i.e., turning $\triangleright P$ into $P$. Later elimination cannot be done unconditionally, and is traditionally linked one-to-one to the physical steps the program performs in the operational semantics, which often caused restrictions in proofs. Recently various techniques (\emph{flexible step indexing} and \emph{later credits}) have been proposed to remedy this restriction.

Unfortunately, there currently exist many variations of these techniques with different subsets of features and proof rules. Integrating these techniques into a domain-specific program logic also requires non-trivial proof engineering of the meta theory. In this paper we aim to consolidate this situation by introducing the new \emph{physical step modality}—a modular building block for step-indexing program logics. We demonstrate that our modality can be integrated into various projects in the Iris eco-system (Actris, RefinedRust, Perennial, Trillium) and both eases the proof engineering of the meta theory, and enables new and/or more concise proof rules that these projects previously did not support. All our results are mechanized in the Rocq prover.