&\ret (D_\textrm{ext}(\omega),D(\omega),x) }\\
&y\gets N(\gamma)(\delta, x);\\
&\ret (\delta_\textrm{ext}, \delta, y)
\stackrel{\ref{let-binding-step1}}= \monadic{
&\omega\gets \mu_X;\\
&\ret (D_\textrm{ext}(\omega),D(\omega),X(\omega)) }\\
&y\gets N(\gamma)(\delta, x);\\
&\ret (\delta_\textrm{ext}, \delta, y)
&= \monadic{
&\omega\gets \mu_X;\\
&y\gets N(\gamma)(\delta, X(\omega));\\
&\ret (D_\textrm{ext}(\omega),D(\omega),y) }
\stackrel{\ref{let-binding-step2}}= \monadic{
&\omega\gets \mu_Y;\\
&\ret (D_\textrm{ext}(\omega),D(\omega),Y(\omega))
\end{align*}

* Uniform:
suppose (1) $\gamma,D,\calP\vDash \forallrv X\ofty A.~ X\sim \operatorname{Unif}[0,1] \wand Q$.
To show $\weakpre(\unif~[0,1],X\ofty A.Q)$, suppose
and $D_\textrm{ext}:\rv\sembr{\Delta_\textrm{ext}}$.
Let $n$ witness $(D_\textrm{ext},\calP_\textrm{frame}\pdot\calP)$'s finite footprint.
Write the Hilbert cube as $[0,1]^\N\cong [0,1]^n \otimes [0,1]^\N$.
Define $\mu'$ via this isomorphism as the product measure
$\mu|_{[0,1]^n}\otimes\lambda$, where $\lambda$ assigns
to each finite-dimensional box $\prod_{i=1}^n [a_i,b_i]\times[0,1]^\N$
the measure $\prod_{i=1}^n|b_i-a_i|$ and extends to a measure on the whole Hilbert cube
by the Carathéodory extension theorem.
Let $\calP_n$ be the restriction of $\mu'$ to measurable sets of the form
$[0,1]^n \times F\times [0,1]^\N$.
Let $X$ be the projection $\pi_{n+1} = (\dots,\omega_{n+1},\dots)\mapsto\omega_{n+1}$.
By construction, the composite $\calP_\textrm{frame}\pdot\calP\pdot\calP_n$ is defined
and $\calP_\textrm{frame}\pdot\calP\pdot\calP_n\plte(\Sigma_\Omega,\mu')$
and $X$ is $\calP_n$-measurable and uniformly distributed in $[0,1]$.
Therefore $\gamma,(D,X),\calP\pdot\calP_n\vDash Q$ by (1), and it only remains to show

\[
\monadic{
&\omega\gets \mu;\\
&v\gets \unif~[0,1];\\
&\ret (D_\textrm{ext}(\omega), D(\omega), v)
} = \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}(\omega), D(\omega), X(\omega))
\]

\begin{align*}
&\omega\gets \mu;\\
&v\gets \unif~[0,1];\\
&\ret (D_\textrm{ext}(\omega), D(\omega), v)
= \monadic{
&\omega_{1\cdots n}\gets \mu|_{[0,1]^n};\\
&v\gets \unif~[0,1];\\
&\ret (D_\textrm{ext}(\omega_{1\cdots n}), D(\omega_{1\cdots n}), v)
&= \monadic{
&(\omega_{1\cdots n},v)\gets \mu|_{[0,1]^n} \otimes \unif~[0,1];\\
&\ret (D_\textrm{ext}(\omega_{1\cdots n}), D(\omega_{1\cdots n}), v)
= \monadic{
&\omega_{1\cdots n+1}\gets \mu'|_{[0,1]^{n+1}};\\
&\ret (D_\textrm{ext}(\omega_{1\cdots n}), D(\omega_{1\cdots n}), \omega_{n+1})
&= \monadic{
&\omega\gets \mu';\\
&\ret (D_\textrm{ext}(\omega), D(\omega), X(\omega))
\end{align*}

* Flip: analogous to Uniform.

* For:
suppose (1) $\forall i\ofty\N.~\forallrv X\ofty\rv A.~\triple{I(i,X)}M{X'}{I(i+1,X')}$.
We need to show
\[I(1,e)\wand \weakpre(\forloop neM,X\ofty A.~I(n+1,X)).\]

We generalize, and show
\[I(n+1-k,V) \wand \weakpre(\mathrm{loop}(n+1-k,V,M),X'.~I(n+1,X'))\]

for all $V$ and all $0\le k\le n$ by induction on $k$, from which this follows at $k=n$.

* Case $k=0$:

\begin{align*}
\top
I(n+1,V) \wand I(n+1,V)\\
I(n+1,V) \wand \weakpre(\ret V,X'.~I(n+1,X'))\\
I(n+1,V) \wand \weakpre(\mathrm{loop}(n+1,V,M),X'.~I(n+1,X'))\\
I(n+1-k,V) \wand \weakpre(\mathrm{loop}(n+1-k,V,M),X'.~I(n+1,X'))
\end{align*}

* Case $k=j+1\le n$:
backwards reasoning from the goal gives

\begin{align*}
&I(n+1-(j+1),V) \wand \weakpre(\mathrm{loop}(n+1-(j+1),V,M),X'.~I(n+1,X'))\\
&\!\!\dashv I(n-j,V) \wand \weakpre(\mathrm{loop}(n-j,V,M),X'.~I(n+1,X'))\\
&\!\!\dashv I(n-j,V) \wand \weakpre((V'\gets M[n-j/i,V/X];~ \mathrm{loop}(n+1-j,V',M)),X'.~I(n+1,X'))\\
&\!\!\dashv I(n-j,V) \wand \weakpre(M[n-j/i,V/X],V'.~\weakpre(\mathrm{loop}(n+1-j,V',M),X'.~I(n+1,X')))
\end{align*}

Now $I(n-j,V)\wand \weakpre(M[n-j/i,V/X],V'.~I(n-j+1,V'))$ by (1)
so it suffices to show

\begin{align*}
&\weakpre(M[n-j/i,V/X],V'.~ I(n+1-j,V')) \\
\wand &\weakpre(M[n-j/i,V/X],V'.~\weakpre(\mathrm{loop}(n+1-j,V',M),X'.~I(n+1,X'))).
\end{align*}

The outer $\weakpre$s are the same, so by the consequence rule it suffices to show

\begin{align*}
\wand \weakpre(\mathrm{loop}(n+1-j,V',M),X'.~I(n+1,X'))
\end{align*}

for all $V'$, which is exactly the induction hypothesis at $j$.

* If: applying properties of Markov kernels and rules for Let and Ret,

\begin{align*}
&\weakpre(\ite EMN, Z.~Q(Z))\\
&\dashv \weakpre\left(\monadic{
&X\gets M; \\
&Y\gets N; \\
&\ret (\ite EXY)
}, Z.~Q(Z)\right) \\
&\dashv \weakpre\left(M, X.~\weakpre\left(\monadic{
&Y\gets N; \\
&\ret (\ite EXY)
}, Z.~Q(Z)\right)\right) \\
&\dashv \weakpre(M, X.~\weakpre(N,Y.~
\weakpre(\ret (\ite EXY), Z.~Q(Z)))) \\
&\dashv \weakpre(M, X.~\weakpre(N,Y.~ Q(\ite EXY)))
\end{align*}

as desired.

The following $\weakpre$ laws hold:

(M,X.(N,Y.Q)) ⊢(XMN,Y.Q)
(XA.  X∼Unif[0,1]Q) ⊢(,XA.Q)
(XA.  X∼pQ) ⊢( p,XA.Q)
I(1,e) * (∀i. XA. I(i,X)MX'I(i+1,X'))
⊢(neiXM,XA. I(n+1,X))

(M,XA. (N,YA.  Q(EXY)))
⊢(EMN,XA. Q)

Unfold $\sembr-$ and apply lemma <ref>.

The following proof rules hold:

*[right=H-Frame $(X\notin F)$]PMXQF*PMXF*Q
*[right=H-Ret] Q[M/X]MXQ
X. QNYR
*[right=H-Uniform] ⊤XX∼ [0,1])
*[right=H-Flip] ⊤ pXX∼p
∀i. XA. I(i,X)MX'I(i+1,X')
P M X Q(X)

X. Q(X) N Y R(EXY)

Rules H-Consequence, H-Frame, and H-Disjunction
follow from Lemma <ref>;
the remaining rules follow from Corollary <ref>.
All proofs go by unfolding the definition of the Hoare triple
and applying the relevant $\weakpre$ law.

§.§ Disintegration

