@article {3254, title = {Symphony: Expressive Secure Multiparty Computation with Coordination}, journal = {The Art, Science, and Engineering of Programming}, volume = {7}, year = {2023}, month = {2/20/2023}, type = {14}, abstract = {

Context: Secure Multiparty Computation (MPC) refers to a family of cryptographic techniques where mutually untrusting parties may compute functions of their private inputs while revealing only the function output. Inquiry: It can be hard to program MPCs correctly and efficiently using existing languages and frameworks, especially when they require coordinating disparate computational roles. How can we make this easier? Approach: We present Symphony, a new functional programming language for MPCs among two or more parties. Symphony starts from the single-instruction, multiple-data (SIMD) semantics of prior MPC languages, in which each party carries out symmetric responsibilities, and generalizes it using constructs that can coordinate many parties. Symphony introduces **first-class shares** and **first-class party sets** to provide unmatched language-level expressive power with high efficiency. Knowledge: Developing a core formal language called λ-Symphony, we prove that the intuitive, generalized SIMD view of a program coincides with its actual distributed semantics. Thus the programmer can reason about her programs by reading them from top to bottom, even though in reality the program runs in a coordinated fashion, distributed across many machines. We implemented a prototype interpreter for Symphony leveraging multiple cryptographic backends. With it we wrote a variety of MPC programs, finding that Symphony can express optimized protocols that other languages cannot, and that in general Symphony programs operate efficiently. [ full abstract at https://doi.org/10.22152/programming-journal.org/2023/7/14 ]\ 

}, doi = {10.22152/programming-journal.org/2023/7/14}, url = {https://arxiv.org/abs/2302.10076}, author = {Ian Sweet and David Darais and David Heath and William Harris and Ryan Estes and Michael Hicks} } @conference {2941, title = {Expanding the VOQC Toolkit}, booktitle = {The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021)}, year = {2021}, month = {06/2021}, abstract = {

voqc [Hietala et al. 2021b] (pronounced \“vox\”) is a compiler for quantum circuits, in the style of
tools like Qiskit [Aleksandrowicz et al. 2019], tket [Cambridge Quantum Computing Ltd 2019],
Quilc [Rigetti Computing 2019], and Cirq [Developers 2021]. What makes voqc different from these
tools is that it has been formally verified in the Coq proof assistant [Coq Development Team 2019].
voqc source programs are expressed in sqir, a simple quantum intermediate representation, which
has a precise mathematical semantics. We use Gallina, Coq\’s programming language, to implement
voqc transformations over sqir programs, and use Coq to prove the source program\’s semantics
are preserved. We then extract these Gallina definitions to OCaml, and compile the OCaml code to
a library that can operate on standard-formatted circuits.
voqc, and sqir, were built to be general-purpose. For example, while we originally designed sqir
for use in verified optimizations, we subsequently found sqir could also be suitable for writing, and
proving correct, source programs [Hietala et al. 2021a]. We have continued to develop the voqc
codebase to expand its reach and utility.
In this abstract, we present new extensions to voqc as an illustration of its flexibility. These
include support for calling voqc transformations from Python, added support for new gate sets
and optimizations, and the extension of our notion of correctness to include mapping-preservation,
which allows us to apply optimizations after mapping, reducing the cost introduced by making a
program conform to hardware constraints.

}, url = {http://rand.cs.uchicago.edu/files/planqc_2021c.pdf}, author = {Kesha Hietala and Liyi Li and Akshaj Gaur and Aaron Green and Robert Rand and Xiaodi Wu and Michael Hicks} } @article {2729, title = {Proving Quantum Programs Correct}, journal = {Schloss Dagstuhl}, year = {2021}, month = {7/13/2021}, abstract = {

As quantum computing steadily progresses from theory to practice, programmers are faced with a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Simon\&$\#$39;s algorithm, Grover\&$\#$39;s algorithm, and quantum phase estimation, a key component of Shor\&$\#$39;s algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.

}, doi = {https://doi.org/10.4230/LIPIcs.ITP.2021.21}, url = {https://arxiv.org/abs/2010.01240}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Liyi Li and Michael Hicks} } @article {2912, title = {Verified Compilation of Quantum Oracles}, year = {2021}, month = {12/13/2021}, abstract = {

Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum algorithm. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits among three different bases via the Quantum Fourier Transform and Hadamard operations, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM\&$\#$39;s design enabled us to prove correct VQO\&$\#$39;s compilers -- from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language -- and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement oracles used in Shor\&$\#$39;s and Grover\&$\#$39;s algorithms, as well as several common arithmetic operators. VQO\&$\#$39;s oracles have performance comparable to those produced by Quipper, a state-of-the-art but unverified quantum programming platform.

}, url = {https://arxiv.org/abs/2112.06700}, author = {Liyi Li and Finnegan Voichick and Kesha Hietala and Yuxiang Peng and Xiaodi Wu and Michael Hicks} } @article {2491, title = {A Verified Optimizer for Quantum Circuits}, journal = {Proceedings of the ACM on Programming Languages}, volume = {5}, year = {2021}, month = {11/12/2020}, abstract = {

We present VOQC, the first fully verified compiler for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. We evaluate VOQC\&$\#$39;s verified optimizations on a series of benchmarks, and it performs comparably to industrial-strength compilers. VOQC\&$\#$39;s optimizations reduce total gate counts on average by 17.7\% on a benchmark of 29 circuit programs compared to a 10.7\% reduction when using IBM\&$\#$39;s Qiskit compiler.

}, doi = {https://doi.org/10.1145/3434318}, url = {https://arxiv.org/abs/1912.02250}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks} } @article {2404, title = {Verified Optimization in a Quantum Intermediate Representation}, year = {2019}, month = {04/12/2019}, abstract = {

We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing {\textquoteleft}quantum assembly\&$\#$39; languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire\&$\#$39;s use as a tool for general verification by proving several quantum programs correct.

}, url = {https://arxiv.org/abs/1904.06319}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks} } @article {2306, title = {Quantitative Robustness Analysis of Quantum Programs (Extended Version)}, journal = {Proc. ACM Program. Lang.}, volume = {3}, year = {2018}, month = {2018/12/1}, pages = {Article 31}, abstract = {

Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called ε-robustness, which characterizes possible \"distance\" between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.

}, doi = {https://doi.org/10.1145/3290344}, url = {https://arxiv.org/abs/1811.03585}, author = {Shih-Han Hung and Kesha Hietala and Shaopeng Zhu and Mingsheng Ying and Michael Hicks and Xiaodi Wu} }