Areej Merhi

Guillaume Grelaud

Nicolas Ripoche

Adam Barlow

Marie P Cifuentes

Mark G Humphrey
email: mark.humphrey@anu.edu.au

Frédéric Paul
email: frederic.paul@univ-rennes1.fr

Christine O Paul-Roth
email: christine.paul@univ-rennes1.fr

A Zinc(II) Tetraphenylporphyrin Peripherally Functionalized with Redox-Active "trans-[(η 5 -C 5 H 5 )Fe(η 5 -C 5 H 4 )C≡C](κ 2dppe) 2 Ru(C≡C)-" Substituents: Linear Electrochromism and Third-Order Nonlinear Optics

Keywords: Porphyrin, Alkynyl complex, Ferrocene, -conjugation, Electrochromism, Nonlinear optics

A nonametallic organometallic-coordination complex (4), assembled from redox-active ferrocenyl (Fc) and Ru( 2 -dppe) 2 fragments (dppe = 1,2-bis(diphenylphosphino)ethane) as peripheral donor groups and a central Zn(II) tetraphenylporphyrin (ZnTPP) core, has been prepared and characterized. Complex 4 is obtained in one step from a pentametallic organometallic porphyrin precursor following substitution of the peripheral chloride ligands by ferrocenylalkynyl moieties (CCFc). The spectroelectrochemistry of 4, and that of previously reported porphyrins featuring related peripheral electron-rich d 6 -transition metal alkynyl units, has been investigated; the optical and redox properties of 4 are briefly discussed, and its potential, and that of a related pentanuclear tetraferrocenyl ZnTPP complex, to function as redox-switchable chromophores is examined. Preliminary studies of the cubic NLO properties of 4 have been undertaken by Z-scan studies at 560 nm and 630 nm, the results from which are also reported.

Introduction

Materials with cubic non linear optical (NLO) properties are required for various applications, in photonics, nanophotonics, and biophotonics [1][2][START_REF] Prasad | Nonlinear Optical Effects in Molecules and Polymers[END_REF]. The processing of optical signals such as ultrafast switching or modulation of optical beams using materials with sizeable third-order NLO responses is of significant interest [START_REF] Prasad | Nonlinear Optical Effects in Molecules and Polymers[END_REF][START_REF] Luther-Davies | [END_REF][5]. Amongst the wide range of molecular chromophores investigated in the last 30 years, organometallic compounds have emerged as very promising building blocks to access new NLO-active materials [6][7][8], while the outstanding cubic NLO properties of porphyrins are also widely recognized [9][10][11][12]; in particular, several families of porphyrins with extended -manifolds have been systematically screened for their large multiphoton absorption cross-sections in the visible/near-IR range [13,14]. Along the same lines, organometallic metal-alkynyl complexes were first investigated for their NLO responses in the mid-1980s [15]. These complexes allow for greater structural control and design than their purely organic counterparts, as the metal centre, oxidation state, ligation and, in some cases the geometry of the complex can be systematically varied [16][17][18].

Moreover, in specially designed dipolar electron-rich d 6 metal-alkynyl derivatives, the polarizable metal centre can act as a powerful donor group, affording access to multipolar organometallic architectures with redox-switchable NLO properties. [19,20] Indeed, due to the existence of kinetically stable oxidized state(s) with distinct NLO properties, redoxswitching of the NLO behaviour has been demonstrated in several instances at selected wavelengths with these particular building blocks [21,22]. More recently, fluorescence has also been switched in a related Zn(II) diphenylporphyrin ([ZnDPP]) conjugate. [23] Peripheral functionalization of a Zn(II) tetraphenylporphyrin core by metal-alkynyl complexes was therefore envisioned as an attractive target. Scheme 1. Selected Organometallic Porphyrin Derivatives.

Accordingly, we have recently found that monomeric Zn(II) tetraphenylporphyrin (ZnTPP) derivatives functionalized by electron-rich metal alkynyl complexes, such as 1-X and 2 (Scheme 1), exhibit strong cubic NLO activity at specific wavelengths in the visible/near-IR range, in particular large effective two-photon absorption (TPA) crosssections in the range 700-750 nm [24,25]. We report herein UV-vis-NIR spectroelectrochemical data for 2 and 3, as well as that of a new ZnTPP derivative 4, obtained in one step from 3, together with preliminary Z-scan studies on 4 at specific wavelengths. The potential of these compounds to exhibit redox-switchable NLO behaviour is briefly discussed, along with the impact of their structural differences on this remarkable property.

Experimental

General procedures

All reactions were performed using standard Schlenk techniques under argon with magnetic stirring [START_REF] Shriver | The Manipulation of Air-Sensitive Compounds[END_REF]. Anhydrous CH 2 Cl 2 was distilled from CaH 2 and sparged with nitrogen before use ; all other solvents were HPLC grade and used as received. Commercially available reagents were used without further purification unless otherwise stated. [Na][PF 6 ] (Sigma-Aldrich) was recrystalized from MeCN.

1 H, 31 P and 13 C NMR spectra were recorded as CDCl 3 solutions using Bruker 200 DPX, 300 DPX and 500 DPX spectrometers. The chemical shifts are given in ppm and referenced to residual solvent peaks. The assignments were performed by 2D NMR experiments: COSY (Correlation Spectroscopy), HMBC (Heteronuclear Multiple Bond Correlation) and HMQC (Heteronuclear Multiple Quantum Coherence). IR spectra were recorded on Bruker IFS 28 spectrometer, using KBr pellets or in dichloromethane solution. UV-vis-NIR spectra were recorded on UVIKON XL (Biotek) and on Cary 5000 (Varian) spectrometers, while spectroelectrochemical experiments were performed using a homemade cell, as described below.

Cyclic voltammograms were recorded at 25 °C in CH 2 Cl 2 solutions (containing 0.10 M [n-Bu 4 N][PF 6 ], purged with nitrogen and maintained under inert atmosphere) at 100 mV/s scan rate using an a e-corder 401 potentiostat system from eDaq Pty Ltd (using a Pt disk as working electrode, a Pt wire as counter-electrode and an Ag/AgCl reference electrode; E° = -0.113 V vs. SCE). The FcH/FcH + couple was used as an internal calibrant for the potential measurement (0.46 V vs. SCE, ΔE p = 0.09 V; i pa /i pc = 1). [START_REF] Connelly | [END_REF] Elemental analyses were performed at the micoanalytical service unit at the Australian National University (ANU). High-resolution mass spectra were recorded on a ZabSpec TOF Micromass spectrometer in FAB mode or ESI positive mode in CH 2 Cl 2 /MeOH mixtures (9:1) at CRMPO in Rennes.