Let $(M,\pdot,\plte,1)$ be a KRM with $1\plte x$ for all $x$.
Let $A$ be a downward-closed subset of $M$ (i.e., $x\plte y\in A$ implies $x\in A$).
Let $(\pdot')$ be the restriction of $(\pdot)$ to $A$; that is,

\begin{align*}
x \pdotp y := \begin{cases}
x\pdot y, & x\pdot y\in A\\
\mathrm{undefined}, & \textrm{otherwise}
\end{cases}
\end{align*}

Then $(A,\pdot',\plte,1)$ is a KRM.

Unit and commutativity are straightforward.
For associativity, note that if $1\plte x$ for all $x$
then by monotonicity of $(\pdot)$ we have $x\plte x\pdot y$ for all $x,y$.
Now suppose $x\pdotp y$ defined and $(x\pdotp y)\pdotp z$ defined.
Then $(x\pdot y)\pdot z \in A$ and by downward closure so is $y\pdot z$
and by associativity so is $x\pdot (y\pdot z)$, so both $y\pdotp z$ and $x\pdotp (y\pdotp z)$
are defined and associativity is inherited from associativity of $(\pdot)$.

Let $\Mdis$ be the set of countably-generated probability spaces $\calP$ that have finite footprint
and can be extended to a Borel measure on the entire Hilbert cube.
The restriction of the KRM given by Theorem <ref> to $\Mdis$ is still a KRM.

By Lemma <ref>,
the restriction to $\Mfin$ is a KRM, so it suffices to show that restricting to
countably-generated spaces that can be extended to a Borel measure still yields a KRM.
First, restricting to countably-generated spaces still yields a KRM because
the independent combination of two countably-generated spaces remains couuntably-generated.
Then, the restriction to spaces that can be extended to a Borel measure
still yields a KRM by Lemma <ref>,
as the set of spaces that can be extended to a Borel measure is downward-closed.

Γ;Δ⊢_xAE P

$\gamma,D,\calP\vDash \D_{x\ofty A\gets E} P$     iff     for all $(\Sigma_\Omega,\mu)\sqsupseteq \calP$

and all $(\Sigma_\Omega,\mu)$-disintegrations
$\{\nu_x\}_{x\in A}$ with respect to $E(\gamma)\circ D$

and $(E\circ D)_*\mu$-almost-all $x\in A$,

$(\gamma,x),D,\nu_x|_\calP\vDash P$

If $\mu$ and $\nu$ are probability measures on a space $(\Omega,\calF)$
generated by a $\pi$-system $\calB$, then
$\mu=\nu$ iff $\mu(B)=\nu(B)$ for all $B\in\calB$.

The left-to-right direction is straightforward.
The right-to-left direction follows from the $\pi$-$\lambda$ theorem:
the set $S:=\{B\in\calB\mid \mu(B)=\nu(B)\}$
is a $\lambda$-system
and $\mu$ and $\nu$ agree on a $\pi$-system that generates $\calF$ by assumption.

$\displaystyle\own E * P \vdash \D_{x\ofty A\gets E} P$.

Suppose $\gamma,D,\underbrace{\calP_E\pdot\calP_P}_\calP\vDash\own E*P$
and $\gamma,D,\calP_E\vDash \own E$
and (1) $\gamma,D,\calP_P\vDash P$.
To show $\D_{x\gets E}P$, suppose
and let $\{\nu_x\}_{x\in A}$ be a $\mu$-disintegration with respect to $E(\gamma)\circ D$.
We need to show $(\gamma,x),D,\nu_x|_\calP\vDash P$ for almost all $x\in A$.
Since $x\notin P$, $(\gamma,x),D,\nu_x|_\calP\vDash P$ is equivalent to
$\gamma,D,\nu_x|_\calP\vDash P$,
so by
assumption (1) and monotonicity it suffices to show $\nu_x|_{\calP_P} = \calP_P$ for almost all $x\in A$.

Write $\calP_P=(\calF_P,\mu_P)$ and
let $S:=\{x\in A\mid \nu_x|_{\calF_P} = \mu_P\}$.
It's enough to show that $S$ is $\Sigma_A$-measurable and has probability $1$.
Let $\calB=\{B_n\}_{n\in\N}$ be a countable basis of $\calF_P$; without loss of generality we may
assume $\calB$ is a $\pi$-system because any countable collection of sets has countable closure
under finite intersections.
By lemma <ref>, we can write $S$ as the countable intersection
$S=\bigcap_{n\in\N}S_n$ where $S_n := \{x\in A\mid \nu_x(B_n) = \mu_P(B_n)\}$.
Because $\sigma$-algebras are closed under countable intersections and measures are countably
subadditive, $S$ is measurable with probability $1$ if each $S_n$ is.

Each $S_n$ is $\Sigma_A$-measurable:
$S_n$ is equal to the preimage of the singleton set $\{\mu_P(B_n)\}$
under the map $\nu_{(-)}(B_n)$; since $\nu$ is a Markov kernel and singletons are Borel,
this preimage must be
It only remains to show each $S_n$ has probability $1$.
Now, suppose for the sake of contradiction that there is some $k$ such that $S_k$ does not have probability $1$,
so $\nu_x(B_n)\ne \mu_P(B_n)$ for all $x\in N:=A\setminus S_k$.
We can write $N$ as a disjoint union of two subsets $N_<$ and $N_>$, defined as follows:

\begin{align*}
N_< &:= \{x\in N\mid \nu_x(B_n) < \mu_P(B_n)\} \\
N_> &:= \{x\in N\mid \nu_x(B_n) > \mu_P(B_n)\}
\end{align*}

These are both measurable, since they can be written as preimages of $[0,\mu_P(B_n))$
and $(\mu_P(B_n),1]$ under $\nu_{(-)}(B_n)$.
Because $N$ has nonzero probability, at least one of $N_<$ or $N_>$ must have nonzero probability too.
Suppose it's $N_<$; the case where $N_>$ has nonzero probability is analogous.
Because $\nu$ is a disintegration of $\mu$ with respect to $E(\gamma)\circ D$, we have

\[
\Ex_{\omega\sim\mu}f(\omega) = \Ex_{x\sim (E(\gamma)\circ D)_*\mu}\Ex_{\omega\sim\nu_x}f(\omega)
\]

for all $f:\Omega\mto\R_{\ge 0}$. Choose $f(\omega):=\ind[\omega\in B_n]\ind[E(\gamma)(D(\omega))\in N_<]$.
Then simplifying LHS gives

\begin{align*}
\Ex_{\omega\sim\mu}f(\omega)
\Ex_{\omega\sim\mu}\ind[\omega\in B_n]\ind[E(\gamma)(D(\omega))\in N_<]\\
\Ex_{\omega\sim\mu}\ind[\omega\in B_n]\Ex_{\omega\sim\mu}\ind[E(\gamma)(D(\omega))\in N_<]\\
\mu(B_n)(E(\gamma)\circ D)_*\mu(N_<)
\end{align*}

Step (a) uses independence of $B_n$ and $(E(\gamma)\circ D)^{-1}(N_<)$:
$\calP_E\pdot\calP_P$ defined and $B_n\in\calP_P$ and $(E(\gamma)\circ D)^{-1}(N_<)\in\calP_E$.
Meanwhile, simplifying RHS gives

\begin{align*}
\Ex_{x\sim (E(\gamma)\circ D)_*\mu}\Ex_{\omega\sim\nu_x} f(\omega)
\Ex_{x\sim (E(\gamma)\circ D)_*\mu}\Ex_{\omega\sim\nu_x}
\ind[\omega\in B_n]\ind[E(\gamma)(D(\omega))\in N_<]\\
\Ex_{x\sim (E(\gamma)\circ D)_*\mu} \Ex_{\omega\sim\nu_x}\ind[\omega\in B_n] \ind[x\in N_<]\\
&= \Ex_{x\sim (E(\gamma)\circ D)_*\mu} \ind[x\in N_<] \Ex_{\omega\sim\nu_x}\ind[\omega\in B_n] \\
&= \Ex_{x\sim (E(\gamma)\circ D)_*\mu} \ind[x\in N_<] \nu_x(B_n) \\
&\hspace{-0.3em}\stackrel{(b)}< \Ex_{x\sim (E(\gamma)\circ D)_*\mu} \ind[x\in N_<] \mu_P(B_n) \\
&= \mu_P(B_n)\Ex_{x\sim (E(\gamma)\circ D)_*\mu}\ind[x\in N_<] \\
&= \mu_P(B_n)(E(\gamma)\circ D)_*\mu(N_<)\\
&= \mu(B_n)(E(\gamma)\circ D)_*\mu(N_<)
\end{align*}

Step (a) holds because $(E(\gamma)\circ D)_*\nu_x(\{x\}) = 1$ for almost all $x$.
Step (b) holds because the expectation is taken over $x\in N_<$,
where the inequality holds by assumption; the inequality remains strict because $N_<$ is
Putting these two together gives $\mathrm{LHS}=\mathrm{RHS}$ and $\mathrm{LHS}<\mathrm{RHS}$, a

The following entailment holds:

\[
\Ex[e[X/x]] = v ~~\land~~ \D_{x:A\gets X} \Ex[E] = e ~~~\vdash~~~ \Ex[E] = v
\]

Fix $(\gamma,D,\calP)$.
By the first conjunct $\Ex_{\omega\sim\calP} e(\gamma,X(\gamma)(D(\omega))) = v(\gamma)$.
By assumption, $\calP$ extends to a Borel measure $\mu$ on the Hilbert cube.
By the disintegration theorem, there exists at least one $\mu$-disintegration
with respect to $X(\gamma)\circ D$; call it $\{\nu_x\}_{x\in A}$.
By the second conjunct $\Ex_{\omega\sim\nu_x}[E(\gamma)(D(\omega))] = e(\gamma,x)$ for almost all $x\in A$.
This along with the existence of the disintegration $\nu$ implies

\begin{align*}
\Ex_{\omega\sim\calP} E(\gamma)(D(\omega))
= \Ex_{x\sim {(X(\gamma)\circ D)}_*\mu} \Ex_{\omega\sim\nu_x} E(\gamma)(D(\omega))
= \Ex_{x\sim {(X(\gamma)\circ D)}_*\mu} e(\gamma,x)
= \Ex_{\omega\in\mu} e(\gamma,X(\gamma)(D(\omega)))
= v(\gamma)
\end{align*}

as desired.

The following entailments hold:

*[lab=C-Entail]P ⊢  Q_xE P ⊢  _xE Q
*[lab=]E * P  ⊢  _xE P

⊢_xX (E E[x/X] )

_xX [E] = e  [e[X/x]] = v
⊢ [E] = v

and C-Total-Expectation follow from lemmas
<ref> and <ref> respectively.

* C-Entail: suppose $P\vdash Q$ and $\gamma,D,\calP\vDash \D_{x\ofty A\gets E}P$.
Let $\{\mu_x\}_{x\in A}$ be a disintegration of $\calP$ with respect to $E(\gamma)\circ D$;
let $\{\calP_x\}_{x\in A}$ be the corresponding restrictions of $\{\mu_x\}_{x\in A}$ to $\calP$.
By assumption, $\gamma,D,\calP_x\vDash P$ for almost-all $x\in A$.
Since $P\vdash Q$, this implies $\gamma,D,\calP_x\vDash Q$ for almost-all $x\in A$ as desired.

* C-Subst:
Fix $(\gamma,D,\calP)$.
Let $\{\mu_x\}_{x\in A}$ be a disintegration of $\calP$ with respect to $E(\gamma)\circ D$.
Let $E_x$ be the event that $E(\gamma)\circ D$ and $E[x/X](\gamma)\circ D$ agree.
We need to show that $E_x$ holds almost-surely with respect to $\mu_x$ for almost all $x\in A$.
By the definition of disintegration,
the event $\{\omega \mid X(\omega) = x\}$ has probability $1$ under $\mu_x$
for almost all $x$. Since
$\{\omega\mid X(\omega) = x\} \subseteq \{\omega \mid E(\gamma)(D\omega) = E[x/X](\gamma)(D\omega)\} =E_x$
this implies $\mu_x(E_x)=1$ for almost-all $x$ as desired.

The following entailments hold:

* Necessitation: if $\vdash P$ then $\displaystyle\vdash \D_{x\gets X}P$.

* Distribution: $\displaystyle\D_{x\gets X}(P\to Q)\vdash \D_{x\gets X} P\to \D_{x\gets X}Q$.

* Distributes over $(\land)$: $\displaystyle\D_{x\gets X} (P\land Q) \vdashiff \D_{x\gets X} P \land
\D_{x\gets X} Q$.

* Semidistributes over $(\lor)$: $\displaystyle\D_{x\gets X} P \lor \D_{x\gets X} Q \vdash \D_{x\gets
X} (P\lor Q)$.

* Necessitation: if $P$ holds in all configurations
then it holds for all disintegrated configurations as well.

* Distribution: it suffices to show $D_{x\gets X}(P\to Q)\land \D_{x\gets X}P\vdash \D_{x\gets X}Q$.
By C-And the premise is equivalent to $\D_{x\gets X}((P\to Q)\land P)$;
the result then follows from C-Entail
via the entailment $(P\to Q)\land P\vdash Q$.

* Distributes over $(\land$):
the left-to-right direction follows from C-Entail
via the entailments $P\land Q\vdash P$ and $P\land Q\vdash Q$.
For the right-to-left entailment, suppose $\gamma,D,\calP\vDash \D_{x\gets E} P$
and $\gamma,D,\calP\vDash \D_{x\gets E} Q$
and let $\{\mu_x\}_{x\in A}$ be a disintegration of $\calP$ with respect to $E(\gamma)\circ D$;
let $\{\calP_x\}_{x\in A}$ be the corresponding restrictions of $\{\mu_x\}_{x\in A}$ to $\calP$.
By assumption, there are two sets $F_1,F_2\subseteq A$ of measure $1$
such that $\gamma,D,\calP_x\vDash P$ for all $x\in F_1$
and $\gamma,D,\calP_x\vDash Q$ for all $x\in F_2$.
Therefore, $\gamma,D,\calP_x\vDash P\land Q$ for all $x\in F_1\cap F_2$.
Moreover, $F_1\cap F_2$ has measure $1$ by subadditivity,
so $\gamma,D,\calP_x\vDash P\land Q$ for almost-all $x$ as desired.

* Semidistributes over $(\lor)$:
it suffices to show $\D_{x\gets X} P\vdash \D_{x\gets X}(P\lor Q)$
and $\D_{x\gets X}Q\vdash \D_{x\gets X}(P\lor Q)$.
These follow from C-Entail via the entailments
$P\vdash P\lor Q$ and $Q\vdash P\lor Q$ respectively.

§ ANNOTATED <REF> PROGRAM

\begin{align*}
&\assertc{ \top }\\
&\hspace{1em}\appllet Z \appleq \flip~1/2 \applin \\
&\assertc{ Z \sim \ber 1/2 }\\
&\hspace{1em}\appllet X \appleq \flip~1/2 \applin \\
&\assertc{ Z \sim \ber 1/2 ~~*~~  X\sim\ber 1/2 }\\
&\hspace{1em}\appllet Y \appleq \flip~1/2 \applin \\
&\assertc{ Z \sim \ber 1/2 ~~*~~  X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2 }\\
&\hspace{1em}\appllet A \appleq X~\applkw{||}~Z \applin \\
&\assertc{ Z \sim \ber 1/2 ~~*~~  X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2
~~*~~ A\asequal (X\lor Z) }\\
&\hspace{1em}\appllet B \appleq Y~\applkw{||}~Z \applin \\
&\assertc{ Z \sim \ber 1/2 ~~*~~  X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2
~~*~~ A\asequal (X\lor Z) ~~*~~ B\asequal (Y\lor Z)}\\
&\hspace{1em}\applret (Z, X, Y, A, B) \\
&\assertc{ \D_{z\gets Z}  \left(X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2
~~*~~ A\asequal (X\lor Z) ~~*~~ B\asequal (Y\lor Z)\right)}~(\DIndep)\\
&\assertc{ \D_{z\gets Z}  \underbrace{\left(X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2
~~*~~ A\asequal (X\lor z) ~~*~~ B\asequal (Y\lor z)\right)}_P}~(\textsc{C-Subst})\\
&\assertc{ \D_{z\gets Z} \left((z = \vtrue\to P[\vtrue/z]) \land (z=\vfalse\to P[\vfalse/z])\right)} \\
&\assertc{ \D_{z\gets Z} \left(
\begin{aligned}
&(z = \vtrue~~\to~~ X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2
~~*~~ A\asequal (X\lor \vtrue) ~~*~~ B\asequal (Y\lor \vtrue)) ~~\land \\
&(z=\vfalse ~~\to~~
X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2
~~*~~ A\asequal (X\lor \vfalse) ~~*~~ B\asequal (Y\lor \vfalse))
\end{aligned}\right)} \\
&\assertc{ \D_{z\gets Z} \left(
\begin{aligned}
&(z = \vtrue~~\to~~ A\asequal \vtrue ~~*~~ B\asequal \vtrue) ~~\land\\
&(z=\vfalse ~~\to~~
X\sim\ber 1/2 ~~*~~ Y\sim\ber 1/2
~~*~~ A\asequal X ~~*~~ B\asequal Y)
\end{aligned}\right)} \\
&\assertc{ \D_{z\gets Z} \left(
\begin{aligned}
&(z = \vtrue~~\to~~ \own A ~~*~~ \own B) ~~\land \\
&(z=\vfalse ~~\to~~ A\sim\ber 1/2 ~~*~~ B\sim\ber 1/2)
\end{aligned}\right)} \\
&\assertc{ \D_{z\gets Z} \left(
\begin{aligned}
&(z = \vtrue\to \own A * \own B) ~~\land\\
&(z=\vfalse \to \own A * \own B)
\end{aligned}\right)} \\
&\assertc{ \D_{z\gets Z} \left(\own A * \own B\right) }
\end{align*}

§ AN EXAMPLE OF CONDITIONAL INDEPENDENCE VIA CONTROL FLOW

\begin{align*}
&\assertc{ \top }\\
&\hspace{1em}\appllet Z \appleq \flip~1/2 \applin \\
&\assertc{ Z \sim \ber 1/2 }\\
&\hspace{1em}\applif~Z~\applthen \\
&\hspace{1em}\hspace{2em}\appllet X_1 \appleq \flip~p \applin \\
&\hspace{2em}\assertc{ X_1 \sim \ber p }\\
&\hspace{1em}\hspace{2em}\appllet Y_1 \appleq \flip~p \applin \\
&\hspace{2em}\assertc{ X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p }\\
&\hspace{1em}\hspace{2em}\applret (Z,X_1,Y_1) \\
&\hspace{1em}\applelse \\
&\hspace{2em}\assertc{ \existsrv~X_1~Y_1.~~X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p }\\
&\hspace{1em}\hspace{2em}\appllet X_2 \appleq \flip~q \applin \\
&\hspace{2em}\assertc{ \left(\existsrv~X_1~Y_1.~~X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p\right)
~~*~~ X_2 \sim \ber q }\\
&\hspace{1em}\hspace{2em}\appllet Y_2 \appleq \flip~q \applin \\
&\hspace{2em}\assertc{ \left(\existsrv~X_1~Y_1.~~X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p\right)
~~*~~ X_2 \sim \ber q ~~*~~ Y_2 \sim \ber q }\\
&\hspace{1em}\hspace{2em}\applret (Z,X_2,Y_2) \\
\begin{aligned}
&Z \sim \ber 1/2 ~~*~~ \existsrv~X_1~Y_1~X_2~Y_2.~~ X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p
~~*~~ X_2 \sim \ber q ~~*~~ Y_2 \sim \ber q ~~*~~ \\
&X \asequal (\ite Z{X_1}{X_2}) ~~*~~ Y \asequal (\ite Z{Y_1}{Y_2})
\end{aligned}}\\
\D_{z\gets Z}\left( \existsrv~X_1~Y_1~X_2~Y_2.~~
\begin{aligned}
&X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p
~~*~~ X_2 \sim \ber q ~~*~~ Y_2 \sim \ber q ~~*~~ \\
&X \asequal (\ite Z{X_1}{X_2}) ~~*~~ Y \asequal (\ite Z{Y_1}{Y_2})
\end{aligned}\right)}~(\DIndep)\\
\D_{z\gets Z}\underbrace{\left( \existsrv~X_1~Y_1~X_2~Y_2.~~
\begin{aligned}
&X_1 \sim \ber p ~~*~~ Y_1 \sim\ber p
~~*~~ X_2 \sim \ber q ~~*~~ Y_2 \sim \ber q ~~*~~ \\
&X \asequal (\ite z{X_1}{X_2}) ~~*~~ Y \asequal (\ite z{Y_1}{Y_2})
\end{aligned}\right)}_P}~(\textsc{C-Subst})\\
\D_{z\gets Z}\left(
\begin{aligned}
&(z=\vtrue ~~\to~~ P[\vtrue/z]) ~~\land \\
&(z=\vfalse ~~\to~~ P[\vfalse/z])
\end{aligned}\right)}\\
\D_{z\gets Z}\left(
\begin{aligned}
&(z=\vtrue ~~\to~~ \existsrv~X_1~Y_1.~~X_1\sim\ber p~~*~~ Y_1\sim\ber p
~~*~~ X\asequal X_1
~~*~~ Y\asequal Y_1) ~~\land\\
&(z=\vfalse ~~\to~~ \existsrv~X_2~Y_2.~~X_2\sim\ber q~~*~~ Y_2\sim\ber q
~~*~~ X\asequal X_2
~~*~~ Y\asequal Y_2)
\end{aligned}\right)}\\
\D_{z\gets Z}\left(
\begin{aligned}
&(z=\vtrue ~~\to~~ X\sim\ber p~~*~~ Y\sim\ber p) ~~\land\\
&(z=\vfalse ~~\to~~ X\sim\ber q~~*~~ Y\sim\ber q)
\end{aligned}\right)}\\
\D_{z\gets Z}\left(
\begin{aligned}
&(z=\vtrue ~~\to~~ \own X ~~*~~ \own Y) ~~\land\\
&(z=\vfalse ~~\to~~\own X ~~*~~ \own Y)
\end{aligned}\right)}\\
&\assertc{ \D_{z\gets Z}(\own X * \own Y) }\\
\end{align*}

