$\displaystyle=\frac{C_{A}}{C_{F}}\,\gamma_{K,q}^{(1)}\,.$ (A.10)

With the implementation of $\overline{\text{MS}}$ subtraction described in
section 4.1, the coefficients in the $a_{s}$ expansion (4.9) of the
renormalisation factor are sums of poles,

$\displaystyle\widehat{Z}_{a}^{(N)}(\zeta/\mu^{2})$
$\displaystyle=\sum_{i=1}^{N+1}\frac{1}{\epsilon^{i}}\,\widehat{Z}_{a}^{(N,i)}(\zeta/\mu^{2})\,.$
(A.11)

The analysis of these pole terms proceeds in the same way as was described for
the DPD renormalisation factor ${}^{RR^{\mskip
1.5mu\prime}\mskip-1.5mu}\mskip-1.5muZ_{ab}$ in section 2.2, with the
simplification that Mellin convolutions are replaced by ordinary products. As
a result, we find that the highest pole at order $a_{s}^{N}$ is
$\epsilon^{-(N+1)}$ and that the anomalous dimension can be obtained from the
single pole as usual:

$\displaystyle\gamma_{F,a}^{(N-1)}(\zeta/\mu^{2})$
$\displaystyle=-2N\widehat{Z}_{a}^{(N,1)}(\zeta/\mu^{2})\,.$ (A.12)

The LO and NLO coefficients in (A.11) read

$\displaystyle\widehat{Z}_{a}^{(1,1)}(\zeta/\mu^{2})$
$\displaystyle=-\frac{1}{2}\mskip 1.5mu\gamma_{F,a}^{(0)}(\zeta/\mu^{2})\,,$
(A.13) $\displaystyle\widehat{Z}_{a}^{(1,2)}$
$\displaystyle=-\frac{1}{4}\mskip 1.5mu\gamma_{K,a}^{(0)}\,,$ (A.14)
$\displaystyle\widehat{Z}_{a}^{(2,1)}(\zeta/\mu^{2})$
$\displaystyle=-\frac{1}{4}\mskip 1.5mu\gamma_{F,a}^{(1)}(\zeta/\mu^{2})\,,$
(A.15) $\displaystyle\widehat{Z}_{a}^{(2,2)}(\zeta/\mu^{2})$
$\displaystyle=\frac{1}{8}\,\biggl{\\{}\Bigl{(}\gamma_{F,a}^{(0)}(\zeta/\mu^{2})\Bigr{)}^{2}+\beta_{0}\gamma_{F,a}^{(0)}(\zeta/\mu^{2})-\frac{1}{2}\mskip
1.5mu\gamma_{K,a}^{(1)}\biggr{\\}}$
$\displaystyle=\frac{1}{8}\,\biggl{\\{}\frac{1}{4}\Bigl{(}\gamma_{K,a}^{(0)}\Bigr{)}^{2}\ln^{2}\frac{\zeta}{\mu^{2}}-\Bigl{(}\frac{1}{2}\beta_{0}+\gamma_{a}^{(0)}\Bigr{)}\mskip
1.5mu\gamma_{K,a}^{(0)}\ln\frac{\zeta}{\mu^{2}}$ $\displaystyle\qquad\ \
+\Bigl{(}\gamma_{a}^{(0)}\Bigr{)}^{2}+\beta_{0}\gamma_{a}^{(0)}-\frac{1}{2}\mskip
1.5mu\gamma_{K,a}^{(1)}\biggr{\\}}\,,$ (A.16)
$\displaystyle\widehat{Z}_{a}^{(2,3)}(\zeta/\mu^{2})$
$\displaystyle=\frac{1}{8}\mskip
1.5mu\gamma_{K,a}^{(0)}\biggl{\\{}\gamma_{F,a}^{(0)}(\zeta/\mu^{2})+\frac{3}{4}\beta_{0}\biggr{\\}}\,.$
(A.17)

## References

  * [1] CDF collaboration, F. Abe et al., _Double parton scattering in $\bar{p}p$ collisions at $\sqrt{s}$ = 1.8 TeV_, _Phys. Rev. D_ 56 (1997) 3811.
  * [2] D0 collaboration, V. M. Abazov et al., _Study of double parton interactions in diphoton + dijet events in $p\bar{p}$ collisions at $\sqrt{s}$ = 1.96 TeV_, _Phys. Rev. D_ 93 (2016) 052008 [1512.05291].
  * [3] LHCb collaboration, R. Aaij et al., _Measurement of the J/ $\psi$ pair production cross-section in pp collisions at $\sqrt{s}$ = 13 TeV_, _JHEP_ 06 (2017) 047 [1612.07451].
  * [4] ATLAS collaboration, M. Aaboud et al., _Study of the hard double-parton scattering contribution to inclusive four-lepton production in $pp$ collisions at $\sqrt{s}$ = 8 TeV with the ATLAS detector_, _Phys. Lett._ B790 (2019) 595 [1811.11094].
  * [5] CMS collaboration, _Observation of same-sign WW production from double parton scattering in proton-proton collisions at $\sqrt{s}$ = 13 TeV_, 2206.02681.
  * [6] N. Paver and D. Treleani, _Multi-Quark Scattering and Large $p_{T}$ Jet Production in Hadronic Collisions_, _Nuovo Cim. A_ 70 (1982) 215.
  * [7] M. Mekhfi, _Multiparton Processes: an Application to Double Drell-Yan_ , _Phys. Rev. D_ 32 (1985) 2371.
  * [8] T. Sjostrand and M. van Zijl, _Multiple Parton-parton Interactions in an Impact Parameter Picture_ , _Phys. Lett. B_ 188 (1987) 149.
  * [9] B. Blok, Y. Dokshitzer, L. Frankfurt and M. Strikman, _The Four jet production at LHC and Tevatron in QCD_ , _Phys. Rev. D_ 83 (2011) 071501 [1009.2714].
  * [10] J. R. Gaunt and W. Stirling, _Double Parton Scattering Singularity in One-Loop Integrals_ , _JHEP_ 06 (2011) 048 [1103.1888].
  * [11] M. G. Ryskin and A. M. Snigirev, _A Fresh look at double parton scattering_ , _Phys. Rev._ D83 (2011) 114047 [1103.3495].
  * [12] B. Blok, Yu. Dokshitser, L. Frankfurt and M. Strikman, _pQCD physics of multiparton interactions_ , _Eur. Phys. J._ C72 (2012) 1963 [1106.5533].
  * [13] M. Diehl, D. Ostermeier and A. Schäfer, _Elements of a theory for multiparton interactions in QCD_ , _JHEP_ 03 (2012) 089 [1111.0910].
  * [14] A. V. Manohar and W. J. Waalewijn, _A QCD Analysis of Double Parton Scattering: Color Correlations, Interference Effects and Evolution_ , _Phys. Rev. D_ 85 (2012) 114009 [1202.3794].
  * [15] A. V. Manohar and W. J. Waalewijn, _What is Double Parton Scattering?_ , _Phys. Lett. B_ 713 (2012) 196 [1202.5034].
  * [16] M. G. Ryskin and A. M. Snigirev, _Double parton scattering in double logarithm approximation of perturbative QCD_ , _Phys. Rev._ D86 (2012) 014018 [1203.2330].
  * [17] J. R. Gaunt, _Single Perturbative Splitting Diagrams in Double Parton Scattering_ , _JHEP_ 01 (2013) 042 [1207.0480].
  * [18] B. Blok, Y. Dokshitzer, L. Frankfurt and M. Strikman, _Perturbative QCD correlations in multi-parton collisions_ , _Eur. Phys. J. C_ 74 (2014) 2926 [1306.3763].
  * [19] M. Diehl, J. R. Gaunt and K. Schönwald, _Double hard scattering without double counting_ , _JHEP_ 06 (2017) 083 [1702.06486].
  * [20] B. Cabouat, J. R. Gaunt and K. Ostrolenk, _A Monte-Carlo Simulation of Double Parton Scattering_ , _JHEP_ 11 (2019) 061 [1906.04669].
  * [21] B. Cabouat and J. R. Gaunt, _Combining single and double parton scatterings in a parton shower_ , _JHEP_ 10 (2020) 012 [2008.01442].
  * [22] O. Fedkevych and A. Kulesza, _Double parton scattering in four-jet production in proton-proton collisions at the LHC_ , _Phys. Rev. D_ 104 (2021) 054021 [2008.08347].
  * [23] F. A. Ceccopieri and M. Rinaldi, _Enlighting the transverse structure of the proton via double parton scattering in photon-induced interactions_ , _Phys. Rev. D_ 105 (2022) L011501 [2103.13480].
  * [24] B. Blok and J. Mehl, _Perturbative Color Correlations in Double Parton Scattering_ , 2210.13282.
  * [25] K. Golec-Biernat and A. M. Stasto, _The momentum sum rule and factorization of double parton distributions_ , 2212.02289.
  * [26] P. Bartalini and J. R. Gaunt, eds., _Multiple Parton Interactions at the LHC_ , vol. 29. World Scientific Publishing, 2019, 10.1142/10646.
  * [27] R. Kirschner, _Generalized Lipatov-Altarelli-Parisi Equations and Jet Calculus Rules_ , _Phys. Lett. B_ 84 (1979) 266.
  * [28] V. P. Shelest, A. M. Snigirev and G. M. Zinovev, _The Multiparton Distribution Equations in QCD_ , _Phys. Lett. B_ 113 (1982) 325.
  * [29] A. M. Snigirev, _Double parton distributions in the leading logarithm approximation of perturbative QCD_ , _Phys. Rev. D_ 68 (2003) 114012 [hep-ph/0304172].
  * [30] J. R. Gaunt and W. J. Stirling, _Double Parton Distributions Incorporating Perturbative QCD Evolution and Momentum and Quark Number Sum Rules_ , _JHEP_ 03 (2010) 005 [0910.4347].
  * [31] F. A. Ceccopieri, _An update on the evolution of double parton distributions_ , _Phys. Lett. B_ 697 (2011) 482 [1011.6586].
  * [32] M. G. A. Buffing, M. Diehl and T. Kasemets, _Transverse momentum in double parton scattering: factorisation, evolution and matching_ , _JHEP_ 01 (2018) 044 [1708.03528v4].
  * [33] S. Moch, J. A. M. Vermaseren and A. Vogt, _The Three loop splitting functions in QCD: The Nonsinglet case_ , _Nucl. Phys. B_ 688 (2004) 101 [hep-ph/0403192].
  * [34] A. Vogt, S. Moch and J. A. M. Vermaseren, _The Three-loop splitting functions in QCD: The Singlet case_ , _Nucl. Phys. B_ 691 (2004) 129 [hep-ph/0404111].
  * [35] S. Moch, J. A. M. Vermaseren and A. Vogt, _The Three-Loop Splitting Functions in QCD: The Helicity-Dependent Case_ , _Nucl. Phys. B_ 889 (2014) 351 [1409.5131].
  * [36] A. Vogt, F. Herzog, S. Moch, B. Ruijl, T. Ueda and J. A. M. Vermaseren, _Anomalous dimensions and splitting functions beyond the next-to-next-to-leading order_ , _PoS_ LL2018 (2018) 050 [1808.08981].
  * [37] M. Mekhfi, _Correlations in Color and Spin in Multiparton Processes_ , _Phys. Rev. D_ 32 (1985) 2380.
  * [38] M. Mekhfi and X. Artru, _Sudakov Suppression of Color Correlations in Multiparton Scattering_ , _Phys. Rev. D_ 37 (1988) 2618.
  * [39] G. Curci, W. Furmanski and R. Petronzio, _Evolution of Parton Densities Beyond Leading Order: The Nonsinglet Case_ , _Nucl. Phys. B_ 175 (1980) 27.
  * [40] R. K. Ellis and W. Vogelsang, _The Evolution of parton distributions beyond leading order: The Singlet case_ , hep-ph/9602356.
  * [41] W. Vogelsang, _The Spin dependent two loop splitting functions_ , _Nucl. Phys. B_ 475 (1996) 47 [hep-ph/9603366].
  * [42] W. Vogelsang, _Next-to-leading order evolution of transversity distributions and Soffer’s inequality_ , _Phys. Rev. D_ 57 (1998) 1886 [hep-ph/9706511].
  * [43] M. G. Echevarria, I. Scimemi and A. Vladimirov, _Unpolarized Transverse Momentum Dependent Parton Distribution and Fragmentation Functions at next-to-next-to-leading order_ , _JHEP_ 09 (2016) 004 [1604.07869].
  * [44] D. Gutierrez-Reyes, I. Scimemi and A. Vladimirov, _Transverse momentum dependent transversely polarized distributions at next-to-next-to-leading-order_ , _JHEP_ 07 (2018) 172 [1805.07243].
  * [45] J. Collins, _Foundations of perturbative QCD_ , vol. 32. Cambridge University Press, 11, 2013.
  * [46] M. G. Echevarria, I. Scimemi and A. Vladimirov, _Universal transverse momentum dependent soft function at NNLO_ , _Phys. Rev. D_ 93 (2016) 054004 [1511.05590].
  * [47] M. A. Ebert, I. W. Stewart and Y. Zhao, _Towards Quasi-Transverse Momentum Dependent PDFs Computable on the Lattice_ , _JHEP_ 09 (2019) 037 [1901.03685].
  * [48] M. Diehl, J. R. Gaunt and P. Plößl, _Two-loop splitting in double parton distributions: the colour non-singlet case_ , _JHEP_ 08 (2021) 040 [2105.08425].
  * [49] G. ’t Hooft and M. J. G. Veltman, _Regularization and Renormalization of Gauge Fields_ , _Nucl. Phys. B_ 44 (1972) 189.
  * [50] P. Breitenlohner and D. Maison, _Dimensional Renormalization and the Action Principle_ , _Commun. Math. Phys._ 52 (1977) 11.
  * [51] M. Diehl, P. Plößl and A. Schäfer, _Proof of sum rules for double parton distributions in QCD_ , _Eur. Phys. J. C_ 79 (2019) 253 [1811.00289].
  * [52] J. Blümlein and S. Kurth, _Harmonic sums and Mellin transforms up to two loop order_ , _Phys. Rev. D_ 60 (1999) 014018 [hep-ph/9810241].
  * [53] S. A. Larin, _The Renormalization of the axial anomaly in dimensional regularization_ , _Phys. Lett. B_ 303 (1993) 113 [hep-ph/9302240].
  * [54] A. Vladimirov, _Soft factors for double parton scattering at NNLO_ , _JHEP_ 12 (2016) 038 [1608.04920].
  * [55] G. S. Bali, _Casimir scaling of SU(3) static potentials_ , _Phys. Rev. D_ 62 (2000) 114503 [hep-lat/0006022].
  * [56] A. Vladimirov, V. Moos and I. Scimemi, _Transverse momentum dependent operator expansion at next-to-leading power_ , _JHEP_ 01 (2022) 110 [2109.09771].
  * [57] D. Binosi and L. Theussl, _JaxoDraw: A Graphical user interface for drawing Feynman diagrams_ , _Comput. Phys. Commun._ 161 (2004) 76 [hep-ph/0309015].
  * [58] D. Binosi, J. Collins, C. Kaufhold and L. Theussl, _JaxoDraw: A Graphical user interface for drawing Feynman diagrams. Version 2.0 release notes_ , _Comput. Phys. Commun._ 180 (2009) 1709 [0811.4113].
  * [59] J. A. M. Vermaseren, _New features of FORM_ , math-ph/0010025.
  * [60] M. Sjödahl, _ColorMath - A package for color summed calculations in SU(Nc)_ , _Eur. Phys. J. C_ 73 (2013) 2310 [1211.2099].


