\section{Introduction}
\label{Intro}
Black holes have remained a laboratory of theoretical curiosities for the 100 years since their prediction. Their formation, stability and evolution have been  studied extensively \cite{Wald} and observational evidence in their favor has been mounting. The acceleration of extra-galactic cosmic rays \cite{Fermi:1949ee, Bhattacharjee:1998qc, Anchordoqui:2018qom}, production of highly relativistic jets in Blazars \cite{Halzen:2002pg} and the observed characteristics of Gamma-Ray Bursts (GRBs) \cite{Piran:1999kx} all show signatures of an inner core powered by a black hole. The detection of gravitational waves by the LIGO collaboration from the merging of black hole binaries \cite{Abbott:2016blz} in 2015 and subsequent events provided even stronger observational evidence in favor of black holes.

For photons in the black hole environment, there exists a least radius below which circular orbits are not sustainable resulting in collapse of the photons into the interior. The radius at which unstable circular orbit exists for photon is called the Photon Ring and for a Schwarzschild black hole lies at $r=3r_g$, where $r_g=GM/c^2$ is the gravitational radius of the black hole. It can be shown \cite{Weinberg:1972kfs}, that an incoming photon with an impact parameter $b<r_c=\sqrt{27}r_g$ would end up inside the photon ring and thus eventually inside the black hole, but the photons with $b>r_c$ will escape to infinity and create an `image' of the black hole that features a bright ring with a dark interior. The dark interior is evidence of the existence of a strong gravitational source and this image is commonly referred to as the `Shadow of a Black Hole'. A recent observational signature for black holes came from the imaging of the shadow of a supermassive black hole by the Event Horizon Telescope (EHT) collaboration \cite{Akiyama:2019cqa} which used a Very Long Baseline Interferometry (VLBI) array to observe the black hole at the centre of M87 (M$87^*$ from here onwards). Over the past decade, the excitement from the discovery of Sagittarius $A^*$ (Sgr $A^*$) at the centre of our galaxy has been growing, and is the next observational goal of the EHT. Such observations can give crucial signals to the near horizon dynamics of black holes \cite{Chen:2019fsq, Davoudiasl:2019nlo, Bambi:2019tjh, Vagnozzi:2019apd, Cunha:2019ikd}, one such signal that we study here is the development of ultralight boson clouds in the black hole environment.

The black hole shadow is subject to evolution due to the interaction of the black hole with its environment. The strong gravitational field of a Kerr black hole has been studied for its superradiant scattering effects. This happens when the rotational speed of spacetime itself exceeds that of the particle being scattered.  For waves the superradiance condition is that the frequency $\omega$ of an incoming wave satisfies \cite{Wald, Endlich:2016jgc}
\begin{equation}\label{eq:sr}
    0<\omega<m\omega_+
\end{equation}
were $\omega_+$ is the angular velocity of the black hole horizon and $m$ is the azimuthal angular momentum separation constant. This has been likened to Cerenkov effect and results in the outgoing flux being larger than the ingoing flux, at the cost of energy and angular momentum to the black hole. For extremely light particles the scattering solutions admit quantum field theoretic interpretation analogous to the Hawking radiation (and Schwinger effect), where quantum fluctuations can give rise to a virtual particle pair, of which one falls into the black hole and the other emerges (in Schwinger effect both emerge) as a net outgoing flux at infinity. Thus a quantised field of ultralight bosons coupled to Kerr geometry  gives rise to an intermediate effect, which has received attention in recent literature. In this, particles created by quantum fluctuations, and satisfying the superradiance condition do not emerge at infinity, but get bound in quasi-stationary states around the black hole. This process has been studied for both spin-0 \cite{Arvanitaki:2010sy} and spin-1 bosons \cite{Baryakhtar:2017ngi}, although we will focus on the spin-0 case in the current work. A precursor of this idea is the ``black hole bomb'' \cite{Press:1972zz, Hod:2014pza} wherein spontaneously created photons can destabilize the black hole when trapped in the black hole environment due to the presence of externally provided mirrors. As observed in \cite{Arvanitaki:2010sy} the occurrence of Hydrogen atom like bound states in Kerr geometry for ultralight bosons substitutes for the mirror like condition, and a black hole laser has been mooted in \cite{Landry:2016arq}. Such a phenomenon where particles arising from vacuum fluctuations remain confined in the vicinity of the strong gravitational source is best understood as \textit{quasi-Hawking} \textit{(qH)} effect.

