  Homomorphic encryption (HE) is a privacy-preserving technique that enables
computation directly on encrypted data. Despite its promise, HE has seen
limited use due to performance overheads and compilation challenges. Recent
work has made significant advances to address the performance overheads but
automatic compilation of efficient HE kernels remains relatively unexplored.
  This paper presents Porcupine, an optimizing compiler, and HE DSL named Quill
to automatically generate HE code using program synthesis. HE poses three major
compilation challenges: it only supports a limited set of SIMD-like operators,
it uses long-vector operands, and decryption can fail if ciphertext noise
growth is not managed properly. Quill captures the underlying HE operator
behavior that enables Porcupine to reason about the complex trade-offs imposed
by the challenges and generate optimized, verified HE kernels. To improve
synthesis time, we propose a series of optimizations including a sketch design
tailored to HE and instruction restriction to narrow the program search space.
We evaluate Procupine using a set of kernels and show speedups of up to 51%
(11% geometric mean) compared to heuristic-driven hand-optimized kernels.
Analysis of Porcupine's synthesized code reveals that optimal solutions are not
always intuitive, underscoring the utility of automated reasoning in this
domain.
