# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1902.00325