§ PROVING A WEIGHTED SAMPLING ALGORITHM CORRECT (FULL)

\begin{align*}
&1~\,\appllet W \appleq \applret(w_1+\dots+w_n) \applin \\
&2~\,\appllet (v_1,\dots,v_n) \appleq \applret(w_1/W,\dots,w_n/W)\applin \\
&3~\,\appllet U \appleq \applunif \applin \\
&4~\,\applforopen n0iJ{\\
&5~\,\hspace{1em}\applif~v_1+\dots+v_{i-1} \le U < v_1 + \dots + v_i \\
&6~\,\hspace{1em}\applthen~\applret i \\
&7~\,\hspace{1em}\applelse~\applret J}\applforclose
\end{align*}

Naive linear-space implementation of weighted sampling.

\begin{align*}
&1~\,\appllet w \appleq \applret\applarray{w_1,\dots,w_n} \applin \\
&2~\,\appllet M \appleq \applret (-\infty) \applin \appllet K \appleq \applret(0)\applin \\
&3~\,\applforopen n{\appltuple{M,K}}i{\appltuple{M,K}}{\\
&4~\,\hspace{1em}\appllet S \appleq\applunif \applin \\
&5~\,\hspace{1em}\appllet U \appleq \applret(S\applexp\applpar{1\applkw{/}\applindex wi})\applin \\
&7~\,\hspace{1em}\applthen~\applret \appltuple{U,i}\\
&8~\,\hspace{1em}\applelse~\applret \appltuple{M,K}}\applforclose
\end{align*}

Constant-space version.

xmin = 0, xmax = 1,
ymin = 0, ymax = 1]
domain = 0:1,
samples = 100,
] x;
domain = 0:1,
samples = 100,
] x^(1/4);
domain = 0:1,
samples = 100,
] x^4;

at (1,1) [rotate=40] $w=1$;
at (0.4,1.5) [rotate=40] $w=4$;
at (1.4,0.5) [rotate=40] $w=\frac{1}{4}$;

Visualization of the function $f(x)=x^{1/w}$.

Weighted sampling example. The constants $w_i$ are inputs.

To exercise Lilac's support for conditional reasoning, continuous random variables,
and substructural handling of independence, we now prove a sophisticated
constant-space weighted sampling algorithm correct using Lilac.  Suppose
you are given a collection of items $\{x_1, \dots, x_n\}$ each with associated
weight $w_i \in \mathbb{R}^+$.  The task is to draw a sample from the collection
$\{x_i\}$ in a manner where each item is drawn with probability proportional to
its weight. This problem is an instance of reservoir
sampling <cit.>, and is an important primitive in
distributed systems.

First, we consider a naive solution
that requires space linear in the number of weights; pseudocode
for this algorithm is presented in Figure <ref>. The first
pass over the weights occurs on Line 1, which computes the normalizing constant
$W=\sum_i w_i$. Line 2 then divides each weight by $W$ so that the result
$(v_1,\dots,v_n)$ forms a probability distribution.
This distribution can be thought of as a partitioning of the interval $[0,1]$
into $n$ subintervals
with lengths $(v_1,\dots,v_n)$; to sample from it
we can choose a point $U$ uniformly at random from $[0,1]$ (Line 3)
and select the item corresponding to the subinterval that $U$ lands in (Lines 4–7).

While simple to understand and implement, this naive approach has a critical
flaw that makes it inappropriate for application in large-scale systems: it requires storing
all previously encountered weights and scanning over them before a single sample can be
drawn, and so does not scale to a streaming setting where new weights are acquired
one at a time (for instance, as each user visits a website). To fix this
limitation, <cit.> proposed the very clever
constant-space solution presented in Figure <ref>. The
core of this approach is to generate a value $S$ uniformly at random from $[0,1]$ on every
iteration (Line 3), perturb $S$ according to the next weight $w_i$ in the stream
(Line 4), and track only the greatest perturbed sample (Lines 5–8). Figure <ref>
gives some intuition for the perturbed quantity $S^{1/w_i}$ on Line 4: if $w_i$
is large (i.e., item $i$ has high weight), then $S^{1/w_i}$ is likely to be large (visualized
by the curve $w=4$); if $w_i$ is small, then $S^{1/w_i}$ is likely to be small (visualized
by the curve $w=1/4$).
The fact that this program is equivalent to the naive one is quite surprising,
and proving it requires the simultaneous application of several important theorems from
probability theory. We show how this can be done formally in Lilac
in a manner similar to a typical informal proof.
Correctness is captured by the following Lilac postcondition:

\begin{align}
{\forall k. \Pr(K=k) = \frac{w_k}{\sum_j w_j}}
\label{eq:post-full}
\end{align}

To establish this postcondition, a typical informal proof
begins by declaring mutually independent, uniformly distributed random variables $\{S_i\}_{1\le i\le n}$,
where $S_i$ denotes the value sampled by Line 4 on the $i$th loop iteration,
and a random variable $K=\argmax_i S_i^{1/w_i}$ that denotes the final result.
Implicit in this setup are the assumptions that each $S_i$ produced by the program is actually
independent and uniformly distributed, and that the for-loop actually computes
the specified $\argmax$. We can formally establish this
by mechanically applying the proof rules described in Section <ref>
to conclude the following at program termination:

\begin{align}
\existsrv S_1 \dots S_n.~\hugestar_i S_i \sim \mathrm{Unif}~[0,1] ~~*~~
K \asequal \argmax_i S_i^{1/w_i}}
\label{eq:post-full1}
\end{align}

The proof makes use of the following
invariant $I_j$ for the loop on
Line 2, which must hold immediately before the execution of the $j$th iteration for all $1\le j\le n+1$:

\begin{align}
I_j \hspace{0.75em}:=\hspace{0.75em} {
\existsrv S_1 \dots S_j.~~ \hugestar_{1\le i< j}~ S_i \sim \mathrm{Unif}~[0,1]
\hspace{0.5em}*\hspace{0.5em} K \asequal \argmax_{1\le i<j} S_i^{1/w_i}
\hspace{0.5em}*\hspace{0.5em} M \asequal \max_{1\le i<j} S_i^{1/w_i}  }
\label{eq:loopinv1-full}
\end{align}

The proof that our program maintains this invariant is completely standard for separation logics,
so we elide the details and focus on the challenge of
deriving the desired post-condition (<ref>) given the
setup (<ref>).
To show (<ref>) in the case $i=k$,
note that

\begin{align}
\Pr(K=k) = \Pr\left(S_k^{1/w_k} > S_j^{1/w_j} \text{ for all } j \ne k\right),
\end{align}

since $K$ is defined to be the $\argmax$ of $j$ over all $S_j^{1/w_j}$.
This is an unwieldy probability to compute directly. The trick is to use conditioning:
in this case, fixing $S_k$ to a deterministic $s_k$ gives

\begin{align}
\Pr(K=k \mid S_k = s_k) &= \Pr\left(s_k^{1/w_k} > S_j^{1/w_j} \text{ for all } j \ne k\right) \label{eq:eqset1:start-full} \\
&= \Pr\left(s_k^{w_j/w_k} > S_j \text{ for all } j \ne k\right) & \text{Exponentiating} \\
&= \prod_{j \ne k} \Pr\left(s_k^{w_j/w_k} > S_j\right) & \text{By conditional independence} \label{eq:indep-ex-full}\\
&= \prod_{j \ne k} s_k^{w_j/w_k} & S_j\text{ uniform}\footnotemark \\
&= \pow{s_k}{\frac{\sum_{j\ne k} w_j}{w_k}}.\label{eq:eqset1:end-full}
\end{align}

If $U$ uniform in $[0,1]$ then $\Pr(u > U) = u$.
Formally, this calculation occurs under the modality $\D_{s_k\gets S_k}$, which is introduced via .
The expression $\Pr(E)$ abbreviates $\Ex[\ind[E]]$, the expectation of the indicator random variable $\ind[E]$.[
If $E$ is an event then the random variable $\ind[E]$ is $1$ if $E$ holds and $0$ otherwise.]
A critical step occurs in Equation <ref>: each
$S_j$ is conditionally independent from all others given $S_k = s_k$. This
permits a critical simplification: the probability of the conjunction becomes a
product of simpler probabilities. This is an application of the derived rule

\begin{align}
\tag{\textsc{Indep-Prod}}
\hugestar_i \own E_i ~~~\vdash~~~ \Pr\Big( \bigcap_i E_i \Big) = \prod_i \Pr(E_i),
} \label{eq:indep-prod-full}
\end{align}

an immediate consequence of Lemma <ref>.
Note that our modal treatment of conditioning leads to a nice separation of concerns here.
Because $\D$ respects entailment, facts like <ref> that appear to be
only about unconditional independence and unconditional
probability are automatically lifted to facts like Equation (<ref>),
with the expected conditional reading.

Finally, to complete the proof we connect the conditional
$\Pr(K=k \mid S_k = s_k)$ to the unconditional $\Pr(K=k)$
using the law of total expectation:

\begin{align}
\Pr(K=k)
&= \Ex\left[\Pr(K=k\mid S_k)\right] & \text{Law of Total Expectation}\label{eq:eqset2:start-full}\\
&= \Ex\left[\pow{S_k}{\frac{\sum_{j\ne k} w_j}{w_k}}\right] & \text{By }(\ref{eq:eqset1:end-full})\\
&= \left(\frac{\sum_{j\ne k} w_j}{w_k} + 1\right)^{-1} & \text{$S_k$ uniform}\footnotemark\\
&= \frac{w_k}{\sum_j w_j}.\label{eq:eqset2:end-full}
\end{align}

Unlike the calculation in Equations <ref>–<ref>,
which take place inside the modality $\D_{s_k\gets S_k}$,
this second calculation (Equations <ref>–<ref>) takes place outside
of it, as it computes the unconditional probability $\Pr(K=k)$.
The gap between the two calculations is bridged by
the following instantiation of C-Total-Expectation:

\begin{align*}
\D_{s_k \gets S_k} \Big(\Ex[\underbrace{\ind[K=k]}_{E}]
= \underbrace{\pow{s_k}{\frac{\sum_{j \ne k}{w_j}}{w_k}}}_{e} \Big)
\land
\Big(
\Ex\Big[\underbrace{\mathrm{pow}\Big(S_k, \frac{\sum_{j \ne k} w_j}{w_k} \Big)}_{e[S_k/s_k]}\Big]
\underbrace{\frac{w_k}{\sum_j w_j}}_{v}
\Big)
\Ex[\underbrace{\ind[K=k]}_{E}] = \underbrace{\frac{w_k}{\sum_j w_j}}_{v}
\end{align*}

If $U$ uniform in $[0,1]$ then $\Ex[U^\alpha] = 1/({\alpha + 1})$.
Putting all this together yields a formal proof of correctness in Lilac.
The next page gives a fully annotated program.

\begin{align*}
&\assert{\{ \top \}}\\
&\hspace{1em}\appllet W \appleq \applret\applarray{w_1,\dots,w_n} \applin \\
&\assert{\{ W \asequal (w_1,\dots,w_n) \}}\\
&\hspace{1em}\appllet M \appleq \applret(-\infty) \applin \\
&\assert{\{ W \asequal (w_1,\dots,w_n) ~~*~~ M\asequal -\infty  \}}\\
&\hspace{1em}\appllet K \appleq \applret 0 \applin \\
&\assert{\{ W\asequal (w_1,\dots,w_n) ~~*~~ M\asequal -\infty ~~*~~ K\asequal 0 \}}\\
&\assert{\text{Let } \begin{aligned}
\quad:=\quad\left(\begin{aligned}
&W \asequal (w_1,\dots,w_n) ~~*~~ 1\le i\le n ~~*~~\\
&\exists S_1 \dots S_i.~~ \hugestar_{1\le j< i}~ S_j \sim \mathrm{Unif}~[0,1]
\hspace{0.3em}*\hspace{0.3em} K \asequal \argmax_{1\le j<i} S_j^{1/w_j}
\hspace{0.3em}*\hspace{0.3em} M \asequal \max_{1\le j<i} S_j^{1/w_j}
\end{aligned}\right)
\end{aligned}}\\
&\assert{\{ I(1,M,K) \}}\\
&\hspace{1em}\applforopen n{\appltuple{M,K}}i{\appltuple{M,K}}{\\
&\hspace{1em}\assert{\{ I(i,M,K) \}}\\
&\hspace{1em}\hspace{1em}\appllet S \appleq\applunif \applin \\
&\hspace{1em}\assert{\{ I(i,M,K) ~~*~~ S\sim\unif~[0,1] \}}\\
&\hspace{1em}\hspace{1em}\appllet U \appleq \applret(S\applexp\applpar{1\applkw{/}\applindex wi}) \applin \\
&\hspace{1em}\assert{\{ I(i,M,K) ~~*~~ S\sim\unif~[0,1] ~~*~~ U\asequal S^{1/w_i} \}}\\
&\hspace{1em}\hspace{1em}\applthen~\applret \appltuple{U,i}\\
&\hspace{1em}\hspace{1em}\applelse~\applret \appltuple{M,K}}\applforclose\\
&\hspace{1em}\assertc{ (M',K').\hspace{1em}
\begin{aligned}
&I(i,M,K) ~~*~~ S\sim\unif~[0,1] ~~*~~ U\asequal S^{1/w_i} ~~*~~ \\
&M' \asequal \max(U,M) ~~*~~ U' \asequal \ite{U>M}iK
\end{aligned}
&\hspace{1em}\assert{\{ (M',K').~~ I(i+1,M',K') \}}\\
&\assert{\{ (M',K').~~I(n+1,M',K') \}}\\
\existsrv S_1 \dots S_n.~\hugestar_i S_i \sim \mathrm{Unif}~[0,1] ~~*~~
K \asequal \argmax_i S_i^{1/w_i}}\\
&\assertc{\forall k. \Pr(K=k) = \frac{w_k}{\sum_j w_j}}
\end{align*}