Holographic Anomalous Chiral Current Near a Boundary

Rong-Xin Miao 111Email<EMAIL_ADDRESS>Yu-Qian Zeng

School of Physics and Astronomy, Sun Yat-Sen University, 2 Daxue Road, Zhuhai
519082, China

###### Abstract

Due to the Weyl anomaly, an axial vector field produces novel anomalous chiral
currents in spacetime with boundaries. Remarkably, the chiral current is not
invariant under the gauge transformation of axial vector fields. As a result,
more potential terms appear, and the chiral current becomes larger than the
electric current near the boundary. This paper investigates the anomalous
chiral current in AdS/BCFT. We find that the minimal holographic model of the
axial vector field cannot produce the expected chiral current. To resolve this
problem, we propose adding a suitable boundary action. Furthermore, we notice
a similar situation for holographic condensation. Finally, we obtain the shape
dependence of holographic chiral current and verify that it agrees with the
field-theoretical result.

###### Contents

  1. 1 Introduction
  2. 2 Holographic condensation
  3. 3 Holographic chiral current
  4. 4 Shape dependence of holographic chiral current
  5. 5 Conclusions and Discussions
  6. A Chiral current from Weyl anomaly

##  1 Introduction

Anomaly-induced transports are novel phenomena with wide applications in
condensed matter, quantum field theory, and cosmology [1]. The famous examples
include the chiral magnetic effect (CME) [2, 3, 4, 5, 6] and chiral vortical
effect (CVE) [7, 8, 9, 10, 11, 12, 13], which originated from the chiral
anomaly. See also [14, 15, 16, 17, 42, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28]
for related works. Recently, it has been found that the Weyl anomaly [29]
leads to novel anomalous currents [30, 31], Fermi condensations [32, 33] and
chiral currents [34] in spacetime with boundaries. Remarkably, the Weyl-
anomaly-induced transports take universal forms near the boundary, which apply
to not only conformal field theory but also the general quantum field theory
because the Weyl anomaly is well-defined for general quantum field theory
[29].

Take free Dirac field as an example

$\displaystyle
S=\int_{M}\sqrt{-g}\bar{\psi}i\gamma^{\mu}\big{(}\nabla_{\mu}-iV_{\mu}-i\gamma_{5}A_{\mu}\big{)}\psi,$
(1)

where $V_{\mu}$ and $A_{\mu}$ are vectors and axial vectors, respectively. We
impose the general chiral bag boundary conditions [35, 36]

$\displaystyle(1+ie^{i\theta\gamma_{5}}\gamma^{n})\psi|_{\partial M}=0$ (2)

where $n$ denotes the normal direction and $\theta$ is a constant. At the
leading order near the boundary, various anomalous transports near the
boundary are given by [30, 31, 32, 33]

$\displaystyle{\text{current}}:\ \ \ \langle
J_{V}^{\mu}\rangle=\frac{1}{6\pi^{2}}\frac{n_{\nu}H^{\nu\mu}}{x}+O(\ln x),$
(3) $\displaystyle{\text{condensation}}:\
\langle\bar{\psi}\psi\rangle=\frac{\cos\theta}{4\pi^{2}}\frac{1}{x^{3}}+O(1/x^{2}),$
(4) $\displaystyle{\text{chiral current}}:\ \ \ \langle
J_{A}^{\mu}\rangle=\frac{-1}{6\pi^{2}}\frac{h^{\mu\nu}A_{\nu}}{x^{2}}+O(1/x),$
(5)

where $H=dV$ denotes the field strength of vectors, $x$ is the distance to the
boundary, $n_{\nu}$ is the inward-pointing normal vector and $h_{\mu\nu}$ is
the induced metric on the boundary. Note that we take signature $(-1,1,1,1)$
in this paper, which is different from [34]. Note also that the above results
apply to $x>\epsilon$, where $\epsilon$ is a cut-off. There are also boundary
contributions at $x=\epsilon$ to the current and chiral current, which make
the total transports finite [30].

This paper studies the anomalous chiral current in AdS/BCFT [38]. We find that
the minimal holographic model of axial vectors cannot reproduce the expected
chiral current (5). To resolve this problem, we propose adding a relevant
boundary term, which is similar to the case of holographic condensation. We
also investigate the shape dependence of holographic chiral current and verify
that it obeys the non-trivial constraint from the Weyl anomaly.

The paper is organized as follows. To warm up, we first discuss holographic
condensation in section 2. We find that an additional boundary action is
necessary in order to derive the expected condensation. In section 3, we study
a non-minimal holographic model of the axial vector field and derive the
desired anomalous chiral current. In section 4, we investigate the shape
dependence of holographic chiral current. Finally, we conclude with some open
questions in section 5.

##  2 Holographic condensation

To warm up, we first study holographic condensation in this section. Due to
the novel boundary effects, the vacuum expectation of a scalar operator is
non-zero [37]

$\displaystyle\langle O\rangle\sim\frac{1}{x^{\Delta}},$ (6)

where $\Delta$ is the conformal dimension, and $x$ is the distance to the
boundary. For $O=\bar{\psi}\psi$ and $\Delta=3$, (6) becomes the Fermi
condensation (4). It is found in [39] that the minimal holographic model
cannot recover the result (6). Instead, one has to add a boundary action on
the end-of-the-world brane $Q$,

$\displaystyle
I=\int_{N}d^{d+1}x\sqrt{|g|}\left(R+d(d-1)-\frac{1}{2}\left(\nabla^{\mu}\phi\nabla_{\mu}\phi+m^{2}\phi^{2}\right)\right)+2\int_{Q}dx^{d}\sqrt{|\gamma|}\left(K-T+\frac{\xi}{2}\phi\right),$
(7)

where $K$ is the extrinsic curvature, $T=(d-1)\tanh\rho$ is the brane tension
111Note that $\rho$ is a constant, which is equal to $\rho^{*}$ of [38].  ,
$\xi$ is a parameter that plays an essential role in deriving condensation
(6). Above we have set $16\pi G_{N}=1$ and AdS radius $l=1$. For simplicity,
following [38], we do not show the boundary terms on the AdS boundary, which
take the same forms as those in AdS/CFT. Following [38], we choose the Neumann
boundary condition (NBC) on $Q$

$\displaystyle K_{ij}-(K-T+\frac{\xi}{2}\phi)\gamma_{ij}=0,$ (8)
$\displaystyle n^{\mu}\nabla_{\mu}\phi+\xi=0,$ (9)

where $n^{\mu}$ is the inward-pointing normal vector on $Q$. See [40, 41] for
other choices of boundary conditions. For simplicity, we focus on the probe
limit with the following bulk metric and embedding function of brane $Q$

$\displaystyle{\text{bulk metric}}:\ \
ds^{2}=\frac{dz^{2}+dx^{2}+\eta_{ab}dy^{a}dy^{b}}{z^{2}},$ (10)
$\displaystyle{\text{Q}}:\ \ x=-\sinh(\rho)z,$ (11)

where $\eta_{ab}=\text{diag}(-1,1,...,1)$. Following [33], we take the
following ansatz of scalar field

$\displaystyle\phi=f(\frac{z}{x}).$ (12)

Substituting (12) into the equation of motion (EOM) of scalar and denoting
$s=z/x$, we obtain

$\displaystyle
s\left(s\left(s^{2}+1\right)f^{\prime\prime}(s)+\left(2s^{2}+1-d\right)f^{\prime}(s)\right)-m^{2}f(s)=0,$
(13)

The above equation can be solved as

