A Quantum Interpretation of Bunched Logic & Quantum Separation Logic

Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu

# # 关于理解

1. 关于$\mathbf{C}-$modification, 实际上对应了经典逻辑中的 substitution，目的就是对于一个 postcondition $\phi$，希望找到一个 substitution $\phi[\mathbf{C}]$ 满足: $\models\{\phi[\mathbf{C}]\}\mathbf{C}\{\phi\}$

# # 技术细节

## # Notations

• Let $\mathbf{V}$ be the set of all quantum variables.

• A quantum register is a list of distinct variables $\bar{q}=q_1,...,q_n$. Each quantum variable $q$ has a type $\mathcal{H}_q$, which is the state Hilbert space of quantum system denoted by $q$.

• For a set of quantum variables $S=\{q_1,...,q_n\}\subseteq\mathbf{V}$ (or a quantum register $\bar{q}=q_1,...,q_n$):

1. $\mathcal{H}_S=\bigotimes_{i=1}^n \mathcal{H}_{q_i}$: the Hilbert space of $S$.

2. $\dim(S)$: the dimension of $\mathcal{H}_S$.

3. $\mathcal{D}(S)$: the set of all (mixed) quantum states of $S$.

4. For any $\rho\in\mathcal{D}(S)$, its domain is defined as $\text{dom}(\rho)\triangleq S$. We write $\mathcal{D}=\bigcup_{S\subseteq\mathbf{V}}\mathcal{D}(S)$ for the set of all states.

5. $\mathcal{P}(S)$: the set of projections on $\mathcal{H}_S$. In particular, for any $P\in\mathcal{P}(S)$, its domain is defined as $\text{free}(P)\triangleq S$.

Since there is a one-to-one correspondence between projections and closed subspaces, we sometimes call closed subspaces of $\mathcal{H}_S$ projections. We write $\mathcal{P}=\bigcup_{S\subseteq\mathbf{V}}\mathcal{P}(S)$ for the set of all projections.

6. $\rho|_S\triangleq \text{tr}_{\text{dom}(\rho)\backslash S}(\rho)$: the restriction of state $\rho$ on $S$, defined as a reduced density operator over $S\cap \text{dom}(\rho)$.

## # Quantum Interpretation of Bunched Logic

Definition(BI logic):

• BI formula is generated with the following syntax:

$\newcommand\sepimp{\mathrel{-\mkern-6mu*}} \phi,\psi::=p\in\mathcal{AP}\mid\top\mid\bot\mid\phi\wedge\psi\mid\phi\wedge\psi\mid\phi\rightarrow\psi\mid\phi *\psi\mid\phi\sepimp\psi\\$

where $p$ ranges over a set $\mathcal{AP}$ of atomic propositions.

• BI frame is a tuple $\mathcal{X}=(X,\circ,\preceq,e)$ where $X$ is a set equipped with a preorder $\preceq$, and $\circ:X\times X\rightarrow X$ is a partial binary operation with an unit element $e$, satisfying:

1. (Unit Existence) $\forall x\in X,x=x\circ e=e\circ x$.
2. (Commutativity) $x\circ y=y\circ x$.
3. (Associativity) $x\circ (y\circ z)=(x\circ y)\circ z$.
4. (Compatible with $\preceq$) If $x\preceq x'$ and $y\preceq y$ and $x\circ y,x'\circ y'$ are defined, then $x\circ y\preceq x'\circ y'$.

The “$=$” means that either both sides are defined, or both undefined.

• A valuation is a mapping $\mathcal{V}:\mathcal{AP}\rightarrow\wp(X)$ where $\wp$ represents the power set. The map is monotonic if $x\in\mathcal{V}(p)$ and $y\succeq x$ implies $y\in\mathcal{V}(p)$.

• A BI frame $\mathcal{X}$ together with a monotonic valuation $\mathcal{V}$ gives a BI model $\mathcal{M}=(X,\circ,\prec,e,\mathcal{V})$.

• Given a BI formula $\phi$ and a BI model $\mathcal{M}$, for each $x\in X$, the satisfaction relation $x\models \phi$ is defined by induction on $\phi$:

