arXiv CSopen access

A Deductive System for Contract Satisfaction Proofs

Unknown · 2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

cryptography, security, privacy, cybersecurity

A Deductive System for Contract Satisfaction Proofs Extended Version

arXiv:2604.09165v1 [cs.PL] 10 Apr 2026

ARTHUR CORRENSON, CISPA Helmholtz Center for Information Security, Germany HAOYI ZENG, Harvard University, USA JANA HOFMANN, Max Planck Institute for Security and Privacy (MPI-SP), Germany Hardware-software contracts are abstract specifications of a CPU’s leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without having to explicitly reason about the microarchitectural details of the CPU. Using the abstraction powers of a contract requires proving that the targeted CPU satisfies the contract in the sense that the contract over-approximates the CPU’s leakage. Besides pen-and-paper reasoning, proving contract satisfaction has been approached mostly from the model-checking perspective, with approaches based on a (semi-)automated search for the necessary invariants. As an alternative, this paper explores how such proofs can be conducted in interactive proof assistants. We start by observing that contract satisfaction is an instance of a more general problem we call relative trace equality, and we introduce relative bisimulation as an associated proof technique. Leveraging recent advances in the field of coinductive proofs, we develop a deductive proof system for relative trace equality. Our system is provably sound and complete, and it enables a modular and incremental proof style. It also features several reasoning principles to simplify proofs by exploiting symmetries and transitivity properties. We formalized our deductive system in the Rocq proof assistant and applied it to two challenging contract satisfaction proofs. CCS Concepts: • Theory of computation → Logic and verification; • Security and privacy → Security in hardware; Information flow control.

Introduction

When multiple parties perform computations on shared hardware (e.g., in cloud computing), potentially secret data leaks into the microarchitecture and can be observed by other parties hosted on the same machine. The effectiveness of such side-channel attacks has been impressively demonstrated by the Meltdown [26] and Spectre [25] attacks and the many exploits that followed [5, 11, 37, 41–43, 45]. Since disabling the sharing of resources is not an option for performance reasons, a lot of work has been invested on how to defend against such attacks. Hardware-Software Contracts. Developing low-impact software defenses requires a precise specification of the hardware’s leakage behavior. Hardware-software contracts address this need by formally characterizing leakage at the level of the instruction set architecture (ISA). This enables software developers to assess a program’s leakage without requiring deep knowledge of the microarchitectural details. For this approach to be correct, the contract needs to soundly over-approximate the leakage of the microarchitecture. This property, called contract satisfaction, is usually expressed as follows [20]: For any program 𝑃 and two inputs 𝜎, 𝜎 ′ , if the contract predicts the same leakage when running 𝑃 on 𝜎 and 𝜎 ′ , then the two runs are also indistinguishable on the hardware. We make this contract satisfaction property more formal in Section 2. For now, note that the property is relational, i.e., a hyperproperty, as it reasons about two contract traces and two hardware traces. In this paper, we develop a deductive system dedicated to proving relational properties of this form.

Authors’ Contact Information: Arthur Correnson, CISPA Helmholtz Center for Information Security, Saarbruecken, Germany, [email protected]; Haoyi Zeng, Harvard University, Cambridge, MA, USA, [email protected]; Jana Hofmann, Max Planck Institute for Security and Privacy (MPI-SP), Bochum, Germany, [email protected].

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

The Challenges of Proving Contract Satisfaction. So far, the task of validating that a given microarchitecture satisfies a contract has been tackled using testing [17, 21, 29, 30] and model checking [16, 39, 47]. Such automated techniques are often very effective, but they rely on the correctness of the underlying algorithms and their implementations. There also exist some rigorous pen-andpaper proofs of contract satisfaction, but their complexity and length make them difficult to verify. As an example, the technical report of the paper proposing hardware-software contracts provides a contract satisfaction proof for a simple processor featuring speculation and out-of-order execution. The corresponding pen-and-paper proof consists of 25 dense pages [20]. To achieve an additional level of formality, we set ourselves the goal of developing contract satisfaction proofs inside a proof assistant (Rocq, in our case). This is challenging, as it involves 4-ary relational reasoning between execution traces induced by two different semantics. Additionally, executions progress asynchronously (one contract execution step can correspond to several hardware steps and vice-versa), and relational invariants need to account for these potential misalignments. Existing Approaches. The challenges induced by this kind of 4-ary reasoning are not specific to hardware-software contracts. Similar issues arise whenever the security of two different systems is put in relation, for example, in relative security [15], information-preserving refinement [3, 4], and secure compilation [1, 2, 6, 8, 32, 35, 44]. Proof techniques for such properties typically require guessing sophisticated witnesses up-front, often some form of simulation relation. In secure compilation, for example, a common technique defines three simulation relations: one between source states, one between target states, and one bridging the first two. This results in a threedimensional simulation diagram justifying that equality of observations at the source level implies equality of observations at the target level [1, 2, 6, 8, 35]. Coming up with such relations requires a deep understanding of the studied compiler. In the context of hardware-software contracts, there is no compiler between the high-level (the contract) and the low-level (the hardware). Instead, both sides execute the same program, expressed in the same ISA, but under two different semantics. In this specific setting, a more direct approach seems to be possible, one that constructs a single 4-ary relation on the fly during the proof. Our Approach. In this paper, we build such a proof technique for contract satisfaction. Specifically, we first observe that contract satisfaction is an instance of what we call relative trace equality, i.e., properties of the form “trace equality implies trace equality”. We then propose relative bisimulation as a sound and complete technique to prove relative trace equality. Building on this definition, we present a deductive system for relative bisimulation proofs. Contrary to existing approaches, our system does not require providing simulation relations up-front. Instead, it takes advantage of recent advances in the field of coinductive proofs to construct invariants incrementally during the proof. To deal with the asynchronicity of the problem, our system supports non-lockstep reasoning via natural alternations of coinductive and inductive reasoning phases. We formalized our deductive system in Rocq and formally proved it sound and complete for relative trace equality. As a case study, we used our system to validate two standard contracts against two simple hardware models: an “always-mispredict” contract to reason about speculative execution of branches, and a “sequential” contract for out-of-order execution. Finally, we showed that our system supports several so-called up-to techniques that exploit symmetry and transitivity properties that can simplify proofs. Structure of the Paper. The rest of the paper is structured as follows. Section 2 gives an overview of microarchitectural side channels and hardware-software contracts. Section 3 introduces the notion of proof by relative bisimulation, together with an associated deductive system. Section 4 demonstrates how to use our deductive system to validate two different hardware-software

A Deductive System for Contract Satisfaction Proofs

contracts. Finally, Section 5 presents several up-to techniques that can be soundly integrated into our deductive system. 2

Hardware-Software Contracts

Before introducing our proof technique, we recall the basics of microarchitectural side channels, noninterference, and hardware-software contracts. 2.1

Microarchitectural Side Channels

Computations performed on CPUs leave traces in the microarchitecture, e.g., in caches, buffers, and in the internal state of branch predictors. When several parties share microarchitectural components, one party can observe the microarchitectural changes generated by the others by using a so-called side channel. If these changes depend on secret data, this constitute a critical information leakage. In a cache-based side-channel attack, for example, the attacker can learn which addresses have been accessed by the victim (just the address, not the value stored at it). If the addresses depend on secrets, the attacker might be able to deduce the value of secret data. 2.2

Noninterference and Contract Satisfaction

Noninterference establishes that the observations an attacker can make are independent of the secrets. Let 𝑃 be a program and (𝜎, 𝜇) be a CPU state composed of an architectural part 𝜎, and a microarchitectural part 𝜇. We write 𝜎 =pub 𝜎 ′ to denote that two architectural states agree on their public values (but might disagree on their secrets). Let furthermore ⟦𝑃⟧ H (𝜎, 𝜇) denote the microarchitectural observations an attacker can make through a cache-based side channel when 𝑃 is executed with initial architectural state 𝜎 and microarchitectural state 𝜇. ⟦𝑃⟧ H (𝜎, 𝜇) is a (potentially infinite) trace typically defined in terms of a labeled operational semantics of the hardware. The program 𝑃 is noninterferent on the modeled CPU if ∀𝜎, 𝜎 ′, 𝜇. 𝜎 =pub 𝜎 ′ ⇒ ⟦𝑃⟧ H (𝜎, 𝜇) = ⟦𝑃⟧ H (𝜎 ′, 𝜇) To establish that a program is noninterferent, we have to reason about the microarchitectural behavior of the specific hardware it is run on. This requires deep knowledge of both the program and the microarchitecture. To split that task between hardware and software engineers, hardwaresoftware contracts have been introduced as an abstraction layer between the two [20]. Contracts are formal models of the expected side-channel leakage of a CPU. They are defined in terms of the instruction set architecture (ISA) and thus abstract away the behavior of the microarchitecture. We write ⟦𝑃⟧ C (𝜎) for the leakage predicted by a contract C when running 𝑃 on 𝜎. As for the hardware, ⟦𝑃⟧ C (𝜎) is a trace defined by a labeled operational semantics. Contracts let us split the noninterference property into two parts. The first property establishes that a hardware satisfies a contract. Definition 1 (Contract Satisfaction [20, 29]). A hardware semantics ⟦−⟧ H satisfies a contract ⟦−⟧ C if ∀𝑃, 𝜎, 𝜎 ′, 𝜇. ⟦𝑃⟧ C (𝜎) = ⟦𝑃⟧ C (𝜎 ′ ) ⇒ ⟦𝑃⟧ H (𝜎, 𝜇) = ⟦𝑃⟧ H (𝜎 ′, 𝜇) The second property establishes that a program is noninterferent w.r.t. a specific contract. Definition 2 ([20]). A program 𝑃 is noninterferent with respect to contract ⟦−⟧ C if ∀𝜎, 𝜎 ′ . 𝜎 =pub 𝜎 ′ ⇒ ⟦𝑃⟧ C (𝜎) = ⟦𝑃⟧ C (𝜎 ′ ) With these definitions, if a CPU with semantics ⟦−⟧ H satisfies a contract ⟦−⟧ C , and 𝑃 is noninterferent w.r.t. ⟦−⟧ C , then 𝑃 is also noninterferent on ⟦−⟧ H . The other direction does not generally hold, since ⟦−⟧ C usually over-approximates the leakage of ⟦−⟧ H . This split into two properties makes reasoning

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

𝜎 (x < |A|)

1 2 3 4 5

if ( x y = z = else : b =

𝜎

l. 1

< | A |) : A [ x ]; B [ y ];

𝜎′

l. 1

A [ a ];

𝜎, 𝜇

l. 1

𝜎 ′, 𝜇

l. 1

𝜎5 (a) l. 5

𝜎2 (x) l. 2

𝜎5′ (a)

𝜎 ′ (x < |A|) l. 5

𝜎3 (A[x]) 𝜎3′ (A[x])

𝜎2′ (x) l. 2

l. 2

𝜎3 (A[x])·𝜎2 (x)·c

l. 2

...

l. 3

𝜎3′ (A[x])·𝜎2′ (x)·c

𝜎2′ (x)·c

...

l. 3

𝜎2 (x)·c

...

l. 3

...

Fig. 1. Program vulnerable to Spectre and potential contract (above) and hardware traces (below). The nodes indicate the line being executed next. The labels correspond to the leakage. 𝜎 and 𝜎 ′ are two initial architectural states, 𝜇 is the initial microarchitectural state, and 𝑐 is the initial cache. 𝜎2 ( ′ ), 𝜎3 ( ′ ), and 𝜎5 ( ′ ) are the states after executing lines 2, 3, and 5, respectively. We assume that the branch condition evaluates to true and that the hardware predicts the correct branch in state 𝜇.

about noninterference a lot more convenient: Definition 1 lets us reason about the leakage of a CPU without worrying about concrete programs and their secrets. Definition 2 lets us reason about the leakages of a program without worrying about the concrete hardware semantics and its microarchitecture. In this paper, we focus on the contract satisfaction property given in Definition 1. We define a deductive system to prove that a given hardware semantics satisfies a contract. 2.3

Example: Always-Mispredict Contract

The goal of developing a deductive system for contract satisfaction proofs was inspired by the dense pen-and-paper proofs that accompany the paper that first introduced this form of contracts [20]. The contracts developed in this paper use the always-mispredict feature for modeling Spectre-style branch misprediction and speculative execution [19]. We later use this feature to demonstrate the usage of our deductive system, so we introduce the intuition behind it. Branch Misprediction. Modern processors have a branch predictor, which predicts the outcome of branching decisions. If the result of evaluating the branch condition is not available yet, the CPU will speculatively execute the predicted branch and potentially roll back to the correct branch when the branch condition has finished evaluating. The architectural effects of speculative execution are fully rolled back, meaning that speculation does not impact functional correctness. Microarchitectural effects, however, cannot be rolled back. As a result, inadvertently executed branches might leak secrets into the microarchitecture. The program on the left in Figure 1 is a typical example demonstrating Spectre-style attacks. The program first checks if x is within the bounds of an array A. If yes, it loads from A at index x. With branch misprediction, it might happen that the if-branch is executed even if x is not within the bounds of A. Then, a value from somewhere in the memory is loaded and stored in y. This value, potentially a secret, is subsequently used as an address and thus leaked into the cache. Always-Mispredict Technique. The always-mispredict technique [19] (used in the CT-SPEC contract in [20]) abstracts away the microarchitectural branch predictor and instead always executes both branches. Figure 1 depicts exemplary traces generated by a contract using the alwaysmispredict technique (upper box, in blue) and a hardware semantics that speculates on branching decisions (lower box, in red). The four traces are obtained from Definition 1 when considering the program given on the left and two initial architectural states 𝜎 and 𝜎 ′ and initial microarchitectural

A Deductive System for Contract Satisfaction Proofs