To illustrate the proof of the final entailment,
we animate the proof state at each step in inference-rule notation,
in the style of interactive theorem provers such as Coq.
First we work backwards from the goal:

_i S_i ∼Unif [0,1]
K _i S_i^1/w_i
[K=k]=w_k/∑_j w_j

_i S_i ∼Unif [0,1]
K _i S_i^1/w_i
[∀jk. S_k^1/w_k> S_j^1/w_j]=w_k/∑_j w_j

_i S_i ∼Unif [0,1]
K _i S_i^1/w_i
[∀jk. S_k^w_j/w_k> S_j] =w_k/∑_j w_j

_i S_i ∼Unif [0,1]
K _i S_i^1/w_i
[[∀jk. S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

_i S_i ∼Unif [0,1]
K _i S_i^1/w_i
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

At this point we begin working forwards from the hypotheses,
to introduce the conditioning modality $\D_{s_k\gets S_k}$
with the aim of computing the conditional probability $\Pr(K=k\mid S_k=s_k)$.

S_k∼Unif [0,1]_s_kS_k _jk S_j ∼Unif [0,1]

K _i S_i^1/w_i
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

S_k∼Unif [0,1]_s_kS_k _jk
S_j ∼Unif [0,1] (
[∏_jk[S_k^w_j/w_k> S_j]]
=[∏_jk[s_k^w_j/w_k> S_j]])

K _i S_i^1/w_i
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

Next, we use conditional independence of $\{S_j\}_{j\ne k}$ given $S_k$, encoded in the
iterated separating conjunction underneath $\D_{s_\gets S_k}$, to interchange product and expectation:

S_k∼Unif [0,1]_s_kS_k _jk
S_j ∼Unif [0,1] (
[∏_jk[S_k^w_j/w_k> S_j]]
= ∏_jk[[s_k^w_j/w_k> S_j]]

K _i S_i^1/w_i
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

Now significant simplifications are possible, completing the first calculation
(Equations <ref>–<ref>):

S_i∼Unif [0,1]_s_kS_k _jk
S_j ∼Unif [0,1] (
[∏_jk[S_k^w_j/w_k> S_j]]
= ∏_jks_k^w_j/w_k

K _i S_i^1/w_i
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

S_k∼Unif [0,1]_s_kS_k _jk
S_j ∼Unif [0,1] (
[∏_jk[S_k^w_j/w_k> S_j]]
= exp(s_k,∑_jk w_j/w_k)

K _i S_i^1/w_i
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

S_k∼Unif [0,1]_s_kS_k
[∏_jk[S_k^w_j/w_k> S_j]]
= exp(s_k,∑_jk w_j/w_k)
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

Having completed the computation of the conditional probability $\Pr(K=k\mid S_k=s_k)$
by working forwards from the hypotheses, we eliminate the conditioning modality by applying the
law of total expectation (C-Total-Expectation):

S_k∼Unif [0,1][∏_jk[S_k^w_j/w_k> S_j]]
= [exp(S_k,∑_jk w_j/w_k)]
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

The remainder of the calculation is straightforward, following
Equations <ref>–<ref>:

S_k∼Unif [0,1][∏_jk[S_k^w_j/w_k> S_j]]
= 1/∑_jk w_j/w_k + 1
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

[∏_jk[S_k^w_j/w_k> S_j]]
= w_k/∑_j w_j
[∏_jk[S_k^w_j/w_k> S_j]] =w_k/∑_j w_j

§ EXAMPLES FROM BARTHE ET. AL.

In this section we consider three of the five examples presented in <cit.>:
one-time pad, oblivious transfer, and private information retrieval.
In each example, the goal is to
verify the perfect secrecy of a cryptographic protocol. Perfect secrecy is established
via two methods: uniformity, which aims to show that each agent's view of others' data is
uniformly distributed at exit, and input independence, which aims to show that the
encrypted output of the protocol is independent of the input.

<cit.> use PSL to establish perfect secrecy of one-time pad and
private information retrieval via both uniformity and input independence,
and perfect secrecy of oblivious transfer via uniformity.
We will show how the same can be done in Lilac.
<cit.> also observe that
the input independence proof for oblivious transfer gets stuck, mentioning that
even an informal proof sketch does not seem easy.
We will show that the
postcondition specifying input indendence for oblivious transfer is in fact unsatisfiable
by giving a countermodel.

To do this, we add some support for length-$n$ bitvectors and reasoning about uniformity.
For bitvectors,

* Let $\ber^n 1/2$ be the uniform distribution on boolean-valued $n$-tuples.

* Let $\flip^n~p$ be the $n$-ary generalization of $\flip$ that produces $n$-tuples of i.i.d. $\ber p$
random variables, with the evident semantics.

* If $X$ is a random variable valued in boolean $n$-tuples, let $\bigoplus X$
be the random variable given by the $\oplus$ of all $n$ components.

* Let $\appland^n$ and $\oplus^n$ be the lifting of boolean $\appland$ and $\oplus$ to $n$-tuples.

* We will make use of algebraic properties of the bitvector xor operator $\oplus^n$ throughout;
in particular the property that $x\oplus^n -$ is invertible.

Next, we import the requisite probability theory facts as derived rules.
For clarity of exposition, we suppress components of Lilac's semantic model
(like underlying probability spaces, the random substitution, and the deterministic substitution)
in the proofs of these rules in favor of a presentation that more closely mirrors textbook probability.
The first few facts concern uniformity of random bitvectors:

If $X$ is a random $n$-bitvector and $f:\sembr\boolty^n\to\sembr\boolty^n$ a bijection then

\[
X \sim \ber^n 1/2 \vdash f(X) \sim \ber^n1/2.
\]

We have $\Pr[f(X) = x] = \Pr[X = f^{-1}(x)] = 1/2^n$ for all $x$.

If $X$ is a random $n$-bitvector and $Y$ a random $m$-bitvector then

\[
X\sim \ber^n 1/2 ~~*~~ Y \sim \ber^m 1/2 \vdashiff (X,Y) \sim \ber^{m+n}1/2
\]

Calculation gives

\[
\Pr[(X,Y)=(x,y)]=\Pr[X=x,Y=y]\stackrel{(a)}=\Pr[X=x]\Pr[Y=y] = (1/2^m)(1/2^n) = 1/2^{m+n}\]

for all $x,y$ as desired. Equation $(a)$ follows from independence of $X$ and $Y$.

This next lemma encodes the key fact of probability theory underlying the perfect secrecy of the examples
we will consider in the next section. Intuitively, it states that any random variable which is “conditionally
uniformly distributed” (that is, uniformly distributed conditional on some other random variable) is
uniformly distributed proper.

If $X$ is a random variable taking on finitely many values[
Though we expect this restriction can be lifted, $\operatorname{cod}(X)$ finite suffices for our examples.]
and $Y$ a random $n$-bitvector then

\[
\own X \land \D_{x\gets X} (Y \sim \ber^n 1/2) \hspace{0.5em}\vdash\hspace{0.5em} \own X ~~*~~ Y \sim \ber^n1/2
\]

It suffices to show $X$ and $Y$ are independent and $Y$ uniform.
This amounts to showing the equality $\Pr[X=x,Y=y] = \Pr[X=x]/2^n$ for all $x,y$.
By assumption $Y$ is uniformly distributed conditional on $X$, so

\[ \Pr[X=x,Y=y] = \Pr[Y=y\mid X=x]\Pr[X=x] = \frac1{2^n}\Pr[X=x] \]

as desired.

To avoid verbosity, we use the abbreviation
$\displaystyle \Down_{x\gets X} P := \own X \land \D_{x\gets X} P$.

Thus the entailment given by Lemma <ref> can be written
$\displaystyle\Down_{x\gets X} (Y\sim\ber^n 1/2) \hspace{0.5em}\vdash\hspace{0.5em} \own X ~~*~~ Y \sim \ber^n1/2$.

We will also frequently make use of the following variant of :

The following entailment holds:

\[  \own X ~~*~~ P  \hspace{0.5em}\vdash\hspace{0.5em} \Down_{x\gets X} P. \]

By the following chain:

\begin{align*}
&\own X * P \\
&\vdash (\own X * P)\land (\own X * P) & \text{idempotency of }\land \\
&\vdash \own X\land (\own X * P) & \text{drop a conjunct} \\
&\vdash \own X\land \D_{x\gets X} P & \DIndep  \\
&\vdash \Down_{x\gets X} P & \text{definition of }\Down
\end{align*}

The final derived rule we will make use of encodes the probability-theoretic fact that,
when proving an assertion of the form $X\sim\mu ~~*~~ P$,
one can first establish that $X$ has distribution $\mu$,
and then separately establish independence of $X$ from other random variables.

Let $X$ be a random variable, $\mu$ a distribution, and $P$ a proposition.

\[
(X\sim \mu)\land (\own X ~~*~~ P)\vdash (X\sim \mu) ~~*~~ P
\]

Suppose $X$ is distributed as $\mu$ with respect to probability space $\mathcal P_X$,
that $P$ holds in space $\mathcal P$,
and that there exists a space $\mathcal P_X'$ independent of $\mathcal P$ for which $X$ is $\mathcal P_X'$-measurable.
Let $\mathcal Q$ be the pullback $\sigma$-algebra of $X$.
We have that $\mathcal P_X\sqsupseteq \mathcal Q\sqsubseteq\mathcal P_X'$ and that
$\mathcal P_X$ and $\mathcal P_X'$ agree on $\mathcal Q$. Thus, $\mathcal Q$ is independent of $\mathcal P$
and the composite $\mathcal Q\pdot \mathcal P$ witnesses $X\sim\mu~~*~~ P$ as desired.

§.§ Verification of one-time pad example

The one-time pad protocol is modelled by the following probabilistic program,
parameterized by a constant $m$ representing the message being encrypted:

\begin{equation}
\tag{\textsc{OneTimePad}}
\begin{aligned}
&\appllet K\appleq\flip~1/2 \applin\\
&\appllet C\appleq\applret(K\oplus m) \applin\\
&\applret C
\end{aligned}
\label{prog:onetimepad}
\end{equation}

§.§.§ Uniformity

Uniformity is specified by the triple
\triple\top{\ref{prog:onetimepad}(m)}C{C\sim\flip~1/2}

This can be established by the following annotation:

\begin{align*}
&\assert{\{\top\}} \\
&\hspace{1em}\appllet K\appleq\flip~1/2 \applin\\
&\assert{\{K\sim \ber1/2\}} \\
&\hspace{1em}\appllet C\appleq\applret(K\oplus m) \applin\\
&\assert{\{K\sim \ber1/2~~*~~C\asequal K\oplus m\}} \\
&\hspace{1em}\applret C\\
&\assert{\{C.~K\sim \ber1/2~~*~~C\asequal K\oplus m\}} & \\
&\assert{\{C.~K\sim \ber1/2~~*~~C\oplus m\asequal K\}} & \text{rearranging the equality} \\
&\assert{\{C.~(C\oplus m)\sim \ber1/2\}} & \text{substituting away }K \\
&\assert{\{C.~C\sim \ber1/2\}} & \text{Lemma~\ref{lem:unif-bij}} \\
\end{align*}

§.§.§ Input independence

Input independence is specified by the triple

\[\triple{\own M}{\ref{prog:onetimepad}(M)}C{\own M ~~*~~ C\sim\ber~1/2}.\]

This can be established by the following annotation:

\begin{align*}
&\assert{\{\own M\}} \\
&\hspace{1em}\appllet K\appleq \flip~1/2 \applin\\
&\assert{\{\own M ~~*~~ K\sim \ber1/2\}} \\
&\hspace{1em}\appllet C\appleq \applret(K\oplus M) \applin\\
&\assert{\{\own M ~~*~~ K\sim \ber1/2~~*~~C\asequal K\oplus M\}} \\
&\hspace{1em}\applret C\\
&\assert{\{C.~\own M ~~*~~ K\sim \ber1/2~~*~~C\asequal K\oplus M\}} \\
&\assert{\{C.~\own M ~~*~~ K\sim \ber1/2~~*~~C\oplus M\asequal K\}} & \text{rearranging the equality} \\
&\assert{\{C.~\own M ~~*~~ (C\oplus M)\sim \ber1/2\}} & \text{substituting away }K \\
&\assertc{C.~\Down_{m\gets M} ((C\oplus M)\sim \ber1/2)} & \text{Lemma~\ref{lem:dindep-variant}} \\
&\assertc{C.~\Down_{m\gets M} ((C\oplus m)\sim \ber1/2)} & \text{replacing }M\text{ with }m \\
&\assertc{C.~\Down_{m\gets M} (C\sim \ber1/2)} & \text{Lemma~\ref{lem:unif-bij}} \\
&\assertc{C.~\own M ~~*~~ C\sim \ber1/2} & \text{Lemma~\ref{lem:indep-unif}} \\
\end{align*}

§.§ Verification of private information retrieval example

Let $i$ be an $n$-tuple of boolean values with only a single component set to $\vtrue$.
The private information retrieval protocol is modelled by the following probabilistic program,
parameterized by $i$:

\begin{equation}
\tag{\textsc{PrivateInformationRetrieval}}
\begin{aligned}
&\appllet Q_0\appleq \flip^n~1/2 \applin\\
&\appllet Q_1\appleq Q_0 \oplus^n i \applin\\
&\appllet A_0\appleq Q_0 \appland^n d \applin\\
&\appllet A_1\appleq Q_1 \appland^n d \applin\\
&\appllet R_0\appleq \applret\left(\bigoplus A_0\right) \applin \\
&\appllet R_1\appleq \applret\left(\bigoplus R_1\right) \applin \\
&\appllet R\appleq \applret(R_0\oplus R_1) \applin \\
&\applret (Q_0, Q_1,A_0, A_1, R_0, R_1, R)
\end{aligned}
\label{prog:pir}
\end{equation}

§.§.§ Uniformity

Uniformity is specified by the triple

\[
\triple\top{\ref{prog:pir}(i)}{(Q_0, Q_1, A_0, A_1, R_0, R_1, R)}
{~ Q_0 \sim \ber^n1/2 ~~\land~~ Q_1 \sim \ber^n 1/2}.
\]

This can be established by the following annotation:

\begin{align*}
&\assert{\{\top\}} \\
&\hspace{1em}\appllet Q_0\appleq \flip^n~1/2 \applin\\
&\assert{\{Q_0 \sim \ber^n1/2\}} \\
&\hspace{1em}\appllet Q_1\appleq Q_0 \oplus^n i \applin\\
&\assert{\{Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i\}} \\
&\hspace{1em}\appllet A_0\appleq Q_0 \appland^n d \applin\\
&\assert{\{Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i ~~*~~ A_0 \asequal Q_0 \appland^n d \}} \\
&\hspace{1em}\appllet A_1\appleq Q_1 \appland^n d \applin\\
&\assert{\{Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~
A_1 \asequal Q_1 \appland^n d \}} \\
&\hspace{1em}\appllet R_0\appleq \applret\left(\bigoplus A_0\right) \applin \\
Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ A_1\asequal Q_1\appland^n d~~*~~
R_0=\bigoplus A_0
} \\
&\hspace{1em}\appllet R_1\appleq \applret\left(\bigoplus R_1\right) \applin \\
Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ A_1\asequal Q_1\appland^n d~~*~~
R_0=\bigoplus A_0 ~~*~~ R_1=\bigoplus A_1
} \\
&\hspace{1em}\appllet R\appleq \applret(R_0\oplus R_1) \applin \\
&Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ A_1\asequal Q_1\appland^n d~~*~~\\
&R_0=\bigoplus A_0 ~~*~~ R_1=\bigoplus A_1 ~~*~~ R\asequal R_0 \oplus R_1
\end{aligned}} \\
&\hspace{1em}\applret (Q_0, Q_1,A_0, A_1, R_0, R_1, R) \\
&\assertc{(Q_0, Q_1,A_0, A_1, R_0, R_1, R).\hspace{0.5em}\begin{aligned}
&Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ A_1\asequal Q_1\appland^n d~~*~~\\
&R_0=\bigoplus A_0 ~~*~~ R_1=\bigoplus A_1 ~~*~~ R\asequal R_0 \oplus R_1
\end{aligned}} \\[-0.75em]
&\hspace{13em}\assert{\vdots} \\[-0.25em]
&\assertc{(Q_0, Q_1,A_0, A_1, R_0, R_1, R).~~
Q_0 \sim \ber^n1/2 ~~\land~~ Q_1 \sim \ber^n1/2} \\
\end{align*}

The final entailment (hidden by the vertical ellipses) can be established as follows:

\begin{align*}
&Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ \\
&R_0=\bigoplus A_0 ~~*~~ R_1=\bigoplus A_1 ~~*~~ R\asequal R_0 \oplus R_1
\end{aligned}\right)\\
&\vdash Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i & \text{dropping some conjuncts}\\
&\vdash (Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i)\land
(Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i)
& \text{by }P\vdash P\land P\\
&\vdash (Q_0 \sim \ber^n1/2)\land
(Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n i)
& \text{weakening first conjunct}\\
&\vdash (Q_0 \sim \ber^n1/2) ~~\land~~ (Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \oplus^n i \asequal Q_0)
& \text{rearranging the equality}\\
&\vdash (Q_0 \sim \ber^n1/2) ~~\land~~ ((Q_1\oplus^n i) \sim \ber^n1/2)
& \text{substituting away }Q_0\\
&\vdash (Q_0 \sim \ber^n1/2) ~~\land~~ (Q_1 \sim \ber^n1/2)
& \text{Lemma~\ref{lem:unif-bij}}
\end{align*}

§.§.§ Input independence

Let $I$ be a random $n$-bitvector.[
Following <cit.>,  we don't even need require that $I$
always have only a single component set to $\vtrue$
to establish input independence.]
Input independence is specified by the triple

\[
\triple{\own I}{\ref{prog:pir}(I)}C{(\own I * \own Q_0) \land (\own I * \own Q_1)}.
\]

This can be established by the following annotation:

\begin{align*}
&\assert{\{\own I\}} \\
&\hspace{1em}\appllet Q_0\appleq \flip^n~1/2 \applin\\
&\assert{\{\own I ~~*~~ Q_0 \sim \ber^n1/2\}} \\
&\hspace{1em}\appllet Q_1\appleq Q_0 \oplus^n I \applin\\
&\assert{\{\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I\}} \\
&\hspace{1em}\appllet A_0\appleq Q_0 \appland^n d \applin\\
&\assert{\{\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I ~~*~~ A_0 \asequal Q_0 \appland^n d \}} \\
&\hspace{1em}\appllet A_1\appleq Q_1 \appland^n d \applin\\
&\assert{\{\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~
A_1 \asequal Q_1 \appland^n d \}} \\
&\hspace{1em}\appllet R_0\appleq \applret\left(\bigoplus A_0\right) \applin \\
\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ A_1\asequal Q_1\appland^n d ~~*~~
R_0=\bigoplus A_0
} \\
&\hspace{1em}\appllet R_1\appleq \applret\left(\bigoplus R_1\right) \applin \\
&\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ A_1\asequal Q_1\appland^n d ~~*\\
&R_0=\bigoplus A_0 ~~*~~ R_1=\bigoplus A_1 ~~*~~ R\asequal R_0 \oplus R_1
\end{aligned}} \\
&\hspace{1em}\appllet R\appleq \applret(R_0\oplus R_1) \applin \\
&\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I ~~*~~ A_0 \asequal Q_0 \appland^n d ~~*~~ A_1\asequal Q_1\appland^n d ~~*\\
&R_0=\bigoplus A_0 ~~*~~ R_1=\bigoplus A_1 ~~*~~ R\asequal R_0 \oplus R_1
\end{aligned}} \\
&\hspace{1em}\applret (Q_0, Q_1,A_0, A_1, R_0, R_1, R) \\
&\assertc{(Q_0, Q_1,A_0, A_1, R_0, R_1, R).\hspace{0.5em}\begin{aligned}
&\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I ~~*~~ A_0 \asequal Q_0 \appland^n d ~~* \\
&A_1\asequal Q_1\appland^n d ~~*~~ R_0=\bigoplus A_0 ~~*~~ R_1=\bigoplus A_1 ~~*~~ R\asequal R_0 \oplus R_1
\end{aligned}} \\
&\assertc{(Q_0, Q_1,A_0, A_1, R_0, R_1, R).~~
\own I ~~*~~ Q_0 \sim \ber^n1/2 ~~*~~ Q_1 \asequal Q_0 \oplus^n I
} \\[-0.5em]
&\assertc{(Q_0, Q_1,A_0, A_1, R_0, R_1, R).~~
(\own I * \own Q_0) \land
(\own I * \own Q_1)
\end{align*}

The final entailment (hidden by the vertical ellipses) can be established as follows.
The left conjunct of the postcondition follows from $Q_0\sim \ber^n 1/2\vdash \own Q_0$ and dropping the equality
$Q_1\asequal Q_0\oplus^n I$.
The right conjunct is established by the following chain of entailments:

\begin{align*}
& \own I ~~*~~ Q_0 \sim \ber^n1/2~~*~~ Q_1\asequal Q_0\oplus^n I \\
& \vdash\Down_{i\gets I} (Q_0 \sim \ber^n1/2~~*~~ Q_1\asequal Q_0\oplus^n I) & \text{Lemma~\ref{lem:dindep-variant}} \\
& \vdash\Down_{i\gets I} (Q_0 \sim \ber^n1/2~~*~~ Q_1\asequal Q_0\oplus^n i) & \text{substituting }i\text{ for }I \\
& \vdash\Down_{i\gets I} (Q_0 \sim \ber^n1/2~~*~~ (Q_1\oplus^n i)\asequal Q_0) & \text{rearranging the equality} \\
& \vdash\Down_{i\gets I} ((Q_1\oplus^n i) \sim \ber^n1/2) & \text{substituting away }Q_0 \\
& \vdash\Down_{i\gets I} (Q_1 \sim \ber^n1/2) & \text{Lemma~\ref{lem:unif-bij}} \\
& \vdash\own I ~~*~~ Q_1 \sim \ber^n1/2 & \text{Lemma~\ref{lem:indep-unif}} \\
& \vdash\own I ~~*~~ \own Q_1 & \text{by }X\sim\mu\vdash\own X
\end{align*}

§.§ Verification of oblivious transfer example

The oblivious transfer protocol is modelled by the following probabilistic program:

\begin{equation}
\tag{\textsc{ObliviousTransfer}}
\begin{aligned}
&\appllet R_0\appleq \flip^n~1/2 \applin\\
&\appllet R_1\appleq \flip^n~1/2 \applin\\
&\appllet D\appleq \flip~1/2 \applin\\
&\appllet (R_D, R_{\neg D})\appleq \applite{D}{\applret(R_1,R_0)}{\applret(R_0,R_1)} \applin\\
&\appllet E\appleq \applret(c\oplus D) \applin\\
&\appllet (F_0,F_1)\appleq \applite{E}{\applret(m_0\oplus R_1,m_1\oplus R_0)}{\applret(m_0\oplus R_0,m_1\oplus R_1)} \applin\\
&\appllet (m_c,F_{\neg c}) \appleq  \applite{c}{\applret (F_1\oplus R_D,m_0\oplus R_{\neg D})}{\applret(F_0\oplus R_D,m_1\oplus R_{\neg D})} \applin\\
&\applret (R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, m_c, F_{\neg c})
\end{aligned}
\label{prog:ot}
\end{equation}

This program is parameterized by the two messages $m_0$ and $m_1$ on offer and the bit $c$ encoding
the receiver's choice.

§.§.§ Uniformity

Uniformity is specified by the triple

\[
\lrtriple\top{\ref{prog:ot}(c,m_0,m_1)}{
\left(\begin{aligned}
&R_0, R_1, D, R_D, R_{\neg D}, \\
&E, F_0, F_1, m_c, F_{\neg c}
\end{aligned}\right)}
{~ \begin{aligned}
&((R_0,R_1)\sim \ber^{2n}1/2 ~~*~~ E\sim\ber1/2) ~~\land\\
&(D\sim\ber1/2 ~~*~~ (R_D,F_{\neg c})\sim \ber^{2n}1/2)
\end{aligned}}.
\]

The next page gives an annotated program that establishes this specification.

\begin{align*}
&\assertc{\top} \\
&\hspace{1em}\appllet R_0\appleq \flip^n~1/2 \applin\\
&\assertc{R_0 \sim \ber^n 1/2} \\
&\hspace{1em}\appllet R_1\appleq \flip^n~1/2 \applin\\
&\assertc{R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2} \\
&\hspace{1em}\appllet D\appleq \flip~1/2 \applin\\
&\assertc{R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2} \\
&\hspace{1em}\appllet (R_D, R_{\neg D})\appleq \applite{D}{\applret(R_1,R_0)}{\applret(R_0,R_1)} \applin\\
&R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal (\ite D{R_0}{R_1})
\end{aligned}} \\
&\hspace{1em}\appllet E\appleq \applret(c\oplus D) \applin\\
&R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal (\ite D{R_0}{R_1}) ~~*~~ E\asequal c\oplus D \\
\end{aligned}} \\
&\hspace{1em}\appllet (F_0,F_1)\appleq \applite{E}{\applret(m_0\oplus R_1,m_1\oplus R_0)}{\applret(m_0\oplus R_0,m_1\oplus R_1)} \applin\\
&R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal (\ite D{R_0}{R_1}) ~~*~~ E\asequal c\oplus D ~~*~~ \\
&F_0 \asequal (\ite E{m_0\oplus R_1}{m_1\oplus R_0}) ~~*~~ F_1\asequal (\ite D{m_0\oplus R_0}{m_1\oplus R_1}) \\
\end{aligned}} \\
&\hspace{1em}\appllet (m_c,F_{\neg c}) \appleq  \applite{c}{\applret (F_1\oplus R_D,m_0\oplus R_{\neg D})}{\applret(F_0\oplus R_D,m_1\oplus R_{\neg D})} \applin\\
&R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal (\ite D{R_0}{R_1}) ~~*~~ E\asequal c\oplus D ~~*~~ \\
&F_0 \asequal (\ite E{m_0\oplus R_1}{m_1\oplus R_0}) ~~*~~ F_1\asequal (\ite D{m_0\oplus R_0}{m_1\oplus R_1}) ~~*~~ \\
&m_c \asequal (\ite c{F_1\oplus R_D}{F_0\oplus R_D}) ~~*~~ F_{\neg c}\asequal (\ite c{m_0\oplus R_{\neg D}}{m_1\oplus R_{\neg D}}) \\
\end{aligned}}}_P} \\
&\hspace{1em}\applret (R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, m_c, F_{\neg c})\\
&\assertc{(R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, m_c, F_{\neg c}).~P} \\[1em]
&\assert{{\bigg\{}(R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, m_c, F_{\neg c}).~
\begin{aligned}
&\overbrace{((R_0,R_1)\sim \ber^{2n}1/2 ~~*~~ E\sim\ber1/2)}^Q ~~\land\\
&\underbrace{(D\sim\ber1/2 ~~*~~ (R_D,F_{\neg c})\sim \ber^{2n}1/2)}_R
\end{aligned} {\bigg\}}} \\
\end{align*}