$\displaystyle f(s)=$ $\displaystyle
c_{1}s^{\Delta}\,_{2}F_{1}\left(\frac{\Delta}{2},\frac{\Delta+1}{2};1-\frac{d}{2}+\Delta;-s^{2}\right)$
(14) $\displaystyle+$ $\displaystyle
c_{2}s^{d-\Delta}\,_{2}F_{1}\left(\frac{d-\Delta}{2},\frac{d-\Delta+1}{2};1+\frac{d}{2}-\Delta;-s^{2}\right),$

which yields the expected asymptotic solution near the AdS boundary

$\displaystyle\phi=z^{d-\Delta}\phi_{0}+z^{\Delta}\frac{1}{2\Delta-d}\langle
O\rangle,\quad z\to 0,$ (15)

where $\Delta=\frac{d}{2}+\sqrt{(\frac{d}{2})^{2}+m^{2}}$ is the conformal
dimension of the operator $O$ dual to $\phi$, and $\phi_{0}$ is the background
scalar coupled to CFTs on the AdS boundary. Following [33], we choose
$\phi_{0}=0$ on the AdS boundary, which gives $c_{2}=0$. Now imposing NBC (9)
on the brane, we fix the integral constant

$\displaystyle
c_{1}=\frac{\xi\tanh(\rho)(-\text{csch}(\rho))^{-\Delta}/\Delta}{\frac{(\Delta+1)\text{csch}^{2}(\rho)\,_{2}F_{1}\left(\frac{\Delta+2}{2},\frac{\Delta+3}{2};-\frac{d}{2}+\Delta+2;-\text{csch}^{2}(\rho)\right)}{-d+2\Delta+2}-\,_{2}F_{1}\left(\frac{\Delta}{2},\frac{\Delta+1}{2};-\frac{d}{2}+\Delta+1;-\text{csch}^{2}(\rho)\right)}.$
(16)

From (14-16), we finally derive the holographic condensation

$\displaystyle\langle
O\rangle=(2\Delta-d)\frac{c_{1}}{x^{\Delta}}\sim\frac{\xi}{x^{\Delta}},$ (17)

which agrees with field-theoretical result (6). Note that $\langle O\rangle$
vanishes in the minimal holographic model with $\xi=0$.

Let us make some comments. First, to derive the expected condensation (6), one
has to consider a non-minimal holographic model with an additional boundary
term on the brane. As we will discuss in the next section, the case of chiral
current is similar. Second, the results of this section are not new. The
special case with $d=4$ and $\Delta=3$ is already studied in [33]. The general
case is also studied in [39]. Here we apply a different method developed in
[42], which is simpler than the initial method of [39].

##  3 Holographic chiral current

In this section, we discuss the holographic chiral current in a flat half
space. For our purpose, we focus on the most interesting case $d=4$. Similar
to holographic condensation, we consider the non-minimal model of axial
vectors with a boundary action on $Q$

$\displaystyle
I=\int_{N}d^{5}x\sqrt{|g|}\left(-\frac{1}{4}\mathcal{F}_{\mu\nu}\mathcal{F}^{\mu\nu}+\frac{\kappa}{2}\epsilon^{\mu\nu\rho\sigma\alpha}\mathcal{A}_{\mu}\mathcal{F}_{\nu\rho}\mathcal{F}_{\sigma\alpha}\right)+\int_{Q}dx^{4}\sqrt{|\gamma|}\left(\frac{\lambda}{2}\gamma^{\mu\nu}\mathcal{A}_{\mu}\mathcal{A}_{\nu}\right),$
(18)

where $\mathcal{F}=d\mathcal{A}$, $\lambda$ is a constant, and
$\gamma_{\mu\nu}$ is the induced metric on the brane. Note that the above
action is not invariant under the gauge transformation of axial vectors
$\delta\mathcal{A}_{\mu}=\partial_{\mu}\alpha$. This is necessary to derive
the non-gauge-invariant chiral current (5). From (18), we derive the EOM

$\displaystyle\nabla_{\mu}\mathcal{F}^{\mu\nu}+\frac{3\kappa}{2}\epsilon^{\nu\rho\sigma\alpha\beta}\mathcal{F}_{\rho\sigma}\mathcal{F}_{\alpha\beta}=0$
(19)

and NBC on the brane $Q$

$\displaystyle
n_{\mu}(\mathcal{F}^{\mu\nu}-2\kappa\epsilon^{\mu\nu\rho\alpha\beta}\mathcal{A}_{\rho}\mathcal{F}_{\alpha\beta})+\lambda\mathcal{A}_{\mu}\gamma^{\mu\nu}=0.$
(20)

Similar to the above section, we focus on the probe limit (10,11). We take the
following ansatz of bulk axial vectors 222Note that one cannot modify the
ansatz (21) to give the correct chiral current without the boundary term in
action (18). See the conclusion section for reasons.

$\displaystyle\mathcal{A}_{z}=\mathcal{A}_{x}=0,\
\mathcal{A}_{a}=A_{a}f_{0}(\frac{z}{x}),$ (21)

where $a$ denotes the direction parallel to the boundary $x=0$, $A_{a}$ is a
constant vector and we choose the Dirichlet boundary condition (DBC) on the
AdS boundary

$\displaystyle f_{0}(0)=1,$ (22)

so that $A_{a}$ of (21) is the axial vector field coupled to CFTs on the AdS
boundary. Substituting (21) into EOM (19), we obtain

$\displaystyle
s\left(s^{2}+1\right)f_{0}^{\prime\prime}(s)+\left(2s^{2}-1\right)f_{0}^{\prime}(s)=0,$
(23)

which can be solved as

$\displaystyle f_{0}(s)=1+b_{1}-\frac{b_{1}}{\sqrt{s^{2}+1}},$ (24)

where we have used DBC (22). Imposing NBC (20) on the brane, we derive the
integral constant

$\displaystyle
b_{1}=\frac{\lambda\cosh(\rho)\coth(\rho)}{\text{csch}(\rho)-\lambda\cosh(\rho)(\coth(\rho)+1)}.$
(25)

Substituting (21,24) into the holographic formula of chiral current [43]

$\displaystyle\sqrt{|h|}J_{A}^{\nu}=\lim_{z\to
0}\sqrt{|g|}(\mathcal{F}^{z\nu}-2\kappa\epsilon^{z\nu\rho\alpha\beta}\mathcal{A}_{\rho}\mathcal{F}_{\alpha\beta}),$
(26)

we finally obtain the holographic chiral current

$\displaystyle J_{A\ a}=b_{1}\frac{A_{a}}{x^{2}},$ (27)

which takes the expected form (5). Note that the second term on the right-hand
side of (26) is of order $O(A^{2})$ and vanishes strictly for the solution
(21,24). Note also that (27) for holographic CFTs needs not to be equal to (5)
for free Dirac fields. Above $g_{\mu\nu}$ is given by the metric (10) with
$d=4$. Thus we have $\sqrt{|g|}=1/z^{5}$. $h_{ij}$ denotes the metric of BCFT.
For our present case, BCFT lives in a flat half space with $\sqrt{|h|}=1$. Now
we finish the holographic derivation of the chiral current in a flat half
space.

##  4 Shape dependence of holographic chiral current

In this section, we investigate the shape dependence of holographic chiral
current. The shape of the boundary is described by the extrinsic curvature
$k_{ab}$, which affects the chiral current at sub-leading order [34]

$\displaystyle J_{A}\sim\frac{A}{x^{2}}+\frac{kA}{x}+...$ (28)

For simplicity, we focus on the results in the linear order of the extrinsic
curvature $k$ and the background axial vector field $A$. Besides, we consider
constant axial vector fields $A=\lim_{z\to 0}\mathcal{A}$ and extrinsic
curvatures $k$ on the AdS boundary.

Note that the back-reaction of axial vector fields to the geometry is of order
$O(A)^{2}$. Therefore, at the linear order of $O(A)$, we can ignore the back-
reaction safely. For a non-flat boundary, the bulk metric and the embedding
function of $Q$ are given by [42]

$\displaystyle
ds^{2}=\frac{1}{z^{2}}\Big{[}dz^{2}+dx^{2}+\big{(}\delta_{ab}-2x\epsilon\bar{k}_{ab}f(\frac{z}{x})-2x\epsilon\frac{k}{3}\delta_{ab}\big{)}dy^{a}dy^{b}\Big{]}+O(\epsilon^{2}),$
(29)

and

$\displaystyle
x=-\sinh(\rho)z+\epsilon\frac{k\cosh^{2}\rho}{6}z^{2}+O(\epsilon^{2}),$ (30)

where $k_{ab}=\text{diag}(k_{1},k_{2},k_{3})$ is the extrinsic curvature, $k$
is the trace and $\bar{k}_{ab}$ is the traceless part of the extrinsic
curvature, $\epsilon$ keeps track of the order of $k$ and should be set to 1
in the end, and $f(s)$ is given by

$\displaystyle
f(s)=1+2\alpha_{1}-\frac{\alpha_{1}\left(s^{2}+2\right)}{\sqrt{s^{2}+1}},$
(31) $\displaystyle\alpha_{1}=\frac{-1}{2(1+\tanh\rho)}.$ (32)

We take the following ansatz of bulk axial vectors

$\displaystyle\mathcal{A}_{z}=\mathcal{A}_{x}=0,\
\mathcal{A}_{a}=\epsilon_{1}A_{a}\big{(}f_{0}(\frac{z}{x})+\epsilon\
xf_{1a}(\frac{z}{x})\big{)},$ (33)

where $\epsilon_{1}$ keeps track of the order of $A$, and we choose the DBC

$\displaystyle f_{0}(0)=1,\ f_{1a}(0)=0$ (34)

so that $A_{a}=\lim_{z\to 0}\mathcal{A}_{a}$ is a constant axial vector on the
AdS boundary. Following the approach of section 3, we solve EOM (19) together
with BCs (20,34) and obtain at order $O(\epsilon\epsilon_{1})$

$\displaystyle f_{1a}(s)$ $\displaystyle=$
$\displaystyle\bar{k}_{aa}\Big{[}b_{1}\left(\frac{2}{3}\alpha_{1}\left(\frac{3}{\sqrt{s^{2}+1}}-\frac{1}{s^{2}+1}-2\right)+\frac{1}{\sqrt{s^{2}+1}}-1\right)+d_{1}\left(\sqrt{s^{2}+1}-1\right)\Big{]}$
(35) $\displaystyle+$ $\displaystyle
k\Big{[}\frac{1}{6}b_{1}\left(1-\frac{1}{\sqrt{s^{2}+1}}\right)+d_{2}\left(\sqrt{s^{2}+1}-1\right)\Big{]},$

where the repeat index of $\bar{k}_{aa}$ does not sum, $b_{1}$, $\alpha_{1}$
are given by (25,32), and $d_{1},d_{2}$ are given by

$\displaystyle
d_{1}=\frac{\lambda\cosh(\rho)((\lambda-11)\sinh(\rho)+(\lambda+1)\sinh(3\rho)-(2\lambda+3)\cosh(\rho)+(2\lambda-1)\cosh(3\rho))}{3\left(\lambda
e^{2\rho}+\lambda-2\right)^{2}},$ (36)

and

$\displaystyle d_{2}=\frac{\lambda\cosh^{2}(\rho)}{-3\lambda
e^{2\rho}-3\lambda+6}.$ (37)

Substituting the solution (33) into the holographic formula (26) with
$\sqrt{|h|}=1-xk+O(x^{2})$, we obtain the shape dependence of holographic
chiral current

$\displaystyle J_{A\ a}=b_{1}\frac{A_{a}}{x^{2}}+\frac{b_{2}\bar{k}_{a}^{\
b}A_{b}+b_{3}kA_{a}}{x}+O(x^{0},\ln x),$ (38)