state 𝜇. The leakage labels of the contract traces follow the constant-time principle, exposing the (correct) result of branching conditions and the addresses of memory accesses. The hardware traces expose the current cache. For this example, we assume that the branch condition evaluates to true in both 𝜎 and 𝜎 ′ . Still, the contract also executes the wrong branch for a fixed number of steps to simulate a potential misprediction. The hardware traces, on the other hand, do not mispredict in microarchitectural state 𝜇. Importantly, the effects of the contract misprediction on the architectural states are reverted after executing 𝑙 .5 on the wrong branch, and both the contract and the hardware traces are synchronized again at line 𝑙 .2 in the same states 𝜎2 and 𝜎2′ . From this point on, the leakage associated with each of the four executions depends on the evaluation of a, x, and A[x] in the successive states. Since the states coincide on the contract and the hardware sides, if the contract traces agree on the value of x and A[x], the hardware traces are also equal. Thus, Definition 1 would be satisfied. Correctness of the Always-Mispredict Technique. Intuitively, any hardware speculating solely on branching outcomes should indeed satisfy the contract, as the always-mispredict contract only exposes “more” information if the hardware does not mispredict. Proving contract satisfaction according to Definition 1 is challenging, though. We need to keep track of four different traces. Two traces of the same type always progress in lockstep, but operate on different inputs 𝜎, 𝜎 ′ . The contract and hardware traces, on the other hand, may proceed at different speeds and produce different observation labels. Especially the former constitutes a challenge in formal proofs, as we cannot just perform a simple induction on the length of one of the contract traces. The setting calls for a simulation-style proof, but this requires finding suitable invariants across the four traces. In the following, we present a proof system that addresses these challenges by combining coinductive and inductive reasoning. We will come back to the always-mispredict technique in Section 4, where we will give a formal semantics for a small ISA and prove the technique correct. 3

Proving Contract Satisfaction by Relative Bisimulation

In this section, we present a new technique to formally prove contract satisfaction as defined in Definition 1. We first emphasize that contract satisfaction is an instance of the more general problem of proving statements of the form “trace equality implies trace equality”. We refer to this problem as relative trace equality. We then show that relative trace equality is fully characterized by a 4-ary variant of bisimilarity which we call relative bisimilarity. Building on relative bisimilarity, we develop a sound-and-complete deductive system to prove relative trace equality. This system offers simple reasoning principles for establishing equality of traces between two states while exploiting the assumption that two other states are trace-equal. 3.1

The Challenges of Trace-Based Reasoning

If we omit assumptions on initial states for a moment, proving contract satisfaction essentially boils down to proving statements of the form ⟦𝑃⟧ C (𝑠 1 ) = ⟦𝑃⟧ C (𝑠 2 ) =⇒ ⟦𝑃⟧ H (ℎ 1 ) = ⟦𝑃⟧ H (ℎ 2 ), where 𝑠 1, 𝑠 2 are two contract states and ℎ 1, ℎ 2 are two hardware states. Executing 𝑃 from the contract states 𝑠 1, 𝑠 2 and the hardware states ℎ 1, ℎ 2 leads to four executions: cobs1

cobs1′

cobs1′′

cobs2

cobs2′

cobs2′′

𝑠 1 −−−→ C 𝑠 1′ −−−→ C 𝑠 1′′ −−−−→ C . . . 𝑠 2 −−−→ C 𝑠 2′ −−−→ C 𝑠 2′′ −−−−→ C . . .

hobs1

hobs1′

hobs1′′

hobs2

hobs2′

hobs2′′

ℎ 1 −−−−→ H ℎ 1′ −−−−→ H ℎ 1′′ −−−−→ H . . . ℎ 2 −−−−→ H ℎ 2′ −−−−→ H ℎ 2′′ −−−−→ H . . .

where → − C and → − H are the small-step operational semantics defining the contract and the hardware model. Hardware labels hobs are used to model microarchitectural information an attacker can observe during executions. Contract labels cobs are architectural approximations of what is

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

leaked to attackers. The four sequences of observations define the following traces: ⟦𝑃⟧ C (𝑠 1 ) = cobs1 cobs1′ cobs1′′ . . .

⟦𝑃⟧ H (ℎ 1 ) = hobs1 hobs1′ hobs1′′ . . .

⟦𝑃⟧ C (𝑠 2 ) = cobs2 cobs2′ cobs2′′ . . .

⟦𝑃⟧ H (ℎ 2 ) = hobs2 hobs2′ hobs2′′ . . .

We want to prove that, assuming the two contract traces are equal, the hardware traces are also equal (i.e., the contract correctly over-approximates the leakage): cobs1 cobs1′ cobs1′′ . . . = cobs2 cobs2′ cobs2′′ . . . =⇒ hobs1 hobs1′ hobs1′′ . . . = hobs2 hobs2′ hobs2′′ . . . If contract traces were guaranteed to be finite and of equal length, we could reason by induction on the length of the two contract traces. Unfortunately, depending on the program 𝑃 and the states 𝑠 1, 𝑠 2 , the executions might be of different lengths. They are not even guaranteed to both be finite as the same program 𝑃 might diverge from a state 𝑠 1 and terminate from another state 𝑠 2 . If both traces are of infinite length, we cannot employ induction anyway as infinite traces are not inductive objects. The exact same problems arise for hardware traces. 3.2

Relative Trace Equality Between Transition Systems

We propose a general solution to the problem of proving relative trace equality, i.e., statements of the form “trace equality implies trace equality“. We do not commit to a specific notion of contract or hardware semantics. Instead, we treat both the contract and the hardware model as arbitrary deterministic and non-terminating state transition systems equipped with an infinite trace semantics. Definition 3 (Transition Systems). A transition system T is a tuple (𝑆, Σ, next, leak), where 𝑆 is a set of states, Σ is a set of observations, next : 𝑆 → 𝑆 is a transition function, and leak : 𝑆 → Σ is a leakage function. Definition 4 (Infinite Traces). Given a transition system T = (𝑆, Σ, next, leak), and a state 𝑠 ∈ 𝑆, we denote by ⟦𝑠⟧ T ∈ Σ𝜔 the (unique) infinite leakage trace starting in 𝑠 ⟦𝑠⟧ T ≜ leak(𝑠) leak(next (𝑠)) leak(next 2 (𝑠)) . . . We note that assuming determinism is in line with previous work on hardware-software contracts [20, 21, 28, 46, 47]. We discuss this assumption and how to potentially lift it in Section 6. We also note that considering only non-terminating systems (and thus only infinite traces) does not result in any loss of generality, as terminating programs can be straightforwardly modeled in the infinite-trace setting by making terminating states self-loop forever. In fact, this approach offers more flexibility: it enables controlling whether non-termination is observable or not simply by choosing the labeling of terminal self-loops adequately. We omit the details here, which are quite standard, but we refer the curious readers to our Rocq development for a full formalization of the encoding(s) of termination in the infinite-trace setting (including proofs of correctness). We note that contract satisfaction (Definition 1) can easily be stated in our transition system formalism. Indeed, let 𝑃 be a program expressed in some ISA, and let TC𝑃 = (𝑆 𝑃C , Σ𝑃C , next 𝑃C , leak𝑃C ) and TH𝑃 = (𝑆 𝑃H , Σ𝑃H , next 𝑃H , leak𝑃H ) be two transition systems representing a machine executing 𝑃 cobs

by following some contract semantics and hardware semantics, respectively (e.g., if 𝑠 −−−→ C 𝑠 ′ , then next 𝑃C (𝑠) = 𝑠 ′ and leak𝑃C (𝑠) = cobs, etc). Then, proving contract satisfaction means proving the following implication ∀𝑃, 𝜎, 𝜎 ′, 𝜇. ⟦𝜎⟧ T 𝑃 = ⟦𝜎 ′ ⟧ T 𝑃 =⇒ ⟦(𝜎, 𝜇)⟧ T 𝑃 = ⟦(𝜎 ′, 𝜇)⟧ T 𝑃 C

A Deductive System for Contract Satisfaction Proofs

3.3

A State-Based Proof Technique: Relative Bisimulation

For the remainder of the section, let two transition systems C = (𝑆 C , Σ C , next C , leak C ) (playing the role of a contract) and H = (𝑆 H , Σ H , next H , leak H ) (playing the role of a hardware model) be given, and let 𝑠 1, 𝑠 2 ∈ 𝑆 C and ℎ 1, ℎ 2 ∈ 𝑆 H be four states. In the remainder of the paper, we often refer to 𝑠 1 and 𝑠 2 as the “contract states”, and ℎ 1 and ℎ 2 as the “hardware states” for convenience. We want to obtain a technique to prove statements of the form ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H Ideally, to avoid the issues mentioned in Section 3.1, the technique should be state-based rather than trace-based. In the remainder of this subsection, we develop such a state-based proof technique as an extension of the standard bisimulation method for proving trace equality. Fixpoints and (Co)Induction. Before introducing our proof technique, we quickly re-iterate over the necessary basics of fixpoints and their connection to proofs by (co)induction. Let 𝑈 be a set, and let 𝐹 : P (𝑈 ) → P (𝑈 ) be a function from subsets of 𝑈 to subsets of 𝑈 . A subset 𝑋 ⊆ 𝑈 is called a fixpoint of 𝐹 if 𝑋 = 𝐹 (𝑋 ). A famous result due to Tarski [40] guarantees that if 𝐹 is monotone (i.e., ∀𝑋, 𝑌 . 𝑋 ⊆ 𝑌 ⇒ 𝐹 (𝑋 ) ⊆ 𝐹 (𝑌 )), then it has a unique greatest fixpoint (noted 𝜈𝐹 ) and a unique least fixpoint (noted 𝜇𝐹 ). Further, least fixpoints come associated with a complete proof principle to show inclusions of the form 𝜇𝐹 ⊆ 𝑋 (induction). Dually, greatest fixpoints enjoy a complete proof principle for inclusions of the form 𝑋 ⊆ 𝜈𝐹 (coinduction). Theorem 5 (Fixpoint Induction and Coinduction). (Induction)

𝜇𝐹 ⊆ 𝑋 ⇐⇒ ∃𝐼 . 𝐼 ⊆ 𝑋 ∧ 𝐹 (𝐼 ) ⊆ 𝐼

(Coinduction) 𝑋 ⊆ 𝜈𝐹 ⇐⇒ ∃𝐼 . 𝑋 ⊆ 𝐼 ∧ 𝐼 ⊆ 𝐹 (𝐼 ) Coinduction and induction can be seen as methods to prove inclusions by “exhibiting an invariant". For example, coinduction can be informally spelled out as follows: to prove that elements of 𝑋 satisfy a property defined as a greatest fixpoint (i.e., 𝑋 ⊆ 𝜈𝐹 ), it suffices to find an “invariant” 𝐼 which holds initially (i.e., 𝑋 ⊆ 𝐼 ), and which is preserved over one 𝐹 -step (i.e., 𝐼 ⊆ 𝐹 (𝐼 )). 𝐼 is usually called a coinduction hypothesis. Bisimulation Proofs. Bisimulation is a standard state-based technique to prove that two states of a transition system generate the same traces (e.g., ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H ). Intuitively, given a transition system T = (𝑆, Σ, next, leak), two states 𝑠 1, 𝑠 2 ∈ 𝑆 are said to be bisimilar if they have the same immediate observations (i.e., leak(𝑠 1 ) = leak(𝑠 2 )) and their successors are again bisimilar. More formally, the bisimilarity relation bisim ⊆ 𝑆 × 𝑆 is defined as a greatest fixpoint. Definition 6 (Bisimilarity). bisim ≜ 𝜈bisimF where bisimF(𝑅) ≜ { (𝑠 1, 𝑠 2 ) | leak(𝑠 1 ) = leak(𝑠 2 ) ∧ (next (𝑠 1 ), next (𝑠 2 )) ∈ 𝑅 } An important result is that bisimilarity is equivalent to trace equality. Theorem 7 (Bisimilarity is Trace Equality). (𝑠 1, 𝑠 2 ) ∈ bisim ⇐⇒ ⟦𝑠 1 ⟧ T = ⟦𝑠 2 ⟧ T Further, since bisim is defined as a greatest fixpoint, one can prove bisimilarity by coinduction. In particular, to prove that two states 𝑠 1 and 𝑠 2 are bisimilar, it suffices to find a relation 𝑅 (usually called a bisimulation) which contains (𝑠 1, 𝑠 2 ) and satisfies 𝑅 ⊆ bisimF(𝑅). This process can be thought of as proving trace equality by exhibiting a suitable relational invariant. Theorem 8 (Proofs by Bisimulation). ⟦𝑠 1 ⟧ T = ⟦𝑠 2 ⟧ T ⇐⇒ ∃𝑅.(𝑠 1, 𝑠 2 ) ∈ 𝑅 ∧ 𝑅 ⊆ bisimF(𝑅)

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

Remember that we aim to prove implications ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H . Omitting the assumption ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C , we could in principle prove ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H by bisimulation. Unfortunately, in the context of contract satisfaction, this equality does not hold by itself: we need to exploit the assumption ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C . Bisimulation alone is therefore not a suitable technique. Relative Bisimilarity. To prove trace equality under a trace equality assumption, we generalize the standard binary notion of bisimilarity to a 4-ary relative bisimilarity relation. Let 𝑠 1, 𝑠 2 ∈ 𝑆 C and ℎ 1, ℎ 2 ∈ 𝑆 H be four states. To prove that ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C implies ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H in a bisimulation-flavored way, the most straightforward approach would be to process the traces generated by the 4 states in lockstep, checking that local equality of leakage on the left implies local equality of leakage on the right. Following this intuition, we say that 𝑠 1, 𝑠 2, ℎ 1, ℎ 2 are lockstep relatively bisimilar if either leak C (𝑠 1 ) ≠ leak C (𝑠 2 ), or if leak H (ℎ 1 ) = leak H (ℎ 2 ) and next C (𝑠 1 ), next C (𝑠 2 ), next H (ℎ 1 ), next H (ℎ 2 ) are again lockstep relatively bisimilar. Lockstep relative bisimilarity is again defined as a greatest fixpoint. Definition 9 (Lockstep Relative Bisimilarity). rbisimlockstep ≜ 𝜈rbisimFlockstep where rbisimFlockstep (𝑅) ≜ (Leak)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | leak C (𝑠 1 ) ≠ leak C (𝑠 2 ) } ∪