1. $x\models_{\mathcal{M}} p$ iff $x\in\mathcal{V}(p)$.
2. $x\models_{\mathcal{M}}\top$: always.
3. $x\models_{\mathcal{M}}\bot$: never.
4. $x\models_{\mathcal{M}}\phi_1\wedge\phi_2$ iff $x\models_{\mathcal{M}}\phi_1$ and $x\models_{\mathcal{M}}\phi_2$.
5. $x\models_{\mathcal{M}}\phi_1\vee\phi_2$ iff $x\models_{\mathcal{M}}\phi_1$ or $x\models_{\mathcal{M}}\phi_2$.
6. $x\models_{\mathcal{M}}\phi_1\rightarrow\phi_2$ iff $\forall x'\succeq x$, $x'\models_{\mathcal{M}}\phi_1$ implies $x'\models_{\mathcal{M}}\phi_2$.
7. $x\models_{\mathcal{M}}\phi_1*\phi_2$ iff $\exists y,z$ s.t. $y\circ z$ is defined and $x\succeq y\circ z$ and $y\models_{\mathcal{M}}\phi_1$ and $z\models_{\mathcal{M}}\phi_2$.
8. x\models_{\mathcal{M}}\phi_1\sepimp\phi_2 iff $\forall y$ s.t. $x\circ y$ is defined, $y\models_{\mathcal{M}}\phi_1$ implies $x\circ y\models_{\mathcal{M}}\phi_2$.

Then we are going to introduce the quantum instance for BI logic:

### # BI frame of quantum states

For a BI frame $\mathcal{X}=(X,\circ,\preceq,e)$, we instantiate it in quantum case:

• $X\triangleq\mathcal{D}$ is the set of all states.

• For $\circ:\mathcal{D}\times\mathcal{D}\rightarrow\mathcal{D}$:

$\rho_1\circ\rho_2\triangleq\begin{cases}\rho_1\otimes\rho_2 & \text{if dom}(\rho_1)\cap\text{dom}(\rho_2)=\emptyset\\ \text{undefined}&\text{otherwise}\end{cases}$

• For preorder $\preceq$ defined on $\mathcal{D}$:

$\rho_1\preceq\rho_2 \text{ iff } \text{dom}(\rho_1)\subseteq\text{dom}(\rho_2)\text{ and }\rho_1=\rho_2|_{\text{dom}(\rho_1)}$

• For the unit $e$, it’s understood as the state over the empty register.

### # Atomic propositions about quantum states

• Propositions denoting free variables:

For each variable set $S\subseteq\mathbf{V}$, we introduce a set of atomic propositions $\mathbf{D}[S]$ with domain defined by $\text{free}(\mathbf{D}[S])\triangleq S$. We interpret it as the state with domain at least $S$:

$[|\mathbf{D}[S]|]\triangleq\{\rho\in\mathcal{D}:S\subseteq\text{dom}(\rho)\}$

• Propositions for qualitative analysis:

For qualitative analysis of quantum programs, we often use projection operators as atomic propositions. For a projection $P\in\mathcal{P}$ as an atomic proposition, its semantics is defined as:

$[|P|]\triangleq\{\rho\in\mathcal{D}:\text{free}(P)\subseteq\text{dom}(\rho)\text{ and supp}(\rho|_{\text{free}(P)})\subseteq P\}$

where the support of a state $\rho\in\mathcal{D}$ is the (topological) closure of the subspaces spanned by its eigenvectors with nonzero eigenvalues, or equivalently:

$\text{supp}(\rho)=\{|\phi\rangle\in\mathcal{H}_{\text{dom}(\rho)}:\langle\phi|\rho|\phi\rangle=0\}^{\bot}$

Let’s carefully explain the definition of $[|P|]$. In the case that $\rho$ has the same domain of $P$, it is natural to define $\rho\in[|P|]$ if its support space $\text{supp}(\rho)$ lies in $P$.