The porphyrin precursor 5,10,15,20-tetrakis{trans-[bis{bis(1,2-(diphenylphosphino)-ethane}chlororuthenium(II)](4-ethynylphenyl)}porphyrinatozinc(II) (3) [25] and ethynylferrocene [28] were prepared according to literature methods.

5,10,15,20-tetrakis{trans-[bis{bis(

Spectroelectrochemistry

Solution UV-vis-NIR spectra of the oxidized species were obtained at 298 K or 248 K by electrogeneration on a platinum mesh electrode in a 0.05 mm optically transparent thin-layer electrochemical (OTTLE) cell, [29] using a silver wire as pseudo-reference and a platinum wire as counter-electrode. Solutions were made up with 0.30 M [n-Bu 4 N][PF 6 ] in dry and deoxygenated CH 2 Cl 2 and kept under an atmosphere of pure nitrogen.

Z-Scan Measurements

Third-order nonlinear optical properties were investigated as previously described [25],

but with some modifications. The laser system is housed in the Research School of Chemistry

Results and Discussion

Synthesis and Characterization of 4

The new nonametallic porphyrin-based assembly was obtained in one step from the previously reported organometallic tetraruthenium-precursor 3 [25], and five equivalents of the ferrocenylalkyne [28]. The coupling proceeded via reaction conditions initially proposed by Touchard et al. for ruthenium alkynyl complex formation [32]. The reaction was monitored by 31 P NMR spectroscopy and was apparently complete after 48 h at room temperature. The desired nonametallic compound 4 was isolated by precipitation, resulting in its isolation in pure form in 63% yield (Scheme 2).

Scheme 2. Synthesis of 4.

This new compound was fully characterized by means of microanalysis, electrospray ionization mass spectrometry (ESI-MS), IR, NMR, and UV-vis-NIR spectroscopies, and cyclic voltammetry (CV). A peak that can be assigned unambiguously to the molecular dication 4 2+ was observed by ESI-MS. The IR spectrum of 4 clearly reveals an intense ν C≡C mode characteristic of σ-alkynyl ruthenium complexes around 2050 cm -1 [20,[33][34][35][36][37]. As often observed [38], the stretching modes of the two distinct alkynyl ligands are not resolved in the infrared spectrum. The 31 P NMR spectrum shows a singlet corresponding to the equivalent phosphorus atoms from the dppe ligands, consistent with a fully symmetric derivative.

Moreover, compared to the 31 P resonance of the precursor 3 at 51 ppm, the signal is shifted to lower field, around 54.5 ppm, as expected for a bis σ-alkynyl complex [39]. The symmetric functionalization of the porphyrin core in 3 is also confirmed by 1 H NMR spectroscopy, which shows a sharp singlet near 9.40 ppm corresponding to the eight equivalent -pyrrole protons of the macrocyclic spacer. Furthermore, a multiplet in the correct ratio is observed near 4.25 ppm corresponding to the overlapped signals of the cyclopentadienyl protons of the terminal ferrocenyl moieties. Additional evidence for the proposed structure is seen in the 13 C NMR spectrum, despite the fact that the diagnostic quintuplets of the C α alkynyl carbon atoms could not be detected [40,41].

Apart from slight shifts, the UV-vis spectrum of 4 strongly resembles that of 3, with the two Q bands at 562 nm and 612 nm and the intense Soret band at 420 nm that are diagnostic of the porphyrin core (Fig. 1 and Table 1). This is unsurprising, because the ethynylferrocene fragment is usually poorly absorbing in the visible range ( < 2000 M -1 .cm - 1 ). [42][43] The weak shoulder on the low energy side of the Soret band is tentatively suggested to be associated with the new d Ru * TPP MLCT bands.

Cyclic voltammetry study of 4

The cyclic voltammetry (CV) study of 4 was performed in dichloromethane, with 0.1 M

[n-Bu 4 N][PF 6 ] as supporting electrolyte. When a solution of 4 is scanned over a small potential window (0.0 to 0.9 V) vs. SCE, two chemically reversible oxidation processes are seen at 0.18 V and 0.76 V, corresponding formally to the Fe(II)/Fe(III) and to the Ru(II)/Ru(III) oxidations, respectively (Fig. 2) [20,35,43,45]. There is a slightly larger peakto-peak separation for the oxidation process of 4 at 0.86 V (90 mV), because it likely coincides with the (weaker) first oxidation process of the ZnTPP core, predicted to occur in the same potential range [25,46]. The oxidation of the Fe(II) centers in 4, while taking place at higher potential than in 2, does however occur at significantly lower values than in ferrocene, due to the presence of proximal electron-rich Ru(κ 2 -dppe) 2 groups. Conversely, oxidation of the Ru(II) centers occurs at significantly higher potentials that in the precursor compound 3 [25], due to the existence of a sizeable electronic coupling between these redox-active groups.

[33] When the potential window is expanded to -1.8 /1.6 V (Supporting Information), the two formally metal-centred redox events become irreversible while two additional (irreversible) oxidations processes can be observed at more positive potentials (around 1.2 V and 1.4 V vs.

FcH + /FcH). The first of these, is significantly less intense than the Fe and Ru oxidation waves, and possibly corresponds to the second monoelectronic oxidation of the ZnTPP core of 4 [25]. The second additional oxidation wave, near 1.4 V, has a comparable intensity to the metal-centered processes observed at lower potentials, and might therefore be associated with a process taking place on the four Fe(III) or Ru(III) centers. Employing a less positive switching potential or increasing the scan rate did not render the second ZnTPP oxidation chemically reversible, consistent with a large kinetic instability associated with the nominally decacationic species 4 10+ at the electrode, that results from the mono-oxidation of the eight Fe(II) and Ru(II) metal centers followed by the di-oxidation of the core. Its pronounced instability is not very surprising. Indeed, we have already observed in several instances that dicationic [FcC≡CRu(κ 2 -dppe) 2 C≡C-] 2+ fragments are not particularly kinetically stable in solution [20,33 ]. Increasing the oxidation state of the central porphyrin core after having di-oxidized each branch of 4 will therefore dramatically reduce the kinetic stability of the resulting dececationic assembly. Also, several irreversible reduction waves are observed in scanning to more negative potentials, with that near -1.5 V possibly corresponding to the monoelectronic reduction of the ZnTPP core [47].

Spectroelectrochemistry of 2, 3 and 4

The spectroelectrochemistry of these compounds was also investigated. Isosbestic points consistent with fully reversible behaviour were obtained for the formation of the tetracation 2[PF 6 ] 4 , the redox state of compound 2 featuring organoiron substituents (Figure 3).

As can be seen in Figure 3a, when the potential of the grid of the OTTLE cell is set at 0.5 V, only moderate changes take place in the electronic spectrum as the sample is oxidized. Thus, the Soret band at 23365 cm -1 (428 nm) and the Q-bands of the porphyrin core at 18620 cm -1 (537 nm) and 15750 cm -1 (635 nm) are red-shifted to lower energy by 160 cm -1 , 605 cm -1 and 1085 cm -1 , respectively, while the MLCT band near 28490 cm -1 (351 nm) disappears and a new band appears near 35100 cm -1 (285 nm). New MLCT bands might also appear at lower energy than the Soret band and might be overlapped with the Q bands. [44] Related observations have also been reported for some [ZnDPP] conjugates featuring a [Fe(  2dppe)( 5 -C 5 Me 5 )(C≡C)] substituent. [23] A closer examination (Figure 3b) reveals that a very weak band also appears near 12600 cm -1 (793 nm) as a shoulder on the lower energy Q-band.

The latter might be associated with the LMCT band often observed in Fe(III) [Fe(C≡CAr)(  2dppe)(  5 -C 5 Me 5 )] metal-alkynyl complex cations [23,48]. A similar electronic spectrum was obtained in the UV-vis range for the isolated tetracationic species 2[PF 6 ] 4 [24]. This cationic species was characterized in solution by NMR spectroscopy (Supporting Information) as being an open shell tetraradical with four apparently uncoupled electrons, one at each Fe(III)

center [49]. The negligible electronic coupling between these unpaired electrons is supported by the ESR spectrum (Figure 4) [48], the resolved rhombic structure being diagnostic of noncoupled electrons for such polyradicals [50,[START_REF] Grelaud | β01β[END_REF]. This confirms that the kinetically stable tetranuclear Fe(III) species can be cleanly (and reversibly) accessed by electrochemical means In contrast to the complete chemical reversibility observed for 2, the oxidation of 3 in the OTTLE cell was not fully reversible, since the spectrum of the neutral starting complex 3

could not be fully restored after the oxidation-reduction cycle (Supporting Information). Thus, we did not pursue investigations with 3 any further. Note, however, that the changes in the UV-vis region of the spectrum resulting from oxidation were less pronounced than observed with 2, while qualitatively similar changes were observed in the near-IR region of the spectrum (except for the sharp decrease in reversibility). Finally, the new nonanuclear porphyrin derivative 4 was subjected to oxidation in the OTTLE cell. The temperature was lowered to avoid any unwanted side-reaction of the presumedly very reactive 4 9+ species; as a result, the starting spectrum could be fully restored after back-reduction. Setting the potential of the grid at 0.44 V afforded the first oxidized state, which most likely corresponds to the tetracation 4[PF 6 ] 4 with four oxidized ferrocenium endgroups [20]. As a result, the Soret band at 23809 cm -1 (420 nm) and the two Q-bands at 17795 cm -1 (562 nm) and 16340 cm -1 (612 nm) in 4 are not significantly shifted, but the intensity of the second band increases significantly upon oxidation, most likely because of the presence of new underlying transitions (Figure 5). More marked, is the hypsochromic shift of the band at 29940 cm -1 (334 nm) for 4, which now appears at 31350 cm -1 (319 nm) in 4[PF 6 ] 4 ; this is possibly due to the blue shift of the ferrocene-based contribution to this band upon oxidation of the ferrocenyl endgroups [42]. Likewise, new absorptions at 15530 cm -1 (644 nm), extending beneath the Q-bands, and also at 6285 cm -1 (1591 nm) have appeared. These transitions can be associated with oxidation of the ferrocenyl endgroups in the four [trans-Ru(κ 2 -dppe) 2 (C≡CFc){C≡C(1,4-C 6 H 4 )}]-branches, as previously seen with a specially designed model compound [20]. The lowest-energy band most likely corresponds to IVCT within each branch, while the 15530 cm -1 band likely corresponds to a charge transfer transition [54]. Further oxidation by setting the grid of the OTTLE cell at 1.0 V affords the second oxidized state; this most likely corresponds to the polycation 4[PF 6 ] 9 , for which all four arms have been formally dioxidized along with a mono-oxidized central [ZnTPP] •+ core. The two intense bands located at 22320 cm -1 (448 nm) and 8820 cm -1 (1134 nm) are diagnostic of the presence of four [trans-Ru(κ 2dppe) 2 (C≡CFc){C≡C(1,4-C 6 H 4 )}] 2+ -dicationic branches, [20] while the disappearance of the Soret band (which is probably masked by the strong absorption at 22320 cm -1 ) might be attributed to the radical cationic nature of the central ZnTPP core. Indeed, not much is known about the optical absorptions of such cores [46,55], but a decrease in intensity of the Soret band and broadening of the Q-bands in the 14280-18180 cm -1 (550-700 nm) range have been reported upon oxidation of divalent metal porphyrin derivatives [46,56]. Again, no transient extra band that might correspond to an IVCT transition between the peripheral organometallic substituents could be detected at any stage during the oxidation process, consistent with a weak (or negligible) electronic coupling of the peripheral organometallic groups through the ZnTPP core in the various MV states [53,57].

In terms of redox switching (or modulation) of the NLO properties, 4 appears to be a much more promising candidate than 2, because the spectra of its redox isomers are more distinct from each other and from that of the starting complex. It is noteworthy that new and intense absorptions are produced in clearly distinct spectral ranges, such as the IVCT transitions observed in the near IR range for 4[PF 6 ] 4 or the two specific transitions of the dicationic arms for 4[PF 6 ] 9 . At the wavelength of these transitions, optimal switching efficiencies of the cubic NLO effects might be obtained, based on results previously obtained with related heterobinuclear complexes, such as 6 (Scheme 3). [19] Scheme 3. Selected Compounds.

Z-scan measurements of 4

Third-order nonlinearities of 4 were determined by Z-scan studies at 560 nm and 630 nm, the results being listed in Table 2. These two wavelengths correspond to the wavelengths of the Q-bands of 4. Although significant absorption occurs at these wavelengths, the γ value is dominated by the real part ( real ) and not by the imaginary part ( im ), emphasizing the importance of refractive over absorptive effects for this complex in this wavelength region.

The cubic nonlinearity of 4 can be compared to those previously determined for the model complexes 7 and 8 (Scheme 3) at 695 nm and 800 nm, respectively [7]. Although assessed at different wavelengths, there is a ca. three order of magnitude increase in the resulting γ value, confirming the importance of the extended π-manifold of 4 on the cubic nonlinearity. Table 2 also includes the (effective) two-photon absorption (TPA) cross-sections ( 2eff ) [10]. A significant increase is noted compared to the TPA cross-sections of the model alkynylmetal complexes 7 and 8, but this is not so surprising considering that the cross-sections for 4 have been assessed at wavelengths where there is linear absorption, which necessitates caution in interpretation of the data (these cross-sections are actually "effective" cross-sections which most likely result from a combination of TPA, saturable absorption (SA) and reverse saturable absorption (RSA) [17]). These particular third-order NLO effects have considerable importance for the possible application in molecular-based devices for all-optical information encoding [58] or optical limiting [11]. Viewed from this perspective, the fact that positive values are found for 4 at 630 nm whereas negative values have previously been found for the related 2 and 1-X derivatives (Scheme 1) at the wavelength of the second Q-band is noteworthy [24,25]. We cautiously suggest that TPA and RSA may dominate over SA effects at this wavelength for 4, in contrast to 2 and 1-X (X= NO 2 , H, OMe). This differing behavior warrants a more in-depth investigation of these compounds to better understand the molecular origin of this particular change; studies directed towards this goal are currently underway. a Conditions: measurements were carried out in CH 2 Cl 2 ;  values are referenced to the nonlinear refractive index of silica n 2 = 2.92  10 -16 cm 2 .W -1 . b Wavelength of the laser in nm. c 10 -33 esu. The SI units for  are C.m 4 .V -3 , while those in the cgs system (used almost exclusively in the literature, and so given here) are cm 5 .statV -2 or esu.

To convert between the two systems,  SI = (1/3) 4  10 -23  cgs . d Effective two-photon absorption cross-sections in Göppert-Mayer units, the conventional unit for TPA in the literature (1 GM = 1  10 -50 cm 4 .s -1 ). e Not determined because of large one-photon absorption.

Conclusion

We have reported the synthesis and characterization of a new nonanuclear heterometallic molecular architecture of C 4 symmetry (4). The latter was obtained in one step by attaching four alkynylferrocene moieties to a tetraruthenium Zn(II) tetraphenyl porphyrin precursor (3).

The electrochromic properties of 4 were investigated, together with those of the related organometallic porphyrin derivatives 2 and 3, which feature metal alkynyl complexes as peripheral substituents. Amongst these redox-active systems, kinetically stable redox isomers of only 2 and 4 can be reversibly accessed via electrochemistry. Unfortunately, the electronic spectra of 2 and 2 4+ are dominated by ZnTPP-based transitions that are not strongly affected by oxidation of the peripheral organometallic substituents. Thus, quite similar linear optical signatures are found for the tetracation 2 4+ and for the starting compound 2, suggesting only a weak redox modulation of the third-order NLO effects. In contrast, the new system 4 gives rise to two redox isomers with distinctly different linear optical signatures: the tetracation 4 4+ generated first upon oxidation, and the nonacation 4 9+ , formed upon further oxidation. The tetracation 4 4+ presents new absorptions in a clearly distinct range (near-IR) from those of 4 assigned to IVCT and CT transitions within the heterobinuclear arms of the compound, while the nonacation 4 9+ also has a dramatically different electronic spectrum due to the oxidation of the central ZnTPP core along with the dioxidation of each arm. Such compounds offer interesting perspectives for modulation of absorptive cubic NLO effects within three redoxaccessible states at several wavelengths. Consistent with its extended π-unsaturated structure, preliminary Z-scan studies of 4 at 560 nm and 630 nm reveal that refractive effects dominate its cubic NLO behaviour (as given by the molecular value) and highlight an interesting nonlinear absorptive effect at 630 nm. Indeed, compared to the related compounds 1-X and 2 which possess a dominant SA behavior at the wavelength of their second Q-band, the behavior of 4 is probably dominated by RSA or TPA. Studies are currently ongoing to better understand the molecular origin of this phenomenon and to further explore the potential of 4 and related compounds for redox modulation of the NLO properties.

  at the Australian National University and consists of a Quantronix Integra-C-3.5-F regenerative amplifier operating as an 800 nm pump and a Quantronix Palitra-FS BIBO crystal-based optical parametric amplifier. This system delivered wavelength tunable pulses of ~130 fs and was operated at a repetition rate of 1 kHz. Solutions of the compounds in dichloromethane of ca. 0.04 w/w% concentration were placed in 1 mm stoppered Starna glass cells; an identical cell was used for measurements of Z-scans on pure solvent. All measurements were calibrated by referencing to signals obtained from a fused silica plate with a thickness of 4.26 mm. Experiments were performed at selected wavelengths (560 nm and 630 nm) by employing wavelength separators and colour glass filters to reject unwanted wavelengths. The pulse energy was attenuated to the J/pulse range, in order to maintain the nonlinear phase shifts obtained from the samples in the range ca. 0.3 -1.5 rad; this was then used as the excitation source for the simultaneous recording of open-aperture and closedaperture Z-scan traces. The beam was focused to provide a focal spot with Gaussian beam waist w 0  45 -60 mm (giving a Rayleigh length that was always sufficiently greater than the thickness of the cell or the reference silica plate, such that a "thin-sample" assumption was justified). The cuvette travelled on a motorized stage (Thor Labs) in the Z-direction, typically from -40 to 40 mm, and the data were collected using three InGaAs photodiodes (Thor Labs) that monitored the laser input, the open-aperture signal and the closed-aperture signal. The outputs were fed into three channels of a Rhode and Schwarz RTM1054 digital oscilloscope and the data were collected using custom LabVIEW software. The open-and closed-aperture traces obtained after dividing the corresponding signals by the laser input reference were analyzed with the help of a custom fitting program that used equations derived by Sheik-Bahae et al. [γ0]. The real and imaginary parts of the second hyperpolarizability, , of the solutes were then calculated assuming additivity of the nonlinear contributions of the solvent and the solute and the applicability of the Lorentz local field approximation [31]. The values of the imaginary parts of  were also converted into values of the two-photon absorption cross-sections σ 2 .

[ 44 ]Fig. 1 .

 441 Fig. 1. UV-vis absorption spectra of the zinc porphyrins 2-4 in CH 2 Cl 2 at 25 °C.

Fig. 2 .

 2 Fig. 2. Cyclic voltammogram of the zinc(II) porphyrins 2-4 in CH 2 Cl 2 /[n-Bu 4 N][PF 6 ] (0.1 M) at 25 °C at 0.1 V/s between -0.8 and 1.2 V vs. SCE, showing the Fe-(left) and Ru-centered (right) oxidations. The ZnTPP-based oxidations are indicated by an arrow, while the asterisk indicates the FcH/FcH + couple (0.46 V) used as an internal calibrant.

from 2

 2 in the OTTLE cell. Consistent with the observation of a single Fe(II/III) oxidation process in the cyclic voltammogram, no transient extra band that might have corresponded to an intervalence charge transfer (IVCT) transition[52] between the peripheral organometallic [Fe(C≡CAr)(  2 -dppe)(  IVCT bands. This contrasts with related metallated porphyrins such as 5 (Scheme 3), in which ferrocenyl redox-active endgroups are directly linked to the TPP core[53].

Fig. 3 .Fig. 4 .

 34 Fig. 3. (a) Spectroelectrochemistry of compound 2 (tetra-oxidized state shown with dotted line). (b) Detail of the near-IR/visible Conditions: CH 2 Cl 2 , 20 °C, [n-Bu 4 N][PF 6 ] 0.3 M, starting potential: -0.6 V, applied potential: 0.7 V vs. SCE.

Fig. 5 .

 5 Fig. 5. UV-vis-NIR spectro-electrochemistry of 4 (tetra-oxidized state shown with dotted line and nonaoxidized state with grey line). Conditions: CH 2 Cl 2 , -40 °C, [n-Bu 4 N][PF 6 ] 0.3 M, starting potential: -0.4 V, applied potentials: 0.4, 1.0 vs. SCE.

Table 1 Selected

 1

	Complex	UV-vis-NIR (CH 2 Cl 2 )	E°[M-based]	E°[TPP-based]
			max nm ( , 10 3 M -1 .cm -1 )	V vs. SCE a , b
	2		351 (34), 428 (330), 537 (16), 635 (15)	-0.14 (M = Fe) c	0.88 c
	2[PF 6 ] 4	d	338 (sh, 27), 431 (262), 555 (21), 587 (sh, 13),
			682 (11), 778 (sh, 5)
	3		327 (93), 418 (364), 452 (sh, 97), 563 (31),	0.49 (M = Ru) e	0.87, 1.16 e
			615 (39)
	4		240 (sh, 227), 278 (sh, 118), 334 (93), 420	0.18 (M = Fe)
			(368), 562 (26), 612 (32)
	4[PF 6 ] 4	f	248 (257), 319 (99), 422 (197), 565 (65), 605	0.76 (M = Ru)	≈ 0.9 g
			(61), 644 (sh, 23), 1591 (31), 2290 (32)
	4[PF 6 ] 9	f	250 (258), 360 (66), 448 (147), 584 (29), 658	≈ 1.4 g (M = Ru)	≈ 1.β g
			(31), 1134 (95)

Optical and Redox Data for 2-4.[24,25] a Redox Potential, Conditions: CH 2 Cl 2 , 0.1 M [n-Bu 4 N][PF 6 ], scan rate: 0.1 V s -1 . b E°[FcH + /FcH] = 0.46 V.[27] c See ref. [24]. d Isolated tetracation. e See ref. [25]. f Species generated in situ by spectro-electrochemistry at -40 °C in the presence of [n-Bu 4 N][PF 6 ] (0.3 M). g Tentative assignment.

Table 2

 2 Experimental Cubic Nonlinear Optical Response Parameters.

		b		 real c		 imag c		|| c	 2	d	Refs.
	2	570 110 ± 10	21 ± 3	112 ± 10	6600 ± 1000	[24]
		650	/	e	/	e	/	e	-6100 ± 1000 [24]
	4	560 -1030 ± 370 37.1 ± 17	1030 ± 370	18400 ± 8200 This work
		630 -710 ± 130	5.7 ± 1.8	710 ± 130	2240 ± 650	This work
	7	695 0.11 ± 0.10	0.017 ± 0.01 0.11 ± 0.10	6 ± 3	[59]

a Complex 

-C 5 Me 5 )]-substituents was detected during the oxidation process. This indicates that if such processes exist, the peripheral redox groups are too weakly coupled through the ZnTPP core in the corresponding mixed valent (MV) states to give rise to intense

-0.17 ± 0.04 0.071 ± 0.02 0.18 ± 0.045 /[22]

Acknowledgments F.P. and C.O. P.-R. thank the "Université Européenne de Bretagne" (UEB), the CNRS (PICS program N° 5676), and FEDER via an EPT grant in the "MITTSI" program from RTR BRESMAT for financial support. M.G.H. and M.P.C. thank the Australian Research Council for financial support, an Australian Professorial Fellowship (M.G.H.) and an Australian Research Fellowship (M.P.C.), A.M., N.R. and G.G thank the "Région Bretagne" (ARED) for financial support. A. Bondon (ISCR/Rennes) is acknowledged for NMR support.

Appendix A. Supplementary data

Complementary experimental data for 4, spectroelectrochemical traces for 3 and Z-scan plots for 4. Supplementary data associated with this article can be found in the online version.


Martin Clochard

Jean-Christophe Filliâtre

Claude Marché

Andrei Paskevich

Formalizing Semantics with an Automatic Program Verifier ⋆

A common belief is that formalizing semantics of programming languages requires the use of a proof assistant providing (1) a specification language with advanced features such as higher-order logic, inductive definitions, type polymorphism, and (2) a corresponding proof environment where higher-order and inductive reasoning can be performed, typically with user interaction. In this paper we show that such a formalization is nowadays possible inside a mostly-automatic program verification environment. We substantiate this claim by formalizing several semantics for a simple language, and proving their equivalence, inside the Why3 environment.

Introduction

Interactive proof environments, also known as proof assistants, are tools of choice to formalize the semantics of programming languages and, more generally, to handle abstract syntax. For example, the project CompCert [START_REF] Leroy | A formally verified compiler back-end[END_REF], formalizes in Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF] the semantics of a very large subset of the C programming language and verifies an optimizing compiler. Similarly, the L4.verified project [START_REF] Klein | seL4: Formal verification of an OS kernel[END_REF] develops a verified operating system on top of a formalization of C in Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF], ACL2 [START_REF] Kaufmann | Computer-Aided Reasoning: An Approach[END_REF] is used to formalize a Java virtual machine [START_REF] Liu | Java program verification via a JVM deep embedding in ACL2[END_REF], and a complete semantics of JavaScript is formalized using Coq [START_REF] Bodin | A trusted mechanised JavaScript specification[END_REF].

Typically, the formalization of a programming language makes heavy use of advanced logic constructs such as algebraic data types (e.g. to represent abstract syntax trees), inductive definition of predicates (e.g. to encode inference rules for typing or evaluation judgments), higher-order functions, dependent types, etc. Proving results on such a formalization (e.g. type soundness) thus typically involves complex reasoning steps, making use of the interactive tactics that a proof assistant provides for induction, case analysis, etc.

Automatic program verifiers aim at providing dedicated environments to verify behavioral properties of programs written in some specific programming language. Examples are Dafny [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF], VeriFast [START_REF] Jacobs | VeriFast: A powerful, sound, predictable, fast verifier for C and Java[END_REF], Frama-C [START_REF] Cuoq | Frama-C: A software analysis perspective[END_REF], or SPARK [START_REF] Guitton | Why Hi-Lite Ada?[END_REF]. They differ from proof assistants in two ways. First, they allow one to verify programs written in some imperative language whereas proof assistants rely on purely functional programming. Second, the main technique for proving properties is via the use of automatic theorem provers, such as SMT solvers. The high level of proof automation in such environments is possible because the specification languages they propose are less expressive than those of proof assistants. They are typically limited to some flavor of first-order logic.

Why3 is a program verifier developed since 2011 [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF] that proposes a rich specification language, which extends first-order logic with type polymorphism, algebraic data types, and inductive predicates [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF]. Recently, it was augmented with some support for higher-order logic. It is thus a good candidate for experimenting in formalizing semantics using fully automated theorem proving. In this paper, we report on such an experiment. We consider exercises related to defunctionalization [START_REF] Danvy | Defunctionalization at work[END_REF] proposed by O. Danvy at the JFLA'2014 conference. Along the presentation of our solution, we expose the techniques used inside Why3 to encode complex logic constructs into the logic of SMT solvers.

This paper is organized as follows. Section 2 defines a direct, big-step style semantics of a minimal arithmetic language; meanwhile we explain how we deal with algebraic data types, recursive functions, and pattern matching. Then Section 3 introduces another definition in continuation-passing style (CPS) and proves it equivalent to the first one; meanwhile we explain how we encode higherorder logic. Section 4 defunctionalizes the CPS code to get a first-order interpreter; meanwhile we explain how we deal with inductive predicates and complex termination proofs.

The complete solution in Why3, including the full source code and a dump of the proof results, is available at http://toccata.lri.fr/gallery/ defunctionalization.en.html.

Direct Semantics

Our running example is a very simple toy language of arithmetic expressions, limited to literals and subtraction. The grammar for this language is as follows. This language is given a big-step operational semantics, with inference rules defining a judgment e ⇒ n meaning that expression e evaluates to the value n.

n ⇒ n e 1 ⇒ n 1 e 2 ⇒ n 2 n 1 -n 2 = n 3 e 1 -e 2 ⇒ n 3
Since this semantics is deterministic and total, the simplest way is to encode it in Why3 as a logic function, as shown on Fig 1 . This definition is recursive and makes use of pattern matching on its argument e. It is worth pointing out that, for any logic function definition, Why3 statically checks that it defines a total function: recursion must be on structurally smaller arguments and pattern matching must be exhaustive [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF].

Interpreting and Proving

Before doing any proof, we can make some quick tests to check our definitions.

For instance, we can define v3 as the application of eval_0 to p3 constant v3: int = eval_0 p3

and then ask Why3 to evaluate its value:

> why3 defunctionalization.mlw --eval v3 Evaluation of v3: 1

Of course, we can also prove that the value of p3 is 1. We first state it:

goal eval_p3: v3 = 1
Then we ask Why3 to run the Alt-Ergo SMT solver [START_REF] Bobot | The Alt-Ergo automated theorem prover[END_REF] on this goal:

> why3 -P alt-ergo defunctionalization.mlw defunctionalization.mlw eval_p3 : Valid (0.02s)

It is discharged in no time.

Encoding Algebraic Data Types and Pattern Matching

Proving such a lemma with the external provers available within Why3 requires encoding the constructs of algebraic data types and pattern matching into the logic of those provers. The encoding is quite simple: the algebraic type is treated as an abstract type, and constructor symbols are treated as uninterpreted functions whose semantics is established via a number of axioms. Let us see how the expr type is transformed. First come the type and the constructors: Here, 'a denotes a type variable which can be instantiated with any type. Why3 natively supports ML-style prenex polymorphism and employs monomorphic instantiation with symbol discrimination, preservation of interpreted types, and lightweight polymorphism encodings [START_REF] Bobot | Expressing Polymorphic Types in a Many-Sorted Language[END_REF][START_REF] Blanchette | Encoding monomorphic and polymorphic types[END_REF] to efficiently translate polymorphic formulas for provers supporting only multi-sorted or mono-sorted logic.

The definition of match_expr suffices to prove that the ranges of Cte and Sub are disjoint. However, most SMT solvers will not deduce this fact automatically, which is why we also define an index function: The terms in square brackets that appear before the quantified expressions in these axioms are instantiation patterns, also known as triggers. First-order SMT solvers accept triggers as hints to control instantiation of universally quantified premises. A trigger prescribes to an SMT solver to produce a new instance whenever a term that matches the trigger occurs in the set of currently assumed facts. The precise semantics of triggers varies among solvers; in particular, a solver may ignore the patterns given by a user, invent its own triggers, or use an instantiation method not based on triggers, e.g. paramodulation.

In the definition of index_expr, the triggers are given to force the index calculation for every occurrence of a constructor, which is enough to deduce that no application of Cte can be equal to an application of Sub, provided that the prover supports integers and knows that 0 is not equal to 1. If we target a prover that has no support for integer arithmetic, Why3 does not generate the index_expr function and produces instead the axioms of pairwise dis-equality of constructors: Cte n = Sub e1 e2

The index function is preferable, however, because an axiom like Cte_Sub would be instantiated for any two occurrences of constructors, producing a quadratic number of instances.

Then we introduce constructor elimination functions, or projections: And finally, we close the expr type with the inversion axiom: Notice that this translation is not complete. Indeed, we do not state (nor can we in a first-order language) that expr is the least fixed point of constructor application: our translation could be applied to a co-inductive type just as well. This is not an important shortcoming, since the automated provers we target do not perform reasoning by induction, and therefore do not need this property. We will see below how proofs by induction can be constructed directly in Why3. Now, let us show how pattern-matching expressions are translated. In simple cases, such as function definition by pattern matching, Why3 just splits the premise into several instances. Thus, the definition of eval_0 turns into the following conjunction: function eval_0 (e: expr) : int axiom eval_0_def :

(forall n: int. eval_0 (Cte n) = n) ∧ (forall e1 e2: expr. eval_0 (Sub e1 e2) = eval_0 e1 -eval_0 e2)

In the general case, a match-with expression in a formula is translated as a conjunction of implications. For example, a Why3 formula When pattern matching happens in a term, we resort to the selector function.

Here is how the match-with expression in the definition of eval_0 is translated: match_expr e (Cte_proj_1 e) (eval_0 (Sub_proj_1 e) -eval_0 (Sub_proj_2 e))

Like ML or Coq, Why3 admits complex patterns, containing wildcards and or-patterns. These are compiled internally into nested match-with expressions over simple patterns [START_REF] Augustsson | Compiling pattern matching[END_REF].

Continuation-Passing Style

The next exercise is to CPS-transform the function eval_0. It amounts to adding a second argument, the continuation, which is a function k to be applied to the result. This trick allows us to replace any recursive call in the body of a program f by a tail call: C[f x] becomes f x (λv. C v). Of course, this can be done only if the language supports higher-order functions. Such a support was added to Why3 recently.

For the function eval_0, we obtain the function eval_1 in Fig. 2. The new interpreter, interpret_1, calls eval_1 with the identity continuation.

Soundness Lemma

The soundness of our CPS-transformed interpreter can be expressed by two lemmas relating the CPS-based semantics with the direct big-step semantics, one for eval_1 and one for interpreter_1. The first lemma must naturally be generalized: for any continuation k, eval_1 e k returns the same result as the application of k to the direct value of e. The second lemma is an easy consequence of the first one, applied to the identity continuation.

lemma cps_correct: forall p. interpret_1 p = interpret_0 p

Proving the first lemma is not easy. It cannot be proved as such by SMT solvers, since it requires induction on e. Why3 provides two ways to perform such an induction.

Structural induction by a dedicated transformation. The first way is to apply a Why3 transformation, that is a kind of proof tactic directly coded in Why3's kernel, that reduces a given goal into one or several sub-goals that, all together, imply the original goal. Resulting sub-goals can in turn be solved by external provers, or subject to another transformation, etc. A Why3 transformation is devoted to structural inductive reasoning on algebraic data-types, producing one sub-goal for each constructor of the considered data type. For our particular lemma, a heuristics selects structural induction on e, as the goal involves a function defined recursively over e, namely eval_1. Then the proof is easily completed using SMT solvers on the sub-goals. Using such a dedicated transformation to add support for induction in an automated verifier is originally due to Leino [START_REF] Leino | Automating induction with an SMT solver[END_REF].

General induction via lemma functions. The second way to perform reasoning by induction, that would work for general recursion, is to use lemma functions. This concept, that should be classified as folklore, was first emphasized in the VeriFast verifier [START_REF] Jacobs | VeriFast: A powerful, sound, predictable, fast verifier for C and Java[END_REF], where some inductive reasoning is required in the context of representations in separation logic. Such a notion also exists in Dafny [START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF], and now in Why3. It is based on the idea that a recursive program can be used to simulate induction, as soon as it is terminating and side-effect free. In Why3, such a lemma function is written as follows: Here we are defining a program, using let instead of function. As for any program, we have to prove it correct, i.e., a verification condition is generated. When such a program is given the extra attribute lemma, its contract is then turned into a logical statement, which is added to the logical context. The statement is exactly that of lemma cps_correct_expr above. For that to be sound, a termination proof is mandatory, hence the variant clause. In this case, it means that recursive calls are made on arguments that are structurally smaller than e.

(More details on variants and termination proofs are given in the next section.)

The VC for this lemma function is easily proved by SMT solvers.

Encoding Higher-Order Functions

Why3 is essentially a first-order system. It treats the mapping type 'a → 'b as an ordinary abstract type whose inhabitants are lambda-abstractions. Why3 desugars functional applications like (k (eval_0 e)) using a binary "mapping application" operation: k @ eval_0 e. Partial applications of function and predicate symbols are replaced with suitable lambda-abstractions. Why3 does not implement higher-order unification and provides no means of construction of new mappings beyond what can be derived from the user axioms using first-order logic. Thus, the only construction that requires special treatment is lambda-abstraction.

Why3 translates abstractions to first-order logic using lambda-lifting. This amounts to representing every lambda-term in the problem as a fresh top-level function which takes the free variables of that lambda-term as arguments. For example, here is how the definition of eval_1 in Fig. 2 Here, lam1 represents the inner lambda-term \ v2. k (v1 -v2). The function lam2 represents the outer term \ v1. eval_1 e2 (\ v2. k (v1 -v2)).

Since eval_1 and the introduced functions lam1 and lam2 are mutually recursive, Why3 puts the translated definition of eval_1 between the declarations of uninterpreted symbols lam1 and lam2 and the axioms that define their semantics.

Why3 assumes extensional equality of mappings, even though it does not include the corresponding axiom in the translation (this may change in future versions). Because of this, lambda-terms that occur under equality are not lifted, but inlined. For example, an equality id = \ n: int. n is rewritten into forall n: int. id @ n = n. Then the axiom of extensionality can be directly proved in Why3.

The current implementation does not detect when two lambda-terms are instances of one common pattern. In particular, this makes it not robust with respect to inlining: if the definition of a function symbol contains a lambda-term and is inlined, then every occurrence of that term will be lifted separately, which

Defunctionalization

The next step of our case study is to "defunctionalize" the code of the previous section. The general idea of defunctionalization is to replace the functions used as continuations by some first-order algebraic data type, having as many constructors as the various lambdas in the CPS code. For our example, this data type is

type cont = A1 expr cont | A2 int cont | I
It has three constructors, corresponding to the three continuations of the code on Fig. 2, two on line 5 and one on line 8. The second continuation on line 5 is (\ v2. k (v1 -v2)). It has two free variables: v1 of type int and k which is itself a continuation. The constructor A2 associated to this continuation is thus given parameters of type int and cont (hence the algebraic data type is recursive). Similarly, the first continuation has both e2 and k as free variables, so the corresponding constructor A1 is given parameters of type expr and cont. Finally, the third continuation has no free variables. It is associated to the constant constructor I.

To derive a new interpreter interpret_2, we introduce an extra function continue_2, defined mutually recursively with function eval_2. It takes as arguments a continuation c and a value v, and evaluates c applied to v. Notice that we now define programs, introduced with let, instead of logic functions introduced with function. The reason is technological: the mutual recursion above cannot be statically checked terminating by Why3, the termination argument being not structural. The termination has to be proved by theorem proving, as shown in Section 4.3 below.

It is worth pointing out that the code of eval_2 and continue_2 only make tail calls. Thus it can be seen as a small-step semantics for our language or, equivalently, as an abstract machine for interpreting programs in this language.

Soundness

Since we wrote a program and not a logic definition, the soundness of our defunctionalized interpreter is not expressed by a pure logical lemma but with a contract for the interpret_2 program, where the post-condition tells that the result coincides with the big-step semantics. To achieve the proof that the interpreter satisfies this contract, we need to find appropriate contracts for the auxiliary programs eval_2 and continue_2. For that purpose, a first idea would be to define a logic function eval_cont (c:cont) (v:int) returning the evaluation of c on v. Such a function would be a non-structurally recursive function, and would be rejected by Why3: logic functions and predicates must be guaranteed to terminate (see Section 5 for a discussion about this limitation of Why3). However, instead of a logic function, we can define a ternary predicate eval_cont (c:cont) (v:int) (r:int) expressing that r is the result of the evaluation of c on v. Such a predicate can be defined inductively as follows.

inductive eval_cont cont int int = | a1 : forall e: expr, k: cont, v r: int. eval_cont (A2 v k) (eval_0 e) r → eval_cont (A1 e k) v r | a2 : forall n: int, k: cont, v r: int. eval_cont k (n -v) r → eval_cont (A2 n k) v r | i : forall v: int. eval_cont I v v Such a definition corresponds to a set of inference rules for an evaluation judgment c v ⇒ r that means "the application of continuation c to the value v evaluates to r". To ensure the consistency of the definition, Why3 checks for the standard positivity conditions of occurrences of eval_cont in each clause. The contracts for our auxiliary programs can then be stated as follows. Annotated as such, those programs are easily proved correct by automated provers. For example, Alt-Ergo, CVC3, and Z3 all discharge the VCs in no time.

Encoding of Inductive Predicates

Translation of inductive predicates for first-order provers is similar to that of algebraic types: Why3 declares an uninterpreted predicate symbol and then adds one axiom per clause of the inductive definition plus the axiom of inversion. Here is the translation of the eval_cont predicate.

. eval_cont k (n -v0) r0 ∧ k0 = A2 n k) ∨ (k0 = I ∧ v0 = r0))
Just like in the case of algebraic types, this translation is incomplete, because we are unable to express in first-order logic that eval_cont is the least relation satisfying the axioms. If we declared eval_cont as a coinductive predicate (which is also supported by Why3), the translation for first-order provers would be exactly the same. This does not present a problem, since these provers do not perform reasoning by induction or by coinduction. However, it is desirable to be able to make proofs by induction over an inductive predicate inside Why3, using dedicated transformations and/or ghost lemmas, similarly to what we do for algebraic types (Sec. 3.1). This is one of the directions of our future work.

Termination

So far, we have proved the partial correctness of our interpreter. This is not fully satisfactory since an implementation that would loop forever would also satisfy the same contract. We thus aim at proving termination as well.

Because the two auxiliary programs are mutually recursive in a quite intricate way, it is not completely trivial to find a termination measure that decreases on each recursive call. One adequate measure is given by the following ad-hoc size functions: Generally speaking, a set of mutually recursive programs can be annotated as

let rec f 1 x 1 variant { v 1,1 (x 1 ) [with R 1 ], . . . , v 1,m (x 1 ) [with R m ] } . . . with f n x n variant { v n,1 (x n ) [with R 1 ], . . . , v n,m (x n ) [with R m ] }
where each v i,j returns a value on some type τ j and R j is a binary relation on τ j . The verification conditions are then:

1. Each relation R j must be well-founded. 2. For each call f i (e) in the body of the program f j , the vector (v i,1 (e), . . . , v i,m (e)) must be strictly less than the vector (v j1 (x j ), . . . , v j,m (x j )) with respect to the lexicographic combination of order relations R 1 , . . . , R m .

These verification conditions ensure termination because if there were an infinite sequence of program calls, there would be an infinite decreasing sequence for R 1 , . . . , R m . Why3 assumes default relations for the variant clauses so that, most of the time, the user does not need to provide the relation. If the type τ j is int, the default relation is

R int y x := x > y ∧ x ≥ 0.
If τ j is an algebraic data type, then R j is the immediate sub-term relation. For our interpreter, the default relation R int is used. The VCs related to termination cannot be proved automatically, since SMT solvers lack the information that sizes are non-negative. So we first state this as two lemmas: Both require induction to be proved. As we did earlier in Section 3.1, we can either use Why3's transformation for structural induction or turn these lemmas into recursive lemma functions. The former is simpler. Once these two lemmas are proved, termination of eval_2 and continue_2 is proved automatically by SMT solvers.

Conclusions

Using the automatic program verifier Why3, we solved a student exercise aiming at illustrating, on a simple language, the relations between various semantics that were described in a research paper [START_REF] Danvy | Defunctionalization at work[END_REF]. Unlike the students, we did not only code the interpreters and tested them, but also proved them correct. We formalized the big-step semantics of that language and proved correct its compilation, first into a CPS-style semantics and then into a small-step one, close to an abstract interpreter. The complete example available at http: //toccata.lri.fr/gallery/defunctionalization.en.html also contains another variant of that language, forbidding negative numbers and possibly raising an "Underflow" exception. It also formalizes another semantics based on rewriting, making an analogy between reduction contexts and continuations, and an explicit abstract machine for executing the language. Even if the specifications and the proofs require advanced features such as algebraic data types, inductive predicates, and higher-order functions, we were able to prove our interpreters formally using only automated theorem provers.

Related Tools and Experiments. Why3 is not the only software verification tool where this kind of formalization can be done. For instance, the second Verified Software Competition [START_REF] Filliâtre | The 2nd verified software competition: Experience report[END_REF] featured a challenge related to the semantics of S and K combinators and this challenge was successfully tackled by systems such as ACL2, Dafny, VCC [START_REF] Cohen | VCC: A practical system for verifying concurrent C[END_REF], or VeriFast. Some features, such as algebraic data types and pattern matching, can be encoded without too much difficulty if a given system does not have a native support for them. Other features, such as type polymorphism, are much more difficult to simulate. Fortunately, polymorphism (parametric or ad-hoc) gained much traction in the mainstream programming languages (Java generics, C++ templates) and the verification tools follow the trail. For instance, both Dafny and VeriFast support generic types.

Perspectives. The question behind this experiment is whether an automatic program verifier can be a reasonable replacement for an interactive proof assistant for formalizing a programming language, its semantics, and its compilation. More generally, any program performing symbolic computation is a potential use case for the proposed techniques. Recently, we developed a generic approach for data types with binders in Why3. On top of it, we built a verified interpreter for lambda-calculus and a verified tableaux-based first-order theorem prover [START_REF] Clochard | Verified programs with binders[END_REF]. A couple of years ago, we formalized in Why3 a simple imperative while-language [START_REF] Marché | Weakest precondition calculus, revisited using Why[END_REF], with an operational semantics, some Hoare-style rules proved correct with respect to the operational semantics, and (partially) a weakest precondition calculus. This former case study was involving a few Coq proofs and was missing support for higher-order logic, hence it would deserve to be revisited with the current Why3 environment.

Along these lines, we intend to improve Why3 in the following ways. In short term, we want to add support for non-structural recursion in pure functions, as it is done for programming functions. We also intend to allow lambda-expressions to be used in programs, provided they are terminating and side-effect free. A key challenge to apprehend large programs and large proofs is the ability to control the logical context. Indeed, automated provers are extremely sensitive to the number, size, and shape of logical premises. Why3 already provides a module system that allows the user to split specification and implementation into small interlinked components [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF]. We are currently working on the principles of refinement for this module system (both for specification and program code). The idea is to verify program components in a most abstract and minimal context, and then to reuse them in a complex and refined development. Another way to minimize the context before invoking automated provers is to provide some limited interaction where the user filters out irrelevant concepts, e.g. everything which is related to the properties of sorted arrays if the conclusion under consideration does not require it.

Fig. 1 .

 1 Fig. 1. Direct, big-step semantics

  type expr function Cte (n: int) : expr function Sub (e1 e2: expr) : expr Then Why3 defines a polymorphic selector function, which will later help us to encode pattern-matching constructions inside terms: function match_expr (e: expr) (b1 b2: 'a) : 'a axiom match_expr_Cte : forall b1 b2: 'a, n: int. match_expr (Cte n) b1 b2 = b1 axiom match_expr_Sub : forall b1 b2: 'a, e1 e2: expr. match_expr (Sub e1 e2) b1 b2 = b2

  function index_expr (e: expr) : int axiom index_expr_Cte : forall n: int [Cte n]. index_expr (Cte n) = 0 axiom index_expr_Sub : forall e1 e2: expr [Sub e1 e2]. index_expr (Sub e1 e2) = 1

axiom

  Cte_Sub : forall n: int [Cte n]. forall e1 e2: expr [Sub e1 e2].

  function Cte_proj_1 (e: expr) : int function Sub_proj_1 (e: expr) : expr function Sub_proj_2 (e: expr) : expr axiom Cte_proj_1_def : forall n: int. Cte_proj_1 (Cte n) = n axiom Sub_proj_1_def : forall e1 e2: expr. Sub_proj_1 (Sub e1 e2) = e1 axiom Sub_proj_2_def : forall e1 e2: expr. Sub_proj_2 (Sub e1 e2) = e2

  axiom expr_inversion : forall e: expr. e = Cte (Cte_proj_1 e) ∨ e = Sub (Sub_proj_1 e) (Sub_proj_2 e)

Fig. 2 .

 2 Fig. 2. Semantics encoded in CPS form

  lemma cps_correct_expr: forall e: expr, k: int → 'a. eval_1 e k = k (eval_0 e)

  let rec lemma cps_correct_expr (e: expr) : unit variant { e } ensures { forall k: int → 'a. eval_1 e k = k (eval_0 e) } = match e with | Cte _ → () | Sub e1 e2 → cps_correct_expr e1; cps_correct_expr e2 end

  is translated: function lam1 (k: int → 'a) (v1: int) : int → 'a function lam2 (k: int → 'a) (e2: expr) : int → 'a function eval_1 (e: expr) (k: int → 'a) : 'a = match e with | Cte n → k @ n | Sub e1 e2 → eval_1 e1 (lam2 k e2) end axiom lam1_def : forall k: int → 'a, v1 v2: int. lam1 k v1 @ v2 = k @ (v1 -v2) axiom lam2_def : forall k: int → 'a, e2: expr, v1:int. lam2 k e2 @ v1 = eval_1 e2 (lam1 k v1)

with 10 | 11 |Fig. 3 .

 10113 Fig. 3. De-functionalized interpreter

  let interpret_2 (p: prog) : int ensures { result = eval_0 p }

  let rec continue_2 (c: cont) (v: int) : int ensures { eval_cont c v result } with eval_2 (e: expr) (c: cont) : int ensures { eval_cont c (eval_0 e) result }

  predicate eval_cont (e: cont) (v r: int) axiom a1 : forall e: expr, k: cont, v r: int. eval_cont (A2 v k) (eval_0 e) r → eval_cont (A1 e k) v r axiom a2 : forall n: int, k: cont, v r: int. eval_cont k (n -v) r → eval_cont (A2 n k) v r axiom a3 : forall v: int. eval_cont I v v axiom eval_cont_inversion : forall k0: cont, v0 r0: int. eval_cont k0 v0 r0 → ((exists e: expr, k: cont. eval_cont (A2 v0 k) (eval_0 e) r0 ∧ k0 = A1 e k) ∨ (exists n: int, k: cont, v0 r0: int

  function size_e (e: expr) : int = match e with | Cte _ → 1 | Sub e1 e2 → 3 + size_e e1 + size_e e2 end function size_c (c: cont) : int = match c with | I → 0 | A1 e2 k → 2 + size_e e2 + size_c k | A2 _ k → 1 + size_c k end The contracts of our auxiliary functions are then augmented with the following variants: let rec continue_2 (c: cont) (v: int) : int variant { size_c c } ... with eval_2 (e: expr) (c: cont) : int variant { size_c c + size_e e } ...

  lemma size_e_pos: forall e: expr. size_e e ≥ 1 lemma size_c_pos: forall c: cont. size_c c ≥ 0

Acknowledgments. We thank Olivier Danvy for proposing these exercises.

⋆ Work partly supported by the Bware project (ANR-12-INSE-0010, http://bware. lri.fr/) and the Joint Laboratory ProofInUse (ANR-13-LAB3-0007, http://www. spark-2014.org/proofinuse) of the French national research organization


Martin Clochard

Automatically verified implementation of data structures based on AVL trees

We propose verified implementations of several data structures, including random-access lists and ordered maps. They are derived from a common parametric implementation of self-balancing binary trees in the style of Adelson-Velskii and Landis trees. The development of the specifications, implementations and proofs is carried out using the Why3 environment. The originality of this approach is the genericity of the specifications and code combined with a high level of proof automation.

Introduction

Formal specification and verification of the functional behavior of complex data structures like collections of elements is known to be challenging [START_REF] Leavens | Specification and verification challenges for sequential object-oriented programs[END_REF][START_REF] Leino | VACID-0: Verification of ample correctness of invariants of data-structures[END_REF]. In particular, tree data structures were considered in many formal developments using various verification environments. In this paper, we consider self-balancing binary trees, in the style of the so-called AVL trees invented by Adelson-Velskii and Landis [START_REF] Adel'son-Vel'skiȋ | An algorithm for the organization of information[END_REF]. We design a generic implementation of these self-balancing trees from which we derive and verify three instances: random access lists, ordered maps and mergeable priority queues. To reach the appropriate level of genericity in the common part of this development we use an abstract binary search mechanism, based in particular on a notion of monoidal measure on stored data. This notion is shared with an approach proposed by Hinze and Paterson [START_REF] Hinze | Finger Trees: A Simple General-purpose Data Structure[END_REF] for the development of another general-purpose tree data structure they called finger trees. This abstraction allows us to clearly separate the concepts of balanced trees on one hand and search trees on the other hand.

Our development is conducted using the Why3 program verifier, and automated theorem provers to discharge proof obligations. The genericity of the development is obtained by using a module cloning mechanism of Why3, which we present briefly in Section 2. Section 3 develops the structure of self-balancing trees, independently of any notion of search. Then Section 4 presents an abstract notion of search trees based on generic selectors. Finally we present and verify the three proposed instances in Section 5. Related work in discussed in Section 6.

The Why3 formalization is available at http://www.lri.fr/ ~clochard/ AVL/avl-why3.tgz.

Preliminary: Cloning modules in Why3

In Why3, generic development of components is done via the notion of cloning [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF]. Cloning a module amounts to copy its contents while substituting some abstract symbols (types, predicates, functions, procedures) and eliminating some axioms by creating proof obligations for them. In case of procedure substitution, proof obligations are generated as well to check for specification inclusion. This cloning mechanism is used both as an instantiation mechanism for generic development as well as a way to declare standard parameters. For example, suppose that we want to write a development generic with respect to a structure of monoid. Then fresh parameters can be created by cloning a standard abstract module for monoid: And the generic module can later be specialized to a concrete monoid, say integers, by instantiating the monoid abstract symbols.

clone Generic with type t = int,constant zero = Int.zero, function op = (+), lemma neutral, lemma associative

Balanced binary trees in AVL style

We first present a certified implementation of the rebalancing operations for AVL trees. Moreover, this implementation is used to directly derive a logarithmic-time implementation of catenable dequeues.

Representation and logic model

The very first step of a verified data structure implementation is to decide not only what is its internal representation but as importantly what it should represent, i.e its logical meaning. Having a simple logical reflection of the structure usually makes reasoning much easier. The internal representation of an AVL tree is a binary tree storing the height at every node for efficiency reasons. The namespace D corresponds to the abstract data stored in the tree. The chosen model is the list of data stored in the tree in infix order, since it is the part expected to be invariant by rebalancing. However, in order to specify rebalancing, the tree structure cannot be completely abstracted away because of the height requirements, so we also add the height to this model. Here is the Why3 formalization (++ denotes list concatenation):

Representation invariant

The balancing criterion for AVL is that the difference between the heights of two sibling trees does not exceed a given positive bound. The structural invariants are readily transformed into the following Why3 predicate: Note that the constant balancing is left abstract as a positive integer. Most implementations use a concrete value, which is a trade-off between the potential tree depth and the cost of re-balancing the tree. Since the only impact of keeping it abstract showed to be writing a name instead of a constant, that decision was left to client code.

Code and Verification

Balancing is performed via smart constructors for tree nodes and catenation operators, specified in terms of the model to build the expected lists. The parts about the height are a bit more complex, as the information about the resulting height has to be precise enough for proof purposes. For example, here is the specification for the core balancing routine, which simulates the construction of a tree node when the two child sub-trees are slightly off balance: More complex balancing is done via another smart constructor making no hypothesis on the relative height of the two trees, and two catenation operators similar to the node constructors.

As for the verification part, it did not require any human help once the right specifications were written. All proof obligations were completely discharged by automated theorem provers.

Finally, the catenable dequeue implementation is immediate from the balancing code: catenation is provided, and all other operations (push and pop at both ends) are internal sub-routines of rebalancing. It is logarithmic-time, and also features a constant-time nearly-fair scission operation directly derived from pattern-matching over the tree.

Selection of elements in balanced trees

AVL trees were first introduced as binary search trees, so most operations over them involve a binary search by comparison. However, Hinze and Paterson [START_REF] Hinze | Finger Trees: A Simple General-purpose Data Structure[END_REF] have shown that using a generalization of binary search based on monoidal annotations, one could implement a variety of data structures. In this section, we present and verify a generalized implementation of usual AVL routines (insertion, deletion, etc) using a similar approach.

Monoidal summary

The usual search mechanism in binary search trees is search by comparison using a total order. However, by keeping summaries of the contents in each subtrees, one can provide a variety of other mechanisms. For example, keeping the number of elements in each subtree gives positional information, which can be used to perform efficient random access. Hinze and Paterson [START_REF] Hinze | Finger Trees: A Simple General-purpose Data Structure[END_REF] proposed monoids as a general mechanism to keep track of those summaries: the content of each subtree is summarized by the sum of the measures of its elements in some given monoid.

We use those annotations as well to provide different search mechanisms. They are integrated in the development with minimal changes as the height bookkeeping is done the same way. We also add parameters corresponding to an abstract monoid and measure.

Abstracting the binary search mechanism

In their paper about finger trees, Hinze and Paterson suggest to implement most data structure operations using a splitting mechanism, which finds an element where a predicate over the monoidal abstraction of the prefix flips. We could have used this technique, but it has some flaws when considering AVL trees. First and foremost, it completely ignores the fact that the internal tree nodes contain elements that could -and would -be used to guide the search. This is not the case for finger trees as elements are stored in the leaves. Second, the usual insertion/deletion/lookup routines coming with AVL trees would be replaced by much slower (though still logarithmic-time) implementations based on complete splitting of the tree followed by catenation of the parts back together.

This last part, however, is perfectly fit for specification since what binary search does is exactly selecting a split of the list model.

Splits are formalized by the following definitions: The structure of splits corresponds exactly to the two possible outcomes of a binary search in the tree: either finding an element in a node or ending on an empty leaf. In order to describe the particular splits we wish to find, we use an abstract selector parameter: Informally, the selector describes the class of splits we want to find, represented by the selected predicate. The selection_possible describes the lists in which splits corresponding to the selector can be found using binary search. This compatibility mean that one can reduce the problem of finding a split in its class by bisection over the node structure, potentially using the summary of the branches to guide the search. We achieve this decription by adding an abstract routine parameter performing this reduction: Note that the routine is expected to compute new selectors as the reduced problem may be different. Also, we need to ensures that whenever the search ends on a leaf, the only possible split is the selected one. This is expressed by an axiom:

axiom selection_empty : forall s:selector. selection_possible s Nil → selected s { left = Nil; middle = None; right = Nil }

Certified routines based on binary search

Using the abstract binary search mechanism, we certified the implementation of a generalization of the usual routines over AVL trees: lookup, insertion, deletion, as well as splitting. The code is skipped here as it is standard, it is just a matter of replacing the decisions usually done by comparison by a case analysis on the result of selected_part, interested readers may find the code for those routines in appendix A.3. We then focus on the specifications of those routines. For example, let us see how we could specify insertion. Earlier, we mentioned that those procedures could be build on top of splitting: one could perform insertion by splitting the tree, replacing the potential middle element, and rebuilding it afterwards. It turns out to be the right specification for insertion: Note that we use a ghost reference instead of an existential quantifier for the split. While using an existential is possible, there are two reasons for using such a reference instead. First, existentially quantified goals tend to be hard for automated provers. In this case, we can very easily give them an explicit witness via the reference. Second, in case the client code is really hard to prove, one can help the automated provers by providing logical cuts. Such cuts will be much easier to write if the existentially quantified value is known.

The three remaining routines have pretty similar specification:

-Deletion is the converse of insertion: any potential middle element is removed of the split before rebuilding. -Lookup amounts to return the middle of the split.

-Splitting returns a split with lists represented by AVL trees.

Verified Instances

Random-access sequences

The first instance use positional selection, which naturally gives random-access sequences. This is obtained by instantiating the monoid by integers and measuring all elements by 1, which gives fast access to the length of the sub-lists. Using that information, binary search is done by finding in which of the three pieces of the list lies the n-th element. Note that reducing the problem to a sub-list requires the index to change. Also, as random-access lists are completely polymorphic, data elements are instantiated with fully polymorphic values (D.t 'a = 'a).

The formal specification of this kind of selection is straightforward: The extra boolean field is intended to specify whether we want the list to be cut in two pieces or split around the n-th element. Having both allows to derive most positional operations over random-access lists directly from the abstract selection routines:

-Assignment is derived from abstract insertion -Positional insertion is also derived from abstract insertion -Positional lookup is implemented by abstract lookup -Positional deletion is derived from abstract deletion -Both kind of positional splits are derived from abstract splitting.

However, the specifications had to be rewritten as the obtained ones did not match the desired ones for random-access lists. This was done by writing specification wrappers around those operations. The automatic verification of this wrapper did not required human help beyond making explicit a trivial induction correlating the length of the list to its monoidal summary.

As an example of the resulting specifications, here is the one for the assignment procedure:

val set (n:int) (d:'a) (l:t 'a) : t 'a requires { c l ∧ 0 ≤ n < length (m l) } ensures { c result ∧ length (m result) = length (m l) } ensures { forall i:int. i = n → nth i (m result) = nth i (m l) } ensures { nth n (m result) = Some d }

Maps and sets

Another instance correspond to the abstract data structures usually implemented with AVL trees: ordered sets and associative arrays. Those naturally correspond to the case of comparison-based binary search in sorted sequences.

Several new parameters are added to reflect the ordering structure.

-An abstract key datatype -A function extracting keys from data -A computable ordering relation over keys

From those parameters, binary search trees lookup, insertion, and deletion are obtained by using straightforward instances for the selection parameters:

-Selection is done by keys, so the selector type is instantiated by keys.

-Selection can be done only in sorted sequences.

predicate selection_possible (_:'b) (l:list (D.t 'a)) = increasing l -A split is selected by a key if it corresponds to elements with keys lower, equal and greater than the selector respectively. As we do not need the extra summaries here, the monoid is instantiated by the unit monoid. Although this instantiation yields a perfectly valid implementation for ordered associative arrays, it is unsatisfactory from the specification point of view as the data structure is still modeled by a list. This is not a suitable model for associative arrays, which are intended to represent finite key-values mappings. In order to get specifications based on such modeling, we wrote specification wrappers over the implementation. The new model was obtained by interpreting the previous list model as an association list: Note that this instantiation does not break the abstraction barrier: the specification wrappers and selectors are based on the model of the AVL trees only.

The obtained specifications indeed corresponds to the expected behavior of an associative array. For example, here is the specification for insertion (others look alike): The verification of those specification wrappers was not completely immediate, as it required a number of facts over sorted association lists that could be proved only by induction. Mostly, it required a bridge lemma between the notion of selected split of the list and a similar notion stated in terms of key-value mappings. This required a small amount of manual work to state the corresponding lemmas and to make explicit the inductive structure of the proofs.

Finally, certified implementations of ordered maps and sets were derived from this implementation by writing immediate specification wrappers over instances of this implementation.

-Sets were obtained from an instance identifying keys and elements. For specifications, the model was reduced to the predicate of presence.

-Maps were obtained by instantiating the elements with couple formed of a key and a polymorphic value. As keys were irrelevant as outputs of the model mapping, that part was removed from specifications.

Mergeable Priority queues

The last instance presented in this paper is selection of the element with the smallest key, which is an immediate implementation of mergeable priority queues. The corresponding monoid is the minimum monoid over keys extended with the positive infinity, which gives fast access to the smallest key of sub-lists. Then, binary search can be done by taking a path leading to a minimum element. For the ordering and keys, we reuse the same setting as for associative arrays. The specification of minimum selection is quite direct as well: it amounts to say that the split has a middle element and that it is minimal. Binary search can obviously be done by taking the path to the minimum element.

From this instantiation, one can map the priority queue operations to the abstract AVL ones:

finding the minimum is exactly lookup.

removing the minimum is deletion.

adding an element can be implemented by prepending the new element.

merging two priority queues can be done by catenation.

Again, those operations were wrapped under new specifications with a bettersuited model. Since the order of the elements inside the structure is irrelevant, the priority queue is represented by a finite bag: type m 'a = { bag : D.t 'a → int; card : int } function as_bag (l:list 'a) : 'a → int = match l with | Nil → \x. 0 | Cons x q → \y. if x = y then as_bag q y + 1 else as_bag q y end

Here is an example of the final specifications, namely the one for the remove_min operation:

Related Work

Verified balanced binary search trees. Numerous verified implementation of balanced binary search trees have been proposed. For example, implementations of AVL trees have been verified in Coq [START_REF] Filliâtre | Functors for Proofs and Programs[END_REF], Isabelle [START_REF] Nipkow | AVL Trees. Archive of Formal Proofs[END_REF] and ACL2 [START_REF] Ralston | ACL2-certified AVL Trees[END_REF], and similar verifications of red-black trees have been carried out [START_REF] Appel | Efficient Verified Red-Black Trees[END_REF][START_REF] Charguéraud | Program Verification Through Characteristic Formulae[END_REF][START_REF] Lammich | The Isabelle Collections Framework[END_REF][START_REF]VACID-0 solutions[END_REF]. A number of them used some kind of proof automation, though developments in proofs assistants are mostly manual. However, those implementations are not as generic as they are restricted to the usual binary search trees.

Finger trees. Finger trees were introduced by Hinze and Paterson [START_REF] Hinze | Finger Trees: A Simple General-purpose Data Structure[END_REF] as a structure general enough to derive several common data structure from it, which is exactly the same level of genericity intended by our certified implementation. However, rather few certified implementation of finger trees were carried out. Mathieu Sozeau verified the implementation of Hinze and Paterson using the Program extension of Coq [START_REF] Sozeau | Program-ing finger trees in Coq[END_REF], and another verification was carried out using Isabelle [START_REF] Nordhoff | Finger Trees. Archive of Formal Proofs[END_REF]. In both cases, proofs are mostly manual while our implementation is verified correct with nearly no human interaction. Also, excepted for Sozeau's implementation of random-access sequences, there was no attempt to check that the specification was indeed strong enough to verify the common instances.

Conclusions and Perspectives

This work presents a generic certified implementation of AVL trees and the verification of three common data structures derived from that generic core. The verification overhead is rather light, as it corresponds to less than 1400 non-empty lines of Why3 for the whole presented development, which amounts to about 550 lines of implementation. Moreover, most of this verification cost corresponds to code specification, as proofs are mostly discharged by automated provers without needing to provide hints. Details about the development size can be found in appendix.

In conclusion, we would like to assess that a high level of abstraction in programs like the one used in this development mingles very well with proof automation. This is first caused by the separation between unrelated concepts like balancing and binary search. Mixing such concepts in a single routine widen greatly the search space of automated provers, as they cannot identify that only one of those is related to a particular goal. Also, another benefit of genericity is that some routines are written and proven once, while proving directly the instances would require a lot of duplication.

We expect that such generic approaches would help to the development of certified libraries, which are a first step towards developing verified programs of consequent sizes. Overall, the proof hints corresponds to about 40 lemmas.

A Size of the development

A.2 Verification setting

The verification was carried out using the development version of Why3, which features abstract program substitution during cloning. Though not released yet at the time this paper is written, this corresponds to the version 0.84. Each goal was discharged using one of the four SMT solvers Alt-Ergo, CVC3, CVC4 or Z3. The time limit was set to 5 seconds for the vast majority of them.

  type t 'a = Empty | Node (t 'a) (D.t 'a) (t 'a) int

  type m 'a = { lis : list (D.t 'a); hgt : int } (* type of the model *) function list_model (t:t 'a) : m 'a = match t with Empty → Nil | Node l d r _ → list_model l ++ Cons d (list_model r) end function height (t:t 'a) : int = match t with Empty → 0 | Node l d r _ → let hl = height l in let hr = height r in 1 + if hl < hr then hr else hl end function m (t:t 'a) : m 'a = { lis = list_model t; hgt = height t }

  predicate c (t:t 'a) = match t with Empty → true | Node l d r h → -balancing ≤ height r -height l ≤ balancing ∧ c l ∧ c r ∧ h = height t end

  val balance (l:t 'a) (d:D.t 'a) (r:t 'a) : t 'a requires { c l ∧ c r } requires { -balancing-1 ≤ (m l).hgt -(m r).hgt ≤ balancing+1 } ensures { let hl = (m l).hgt in let hr = (m r).hgt in let he = 1 + (if hl < hr then hr else hl) in let hres = (m result).hgt in 0 ≤ he -hres ≤ 1 ∧ (-balancing ≤ hl -hr ≤ balancing → he = hres) } ensures { c result ∧ (m result).lis = (m l).lis ++ Cons d (m r).lis }

  type split 'a = { left : list 'a; middle : option 'a; right : list 'a } function rebuild (s:split 'a) : list 'a = s.left ++ option_to_list s.middle ++ s.right

  type part = Here | Left selector | Right selector val selected_part (ghost llis rlis:list (D.t 'a)) (s:selector) (l:M.t) (d:D.t 'a) (r:M.t) : part requires { selection_possible s (llis ++ Cons d rlis) } requires { l = M.sum D.measure llis ∧ r = M.sum D.measure rlis } returns { Here → selected s { left = llis; middle = Some d; right = rlis } | Left sl → selection_possible sl llis ∧ forall sp. selected sl sp ∧ rebuild sp = llis → selected s { sp with right = sp.right ++ Cons d rlis } | Right sr → selection_possible sr rlis ∧ forall sp. selected sr sp ∧ rebuild sp = rlis → selected s { sp with left = llis ++ Cons d sp.left } }

  val insert (ghost r:ref (split (D.t 'a))) (s:selector) (d:D.t 'a) (t:t 'a) : t 'a requires { selection_possible s (m t).lis ∧ c t } ensures { c result ∧ (m result).lis = !r.left ++ Cons d !r.right } ensures { selected s !r ∧ rebuild !r = (m t).lis } writes { r }

  type selector = { index : int; hole : bool } predicate selected (s:selector) (sp:split 'a) = s.index = length sp.left ∧ (s.hole ↔ sp.middle = None) predicate selection_possible (s:selector) (l:list 'a) = if s.hole then 0 ≤ s.index ≤ length l else 0 ≤ s.index < length l

  predicate selected (k:Key.t) (sp:split (D.t 'a)) = upper_bound k sp.left ∧ lower_bound k sp.right ∧ match sp.middle with None → true | Some d → eq k (key d) end -Binary search is done by mirroring comparison

  type m 'a = { func : Key.t → option (D.t 'a); card : int } function association (l:list (D.t 'a)) : Key.t → option (D.t 'a) = match l with | Nil → \k. None | Cons d q → \k. if eq k (key d) then Some d else association q k end function m (t:t 'a) : m 'a = { func = association (AVL.m t); card = length (AVL.m t); } predicate c (t:t 'a) = AVL.c t ∧ increasing (AVL.m t)

  val insert (d:D.t 'a) (t:t 'a) : t 'a requires { c t } ensures { c result } ensures { c result ∧ (if (m t).func (key d) = None then (m result).card = (m t).card + 1 else (m result).card = (m t).card) ∧ forall k:Key.t. if eq k (key d) then (m result).func k = Some d else (m result).func k = (m t).func k }

  type selector = unit predicate selected (_:unit) (sp:split (D.t 'a)) = match sp.middle with | None → false | Some d → lower_bound (key d) sp.left ∧ lower_bound (key d) sp.right end predicate selection_possible (_:unit) (l:list (D.t 'a)) = l = Nil

  val remove_min (ghost r:ref (D.t 'a)) (t:t 'a) : t 'a requires { c t ∧ (m t).card ≥ 1 } writes { r } ensures { c result ∧ (m t).card = (m result).card + 1 ∧ (m t).bag !r = (m result).bag !r + 1 ∧ (forall d. d = !r → (m t).bag d = (m result).bag d) ∧ (forall d. (m t).bag d > 0 → le (key !r) (key d)) }

  let rec insert (ghost r:ref (split (D.t 'a))) (s:selector) (d:D.t 'a) (t:t 'a) : t 'a requires { selection_possible s (m t).lis ∧ c t } ensures { c result ∧ (m result).lis = !r.left ++ Cons d !r.right } ensures { selected s !r ∧ rebuild !r = (m t).lis } writes { r } (* extra postcondition needed to prove the recursion. *) ensures { 1 ≥ (m result).hgt -(m t).hgt ≥ 0 } | ANode tl td tr _ _ → match selected_part (m tl).lis (m tr).lis s (total tl) td (total tr) with | Left sl → let res = get r sl tl in r := { !r with right = (!r).right ++ Cons td (m tr).lis }; res | Right sr → let res = get r sr tr in r := { !r with left = (m tl).lis ++ Cons td (!r).left }; res | Here → r := { left = (m tl).lis; middle = Some td; right = (m tr).lis }; Some td end end

  Code for insertion, lookup and deletionNote: the expensive list-manipulating code is ghost, and as such is not executed.

	Prover discharged goals average time maximum time
	Alt-Ergo	471	0.29s	6.76s
	CVC3	283	0.29s	3.01s
	CVC4	66	0.68s	7.39s
	Z3	11	1.37s	4.84s
	A.3