年轻人！怎么，对这古老的祖国你不打算出点力？

A Quantum Interpretation of Bunched Logic & Quantum Separation Logic

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

# 关于理解

关于 $\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:

For atomic proposition $\mathbf{D}[S]$ , $\mathbf{D}[S][\mathbf{C}]\triangleq\mathbf{D}[S]$ .
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).
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$ $C = q : = ∣ 0 ⟩$ , 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'$ 。