(Step)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | leak H (ℎ 1 ) = leak H (ℎ 2 ) ∧ (next C (𝑠 1 ), next C (𝑠 2 ), next H (ℎ 1 ), next H (ℎ 2 )) ∈ 𝑅 }

It is not difficult to see that lockstep relative bisimilarity is a sound approximation of relative trace equality: if four states are lockstep relatively bisimilar, they also satisfy relative trace equality. Theorem 10. (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ rbisimlockstep =⇒ (⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H ) Unfortunately the reverse implication does not hold: rbisimlockstep is not a complete characterization of relative trace equality. As a counterexample, consider the following scenario where obsA, obsB, obsC, obsD, obsE are 5 distinct observations: obsA

obsB

ℎ 1 −−−→ . . .

obsA

obsC

ℎ 2 −−−→ . . .

𝑠 1 −−−→ 𝑠 1′ −−−→ . . . 𝑠 2 −−−→ 𝑠 2′ −−−→ . . .

obsD obsE

Since obsB ≠ obsC, the trace of 𝑠 1 is different from the trace of 𝑠 2 and relative trace equality trivially holds for 𝑠 1, 𝑠 2, ℎ 1, ℎ 2 . However, the four states are not relatively bisimilar according to bisimlockstep because neither leak(𝑠 1 ) ≠ leak(𝑠 2 ) nor leak(ℎ 1 ) = leak(ℎ 2 ). Here, the problem comes from the lockstep nature of bisimlockstep . Concretely, we would like to be allowed to "skip" steps on the left-hand side, independently of the right-hand side. In the previous example, this would have allowed us to fast-forward to the “contract states” 𝑠 1′ , 𝑠 2′ , and then exploit the inequality obsB ≠ obsC without having to prove anything about the “hardware states” in between. Such examples where we need non-lockstep arguments abound in practice, particularly in the context of contract satisfaction. To support non-lockstep arguments, a naive idea would be to slightly update the definition of rbisimlockstep to decouple “contract steps” and “hardware steps”. For example, we could relax the

A Deductive System for Contract Satisfaction Proofs

definition of rbisimlockstep as follows: rbisimrelaxed ≜ 𝜈rbisimFrelaxed rbisimFrelaxed (𝑅) ≜ (C-Leak)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | leak C (𝑠 1 ) ≠ leak C (𝑠 2 ) } ∪

(C-Step)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (next C (𝑠 1 ), next C (𝑠 2 ), ℎ 1, ℎ 2 ) ∈ 𝑅 } ∪

(H-Step)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | leak H (ℎ 1 ) = leak H (ℎ 2 ) ∧ (𝑠 1, 𝑠 2, next H (ℎ 1 ), next H (ℎ 2 )) ∈ 𝑅 }

The addition of the disjunct (C-Step) lets us skip contract execution steps, as we wanted. In particular, the following implication now holds by definition (next C (𝑠 1 ), next C (𝑠 2 ), ℎ 1, ℎ 2 ) ∈ rbisimrelaxed =⇒ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ rbisimrelaxed Unfortunately, with this naive modification, rbisimrelaxed is no longer sound for relative trace equality. The problem is that considering the greatest fixpoint of rbisimFrelaxed gives an overly permissive notion of relative bisimilarity: it enables proving that a relation 𝑅 is a (relaxed) relative bisimulation via (C-Step) without ever proving anything useful about relative trace equality (i.e., without providing evidences that ⟦𝑠 1 ⟧ C ≠ ⟦𝑠 2 ⟧ C , nor evidences that ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H ). In fact, any quadruple of states vacuously satisfies rbisimrelaxed . Indeed, let ⊤ = 𝑆 C ×𝑆 C ×𝑆 H ×𝑆 H be the set of all quadruple of states. Using (C-Step), we can trivially prove ⊤ ⊆ bisimFrelaxed (⊤). By coinduction, it follows that ⊤ ⊆ rbisimrelaxed (i.e., all quadruples of states are relatively bisimilar according to the relaxed definition). To achieve soundness while preserving support for non-lockstep reasoning, the solution is to employ an alternation of greatest and least fixpoint, as demonstrated by the following definition. Definition 11 (Relative Bisimilarity). rbisim ≜ 𝜈𝑅1 . rbisimF(𝑅1 ) where rbisimF(𝑅1 ) ≜ 𝜇𝑅2 . (C-Leak)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | leak C (𝑠 1 ) ≠ leak C (𝑠 2 ) } ∪

(C-Step)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (next C (𝑠 1 ), next C (𝑠 2 ), ℎ 1, ℎ 2 ) ∈ 𝑅2 } ∪

(H-Step)

{ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | leak H (ℎ 1 ) = leak H (ℎ 2 ) ∧ (𝑠 1, 𝑠 2, next H (ℎ 1 ), next H (ℎ 2 )) ∈ 𝑅1 }