where

$\displaystyle
b_{2}=\frac{6d_{1}-2\left(2\alpha_{1}+3\right)b_{1}}{6}=\frac{\lambda\cosh(\rho)((2\lambda-3)\cosh(\rho)+3\sinh(\rho))}{3((\lambda-1)\cosh(\rho)+\sinh(\rho))^{2}},$
(39)

and

$\displaystyle
b_{3}=\frac{1}{6}\left(b_{1}+6d_{2}\right)=-\frac{2\lambda\cosh^{2}(\rho)}{3\left(\lambda
e^{2\rho}+\lambda-2\right)}.$ (40)

Now we finish the derivation of the shape dependence of holographic chiral
current. Comparing (38) with the field-theoretical result (46), we get a
constraint

$\displaystyle b_{3}=\frac{1}{3}b_{1}.$ (41)

From (25) and (40), we verify that (41) is indeed satisfied. This is a
nontrivial check of our results.

##  5 Conclusions and Discussions

This paper investigates the holographic anomalous chiral current near a
boundary. We find that one has to consider a non-minimal holographic model of
axial vectors in order to produce the non-gauge invariant chiral current
$J_{A}\sim A/x^{2}$. The reasons are as follows. The Chern-Simons term in the
minimal model is of order $O(\mathcal{A}^{3})$, which is irrelevant to the
chiral current linear in $O(A)$. Ignoring the Chern-Simons term at leading
order, the minimal action $\mathcal{F}^{2}_{\mathcal{A}}$ becomes gauge
invariant and cannot give a non-gauge invariant chiral current. To recover the
expected result $J_{A}\sim A/x^{2}$, one must add an action of order
$O(\mathcal{A}^{2})$ so that the EOM or BC is of order $O(\mathcal{A})$. One
cannot add a bulk action $\mathcal{A}^{2}$ (affect EOM), since it would make
the axial vector $\mathcal{A}$ massive and change the conformal dimension of
dual chiral current $J_{A}$. The only choice is to add a boundary action
$\int_{Q}\mathcal{A}^{2}$ (affect BC) on the brane. In this way, we derive the
expected chiral current $J_{A}\sim A/x^{2}$. We notice that one also considers
a non-minimal holographic model of scalars in order to derive the correct
condensation. Finally, we work out the shape dependence of holographic chiral
current and verify that it agrees with the results of field theories. It is
interesting to generalize the discussions of this paper to Chern-Simons
gravity and explore the corresponding one-point function of stress tensors. We
hope we can address this problem in the future.

## Acknowledgements

We thank C. S. Chu for helpful discussions and comments. R. X. Miao
acknowledges the supports from National Natural Science Foundation of China
(No. 11905297) and Guangdong Basic and Applied Basic Research Foundation
(No.2020A1515010900).

##  Appendix A Chiral current from Weyl anomaly

In this appendix, we focus on the conformal field theory in four dimensions
instead of the holographic theory in five dimensions. In general, there are
boundary contributions to the Weyl anomaly. See [44, 45] for example.
According to [34], the Weyl anomaly induced by a background axial vector takes
the following form

$\displaystyle\mathcal{A}=-\int_{M}dx^{4}\sqrt{-g}a_{1}F_{\mu\nu}F^{\mu\nu}-\int_{\partial
M}dx^{3}\sqrt{-h}[a_{2}(B_{1}-B_{2})+a_{3}\bar{k}_{\mu\nu}A^{\mu}A^{\nu}],$
(42)

where $a_{i}$ are central charges and

$\displaystyle
B_{1}=\frac{2}{3}k(n^{\mu}n^{\nu}-h^{\mu\nu})A_{\mu}A_{\nu}+A_{n}\nabla_{\mu}A^{\mu}+2A_{\mu}h^{\mu\nu}\nabla_{n}A_{\nu},$
(43) $\displaystyle
B_{2}=n^{\mu}A^{\nu}\nabla_{\nu}A_{\mu}-\frac{1}{3}kA_{\mu}A^{\mu}.$ (44)

Note that the notation of this paper is different from that of [34]. In this
paper, the metric signature is $(-1,1,1,1)$, $n_{\mu}$ is inward pointing,
$h_{\mu\nu}$ is the induced metric on the boundary,
$k_{\mu\nu}=-h^{\alpha}_{\mu}h^{\beta}_{\nu}\nabla_{\alpha}n_{\beta}$ is the
extrinsic curvature and $\bar{k}_{\mu\nu}$ is its traceless part. Although
$B_{1}$ and $B_{2}$ are both Weyl invariant, only the combination
$(B_{1}-B_{2})$ can appear in Weyl anomaly. Otherwise, the chiral current
derived from Weyl anomaly would have the normal component $J^{\mu}\sim
n^{\mu}A_{n}/x^{2}$, which means that it cannot satisfy the conservation law
$\nabla_{\mu}J^{\mu}\sim A_{n}/x^{3}\neq O(1)$. According to [30, 34], we have
the “integrability” relation

$\displaystyle(\delta\mathcal{A})_{\partial
M_{\epsilon}}=\left(\int_{M_{\epsilon}}dx^{4}\sqrt{-g}\ J_{A}^{\mu}\delta
A_{\mu}\right)_{\log\frac{1}{\epsilon}},$ (45)

where $\epsilon$ is the cutoff of $x$, i.e., the distance to the boundary,
$M_{\epsilon}$ is defined by the region $x\geq\epsilon$,
$()_{\log\frac{1}{\epsilon}}$ means the coefficient of
$\log\frac{1}{\epsilon}$, which comes from the $\frac{1}{x}$ term in the
integral $\sqrt{-g}\ J_{A}^{\mu}\delta A_{\mu}$ since we have
$\int_{\epsilon}^{\infty}dx\frac{1}{x}\sim\log\frac{1}{\epsilon}$. Please see
[30] for the proof of the “integrability” relation for the current. The
generalization to the chiral current (45) is straightforward. By applying
(45), one derives the chiral current [34]

$\displaystyle
J^{a}_{A}=\frac{-2a_{2}A^{a}}{x^{2}}+\frac{2(a_{2}-a_{3})\bar{k}^{ab}A_{b}-\frac{2}{3}a_{2}kA^{a}}{x}+\frac{4a_{1}n_{\mu}F^{\mu
a}+2a_{2}D^{a}(n_{\mu}A^{\mu})}{x}+...,$ (46) $\displaystyle
J^{n}_{A}=\frac{-2a_{2}D_{a}A^{a}}{x}+...,\ \quad x\sim 0,$ (47)

where $n$ and $a$ denote respectively the normal and tangential directions,
$D_{a}$ is the covariant derivative on the boundary. Note that the above
$A^{a}$ depends on $x$ generally. To see this, we take
$ds^{2}=dx^{2}+\Big{(}h_{ab}-2xk_{ab}+O(x^{2})\Big{)}dy^{a}dy^{b}$ and
$A_{\mu}=A_{0\ \mu}+xA_{1\ \mu}+O(x^{2})$ in Gauss normal coordinate. Then we
have $A^{a}=A_{b}(h^{ab}+2xk^{ab})+O(x^{2})=A^{\ a}_{0}+xA^{\
a}_{1}+2xk^{ab}A_{0\ b}+O(x^{2})$. To compare with the holographic
calculations with constant axial vectors and extrinsic curvatures, we can set
$A_{1\ \mu}=n_{\mu}F^{\mu a}=D^{a}(n_{\mu}A^{\mu})=D_{a}A^{a}=0$ in (46,47).

## References

  * [1] For a review, see for example, D. E. Kharzeev, “The Chiral Magnetic Effect and Anomaly-Induced Transport,” Prog. Part. Nucl. Phys. 75 (2014) 133 [arXiv:1312.3348 [hep-ph]]; K. Landsteiner, “Notes on Anomaly Induced Transport,” Acta Phys. Polon. B 47 (2016) 2617 [arXiv:1610.04413 [hep-th]].
  * [2] A. Vilenkin, “Parity nonconservation and neutrino transport in magnetic fields,” Astrophys. J. 451 (1995) 700.
  * [3] A. Vilenkin, “Equilibrium Parity Violating Current In A Magnetic Field,” Phys. Rev. D 22 (1980) 3080.
  * [4] M. Giovannini and M. E. Shaposhnikov, “Primordial hypermagnetic fields and triangle anomaly,” Phys. Rev. D 57 (1998) 2186 [hep-ph/9710234].
  * [5] A.Y. Alekseev, V. V. Cheianov, and J. Froehlich, Phys. Rev. Lett.81 (1998) 3503 [cond-mat/9803346].
  * [6] K. Fukushima, “Views of the Chiral Magnetic Effect,” Lect. Notes Phys. 871 (2013) 241 [arXiv:1209.5064 [hep-ph]].
  * [7] D. Kharzeev and A. Zhitnitsky, “Charge separation induced by P-odd bubbles in QCD matter,” Nucl. Phys. A 797, 67 (2007) [arXiv:0706.1026 [hep-ph]].
  * [8] J. Erdmenger, M. Haack, M. Kaminski and A. Yarom, “Fluid dynamics of R-charged black holes,” JHEP 0901 (2009) 055 [arXiv:0809.2488 [hep-th]].
  * [9] N. Banerjee, J. Bhattacharya, S. Bhattacharyya, S. Dutta, R. Loganayagam and P. Surowka, “Hydrodynamics from charged black branes,” JHEP 1101 (2011) 094 [arXiv:0809.2596 [hep-th]].
  * [10] D. T. Son and P. Surowka, “Hydrodynamics with Triangle Anomalies,” Phys. Rev. Lett. 103 (2009) 191601 [arXiv:0906.5044 [hep-th]].
  * [11] K. Landsteiner, E. Megias and F. Pena-Benitez, “Gravitational Anomaly and Transport,” Phys. Rev. Lett. 107 (2011) 021601 [arXiv:1103.5006 [hep-ph]].
  * [12] S. Golkar and D. T. Son, “(Non)-renormalization of the chiral vortical effect coefficient,” JHEP 1502, 169 (2015) [arXiv:1207.5806 [hep-th]].
  * [13] K. Jensen, R. Loganayagam and A. Yarom, “Thermodynamics, gravitational anomalies and cones,” JHEP 1302, 088 (2013) [arXiv:1207.5824 [hep-th]].
  * [14] M. N. Chernodub, Phys. Rev. Lett. 117, no. 14, 141601 (2016) [arXiv:1603.07993 [hep-th]].
  * [15] M. N. Chernodub, A. Cortijo and M. A. H. Vozmediano, Phys. Rev. Lett. 120, no. 20, 206601 (2018) [arXiv:1712.05386 [cond-mat.str-el]].
  * [16] C. Chu and R. Miao, JHEP 07, 151 (2019) [arXiv:1812.10273 [hep-th]].
  * [17] C. Chu, Fortsch. Phys. 67, no.8-9, 1910005 (2019) [arXiv:1903.02817 [hep-th]].
  * [18] R. Miao and C. Chu, JHEP 03, 046 (2018) [arXiv:1706.09652 [hep-th]].
  * [19] R. Miao, JHEP 07, 098 (2019) [arXiv:1808.05783 [hep-th]].
  * [20] M. N. Chernodub, V. A. Goy and A. V. Molochkov, Phys. Lett. B 789, 556 (2019) [arXiv:1811.05411 [hep-th]].
  * [21] M. Chernodub and M. A. Vozmediano, Phys. Rev. Research. 1, 032002 (2019) [arXiv:1902.02694 [cond-mat.str-el]].
  * [22] V. E. Ambrus and M. Chernodub, [arXiv:1912.11034 [hep-th]].
  * [23] J. Zheng, D. Li, Y. Zeng and R. Miao, Phys. Lett. B 797, 134844 (2019) [arXiv:1904.07017 [hep-th]].
  * [24] P. J. Hu, Q. L. Hu and R. X. Miao, Phys. Rev. D 101, no.12, 125010 (2020) [arXiv:2004.06924 [hep-th]].
  * [25] M. Kawaguchi, S. Matsuzaki and X. G. Huang, JHEP 10, 017 (2020) [arXiv:2007.00915 [hep-ph]].
  * [26] M. Kurkov and D. Vassilevich, Phys. Rev. Lett. 124, no.17, 176802 (2020) [arXiv:2002.06721 [hep-th]].
  * [27] M. Kurkov and D. Vassilevich, JHEP 03, 072 (2018) [arXiv:1801.02049 [hep-th]].
  * [28] I. Fialkovsky, M. Kurkov and D. Vassilevich, Phys. Rev. D 100, no.4, 045026 (2019) [arXiv:1906.06704 [hep-th]].
  * [29] M. J. Duff, Class. Quant. Grav. 11, 1387 (1994)
  * [30] C. S. Chu and R. X. Miao, Phys. Rev. Lett. 121, no.25, 251602 (2018) [arXiv:1803.03068 [hep-th]].
  * [31] C. S. Chu and R. X. Miao, JHEP 07, 005 (2018) [arXiv:1804.01648 [hep-th]].
  * [32] C. S. Chu and R. X. Miao, Phys. Rev. D 102, no.4, 046011 (2020) [arXiv:2004.05780 [hep-th]].
  * [33] C. S. Chu and R. X. Miao, JHEP 08, 134 (2020) [arXiv:2005.12975 [hep-th]].
  * [34] C. S. Chu and R. X. Miao, [arXiv:2210.01382 [cond-mat.mes-hall]].
  * [35] A. Chodos, R. L. Jaffe, K. Johnson, C. B. Thorn and V. F. Weisskopf, Phys. Rev. D 9, 3471 (1974).
  * [36] A. Chodos, R. L. Jaffe, K. Johnson and C. B. Thorn, Phys. Rev. D 10, 2599 (1974).
  * [37] M. Billo, V. Goncalves, E. Lauria and M. Meineri, JHEP 04, 091 (2016) [arXiv:1601.02883 [hep-th]].
  * [38] T. Takayanagi, Phys. Rev. Lett. 107 (2011) 101602 [arXiv:1105.5165 [hep-th]].
  * [39] M. Fujita, T. Takayanagi and E. Tonni, JHEP 11, 043 (2011) [arXiv:1108.5152 [hep-th]].
  * [40] R. X. Miao, JHEP 02, 025 (2019) [arXiv:1806.10777 [hep-th]].
  * [41] C. S. Chu and R. X. Miao, JHEP 01, 084 (2022) [arXiv:2110.03159 [hep-th]].
  * [42] R. X. Miao and C. S. Chu, JHEP 03, 046 (2018) [arXiv:1706.09652 [hep-th]].
  * [43] A. Gynther, K. Landsteiner, F. Pena-Benitez and A. Rebhan, JHEP 02, 110 (2011) [arXiv:1005.2587 [hep-th]].
  * [44] C. P. Herzog, K. W. Huang and K. Jensen, JHEP 1601, 162 (2016) [arXiv:1510.00021 [hep-th]].
  * [45] D. Fursaev, JHEP 1512, 112 (2015) [arXiv:1510.01427 [hep-th]].


# SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations
from SML Programs with Contracts

Laila El-Beheiry Giselle Reis Ammar Karkour Carnegie Mellon University, Qatar
<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Formally reasoning about functional programs is supposed to be straightforward
and elegant, however, it is not typically done as a matter of course.
Reasoning in a proof assistant requires “reimplementing” the code in those
tools, which is far from trivial. SMLtoCoq provides an automatic translation
of SML programs and function contracts into Coq. Programs are translated into
Coq specifications, and function contracts into theorems, which can then be
formally proved. Using the Equations plugin and other well established Coq
libraries, SMLtoCoq is able to translate SML programs without side-effects
containing partial functions, structures, functors, records, among others.
Additionally, we provide a Coq version of many parts of SML’s basis library,
so that calls to these libraries are kept almost _as is_.

##  1 Introduction

Programming language implementations are built for programming, so the aim is
to provide useful libraries and constructs to make writing _code_ as easy as
possible. Proof assistants, on the other hand, are built for reasoning and as
such the aim is to make writing _proofs_ as easy as possible. As much as
functional programs look similar to (relational or functional) specifications,
if one wants to prove properties about an implemented program, it is necessary
to “reimplement” it in the language of a proof assistant. This requires
familiarity with both the programming language and the proof assistant, since
not all programs are supported by reasoning tools (e.g. non-terminating
programs are typically forbidden), and not all libraries are available in both
tools.

In this work we present SMLtoCoq: a tool that _automatically translates SML
code into Coq specifications_. Moreover, we extend SML with _function
contracts which are directly translated into Coq theorems_. By using this
tool, programs can be written using all conveniences of a programming
language, and their contracts (functions’ pre and post conditions) can be
proved using the full power of a proof assistant. Our target audience are
programmers fluent in functional programming, but with little expertise in
proof assistants. By having programs automatically translated into Coq code
that looks as similar as possible to SML, programmers can learn quickly how
program specifications look like, thus lowering the entry barrier for using
the proof assistant.

Even though both tools use a functional language, representing SML programs in
Coq is complicated due to their various differences. The first immediate
challenge is that SML programs may be partial and have side-effects, while Coq
programs/specifications need to be pure and total. Another issue is that Coq
requires recursive definitions to be structurally decreasing so that
termination is guaranteed. SML programs can certainly diverge, and even if
they terminate, it might be because of a more complicated argument than a
straightforward structural induction. Coq does have extensions – such as the
Program command – that are used to define non-structurally-decreasing,
terminating recursive functions. However, a proof of termination must be
provided. On top of these more fundamental problems, we have encountered many
small mismatches between the two languages, such as how records are
represented, and what type-checking can infer.

By using a number of Coq features and information available in SML’s abstract
syntax tree (AST), SMLtoCoq is able to translate an extensive fragment of
_pure_ SML (i.e. without side effects), including partial functions, records,
and functors, among others. The resulting Coq specification looks very similar
to the original code, so someone proving properties can easily map parts of
specifications back to their program counterpart. Using the Equations library,
we translate partial, mutually recursive, and recursive functions out of the
box. Non-terminating functions are not accepted by Coq, but their translations
type check.

Our contributions are:

  * •

We extend HaMLet’s implementation of SML to parse and type-check function
contracts, written as function annotations. These are included in the SML’s
AST and translated into theorems.

  * •

We design and implement a tool, SMLtoCoq, that is able to translate pure SML
programs and contracts into Coq specifications and theorems completely
automatically. Moreover, the translated code looks very similar to the
original code.

  * •

We implement in Coq the SML libraries111Some of these libraries are very
pervasive and we needed their implementation to test the translation. This is
why they were not translated using SMLtoCoq. See Section 2.3.: INTEGER, REAL,
STRING, CHAR, Bool, Option, List, ListPair, and IEEEReal.

  * •

We provide many examples of translated code, including a case study where we
translate non-trivial SML code and prove properties on the Coq output. This
aligns with the intended workflow for the tool: translate SML code, then prove
properties in Coq.

SMLtoCoq can be found at: https://github.com/meta-logic/sml-to-coq/

##  2 Infrastructure

In its core, SMLtoCoq implements a translation of SML’s abstract syntax tree
(AST) into Gallina’s (Coq’s specification language) AST – which is
subsequently used to generate Gallina code. SML was chosen for being a
language with an incredibly formal and precise definition, which helped in
understanding precisely what fragments of the language were covered by our
translation. Coq was chosen for being an established and powerful proof
assistant, with many libraries and plugins available. In particular, it
provides the Equations library which was crucial for efficiently automating
the translation and generating correct code that looks close to SML.

SML’s AST is obtained from HaMLet222https://people.mpi-
sws.org/~rossberg/hamlet/. SML’s implementation in HaMLet can be separated
into three phases: _parsing_ , _elaboration_ , and _evaluation_. If a
program’s syntax is correct, _parsing_ will succeed returning an AST with
minimal annotation at each node, containing only their position in the source
code. Other well-formedness conditions (e.g. non-exhaustive or redundant
matches) and type-checking (i.e. static semantics) are computed during
_elaboration_ , which populates the annotations in the AST with more
information. _Evaluation_ will simply evaluate the program (i.e. dynamic
semantics).

We use the AST after the elaboration phase, when annotations contain useful
information such as inferred types and exhaustiveness of matches. Such
information is crucial for the generated Coq code. We call evaluation to make
sure the program executes correctly and terminates (i.e. no exceptions raised
or infinite loops entered) before starting the translation, but the evaluation
result is not used. SMLtoCoq is implemented in SML.

###  2.1 HaMLet

HaMLet is an SML implementation whose goal is to be an accurate implementation
of the language definition [7] and a platform for experimentation. We chose
this implementation for three main reasons:

  1. 1.

It is faithful to SML’s definition, and all deviations and design choices are
thoroughly documented.

  2. 2.

The resulting objects from each compilation step are easily accessible.
Particularly, the AST after the elaboration phase could be obtained with a
couple of function calls.

  3. 3.

Due to the detailed documentation, HaMLet could be easily modified as per the
translation needs.

HaMLet was extended with function contracts, written as code annotations in
the following syntax:

⬇

REQUIRES: exp1;

ENSURES: exp2; !!)

This contract must be placed immediately before f’s declaration. The first
line includes the function name f followed by the variable bindings
representing its input. These can be curried, uncurried, typed, or untyped,
following the syntax of function parameters in SML. This is followed by
output, which is one named variable, typed or not, representing the function’s
output. The variable names in input and output are in the scope of the
contract only, and should not be confused with variables inside the function.
REQUIRES and ENSURES are new keywords used for indicating the pre and post
condition of the function, respectively. They are followed by SML boolean
expressions exp1 and exp2. The type of these expressions is enforced by the
type checker. The variables used in input and output can be used in exp1 and
exp2. Variables in the function declaration are not available in the contract,
but exp1 and exp2 can use functions or variables defined previously in the
code.

In addition to changing HaMLet’s lexer and parser, SML’s AST was modified to
account for functions with contracts. The node representing function
declaration was augmented to hold the variable bindings and expressions from
contracts. If the function has no contracts, these fields are empty.

Besides the implementation of function contracts, HaMLet needed to be modified
so that the translation would be as faithful as possible. During parsing,
constructs called _derived forms_ are transformed into semantically equivalent
code using other constructs. This makes the core language smaller. For
example, if-then-else expressions are transformed into case expressions
(which, in turn, are transformed into anonymous functions). As a result, the
AST computed after parsing would not have nodes for if-then-else, and its
translation would result in a different (although semantically equivalent) Coq
specification. We have changed HaMLet to skip the transformation of derived
forms, and added constructors to the AST to account for them. The constructors
added were:

  * •

Expressions

    * –

() and (e_1, ..., e_n)

    * –

[e_1, ..., e_n]

    * –

case e of m

    * –

if e_1 then e_2 else e_3

    * –

e_1 andalso e_2 and e_1 orelse e_2

    * –

e_1 op e_2 (infix expressions)

  * •

Patterns: (), (p_1, ..., p_n), [p_1, ..., p_n], and p_1 op p_2 (infix
patterns)

  * •

Tuple types: t_1 * ... * t_n

  * •

