Popular RLWE-based Fully Homomorphic Encryption (FHE) schemes add some small noise to the message during encryption. The noise accumulates with each homomorphic operation. When the noise exceeds a critical value, the FHE circuit produces an incorrect output. This makes developing FHE applications quite tedious and error-prone as existing libraries and compilers offer limited support to statically track the noise. Additionally, FHE circuits are also plagued by wraparound errors that are common in finite modulus arithmetic. Unfortunately, none of the existing compilers and libraries guarantee correct FHE evaluation.

In this work, we present a correctness-oriented IR, ILA, for type-checking circuits intended for homomorphic evaluation. Our IR is backed by a type system that tracks low-level quantitative bounds (e.g., ciphertext noise) without using the secret key. Using our type system, we identify and prove a strong functional correctness criterion for ILA circuits. Additionally, we have designed ILA to be maximally general: our core type system does not directly assume a particular FHE scheme, but instead axiomatizes a model of FHE. We instantiate this model with the BGV scheme and get functional correctness for free.

We implemented the static ILA type checker parameterized by the noise estimators. We also use the type checker to infer the optimal placement of modulus switching, a noise reducing operation. Evaluation shows that the type checker is sound (always detects noise overflows) and practical (noise estimates are tight).