This definition closely resembles the definition of rbisimrelaxed , except that contract steps are now treated inductively instead of coinductively. The resulting notion of (non-lockstep) relative bisimilarity turns out to exactly coincide with relative trace equality. Theorem 12 (Relative Bisimilarity is Relative Trace Equality). (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ rbisim ⇐⇒ (⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H ) Proof. (Soundness =⇒ ). Since bisimilarity implies trace equality (Theorem 7), it suffices to prove (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ rbisim =⇒ (⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ (ℎ 1, ℎ 2 ) ∈ bisim). The proof proceeds by coinduction on bisim, and by induction on the inductive part of rbisim. (Completeness ⇐= ). We proceed by case distinction and first suppose ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C . By assumption it follows that ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H . Proving (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ rbisim now degenerates into a standard bisimulation proof between ℎ 1 and ℎ 2 using only (H-Step) and ignoring 𝑠 1 and 𝑠 2 . For the other case, let ⟦𝑠 1 ⟧ C ≠ ⟦𝑠 2 ⟧ C , so there must exist some 𝑛 ∈ N such that next𝑛C (𝑠 1 ) ≠ next𝑛C (𝑠 2 ). Under this assumption, we can prove (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ rbisim by induction on 𝑛 (using (Leak) in the base case and (C-Step) in the inductive case). □ As a consequence of Theorem 12, we obtain a sound and complete invariant-based technique to prove relative trace equality. Indeed, since rbisim is defined as a greatest fixpoint, we can prove

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

relative bisimilarity (and hence relative trace equality) by coinduction: it suffices to find a relation 𝑅 containing the four initial states and satisfying 𝑅 ⊆ rbisimF(𝑅). Theorem 13 (Proofs by Relative Bisimulation). (⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H ) ⇔ ∃𝑅. (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ 𝑅 ∧ 𝑅 ⊆ rbisimF(𝑅) Weak Relative Bisimilarity. Our final definition of relative bisimilarity (rbisim) enables a form of non-lockstep reasoning where “contract steps” can be decoupled from “hardware steps”. However, the two contract states are progressing in locksteps, and so are the two hardware states. This is required in our setting, because we work with a strong notion of trace equality where equality between observations must hold at each step. However, it is sometimes useful to consider a relaxed setting where some of the computation steps emit so-called tau events (noted 𝜏), indicating that no observation is produced. In this case, traces are only required to be equal up to removal of 𝜏’s (usually called weak trace equality), and non-lockstep reasoning between the two contract states (or the two hardware states) becomes a particularly useful feature to skip silent steps and realign states as needed. It is well-know that bisimilarity can be weakened to support weak trace equality. Similarly, we can adapt relative bisimilarity to support weak relative trace equality (i.e., weak trace equality implies weak trace equality). Concretely, we can define a relation weak_rbisim which enables skipping 𝜏-labeled steps from any of the four states without changing the other three. For the purpose of clarity, and since recent works on hardware-software contracts did not make use of 𝜏 labels, the rest of the paper also sticks to the strict setting without 𝜏’s. We refer the curious readers to our Rocq development for the definition and the soundness proof of weak_rbisim. We leave the completeness proof as future work. 3.4

A Deductive System for Relative Bisimilarity

As stated in Theorem 13, relative bisimilarity provides a sound and complete state-based technique to prove relative trace equality. Still, finding a suitable relational invariant (call it 𝑅) and checking that it is indeed a relative bisimulation (i.e., 𝑅 ⊆ rbisimF(𝑅)) can be tedious. Instead, we propose a simple deductive system to prove relative bisimilarity. Our deductive system is based on parameterized coinduction [23], and enables a modular and incremental proof style that progressively builds a relative bisimulation rather than having to provide it up-front. Parameterized Coinduction. Parameterized coinduction (Paco) was introduced by Hur et al. [23] as a technique to simplify proofs by coinduction in interactive proof assistants. The key idea is to replace predicates defined as greatest fixpoints 𝜈𝐹 by parameterized predicates 𝐺 𝐹 (𝐼 ) ≜ 𝜈𝑋 . 𝐹 (𝑋 ∪𝐼 ) where 𝐼 can be thought of as a coinduction hypothesis “in construction”. By definition it is clear that 𝐺 𝐹 (∅) = 𝜈𝐹 , which means that proving 𝑋 ⊆ 𝜈𝐹 is equivalent to proving 𝑋 ⊆ 𝐺 𝐹 (∅). The benefit of replacing 𝜈𝐹 with 𝐺 𝐹 (∅) is that it supports useful rules to construct an invariant incrementally. In particular, the following three rules can be derived from the definition of 𝐺 𝐹 (𝐼 ) [23]. Paco-Init

Paco-Step

Paco-Accumulate

𝑋 ⊆ 𝐺 𝐹 (∅)

𝑋 ⊆ 𝐹 (𝐼 ∪ 𝐺 𝐹 (𝐼 ))

𝑋 ⊆ 𝐺 𝐹 (𝐼 ∪ 𝑋 )

𝑋 ⊆ 𝜈𝐹

𝑋 ⊆ 𝐺 𝐹 (𝐼 )

When proving a statement of the form 𝑋 ⊆ 𝜈𝐹 , instead of directly using standard coinduction (which requires guessing 𝐼 ⊇ 𝑋 such that 𝐼 ⊆ 𝐹 (𝐼 )), we can use Paco-Init to prove 𝑋 ⊆ 𝐺 𝐹 (∅) instead. From there, we use the rules Paco-Step and Paco-Accumulate to progressively enlarge the parameter 𝐼 until it is big enough to directly prove 𝑋 ⊆ 𝐹 (𝐼 ) using Paco-Step. In the context of a proof by bisimulation (i.e., when 𝐹 = bisimF), this intuitively corresponds to starting with an empty bisimulation, and following transitions (using Paco-Step) while accumulating pairs of states

A Deductive System for Contract Satisfaction Proofs

(using Paco-Accumulate) until we obtain a valid bisimulation relation. Importantly, not all states need to be accumulated. In many cases, the parameter 𝐼 does not need to be a full bisimulation relation to conclude a proof, but rather a small fragment of a bisimulation. In extreme cases, it even suffices to accumulate a single pair of states to justify the existence of a bisimulation. Proof Quintuples. Remember that relative bisimilarity is defined as a greatest fixpoint rbisim = 𝜈𝑅. rbisimF(𝑅). This means we can already use the rules of Paco to prove relative trace equality (just take 𝐹 = rbisimF). To simplify notations, we avoid referring to 𝐺 bisimF directly, and instead introduce the following proof quintuples to denote the possible states of a proof. Definition 14 (Proof Quintuples). Let 𝐹 ≜ rbisimF. We define 𝑠1 ℎ1 𝑠1 ℎ1 𝑅 ⊢ ≜ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ 𝐺 𝐹 (𝑅) ≜ (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ (𝑅 ∪ 𝐺 𝐹 (𝑅)) 𝑅 ⊢ 𝑠2 ℎ2 𝑠2 ℎ2 The quintuple with a solid box corresponds to a state of a proof “before a Paco step”, and a dashed box corresponds to a state “after a Paco step”. After using Paco-Step, the current coinduction hypothesis 𝑅 can be used to conclude the proof. For this reason, we often refer to 𝑅 as a guarded hypothesis and 𝑅 as an unguarded hypothesis. This notation (and naming convention) is borrowed from recent works on parameterized coinduction [12–14]. Directly using the rules of Paco is still not very helpful though: the rules would be formulated in terms of rbisimF, which hides an inner least fixpoint that users still have to handle manually. Instead, we specialize the rules of Paco to obtain reasoning principles that are specific to relative bisimilarity. In particular, we formulate our reasoning rules in terms of atomic contract steps and hardware steps. Theorem 15 (Core Reasoning Rules of Proof Quintuples). Quintuples admit the following rules: H-Step C-Step

next C (𝑠 1 ) ℎ 1 𝑅 ⊢ next C (𝑠 2 ) ℎ 2 𝑠 ℎ1 𝑅 ⊢ 1 𝑠2 ℎ2

C-Leak

leak C (𝑠 1 ) ≠ leak C (𝑠 2 ) 𝑠 ℎ1 𝑅 ⊢ 1 𝑠2 ℎ2

leak H (ℎ 1 ) = leak H (ℎ 2) 𝑠 next H (ℎ 1 ) 𝑅 ⊢ 1 𝑠 2 next H (ℎ 2 ) 𝑠 ℎ1 𝑅 ⊢ 1 𝑠2 ℎ2

Invariant

(𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ 𝑅 ′ ′ 𝑠 𝑅 ∪ 𝑅 ⊢ 1′ 𝑠2 𝑠 ℎ1 𝑅 ⊢ 1 𝑠2 ℎ2

∀(𝑠 1′ , 𝑠 2′ , ℎ 1′ , ℎ 2′ ) ∈ 𝑅 ′ .

′

ℎ 1′ ℎ 2′

Cycle

(𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ 𝑅 𝑠1 ℎ1 𝑅 ⊢ 𝑠2 ℎ2

Guard

𝑠 𝑅 ⊢ 1 𝑠2 𝑠 𝑅 ⊢ 1 𝑠2

ℎ1 ℎ2

Step Rules. The three rules C-Leak, C-Step and H-Step are derived from Paco-Step and correspond to the three disjuncts with the same names in the definition of relative bisimilarity (Definition 11). On the contract side, the rule C-Leak enables concluding a proof whenever the two contract states have different observations (leak C (𝑠 1 ) ≠ leak C (𝑠 2 )), and the the rule C-Step just skips one contract execution step. On the hardware side, the rule H-Step requires proving that leak H (ℎ 1 ) = leak H (ℎ 2 ), and in exchange it replaces the current hardware states by their successors. Note that H-Step releases the guard of 𝑅, while C-Step does not. This asymmetry stems from the fact that hardware steps are treated coinductively, while contract steps are treated inductively within the definition of rbisim. Since we want to prove ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H , this

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

difference makes sense: taking a hardware step makes progress towards proving ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H , while taking a contract step just “unrolls” the assumption ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C . Cycle and Guard Rules. Whenever the guard around the hypothesis is released (i.e., after using the rule H-Step), we can use the rule Cycle to immediately conclude a proof if the four current states are already contained in 𝑅. If not, we restore the guard using the rule Guard, and we need to keep going (either by taking more steps, or by extending the hypothesis using Invariant). Invariant Rule. The last rule is the Invariant rule, which is derived from Paco-Accumulate. It is used to enlarge the current hypothesis by “guessing” a relational invariant. More precisely, if the current states (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) satisfy a relation 𝑅 ′ , we can replace the current hypothesis 𝑅 with 𝑅 ∪ 𝑅 ′ . In exchange, we then need to prove a quintuple for all states in 𝑅 ′ , not just the current states. We will be able to exploit this new hypothesis via the Cycle rule if we re-encounter states satisfying 𝑅 ′ later on. Enhanced C-Step Rule. We note that C-Step and C-Leak can be combined into a convenient third rule to simultaneously skip a contract step and assume equality of (contract) leakage: C-Step’

next C (𝑠 1 ) leak C (𝑠 1 ) = leak C (𝑠 2 ) =⇒ 𝑅 ⊢ next C (𝑠 2 ) 𝑠 ℎ1 𝑅 ⊢ 1 𝑠2 ℎ2

ℎ1 ℎ2

In practice, we use this rule instead of C-Step because we typically need to exploit the assumption leak C (𝑠 1 ) = leak C (𝑠 2 ) right after a contract step. Soundness and Completeness of Quintuples. By definition, quintuples with an empty hypothesis are equivalent to relative bisimilarity, and hence equivalent to relative trace equality. 𝑠1 ℎ1 Theorem 16. ∅ ⊢ ⇐⇒ (⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H ) 𝑠2 ℎ2 A result that is a little less obvious is that the six proof rules of Theorem 15 constitute a complete deductive system for relative trace equality. Theorem 17 Suppose that (⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H ), then we can (Completeness). 𝑠1 ℎ1 prove ∅ ⊢ using only the rules C-Leak, C-Step, H-Step, Invariant, Cycle, and Guard. 𝑠2 ℎ2 Proof. Suppose ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H . By Theorem 13, it follows that (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ rbisim, and we can use rbisim itself as an invariant via the Invariant rule. The rest of the proof proceeds by induction on the inductive part of rbisim. The three cases ((C-Leak), (C-Step), and (H-Step)) are covered using the three rules with the same names. The case of (C-Step) is concluded by induction. The case of (H-Step) is concluded by Cycle. □ 4 Case Study We used the proof system presented in Section 3.4 to formally prove two of the most important ideas underlying the CT-SPEC contract, which was developed for a hardware model that features branch speculation and out-of-order execution [20]. The first idea is to abstract away the branch predictor by employing a contract which always starts by mispredicting (as described in Section 2). The second idea is to abstract away the out-of-order execution of instructions by employing a contract which executes instructions sequentially. Our formalization of both abstractions use a

A Deductive System for Contract Satisfaction Proofs

simpler ISA and hardware semantics as opposed to [20], but they contain the key features that make CT-SPEC such a useful abstraction. We present the first example, the always-mispredict abstraction, in detail and give a short overview of the second example. A more detailed description of the out-of-order example can be found in the appendix in Section B. 4.1

A Small ISA

We formulate a small toy ISA that consists of three instructions that manipulate two registers, and can load from memory. We omit stores for this example, as they behave just as loads from a leakage point of view. For similar reasons, we ignore expressions other than addition. Registers Constants Locations Instructions Programs

𝑥 𝑘 𝑙 𝑖 𝑝

∈ ∈ ∈ := :=

{𝑟 1, 𝑟 2 } Z N load 𝑥 1, 𝑥 2 | add 𝑥 1, 𝑥 2, 𝑘 | beqz 𝑥, 𝑙 𝑖 | 𝑝1; 𝑝2

An architectural state 𝜎 = (𝑚, 𝑎, pc) consists a memory 𝑚 : N → Z, a register assignment 𝑎 : {𝑟 1, 𝑟 2 } → Z, and a program counter pc : N. Technically, the program 𝑃 is also part of the architectural state, but we keep 𝑃 a global variable in the semantics. The hardware state 𝑠 = (𝜎, 𝑐) adds to the architectural state a cache 𝑐, storing the recently accessed addresses. The vanilla architectural and hardware semantics implement the expected behavior. To simplify the presentation of subsequent examples, the semantics are given as a base relation describing the effect on the state when executing a single instruction. The full semantics are given in the appendix in Section A. As an example, the two rules for loads are the following: LoadHW

LoadArch

𝑣 = 𝑚(𝑎(𝑥 2 ))

(𝜎, load 𝑥 1, 𝑥 2 ) ⇒isa 𝜎 ′

(𝑚, 𝑎, pc, load 𝑥 1, 𝑥 2 ) ⇒isa (𝑚, 𝑎[𝑥 1 ↦→ 𝑣], pc + 1)

(𝜎, 𝑐, load 𝑥 1, 𝑥 2 ) ⇒ H (𝜎 ′, 𝑎(𝑥 2 ) ::𝑐)

Apart from state transformations, the hardware semantics also models a cache-based attacker by adding observation labels to the semantics. In this case, the attacker can observe the contents of the cache at any time, so we expose it in every step. For readability, we omitted from the semantics the fact that values, when used as addresses in the Load rules, are truncated to 0 if they are negative. 4.2

Speculation and Always-Mispredict Contract

Speculating Hardware Semantics. We now come back to our example from Section 2.3 and formalize a speculating hardware semantics and an always-mispredict contract. We extend the vanilla hardware semantics with speculative execution in Figure 2. The microarchitecture now contains a branch predictor Φ : N → {jump, next}, which predicts the outcome of a branching decision based on the current program counter. This function is used as a global variable as it does not change during execution. It could easily be extended with a local state to model training of the predictor. We use 𝑠.pc, 𝑠.𝑐, and 𝑠.𝑎 to access the components of the hardware state. We now also assume that a program 𝑃 is being executed, compared to before, where we only executed a single instruction. We write 𝑃 (𝑠.pc) to access the instruction that the program counter points to. The hardware now keeps track of a speculation window 𝜔 ∈ N ∪ {∞} and a checkpoint pair cp. When not in speculation, 𝜔 = ∞ and cp = ⊥. Upon reaching a branching instruction (rules Branch Next and Branch Jump), we initialize the speculation window with a constant 𝑤. The checkpoint serves as an oracle that will be queried after 𝑤 steps to check if the prediction was correct (Boolean tag b) and where to rollback to (state 𝜎𝑏 ) if the prediction was wrong. This is implemented in rules Rollback and Commit and models the fact that the hardware only learns later if the branching

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

Rollback 𝑠 ′ = (𝜎𝑏 , 𝑠.𝑐)

Commit

s.c

(𝑠, 0, (false, 𝜎𝑏 )) −−→ H (𝑠 ′, ∞, ⊥)

(𝑠, 0, (true, 𝜎𝑏 )) −−→ H (𝑠, ∞, ⊥)

Step cp ≠ ⊥ ∨ 𝑃 (𝑠.pc) ≠ beqz ·, ·

(𝑠, 𝑃 (𝑠.pc)) ⇒ H 𝑠 ′

(𝑠, 𝜔 + 1, cp) → − H (𝑠 ′, 𝜔, cp) Branch Next 𝑃 (𝑠.pc) = beqz 𝑥, 𝑙

Φ(𝑠.pc) = next

(𝑠, beqz 𝑥, 𝑙) ⇒ H (𝜎 ′, _)

b = 𝜎 ′ .pc = 𝑠.pc + 1 ?

s.c

(𝑠, ∞, ⊥) −−→ H (𝑠 [𝑝𝑐 ↦→ 𝑠.pc + 1], 𝑤, (b, 𝜎 ′ )) Branch jump 𝑃 (𝑠.pc) = beqz 𝑥, 𝑙

Φ(𝑠.pc) = jump

(𝑠, beqz 𝑥, 𝑙) ⇒ H (𝜎 ′, _)

b = 𝜎 ′ .pc = 𝑙 ?

s.c

(𝑠, ∞, ⊥) −−→ H (𝑠 [𝑝𝑐 ↦→ 𝑙], 𝑤, (b, 𝜎 ′ )) Fig. 2. Hardware semantics with a branch predictor Φ.

Step  𝜎.a(x2 )     o = 𝜎.a(x) =? 0   ⊥ 

if 𝑃 (𝜎.pc) = load 𝑥 1, 𝑥 2 𝜎𝑏 ≠ ⊥ ∨ 𝑃 (𝜎.pc) ≠ beqz ·, ·

if 𝑃 (𝜎.pc) = beqz 𝑥, 𝑙 otherwise

(𝜎, 𝑃 (𝜎.pc)) ⇒isa 𝜎 ′

(𝜎, 𝜔 + 1, 𝜎𝑏 ) → − C (𝜎 ′, 𝜔, 𝜎𝑏 ) Rollback (𝜎, 0, 𝜎𝑏 ) → − C (𝜎𝑏 , ∞, ⊥)

Branch 𝑃 (𝜎.pc) = beqz 𝑥, 𝑙

(𝜎, beqz 𝑥, 𝑙) ⇒isa 𝜎 ′

pc ⊥ = (𝑎(𝑥) = 0) ? (pc + 1) : 𝑙

𝜎 .a(x ) = 0

(𝜎, ∞, ⊥) −−−−−−−→ C (𝜎 [𝑝𝑐 ↦→ pc ⊥ ], 𝑤, 𝜎 ′ ) Fig. 3. Always-mispredict contract.

decision was correct. Our semantics does not allow nested speculation (this is further discussed in Section 6). Always-Mispredict Contract. We adapt the always-mispredict technique described in Section 2.3 to our example with the contract given in Figure 3. Whenever the contract executes a load, the address of the load is exposed as an observation label. Similar to the speculating hardware semantics, the contract uses a speculation window 𝜔 and a rollback state 𝜎𝑏 . Differently, the contract gets immediate access to the correct branch. This enables it to always first execute the wrong branch before returning to the correct one. Following the CT-SPEC contract, we also expose what the correct branching decision would be, which is an adoption of the constant-time model. We note that even though all our semantics are presented in a small-step relational style for clarity, they can equivalently be stated in a functional style by defining separately two functions next 𝑜 𝑜 and leak: for a small-step labeled relation 𝑠 → − 𝑠 ′ , we have 𝑠 → − 𝑠 ′ ⇐⇒ 𝑠 ′ = next (𝑠) ∧ 𝑜 = leak(𝑠).

A Deductive System for Contract Satisfaction Proofs

4.3

Proof of the Always-Mispredict Contract

We use our proof system to formally prove that the always-mispredict contract is satisfied by our simplified model of a speculating CPU. More precisely, for any program 𝑃, for any initial memories and register assignments 𝑚 1, 𝑚 2, 𝑎 1, 𝑎 2 , for any initial cache 𝑐, and for any initial program counter pc, we prove the following statement: ⟦𝑃⟧ C ((𝑚 1, 𝑎 1, pc), ∞, ⊥) = ⟦((𝑚 2, 𝑎 2, pc), ∞, ⊥)⟧ C =⇒ ⟦𝑃⟧ H ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥) = ⟦𝑃⟧ H ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥) By the soundness of our proof system (Theorem 16), it suffices to instead prove ((𝑚 1, 𝑎 1, pc), ∞, ⊥) ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥) ∅ ⊢ ((𝑚 2, 𝑎 2, pc), ∞, ⊥) ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥) We will use all quadruples of states of this exact form as an invariant. We define 𝐼 ≜ { all ((𝑚 1, 𝑎 1, pc), ∞, ⊥), ((𝑚 2, 𝑎 2, pc), ∞, ⊥), ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥), ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥) } and we use the Invariant rule to obtain 𝐼 as a (guarded) hypothesis. ((𝑚 1, 𝑎 1, pc), ∞, ⊥) ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥) 𝐼 ⊢ ((𝑚 2, 𝑎 2, pc), ∞, ⊥) ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥) We note that when using the deductive system in Rocq, we do not have to explicitly write down the definition of 𝐼 (because it just consists of all states of the same form as the one currently being in focus). From there, we can start making progress by inspecting possible execution steps. We perform a case analysis on the instruction 𝑃 (pc) currently being executed. The cases of add and load are very similar, but load is slightly more involved because loading an address modifies the microarchitectural state. We therefore only detail the case of load. Supposing 𝑃 (pc) = load 𝑥 1, 𝑥 2 , we start by applying the rule C-Step. Importantly, this enables us to assume that the leakage is the same for both contract states. By definition of the always-mispredict contract, loads leak the loaded address, so we get to assume 𝑎 1 (𝑥 2 ) = 𝑎 2 (𝑥 2 ). ((𝑚 1, 𝑎 1, pc), ∞, ⊥) ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥) 𝐼 ⊢ ((𝑚 2, 𝑎 2, pc), ∞, ⊥) ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥) (C-Step’) Suppose 𝑎 1 (𝑥 2 ) = 𝑎 2 (𝑥 2 ) = adr (1) ((𝑚 1, 𝑎 1 [𝑥 1 ↦→ 𝑚 1 (adr)], pc + 1), ∞, ⊥) ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥) 𝐼 ⊢ ((𝑚 2, 𝑎 2 [𝑥 1 ↦→ 𝑚 2 (adr)], pc + 1), ∞, ⊥) ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥) Now, we can use the rule H-Step to get access to the hypothesis 𝐼 . To do so, we have to prove that the leakage is the same for both hardware states. Here the content of the cache is leaked, which is not a problem because we started from the same cache 𝑐 in both hardware states. Further, the contract guarantees that the loaded addresses must be the same address adr (assumption (1)), so the content of the cache remains the same in both hardware states even after loading. Therefore, the invariant 𝐼 is restored after executing the load, and we can conclude using Cycle. (H-Step) 𝑐 = 𝑐 ∧ ((𝑚 1, 𝑎 1 [. . .], pc + 1), ∞, ⊥) ((𝑚 1, 𝑎 1 [𝑥 1 ↦→ 𝑚 1 (𝑎 1 (𝑥 2 ))], pc, 𝑎 1 (𝑥 2 ) ::𝑐), ∞, ⊥) 𝐼 ⊢ ((𝑚 2, 𝑎 2 [. . .], pc + 1), ∞, ⊥) ((𝑚 2, 𝑎 2 [𝑥 1 ↦→ 𝑚 2 (𝑎 2 (𝑥 2 ))], pc, 𝑎 2 (𝑥 2 ) ::𝑐), ∞, ⊥) ((𝑚 1, 𝑎 1 [. . .], pc + 1), ∞, ⊥) ((𝑚 1, 𝑎 1 [𝑥 1 ↦→ 𝑚 1 (adr)], pc, adr ::𝑐), ∞, ⊥) (By (1)) 𝐼 ⊢ ((𝑚 2, 𝑎 2 [. . .], pc + 1), ∞, ⊥) ((𝑚 2, 𝑎 2 [𝑥 1 ↦→ 𝑚 2 (adr)], pc, adr ::𝑐), ∞, ⊥) (Cycle) ((. . . , ∞, ⊥), (. . . , ∞, ⊥), ((. . . , adr ::𝑐), ∞, ⊥), ((. . . , adr ::𝑐), ∞, ⊥)) ∈ 𝐼

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

