Hardware-software contracts provide a principled abstraction for separating the concerns of hardware (hardware designers) and software (compiler writers). Recently, leakage contracts have emerged as a robust method for mitigating microarchitectural side-channel attacks. By formalizing the security guarantees provided by the hardware, these contracts enable software to be verified against a well-defined leakage model.

However, ensuring that a hardware implementation faithfully satisfies these contractual guarantees remains a critical challenge. Current approaches address this problem using post-hoc Register Transfer Level (RTL) verification, but such techniques are inherently limited by the scalability and efficiency bottlenecks of existing verification tools. Moreover, this approach places a significant burden on verification engineers, who must manually map high-level architectural leakage specifications to low-level RTL design — a complex, non-trivial, and error-prone process.

In this work, we argue that adherence to leakage contracts should be enforced modularly during the design phase. We introduce Latent, a hardware description language with a type system for reasoning about leakages. Instead of exposing snapshots of microarchitectural state, Latent characterizes leakage through histories of values exchanged across component interfaces. This formulation follows from the observation that microarchitectural state preserves and transforms different versions of prior inputs over time. A type in Latent summarizes both the data dependencies of a term and the dependencies that may influence its latency. Together, these summaries capture explicit, implicit, and timing channels uniformly. Component interfaces expose them as leakage specifications for exchanged values, from which the type system infers internal summaries compositionally.