The final entailment (hidden by the vertical ellipses), abbreviated $P\vdash Q\land R$,
can be established as follows.
First, to show $P\vdash Q$,

\begin{align*}
&P \\
&\vdash R_0 \sim \ber^n1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim \ber1/2 ~~*~~ E\asequal c\oplus D
& \text{dropping conjuncts} \\
&\vdash R_0 \sim \ber^n1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim \ber1/2 ~~*~~ E\oplus c\asequal D
& \text{rearranging the equality} \\
&\vdash R_0 \sim \ber^n1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ (E\oplus c)\sim \ber1/2
& \text{substituting away }D \\
&\vdash R_0 \sim \ber^n1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ E\sim \ber1/2
& \text{Lemma~\ref{lem:unif-bij}} \\
&\vdash (R_0,R_1) \sim \ber^{2n}1/2 ~~*~~ E\sim \ber1/2
& \text{Lemma~\ref{lem:unif-fuse}} \\
&= Q
\end{align*}

Second, $P\vdash R$ can be established by the following chain:

\begin{align*}
&P \\
&\vdash {\left({\begin{aligned}
&R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal (\ite D{R_0}{R_1})~~*~~\\
&F_{\neg c}\asequal (\ite c{m_0\oplus R_{\neg D}}{m_1\oplus R_{\neg D}})
\end{aligned}}\right)} & \text{dropping some conjuncts} \\
&\vdash \dots \\
&\vdash {\left({\begin{aligned}
&R_D \sim \ber^n 1/2 ~~*~~ R_{\neg D}\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&F_{\neg c}\asequal (\ite c{m_0\oplus R_{\neg D}}{m_1\oplus R_{\neg D}}) \\
\end{aligned}}\right)}  \\
&\vdash {\left({\begin{aligned}
&R_D \sim \ber^n 1/2 ~~*~~ R_{\neg D}\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&F_{\neg c}\asequal (\ite c{m_0}{m_1})\oplus R_{\neg D} \\
\end{aligned}}\right)}
& \text{commuting conversion}\\
&\vdash {\left({\begin{aligned}
&R_D \sim \ber^n 1/2 ~~*~~ R_{\neg D}\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2~~*~~ \\
&(\ite c{m_0}{m_1})\oplus F_{\neg c}\asequal R_{\neg D} \\
\end{aligned}}\right)}
& \text{property of }\oplus\\
&\vdash {\left({\begin{aligned}
&R_D \sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&((\ite c{m_0}{m_1})\oplus F_{\neg c})\sim \ber^n 1/2
\end{aligned}}\right)}
& \text{substitute away }R_{\neg D}\\
&\vdash {
R_D \sim \ber^n 1/2 ~~*~~ D\sim\ber1/2  ~~*~~
F_{\neg c}\sim \ber^n 1/2
& \text{Lemma~\ref{lem:unif-bij}} \\
&\vdash D\sim\ber1/2 ~~*~~ (R_D,F_{\neg c})\sim \ber^{2n}1/2 & \text{Lemma~\ref{lem:unif-fuse}}\\
&= R
\end{align*}

The entailment hidden by ellipses
establishes the mutual independence of $D$, $R_D$, and $R_{\neg D}$,
the key property that perfect secrecy hinges on. The proof goes by case analysis on $D$,
and is shown on the next page.

\begin{align*}
&R_0 \sim \ber^n 1/2 ~~*~~ R_1\sim \ber^n 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal (\ite D{R_0}{R_1})
\end{aligned}}\right)} \\
&\vdash \underbrace{\left({\begin{aligned}
&(R_0, R_1) \sim \ber^{2n} 1/2 ~~*~~ D\sim\ber1/2 ~~*~~ \\
&R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal (\ite D{R_0}{R_1})
\end{aligned}}\right)}_{S[D\sim\ber 1/2]} & \text{Lemma~\ref{lem:unif-fuse}} \\
&\vdash S[D\sim\ber1/2] \land S[D\sim\ber 1/2] & \text{property of }\land \\
&\vdash S[D\sim\ber 1/2] \land (D\sim\ber 1/2) & \text{drop conjuncts}\\
&\vdash S[\own D] \land (D\sim\ber 1/2) & X\sim\mu\vdash \own X\\
{\Down_{d\gets D} \left(
(R_0, R_1) \sim \ber^{2n} 1/2 ~~*~~
R_D \asequal (\ite D{R_1}{R_0}) ~~*~~ \dots
\right)}
\land (D\sim\ber 1/2) & \text{Lemma~\ref{lem:dindep-variant}} \\
{\Down_{d\gets D} \underbrace{\left({\begin{aligned}
&(R_0,R_1) \sim \ber^{2n}1/2 ~~*~~\\
&R_D \asequal (\ite d{R_1}{R_0}) ~~*~~ R_{\neg D}\asequal \dots
\end{aligned}}\right)}_{Q(d)}}
\land (D\sim\ber 1/2) & \text{replace }D\textrm{ with }d \\
\Down_{d\gets D} \left(Q(\vtrue) \land Q(\vfalse)\right)
\land (D\sim\ber 1/2) & \text{cases on }d \\
\Down_{d\gets D} \bigg(\begin{aligned}
(R_0,R_1) \sim \ber^{2n} ~~*~~
R_D \asequal R_1 ~~*~~ R_{\neg D}\asequal R_0\right)
}^{Q(\vtrue)} \land \\
(R_0,R_1) \sim \ber^{2n} 1/2 ~~*~~
R_D \asequal R_0 ~~*~~ R_{\neg D}\asequal R_1\right)
\end{aligned}\bigg)
\land(D\sim\ber 1/2) & \text{unfold }Q \\
\Down_{d\gets D}\bigg(
((R_{\neg D},R_D) \sim \ber^{2n} 1/2) \land
((R_D,R_{\neg D}) \sim \ber^{2n} 1/2)\bigg)
\land (D\sim\ber 1/2) & \text{substitute} \\
\Down_{d\gets D}\bigg(\begin{aligned}
&(R_{\neg D}\sim\ber^n1/2 ~~*~~ R_D\sim\ber^n 1/2) \land  \\
&(R_D \sim \ber^{n} 1/2 ~~*~~ R_{\neg D}\sim\ber^n 1/2)\end{aligned}\bigg)
\land (D\sim\ber 1/2) & \text{Lemma~\ref{lem:unif-fuse}} \\
\Down_{d\gets D} (R_{\neg D} \sim \ber^n 1/2 ~~*~~ R_D\sim \ber^n 1/2)
\land (D\sim\ber 1/2) & \text{by }P\land P\vdash P \\
\Down_{d\gets D} ((R_D,R_{\neg D}) \sim \ber^{2n} 1/2)
\land (D\sim\ber 1/2) & \text{Lemma~\ref{lem:unif-fuse}} \\
(\own D ~~*~~ R_{\neg D} \sim \ber^n 1/2 ~~*~~ R_D\sim \ber^n 1/2)
\land (D\sim\ber 1/2) & \text{Lemma~\ref{lem:indep-unif}} \\
D\sim\ber1/2 ~~*~~ R_{\neg D} \sim \ber^n 1/2 ~~*~~ R_D\sim \ber^n 1/2
& \text{Lemma~\ref{lem:separate-own-dist}}
\end{align*}