Next, we cover the case where 𝑃 (pc) = beqz 𝑥, 𝑙. This is the most interesting case since we have to reason about the different ways in which the CPU might speculate. We first take a contract step. ((𝑚 1, 𝑎 1, pc), ∞, ⊥) ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥) 𝐼 ⊢ ((𝑚 2, 𝑎 2, pc), ∞, ⊥) ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥) ?

(C-Step’)

Suppose (𝑎 1 (𝑥) = 0) = (𝑎 2 (𝑥) = 0) (2) ((𝑚 1, 𝑎 1, pc ⊥ ), 𝑤, (𝑚 1, 𝑎 1, pc ⊤ )) ((𝑚 1, 𝑎 1, pc, 𝑐), ∞, ⊥) 𝐼 ⊢ ((𝑚 2, 𝑎 2, pc ⊥ ), 𝑤, (𝑚 1, 𝑎 2, pc ⊤ )) ((𝑚 2, 𝑎 2, pc, 𝑐), ∞, ⊥)

In this step, the always-mispredict contract jumps to the incorrect location first, saves the correct future state, and reveals the positivity of the register 𝑥. In particular, we get to assume ? ? that (𝑎 1 (𝑥) = 0) = (𝑎 2 (𝑥) = 0). Thanks to this assumption, we can also deduce that the two contract states jump to the same (incorrect) location. Importantly, the two contract states are then in speculation mode for 𝑤 steps, where 𝑤 is the maximal speculation window. We now have to reason about what happens on the hardware side: the branch predictor will be queried, resulting in a jump to either the correct or the incorrect next location. Since our branch predictor depends only on the program counter, both hardware states will jump to the same (correct or incorrect) location. We denote the correct and the incorrect locations after executing beqz 𝑥, 𝑙 with pc ⊤ and pc ⊥ . The easier case is when the hardware, as the contract, also mispredicts. In this case, both the contract and the hardware side are then temporarily executing the same (incorrect) code. Therefore, 𝑤 steps of straightforward lockstep reasoning are sufficient to skip-through the misprediction, re-establish the invariant 𝐼 , and conclude. The more challenging case is when the hardware correctly predicts the outcome of the branch. Contrary to the previous cases, this one critically requires non-lockstep reasoning as the contract and the hardware are temporarily executing different instructions. Starting from the configuration where the two contract states are positioned at the same incorrect location, the two hardware states jump to the same correct location after using H-Step. (. . . , 𝑤, (𝑚 1, 𝑎 1, pc ⊤ )) ((𝑚 1, 𝑎 1, pc ⊤, 𝑐), 𝑤, (true, (𝑚 1, 𝑎 1, pc ⊥ ))) (H-step + (2)) 𝐼 ⊢ (. . . , 𝑤, (𝑚 2, 𝑎 2, pc ⊤ )) ((𝑚 2, 𝑎 2, pc ⊤, 𝑐), 𝑤, (true, (𝑚 2, 𝑎 2, pc ⊥ ))) Because the contract leaked the positivity of the register (assumption (2)), we know that the speculation will eventually be resolved in the same way for both hardware states (in particular, the flag is set to true in both). From there, we exploit the asynchronicity of our proof system to skip through 𝑤 steps on the contract side. After these 𝑤 steps, the two contract states roll back. ((𝑚 1, 𝑎 1, pc ⊤ ), ∞, ⊥) ((𝑚 1, 𝑎 1, pc ⊤, 𝑐), 𝑤, (true, (𝑚 1, 𝑎 1, pc ⊥ ))) (𝑤 times C-Step) 𝐼 ⊢ ((𝑚 2, 𝑎 2, pc ⊤ ), ∞, ⊥) ((𝑚 2, 𝑎 2, pc ⊤, 𝑐), 𝑤, (true, (𝑚 2, 𝑎 2, pc ⊥ ))) Finally, since both the contract and the hardware side are now re-aligned at the same program counter, we can conclude by 𝑤 − 1 steps of lockstep reasoning, followed by an asynchronous hardware step to finalize the resolution of the speculation and restore the relational invariant. ((𝑚 1′ , 𝑎 1′ , pc ′ ), ∞, ⊥) ((𝑚 1′ , 𝑎 1′ , pc ′, 𝑐 ′ ), 0, (true, (𝑚 1, 𝑎 1, pc ⊥ ))) ((𝑚 2′ , 𝑎 2′ , pc ′ ), ∞, ⊥) ((𝑚 2′ , 𝑎 2′ , pc ′, 𝑐 ′ ), 0, (true, (𝑚 2, 𝑎 2, pc ⊥ ))) ((𝑚 1′ , 𝑎 1′ , pc ′ ), ∞, ⊥) ((𝑚 1′ , 𝑎 1′ , pc ′, 𝑐 ′ ), ∞, ⊥) 𝐼 ⊢ ((𝑚 2′ , 𝑎 2′ , pc ′ ), ∞, ⊥) ((𝑚 2′ , 𝑎 2′ , pc ′, 𝑐 ′ ), ∞, ⊥) ((. . . , ∞, ⊥) (. . . , ∞, ⊥) (. . . , ∞, ⊥) (. . . , ∞, ⊥)) ∈ 𝐼

(𝑤 − 1 steps) (H-Step) (Cycle)

𝐼 ⊢

A Deductive System for Contract Satisfaction Proofs

We note that the first 𝑤 steps actually hide a bit of non-lockstep reasoning to cover the case of branches. Indeed, even though the hardware states cannot do nested speculation during these 𝑤 steps, the contract states still can. In that case it suffices to, again, skip through the misspeculation by repeated application of C-Step. In Rocq, these redundant phases of the proof can be conveniently factored as lemmas, and composed as needed. Indeed, the compositional nature of parameterized coinduction allows to prove a quintuple once, and reuse it in the derivation of another quintuple. 4.4

Proof of the Sequential Contract

Another key idea in the CT-SPEC contract is to abstract away the fact that modern processors execute instructions out-of-order and instead use a sequential execution semantics. To validate the correctness of this abstraction, we add simple out-of-order execution to our CPU model. Hardware Semantics and Contract. We enrich the vanilla hardware semantics with a one-instruction buffer. Concretely, hardware states are pairs (𝑠, 𝑏), where 𝑠 is a vanilla hardware state, and 𝑏 is a buffer which can either be empty (𝑏 = ⊥) or contain one instruction. When the buffer is empty, instead of executing the current instruction at 𝑠.pc (call it 𝑖 1 ), the CPU can decide to instead store 𝑖 1 in the buffer and execute the instruction at 𝑠.pc + 1 first (call it 𝑖 2 ). Importantly, not all instructions can be executed out-of-order without affecting the semantics of the executed programs. We define a predicate delayable(𝑖 1, 𝑖 2 ) to describe when 𝑖 1 can be safely delayed. We note that branches are not delayable (i.e., delayable((beqz·, ·), 𝑖 2 ) is false regardless of 𝑖 2 ). When the buffer is full, the instruction in the buffer is immediately executed, leaving the buffer empty again. On the contract side, the semantics is straightforward: contract states are composed of an architectural state 𝜎, and instructions are executed sequentially by following the ISA semantics. The predicted leakage is the same as for the always-mispredict contract (loads leak the loaded address, and branches leak the result of the branch condition). Contract Satisfaction Proof. We prove contract satisfaction by deriving the following quintuple, which requires initial states to have the same pc, cache, and buffer: ∅ ⊢

(𝑚 1, 𝑎 1, pc) (𝑚 2, 𝑎 2, pc)

((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥)

As in the previous example, we use all quadruples of states with this exact form as an invariant: 𝐼 ≜ { all ((𝑚 1, 𝑎 1, pc), (𝑚 2, 𝑎 2, pc), ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥), ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥)) } After fixing 𝐼 as a guarded hypothesis using the Invariant rule, we first do a case analysis on whether the execution of the current instruction is delayed or not. If not, the contract and the hardware proceeds in lockstep. The interesting case is when an instruction is delayed. In this case, the contract executes the instruction at pc first, while the hardware executes the instruction at pc + 1 first. In the proof, we therefore first use the rule C-Step’ twice in order to pre-shot the leakage of the next two execution steps. We can then use H-Step twice to simulate the execution of the instruction at pc + 1 followed by the instruction in the buffer. After this, the buffer is empty and the invariant is restored, enabling us to conclude the proof by Cycle. Justifying the equality of hardware leakage after each H-Step and proving that the invariant is ultimately restored relies on two additional observations: (1) swapping two delayable instructions preserves the leakage allowed by the contract, and (2) swapping the execution of delayable instructions preserves the semantics. These two properties are proven as separate lemmas about the delayable predicate.

5 5.1

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

Up-To Techniques for Relative Bisimilarity Exploiting Symmetries and Transitivity in Relative Bisimulation Proofs

During a relative trace equality proof, it can be useful to replace one of the four states with another one in order to simplify the proof or to avoid redundant reasoning. For example, when proving ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H , we can always replace the contract state 𝑠 1 (resp. 𝑠 2 ) with another contract state 𝑠 1′ (resp. 𝑠 2′ ) such that ⟦𝑠𝑖 ⟧ C = ⟦𝑠𝑖′ ⟧ C . Similarly, by symmetry of equality, we can always swap 𝑠 1 and 𝑠 2 , or ℎ 1 and ℎ 2 . More subtly, we can also exploit transitivity of implication to split proofs. For example, if we have to prove ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H , and if we additionally know that ⟦𝑠 1 ⟧ C = ⟦𝑠 2 ⟧ C =⇒ ⟦𝑠 1′ ⟧ C = ⟦𝑠 2′ ⟧ C , we can instead prove ⟦𝑠 1′ ⟧ C = ⟦𝑠 2′ ⟧ C =⇒ ⟦ℎ 1 ⟧ H = ⟦ℎ 2 ⟧ H . Intuitively, this can be understood as replacing a pair of contract states with two states that “leak less”. Again, the same observations applies to hardware states (i.e., we can replace a pair of hardware states with two states that “leak more”). An interesting question is whether these tricks transfer to proof quintuples. Since quintuples with an empty hypothesis are equivalent to relative trace equality (Theorem 16), it is straightforward to reformulate the above observations as reasoning rules when the hypothesis is ∅. It is less obvious that such principles also apply mid-proof, i.e., when the guarded hypothesis is not empty. In fact, it not always the case! As an example, in the following figure, the rule on the left (which exploits transitivity to replace the hardware states with states that leak more) is easily proven sound, while its generalization on the right is unsound (we show why in Section 5.4). ′ ′ 𝑠 ℎ 1′ ℎ1 ℎ1 𝑠 1 ℎ 1′ ℎ1 ℎ1 ∅ ⊢ 1 ⊢ ⊢ ⊢ ∅ 𝑅 ∅ 𝑠 2 ℎ 2′ ℎ 2′ ℎ 2 𝑠 2 ℎ 2′ ℎ 2′ ℎ 2 𝑠 ℎ1 𝑠 ℎ1 ∅ ⊢ 1 𝑅 ⊢ 1 𝑠2 ℎ2 𝑠2 ℎ2 This is unfortunate, because applying these principles mid-proof can, in some cases, dramatically simplify proofs. In particular, using such rules when the hypothesis is unguarded would enable using the Cycle rule even if the current states are not exactly in the hypothesis 𝑅, but almost in it up to symmetries or up to transitivity. This would allow us to work with simpler relational invariants, and to better decompose proofs. 5.2

