Quantum Intermediate Representation (QIR) is a Microsoft-developed, LLVM-based intermediate representation for quantum program compilers. QIR aims to provide a general solution for quantum program compilers independent of front-end languages and back-end hardware, thus avoiding duplicate development of intermediate representations and compilers. Since it is still under development, QIR is described in natural language and lacks a formal definition, leading to ambiguity in its interpretation and a lack of rigor in implementing quantum functions. In this paper, we provide formal definitions for the data types and instruction sets of QIR, aiming to provide correctness and security guarantees for operations and intermediate code conversions in QIR. To validate our design, we show some samples of unsafe QIR code where errors can be detected by our formal approach.

翻译：量子中间表示（Quantum Intermediate Representation, QIR）是微软开发的一种基于LLVM的量子程序编译器中间表示。QIR旨在为量子程序编译器提供独立于前端语言和后端硬件的通用解决方案，从而避免中间表示与编译器的重复开发。由于仍处于开发阶段，QIR以自然语言描述且缺乏形式化定义，导致其解释存在歧义，且量子函数实现缺乏严谨性。本文针对QIR的数据类型与指令集提供形式化定义，旨在为QIR中的操作及中间代码转换提供正确性与安全保障。为验证设计方案，我们展示了若干存在潜在错误的非安全QIR代码示例，这些错误均可通过形式化方法检测。