Function declarations (originally transformed into val rec): fun id pats = e

  * •

Functor instantiation with inline specification (e.g. FuncID (structure
<strdesc>))

  * •

Type definitions in signatures (e.g. type t = s, which was expanded to an
inline signature)

SML’s AST is annotated during elaboration phase. The annotation of the new
constructs can happen in one of two ways: (1) its equivalent form is
constructed, elaborated, and we use the resulting annotation interpreted in
the context of the derived form; or (2) a new elaboration case is implemented
for the construct. We have used a combination of both approaches which
incurred as few changes as possible in the elaboration phase. The annotations
produced by both approaches are equivalent since they are added during the
elaboration phase which only considers the static semantics up to which the
derived form and its equivalent form are equivalent.

###  2.2 Coq

Coq’s core language for writing specifications is called Gallina. To be able
to generate Gallina’s AST, we have implemented it as a datatype in our system.
The implementation follows closely the grammar of Gallina’s
specification333https://coq.inria.fr/distrib/current/refman/language/core/index.html,
with a few small changes described in what follows.

Extra term and pattern constructors were added for string, real, char, tuple,
list, unit, and infix. SML expressions of those types are directly translated
to Gallina using these constructors, and they can be directly mapped to Coq
code either using common libraries or notations (e.g. Datatypes, List), or Coq
libraries that we have implemented to match SML libraries (e.g. string, real,
char). New term constructors for product types, and boolean conjunction and
disjunction, were implemented for the same reasons as above. To be able to
generate theorems, Gallina’s AST includes the Prop operators for conjunction,
disjunction, equality, and quantification. Finally, match terms need to have a
field indicating exhaustiveness.

Some syntactical elements of Gallina were left out since there is no corresponding SML code which generates them. For example, type coercion (:>) and “or” patterns (p_1 | p_2 $\Rightarrow\;$ t).

##### Equations

Equations [9] is a Coq plugin which allows a richer form of pattern-matching
and arbitrarily complex recursion schemes in the setting of dependent type
theory. Using this plugin, SMLtoCoq can generate concise and elegant code that
is visually similar to SML. The output is considerably improved when compared
to one generated in pure Gallina, and the derived proof principles can be used
to reason about the high-level code. Among the main advantages of using
Equations, is the ability to define partial functions using dependent types.
Domain restrictions identified on the original SML function can be translated
to a dependent type, which is added as one of the function’s arguments. The
resulting code has minimal overhead compared to its SML counterpart, not
needing extra default values or ad-hoc constructs to handle unmatched cases.
In addition to that, Equations provides a simple interface to handle non-
trivial recursion where proofs of termination must be provided by the user.

###  2.3 Libraries

SML’s basis library is included in most of its implementations and contains
some of the more popular datatypes and functions. Since most SML programs will
make use of some part of the basis library, we have implemented Coq
equivalents to: INTEGER, REAL, CHAR, Bool, STRING (and partially StringCvt),
Option, List, ListPair, and IEEEReal. They have the same interface as their
SML counterpart, so function calls to these libraries can be translated almost
“as is” to Coq. Most of the implementations build on existing Coq libraries,
such as List, ZArith, Ascii, Bool, Floats, String etc.

Several of SML’s basis library functions raise exceptions for a given set of
inputs. However, Gallina is pure and does not have side effects. In
particular, it does not support exceptions. In order to handle these cases, we
return an Axiom instead of raising an exception. For example, the function
List.hd in SML’s basis library raises the exception Empty if an empty list is
passed to it. The equivalent implementation of List.hd in our libraries return
the axiom EmptyException, defined as:

Note that this means it is not possible to _catch_ the exception, and renders
Coq inconsistent. We are currently investigating possible solutions for
exceptions, and side-effects in general (see Section 5).

A natural question to ask is why we have not used SMLtoCoq itself to translate
SML’s libraries. The reason is purely of a practical matter: function
translation was being developed at the same time libraries were being
implemented in Coq, and one development informed the other. Moreover, a lot of
SML code relies on these libraries, so we needed equivalent ones in Coq to
test our translation.

##  3 Translation

The translation from an SML’s AST $\mathcal{S}$ into a Gallina’s AST
$\mathcal{G}$ is defined inductively on $\mathcal{S}$. Depending on the type
of construct being translated, we rely on (local or global) auxiliary
contexts. We describe in this section the relevant parts of the translation,
including examples for each of them. The code in all figures in this section
is exactly the one used and generated by SMLtoCoq, except for some line breaks
and spaces removed to fit the pages. All the Coq code was tested with the
following header, which imports the libraries discussed in Section 2.3,
Equations, and sets generalization of variables by default.

⬇

Require Import realSml. Require Import stringSml.

Require Import charSml. Require Import boolSml.

Require Import optionSml. Require Import listPairSml.

Require Import notationsSml.

From Equations Require Import Equations.

Generalizable All Variables.

More involved examples can be found in the examples folder in the
repository444https://github.com/meta-logic/sml-to-coq/tree/sml-to-coq-with-
hamlet/examples. In particular, we would like to highlight the tree_proof.v
file which contains the translated code for functions on trees, and proofs of
non-trivial theorems about these functions.

###  3.1 Overloaded operators

Some comparison and arithmetic operators in SML are overloaded for multiple
types. For example, the equality check works for strings and integers: val b =
"a" = "a" andalso 5 = 3.

Boolean equality checks for string and integers in Coq, denoted by =??, are
defined in string_scope and Z_scope, respectively. However, the last opened
scope shadows the first, and trying to use both at the same time fails. For
example:

⬇

Require Import String. Open Scope string_scope.

Require Import Bool.

Fail Definition b := ("a" =? "a") && (5 =? 3).

fails because Coq expects 5 to be of type string.

Operation overload is solved using typeclasses. We have defined several
typeclasses for different sets of operators and instantiated them with the
types supported. We also defined notations for the operators to be the same as
SML whenever possible. For example, the typeclass below is instantiated for
strings and integers (among others):

⬇

eqb : A $\rightarrow\;$ A $\rightarrow\;$ bool;

neq : A $\rightarrow\;$ A $\rightarrow\;$ bool

}.

Infix "=" := eqb (at level 70).

###  3.2 Records

A record is a set of named fields typed by record types, for example:

In SML, records can occur as expressions, patterns, or types. When matching a
record pattern, the user can specify the names of relevant fields and omit the
remaining using ellipsis, as long as SML’s type checker can infer the full
record type. For example:

⬇

case r of {age = x, ...} $\Rightarrow\;$ x;

Gallina supports record types, however these must be declared using Record. So
the getAge function above could be:

⬇

Definition getAge (r : rec) := match r with

{| name := _; age := x |} $\Rightarrow\;$ x.

There are three important points that must be taken into consideration when
translating records:

  1. 1.

Any record expression, type, or pattern in an SML declaration might require a
Record declaration preceding the translation, and record types must be
replaced by the Record identifier.

  2. 2.

The Record declaration automatically generates projection functions for each
of the record’s fields. As a result, field names cannot be reused in the code.

  3. 3.

There is no Gallina equivalent to SML’s ellipsis when pattern matching
records. So the translation must make all record fields explicit in patterns.

To make sure all necessary records are declared in the translation, we make
use of a _record context_ associated with Gallina’s AST. This context is split
into a local and a global part. The global record context $\mathcal{R}_{\\_}g$
contains all record types that already have a declaration in the AST. The
local record context $\mathcal{R}_{\\_}l$ is used in the translation of SML’s
declarations, and starts empty. As the declaration is deconstructed, record
expressions, patterns, or types may be encountered. If there exists a record
type in $\mathcal{R}_{\\_}g$ or $\mathcal{R}_{\\_}l$ such that the fields are
the same, and their types are more general, then the translation proceeds as
usual. If not, the type is stored in $\mathcal{R}_{\\_}l$ using a fresh name.
Once the declaration translation is done, the types from $\mathcal{R}_{\\_}l$
are translated into Records occurring before the declaration. The content of
$\mathcal{R}_{\\_}l$ is then added to $\mathcal{R}_{\\_}g$.

To avoid name clashing, we modify the record fields’ names by prefixing it
with the fresh name used for the record type. Each time a record type,
expression, or pattern is found, either its type is found in the record
context, or a new type is created. In both situations we are able to tell what
this prefix is, and rename the fields accordingly.

Ellipsis on record patterns are resolved by looking into the annotations after
SML’s elaboration phase. Since the record type must be able to be inferred,
this information can be extracted after elaboration, and the pattern can be
unfolded with all fields.

The result of translating a record type and a function on this type is shown
in Figure 1.

⬇ fun isBob ({name = "Bob",...}: r) = true | isBob {...} = false
---
⬇ Definition r := rid_1. Equations isBob (x1: r): bool := isBob {| rid_1_age
:= _; rid_1_name := "Bob" |} := true; isBob {| rid_1_age := _; rid_1_name := _
|} := false.
Figure 1: Translation for records

###  3.3 Polymorphic Types

The treatments of polymorphic values in SML and Coq are different. For
example, in SML val L = [] declares an empty list L of type ’a list, where ’a
is a type variable. This value can be safely used with instantiated lists: L =
[3] is a well-typed boolean expression (which evaluates to false).

In contrast, a “polymorphic” empty list can be declared in Coq in (at least)
two different ways:

⬇

Definition L2 {A : Type} := [] : list A.

The types of the terms L1 and L2 _as is_ (i.e. without annotations) are
sligthly different:

⬇

L2 : list ?A where ?A : [ |- Type]

The definition of L1 looks more similar to what is written in SML. However, if
we want to use L1 in other terms with instantiated lists (such as L = [3]),
then we need to write: (L1 _) = [3]555Here _ represents the type variable A
whose type is inferred by Coq.. To avoid adding the type parameter explicitly,
we can use L2, which is implicitly interpreted as L2 _ by Coq. Indeed, the
(type-)check L2 = [3] succeeds.

As a result, type variables are made explicit when translating polymorphic SML
value declarations so that these values can be used _as is_ in the rest of the
program, like the example of L2. This is done using a type variable context
$\mathcal{T}$. The type variable context is always empty at the beginning of a
declaration’s translation and, as the declaration is traversed, “unknown”
types are added to the context. An unknown type becomes “known” when it is
added to $\mathcal{T}$. That is, when the translator encounters an expression
e with unknown type $\alpha$, it adds $\alpha$ to $\mathcal{T}$. If a later
expression e’ has type $\alpha$, the translator treats this as a known type,
not changing the type variable context. At the end of the translation,
$\alpha$ is added as an implicit argument of the resulting Coq definition, and
the translation of the expression e is annotated with the type $\alpha$. For
example, val L = [] is translated to:

where _’13405 is the name of the type variable determined by HaMLet.

Note that this is only needed for value declarations. Functions on polymorphic
types do not need explicit type parameters since they can be automatically
generalized using Generalizable All Variables.

###  3.4 Non-exhaustive Matches

A very common practice when programming in SML is to use patterns for values
to deconstruct expressions. For example: val x::l = [1,2,3] would result on
value x being bound to 1 and l bound to [2,3]. SML’s interpreter will issue a
Warning: binding not exhaustive, but accepts the code. The warning makes sense
since it is usually not possible to tell before runtime if the expression on
the right will match the pattern (for example, when it is the result of a
function application). Non-exhaustiveness is indicated by a flag in the
declaration’s annotation after elaboration.