Compatible Up-To Techniques

In a standard proof by coinduction, we prove a statement 𝑋 ⊆ 𝜈𝐹 by identifying a coinduction hypothesis 𝐼 such that 𝑋 ⊆ 𝐼 and 𝐼 ⊆ 𝐹 (𝐼 ). Often, we find 𝐼 ’s such that the second condition is not satisfied (i.e., 𝐼 ⊈ 𝐹 (𝐼 )), but it would be satisfied if we were considering a slightly larger 𝐼 on the right. That is, for a certain function 𝑓 (which given a set, returns a larger set), we can easily prove 𝐼 ⊆ 𝐹 (𝑓 (𝐼 )). It turns out that for 𝑓 ’s that satisfy a certain compatibility criterion, reasoning up-to 𝑓 -enlargements of 𝐼 is sound! This gives a powerful reasoning principle often referred to as coinduction up-to 𝑓 [34]. Definition 18 (Compatibility). Let 𝑓 and 𝐹 be two monotone functions over subsets of a set 𝑈 . We say that 𝑓 is compatible with 𝐹 if ∀𝑋 . 𝑓 (𝐹 (𝑋 )) ⊆ 𝐹 (𝑓 (𝑋 )) Theorem 19 (Coinduction Up-to). Suppose 𝑓 is compatible with 𝐹 , then (∃𝐼 . 𝑋 ⊆ 𝐼 ∧ 𝐼 ⊆ 𝐹 (𝑓 (𝐼 ))) =⇒ 𝑋 ⊆ 𝜈𝐹 The idea of coinduction up-to was first explored in the specific context of proofs by bisimulation [36], and more recently extended in several ways to the general case of proofs by (parameterized) coinduction [23, 33, 34, 49]. Building on these works (and in particular on the “companion approach”

A Deductive System for Contract Satisfaction Proofs

of Pous [34], and the GPaco library [49]), we can extend our deductive system with the following rule enabling the exploitation of any function 𝑓 compatible with rbisimF: Up-To

𝑓 is compatible with rbisimF

(𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) ∈ 𝑓 𝑠1 ℎ1 𝑅⊢ 𝑠2 ℎ2

𝜆𝑠 1′ , 𝑠 2′ , ℎ 1′ , ℎ 2′ . 𝑅 ⊢

′ 𝑠1 𝑠 2′

ℎ 1′ ℎ 2′

Note that the absence of a frame around the hypothesis 𝑅 indicates that the rule Up-to can be used regardless of whether it is guarded or not, but guarded hypotheses remain guarded after applying the rule. We omit the soundness proof, which requires a slight adaption of the definition of quintuples (Definition 14), and we refer the readers to [23, 34, 49] (and to our Rocq development) for details regarding the combination of up-to techniques and Paco-style proofs. Using the newly introduced Up-to rule, we obtain a systematic method to soundly integrate (and combine!) the reasoning principles discussed in the previous subsection. It suffices to encode each principle as a compatible function 𝑓 . Although these compatibility proofs are fairly technical (they required us to prove a dozen auxiliary lemmas about rbisimF), the soundness of each principle then immediately follows from Up-to. We show in the next two subsections that all the principles discussed so far can be derived in this way, with the exception of the principle for augmenting hardware leakage. This last principle requires a subtle modification in order to be sound. 5.3

Reasoning Up To Symmetries and Equivalences

Reasoning up to symmetries and leakage-equivalent states is always sound, even mid-proof. This is reflected by the following set of rules. We write ≃ for equivalence of leakage (i.e., trace equality).

C-Swap

𝑠 𝑅⊢ 2 𝑠1 𝑠 𝑅⊢ 1 𝑠2

ℎ1 ℎ2

H-Swap

𝑠 𝑅⊢ 1 𝑠2 𝑠 𝑅⊢ 1 𝑠2

C-Leak-Eq

ℎ2 ℎ1

ℎ1 ℎ2

′ 𝑠 𝑅⊢ 1 𝑠2 𝑠 ℎ1 𝑅⊢ 1 𝑠2 ℎ2

𝑠 1 ≃ 𝑠 1′

H-Leak-Eq

ℎ1 ℎ2

ℎ 1 ≃ ℎ 1′ 𝑅⊢

𝑠1 𝑠2 ℎ1 ℎ2

𝑅⊢ 𝑠1 𝑠2

ℎ 1′ ℎ2