§.§.§ Input independence

Following <cit.>, the following Hoare triple specifies input
independence for <ref>:

\begin{align*}
&\assertc{\own (C, M_0, M_1)} \\
&\hspace{1em}{\ref{prog:ot}(M_0,M_1,C)} \\
&\assertc{(R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, M_C, M_{1-C}, F_{\neg C}).~
\begin{aligned}
&(\own C ~~*~~ \own (R_0, R_1, E)) ~~\land \\
&(\own M_{1-C} ~~*~~ \own (D, R_D, F_0, F_1)) \\
\end{aligned}}
\end{align*}

In the postcondition, $M_{1-C}$ denotes the random variable $(\ite{C}{M_0}{M_1})$.

<cit.> observe that the proof gets stuck, mentioning
that even an informal proof sketch does not seem easy.
We show that this triple is in fact
impossible to establish by giving an explicit counterexample. This takes the form of
three random variables $C$, $M_0$, and $M_1$ such that
the postcondition fails.
In particular, we choose $C = 0$ and $M_0 = M_1 = M$ for some uniformly-distributed $M$.
Now the triple reads

\begin{align*}
&\assertc{\own (C, M, M)} \\
&\hspace{1em}{\ref{prog:ot}(M, M, C)} \\
&\assertc{(R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, M_C, M_{1-C}, F_{\neg C}).~
\begin{aligned}
&(\own C ~~*~~ \own (R_0, R_1, E)) ~~\land \\
&(\own M ~~*~~ \own (D, R_D, F_0, F_1)) \\
\end{aligned}}
\end{align*}

Suppose this triple holds.
Then so does the following triple, where we have dropped the first conjunct of the postcondition:

\begin{align*}
&\assertc{\own (C, M, M)} \\
&\hspace{1em}{\ref{prog:ot}(M, M, C)} \\
&\assertc{(R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, M_C, M_{1-C}, F_{\neg C}).~
(\own M ~~*~~ \own (D, R_D, F_0, F_1))} \\
\end{align*}

Lilac's semantic model validates the following derived rule:

Let $X$ be a random variable and $f : \mathrm{cod}(X)\to B$ measurable.
Then $\own X\vdash \own (f\circ X)$.

The composition of measurable maps remains measurable.

Thus we have that $\own (D,R_D, F_0,F_1) \vdash \own (R_D\oplus F_0)$,
so the following triple holds:

\begin{align*}
&\assertc{\own (C, M, M)} \\
&\hspace{1em}{\ref{prog:ot}(M, M, C)} \\
&\assertc{(R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, M_C, M_{1-C}, F_{\neg C}).~
(\own M ~~*~~ \own (R_D\oplus F_0))} \\
\end{align*}

At this point we transition from working in Lilac to reading off
the meanings of Lilac propositions in our semantic model.
We know that, by forward symbolic execution as in the previous section,
the OT protocol sets

\begin{align*}
F_0 &\asequal (\ite E{M_0\oplus R_1}{M_1\oplus R_0}) \\
E &\asequal C\oplus D \\
R_D &\asequal (\ite D{R_1}{R_0})
\end{align*}

We have set $M_0 = M_1 = M$ and $C = 0$ for the sake of contradiction, so these equations become

\begin{align*}
F_0 &\asequal M \oplus (\ite E{R_1}{R_0}) \\
E &\asequal D \\
R_D &\asequal (\ite D{R_1}{R_0})
\end{align*}

Further substitution gives

\[ F_0 \asequal M\oplus (\ite D{R_1}{R_0})\asequal M\oplus  R_D. \]

Reading the final Hoare triple obtained above in terms of the model, we have that
$\sembr{\ref{prog:ot}}$ is a Markov kernel
whose pushforward along the distribution on $(C,M,M)$
gives a distribution on
\[(R_0, R_1, D, R_D, R_{\neg D}, E, F_0, F_1, M_C, M_{1-C}, F_{\neg C})\]

in which $M$ is independent of $(R_D\oplus F_0)$.
But we also have

\[ R_D \oplus F_0 = R_D\oplus (M\oplus R_D) = M \]

by the above deduction, so this Hoare triple asserts
the self-independence of $M$.
This is a contradiction: we have chosen $M$ to be a uniformly-distributed $n$-tuple
of boolean values, which cannot be self-independent.

Intuitively, the special case $C=0$ and $M_0=M_1=M$ that we have chosen
is the situation where both messages offered by the sender are exactly the same
and the receiver always opts to receive message $0$. The failure of input
independence corresponds to the fact that the receiver manages to learn what
message $1$ is. But it only learns message $1$ because in this particular situation
the two messages happen to be the same! Thus this counterexample appears
to be more an issue with this particular specification of perfect secrecy via
input independence than a vulnerability in the OT protocol.


# Symmetries and conservation laws for the generalized $n$-dimensional Ermakov
system

Andronikos Paliathanasis
Institute of Systems Science, Durban University of Technology
PO Box 1334, Durban 4000, Republic of South Africa
Instituto de Ciencias Físicas y Matemáticas,
Universidad Austral de Chile, Valdivia, Chile Email:
<EMAIL_ADDRESS>Author Genly Leon
Departamento de Matemáticas, Universidad Católica del Norte, Avda.
Angamos 0610, Casilla 1280 Antofagasta, Chile
Institute of Systems Science, Durban University of Technology
PO Box 1334, Durban 4000, Republic of South Africa P.G.L. Leach
Institute of Systems Science, Durban University of Technology
PO Box 1334, Durban 4000, Republic of South Africa

###### Abstract

We revise recent results on the classification of the generalized three-
dimensional Hamiltonian Ermakov system. We show that a statement published
recently is incorrect, while the solution for the classification problem was
incomplete. We present the correct classification for the three-dimensional
system by using results which related the background space with the dynamics.
Finally, we extend our results for the generalized $n$-dimensional Hamiltonian
Ermakov system.

Keywords: Lie symmetries; Noether symmetries; Ermakov system; Integrability

##  1 Introduction

At the end of the 19th century, Ermakov [1] solved the problem for the
derivation of first integral for the time-dependent linear equation

$\ddot{x}+\omega^{2}(t)x=0,$ (1)

where an overdot means total derivative with respect to the time-variable,
$t$, that is, $\dot{x}=\frac{dx}{dt}$.

By introducing the new variable $\rho\left(t\right)$ which satisfies the
second-order differential equation

$\ddot{\rho}+\omega^{2}(t)\rho=\rho^{-3}$ (2)

the time-dependent term in (1) can be eliminated and the following function
$J\left(\rho,\dot{\rho},x,\dot{x}\right)$ can be constructed

$J\left(\rho,\dot{\rho},x,\dot{x}\right)=\frac{1}{2}\left[(\rho\dot{x}-\dot{\rho}x)^{2}+(x/\rho)^{2}\right],$
(3)

which is a conservation law, i.e. $\dot{J}=0$. The second-order ordinary
differential equation (2) was solved by Pinney in [2]. The analytic solution
is

$\rho^{2}\left(t\right)=c_{1}\left(\rho_{1}\left(t\right)\right)^{2}+c_{2}\left(\rho_{2}\left(t\right)\right)^{2}+2c_{3}\rho_{1}\left(t\right)\rho_{2}\left(t\right),$
(4)

where $\rho_{1}\left(t\right)$ and $\rho_{2}\left(t\right)$ are solutions of
equation (1) and $c_{1}$, $c_{2}$ and $c_{3}$ are constants, of which only two
are independent. Hence, equation (2) is known as the Ermakov-Pinney equation.
Furthermore, in [3], Lewis investigated the integral properties for the time-
dependent harmonic oscillator, of equation (1) in classical and quantum
systems. Lewis rediscovered the the Ermakov invariant (3) and function
$J\left(\rho,\dot{\rho},x,\dot{x}\right)$ nowadays is called Ermakov-Lewis
invariant. The oscillator appears in many physical problems and other areas of
Applied Mathematics. Consequently, the Ermakov-Lewis invariant and the
Ermakov-Pinney equation have appeared in many studies, from quantum mechanics
[3, 4, 5], to gravitational theory [6, 7] and others [8, 9, 10, 11]. Recently,
in [12] the physical interpretation of the Ermakov-Lewis invariant was
discussed.

The application of the Lie theory on the Ermakov-Pinney equation provides that
equation (2) admits three Lie point symmetries which form the $SL(2,R)$
algebra [13]. The representation of the Lie algebra depends upon the term
$\omega^{2}\left(t\right).$ Thus, there exists a point transformation in which
the term $\omega^{2}\left(t\right)$ can be eliminated and equation (2) to be
reduced in the simple form

$\ddot{\rho}=\rho^{-3}.$ (5)

There are many extensions and generalization of the Ermakov-Pinney equation in
the literature. The two-dimensional system,

$\displaystyle\ddot{x}+\omega^{2}\left(t\right)x$ $\displaystyle=$
$\displaystyle\frac{f\left(\frac{y}{x}\right)}{x^{3}}$ (6)
$\displaystyle\ddot{y}+\omega^{2}\left(t\right)y$ $\displaystyle=$
$\displaystyle\frac{g\left(\frac{y}{x}\right)}{y^{3}},$ (7)

is known as an Ermakov system [14]. System (6), (7) admits the conservation
law [15]

$I\left(x,\dot{x},y,\dot{x}\right)=\frac{1}{2}\left(x\dot{y}-\dot{x}y\right)^{2}+\int^{y/x}\left(uf\left(u\right)-u^{-3}g\left(u\right)\right)du$
(8)