In the case where $\text{dom}(\rho)$ and $\text{free}(P)$ are not the same, in order to make $[|P|]$ upward-closed (i.e. monotonic): $\rho\in[|P|]$ and $\rho\preceq\rho'$ imply $\rho'\in[|P|]$, it is appropriate to require that $\rho\in[|P|]$ iff $\text{dom}(\rho)\supseteq \text{free}(P)$ and the restricted state of $\rho$ on $\text{free}(P)$ is in $[|P|]$.

• Atomic propositions expressing uniformity in quantum security

For each variable set $S\subseteq\mathbf{V}$, we introduce an atomic proposition $\mathbf{U}[S]$. Its domain is $\text{free}(\textbf{U}[S])\triangleq S$. The semantics is defined as:

$[|\textbf{U}(S)|]\triangleq \left \{\rho\in\mathcal{D}:S\subseteq \text{dom}(\rho)\text{ and }\rho|_S=\frac{I_S}{\dim(S)}\right \}$

The intuition is: for a state $\rho\in[|\textbf{U}(S)|]$ such that $S\subseteq\text{dom}(\rho)$, its restriction on $S$ should be the completely mixed state, $\frac{I_S}{\dim(S)}$, which means “uniformly distributed” over all orthonormal bases of the system denoted by $S$.

• Axiom schema for atomic formulas

1. $\models \mathbf{D}[S]\leftrightarrow I_S$, where $I_S$ is the identity operator over $\mathcal{H}_S$, i.e. $[|\mathbf{D}(S)|]=[|I_S|]$.
2. For all $P,Q\in\mathcal{P}$ with disjoint domains, $\models P\wedge Q\leftrightarrow P\otimes Q$.
3. If $S_1\subseteq S_2$, then $\models \mathbf{U}[S_2]\rightarrow\mathbf{U}[S_1]$.
4. If $S_1\cap S_2=\emptyset$, then $\models (\mathbf{U}[S_1]*\mathbf{U}[S_2])\leftrightarrow \mathbf{U}[S_1\cup S_2]$.

### # Restriction property

The formulas generated by following grammar are denoted by RES:

$\phi,\psi::=p\in\mathcal{AP}\mid\top\mid\bot\mid\phi\wedge\psi\mid\phi\vee\psi\mid\phi*\psi$

Any formular $\phi\in\text{Res}$ is restrictive, that is, for any $\rho\models\phi,\rho|_{\text{free}(\phi)}\models\phi$.

### # Modification of BI Formulas

Let $\mathbf{C}$ be a unitary transformation $\bar{q}:=U[\bar{q}]$ or an initialization $q:=|0\rangle$,

For any $p\in\mathcal{AP}$, we write $p[\mathbf{C}]$ for the modification:

1. For atomic proposition $\mathbf{D}[S]$, $\mathbf{D}[S][\mathbf{C}]\triangleq\mathbf{D}[S]$.

2. For a projection $P$,

$P[\bar{q}:=U[\bar{q}]]\triangleq\begin{cases} P_{U[\bar{q}]}&\bar{q}\subseteq\text{free}(P)\\ P&\bar{q}\cap\text{free}(P)=\emptyset\\ \text{undefined}&\text{otherwise} \end{cases}\\ P[\bar{q}:=|0\rangle]\triangleq\begin{cases} \textbf{D}[q]\wedge \lceil P\rceil_q &q\in\text{free}(P)\\ P&\text{otherwise} \end{cases}\\$

where

$P_{U[\bar{q}]}=(U^{\bar{q}\dagger}\otimes I_{\text{free}(P)\backslash \bar{q}})P(U^{\bar{q}}\otimes I_{\text{free}(P)\backslash \bar{q}})$

and $\lceil P\rceil_q=\bigsqcup\{$ closed subspaces $T:|0\rangle_q\langle 0|\otimes T\subseteq P\}\in\mathcal{P}(\text{free}(P)\backslash q)$.

Here $\sqcup$ is the disjunction of projections in quantum logic, that is, for projections $P,Q$ with the same domain, $P\sqcup Q=\overline{\text{span}(P\cup Q)}$ with “$\overline{\cdot}$” standing for (topological closure).