The four rules are derived from Up-To by choosing an appropriate compatible function. For example, the compatible function implementing C-Swap is: 𝑓C-Swap (𝑅) ≜ { (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (𝑠 2, 𝑠 1, ℎ 1, ℎ 2 ) ∈ 𝑅 } The functions implementing all other rules can be found in Section C of the appendix. We note that by combining Swap rules and Leak-Eq rules, we can replace any of the four states with a leakage-equivalent one. Further, since equality of leakage is equivalent to bisimilarity, the side-goals 𝑠 1 ≃ 𝑠 1′ and ℎ 1 ≃ ℎ 2′ can also be proven by parameterized coinduction. 5.4

Transitive Reasoning

Composing quintuples horizontally is sound, even mid-proof. This allows decomposing a proof by artificially reducing (resp. augmenting) leakage at the contract level (resp. hardware level) as reflected by the following two rules.

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

Reduce-Contract-Leakage

𝑠 ∅ ⊢ 1 𝑠2

𝑠 1′ 𝑠 2′

𝑠 𝑅⊢ 1 𝑠2

𝑠′ 𝑅 ⊢ 1′ 𝑠2 ℎ1 ℎ2

ℎ1 ℎ2

Augment-Hardware-Leakage ′ ℎ 𝑠 ℎ′

𝑅⊢

𝑠2

1 ℎ 2′

∅ ⊢lockstep 1′ ℎ2 𝑠 ℎ1 𝑅⊢ 1 𝑠2 ℎ2

ℎ1 ℎ2

Importantly, the two rules are not exactly symmetrical: on the hardware side, we can only compose with a lockstep variant of our quintuples on the right, defined as ′ ℎ1 ℎ1 𝑅 ⊢lockstep ′ ≜ (ℎ 1′ , ℎ 2′ , ℎ 1, ℎ 2 ) ∈ 𝐺 rbisimFlockstep (𝑅) ℎ2 ℎ2 Without this restriction, the rule Augment-Hardware-Leakage is unsound. Indeed, consider the following scenario: leak H (ℎ 1 ) ≠ leak H (ℎ 2 )

leak H (ℎ 1′ ) = leak H (ℎ 2′ )

leak H (next H (ℎ 1′ )) ≠ leak H (next H (ℎ 2′ ))

Under these assumptions, for any contract state 𝑠, we can easily prove the following first two quintuples, and yet disprove the third one: ′ 𝑠 ℎ 1′ ℎ1 ℎ1 𝑠 ℎ1 ⊤ ⊢ ∅ ⊢ ⊢ ¬ ⊤ 𝑠 ℎ 2′ 𝑠 ℎ2 ℎ 2′ ℎ 2 The first quintuple is proven using H-Step (exploiting leak(ℎ 1′ ) = leak(ℎ 2′ )), and then Cycle. The second quintuple is proven using C-step followed by C-Leak (exploiting leak H (next H (ℎ 1′ )) ≠ leak H (next H (ℎ 2′ ))). Even though we proved these two quintuples, the third one does not hold. This is because the two contract traces are equal by definition (so we can never use C-Leak to conclude), and because leak H (ℎ 1 ) ≠ leak H (ℎ 2 ) (so we cannot use H-Step to conclude either). The main issue in this counterexample is that the second quintuple (involving ℎ 1′ , ℎ 2′ , ℎ 1, ℎ 2 ) only holds because ℎ 1′ and ℎ 2′ have different traces, which we were able to discover using non-lockstep reasoning. However, the quintuple carries no information about ℎ 1 and ℎ 2 , nor about 𝑠 1 and 𝑠 2 . Working with lockstep relative bisimilarity instead fixes the problem: it forces a tighter connection between the four states. 6

Discussion: Limitations and Future Work

Additional Contract Features. We used the proof system to prove some of the key features of the original CT-SPEC contract (the one that uses the always-mispredict technique) [20], but there is still some work to be done to prove the entire contract correct. Most notably, our hardware semantics uses a simplified scheduler that does not feature a fetch-execute-retire pipeline. Furthermore, we are yet to combine the always-mispredict feature with the out-of-order scheduler. While the proof will require a non-negligible amount of work, judging from our experience using the proof system, we are confident that the proof will be feasible. Additionally, we have not considered nested speculation in this paper. Nested speculation is usually modeled by an explicit stack at the contract level. At the hardware level, though, speculation is typically implemented in a less structured way (e.g, using buffers). As a result, reasoning about nested speculation requires subtle invariants linking stacks with lower-level data-structures. Although our deductive system is complete, finding and expressing such invariants might be difficult in practice. To facilitate the process, an idea would be to extend our deductive system with built-in support for reasoning about a logical view of the hardware states rather than directly against low-level data-structures (e.g. taking inspiration of ghost states in modern separation logics [24]). This would certainly enable working with simpler invariants connecting contract and hardware states.

A Deductive System for Contract Satisfaction Proofs

Towards a Program Logic. Our proof system simplifies the process of mechanizing contract satisfaction proofs. Still, it requires explicit reasoning about concrete hardware and contract states. Conducting proofs with the help of a proof assistant such as Rocq significantly helps with the associated bookkeeping. However, for larger proofs and more complicated examples, reasoning implicitly about a more abstract set of states is desirable. To achieve this, an idea would be to enable reasoning about 4-ary predicates expressed in a carefully curated logic, rather than relying on the logic of the proof assistant to reason explicitly about quadruples of concrete states. This would certainly enable more modular proofs, in the style of what can be achieved using modern mechanized separation logics such as [24] or [18]. Nondeterminism. In this paper, we assumed that both the contract and the hardware semantics are deterministic. This follows the assumptions made in recent works on hardware-software contracts [20, 21, 28, 46, 47]. Adding support for nondeterminism would be a non-trivial research challenge. The first question would be how to define contract satisfaction in that setting. The current definition (Definition 1) would not be adequate anymore, as traces might change either because of leakage or because of nondeterminism. One option could be to use a ∀∃ quantifier alternation, inspired by how the noninterference property can be generalized to nondeterministic settings [27]. In the presence of a quantifier alternation, we would have to develop new reasoning principles to resolve existential quantifiers. Relative Bisimulation for SNI. The development of our deductive system was motivated by contract satisfaction proofs, but it could find further applications. A particularly interesting one is proving Speculative Non-Interference (SNI) [19], another instance of relative trace equality. SNI requires a program to not leak more than what is leaked through sequential, non-speculative execution of the CPU. Combining proofs of contract satisfaction and SNI guarantees the absence of information leakage when running a program [20]: first prove that a CPU satisfies a contract, and then prove that specific programs satisfy SNI with respect to that contract. Both proofs can in principle be developed within our deductive system. 7

Related Work

Contract Validation. There is a growing interest in validating CPUs against hardware-software contracts. Validation efforts either employ testing (mostly of black-box CPUs) [17, 21, 29, 30, 30], or they model-check white-box designs [39, 47]. When model-checking hardware-software contracts, the biggest challenge is finding invariants that enable the model checker to find a proof. Existing works tackle this challenge with inductive invariant learning (e.g., LeaVe [47]) or by requiring additional user input (e.g., shadow logic [39]). While having the advantage of automation, modelchecking techniques might abort (in the case of bounded model checking) or not terminate, leaving the user with little information as to why the proof fails. Additionally, model checking is vulnerable to logical and implementation bugs. We are the first to propose a foundational proof system for generating fully mechanized proofs for contract satisfaction. Secure Compilation. Our proof system builds on the rich tradition of simulation-based proofs for security. 4-ary reasoning is particularly prominent in the context of secure compilation to reason about the preservation of constant-timeness [1, 6–8], noninterference [9, 10], and, generally, ksafety hyperproperties [31, 35]. Many of these works have also been formalized in a proof assistant. Recently, secure compilation w.r.t. constant-timeness and noninterference has been extended to speculative semantics as well [2, 32, 44]. There are some key differences between our work and secure compilation. When proving that a compiler preserves noninterference, high-level objects (source programs) and low-level objects (target programs) are structurally very different, either

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

because the compiler is optimizing, or because the source and target languages are different. Further, there is a strict dependency between high and low level (i.e., we only reason about target programs obtained by compiling a source program). In the case of contracts, there is no compiler between the higher level (the contract) and the lower level (the hardware). The program is the same across the four compared executions, but it is executed under two different semantics. Our proof system take advantages of these observations, and lets the developer establish an artificial relation between the contract and the hardware for the purpose of the proof. 4-ary Reasoning Beyond Secure Compilation. Apart from secure compilation, there exist additional security properties that require 4-ary reasoning. Example are speculative noninterference [19, 20] and information-preserving refinement. for the latter, different simulation techniques have been chained to obtain a formal proof spanning the entire hardware-software stack [3, 4]. Another example is relative security, which compares the information flows occurring under different semantics [15]. Hardware-software contract satisfaction can be seen as an instance of relative security. Dongol et al [15] introduce a simulation-based proof technique for relative security. In contrast to our setting, they rely on proving that a collection of conditions hold for a simulation relation provided up-front. Our proof system lets us construct the simulation relation on the fly. Another distinction is that they use timers to bound their vanilla traces (corresponding to our contract traces), ensuring they do not execute infinitely without making progress. In our framework, this is handled implicitly through the use of coinductive-inductive predicates (the inductive part implicitly encodes the progress assumptions). We designed our notion of relative bisimilarity with contract satisfaction in mind, but we expect that it could be applicable to relative security as well. Parameterized Coinduction. Our work is strongly rooted in recent developments in the field of interactive proofs by coinduction. In particular, our proof technique leverages the framework of parameterized coinduction, introduced by Hur et al. [23]. Our Rocq formalization is based on their implementation of parameterized coinduction, Paco [22]. To prove the soundness of the techniques we presented in Section 5, we also leverage the notion of up-to techniques for coinductive proofs. In the paper introducing Paco, Hur et al. already identified that up-to techniques can be combined with parameterized coinduction. Later on, Pous developed a more general and systematic approach for the principled development and integration of up-to techniques via the so-called companion approach [34]. More recently, Zakowski et al. showed that the approach of Pous can also be integrated in Paco via generalized parameterized coinduction [49]. The extensions we developed in Section 5 rely on their implementation of generalized parameterized coinduction, which is now integrated in the Paco library [22]. Interaction Trees. Interaction Trees (ITrees) are a general purpose coinductive structure for representing impure computations [48]. ITrees are mechanized in Rocq, and come associated with several notions of behavioral equivalences, including ones specifically designed to prove security properties such as non-interference [38]. As our proof quintuples, these equivalences are defined as coinductive relations, and come associated with high-level reasoning principles facilitating proofs. However, to the best of our knowledge, ITrees do not feature reasoning principles for direct 4-ary reasoning in the style of our deductive system. Coinductive Proofs for Hyperproperties. Recently, Correnson and Finkbeiner applied parameterized coinduction to the verification of temporal hyperproperties [13]. Their mechanized framework, HyCo, supports the verification of a large class of hyperproperties. However, contract satisfaction is out of the scope their proof framework. In particular, HyCo does not support asynchronous reasoning in the style of our coinductive-inductive relation.

A Deductive System for Contract Satisfaction Proofs

Data Availability The Rocq development accompanying this paper is available on Zenodo at the following address: https://doi.org/10.5281/zenodo.19054166 Acknowledgements This work was supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany’s Excellence Strategy - EXC 2092 CASA - 390781972 and by the European Research Council (ERC) Grant HYPER (No. 101055412). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them. A. Correnson carried out this work as a member of the Saarbrücken Graduate School of Computer Science. References [1] Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2022. Enforcing Fine-grained Constant-time Policies. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (Los Angeles, CA, USA) (CCS ’22). Association for Computing Machinery, New York, NY, USA, 83–96. doi:10.1145/3548606.3560689 [2] Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, and Vincent Laporte. 2025. Preservation of Speculative Constant-Time by Compilation. Proc. ACM Program. Lang. 9, POPL, Article 44 (Jan. 2025), 33 pages. doi:10.1145/3704880 [3] Anish Athalye, Henry Corrigan-Gibbs, M. Frans Kaashoek, Joseph Tassarotti, and Nickolai Zeldovich. 2024. Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4-6, 2024. ACM, 655–672. [4] Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information-Preserving Refinement. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, 503–519. [5] Enrico Barberis, Pietro Frigo, Marius Muench, Herbert Bos, and Cristiano Giuffrida. 2022. Branch History Injection: On the Effectiveness of Hardware Mitigations Against Cross-Privilege Spectre-v2 Attacks. In 31st USENIX Security Symposium (USENIX Security 22). USENIX Association, Boston, MA, 971–988. https://www.usenix.org/conference/ usenixsecurity22/presentation/barberis [6] Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2019. Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4, POPL, Article 7 (Dec. 2019), 30 pages. doi:10.1145/3371075 [7] Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2021. Structured leakage and applications to cryptographic constant-time and cost. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. 462–476. [8] Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). 328–343. doi:10.1109/CSF.2018.00031 [9] Gilles Barthe, Tamara Rezk, and Amitabh Basu. 2007. Security types preserving compilation. Computer Languages, Systems & Structures 33, 2 (2007), 35–59. doi:10.1016/j.cl.2005.05.002 [10] Gilles Barthe, Tamara Rezk, Alejandro Russo, and Andrei Sabelfeld. 2010. Security of multithreaded programs by compilation. ACM Trans. Inf. Syst. Secur. 13, 3, Article 21 (July 2010), 32 pages. doi:10.1145/1805974.1805977 [11] Claudio Canella, Daniel Genkin, Lukas Giner, Daniel Gruss, Moritz Lipp, Marina Minkin, Daniel Moghimi, Frank Piessens, Michael Schwarz, Berk Sunar, Jo Van Bulck, and Yuval Yarom. 2019. Fallout: Leaking Data on Meltdownresistant CPUs. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (London, United Kingdom) (CCS ’19). Association for Computing Machinery, New York, NY, USA, 769–784. doi:10.1145/3319535. 3363219 [12] Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, and Derek Dreyer. 2023. Stuttering for Free. Proc. ACM Program. Lang. 7, OOPSLA2, Article 281 (Oct. 2023), 28 pages. doi:10.1145/3622857 [13] Arthur Correnson and Bernd Finkbeiner. 2025. Coinductive Proofs for Temporal Hyperliveness. Proc. ACM Program. Lang. 9, POPL, Article 53 (Jan. 2025), 28 pages. doi:10.1145/3704889

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

[14] Arthur Correnson, Iona Kuhn, and Bernd Finkbeiner. 2025. Almost Fair Simulations. Proc. ACM Program. Lang. 9, ICFP, Article 243 (Aug. 2025), 24 pages. doi:10.1145/3747512 [15] Brijesh Dongol, Matt Griffin, Andrei Popescu, and Jamie Wright. 2024. Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities. In 37th IEEE Computer Security Foundations Symposium, CSF 2024, Enschede, Netherlands, July 8-12, 2024. IEEE, 403–418. doi:10.1109/CSF61375.2024.00027 [16] Mohammad Rahmani Fadiheh, Johannes Müller, Raik Brinkmann, Subhasish Mitra, Dominik Stoffel, and Wolfgang Kunz. 2020. A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors. In 2020 57th ACM/IEEE Design Automation Conference (DAC). 1–6. doi:10.1109/DAC18072.2020.9218572 [17] Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, and Gururaj Saileshwar. 2025. AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 (Rotterdam, Netherlands) (ASPLOS ’25). Association for Computing Machinery, New York, NY, USA, 32–47. doi:10.1145/3676641.3716247 [18] Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022. Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6, POPL, Article 28 (Jan. 2022), 31 pages. doi:10.1145/3498689 [19] Marco Guarnieri, Boris Köpf, José F Morales, Jan Reineke, and Andrés Sánchez. 2020. Spectector: Principled detection of speculative information flows. In 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 1–19. [20] Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware-Software Contracts for Secure Speculation. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE. [21] Jana Hofmann, Emanuele Vannacci, Cedric Fournet, Boris Kopf, and Oleksii Oleksenko. 2023. Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions. In 32nd USENIX Security Symposium (USENIX Security 23). USENIX Association, Anaheim, CA, 7143–7160. https://www.usenix.org/conference/usenixsecurity23/ presentation/hofmann [22] Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. 2013. Paco: A Coq Library for Parameterized Coinduction. https://plv.mpi-sws.org/paco/ [23] Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. 2013. The power of parameterization in coinductive proof. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 193–206. doi:10.1145/2429069. 2429093 [24] Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India) (POPL ’15). Association for Computing Machinery, New York, NY, USA, 637–650. doi:10.1145/2676726.2676980 [25] Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In 2019 IEEE Symposium on Security and Privacy (SP). 1–19. doi:10.1109/SP.2019.00002 [26] Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading Kernel Memory from User Space. In 27th USENIX Security Symposium (USENIX Security 18). [27] D. McCullough. 1988. Noninterference and the composability of security properties. In Proceedings. 1988 IEEE Symposium on Security and Privacy (S&P’88). 177–186. doi:10.1109/SECPRI.1988.8110 [28] Gideon Mohr, Marco Guarnieri, and Jan Reineke. 2024. Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors (DATE’24). 1–6. [29] Oleksii Oleksenko, Christof Fetzer, Boris Köpf, and Mark Silberstein. 2022. Revizor: Testing Black-box CPUs against Speculation Contracts. In 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’22). ACM. [30] Oleksii Oleksenko, Marco Guarnieri, Boris Kopf, and Mark Silberstein. 2023. Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing . In 2023 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, Los Alamitos, CA, USA, 1737–1752. doi:10.1109/SP46215.2023.10179391 [31] Marco Patrignani and Deepak Garg. 2017. Secure Compilation and Hyperproperty Preservation. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 392–404. doi:10.1109/CSF.2017.13 [32] Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (Virtual Event, Republic of Korea) (CCS ’21). Association for Computing Machinery, New York, NY, USA, 445–461. doi:10.1145/3460120.3484534 [33] Damien Pous. 2007. Complete Lattices and Up-To Techniques. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 351–366.

A Deductive System for Contract Satisfaction Proofs

[34] Damien Pous. 2016. Coinduction All the Way Up. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (New York, NY, USA) (LICS ’16). Association for Computing Machinery, New York, NY, USA, 307–316. doi:10.1145/2933575.2934564 [35] Julian Rosemann, Sebastian Hack, and Deepak Garg. 2025. Non-interference Preserving Optimising Compilation. Proc. ACM Program. Lang. 9, OOPSLA2, Article 323 (Oct. 2025), 26 pages. doi:10.1145/3763101 [36] DAVIDE SANGIORGI. 1998. On the bisimulation proof method. Mathematical Structures in Computer Science 8, 5 (1998), 447–479. doi:10.1017/S0960129598002527 [37] Michael Schwarz, Moritz Lipp, Daniel Moghimi, Jo Van Bulck, Julian Stecklina, Thomas Prescher, and Daniel Gruss. 2019. ZombieLoad: Cross-Privilege-Boundary Data Sampling. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (London, United Kingdom) (CCS ’19). Association for Computing Machinery, New York, NY, USA, 753–768. doi:10.1145/3319535.3354252 [38] Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. 2023. Semantics for Noninterference with Interaction Trees. In 37th European Conference on Object-Oriented Programming (ECOOP 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263), Karim Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl – LeibnizZentrum für Informatik, Dagstuhl, Germany, 29:1–29:29. doi:10.4230/LIPIcs.ECOOP.2023.29 [39] Qinhan Tan, Yuheng Yang, Thomas Bourgeat, Sharad Malik, and Mengjia Yan. 2025. RTL Verification for Secure Speculation Using Contract Shadow Logic. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1 (Rotterdam, Netherlands) (ASPLOS ’25). Association for Computing Machinery, New York, NY, USA, 970–986. doi:10.1145/3669940.3707243 [40] Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. (1955). [41] Daniël Trujillo, Johannes Wikner, and Kaveh Razavi. 2023. INCEPTION: exposing new attack surfaces with training in transient execution. In Proceedings of the 32nd USENIX Conference on Security Symposium (Anaheim, CA, USA) (SEC ’23). USENIX Association, USA, Article 409, 18 pages. [42] Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx. 2018. Foreshadow: extracting the keys to the intel SGX kingdom with transient out-of-order execution. In Proceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (SEC’18). USENIX Association, USA, 991–1008. [43] Jo Van Bulck, Daniel Moghimi, Michael Schwarz, Moritz Lippi, Marina Minkin, Daniel Genkin, Yuval Yarom, Berk Sunar, Daniel Gruss, and Frank Piessens. 2020. LVI: Hijacking Transient Execution through Microarchitectural Load Value Injection. In 2020 IEEE Symposium on Security and Privacy (SP). 54–72. doi:10.1109/SP40000.2020.00089 [44] Sören van der Wall and Roland Meyer. 2025. SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations. Proc. ACM Program. Lang. 9, POPL, Article 51 (Jan. 2025), 30 pages. doi:10.1145/3704887 [45] Stephan van Schaik, Alyssa Milburn, Sebastian Österlund, Pietro Frigo, Giorgi Maisuradze, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. 2019. RIDL: Rogue In-Flight Data Load. In 2019 IEEE Symposium on Security and Privacy (SP). 88–105. doi:10.1109/SP.2019.00087 [46] Zilong Wang, Gideon Mohr, Klaus Gleissenthall, Jan Reineke, and Marco Guarnieri. 2025. Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors. [47] Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. 2023. Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. (2023), 2128–2142. doi:10. 1145/3576915.3623192 [48] Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2019. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4, POPL, Article 51 (Dec. 2019), 32 pages. doi:10.1145/3371119 [49] Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. 2020. An equational theory for weak bisimulation via generalized parameterized coinduction. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) (CPP 2020). Association for Computing Machinery, New York, NY, USA, 71–84. doi:10.1145/3372885.3373813

Full Architectural and Hardware Semantics

Figures 4 and 5 contain the full vanilla architectural and hardware semantics. B

Example 2: Out-of-Order Scheduler

This section presents the proof of our second example, the out-of-order scheduler in more detail. The full formalization and proof can be found in our accompanying Rocq development. This example gives a proof that out-of-order execution does not impact the leakage behavior if it preserves

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

Add

𝑣 = 𝑎(𝑥 2 ) + 𝑘 (𝑚, 𝑎, pc, add 𝑥 1, 𝑥 2, 𝑘) ⇒isa (𝑚, 𝑎[𝑥 1 ↦→ 𝑣], pc + 1) Branch

Load

𝑣 = 𝑚(𝑎(𝑥 2 ))

pc ′ = (𝑎(𝑥) = 0) ? 𝑙 : (pc + 1)

(𝑚, 𝑎, pc, load 𝑥 1, 𝑥 2 ) ⇒isa (𝑚, 𝑎[𝑥 1 ↦→ 𝑣], pc + 1)

(𝑚, 𝑎, pc, beqz 𝑥, 𝑙) ⇒isa (𝑚, 𝑎, pc ′ )