which is a generalization of the Ermakov-Lewis invariant. We remark that there
exist a point transformation such that the system (6), (7) can be written in
an equivalent form without the $\omega^{2}\left(t\right)$ term. Moreover, the
two-dimensional Ermakov system admits three point symmetries which form the
the $SL\left(2,R\right)$ algebra. In the special case for which
$f\left(\frac{y}{x}\right)=V\left(x,y\right)_{,x}$ and
$g\left(\frac{y}{x}\right)=V\left(x,y\right)_{y}$, the dynamical system
follows from a variational principle and the Lie symmetries are also Noether
symmetries.

By using the latter property for the Ermakov system, that is, the admitted Lie
symmetries for a given dynamical system to form the $SL\left(2,R\right)$
algebra, there have been various generalizations of the Ermakov system in
higher-dimensions [13], in curved geometries [16] or many others see for
instance [18, 19, 20, 21] and references therein. The three-dimensional
Ermakov system introduced in [13], for which it was found that in the case
that the Ermakov system is Hamiltonian the Ermakov-Lewis invariant is a
function of the variational conservation laws which are determined by the
applications of Noether’s second theorem for the elements of the
$SL\left(2,R\right)$ algebra, see also the discussion in [17]. However, such a
property was found also in the case of curved geometries. Moreover, for the
Hamiltonian Ermakov system, the Ermakov-Lewis invariant can be constructed by
Noether’s second theorem for contact symmetries. Indeed, there was found to be
an exact relation for the existence of the Killing tensor which provides the
Ermakov-Lewis invariant and of the main generator vector for the background
space of the $SL\left(2,R\right)$ Lie algebra [16]. The $SL\left(2,R\right)$
Lie algebra plays an important role in the study of the integrability of
various Hamiltonian systems, we refer the reader in some recent studies [22,
23, 24, 25, 26, 27, 28]

A complete classification of variational symmetries for the Hamiltonian three-
dimensional Ermakov [13] system performed in [29]. The authors determined the
functional form for the unknown potential functions for the generalized
Ermakov system to admit additional variational symmetries which produce
conservation laws except from the elements of the $SL\left(2,R\right)$
algebra. The authors determined eight different potential functions of which
they claim that four of these functions are new in the literature and new
exact solutions were determined. However, this claim is false. As we shall see
with a simple construction method the potential functions the authors
determined in [29] are well known in the literature. Nevertheless, inspired by
the problem which the authors of [29] study, we extend our analysis and we
find a general result for the generalized Hamiltonian Ermakov system in
$n-$dimensional Euclidian geometry. The plan of the paper is as follow.

In Section 2 we present basic properties and definitions of the symmetry
analysis. In Section 3 we discuss the two-dimensional Ermakov system and the
Lewis invariant. The analysis of the three-dimensional generalized Ermakov
system is presented in Section 4. Finally, in Section 5 we draw our
conclusions.

##  2 Preliminaries

In this Section we present the basic properties and definitions for the theory
of symmetries of differential equations. We assume a system of second-order
ordinary differential equations of the form

$\ddot{x}^{i}=\Omega^{i}\left(t,x^{j},\dot{x}^{j}\right)~{},$ (9)

in which $x^{i}$ are the dependent variables and $t$ is the independent
variable. Furthermore, consider the one-parameter point transformation
$\Phi\left(t,x;\varepsilon\right)$ with infinitesimal generator
$\xi\left(t,x^{j}\right)\partial_{t}+\eta^{i}\left(t,x^{j}\right)\partial_{i}$
defined in the augmented space $\\{t,x^{i}\\}$. Thus, we say that the vector
field $X$ is a Lie point symmetry for the system (9) if the set of
differential equations remains invariant under the action of the one-parameter
point transformation $\Phi\left(t,x;\varepsilon\right)$, equivalently when the
following condition is true [30]

$X^{\left[2\right]}\left(\ddot{x}^{i}-\Omega^{i}\left(t,x^{j},\dot{x}^{j}\right)\right)=0~{},$
(10)

where $X^{\left[2\right]}$ is the second prolongation of $X$ defined by the
formula
$X^{\left[2\right]}=X+\left(\dot{\eta}^{i}-\dot{x}^{i}\dot{\xi}\right)\partial_{\dot{x}^{i}}+\left(\ddot{\eta}^{i}-\dot{x}^{i}\ddot{\xi}-2\ddot{x}^{i}\dot{\xi}\right)\partial_{\ddot{x}^{i}}$.
An equivalent way to express the symmetry condition (10) is [30]

$\left[X^{\left[1\right]},A\right]=\lambda\left(x^{k}\right)A~{},$ (11)

in which now $X^{\left[1\right]}$ is the first prolongation of $X$ and $A$ is
the Hamiltonian vector field
$A=\partial_{t}+\dot{x}\partial_{x}+\Omega^{i}\left(t,x^{j},\dot{x}^{j}\right)\partial_{\dot{x}^{i}}.$

If the system of differential equations results from a variational principle,
that is, there exists a Lagrangian function
$L=L\left(t,x^{j},\dot{x}^{j}\right),$ then the infinitesimal generator $X$
for the one-parameter point transformation is characterized as variational
symmetry or as Noether symmetry for the given Lagrangian function, if there
exists a function $G$ such that the condition of Noether’s first theorem is
satisfied [31]

$X^{\left[1\right]}L+L\frac{d\xi}{dt}=\frac{dG}{dt}$ (12)

Function $G$ is boundary term introduced to allow for the infinitesimal
changes in the value of the Action Integral produced by the infinitesimal
change in the boundary of the domain caused by the infinitesimal
transformation of the variables in the Action Integral.

The importancy of the determination of Noether symmetries for a given system
is that there exist a unique relation between Noether symmetries and
conservation laws. Indeed, if $X$ is a Noether symmetry vector with
corresponding boundary term $G$, then according to Noether’s second theorem
the following function

$I\left(t,x^{j},\dot{x}^{j}\right)=\xi\left(\dot{x}^{i}\frac{\partial
L}{\partial\dot{x}^{i}}-L\right)-\frac{\partial
L}{\partial\dot{x}^{i}}\eta^{i}+G$ (13)

is a conservation law for the dynamical system, that is
$\dot{I}\left(t,x^{j},\dot{x}^{j}\right)=0$. For a recent review on Noether’s
theorems we refer the reader to [32].

##  3 The Ermakov system

In the following we consider the Ermakov system and without loss of generality
we can omit the linear term with the time-dependent component
$\omega^{2}\left(t\right)$.

As we mentioned before the Ermakov-Pinney equation (5) admits three Lie point
symmetries, the vector fields

$X^{1}=\partial_{t}~{},~{}X^{2}=2t\partial_{t}+\rho\partial_{\rho}\text{~{}},~{}X^{3}=t^{2}\partial_{t}+t\rho\partial_{\rho}~{}.$
(14)

Equation (5) admits the Lagrangian function

$L\left(\rho,\dot{\rho}\right)=\frac{1}{2}\left(\dot{\rho}^{2}-\rho^{-2}\right).$
(15)

Thus, by replacing the vector fields $\left\\{X^{1},X^{2},X^{3}\right\\}$ in
Noether’s condition we find that the three vector fields are Noether
symmetries with corresponding boundary terms $G\left(X^{1}\right)=G_{0}$,
$G\left(X^{2}\right)=0$ and $G\left(X^{3}\right)=\frac{1}{2}\rho^{2}$
respectively.

Hence, from expression (13) we define the conservation laws

$\displaystyle I_{1}\left(X^{1}\right)$ $\displaystyle=$
$\displaystyle\frac{1}{2}\left(\dot{\rho}^{2}+\rho^{-2}\right)\equiv\mathcal{H},$
(16) $\displaystyle I_{2}\left(X^{2}\right)$ $\displaystyle=$ $\displaystyle
2t\mathcal{H}-\rho\dot{\rho}~{},~{}$ (17) $\displaystyle
I_{3}\left(X^{3}\right)$ $\displaystyle=$ $\displaystyle
t^{2}\mathcal{H}-t\rho\dot{\rho}+\frac{1}{2}\rho^{2}~{},$ (18)

where $\mathcal{H}$ is the Hamiltonian function.

Consider now the two-dimensional Hamiltonian Ermakov system

$\ddot{x}=\frac{\left(V\left(\frac{y}{x}\right)\right)_{x}}{x^{3}},~{}\ddot{y}=\frac{\left(V\left(\frac{y}{x}\right)\right)_{y}}{y^{3}},$
(19)

or in polar coordinates
$\left(x,y\right)=\left(r\cos\theta,r\sin\theta\right)$,

$\displaystyle\ddot{\rho}-\rho\dot{\theta}^{2}$ $\displaystyle=$
$\displaystyle\frac{V\left(\theta\right)}{\rho^{3}}~{},$ (20)
$\displaystyle\ddot{\theta}+2\rho\dot{\theta}$ $\displaystyle=$
$\displaystyle\frac{V\left(\theta\right)_{,\theta}}{2\rho^{4}}.$ (21)

with Lagrangian function

$L\left(\rho,\dot{\rho},\theta,\dot{\theta}\right)=\frac{1}{2}\left(\dot{\rho}^{2}+\rho^{2}\dot{\theta}^{2}-\frac{V\left(\theta\right)}{\rho^{2}}\right).$
(22)

For arbitrary potential function $V\left(\theta\right)$ the dynamical system
(20), (21) admits as Lie point symmetries the vector fields
$\left\\{X^{1},X^{2},X^{3}\right\\}$ which are also Noether symmetries for the
Lagrangian function (22). The corresponding conservation laws are the
$I_{1}\left(X^{1}\right)$, $I_{2}\left(X^{2}\right)$ and
$I_{3}\left(X^{3}\right)$ where now

$\mathcal{H}=\frac{1}{2}\left(\dot{\rho}^{2}+\rho^{2}\dot{\theta}^{2}+\frac{V\left(\theta\right)}{\rho^{2}}\right).$
(23)

By using these three functions we can define the following expression [13]

$J\left(\rho,\dot{\rho}\right)=4I_{3}\left(X^{1}\right)\mathcal{H}-\left(I_{2}\left(X^{2}\right)\right)^{2}$
(24)

which is nothing else than the Ermakov-Lewis invariant, that is

$J\left(\rho,\dot{\rho}\right)=\frac{1}{2}\left(\dot{\rho}^{2}+\rho^{-2}\right).$
(25)

However, for specific forms of $V\left(\theta\right)$ additional Noether
symmetries can exist. Indeed when $V\left(\theta\right)=V_{0}$, equation (21)
reads $\left(\mathcal{L}\right)^{\cdot}=0$, where
$\mathcal{L}=\rho^{2}\dot{\theta}$ is the angular momentum. The additional
Noether symmetry in this case is the vector field $X^{4}=\partial_{\phi}$. The
functional forms of $V\left(\theta\right)$ for which additional variational
symmetries exist are presented in [33]. We omit the presentation of the
symmetry vector and we present the potential functions.

The potentials are $V_{A}\left(\theta\right)=V_{0}$,
$V_{B}\left(\theta\right)=V_{0}\left(\cos\theta\right)^{-2}$,
$V_{C}\left(\theta\right)=V_{0}\left(\sin\theta\right)^{-2}$,
$V_{D}\left(\theta\right)=V_{1}\left(\cos\theta\right)^{-2}+V_{2}\left(\sin\theta\right)^{-2}$
and
$V_{E}\left(\theta\right)=V_{0}\left(V_{1}\sin\theta-\cos\theta\right)^{-2}$.
We remark that potentials $V_{B}\left(\theta\right)$ and
$V_{C}\left(\theta\right)$ are the same potential function, because
$\sin\theta=\cos\left(\theta-\frac{\pi}{2}\right)$. Thus there are only four
potentials. As we discussed, potential $V_{A}\left(\theta\right)$ provides the
conservation law of angular momentum.

For potential $V_{B}\left(\theta\right)$, if we go into Cartesian coordinates
the Lagrangian function for the Ermakov system (19) is

$L_{B}\left(x,\dot{x},y,\dot{y}\right)=\frac{1}{2}\left(\dot{x}^{2}+\dot{y}^{2}-\frac{V_{0}}{x^{2}}\right)~{},$
(26)

which provides the second-order differential equations
$\ddot{x}=\frac{V_{0}}{x^{3}}$ , $\ddot{y}=0.$ The time-independent
conservation laws are
$J\left(x,\dot{x}\right)=\frac{1}{2}\left(\dot{x}^{2}+V_{0}x^{-2}\right)$ and
$I^{2}=\dot{y}^{2}$. The potential $V_{C}\left(\theta\right)$ gives the same
conservation laws with $\left(x,y\right)\rightarrow\left(y,x\right)$.

For potential $V_{D}\left(\theta\right)$ in Cartesian coordinates the
Lagrangian function becomes

$L_{D}\left(x,\dot{x},y,\dot{y}\right)=\frac{1}{2}\left(\dot{x}^{2}+\dot{y}^{2}-\frac{V_{1}}{x^{2}}-\frac{V_{2}}{y^{2}}\right)~{},$
(27)

with equations of motion $\ddot{x}=\frac{V_{1}}{x^{3}}$ and
$\ddot{y}=\frac{{}_{2}}{y^{3}}$, for which the conservation laws are
$J_{1}\left(x,\dot{x}\right)=\frac{1}{2}\left(\dot{x}^{2}+V_{1}x^{-2}\right)$
and
$J_{2}\left(y,\dot{y}\right)=\frac{1}{2}\left(\dot{y}^{2}+V_{1}y^{-2}\right)$.

Finally, for the potential function $V_{E}\left(\theta\right)$ we have the
Lagrangian

$L_{E}\left(x,\dot{x},y,\dot{y}\right)=\frac{1}{2}\left(\dot{x}^{2}+\dot{y}^{2}-\frac{V_{0}}{\left(\alpha
y-x\right)^{2}}\right).$ (28)

By doing the second change of variables $x=X+\alpha y$ it follows that
$L_{E}\left(X,\dot{X},y,\dot{y}\right)=\frac{1}{2}\left(\dot{X}^{2}+2\alpha\dot{X}\dot{Y}+\left(1+\alpha^{2}\right)\dot{y}^{2}-\frac{V_{0}}{X^{2}}\right)$
for which the equations of motion are
$\ddot{X}=\frac{V_{0}\left(1+\alpha^{2}\right)}{X^{3}}$,
$\ddot{y}=-\frac{\alpha V_{0}}{x^{3}}$. The time-independent conservation laws
are $J\left(X,\dot{X}\right)=\frac{1}{2}\left(\dot{X}^{2}-V_{0}X^{-2}\right)$
and
$I\left(X,\dot{X},\dot{Y}\right)=\left(2\alpha\dot{X}\dot{Y}+\left(1+\alpha^{2}\right)\dot{y}^{2}\right)$.