Axions are a class of ultralight pseudo-scalar bosons proposed to resolve the $CP$ problem of strong interactions \cite{Peccei:2006as}, but occurring more generically in string theory, with possible values of rest mass ranging from $10^{-9}$ eV-$10^{-21}$ eV \cite{Arvanitaki:2010sy}. The bound states of these axions to black holes can result in the quasi-Hawking effect leading to a reduction of the spin parameter $a_*$ of the black hole which in turn could lead to substantial variation in the observed black hole shadow. In the current work we develop this idea to determine whether variation in the features of the black hole shadow is significant enough for detection and if so, whether it takes place over observational time scales. Based on this analysis, we identify the optimal candidate black hole for observation of this phenomenon. As mentioned before, we will focus on spin-0 bosons in this work which could be either scalar or pseudo-scalar. Hence, throughout the rest of the work `bosons' will refer to spin-0 bosons unless stated otherwise. We will use the $G=c=\hbar=1$ system of units for the rest of the work.

\section{Boson cloud formation}
\label{bosonCloud}
Consider a Kerr black hole with mass $M$, angular momentum $J$ and scalar bosons of mass $m_s$. It is convenient to use the rescaled mass parameter $\mu_a=m_s G/\hbar c$, which in the system of units defined above expresses the mass of the scalar field. It has been shown \cite{Starobinsky:1973aij} that in the limit $\mu_aM\ll1$ and $\omega M \ll1 $, the Klein-Gordon equation satisfied by the bosons in the Kerr geometry takes a relatively simple form of the Schr\"odinger equation for Hydrogen atom with the fine structure constant replaced by the gravitational fine structure constant $\alpha=\mu_aM$.  The energy eigenvalues in this case develop imaginary parts \cite{Ternov, Detweiler:1980uk}, whereas the real part could be expressed in terms of the quantum number $n$ of the usual quantum numbers $nlm$ by
\begin{equation}\label{eq:energy}
     \omega =\mu_a\Bigg(1-\frac{\alpha^2}{2n^2}\Bigg)
\end{equation}
On the other hand, the small imaginary part $\Gamma_{sr}$, gives rise to either damped or growing modes. In single particle quantum mechanics these modes may be interpreted either as trapped particles whose bound state is subject to eventual collapse, or whose amplitude grows, suggesting instability of the black hole \cite{Detweiler:1980uk}. However if we have ultra-light bosons, whose Compton wavelength is comparable to the black hole gravitational radius, the solutions may be interpreted to lead to spontaneous creation of particles and accumulation of the same in quasi-stationary modes around the black hole \cite{Ternov}. We refer to this as the quasi-Hawking effect.

During this process, bosons extract mass and angular momentum from the black hole and begin to populate the quasi-stationary states. This phenomenon leads to the formation of large boson clouds in the black hole environment. This black hole-boson cloud system is often referred to as the ``Gravitational Atom".
The population of the cloud increases exponentially with time and the growth stops when enough spin has been extracted from the black hole such that the superradiance condition Eq. (\ref{eq:sr}) is no longer satisfied. The occupation number $N$ of a quantum level, denoted by $nlm$, that satisfies the superradiance condition will grow exponentially with time at a rate $\Gamma_{sr}$ \cite{Arvanitaki:2014wva}
\begin{equation}\label{eq:growth}
     \frac{dN}{dt}\Bigg|_{sr}=\Gamma_{sr}N
\end{equation}
After the process is complete, the maximum occupancy of a level with azimuthal quantum number $m$ could be expressed as \cite{Arvanitaki:2010sy}
 \begin{equation}\label{eq:Nmax}
     N_{max}\simeq 10^{76}\times \Bigg(\frac{\Delta a_*}{0.1}\Bigg)\Bigg(\frac{M}{10M_\odot}\Bigg)^2
 \end{equation}
where $\Delta a _* $ is the change in black hole spin. The entire process occurs over characteristic time scale $\tau_{sr}$ which depends on the mass of the black hole $M$, mass of the scalar field $\mu_a$ and the spin parameter $a_*$.

\section{Superradiance time scale}
\label{SupTime}
We define the parameter $j=\sqrt{l(l+1)}$ which denotes the angular momentum per boson in the boson-cloud. Within the approximation $\alpha/l\ll1$, it can be shown that for black hole masses $M_\odot- 10^{12} M_\odot$, the permitted range of values for the scalar field mass is $10^{-9}$ eV$\geq\mu_a\geq10^{-21}$ eV. The spin parameter of the black hole, at any point in time, could then be expressed in terms of $j$, $\mu_a$ and the occupation number $N$ as
\begin{equation}\label{eq:a_*}
    a_*(N)=\frac{J-Nj}{(M-N\mu_a)^2}
\end{equation}
where $J$ and $M$ are the initial angular momentum and mass of the black hole. Using this formula in Eq. (\ref{eq:growth}) we get the superradiant time scale expression as
\begin{equation}\label{eq:tsr}
    \tau_{sr}= \int_{a_{i}}^{a_{min}} \frac{1}{\Gamma_{sr}(a_*,\alpha)N}\frac{dN}{da_*} da_*
\end{equation}
where $a_{min}$ denotes the lowest spin of black hole before violating the superradiance condition, and $a_i$ is the initial black hole spin. Here $\frac{dN}{da_*}$ and $N(a_*)$ can be found by inverting Eq. (\ref{eq:a_*}). $a_{min}$ is determined by $\alpha$ through the superradiance condition Eq. (\ref{eq:sr})
\begin{equation}\label{eq:amin}
  a_{min}=\frac{2k_{nlm}}{1+k_{nlm}^2}
\end{equation}
where $k_{nlm}(\alpha)=(2\alpha/m)(1-\alpha^2/2n^2)$.  In the $\alpha/l\ll1$ limit, the superradiance rate $\Gamma_{sr}$ is well approximated by \cite{Arvanitaki:2014wva}
\begin{equation}\label{eq:gamma}
   \Gamma_{sr} \approx \Gamma_{nlm}=2\mu_a\alpha^{4l+4}r_+(m\omega_+-\mu_a)C_{nlm}
\end{equation}
where
\begin{align}\label{eq:Cnlm}
&C_{nlm}=\frac{2^{4l+2}(l+n)!}{n^{2l+4}(n-l-1)!}\Bigg(\frac{l!}{(2l)!(2l+1)!}\Bigg)^2\nonumber\\ &\times \prod_{i=1}^{l}\Bigg(i^2(1-a_*^2)+4r_+^2(m\omega_+-\mu_a)^2\Bigg)
\end{align}

where $r_+=M+\sqrt{M^2-a^2}$ represents the event horizon of the black hole. The sign of $\Gamma_{sr}$ is determined by the sign of the term $(m\omega_+-\mu_a)$, in agreement with Eq. (\ref{eq:sr}) in the low $\alpha/l$ limit.

As shown in \cite{Arvanitaki:2010sy}, the function $\Gamma_{sr}$ drops exponentially with an increase in the quantum number $l$. Hence the bosons would start filling the states  corresponding to different values of $l$, with $l=1$ being the fastest growing level. Due to the subsequent slow down of the black hole, this will also be the first level to fall below the requirement of the superradiance condition. The subsequent evolution has many possibilities, and if observable can refine the confirmation of this process, but they do not interfere with the effect we discuss and we shall focus on the main effect. We will be concerned with the $l=1$ level from here onwards, unless mentioned otherwise.

Given a value for the initial spin of the black hole $a_i$, we can put an upper limit on the desirable value of $\alpha$ since the minimum spin should be less than the initial spin of the black hole i.e. $a_{min}(\alpha)< a_i$.
Taking a near extremal spin of $a_i=0.99$ and the condition $\alpha\ll1$, we get the upper bound on $\alpha$ to be $0.42$.
$\tau_{sr}$ is found to be relatively insensitive to the possible $a_i$ values. However, our numerical study shows that $\tau_{sr}$ has an $\sim\alpha^{-5.7}$ dependence and hence increases sharply for lower values of $\alpha$. From numerical integration, it is found out that $\alpha>0.19$ is a reasonable estimate to keep the time scale in observational limits, viz., $\leq75$ years for $10^5M_\odot$. Thus the optimistic range of values of $\alpha$ is $0.19\leq\alpha\leq0.42$. Since $\alpha \sim M m_s$, we can still have a large possible range for the mass of the bosons by choosing different mass for black holes.
Choosing a value of $\alpha=0.28$ and $a_i=0.99$, we find the superradiance time scale as
\begin{equation}\label{eq:tsrfinal}
    \tau_{sr}\approx 5.43\times \left(\frac{M}{10^5M_\odot}\right)\left(\frac{0.28}{\alpha}\right)^{5.7} \  \mathrm{years}

\end{equation}
It should be noted here that the dependence of $\tau_{sr}$ on $\alpha^{-5.7}$ is an approximation while the dependence on $M$ is exact. The precise value of the superradiant time scales can be obtained by numerically integrating Eq. (\ref{eq:tsr}). The values of the superradiance times reported in this paper are calculated by numerical integration of Eq. (\ref{eq:tsr}).

\section{Simulation and prediction}
\label{sim}
We have simulated the shadow of a Kerr black hole  for a static observer at infinity using the contour equations as provided in \cite{Bardeen:1973tla, Cunha:2018acu}. The features of the shadow contour of a black hole could be expressed in terms of the `Shadow Parameter' $\delta x$ defined as
\begin{equation}\label{eq:shadowpar}
    \delta x=(x_{max}-x_{min})
