Quantum Hoare Logic with Ghost Variables

TL;DR

This paper introduces ghost variables into quantum Hoare logic, enhancing its ability to specify and reason about quantum program properties, demonstrated through a security proof of the quantum one-time pad.

Contribution

It extends quantum Hoare logic with ghost variables, allowing for more expressive pre-/postconditions and reasoning about quantum program properties.

Findings

Enhanced expressiveness in quantum program verification

Ability to specify classical and distributional properties

Successful proof of quantum one-time pad security

Abstract

Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces "ghost variables" to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually occur in the program and are allowed to have arbitrary quantum states (in a sense, they are existentially quantified), and be entangled with program variables. Ghost variables allow us to express properties such as the distribution of a program variable or the fact that a variable has classical content. And as a case study, we show how quantum Hoare logic with ghost variables can be used to prove the security of the quantum one-time pad.