Tuffy IR Language Reference

This document is the reference manual for the Tuffy IR, the intermediate representation used by the tuffy compiler. It describes the type system, instruction set, control flow structure, and textual format of the IR.

Status: This spec describes the currently implemented IR. Features described in the IR Design RFC but not yet implemented are noted as planned.

Source of truth: The formal definitions in Lean 4 (lean/TuffyLean/IR/) are authoritative. This spec is a human-readable description that must conform to the Lean definitions. When in doubt, consult the Lean code.

Introduction

Tuffy IR is a typed, SSA-based intermediate representation organized around a hierarchical control flow graph with SESE (Single Entry, Single Exit) regions.

Key design principles:

• Infinite precision integers — no fixed bit widths; range constraints via assert nodes
• Block arguments instead of PHI nodes (Cranelift/MLIR style)
• Hierarchical CFG — loops and structured control flow are explicit SESE regions
• Poison-only UB model — no undef; only poison
• Single data structure — one IR across all compilation stages

Table of Contents

• Type System
• Values
• Functions
• Regions
• Basic Blocks
• Instructions
  • Constants
  • Arithmetic
  • Floating Point Arithmetic
  • Comparison
  • Value Annotations
  • Memory Operations
  • Atomic Operations
  • Type Conversion
  • Pointer Operations
  • Function Calls
  • Terminators
• Text Format
• Planned Features