Such declarations cannot be directly translated into Gallina because
Definitions cannot be patterns, only identifiers. Patterns are accepted in let
’ pat := term expressions, but term can _only_ resolve to pat (i.e. its type
has only one constructor). The translation of non-exhaustive declarations is
made exhaustive by adding a default case resulting in a patternFailure axiom:
(the same strategy is used in [10]): Local Axiom patternFailure: forall {a},
a. We should note here that the default case will never be reached in the
translated code, as this would mean there was a Bind exception raised when
evaluating the SML code. As mentioned before, the SML code is evaluated before
starting the translation, and if it terminates abnormally (with an exception,
for example), SMLtoCoq terminates too.

In addition to that, top level declarations need to be split into as many
definitions as there are variables being bound. This is done by recursively
traversing the pattern and collecting the variables. For each of them, a new
Gallina definition is created. For example, val x::l = [1,2,3] becomes:

⬇

| _ $\Rightarrow\;$ patternFailure

end.

Definition l := match [1; 2; 3] with (x :: l) $\Rightarrow\;$ l

| _ $\Rightarrow\;$ patternFailure

end.

Note that the structure of the match term is the same, apart from the variable
returned on the non-default case. If the declaration is inside a let block, it
is translated into multiple nested let blocks.

###  3.5 Functions

Unless a function is total and structurally decreasing at every recursive
call, it cannot be translated into Fixpoint (or Definition, in case it is not
recursive) directly. Most of the problems we encountered in function
translation could be solved using the Equations plugin, which provides a
powerful tool for defining terminating functions via pattern-matching on
dependent types. Equations turned out to be more flexible and easier to use
than Coq’s built-in Program command.

####  3.5.1 Pattern matching

Programming in SML typically makes extensive use of pattern-matching, most
common among which is pattern-matching on function inputs, for example:

⬇

| length (x :: l) = 1 + length l

Gallina, however, does not allow pattern-matching on function parameters which
means that the above function would – in the best case – be translated to the
following Coq code:

⬇

match id with

| [] $\Rightarrow\;$ 0

| x :: l $\Rightarrow\;$ 1 + length l

end.

While this looks acceptable, the translation is complicated as the number of
(curried) parameters increases since match only deals with one term at a time.
Equations allows the definition of functions by pattern matching on the
arguments without the need for an intermediary match expression. This enables
SMLtoCoq to produce code that looks much more similar to the corresponding SML
code. For example, the length function defined above translates to the
following in Coq with Equations:

⬇

length [] := 0;

length (x :: l) := (1 + (length l)).

The main limitation associated with using Equations is that the function’s
input and output types have to be explicit. This does not pose much of a
threat since we have type information from HaMLet’s elaboration, and having
them explicit does not affect the semantics of the code.

⬇ REQUIRES: x > 0 andalso y > 0; ENSURES: b > x andalso b > y; !!) fun
posAdd(x, y) = x + y;
---
⬇ posAdd (x, y) := (x + y). Theorem posAdd_THM: forall x y b, posAdd(x, y)=b
/\ ((x > 0) && (y > 0)) = true $\rightarrow\;$ ((b > x) && (b > y)) = true.
Admitted.
Figure 2: Translation for function contracts

####  3.5.2 Contracts

Deductive verification is a common way to do formal verification, which
consists of generating mathematical proof obligations from the code’s
specifications, then discharging these obligations using proof assistants such
as Coq or automated theorem provers. Generating correct proof obligations is a
crucial step in this process. To aid in this task, SMLtoCoq automatically
translates function contracts (added to HaMLet as explained in Section 2.1)
into Coq theorems. A contract of the form:

⬇

REQUIRES: precond;

ENSURES: postcond; !!)

is translated into:

⬇

$\rightarrow\;$ postcond = true.

The theorem’s precond and postcond are the translations of SML boolean
expressions precond and postcond, respectively. As such, they have type bool
and not Prop, hence the need to use = true in the theorem statement. The
quantified vars are the set of variables used in input and output. This
theorem is placed after the function definition in the Gallina code followed
by Admitted, and the proof is left to the user. An example of the resulting
translation of a function with pre and post conditions is shown in Figure 2.

####  3.5.3 Mutual recursion

Figure 3 shows the translation of a mutually recursive type and function.
SML’s and construct maps nicely to Coq’s with, which can also be used for
Equations. One interesting thing to note about this example is how the
polymorphic types evenList and oddList need to be annotated in Coq. First of
all, they take a type variable as an implicit type due to the treatment of
polymorphism explained in Section 3.3. As a result, when this type is used and
a type variable is passed explicitly to it, it must be preceded by @. Another
thing noticeable in the translation is the presence of %type annotating tuple
types. Depending on the context, Coq cannot distinguish whether * is the tuple
type or nat multiplication, so the annotation indicates to Coq that this is
indeed a type.

⬇ | ECons of ’a * ’a oddList and ’a oddList = OCons of ’a * ’a evenList fun lengthE (ENil: ’a evenList): int = 0 | lengthE (ECons (_, l)) = lengthO l and lengthO (OCons (_, l)) = lengthE l
---
⬇ | ENil | ECons : (_a * @oddList _a)%type $\rightarrow\;$ @evenList _a with oddList {_a : Type} : Type := | OCons : (_a * @evenList _a)%type $\rightarrow\;$ @oddList _a. Equations lengthE ‘(x1: @evenList _a): Z := lengthE ENil := 0; lengthE (ECons (_, l)) := (lengthO l) with lengthO ‘(x1: @oddList _a): Z := lengthO (OCons (_, l)) := (lengthE l).
Figure 3: Translation for mutually recursive type and function

####  3.5.4 Partial functions

One of the powerful features of SMLtoCoq is its ability to handle partial
functions. While it is not possible to define partial functions in Coq as is,
restricting the translation to total code would be a big loss, not only
because partial functions are pervasive in programming, but also: (1) many
times partial functions are defined with guarantees that the function will not
be called on non-valid arguments and (2) Coq’s rich type system accepts
preconditions on functions as part of the function inputs. To address this
issue, we exploit Coq’s powerful support for dependent types to constrain the
function domain. That is, we generate preconditions for partial functions and
add them as function inputs, which Equations can then use to accept functions
that handle the subset of inputs that satisfies the generated preconditions.

A typical example is the head function that returns the head of the list fun
hd (x::l) = x, which is translated to:

⬇

hd (x :: l) := x;

hd _ := _.

Note that the implicit parameter H ensures the function is only called on non-
empty lists, and is thus total.

In simple cases, Equations can automatically derive a contradiction between
the second case and the precondition and all obligations will be discharged.
In more complicated cases, Equations would not be able to derive the
contradiction, and an obligation remains for the user to solve666Coq accepts
unsolved obligations at first, and a user can optionally “admit obligations”
and resolve them when needed..

The preconditions can be generated by simply requiring that the input
parameters match one of the function’s cases, for example: x = case1 \/ x =
case2 \/ ... \/ x = casen. But this can lead to unnecessarily complicated
preconditions in the case of multiple input arguments and/or a function with
multiple branches. Instead, we use the AST’s knowledge of exhaustive patterns
to generate preconditions that are considerably smaller than what would be
produced by this naive procedure. Our algorithm works by identifying _generic_
patterns, which match any input. For example, a single identifier or a
constructor for a datatype with one constructor would be generic patterns.
When preconditions are generated, generic patterns are eliminated because they
are not imposing restrictions on the input. Consider this example:

⬇

| hd_sum ((a,b)::l) l’ init = init + a + b

| hd_sum l ((a’,b’)::l’) init = init + a’ + b’

The naive search would produce the following proposition:

⬇

(\exists a b l, x1 = (a, b)::l /\ \exists l’, x2 = l’ /\ \exists init, x3 =
init) \/

(\exists l, x1 = l /\ \exists a’ b’ l’, x2 = (a’, b’)::l’ /\ \exists init, x3
= init)

Our procedure, however, produces:

⬇

(\exists y1 l, x1 = y1 :: l) \/

(\exists y2 l’, x2 = y2 :: l’)

Note that this can be further simplified to (\exists y1 l, x1 = y1 :: l) \/
(\exists y2 l’, x2 = y2 :: l’). This requires the implementation of a
simplification algorithm for formulas, which we leave for future work. The
actual translation of the hd_sum function is:

⬇

{H: exists y1 y2, eq (x1) (y1 :: y2) /\ exists y1 y2, eq (x2) (y1 :: y2) \/

exists y1 y2, eq (x1) (y1 :: y2) \/ exists y1 y2, eq (x2) (y1 :: y2)}: Z :=

hd_sum ((a, b) :: l) ((a’, b’) :: l’) := (((a + b) + a’) + b’);

hd_sum ((a, b) :: l) l’ := (a + b);

hd_sum l ((a’, b’) :: l’) := (a’ + b’);

hd_sum _ _ := _.

⬇ Parameter t1 : Type. Parameter t2 : Type. Definition t := (t1 * t2)%type.
Parameter default : unit $\rightarrow\;$ t. End PAIR. Module IntString <:
PAIR. Definition t1 := Z. Definition t2 := string. Definition t := (t1 *
t2)%type. Equations default (x1: unit%type): (Z * string)%type := default tt
:= (0, ""). End IntString. Module Example ( Pair : PAIR ). Definition a :=
match (Pair.default tt) with (a, b) $\Rightarrow\;$ a end. Definition b :=
match (Pair.default tt) with (a, b) $\Rightarrow\;$ b end. End Example. Module
S := !Example IntString.
---
Figure 4: Translation for the module system

###  3.6 Structures, Signatures, and Functors

An SML program can be divided into structures – with each structure comprising
a collection of components, (i.e. datatypes, types, and values). A structure
can ascribe to a signature, which acts like an interface. In addition to
structures and signatures, SML also provides _functors_ , which are
essentially structures parametrizes by other structures [5]. Gallina has also
a module system that provides similar mechanisms for structuring programs.
While Gallina’s modules and module types conveniently match SML’s module
language, there is one major syntactical limitation: inline structures and
signatures.

Structure and signature expressions in SML can be either top-level or inline.
Top-level structure and signature expressions in SML have a single format,
where S is the component’s name:

⬇

signature S = signature_exp

Inline structure expressions occur as functors’ parameters:

and inline signature expressions can occur in any of the following ways:

⬇

structure_exp :> signature_exp

include signature_exp

structure S : signature_exp

functor F (structure S : signature_exp) = structure_exp

Note that inline structures and signatures are unnamed.

In Gallina, inline modules and module types are not allowed; they must be
replaced by identifiers. For example, the following attempt of instantiating a
ListOrdered module directly in the parameter of the Dict module: Module D :=
Dict(ListOrdered(IntOrdered)) fails. Therefore, we distinguish between the
translation of top-level expressions and inline expressions. The translation
of inline expressions uses a structure/signature context $\Sigma$. This
context is initially empty and gets populated with ASTs for inline signature
and structure declarations as they are discovered in (possibly nested) inline
expressions. Each declaration in this context is assigned a new name, and this
name is used for instantiating the Coq module. An example of how modules are
translated is shown in Figure 4.

###  3.7 Infix Functions

SML allows the declaration of infix functions via the infix and fun op
constructs. HaMLet keeps track of infix functions in the _infix environment_ ,
which is returned after parsing, together with the AST. As a result, the infix
declaration is not part of the AST. When an infix function is used as a
prefix, it is preceded by op, and this information is available in the AST.
Infix functions can be declared in Coq using Notation or Infix. For our
translation we need to use Notation because Infix assumes the function to be
curried, while in SML infix functions are always uncurried.

Once a function declaration of the shape fun op f is found in SML’s AST,
SMLtoCoq checks if f in the infix environment, in which case it was declared
as an infix function777Note that SML allows non-infix functions to be declared
using fun op.. If f is infix, it creates two additional Gallina sentences to
be placed after the function definition. First, it defines opf as f to be used
when op f is used in the SML code. Secondly, it defines the Notation "x ’f’ y"
so that f can be used in infix form from this point onward. See an example in
Figure 5. Similar to records, SMLtoCoq uses a context to keep track of which
functions have infix notations in the Gallina AST.