3. For uniformity atomic proposition,

$\mathbf{U}[S][\bar{q}:=U[\bar{q}]]=\begin{cases} \mathbf{U}[S]&\bar{q}\subseteq S\text{ or }\bar{q}\cap S=\emptyset\\ \text{undefined} &\text{otherwise} \end{cases}\\ \mathbf{U}[S][\bar{q}:=|0\rangle]=\begin{cases} \mathbf{U}[S]&q\notin S\\ \text{undefined} &\text{otherwise} \end{cases}\\$

we write $\phi[\mathbf{C}]\downarrow$ when $\phi[\mathbf{C}]$ is defined.

• if $\phi=\top,\bot$, $\phi[\mathbf{C}]\triangleq \phi$;

• if $\phi=p\in\mathcal{AP}$, $\phi[\mathbf{C}]$ is defined as above;

• if $\phi=\phi_1\wedge\phi_2$ and $\phi_1[\mathbf{C}]\downarrow$ and $\phi_2[\mathbf{C}]\downarrow$, then $\phi[\mathbf{C}]=\phi_1[\mathbf{C}]\wedge\phi_2[\mathbf{C}]$;

• if $\phi=\phi_1\vee\phi_2$ and $\phi_1[\mathbf{C}]\downarrow$ and $\phi_2[\mathbf{C}]\downarrow$, then $\phi[\mathbf{C}]=\phi_1[\mathbf{C}]\vee\phi_2[\mathbf{C}]$;

• if $\phi=\phi_1*\phi_2$ and $\phi_1[\mathbf{C}]\downarrow,\phi_2[\mathbf{C}]\downarrow$ and ($\bar{q}\subseteq \text{free}(\phi_1)$ or $\bar{q}\wedge\text{free}(\phi_1)=\emptyset$) and ($\bar{q}\subseteq \text{free}(\phi_2)$ or $\bar{q}\wedge\text{free}(\phi_2)=\emptyset$), then

• if $\mathbf{C}=\bar{q}:=U[\bar{q}]$, then $\phi[\mathbf{C}]=\phi_1[\mathbf{C}]*\phi_2[\mathbf{C}]$;
• if $\mathbf{C}=q:=|0\rangle$, then
• if $q\notin\text{free}(\phi_1)\cup\text{free}(\phi_2)$, $\phi[\mathbf{C}]=\phi_1[\mathbf{C}]*\phi_2[\mathbf{C}]$;
• if only one of $q\in\text{free}(\phi_1)$ or $q\in\text{free}(\phi_2)$is satisfied, then $\phi[\mathbf{C}]=(\phi_1[\mathbf{C}]\wedge\phi_2[\mathbf{C}])\wedge (\mathbf{D}[\text{free}(\phi_1)\backslash q]*\mathbf{D}[\text{free}(\phi_2)\backslash q])$.
• otherwise, $\phi[\mathbf{C}]$ is undefined.

Proposition:

• $\text{free}(\phi)=\text{free}(\phi[\mathbf{C}])$.
• for all $\rho\in\mathcal{D}(\text{free}(\phi)\cup\text{var}(\mathbf{C}))$, if $\rho\models \phi[\mathbf{C}]$, then $[|\mathbf{C}|](\rho)\models \phi$.

## # Quantum Separation Logic

Let $\mathbf{V}$ be a set of quantum variables with $\text{free}(\phi),\text{free}(\psi),\text{var}(\mathbf{C})\subseteq\mathbf{V}$. Then $\mathbf{V}\models\{\phi\}\mathbf{C}\{\psi\}$ is true in the sense of partial correctness if we have:

$\forall \rho\in\mathcal{D}(\mathbf{V}),\rho\models\phi\Rightarrow[|\mathbf{C}|]_{\mathbf{V}}(\rho)\models\psi$

Inference rules:

\begin{aligned} &\frac{}{\{\phi\}\text{skip}\{\psi\}}\\ &\frac{\phi[q:=|0\rangle]\downarrow}{\{\phi[q:=|0\rangle\}q:=|0\rangle\{\phi\}}\\ &\frac{\{\phi\}\mathbf{C}_1\{\psi\}\quad\{\psi\}\mathbf{C}_2\{\mu\}}{\{\phi\}\mathbf{C}_1;\mathbf{C}_2\{\mu\}}\\ & \frac{\forall m,\{\phi*M_m\}\mathbf{C}_m\{\phi\}\quad \psi\in\text{CM}}{\{\phi*\mathbf{D}(\bar{q})\}\text{if }(\square m.M[\bar{q}]=m\rightarrow\mathbf{C}_m)\text{ fi}\{\psi\}}\\ &\frac{\{\phi*M_1\}\mathbf{C}\{\phi*\mathbf{D}(\bar{q})\}\quad \phi\in\text{CM}}{\{\phi*\mathbf{D}(\bar{q})\}\text{while }M[\bar{q}]=1\text{ do }\mathbf{C}\text{ od}\{\phi\wedge M_0\}} \end{aligned}

where “CM” stands for closed under mixtures. i.e., if $\text{dom}(\rho)=\text{dom}(\rho')$ and $\rho\models\phi,\rho'\models\phi$, we have $\forall \lambda\in[0,1],\lambda\rho+(1-\lambda)\rho'\models \phi$.

Proposition: The formulas generated by following grammar are CM:

$\phi,\psi::=p\in\mathcal{AP}\mid\top\mid\bot\mid\phi\wedge\psi\mid\mathbf{U}[S]*\phi$

Structural rules:

\begin{aligned} &\frac{\mathbf{D}[\text{free}(\phi)\cup\text{free}(\phi')]\rightarrow(\phi\rightarrow\phi')\quad \{\phi'\}\mathbf{C}\{\psi'\}\quad\mathbf{D}[\text{free}(\psi)\cup\text{free}(\psi')]\rightarrow(\psi\rightarrow\psi')}{\{\phi\}\mathbf{C}\{\psi\}}\\ &\frac{\{\phi_1\}\mathbf{C}\{\psi_1\}\quad\{\phi_2\}\mathbf{C}\{\psi_2\}}{\{\phi_1\wedge\phi_2\}\mathbf{C}\{\psi_1\wedge\psi_2\}}\\ &\frac{\{\phi_1\}\mathbf{C}\{\psi_1\}\quad\{\phi_2\}\mathbf{C}\{\psi_2\}}{\{\phi_1\vee\phi_2\}\mathbf{C}\{\psi_1\vee\psi_2\}}\\ &\frac{\{\phi\}\mathbf{C}\{\psi\}\quad\text{free}(\mu)\cap\text{var}(\mathbf{C})=\emptyset}{\{\phi\wedge\mu\}\mathbf{C}\{\psi\wedge \mu\}}\\ &\frac{\{\phi\}\mathbf{C}\{\psi\}\quad\text{free}(\mu)\cap\text{var}(\mathbf{C})=\emptyset\quad\text{free}(\psi)\cup\text{var}(\mathbf{C})\subseteq\text{free}(\phi)\text{ or }\psi\in\text{SP}}{\{\phi*\mu\}\mathbf{C}\{\psi*\mu\}} \end{aligned}

​ A formula $\psi$ is called supported, written $\psi\in\text{SP}$, if $[|\psi|]$ is nonempty then it has a least element, or equivalently, there exists a $S\subseteq\mathbf{V}$ such that

• at most one $\rho\in\mathcal{D}(S)$ satisfies $\psi$.
• if $\sigma\models\psi$, $\sigma\succeq \rho$.

​ 其中，条件中的$\rho\models\mathbf{D}[\text{free}(\phi)\cup\text{free}(\phi')]\rightarrow(\phi\rightarrow\phi')$ 前面那个 D，其实就是限定了要求那些满足$\text{free}(\phi)\cup\text{free}(\phi')\subseteq\text{dom}(\rho)$$\rho$ 可以$\rho\models \phi\rightarrow\phi'$

Edited on Views times