A Reversible Three-Tier Intermediate Representation with Formal Semantic Preservation

Overview This work introduces the Universal Intermediate Representation (UIR), a vertically stratified compiler architecture designed to preserve semantic intent across progressive lowering stages. Unlike dialect-fragmented intermediate representation ecosystems, UIR organizes abstraction into three formally defined tiers: Tier 3 — Semantic Layer: Declarative intent, parallel semantics, memory models, and typed effect systems. Tier 2 — Optimization Layer: Structured computational forms including affine domains, polyhedral schedules, dependence graphs, and vector patterns. Tier 1 — Execution Layer: Canonical SSA-based representation with explicit control flow and memory operations, suitable for backend lowering. The defining property of UIR is reversible lowering. Each transformation between tiers is accompanied by a semantic preservation contract that enables round-trip equivalence within defined invariants. Core Contribution The paper formalizes: A three-tier IR architecture with explicit abstraction boundaries. A semantic equivalence relation across tiers: Semantics(S₃) = Semantics(S₂) = Semantics(S₁) Lowering and raising mappings: L₃₂: S₃ → S₂L₂₁: S₂ → S₁R₁₂: S₁ → S₂R₂₃: S₂ → S₃ A proof sketch demonstrating semantic preservation under transformation constraints. Architectural and formal mapping diagrams illustrating reversible compilation flow. UIR reframes compilation not as irreversible descent, but as structured semantic projection across layers. Motivation Most IR pipelines encode semantic intent into structural artifacts (loops, CFGs, barriers) during lowering. Over time, the original declarative meaning becomes non-recoverable. UIR enforces semantic continuity by: Separating meaning from structure. Encoding memory models and effect systems explicitly. Requiring invertible or reconstructible transformation metadata. Treating execution form as a projection of semantic intent. This approach enables: Late-stage re-optimization. Cross-platform retargeting after partial lowering. Autotuning at structured intermediate levels. Formal verification at the semantic layer independent of backend artifacts. Improved portability across heterogeneous architectures. Relevance UIR is relevant to research in: Compiler architecture Intermediate representation design Formal methods in compilation Polyhedral optimization Heterogeneous systems SSA-based infrastructures Semantic-preserving transformations The framework is especially applicable to emerging compute ecosystems where hardware heterogeneity and distributed execution demand stronger abstraction guarantees.