Fig. 4. Vanilla architectural semantics. Load

Other

(𝜎, load 𝑥 1, 𝑥 2 ) ⇒isa 𝜎 ′

(𝜎, 𝑖) ⇒isa 𝜎 ′

(𝜎, 𝑐, 𝑖) ⇒ H (𝜎 ′, 𝑐)

(𝜎, 𝑐, load 𝑥 1, 𝑥 2 ) ⇒ H (𝜎 ′, 𝑎(𝑥 2 ) ::𝑐)

Fig. 5. Vanilla hardware semantics. Execute

Execute Heap

Σ(𝑠.pc) = execute

(𝑠, 𝑃 (𝑠.pc)) ⇒ H 𝑠 ′

(𝑠, 𝑖) ⇒ H 𝑠 ′

(𝑠, ⊥) → − H (𝑠 ′, ⊥)

(𝑠, 𝑖) → − H (𝑠 ′ [pc ↦→ 𝑠.pc], ⊥)

Delay

Σ(𝑠.pc) = delay

𝑃 (𝑠.pc + 1) = 𝑖 2

𝑃 (𝑠.pc) = 𝑖 1 delayable(𝑖 1, 𝑖 2 )

𝑠 [pc ↦→ 𝑠.pc + 1] ⇒ H 𝑠 ′

(𝑠, ⊥) → − H (𝑠 ′, 𝑖 1 ) delayable(𝑖 1, 𝑖 2 ) = 𝑖 1 ≠ beqz ·, · ∧ des(𝑖 1 ) ≠ 𝑑𝑒𝑠 (𝑖 2 ) ∧ des(𝑖 1 ) ≠ 𝑠𝑟𝑐 (𝑖 2 ) ∧ src(𝑖 1 ) ≠ 𝑑𝑒𝑠 (𝑖 2 ) src(add 𝑥 1, 𝑥 2, 𝑘) = 𝑥 2

des(add 𝑥 1, 𝑥 2, 𝑘) = 𝑥 1

src(load 𝑥 1, 𝑥 2 ) = 𝑥 2

des(load 𝑥 1, 𝑥 2 ) = 𝑥 1

src(beqz 𝑥, 𝑙)

=𝑥

des(beqz 𝑥, 𝑙)

= 𝑠.pc

Fig. 6. Hardware semantics with out-of-order execution.

functional correctness. This is not trivial, as the out-of-order execution impacts the cache, which is observable by the attacker. We define a simple out-of-order scheduler that can decide to delay the execution of an instruction for one step by putting it on a heap. If there is an instruction on the heap, it is the one executed next. Out-of-Order Hardware Semantics. The semantics of the out-of-order scheduler is given in Figure 6. It uses a scheduling function Σ, which depends on the program counter. The functionality of the out-of-order scheduler is implemented in rule Delay. If the heap is empty, the scheduler can decide to delay the current instruction and execute the next one. This is only possible if the instruction is delayable. This predicate is encoded with a predicate that checks if one instruction impacts the execution of the other. The predicate is defined as expected: two instructions can be swapped if the components one instruction writes to are not read or written by the other instruction. Note that

A Deductive System for Contract Satisfaction Proofs

Step

𝜎 ⇒isa 𝜎

′

 𝜎.a(x2 )     o = 𝜎.a(x) =? 0   ⊥ 

if 𝑃 (𝜎.pc) = load 𝑥 1, 𝑥 2 if 𝑃 (𝜎.pc) = beqz 𝑥, 𝑙 otherwise

𝜎→ − C 𝜎′ Fig. 7. Sequential contract.

the combination of the predicate and the scheduling decision can result in the execution getting stuck. In our formalization, we only consider valid schedulers — that is, ones that return delay only when the hardware state is delayable, but not necessarily every time it is. Sequential Contract. The out-of-order execution can be abstracted away with a leakage contract that follows a simple in-order semantics that we formalize in Figure 7. The contract just exposes accessed addresses and the result of branching decisions. It is similar to the sequential contract CT-SEQ described previously [20]. Contract Satisfaction Proof. To establish that the sequential contract is satisfied by our simple outof-order execution hardware model, we rely on the soundness of our proof system for relative trace equality (Theorem 16). Accordingly, for any initial memories and register assignments 𝑚 1, 𝑚 2, 𝑎 1, 𝑎 2 , for any initial cache 𝑐 and initial program pointer pc, and for any valid scheduler Σ, it suffices to show that: (𝑚 1, 𝑎 1, pc) ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) ∅ ⊢ (𝑚 2, 𝑎 2, pc) ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥) As in the always-mispredict example, we apply the Invariant rule to establish the relational invariant needed for the proof: 𝐼 = { (𝑠 1, 𝑠 2, (ℎ 1, ⊥), (ℎ 2, ⊥)) | 𝑠𝑖 .𝑚 = ℎ𝑖 .𝑚 ∧ 𝑠𝑖 .𝑎 = ℎ𝑖 .𝑎 ∧ 𝑠𝑖 .pc = ℎ𝑖 .pc ∧ 𝑠 1 .pc = 𝑠 2 .pc ∧ ℎ 1 .𝑐 = ℎ 2 .𝑐 } After applying the Invariant rule, we now have 𝐼 as a (guarded) hypothesis. (𝑚 1, 𝑎 1, pc) ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) 𝐼 ⊢ (𝑚 2, 𝑎 2, pc) ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥) We perform a case analysis on the results of scheduler Σ(pc). When the scheduler returns execute, the hardware step is fully synchronized with the contract. In this case, we only need to show that after both the contract and hardware take a step, the relational invariant 𝐼 still holds. (𝑚 1, 𝑎 1, pc) ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) 𝐼 ⊢ (𝑚 2, 𝑎 2, pc) ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥) next C (𝑚 1, 𝑎 1, pc) next H ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) (C-Step’, H-Step) 𝐼 ⊢ next C (𝑚 2, 𝑎 2, pc) next H ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥) (Cycle) (next C (. . .), next C (. . .), next H (. . . , ⊥), next H (. . . , ⊥)) ∈ 𝐼 We note that in order to use H-Step, we first need to prove equality of leakage: leak H ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) = leak H ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥) According to our cache-based attacker model, only the cache is leaked. Since the cache is the same in both hardware states at this point, the equality trivially holds (the leakage is 𝑐 on both sides). We also note that to use the rule Cycle, we need to show that the invariant 𝐼 still holds after

Arthur Correnson, Haoyi Zeng, and Jana Hofmann

executing the current instruction. Fortunately, using the rule C-Step’ generates the assumption leak C (𝑚 1, 𝑎 1, pc, 𝑐) = leak C (𝑚 1, 𝑎 1, pc, 𝑐). This assumption is sufficient to prove that the invariant is restored. The only non-trivial case is when a load instruction is executed. In this case the cache changes, but since the contract leaks the loaded address, the cache remains the same in both hardware states and the invariant 𝐼 is restored. When the scheduler returns delay, there is a mismatch between the contract and the hardware execution. The hardware executes the instruction at pc + 1 first, and then the instruction at pc. The contract, however, executes instructions in order (pc, then pc + 1). To handle this misalignment, the trick is to first simulate two contract steps using C-Step’, and then simulate two hardware steps using H-Step. (𝑚 1, 𝑎 1, pc) ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) 𝐼 ⊢ (𝑚 2, 𝑎 2, pc) ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥) next C (next C (𝑚 1, 𝑎 1, pc)) ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥) (C-Step’ × 2) 𝐼 ⊢ next C (next C (𝑚 2, 𝑎 2, pc)) ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥) next C (next C (𝑚 1, 𝑎 1, pc)) next H (next H ((𝑚 1, 𝑎 1, pc, 𝑐), ⊥)) (H-Step × 2) 𝐼 ⊢ next C (next C (𝑚 2, 𝑎 2, pc)) next H (next H ((𝑚 2, 𝑎 2, pc, 𝑐), ⊥)) (Cycle) (next C (next C (. . .)), next C (next C (. . .)), next H (next H (. . .)), next H (next H (. . .))) ∈ 𝐼 To justify these five proof steps, we have a quite a few things to unpack: we need to justify the applicability of H-Step, and we need to prove that the invariant 𝐼 was indeed restored. We start by noting that the applications of C-Step’ generate two equality assumptions: leak C (. . .) = leak C (. . .) ∧ leak C (next C (. . .)) = leak C (next C (. . .)) Using H-Step two times requires us to prove the two following equality: leak H ((. . . , 𝑐), ⊥) = leak H ((. . . , 𝑐), ⊥) ∧ leak H (next H (. . . , ⊥)) = leak H (next H (. . . , ⊥)) To justify that the two applications of H-Step were valid, we can therefore prove the following implication: leak C (. . .) = leak C (. . .) ∧ leak C (next C (. . .)) = leak C (next C (. . .)) =⇒ leak H ((. . . , 𝑐), ⊥) = leak H ((. . . , 𝑐), ⊥) ∧ leak H (next H (. . . , ⊥)) = leak H (next H (. . . , ⊥)) Since a valid scheduler Σ only returns delay if the state is delayable, this also implies that instruction 𝑃 (pc) cannot be a branch. Thus, we have 6 combination of instructions to consider. As the cases are very similar, we only focus on the case of two successive loads as a representative example. I.e., we suppose 𝑃 (pc) = 𝑖 1 = load 𝑥 1, 𝑥 2 and 𝑃 (pc + 1) = 𝑖 2 = load 𝑥 1′ , 𝑥 2′ . First, let us examine how our implication can be proved in this case. Since both instructions are loads, the contract leaks the loaded addresses. On the hardware side, the cache is leaked. After unfolding the definitions of leak C and leak H , our implication therefore becomes: 𝑎 1 (𝑥 2 ) = 𝑎 2 (𝑥 2 ) ∧ next C (. . .).𝑎(𝑥 2′ ) = next C (. . .).𝑎(𝑥 2′ ) =⇒ 𝑐 = 𝑐 ∧ next H (. . . , ⊥).𝑎 1 (𝑥 2 ) = next H (. . . , ⊥).𝑎 2 (𝑥 2 ) The equality 𝑐 = 𝑐 is trivially true, but we still need to show next H (. . . , ⊥).𝑎(𝑥 2 ) = next H (. . . , ⊥).𝑎(𝑥 2 ) Unfortunately, the equality assumptions generated by the contract do not immediately match: we only know 𝑎 1 (𝑥 2 ) = 𝑎 2 (𝑥 2 ). However, we know that the two successive loads satisfy the delayable predicate. By definition (see Figure 6), this means that reordering their executions does not affect

A Deductive System for Contract Satisfaction Proofs

the values they read. In particular, 𝑎 1 (𝑥 2 ) must be equal to next H (. . . , ⊥).𝑎 1 (𝑥 2 ), and 𝑎 2 (𝑥 2 ) must be equal to next H (. . . , ⊥).𝑎 2 (𝑥 2 ). This concludes the leakage equality proof. We still need to show that the invariant was restored after the two contract steps and the two hardware steps. In the case of two successive loads, it is easy to verify that swapping their execution order does not impact the final state. Formally, assuming 𝑖 1 and 𝑖 2 are loads, for any microarchitectural states ℎ, ℎ𝑖 1 , ℎ𝑖 2 , ℎ ′ can show: (ℎ, 𝑖 1 ) ⇒ H ℎ𝑖 1 ∧ (ℎ𝑖 1 , 𝑖 2 ) ⇒ H ℎ ′ ⇐⇒ (ℎ, 𝑖 2 ) ⇒ H ℎ𝑖 2 ∧ (ℎ𝑖 2 , 𝑖 1 ) ⇒ H ℎ ′ Since we can swap the execution of these two load instructions without changing the hardware state, the contract states and the architectural states of the hardware states are synchronized after two steps. At this point, the reorder buffer is empty again, and the invariant 𝐼 is restored. C

Up-to Functions

Section 5 extends our deductive system with several up-to techniques to simplify proofs. The soundness of each up-to technique is justified by picking a compatible function 𝑓 and instantiating the rule Up-To. The following table explicitly describes which function is chosen to justify each up-to technique. Rule

Corresponding Compatible Function

C-Swap

𝑓 (𝑅) ≜ { (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (𝑠 2, 𝑠 1, ℎ 1, ℎ 2 ) ∈ 𝑅 }

H-Swap

𝑓 (𝑅) ≜ { (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (𝑠 1, 𝑠 2, ℎ 2, ℎ 1 ) ∈ 𝑅 }

C-Leak-Eq

𝑓 (𝑅) ≜ { (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (𝑠 1, 𝑠 1′ ) ∈ bisim ∧ (𝑠 1′ , 𝑠 2, ℎ 1, ℎ 2 ) ∈ 𝑅 }

H-Leak-Eq

𝑓 (𝑅) ≜ { (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (ℎ 1, ℎ 1′ ) ∈ bisim ∧ (𝑠 1, 𝑠 2, ℎ 1, ℎ 1′ ) ∈ 𝑅 }

Reduce-C-Leakage

𝑓 (𝑅) ≜ { (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (𝑠 1, 𝑠 2, 𝑠 1′ , 𝑠 2′ ) ∈ rbisim ∧ (𝑠 1′ , 𝑠 2′ , ℎ 1, ℎ 2 ) ∈ 𝑅 }

Augment-H-Leakage

𝑓 (𝑅) ≜ { (𝑠 1, 𝑠 2, ℎ 1, ℎ 2 ) | (ℎ 1′ , ℎ 2′ , ℎ 1, ℎ 2 ) ∈ rbisimlockstep ∧ (𝑠 1, 𝑠 2, ℎ 1′ , ℎ 2′ ) ∈ 𝑅 }

Record · ID 5905 · SHA-256 854d3b64dc85a4a1
Conceptio Open Knowledge Archive — every document is proof-bundled with source, license, and retrieval metadata.