Step-indexing and the later modality (sic) P. are widely used in program logics. A key challenge in proofs in step-indexed logics is turning (sic) P into P, coined the later elimination problem. Later elimination cannot be done unconditionally, and has traditionally been linked one-to-one to the physical steps the program performs in the operational semantics. This one-to-one correspondence proved limiting in practice, and various techniques (flexible step-indexing and later credits) have been proposed to relax this correspondence. Unfortunately, there exist many variations of these techniques with different features and proof rules. Moreover, integrating these techniques into a program logic for a specific domain ( e.g., crash safety or trace refinement) requires non-trivial proof engineering of the metatheory. Our goal is to consolidate this situation. We introduce the physical-step modality-a modular building block that enables designers of program logics to obtain all existing features and rules with little proof engineering effort. We integrate our modality into various projects in the Iris ecosystem (Actris, RefinedRust, Perennial, Trillium), and show that it unlocks new proof rules that these projects previously did not support. All our results are mechanized in the Rocq prover.
Verifying cache coherence protocols is a notoriously difficult problem. At the intersection between distributed protocol and computer architecture, it has long served as a premier target for formal methods. Current verification approaches hinge on the challenging discovery of large global inductive invariants. This paper introduces an alternative proof strategy that tames the complexity through two main contributions: protocol decomposition and a framework of local invariants. We prove the correctness of the standard MSI protocol compositionally by independently verifying the simpler MI and SI subprotocols and proving MSI behaves as their combination. This decomposition revealed a useful insight: the invariants necessary in these proofs can be established using a small set of simple local invariants: invariants between a single cache and the parent and memory, eliminating complex global reasoning across children caches. We demonstrate how our approach reduces the number of required invariants from several dozens to hundreds in prior work to a small, structured and manageable set, simplifying the proof of correctness. The entire development is formalized in Lean 4.
While the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. This paper presents a toolbox for the Rocq proof assistant that can be used to verify the decidability of theword problem for a given monoid and, in some cases, to produce the corresponding decision procedure. As this verification can be computationally intensive, the toolbox heavily relies on proofs by reflection guided by an external oracle. This approach has been successfully used on several large presentations from the literature, as well as on a database of one million 1-relation monoids. The huge size of this database forced some unusual considerations onto the Rocq formalization, so that the formal proofs could be checked in a reasonable amount of time.
In constructive commutative algebra, we revive the bar inductive characterization of Noetherian rings. We contribute the first constructive (axiom free) implementation of Hilbert's basis theorem, in the Rocq proof assistant. We show that the polynomial ring R[X] is Noetherian when the ring R is Noetherian, without assuming any additional condition on R, like coherence or else strong discreteness. We also contribute and implement a new result, that Noetherian rings are closed under direct products, again without assuming any supplementary condition on rings. We study induction principles for Noetherian rings, and relate bar Noetherianity with some other constructive characterizations.
We present an intrinsic representation of type theory in the proof assistant Cubical Agda, inspired by Awodey's natural models of type theory. The initial natural model is defined as quotient inductive-inductive-recursive types, leading us to a syntax accepted by Cubical Agda without using any transports, postulates, or custom rewrite rules. We formalise some meta-properties such as the standard model, normalisation by evaluation for typed terms, and strictification constructions. Since our formalisation is carried out using Cubical Agda's native support for quotient inductive types, all our constructions compute at a reasonable speed. When we try to develop more sophisticated metatheory, however, the 'transport hell' problem reappears. Ultimately, it remains a considerable struggle to develop the metatheory of type theory using an intrinsic representation that lacks strict equations. The effort required is about the same whether or not the notion of natural model is used.