\end{equation}
and its `Circularity' defined as
\begin{equation}\label{eq:circ}
    \chi=\frac{(y_{max}-y_{min})}{(x_{max}-x_{min})}
\end{equation}
where $(x,y)$ denotes the coordinates of the black hole contour in the local sky of an observer at infinity. The parameter $\delta x$ and $\chi$ depends on the spin parameter and inclination $\theta_0$, which is the angle between the line of sight and the axis of rotation of the black hole. Table \ref{tab:table1} shows the shadow parameter and the fractional change in mass ($\delta m= (M_i-M_f)/M_i$), due to the extraction of mass by the boson cloud, from our simulation during different stages of the quasi-Hawking process. Note that the net extracted mass $\Delta M=(M_i-M_f)$ is calculated by multiplying the maximum occupancy of the boson cloud with the mass of individual bosons i.e. $\Delta M=N_{max}\mu_a$, where $N_{max}$ is given by Eq. (\ref{eq:Nmax}).
\begin{table}[b]
\caption{\label{tab:table1
The shadow parameter for an observer at infinity, with $\theta_0$= $90^\circ$, $60^\circ$, $17^\circ$ has been given for five values of the spin parameter $a_*$ corresponding to five values of the $\alpha$ parameter: $0.43$, $0.36$, $0.28$, $0.24$, $0.19$. The fractional change in mass of the black hole is also given in terms of $\delta m=\frac{\Delta M}{M_i}$ for an initial spin of $a_i=0.995$. The shadow parameters are given in units of the gravitational radius $r_g$
}
\begin{ruledtabular}
\begin{tabular}{ c c c c c }
\textrm{$a_*$}&
\textrm{$100\times\delta m$}&
\textrm{$\delta x\ (90^\circ)$}&
\textrm{$\delta x\ (60^\circ)$}&
\textrm{$\delta x\ (17^\circ)$}\\
\colrule
0.995 & 0 & 9.27 & 9.29 & 9.60\\
0.95 & 2.21 & 9.48 & 9.49 & 9.70\\
0.85 & 4.33 & 9.75 & 9.76 & 9.87\\
0.78 & 4.98 & 9.89 & 9.90 & 9.97\\
0.66 & 5.41 & 10.08 & 10.08 & 10.12\\
\end{tabular}
\end{ruledtabular}
\end{table}
\begin{table}[hbt]
\caption{\label{tab:table2
Taking the mass of Sgr$A^*$ as $M=4.2\times 10^6M_\odot$ and inclination angle $\theta_0=60^\circ$, we present the corresponding quantities namely $a_{min}$, $\tau_{sr}$, $m_s$, $\Delta d$ and $\Delta \chi$ for five representative values of $\alpha$ and for a fixed initial spin parameter $a_i=0.995$ ($\chi_i=0.902$):
}
\begin{ruledtabular}
\begin{tabular}{c c c c c c }
\textrm{$\alpha$}&
\textrm{$a_{min}$}&
\textrm{$\tau_{sr} (years)$}&
\textrm{$m_s (eV)$}&
\textrm{$\Delta d (\mu as) $}&
\textrm{$\Delta \chi$}\\
\colrule
$0.19$ &  $0.662$ & $2369.43$ & $3.81\times 10^{-17}$ & $1.30$ & 0.077 \\
$0.24 $& $ 0.777 $& $509.15 $& $4.81\times 10^{-17} $&$ 0.71$ & 0.060 \\
$0.28 $&  $0.848 $& $216.55 $& $5.62\times 10^{-17} $& $0.32$ & 0.046\\
$0.32 $&  $0.903$ & $121.61 $& $6.42\times 10^{-17} $& $0.07$ & 0.034\\
$0.34 $&  $0.924$ & $100.51 $& $6.82\times 10^{-17} $& $0.01$ & 0.028\\
\end{tabular}
\end{ruledtabular}
\end{table}
The recent imaging of the shadow of the black hole at the centre of M87 shows a bright ring $(\sim 42\pm 3\ \mu as)$ and a dark region at the centre with a contrast depression of about $10:1$ with the ring \cite{Akiyama:2019cqa}. This is evidence of the presence of an extremely compact object that lenses light from the accretion disk to create a shadow. The angular diameter of the ring is determined by the formula
\begin{equation}\label{eq:ringdia}
    d=42\times\Bigg(\frac{\delta x_i}{11}\Bigg)\Bigg(\frac{M}{6.5\times10^9M_\odot}\Bigg)\Bigg( \frac{16.8\ Mpc}{D}\Bigg) \mu as
\end{equation}
where $D$ is the distance from Earth to the black hole. Therefore a change in the black hole ring diameter could be given by
\begin{equation}\label{eq:delringdia}
    \Delta d=d\times\Bigg[\Bigg(\frac{\delta x_f}{\delta x_i}\Bigg)(1-\delta m)-1\Bigg]\ \mu as
\end{equation}
where $\delta x_i$ and $\delta x_f$ are the initial and final shadow parameters before and after the quasi-Hawking process. For a change in the spin parameter $\Delta a_*= 0.1$ (from $0.95$ to $0.85$ for $\theta_0=17^\circ$ in Table \ref{tab:table1}) and mass $\delta m=0.043$  the angular diameter of the ring of M$87^*$, with an initial mass of $\sim 6.2\times 10^9 M_\odot$ and a distance of $\sim 16.8$ Mpc \cite{Akiyama:2019cqa}, changes by $\Delta d \sim 0.28\ \mu$as. For observations at a wavelength of 1.3 mm, the EHT collaboration has a theoretical diffraction-limit resolution of about $\sim25\ \mu$as \cite{Akiyama:2019cqa}, making this variation far below the resolution of EHT. Moreover, the excessive mass stretches this variation over a duration of $4.5\times10^{5}$ years. Hence, the observation of shadow evolution of M$87^*$ and similar higher mass black holes will remain unrealistic in this scenario.

A more promising case is the supermassive black hole at the centre of our galaxy, Sagittarius $A^*$ under observation by the EHT collaboration
for which  $M$ lies in the range $\sim 3.3\times 10^6 M_\odot$ \cite{Aschenbach:2006vb} to  $4.1\times 10^6 M_\odot$  \cite{Ghez:2008ms, Gillessen:2008qv}, $\theta_0=60^\circ$ \cite{Roelofs:2019nmh} and $a_*$ is determined to be $\sim 0.99676$ \cite{Aschenbach:2004fx, Aschenbach:2006vb}.  Table \ref{tab:table2} shows the time scales of variation, the change in the shadow diameter $\Delta d$ and change in circularity of the shadow from our simulations for different values of the $\alpha$ parameter. For observation to be made, the time scale must be as low as possible with the change in shadow being as large as possible. Therefore there exists a tradeoff since $\tau_{sr}$, $\Delta d$ and $\Delta \chi$ all increases with an increase in $\alpha$. As already mentioned, with a resolution limit of 25 $\mu$as, the variations in the shadow feature of Sgr$A^*$ is far below the resolution of EHT. Improvements in the resolution of EHT has already been suggested with the possibility that EHT analyses can attain the accuracy of $1.5\ \mu$as \cite{Johannsen:2015hib} as well as the proposed imaging techniques at lower wavelengths $\sim 0.8$ mm and with space-based interferometers aiming to achieve a resolution of $\sim3\ \mu$as \cite{Fish}. As is evident from Table \ref{tab:table2}, the search for ultralight bosons in the range $\alpha=(0.3-0.2)$ might become instrumental in the future of black hole imaging with resolution in the order of 0.1 $\mu$as.

The ratio of $M$ and $D$ must satisfy $M/D\geq1.64\times10^{16}$ kg/m for the ring diameter $d$ to be large enough for observation in the current EHT resolution. If we focus our attention to black holes with mass $M\leq10^{6}M_\odot$ which have favourable superradiant time scales,
we can put an upper bound on $D$ given by $D\leq3.95\times 10^3$ pc. This is the intra-galactic scale and hence we only need to focus on black holes inside the Milky Way galaxy.
For a solar mass black hole with $M=10M_\odot$ inside the milky way, $D$ must be $3.95\times10^{-2}$ pc for its ring diameter to be observable. The nearest such black hole candidate is the V616 Monocerotis which has $D\sim10^3$ pc \cite{Cantrell:2010vh} from Earth thus violating the requirement on $M/D$.
For the present the only candidates which satisfy the $M/D$ constraint are M$87^*$ and Sgr$A^*$ and since the time duration of the effect for M$87^*$ is way too large for observations, the optimal candidate for observation of shadow evolution is Sgr$A^*$. An important assumption of our analysis lies in the fact that there should be no previous population of boson cloud in the black hole environment. But even if the boson cloud levels are previously populated, the population depletes through self annihilation as discussed in \cite{Arvanitaki:2014wva}. This depletion process takes place over $\tau_{regge}\sim 10^{11}$ yr for black holes of $M\sim10^6M_\odot$ for the $l=1$ level \cite{Arvanitaki:2014wva}. And only after depletion of lower $l$ levels, the higher $l$ levels could start to fill. Thus, the effect might also be observed for older black holes, by observing shadow evolution for higher $l$ levels, the essential analysis for which remains the same as done in this work.

\section{Conclusion}
\label{conclusion}
We have searched for signatures of Ultralight Boson cloud evolution in the features of a black hole shadow. Our analysis shows the variation in the shadow due to boson cloud evolution is far below the current EHT resolution, even for the most optimistic case. But such searches may become instrumental in future EHT with the optimal candidate for shadow evolution being Sgr$A^*$ subject to different parameters such as its spin and mass of the ultralight bosons. Further, the discoverability of such an effect would improve significantly if  a population of $10^3 M_\odot-10^5 M_\odot$ black holes were to be found inside the Milky Way galaxy.

Another interesting signature of Ultralight Boson Cloud from black hole shadow can be obtained if the backreaction of the boson cloud becomes significant enough on the background metric. The photon geodesics in the black hole environment would then get perturbed and hence the shape of the shadow will change. This change will be reflected in the features of the shadow of the black hole. A very close study in this respect using backward ray tracing has been done in \cite{Cunha:2015yba}.

In conclusion, the next best thing to observing the Hawking effect itself would be to observe quasi-Hawking effect obtaining in the vicinity of Kerr black holes where the superradiance condition can be satisfied. We have shown that the shadow of a black hole could be used to detect such an effect, simultaneously providing a detection mechanism for such ultra-light bosonic particles.

\section{Acknowledgement}
\label{ack}
We would like to thank M. B. Paranjape for useful discussion and comments.

\nocite{*}


\section{Introduction}
Since the invention of a blockchain data structure in 2008 various
cryptocurrencies have been emerging, evolving and gaining popularity.
This popularity is explained by the fact that blockchain systems are
fully operable without a trusted entity. Recent cryptocurrencies
support creation of \textit{smart contracts} -- stateful programs
executed on a blockchain that encode the rules governing
transactions. The execution of smart contracts is enforced by the
consensus algorithm in the underlying blockchain system.

Smart contracts are a powerful tool to encode arbitrary contractual
agreements in a machine-readable form but as with any programs they
are error-prone and hard to reason about. Furthermore, the blockchain
systems design principles make impossible contract's code modification
after it has been deployed to blockchain.  Also smart contracts hold
and transfer significant amount of digital currency which makes them
an attractive target of various attacks and drastically increases the
cost of an error in smart contract code. It has been shown that many
contracts deployed to public ledgers contain security vulnerabilities
and these vulnerabilities have led to theft of millions of US dollars
in cryptocurrency equivalent. Thus, it is of paramount importance to
ensure that smart contracts are correct. Various methods based on
formal verification have been proposed to achieve this
goal~\cite{bhargavan2016formal, luu2016making, hirai2017defining}.

Another method to build correct programs is program synthesis, which
has a lot in common with formal verification.  The problem of program
synthesis is formulated as follows: given a specification in formal
logic, construct a program conforming to that specification. This
problem is known to be undecidable in general, however various methods
were proposed for some special cases of programs. Unlike formal
verification, automated synthesis of smart contracts has received very
little attention, although program synthesis application for smart
contracts looks promising given the fact that they are relatively
small (less than 100 SLOC in average~\cite{hegedus2019towards}).

Program synthesis is a very broad topic and in this work we only focus
on the problem of FSM synthesis where programs are defined in terms of
FSMs. The rationale behind this is that smart contract logic can often
be expressed with an FSM. Moreover, modeling contracts as FSMs is a
recommended design pattern for Solidity -- a language of
Ethereum~\cite{wood2014ethereum}
contracts~\cite{solidity-fsm-pattern}. In fact there is a tool
\textsc{VeriSolid}~\cite{mavridou2017designing} that facilitates
creating FSM smart contract models and generating Solidity code from
these models. A user can specify temporal properties and verify that
generated contracts conform to these properties.

\begin{figure}[h!]
  \centering
  \includegraphics[scale=0.6]{gdraw/diagram-new}
  \caption{Data-flow diagram of the proposed approach.}
  \label{fig:approach-diagram}
\end{figure}

In this work we employ techniques and tools
(\textsc{EFSM-tools}~\footnote{\url{https://github.com/ulyantsev/EFSM-tools/}})
outlined in~\cite{efsm-tools}. We have no intent to compare different
FSM synthesis tools as for case studies in
Section~\ref{sec:case-studies} synthesis solving terminates within
seconds. In our approach input events of a FSM correspond to methods
of a contract and output actions -- to implementations of those
methods. We synthesize smart contract FSM models based on formal
specification in temporal logic and test scenarios.  Afterwards, given
the contract's state declaration and the implementation of its methods
in a corresponding programming language, we can generate contract's
code that is guaranteed to be correct with respect to the
specification.  Code generation is straightforward and similar to that
in \textsc{VeriSolid} tool, however \textsc{VeriSolid} does not
support multiple transitions labeled by the same event so we had to
implement our own tool
\textsc{fsmc}~\footnote{\url{https://github.com/d-suvorov/fsmc/}}.
The high-level data-flow diagram for the proposed approach is shown in
Figure~\ref{fig:approach-diagram}.

\textbf{Contributions.} To the best of our knowledge, this work is the
first attempt to employ specification-based program synthesis
techniques to automatically generate smart contract source
code. Specifically, we provide case studies to show that LTL synthesis
can be successfully applied for some types of contracts to generate
their FSM models and use these models to obtain source code that meets
some formal properties. We also briefly discuss the applicability of
program synthesis for automated smart contract generation.

\section{Background and related work}
In this section we introduce some basic concepts of blockchain systems
and smart contracts necessary to understand the rest of the paper.
Then we define FSMs that are used to model smart contracts and
introduce formalism that are used to specify them. Finally we state
the problem of specification-based FSM synthesis and provide some
references to its efficient solutions.

\subsection{Smart contracts}
A blockchain is a list of records, called blocks, containing some
data. Blockchain can be used as a ledger that is maintained in a
distributed network, for instance in cryptocurrencies this ledger
stores a transaction list. Effectively, a ledger in cryptocurrencies
stores the mapping from accounts to their balances in digital
currency. We refer to this digital currency as \textit{coins}.  The
nodes of a network called \textit{miners} execute consensus algorithm
and decide on which blocks will be added.  It is assumed that the
majority of nodes are honest as they are incentivized to add new valid
blocks, and the integrity of the system is based on that assumption.

Modern blockchain systems support \textit{smart contracts} --
executable programs stored on a blockchain.  A contract is executed by
miners which agree on the outcome of the execution and update the
blockchain accordingly. Hence arbitrary contractual agreements can be
expressed in program code and enforced without relying on a trusted
party. Most popular smart contract systems share the same concepts but
for the rest of the paper we consider Ethereum-like smart contracts.

In Ethereum~\cite{wood2014ethereum}, smart contracts are a type of
accounts associated with executable code and a storage file.  Smart
contracts can be created by sending a transaction of a special kind to
a blockchain.  A code of the contract consists of methods -- entry
points which are called when transactions are send to the address of
that contract. Essentially, transactions act as method
invocations. Contracts can receive coins with these transactions and
send coins to other accounts via \texttt{send} instructions. Each
instruction of a method consumes some amount of \textit{gas} during
execution. The user who sends a transaction must pay gas for its
execution. If a transaction runs out of gas during its execution the
control returns to sender. An example of a smart contract is shown in
the next section.

The problem of creating correct smart contracts have been actively
studied over the past years.  One of the first work by
Delmolino~\emph{et al.} outlines common pitfalls specific to smart
contract development. Since then, a variety of techniques have been
used to verify smart contracts.  Different tools based on symbolic
execution were created: \textsc{Oyente}~\cite{luu2016making},
\textsc{Mythril}~\cite{mythrill-github},
\textsc{Manticore}~\cite{manticore-github},
\textsc{Maian}~\cite{nikolic2018finding}.  An early work of
Bhargavan~\emph{et al.} uses F* programming
language~\cite{bhargavan2016formal}. Lately modern theorem provers
have been employed to formalize different aspects of smart contracts
in blockchain systems~\cite{hirai2017defining, amani2018towards,
  grishchenko2018semantic} and used to mechanize reasoning about those
aspects.  Sergey~\emph{et al.}~\cite{sergey2018scilla} design a new
functional language, implement its embedding into Coq and mechanize
proofs of safety and liveness properties of smart
contracts. Flint~\cite{schrans2018writing} is a programming language
that was designed specifically for writing robust smart
contracts. Flint employs linear type theory to prevent unintentional
loss of coins. An interesting example of contract-oriented languages
are Bamboo~\cite{bamboo-github} and
Obsidian~\cite{coblenz2017obsidian} as they model smart contracts as
state machines and make state transitions explicit.  Model checking
can also be used to verify smart contracts. Nehai~\emph{et
  al.}~\cite{nehai2018model} use \textsc{NuSMV} model checker to
create a blockchain application model (including a blockchain model
itself) and check its temporal properties.

Idelberger~\emph{et al.}~\cite{idelberger2016evaluation} propose to
use defeasible deontic logic to create smart contracts, which is
somewhat similar to our approach. However, the execution of such smart
contracts relies on an external logic engine. This setup negatively
affects the performance. We generate FSM models which can be encoded
in some programming language and executed directly.

\subsection{Specification-based FSM synthesis}

\begin{figure}[h!]

  \sidesubfloat[]{
  \begin{tikzpicture}
    [
      ->,>=stealth',
      shorten >=1pt,

      node distance=3.5cm,

      initial text=$ $
    ]

    \node[state,initial] (1) {$1$};
    \node[state,right of=1] (2) {$2$};

    \draw (1) edge[bend left, above] node{$e_2 / z_1$} (2)
          (2) edge[bend left, below] node[text width=1cm,align=center]{$e_1 / z_1$ \\ $e_2 / z_2$} (1)
          (1) edge[loop above] node{$e_1 / z_1$} (1);
  \end{tikzpicture}
  } \\

  \sidesubfloat[]{
  \begin{tikzpicture}
    [
      ->,>=stealth',
      shorten >=1pt,

      node distance=2.5cm,

      initial text=$ $,
      state/.style={
           rectangle,
           rounded corners,
           draw=black, thick,
           minimum height=2em,
           inner sep=2pt,
           text centered,
      },
      every loop/.style={min distance=10mm,looseness=10}
    ]

    \node[state,initial] (1) {$(1, e_1, z_1, 1)$};
    \node[state,right of=1,xshift=1cm] (2) {$(2, e_1, z_1, 1)$};
    \node[state,initial,below of=1] (3) {$(1, e_2, z_1, 2)$};
    \node[state,below of=2] (4) {$(2, e_2, z_2, 1)$};

    \draw
    (2) edge (1)
    (1) edge (3)
    (4) edge (1)
    (3) edge[bend left=8] (2)
    (2) edge[bend left=8] (3)
    (3) edge[bend left=7] (4)
    (4) edge[bend left=7] (3)
    (1) edge[loop above]  (1);
  \end{tikzpicture}
  }

  \caption{An example of an FSM (a) and its Kripke structure (b).}
  \label{fig:kripke}
\end{figure}

We are following~\cite{efsm-tools} and define a \textit{finite state
  machine} (FSM) as a tuple $(S, s_{\mathrm{init}}, E, Z, \delta,
\lambda)$, where
\begin{itemize}
  \item $S$ is a finite set of states,
  \item $s_{\mathrm{init}} \in S$ is the \textit{initial state},
  \item $E$ is a finite set of input \textit{events},
  \item $Z$ is a finite set of output \textit{actions},
  \item $\delta : S \times E \to S$ is the \textit{transition
    function},
  \item $\lambda : S \times E \to Z^{*}$ is the \textit{output
    function} (with $Z^{*}$ we denote a set of strings over $Z$).
\end{itemize}
An FSM reads a sequence of input events one by one and transforms it
into a sequence of output actions.  With each input event it generates
new output actions according to $\lambda$ and changes its active state
according to $\delta$.

\textbf{Model checking.}  Model checking is a technique for
automatically verifying finite-state systems with respect to a given
specification~\cite{grumberg1999model}. It is common to formalize the
specification as a formula in temporal logic. In linear temporal logic
(LTL), formulas express some properties of execution
paths~\cite{pnueli1977temporal}.  To proceed with its definition we
first define a Kripke structure. With $P$ we denote a set of atomic
propositions, which characterize execution states.  Formally, a Kripke
structure is a tuple $(S_K, I, T, L)$, where
\begin{itemize}
  \item $S_K$ is a set of states,
  \item $I \subseteq S_K$ is a set of initial states,
  \item $T \subseteq S_K \times S_K$ is a transition relation, which
    must be left-total (that is, from each state there is a transition
    to at least one state),
  \item $L : S_K \to 2^P$ is a labeling function.
\end{itemize}
An example of an FSM and a corresponding Kripke structure is shown in
Figure~\ref{fig:kripke}. To label transitions we use this notation:
\textit{input event / output action}.

LTL formulas are defined over infinite paths in Kripke structures. The
formulas are built up from temporal operators, atomic propositions and
connectives familiar from propositional logic ($\wedge$, $\vee$,
$\neg$, $\to$).  If $f$ is a Boolean formula, then it simply states
with which atomic propositions the first state of the path is marked.
If $f$ is an LTL formula, then saying that $f$ holds for a state of an
infinite path means that it holds for the infinite suffix of the path
starting from this state. The following temporal operators can be
used.
\begin{itemize}
  \item The $ne\textbf{X}t$ operator: $\textbf{X}\:f$ means that $f$
    has to hold at the next state of the path.
  \item The $\textbf{G}lobally$ operator: $\textbf{G}\:f$ means that
    $f$ has to hold on the entire suffix of the path.
  \item The $\textbf{F}uture$ operator: $\textbf{F}\:f$ means that $f$
    eventually has to hold (somewhere on the suffix of the path
    starting from this state).
  \item The $\textbf{U}ntil$ operator: $f\:\textbf{U}\:g$ means that
    $f$ has to hold at least until $g$ becomes true, which must hold
    at this or some future state.
  \item The $\textbf{R}elease$ operator: $f\:\textbf{R}\:g$ means that
    $g$ has hold until and including the point where $f$ first becomes
    true; if $f$ never becomes true, $g$ must remain true forever.
\end{itemize}
The formula $f$ is true for some Kripke model $M$ means that it is
satisfied for all infinite paths of $M$.

\textbf{FSM synthesis.} The problem of FSM synthesis by the
specification is well-known. In its different statements the
specification may be given as temporal formula, a set of test
scenarios or the combination of the two.  A test scenario for FSM $(S,
s_{init}, E, Z, \delta, \lambda)$ is a sequence of pairs $(e_1, A_1),
\dotsc, (e_n, A_n)$, where each $e_i \in E$ and $A_i \in Z^{*}$ and, a
FSM conforms to it if and only if it produces a sequence of actions
$A_1 \cdot A_2 \cdot \dotsc \cdot A_n$ (with $\cdot$ we denote
sequence concatenation) given a sequence of events $e_1, \dotsc, e_n$
as its input. Exact synthesis methods are mostly based on transition
to SAT~\cite{efsm-tools, walkinshaw}. In~\cite{efsm-tools} different
approaches based on transition to SAT and QSAT were examined. In the
most efficient approach scenarios are encoded in SAT and LTL formulas
are incorporated with iterative counterexample prohibition. In
\textsc{BoSy} tool~\cite{not-bosy, bosy}, encoding in QSAT instead of
SAT is used and a transition system is generated only from a set of
LTL formulas. The generated transition system is guaranteed to be
minimum in terms of the number of states.

\section{Case studies}\label{sec:case-studies}

\begin{figure}[h!]

  \subimport{tikz/}{blinded-auction}
  \caption{Blinded auction. FSM generated for $\var{size} = 4$
    states.}
  \label{fig:blinded-auction}
\end{figure}

\begin{figure*}[h!]
  \lstinputlisting[multicols=2]{snippets/blinded-auction.sol}
  \caption{Blinded auction. Generated Solidity code.}
  \label{fig:blinded-auction-code}
\end{figure*}

This section contains case studies that evolve from simple example for
illustration purposes only to more realistic examples taken from the
literature. For each case study we provide a formal LTL specification
and a result model that was generated with this specification and test
scenarios.

In this section we extend FSMs with guard conditions.  A \textit{guard
  condition} is a Boolean expression that labels FSM transition.
Guard conditions affect the semantics of FSMs in the following way:
the transition can be executed only if its guard condition is
satisfied.  We use this notation to label transitions:
\mbox{\textit{input event [guard condition] / output action}}.  A test
scenario now is a sequence of triples $\{ (e_i, c_i, A_i) \}$, where
$e_i$ is an input event, $c_i$ is a guard condition and $A_i$ is a
sequence of output actions. If a sequence of output actions is omitted
(as in \mbox{\textit{input event [guard condition] /}} or $(e_i, c_i,
.)$) it is implicitly assumed that it consists of one action with the
same name as the corresponding input event.

In our approach input events of an FSM correspond to methods of a
contract and output actions -- to implementations of those methods.
We specify smart contracts with a set of LTL formulas in terms of
these events and actions.  Formal specification is then combined with
test scenarios and provided as input to \textsc{EFSM-tools} to
generate an FSM that complies with given specification and test
scenarios. Figure~\ref{fig:blinded-auction} shows an example of a
generated FSM. Given the implementation of FSM output actions and the
definitions of used predicates, FSM can be translated to executable
code.  Figure~\ref{fig:blinded-auction-code} shows an example of
generated Solidity code, where lines 2\,--\,12 correspond to
contract's state definition, lines 14\,--\,19 -- to predicate
definition and lines 40\,--\,44 -- to $\mathtt{bid}$ action definition
(other action definitions are omitted for brevity).

\subsection{Crowdfunding}
For illustrative purpose, let us first consider a simplistic example
of a crowdfunding platform.  In such a platform users can donate coins
(denoted with event $\var{donate}$) during a predefined period of time
which ends when variable $\var{donationOver}$ becomes true. When the
donation period is over, the owner of the campaign can request
collected coins (event $\var{getFunds}$). After that donors can claim
their donations back (event $\var{reclaim}$) and possibly get them
back if not enough coins were collected during the campaign
($\var{notFunded} = \true$). Intuitively, one can model the logic
of this contract using an FSM with two states. More formally, the
logic of described contract is formulated as follows:
\begin{enumerate}
\item $\var{getFunds}$ cannot happen more than
  once;\label{prop:crowdfunding.1}
\item $\var{donate}$ cannot happen after $\var{getFunds}$ has
  happened;
\item $\var{reclaim}$ cannot happen before
  $\var{getFunds}$;\label{prop:crowdfunding.3}
\item $\var{getFunds}$ can happen only if $\var{donationOver} =
  \true$;
\item $\var{reclaim}$ can happen only if $\var{notFunded} =
  \true$.
\end{enumerate}
With a straightforward translation we can formalize these properties
in LTL as follows.
\begin{align}
& \textbf{G} (\var{getFunds}\to\textbf{X} \neg \textbf{F} \var{getFunds}) \\
& \textbf{G} (\var{getFunds}\to\neg \textbf{F} \var{donate}) \\
& \var{getFunds}\:\textbf{R}\:\neg \var{reclaim} \\
& \textbf{G} (\var{getFunds}\to\var{donationOver}) \\
& \textbf{G} (\var{reclaim}\to\var{notFunded})
\end{align}
Figure~\ref{fig:crowdfunding} shows an FSM generated with
\textsc{EFSM-tools} from this specification the set of scenarios $S =
\{ s_1, s_2, s_3 \}$, where
\begin{align*}
s_1 = [ & (\var{donate}, \true, .), (\var{donate}, \true, .),\\
        & (\var{donate}, \true, .)];\\
s_2 = [ & (\var{getFunds}, \var{donationOver}, .),\\
  & (\var{reclaim}, \var{notFunded}, .),\\
  & (\var{reclaim}, \var{notFunded}, .)];\\
s_3 = [ & (\var{donate}, \true, .), (\var{getFunds}, \var{donationOver}, .),\\
  & (\var{reclaim}, \var{notFunded}, .), (\var{reclaim}, \var{notFunded}, .)].
\end{align*}
Another advantage of using formal logic is that now we can reason
about about the system.  For instance, from
properties~\ref{prop:crowdfunding.1} and \ref{prop:crowdfunding.3} we
can derive that $\var{getFunds}$ cannot happen after $\var{reclaim}$.

\begin{figure}[h!]
  \centering

  \subimport{tikz/}{crowdfunding}
  \caption{Crowdfunding. FSM generated for $\var{size} = 2$ states.}
  \label{fig:crowdfunding}
\end{figure}

\subsection{Blinded auction}
Now we consider a more realistic example of blinded auction taken
from~\cite{mavridou2017designing}. During a predefined period of time
after contract creation, users can make hidden bids (denoted with
event $\var{bid}$). When this period is over ($\var{biddingOver} =
\true$) the auction can be closed (event $\var{close}$), after
which follows the next period when users are allowed to $\var{reveal}$
their bids. When the second period is over ($\var{revealOver} =
\true$) the auction can be finished (event $\var{finish}$). At
any time before finishing the auction can be canceled
($\var{cancel}$), after which users can claim back their bids (event
$\var{unbid}$).

The logic of this blinded auction can be formulated as follows (we
provide corresponding LTL formulas alongside).
\begin{enumerate}
\item $\var{close}$, $\var{finish}$ and $\var{cancel}$ cannot happen more than once:
  \begin{align*}
    & \textbf{G} (\var{close}\to\textbf{X} \neg \textbf{F} \var{close}), \\
    & \textbf{G} (\var{finish}\to\textbf{X} \neg \textbf{F} \var{finish}), \\
    & \textbf{G} (\var{cancel}\to\textbf{X} \neg \textbf{F} \var{cancel});
  \end{align*}
\item $\var{bid}$ cannot happen after $\var{close}$ has happened:
  \begin{align*}
    & \textbf{G} (\var{close}\to\neg \textbf{F} \var{bid});
  \end{align*}
\item $\var{reveal}$ and $\var{cancel}$ cannot happen after
  $\var{finish}$ has happened:
  \begin{align*}
    & \textbf{G} (\var{finish}\to\neg \textbf{F} (\var{reveal}\vee\var{cancel}))
  \end{align*}
\item $\var{finish}$, $\var{close}$, $\var{bid}$ and $\var{reveal}$
  cannot happen after $\var{cancel}$ has happened:
  \begin{align*}
    & \textbf{G} (\var{cancel}\to\neg \textbf{F} (\var{finish}\vee\var{close}\vee\var{bid}\vee\var{reveal}))
  \end{align*}
\item $\var{finish}$ and $\var{reveal}$ cannot happen before
  $\var{close}$:
  \begin{align*}
    & \var{close}\:\textbf{R}\:(\neg \var{finish}\wedge\neg \var{reveal});
  \end{align*}
\item $\var{unbid}$ cannot happen before $\var{cancel}$:
  \begin{align*}
    & \var{cancel}\:\textbf{R}\:\neg \var{unbid};
  \end{align*}
\item $\var{withdraw}$ cannot happen before $\var{finish}$:
  \begin{align*}
    & \var{finish}\:\textbf{R}\:\neg \var{withdraw};
  \end{align*}
\item $\var{close}$ can happen only if $\var{biddingOver} =
  \true$:
  \begin{align*}
    & \textbf{G} (\var{close}\to\var{biddingOver});
  \end{align*}
\item $\var{finish}$ can happen only if $\var{revealOver} =
  \true$:
  \begin{align*}
    & \textbf{G} (\var{finish}\to\var{revealOver}).
  \end{align*}
\end{enumerate}

This formal LTL specification and a set of test scenarios was used to
generate a FSM depicted in Figure~\ref{fig:blinded-auction}. Test
scenarios for this and the next case study can be found
online~\footnote{\url{https://github.com/d-suvorov/sc-gen}}.  Given
Solidity code associated with output actions labeling FSM transitions,
the full smart contract code can be generated.  The code generated
from synthesized FSM is shown in
Figure~\ref{fig:blinded-auction-code}.

\subsection{License server}
This is an example taken from~\cite{idelberger2016evaluation}. Here we
consider a smart contract that could be used to monitor the execution
of the agreement between two parties, namely Licensor and Licensee. We
assume that these parties perform as client agents connected to some
blockchain network. The contract consists of the following clauses
which were copied from~\cite{idelberger2016evaluation} and annotated
with event names that we are going to use in the rest of this section
to model contract execution.
\begin{enumerate}
\item The Licensor grants the Licensee a license to evaluate the
  Product ($\var{getLicense}$).
\item Licensee must not $\var{publish}$ the results of the evaluation
  ($\var{use}$) of the Product without the approval
  ($\var{getApproval}$) of the Licensor; the approval must be obtained
  before the publication. If the Licensee publishes results of the
  evaluation of the Product without approval from the Licensor, the
  Licensee has 24 hours to $\var{remove}$ the material.
\item The Licensee must not publish comments ($\var{comment}$) on the
  evaluation of the Product, unless the Licensee is permitted to
  publish the results of the evaluation.
\item If the Licensee is commissioned ($\var{getCommission}$) to
  perform an independent evaluation of the Product, then the Licensee
  has the obligation to publish the evaluation results.
\item This license will $\var{terminate}$ automatically if Licensee
  breaches this Agreement.
\end{enumerate}

There is not a timer that can be used to trigger some transition in a
blockchain system, that is why we introduce special events
$\var{noRemove}$ and $\var{noPublish}$. $\var{noRemove}$ happens if
the results of the evaluation of the Product were not removed in due
time. $\var{noPublish}$ happens if the Licensee was commissioned to
perform an independent evaluation and did not published the
results. Thus LTL specification is less abstract and at the first
sight less intuitive than the informal description above. For instance
to state that it is permitted to use and publish results after getting
an approval we introduce the property
$\textbf{G}(\var{getApproval}\to\textbf{G}(\neg\var{noRemove}))$:
``$\var{noRemove}$ cannot happen after $\var{getApproval}$ has
happened''. Given that property, and the fact that $\var{getApproval}$
can only happen after $\var{getLicense}$, we can derive that
$\var{terminate}$ cannot happen after $\var{getApproval}$.  The latter
property can be formalized and verified, which is an advantage of
using formal logic system for specifying a contract.

We introduce LTL specification in two stages. The following formulas
encode general principles of the system (e.g., ``$\var{remove}$ cannot
happen if nothing has been published'').
\setcounter{equation}{0}
\begin{align}
  & \textbf{G} (\var{getLicense}\to\textbf{X} \neg \textbf{F} \var{getLicense}) \\
  & \textbf{G} (\var{getApproval}\to\textbf{X} \neg \textbf{F} \var{getApproval}) \\
  & \textbf{G} (\var{noRemove}\to\textbf{X} \neg \textbf{F} \var{noRemove}) \\
  & \textbf{G} (\var{noPublish}\to\textbf{X} \neg \textbf{F} \var{noPublish}) \\
  & \var{publish}\:\textbf{R}\:\neg \var{remove} \\
  & \textbf{G} (\var{remove}\to\textbf{X} (\var{publish}\:\textbf{R}\:\neg \var{remove})) \\
  & \var{publish}\:\textbf{R}\:\neg \var{noRemove} \\
  & \textbf{G} (\var{remove}\to\textbf{X} (\var{publish}\:\textbf{R}\:\neg \var{noRemove})) \\
  & \var{getLicense}\:\textbf{R}\:\neg \var{getApproval} \\
  & \var{getLicense}\:\textbf{R}\:\neg \var{getCommission} \\
  & \var{getCommission}\:\textbf{R}\:\neg \var{noPublish} \\
  & \textbf{G} (\var{publish}\to\textbf{X} (\var{getCommission}\:\textbf{R}\:\neg \var{noPublish})) \\
  & \textbf{G} (\var{terminate}\to\textbf{X} \neg \textbf{F} \var{noRemove}) \\
  & \textbf{G} (\var{terminate}\to\textbf{X} \neg \textbf{F} \var{noPublish}) \\
  & \textbf{G} (\var{terminate}\to \nonumber\\
  & \phantom{AA}\neg \textbf{F} (\var{getLicense}\vee\nonumber \\
  & \phantom{AA}\phantom{AA}\var{getApproval}\vee\var{getCommission}))
\end{align}
The following formulas encode contractual clauses.
\setcounter{equation}{0}
\begin{align}
& (\var{getLicense}\vee\var{terminate})\:\textbf{R}\:\nonumber\\
& \phantom{AA}((\var{use}\vee\var{publish})\to\var{terminate}) \\
& \textbf{G} (\var{getLicense}\to \nonumber\\
& \phantom{AA}\neg \textbf{F} ((\var{use}\vee\var{publish})\wedge\var{terminate})) \\
& (\var{getApproval}\vee\var{getCommission}\vee\var{terminate})\:\textbf{R} \nonumber\\
& \phantom{AA} (\var{comment}\to\var{terminate}) \\
& \textbf{G} (\var{noRemove}\to\var{terminate}) \\
& \textbf{G} (\var{noPublish}\to\var{terminate}) \\
& \textbf{G} (\var{getApproval}\to\textbf{G} \neg \var{noRemove}) \\
& \textbf{G} (\var{getCommission}\to\textbf{G} \neg \var{noRemove})
\end{align}

An FSM generated from this specification and test scenarios is shown
in Figure~\ref{fig:license}. Test scenarios are available online (the
link was provided in the previous section).

\begin{figure*}[h!]и
  \centering

  \subimport{tikz/}{license}
  \caption{License. FSM generated for $\var{size} = 6$ states.}
  \label{fig:license}
\end{figure*}

The original contract is formulated in terms of deontic modalities,
i.e., in terms of permissions, obligations and related concepts.  A
shortcoming of specifying this smart contract in temporal logic (and
using it to synthesize FSM model) is not tracking these modalities:
given a sequence of actions there is no easy way to figure out
permissions and obligations of contractual parties. On the other hand,
the resulting representation is efficient, which is important in case
of on-chain deployment, and could be used to determine whether or not
the given sequence of actions leads to contract termination.

\section{Conclusion and discussion}
We argue that automated program synthesis could find more applications
for smart contract generation as they often have simpler structure
than general purpose programs and it is an open research question
whether a Turing-complete language is necessary for smart contract
programming. We would like to draw attention of the community to the
problem of automatic synthesis of smart contracts.  We provided
several case studies to show that LTL synthesis can be applied to
generate FSM models for smart contracts of some types. In these models
input events correspond to smart contract methods and output actions
correspond to these methods' implementation. Generated FSM models can
further be used to obtain programs that are correct with respect to
some formal temporal properties.

Our approach can be straightforwardly extended for systems of
interacting smart contracts and used to specify, synthesize and verify
them. Another interesting method to extend the supported class of
verified properties is to incorporate source-level formal verification
techniques. Output actions in synthesized FMSs correspond to smart
contract methods, hence we can use other verification frameworks to
prove source-level properties about these methods and combine them
with temporal properties of FSM models itself.

In practice smart contracts receive, hold and send coins and
transaction execution costs some amount of gas.  It is important to be
able to use these concepts to formulate properties of interest about
smart contracts.  Hence, other possibilities for future work include
using SAT or SMT to encode such concepts and extending specification
language to incorporate these.

A drawback of using LTL synthesis is that LTL is not expressive enough
to formulate properties of kind ``$\phi$ \emph{can happen} infinitely
often (while $\psi$ has not happened)''. For example the formula
$\textbf{EG}\:\phi$ in CTL can be used to state that there is a path
on which $\phi$ always holds. However this problem can be easily
mitigated by specifying test scenarios in which $\var{donate}$ repeats
$N$ times, where $N$ is greater than the number of transitions of FSM
to be generated.

Despite the simple remedy for the above problem we believe that a more
suitable formal system to specify smart contracts is yet to be
identified. It is an interesting research question: how to strike a
balance between simplicity and expressivity of this system to allow
effective synthesis of practical smart contracts.

\ifCLASSOPTIONcompsoc

  \section*{Acknowledgments}
\else

  \section*{Acknowledgment}
\fi

The authors would like to thank Igor Buzhinsky and Daniil Chivilikhin
for their feedback.  This work was supported by the Government of
Russia (Grant 08-08).

\bibliographystyle{IEEEtran}


\section{Background}

Nos\'e-Hoover dynamics was developed in 1984 as a side benefit of a Centre Europ\'een de Calcul
Atomique et Mol\'eculaire (``CECAM'') Workshop on Constrained Dynamics organized by Carl Moser.
The workshop was held at Orsay, about 20 miles southwest of Paris.  Shuichi Nos\'e and Bill
Hoover met by chance at the Orly airport a few days prior to the Orsay meeting and were able to
spend several hours together near the Notre Dame cathedral, discussing Nos\'e's recent work on the
thermal control of molecular dynamics simulations\cite{b2,b3}.

Seeking better to understand Nos\'e's innovative work Hoover applied Nos\'e's ideas to the
one-dimensional harmonic oscillator problem\cite{b4,b5,b6,b7,b8,b9,b10,b11,b12}. He generated
hundreds of solutions of the set of three ordinary differential equations using the fourth-order
Runge-Kutta algorithm. The time-dependent variables $(q,p,\zeta)$ are respectively the oscillator
coordinate, momentum, and friction coefficient. Here are the three equations :
$$
\{ \ \dot q = p \ ; \ \dot p = -q -\zeta p \ ; \ \dot \zeta = [ \ p^2 - 1 \ ]/\tau^2 \ \} \
[ \ {\rm Nos\acute{e}-Hoover} \ ] .
$$
Provided that the mean value of the friction coefficient $\zeta$ is finite ( so that the longtime
average  of its time derivative, $\langle \ \dot \zeta \ \rangle$, vanishes ) the last equation
implies that the mean oscillator temperature $\langle \ p^2 \ \rangle$ is unity for long times.
Thus $\zeta$ acts as a ``thermostat''. Posch, Hoover, and Vesely explored the detailed nature of
the oscillator solutions\cite{b5} for a variety of response times $\tau$.  Wang and Yang extended
this work\cite{b9,b10} and found, in addition to the known periodic, toroidal, and fat-fractal
chaotic trajectories, additional periodic trajectories, and tori, in the form of knots ! The types
of solutions found vary with $\tau$ and with the initial values of $(q,p,\zeta)$.  In the present
work we choose $\tau = 1$.

\section{Consequences of Time Scaling}

In the Summer of 1996 Carl Dettmann discovered a {\it vanishing} Hamiltonian which precisely
reproduces the time-dependence of the Nos\'e-Hoover flow where the Nos\'e-Hoover momentum becomes
$(p/s)$\cite{b6,b7}.
$$
{\cal H}_D(q,p,s,\zeta) \equiv (s/2)[ \ q^2 + (p/s)^2 + \ln(s^2) + \zeta^2  \ ] \equiv 0 \rightarrow
$$
$$
s^2 = e^{-(q^2 + (p/s)^2 + \zeta^2)} \ .
$$
The ``time-scaling variable'' $s$ has the conjugate momentum $p_s = \zeta$. $| s |$ must be less than
unity for ${\cal H}_D$ to vanish. We select positive values, $0 < s < 1$, in our numerical work. The
various resulting flows can occupy one-, two-, or three-dimensional subspaces of the full stationary
solution, the Gaussian function :
$$
(2\pi)^{-3/2}\exp [ \ -( q^2 + (p/s)^2 + \zeta^2 )/2 \ ] \ .
$$
With this Gaussian distribution known the normalized probability density for $s$ follows easily,
$$
\sqrt{(2/\pi)\ln(s^{-2})} \ .
$$

\begin{figure}
\includegraphics[width=3.0in,angle=+90.]{fig1.eps}
\caption{
Analytic and numerical probability densities for the time-scaling variable $s$. Both are based on
the three-dimensional Gaussian distribution with numerical values from the Hoover-Holian model.
}
\end{figure}
Figure 1 compares this analytic distribution to a thousand-point histogram from a fourth-order
Runge-Kutta solution of the ( ergodic ) Hoover-Holian oscillator equations\cite{b8} :
$$
\{ \ \dot q = p \ ; \ \dot p = - q - \zeta p - \xi p^3 \ ; \ \dot \zeta = p^2 - 1
\ ; \ \dot \xi = p^4 - 3p^2 \ \} \ .
$$
For the Figure  $q$ and $p$ were initially unity and the two control variables were zero.
Ten million timesteps, $dt = 0.001$, were used.  The stationary distribution for the Hoover-Holian
equations is the four-dimensional Gaussian $(2\pi)^{-2}\exp[ \ ( -q^2 - p^2 -\zeta^2 -\xi^2 )/2 \ ] \ $.
Because the model is ergodic, covering the entire four-dimensional Gaussian\cite{b8}, we were able to use
the three-dimensional Hoover-Holian subset $( \ q^2,p^2,\zeta^2 \ )$ data as a model for the stationary
Dettmann distribution $( \ q^2,(p/s)^2,\zeta^2 \ )$ with $s$ determined from the condition ${\cal H}_D
\equiv 0$. These numerical data, confirming our analytic work, are shown in Figure 1.

Following up his earlier investigations of oscillator trajectories ( including knots\cite{b9,b10}
! ) Professor Xiao-Song Yang has recently proved that the oscillator motion, independent of the
chosen initial conditions, must nearly always cross the $\zeta = 0$ plane\cite{b1}.  Yang
considered the Nos\'e-Hoover equations, which follow from Dettmann's Hamiltonian with the
replacement $(p/s) \rightarrow p$ :
$$
\{ \ \dot q = p \ ; \ \dot p = - q - \zeta p \ ; \ \dot \zeta = p^2 - 1 \ \} \ .
$$
The only situation in which the $\zeta = 0$ plane is not crossed repeatedly is an unstable
straight-line portion of the $\zeta$ axis :
$$
q(t) = q(0) = 0 \ ; \ p(t) = p(0) = 0 \ ; \ \zeta(t) = \zeta(0) - t \ .
$$

In the present work we first consider oscillator trajectories from the standpoint of the continuity
equation in $(q,p,\zeta)$ space. Because the Nos\'e-Hoover equations are not strictly Hamiltonian,
except in the ${\cal H}_D \equiv 0$ case discovered by Dettmann, the Nos\'e-Hoover flow is
compressible -- the three-dimensional divergence is locally nonzero, responding linearly to the
control variable $\zeta$ :
$$
(\partial \dot q/\partial q) + (\partial \dot p/\partial p) +
(\partial \dot \zeta/\partial \zeta) = 0 -\zeta + 0 \ [ \ {\rm Dettmann=Nos\acute{e}-Hoover} \ ] \ .
$$
Consider a longtime trajectory. Evidently a {\it positive} longtime average of $\zeta$ would
correspond to a {\it vanishing of the comoving volume} and a dimensionality loss. A negative average
would correspond to divergence, a numerical instability.  In fact, the continuity equation has been
used to explain the fractal nature of chaotic flows with positive friction\cite{b12}.

In $(q,p,\zeta)$ space the continuity equation shows that the comoving volume element $\otimes$
vanishes and can become fractal if the longtime-averaged control variable is positive. The volume
diverges, and the simulation stops, if that averaged variable is negative. The motion equations for
the oscillator, in either $(q,p,\zeta)$ space or $(q,p,s,p_s=\zeta)$ space, can also be used to prove
Professor Yang's zero-crossing result.  We turn to that next.

\section{Proofs of Professor Yang's $\zeta = 0$ Plane Result}

Yang's recent contribution\cite{b1} considers the three-variable Nos\'e-Hoover oscillator and
shows algebraically that any longtime trajectory -- other than the special constant $(q,p,\dot \zeta)$
unstable straight line -- must repeatedly cross the $\zeta = 0$ plane.  This is a handy result as the
Poincar\'e sections at that plane are commonly used to diagnose the fractal character of nonlinear
flows. Yang's proof-of-crossing is relatively long, thirty pages, mainly algebra. Let us provide two
simpler demonstrations of his result. Multiply the three motion equations by $q$, $p$, and $\zeta$
respectively and compute their longtime $(t \rightarrow \infty)$ averages $\langle \ \dots \ \rangle$
in the usual way :
$$
\langle \ f[q,p,\zeta] \ \rangle =
(1/t)\int_0^{t\rightarrow \infty} f[ \ q(t^\prime),p(t^\prime),\zeta(t^\prime) \ ]dt^\prime \ .
$$
Assume also that
$\langle \ q^2,p^2,\zeta^2 \ \rangle$ are finite ( so that their time derivatives average to zero ).
The three Nos\'e-Hoover differential equations then give three identities:
$$
\{ \
  \langle \ qp \ \rangle = 0 \ ;
\ \langle \ qp \ \rangle = \langle \ -\zeta p^2 \ \rangle \ ;
\langle	  \ \zeta \ \rangle = \langle	       \ \zeta p^2 \ \rangle \
\ \} \ .
$$
Combining the three shows that the mean value of $\zeta$ vanishes, equivalent to Professor Yang's
result.

An even simpler demonstration follows from Nos\'e's original Hamiltonian\cite{b2,b3}, ${\cal H}_N \equiv
(1/s){\cal H}_D$, which gives a simple evolution equation for $s$ : $\dot s = p_s$. Because
$p_s$ and $\zeta$ are identical, as shown by Dettmann, the time-average of the $\dot s$ equation shows directly (assuming numerical convergence
of the motion) that the control variable $\zeta$ has mean value zero, again implying Yang's result.

\section{An Afterword for Young Researchers}

Lingering geometric and topological questions remain where the chaotic sea is concerned. The
sea is an enduring paradoxical concept. Is it a set of three-dimensional points? Is it a
continuum with holes here and there? Is it just a single chaotic trajectory? Is it an ill-defined
limit? These questions remain at the research frontier.  Let us have a look at the chaotic sea
for the Nos\'e-Hoover oscillator.

{\bf Figure 2} shows cross-sections of the three-dimensional oscillator's $(q,p,\zeta)$
phase space showing about ten million crossings of the three planes where each of the variables
vanishes.  The fourfold symmetry of these sections reflects the time-reversibility of the motion
equations as well as the fact that any solution $\{ \ +q,+p,+\zeta \  \}_t$ implies the existence of
a mirror-image solution $\{ \ -q,-p,+\zeta \  \}_t$, as well as $\{ \ +q,-p,-\zeta \ \}_t$.

\begin{figure}
\includegraphics[width=2.0in,angle=-90.]{fig2.eps}
\caption{
Sections of the Nos\'e-Hoover Chaotic Sea where $q$ or $p$ or $\zeta$ vanishes.  Only one quadrant is
shown here as each of the Sections has fourfold symmetry.
}
\end{figure}

For $\tau = 1$ about six percent of the Gaussian distribution\cite{b13} $e^{-(q^2+p^2+\zeta^2)/2}$
appears to be a cohesive connected sea, penetrated by infinitely many regular orbits with zero
Lyapunov exponents $\{ \ \lambda \ \}$. These exponents describe the longtime average growth or
decay rates of small perturbations. The boundary between points with a positive $\lambda$,
charateristic of the sea, and points with all zero Lyapunov exponents is evidently murky and
uncertain. The boundary region is likely fractal in the sense that in the neighborhood of any
chaotic point in the sea there must be other points only a small distance away, located on
periodic orbits of great length, well beyond our capacity to compute in any meaningful way.

The mathematics of such sets of points is confused through concepts related to Hilbert's Hotel and
the Banach-Tarski Theorem.  Hilbert's Hotel, with positive integer room numbers, is alway full
( with $\aleph_0$ guests ) but with always an available room ( by moving customers from n to n+1 ).
Similar mappings of points in two or three ( or many ) dimensional spaces enable the disection of
a sphere into a finite number of pieces which can then be reassembled to make two spheres. This is
an active field of mathematics at the moment. For a nicely illustrated description of the
Banach-Tarski paradox see Reference 14.

\section{Acknowledgement}

We thank Professor Xiao-Song Yang for useful email communications and the anonymous referee
for several useful suggestions which have improved this manuscript.

\newpage