.png){kind=icon}
.png){kind=icon}
Return
Building Blocks for Step-Indexed Program Logics
.png){kind=icon}
PRE
AI
DOI：10.1145/3779031.3779095.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
Step-Indexing
Later Modality
Iris
Rocq
Journal
P
IF:
0
Papers:
27
Citations:
0