⬇ F (x, y) := ((x * x) + y). Definition opF := F. Notation "x ’F’ y" := (F (x,
y)) (left associativity, at level 29). Definition x := (5 F 2). Definition y
:= (opF (2, 3)).
---
Figure 5: Translation for infix functions

###  3.8 Typed patterns

SML supports types in patterns at any level. The same does not hold for
Gallina. For example:

⬇

Fail Definition f := fun ’((x: nat, y: nat)) $\Rightarrow\;$ x + y.

Fail Definition f x := match x with | x : nat $\Rightarrow\;$ 1 | _ $\Rightarrow\;$ 0 end.

Typing the pattern in the first definition is accepted, however, types
“inside” the pattern as in the second definition are rejected. Also, typing
patterns in match expressions is not accepted at all.

If we want to retain the same explicit types as in the SML code, it is
possible to extract types nested in patterns to the top level. However, this
may include other types that were not explicit. Also, we would need to
identify precisely when top-level patterns are not supported, and find an
alternative to make the types explicit. For match expressions, for example,
one can type the expression being matched as opposed to the pattern. Due to
these conflicts, our design choice was to ignore types in patterns. Most of
the times this is not problematic as Coq is able to infer the correct types.
Moreover, function types are already explicit since Equations requires it.

##  4 Related Work

Closest to our approach are hs-to-coq [10], which translates Haskell code into
Coq specifications, and coq-of-ocaml888https://clarus.github.io/coq-of-ocaml/,
which translates OCaml code into Coq specifications. Even if these projects
look (superficially) the same, an important difference is that our main goal
is to lower the entry barrier into interactive theorem proving (in particular,
Coq) for those that are familiar with functional programming (in particular,
in SML). As such, we aim for a translation that looks as similar as possible
to the SML code, which is obtained using the Equations plugin. We note that
Equations is not used in hs-to-coq or coq-of-ocaml, and getting similarly
looking code does not seem to be a priority in those projects, which are more
focused on the formal verification of large codebases. Another distinguishing
feature is the implementation of contracts for functions, which is not
available in Haskell or OCaml.

As mentioned, SMLtoCoq uses the Equations plugin, while both hs-to-coq and
coq-of-ocaml translate functions to Definitions or Fixpoints. As such, they
look quite different (and less elegant) than their Haskell or OCaml
counterparts. For example, definitions of mutually recursive functions in hs-
to-coq require the bodies of the functions to be repeated for each definition,
a problem that is solved using mutually defined Equations (Section 3.5.3). We
find that the Equations plugin helps in obtaining more aesthetically pleasing
functions. Haskell functions are defined via cases, like in SML, but this is
not supported in Gallina (as explained in Section 3.5.1). Therefore, hs-to-coq
must create intermediate names for the arguments to be used in match
expressions. SMLtoCoq avoids this, again via the Equations plugin. When it
comes to partial functions, both hs-to-coq and coq-of-ocaml add a default case
on match expressions, and use an Axiom as its return value. In contrast,
SMLtoCoq generates the domain restriction as a dependent type to be used in
the Equations and avoids the need for a (yet another) Axiom (see Section
3.5.4). We find this is a particularly elegant solution, as it reduces the
amount of inconsistent axioms that need to be used.

Other smaller differences include the treatment of built-in types and records.
While hs-to-coq translate types such as Int into their own implementation
GHC.Types.Int, SMLtoCoq tries to leverage Coq’s types as much as possible,
translating int into Coq’s Z. Records in hs-to-coq are translated into
Inductive types with associated projection functions. SMLtoCoq uses Coq’s
built-in Records, having no need to declare projection functions explicitly
(see Section 3.2). The treatment of these constructs in coq-of-ocaml is
similar to ours. It is worth noting that coq-of-ocaml curries all
constructors, while SMLtoCoq and hs-to-coq retain the user defined datatypes
as faithful as possible to the original definition.

CFML [2] is a tool for verifying Caml programs based on the so-called
_characteristic formulae_. These formulas are derived automatically from the
program (without the need for annotations), and describe its behaviour. The
resulting formula can be proved using Coq. CFML’s newest version uses
separation logic to reason about OCaml code [3]. Differently from SMLtoCoq,
CFML “translates” functions into specification lemmas in Coq, in the style of
Hoare triples.

The Why tool [4] encompasses WhyML, and ML-like language with support for
annotations, and the verifier Why3. Why3 leverages several automated and
interactive theorem provers to discharge proof obligations coming from WhyML
code as automatically as possible. Even if the language resembles our use of
contracts in SML, the goal is not the same. SMLtoCoq uses solely Coq for
verification, and does not aim at automation.

SMLtoCoq translates SML programs into Coq specifications for reasoning. Going
in the other direction, Coq has an extraction mechanism which exports
specifications to OCaml, Haskell, or Scheme. Similarly, F∗ [11] is an OCaml-
like functional language which allows the programmer to state and prove lemmas
about the code. After verification, programs can be extracted in OCaml, F#, C,
WASM, or ASM. To use those tools the programmer needs to have expertise with
proof assistants in advance. SMLtoCoq assumes a greater fluency in programming
and less in theorem proving, thus enabling the user to write programs in their
comfort zone, and later experiment with proving properties in a proof
assistant. We believe this direction helps beginners in Coq understanding how
program specifications would look like.

##  5 Conclusion & Future Work

We have described SMLtoCoq, a tool for automatically generating Coq
specifications from SML programs. To the best of our knowledge, this is the
first tool of its kind. SMLtoCoq is able to handle a considerable fragment of
SML, including constructs that are not trivially translated into Gallina, such
as partial functions, structures, and records. Additionally, we have
implemented contracts for functions and their translation into Coq theorems.
We have also ported a big part of SML’s basis library into Coq, so that the
code can be translated with the minimum amount of modifications. Using the
resulting translation the user is able to prove properties about their code
using Coq.

We plan to improve and extend SMLtoCoq in several ways.

##### Simplification of automatically generated pre-conditions

As mentioned in Section 3.5.4, the automatically generated preconditions for
functions can be further simplified by using logical equivalences. Since the
result is always a proposition in disjunctive normal form, we plan to improve
our procedure by converting that to conjunctive normal form and applying SAT
heuristics for simplifying propositions.

##### Functions inside let blocks

One of the drawbacks of using the Equations library is that Equations is a
top-level declaration. In SML, functions can be declared nested inside let
blocks, for example:

⬇

val n = let fun h x = x + 1 in h 7 end

The definitions of f and g could be declared mutually using Equations’ where
construct. However, if the nesting depth is bigger than 2, the translation
would flatten the structure, which could turn out to be problematic if some
functions have the same name. The definition of h, on the other hand, cannot
be translated into Equations. In this case, we need to define a new
translation using Coq’s native let (fix).

##### Non-trivial recursion

One of the fundamental differences between SML and Coq is that Coq only
accepts terminating functions. Among those, functions that are non-trivially
terminating must be accompanied by a proof of termination to be accepted. At
the moment, SMLtoCoq translates all functions correctly, but those that need
termination proofs cannot be compiled in Coq.

For example, the div_two function:

⬇

div_two 0 := 0;

div_two 1 := 0;

div_two n := 1 + div_two (n / 2) .

is terminating, but not trivially since the recursive call is not on the
predecessor of n, but on n / 2. To make Coq accept this function, we can
annotate it with the well-founded inductive measure to use for the recursive
calls. In this case it is the simple lt function:

⬇

div_two 0 := 0;

div_two 1 := 0;

div_two n := 1 + div_two (n / 2) .

This generates the proof obligation $n/2<n$ for $n\geq 2$ that needs to be
proved by the user.

Using the by annotation, we can also have Coq accept non-terminating
functions, but at the cost of an inconsistent axiom and admitted obligations.

⬇

Equations loop (x1: Z): Z by wf (indMeasure x1) _ :=

loop x := (loop1 ((x + 1))).

Admit Obligations.

We are investigating ways to determine termination information for SML
functions, ideally analogous to Coq’s termination check. It is unlikely we can
automatically figure out the correct inductive measure to use in the
annotation (if there is any), but we can at least have functions that compile,
and leave it up to the user to remove the use of inconsistent axioms and prove
the obligations when possible.

##### Side-effects

Two language features that we have largely (and reasonably) ignored were
exceptions and reference cells. These operations involve side effects and,
naturally, have no easy correspondence in Coq. Fortunately, dealing with side-
effects in pure functional settings is a well-studied problem [8, 12, 6] and
there are different solutions, including Coq libraries, that we could adapt to
translate effectful SML code.

##### Correctness

We would like to formally prove that our translation for SML into Gallina is
correct, which would ultimately guarantee that the reasoning about the code in
Coq translates to its SML source. To that end, we started to formalize our
translation as a derivation system. Our goal is to show a simulation theorem
between the SML source and its translation, using both languages’ evaluation
semantics. We will start with a small, purely functional, core of both
languages, and extend from there.

## References

  * [1]
  * [2] Arthur Charguéraud (2010): _Program Verification through Characteristic Formulae_.  In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP ’10, Association for Computing Machinery, New York, NY, USA, p. 321–332, 10.1145/1863543.1863590.
  * [3] Arthur Charguéraud (2020): _Separation logic for sequential programs (functional pearl)_.  Proc. ACM Program. Lang. 4(ICFP), pp. 116:1–116:34, 10.1145/3408998.
  * [4] Jean-Christophe Filliâtre & Andrei Paskevich (2013): _Why3 — Where Programs Meet Provers_.  In Matthias Felleisen & Philippa Gardner, editors: Proceedings of the 22nd European Symposium on Programming, Lecture Notes in Computer Science, Springer, pp. 125–128, 10.1007/978-3-642-37036-68.
  * [5] Robert Harper (2011): _Programming in Standard ML_.  Licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0.
  * [6] Thomas Letan & Yann Régis-Gianas (2020): _FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq_.  In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, Association for Computing Machinery, p. 32–46, 10.1145/3372885.3373812.
  * [7] Robin Milner, Mads Tofte & David Macqueen (1997): _The Definition of Standard ML_.  MIT Press, 10.7551/mitpress/2319.001.0001.
  * [8] Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau & Lars Birkedal (2008): _Ynot: Dependent Types for Imperative Programs_.  In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP ’08, Association for Computing Machinery, p. 229–240, 10.1145/1411204.1411237.
  * [9] Matthieu Sozeau, Cyprien Mangin, Pierre-Marie Pédrot, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Robin Green, Maxime Dénès, Hugo Herbelin, Guillaume Claret, Siddharth, Enrico Tassi, Anton Trunov, Joachim Breitner, Antonio Nikishaev, SimonBoulier, Søren Nørbæk, Vincent Laporte & Yves Bertot (2020): _mattam82/Coq-Equations: Equations 1.2.3 for Coq 8.11_.  10.5281/zenodo.3967149.
  * [10] Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah & Stephanie Weirich (2018): _Total Haskell is reasonable Coq_.  Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018, 10.1145/3167092.
  * [11] Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué & Santiago Zanella-Béguelin (2016): _Dependent Types and Multi-Monadic Effects in F*_.  In: 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, pp. 256–270, 10.1145/2837614.2837655.
  * [12] Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce & Steve Zdancewic (2020): _Interaction trees: representing recursive and impure programs in Coq_.  Proceedings of the ACM on Programming Languages 4(POPL), p. 1–32, 10.1145/3371119.