  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.
