Desired function
Maintain contracts between passes and repair IR when possible.
Futamura role
Cross-cutting infrastructure ensuring all passes see IR satisfying their expectations.
Inputs
- IR before/after major passes.
- Invariant specifications per pass.
Processing
- Check invariants; on failure either:
- Report diagnostics, or
- Apply adapter transformations (e.g., reinsert primitives, re-normalize types).
- Track which “hard algorithms” require/produce which IR flavors.
Outputs
- Verdict (safe/unsafe/unknown); counterexamples or proofs
- IR satisfying downstream contracts.
- Reports on violations and repairs.
Desired function
Maintain contracts between passes and repair IR when possible.
Futamura role
Cross-cutting infrastructure ensuring all passes see IR satisfying their expectations.
Inputs
Processing
Outputs