We have seen that in all cases for which additional point symmetries exist the
Hamiltonian Ermakov system, when it is written in Cartesian coordinates, the
potential function $\frac{V\left(\theta\right)}{\rho^{2}}$ becomes
$V\left(x,y\right)=\frac{V_{1}}{x^{2}}+\frac{V_{2}}{y^{2}}$ and
$V\left(x,y\right)=\frac{V_{0}}{\left(\alpha y-x\right)^{2}}$. In these cases
the additional point symmetries follow from the the gradient Killing
symmetries of the Euclidian space.

##  4 The 3D generalized Ermakov system

Consider now the three-dimensional Ermakov system with Lagrangian function

$L\left(\rho,\dot{\rho},\theta,\dot{\theta},\phi,\phi\right)=\frac{1}{2}\left(\dot{\rho}^{2}+\rho^{2}\dot{\theta}+\rho^{2}\sin^{2}\theta~{}\dot{\phi}^{2}-\frac{V\left(\theta,\phi\right)}{\rho^{2}}\right)~{}$
(29)

and equations of motion

$\displaystyle\ddot{\rho}-\rho\dot{\phi}^{2}-\rho\sin^{2}\theta~{}\dot{\phi}^{2}-\frac{V\left(\theta,\phi\right)}{R^{3}}$
$\displaystyle=$ $\displaystyle 0,$ (30)
$\displaystyle\ddot{\theta}+\frac{2}{\rho}\dot{\rho}\dot{\theta}-\sin\theta\cos\theta~{}\dot{\phi}^{2}+\frac{V\left(\theta,\phi\right)_{,\theta}}{2R^{4}}$
$\displaystyle=$ $\displaystyle 0$ (31)
$\displaystyle\ddot{\phi}+\frac{2}{\rho}\dot{\rho}\dot{\phi}+\cot\theta~{}\dot{\theta}\dot{\phi}+\frac{V\left(\theta,\phi\right)_{,\phi}}{2R^{4}\sin^{2}\theta}$
$\displaystyle=$ $\displaystyle 0.$ (32)

At this point we discuss the analysis presented in [29]. The authors
investigated the functional forms of $V\left(\theta,\phi\right)$ for the
dynamical system to admit additional conservation laws based upon point
symmetries and contact symmetries. The authors determined the following
functional forms for the potential $V\left(\theta,\phi\right),$

$V_{A}\left(\theta,\phi\right)=V_{0}~{},~{}V_{B}\left(\theta,\phi\right)=V_{0}\left(\cos\theta\right)^{-2}\text{~{},~{}}V_{C}\left(\theta,\phi\right)=V_{0}\left(\sin\theta\right)^{-2}~{},$
(33)
$V_{D}\left(\theta,\phi\right)=V_{0}\left(\cos\theta\sin\phi\right)^{-2}~{},~{}V_{E}\left(\theta,\phi\right)=V_{0}\left(\cos\theta\cos\phi\right)^{-2}~{},$
(34)
$V_{F}\left(\theta,\phi\right)=\frac{8}{\cos\left(2\phi-2\theta\right)+\cos\left(2\phi+2\theta\right)+2\cos\left(2\theta\right)-2\cos\left(2\phi\right)+6}~{},$
(35)
$V_{G}\left(\theta,\phi\right)=\frac{8}{2\cos\left(2\phi\right)+2\cos\left(2\theta\right)-\cos\left(2\phi-2\theta\right)-\cos\left(2\phi+2\theta\right)+6}~{}.$
(36)

If we simplify potential functions $V_{F}$ and $V_{G}$ by using trigonometric
identities we find

$V_{F}\left(\theta,\phi\right)=\left(\cos^{2}\phi\sin^{2}\theta-1\right)^{-1},$
(37)
$V_{G}\left(\theta,\phi\right)=\left(1-\sin^{2}\phi\sin^{2}\theta\right)^{-1}.$
(38)

As we discussed above the potentials are related, for instance $V_{B}$ and
$V_{C}$ are the same potential function, as are also potentials
$V_{D},~{}V_{E}$ and $V_{F},~{}V_{G}$. In order to understand that we should
write the dynamical systems in Cartesians coordinates. we assume the
transformation

$\left(x,y,z\right)=\left(r\sin\theta,r\cos\theta\sin\phi,r\cos\theta\cos\phi\right)\text{.}$
(39)

Then

$\rho^{-2}V_{C}\left(\theta,\phi\right)=x^{-2}~{},~{}\rho^{-2}V_{D}\left(\theta,\phi\right)=y^{-2}$
(40)

and

$\rho^{-2}V_{F}\left(\theta,\phi\right)=\left(x^{2}+z^{2}\right)^{-1}~{}$ (41)

while in a similar way the remaining potentials reduce to similar potentials
in Cartesians coordinates, by doing a change on the variables
$\left\\{x,y,z\right\\}$. These potentials are not new and have been found
before and widely studied in [34]. In addition the classification scheme in
[29] is incomplete, for which see below.

We want to omit any calculation and use results from the previous section as
also important properties of the symmetries for the Euclidian space
$\mathbb{R}^{3}$. There is a direct relation of the Noether symmetries with
the elements of the Homothetic algebra of the Euclidian space, for more
details we refer the reader in [33]. The proper homothetic vector of the
$\mathbb{R}^{3}$ is the generator of the two vector fields of the
$SL\left(2,R\right)$ algebra. However, the $\mathbb{R}^{3}$ space admits six
isometries. Three rotations which form the $O\left(3\right)$ Lie algebra and
three translations which form the $T\left(3\right)$ Lie algebra. From the
nature of the $O\left(3\right)$, if an element of $O\left(3\right)$ is a
symmetry vector then we can change the coordinates
$\left(\theta,\phi\right)\rightarrow\left(\bar{\theta},\bar{\phi}\right),$ the
symmetry vector to be always the $\partial_{\bar{\phi}}$ which provides the
conservation law for the angular momentum $\mathcal{L}=$
$\rho^{2}\sin^{2}\theta~{}\dot{\phi}^{2}$. If we assume that two elements of
$O\left(3\right)$ to be Noether symmetries, then it follows that
$V\left(\theta,\phi\right)=V_{0}$.

Therefore, when $V\left(\theta,\phi\right)=V_{A}^{1}\left(\theta\right)$ or
$V\left(\theta,\phi\right)=V_{A}^{20}$, the additional Noether symmetries
follow from the elements of the $O\left(3\right)$ Lie algebra. On the other
hand, if we assume that the symmetry is generated by an element of the
$T\left(3\right)$ Lie algebra, it follows that in the Cartesians coordinates
the system is similar to that found above for the two-dimensional system.

Indeed, we perform the symmetry classification

$V_{A}\left(x,y,z\right)=\frac{V_{1}}{x^{2}}+\frac{V_{2}}{y^{2}}+\frac{V_{3}}{z^{2}}~{},$
(42)
$V_{B}\left(x,y,z\right)=\frac{V_{0}}{x^{2}+y^{2}}~{}+\frac{V_{1}}{z^{2}},$
(43) $V_{E}=\frac{V_{0}}{\left(\alpha x-\beta y-\gamma
z\right)^{2}}\text{~{},~{}~{}}V_{E}=\frac{V_{0}}{\left(\alpha x-\beta
y\right)^{2}}+\frac{V_{1}}{z^{2}}\,,$ (44)

where $V\left(x,y,z\right)=\rho^{-2}V\left(\theta,\phi\right)$.

It is obvious that we have found new potentials which have not been presented
before in [29]. Furthermore, if we apply the Killing tensors to determine new
potential functions, from the algorithm described in [35]; it is clear that
there are no additional potential functions.

##  5 Conclusions

In this work we revised previous results on the classification problem of the
three-dimensional Hamiltonian Ermakov system by using point and contact
symmetries. We show that the classification problem solved in [29] is not
correct and incomplete. We were able to show that with a constructive approach
by using previous results which relate properties of the background space with
the dynamical system.

We show that there is a natural extension on the classification scheme from
the two-dimensional Ermakov system to the three-dimensional problem. Hence we
can use the analysis to elevate the solution in higher dimensions. We
summarize our analysis in the following proposition.

Proposition: Consider the $n$-dimensional Hamiltonian Ermakov system generated
by the Lagrangian function

$L\left(\rho,\dot{\rho},\theta_{1},\dot{\theta}_{1},...,\theta_{n-1},\dot{\theta}_{n-1}\right)=\frac{1}{2}\left(\dot{\rho}^{2}+\rho^{2}\left(\dot{\theta}_{1}^{2}+\sin^{2}\theta_{1}\left(\dot{\theta}_{2}^{2}+\sin^{2}\left(...\right)\right)\right)-\frac{V\left(\theta_{1},\theta_{2},...,\theta_{n-1}\right)}{\rho^{2}}\right),$
(45)

which admits the $SL\left(2,R\right)$ as Noether symmetries. The functional
forms for the potential $V\left(\theta_{1},\theta_{2},...,\theta_{n-1}\right)$
in which additional conservation laws linear or quadratic in the momentum are:

$V\left(\theta_{1},\theta_{2},...,\theta_{n-1}\right)=V_{0}$ (46)
$V\left(x_{1},x_{2},...,x_{n}\right)=\sum_{i}V_{i}\left(x^{i}\right)^{-2}$
(47)
$V\left(x_{1},x_{2},...,x_{n}\right)=\sum_{i}\frac{V_{i}}{\sum_{\kappa}x^{\kappa}x_{\kappa}}+\sum_{i}\frac{V_{i}}{\left(x^{\lambda}\right)^{2}}~{},~{}\kappa\neq\lambda\text{,}$
(48)
$V\left(x_{1},x_{2},...,x_{n}\right)=\sum_{i}\frac{V_{i}}{\sum_{\kappa}\left(\alpha^{\kappa}x_{\kappa}\right)^{2}}+\sum_{i}\frac{\alpha_{\lambda}V_{i}}{\left(x^{\lambda}\right)^{2}}~{},~{}\kappa\neq\lambda\text{,~{}}$
(49)

where $\left(x_{1},x_{2},...,x_{n}\right)\,$ are the Cartesians coordinates
for the $n$-dimensional Euclidian space and
$\rho^{-2}V\left(\theta_{1},\theta_{2},...,\theta_{n-1}\right)=V\left(x_{1},x_{2},...,x_{n}\right)$.

In a future work we plan to extend this procedure to other attempts on the
generalization of the Ermakov system.

### Acknowledgements

GL was funded by Comisión Nacional de Investigación Científica y Tecnológica
(CONICYT) through FONDECYT Iniciación 11180126. GL thanks the Department of
Mathematics and the Vicerrectoría de Investigación y Desarrollo Tecnológico at
Universidad Católica del Norte for financial support. This work does not have
any conflicts of interest.

## References

  * [1] V. Ermakov, Univ. Isz. Kiev Series III 9, (1880) (translated by Harin A.O.)
  * [2] E.Pinney, Proc. Am. Math. Soc. 1 681 (1950)
  * [3] H.R. Lewis, Phys. Rev. Lett. 18 510 (1967)
  * [4] H.R. Lewis and W.B. Riesenfeld, J. Math. Phys. 10, 1458 (1969)
  * [5] E.R. Floyd, Phys. Lett. A 214, 259 (1996)
  * [6] M. Tsamparlis and A. Paliathanasis, Symmetry 10, 233 (2018)
  * [7] A. Paliathanasis and P.G.L. Leach, Phys. Lett. A 381, 1277 (2017)
  * [8] S.C. Mancas and H.C. Rosu, Phys. Lett. A 378, 2113 (2014)
  * [9] A. Sen and Z. Silagadze, Int. J. Theor. Phys. 59, 2187 (2020)
  * [10] C. Rogers, C. Hoenselaers and J. R. Ray, J. Phys. A: Math. and Gen. 26 2625 (1993)
  * [11] W.K. Schief, C. Rogers and A.P Bassom, J. Phys. A: Math. and Gen. 29 903 (1996)
  * [12] T. Padmanabhan, MPLA 33, 1830005 (2018)
  * [13] S. Moyo and P.G.L. Leach, J. Math. Phys. A: Math. Gen. 35, 5333 (2002)
  * [14] J.R. Ray and J.L Reid, Phys. Lett. A 71, 317 (1979)
  * [15] P.G.L. Leach, Phys. Lett. A 158, 102 (1991)
  * [16] M. Tsamparlis and A. Paliathanasis, J. Phys. A: Math. Theor. 45, 275202 (2012)
  * [17] F. Haas and J. Goedert, Phys. Lett. A 279 281 (2001)
  * [18] J. Goedert and F. Haas, Phys. Lett. A 239, 348 (1998)
  * [19] C. Athorne, J. Phys. A: Math and Gen 24, L1385 (1991)
  * [20] K.S. Govinder and P.G.L. Leach, Phys. Lett. A 186 391 (1974)
  * [21] A. Mitsopoulos and M. Tsamparlis, Eur. Phys. J. Plus 136, 933 (2021)
  * [22] P. Morando, C. Muriel and A. Ruiz, Mathematics 8, 2167 (2020)
  * [23] R. Campoamor-Stursberg, The Lie algebra SL(2,R) and Noether point symmetries of Lagrangian systems, Proceedings of the twentieth international conference on Geometry, Integrability and Quantization, pages 99-114, edited by I.M. Mladenov et al. (2019)
  * [24] M.C. Nucci and R. Campoamor-Stursberg, J. Math. Phys. 62, 012702 (2021)
  * [25] A. Ballesteros and A. Blasco, Annals of Physics 325, 2787 (2010)
  * [26] J. Roberts, S. Shkoller and T.C. Sideris, Comm. Math. Phys. 375, 1003 (2020)
  * [27] X. Gu, W.X. Ma and W.Y. Zhang, J. Math. Phys. 58, 053512 (2017)
  * [28] M. de la Cruz, N. Gaspar, L. Jimenez-Lara and R. Linares, Annals of Physics 379, 112 (2017)
  * [29] R. Naz and F.M. Mahomed, Math. Meth. Appl. Sci. 44, 4467 (2021)
  * [30] H. Stephani, Differential Equations: Their Solutions using Symmetry, Campridge: Cambridge University Press, (1989)
  * [31] E. Noether, Nachr. v.d. Ges. d. Wiss. zu Gottingen 235, (1918)
  * [32] A. Halder, A. Paliathanasis and P.G.L. Leach, Symmetry 10, 744 (2018)
  * [33] M. Tsamparlis and A. Paliathanasis, J. Phys. A: Math. Theor. 44, 175202 (2011)
  * [34] M. Tsamparlis, A. Paliathanasis and L. Karpathopoulos, J. Phys. A: Math. Theor. 45, 275201 (2012)
  * [35] L. Karpathopoulos, M. Tsamparlis and A. Paliathanasis, J. Geom. Phys. 133, 279 (2018)