Member, IEEE, Zabih Ghassemlooy Senior Member, IEEE, Stanislav Zvanovec, Senior Member IEEE Elizabeth Eso
email: elizabeth.eso@northumbria.ac.uk

Zabih Ghassemlooy
email: z.ghassemlooy@northumbria.ac.uk

Stanislav Zvanovec
email: xzvanove@fel.cvut.cz.

Juna Sathian
email: juna.sathian@northumbria.ac.uk

Asghar Gholami
email: gholami@cc.iut.ac.ir

Fundamental Analysis of Vehicular Light Communications and the Mitigation of Sunlight Noise

Keywords: vehicular visible light communications, fundamental analysis, intelligent transport systems, infrared, sunlight noise I

de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

supports several applications such as emergency braking warning and intersection collision warnings. However, some doubts still exist on the capability of DSRC in meeting the low latency and high reliability requirements in ITS considering both the network outages and security issues [START_REF] Memedi | Impact of Vehicle Type and Headlight Characteristics on Vehicular VLC Performance[END_REF]. Consequently, considering the aforementioned issues, optical wireless communications (OWC) have emerged as an attractive and complementary technology in vehicular communications. It is interesting to note that, the OWC technology employing light emitting diodes (LEDs) gives rise to a smaller collision domain, which results in reduced packet losses due to interference, compared with the RF wireless systems [START_REF] Memedi | Impact of Vehicle Type and Headlight Characteristics on Vehicular VLC Performance[END_REF]. Furthermore, the directionality of OWC increases the security of the communication networks, thus reducing the possibility of eavesdropping drastically.

The expanding multi-media-based services is the main driving force of the fifth generation (5G) and the emerging sixth generation (6G) and beyond wireless networks, which will be based on multiple technologies to ensure high quality of services [START_REF] Zhou | Service-aware 6G: An intelligent and open network based on the convergence of communication, computing and caching[END_REF][START_REF] Zhou | Fog Computing Enabled Future Mobile Communication Networks: A Convergence of Communication and Computing[END_REF]. OWC is envisaged to be part of 5G/6G and beyond wireless networks for use in application areas where RF-based technologies cannot be used due to insufficient bandwidth and other issues such as security, susceptibility to electromagnetic interference, etc. Several novel concepts on the use of OWC in 6G have been reported in [START_REF] Katz | Opportunities and Challenges for Visible Light Communications in 6G[END_REF], including (i) hybrid radio-optical wireless networks, where wireless nodes or devices are equipped with both RF and optical interfaces; and (ii) through-the-tissue optical communications, where very short ranges are considered to provide a highly secure link for intra-body and to/from body transmission. Note, the unique features of OWC that makes it an attractive technology for 5G/6G includes a large unlicensed spectrum, high security, high safety, lower power consumption, simplicity in implementation, low costs, and not susceptible to RF-induced interference. Consequently, the coexistence of the OWC and RF technologies can efficiently solve most of the limitations of the individual RF and OWC links [START_REF] Chowdhury | The Role of Optical Wireless Communication Technologies in 5G/6G and IoT Solutions: Prospects, Directions, and Challenges[END_REF]. With the ever-increasing demand for internet of things, 5G is not guaranteed to meet up all the requirements of new services in the future [START_REF] Zhou | Service-aware 6G: An intelligent and open network based on the convergence of communication, computing and caching[END_REF], hence a hybrid/heterogenous system i.e., OWC with RF, enables 5G to be used in areas where RF cannot be utilised.

A growing number of research works on visible vehicular light communications (V-VeLC) have been reported in the literature. In [START_REF] Luo | Performance analysis of a car-to-car visible light communication system[END_REF], an analytical model for the bit error rate (BER) performance as a function of the communication distance for V-VeLC under different communication geometries and using a headlight (HL) beam pattern model was reported. It was shown that, (i) there were sharp degradations in the BER performance distribution to the left-hand side in the vertical plane, which is due to the asymmetric beam pattern of the low beam HL; and (ii) an increase in the achievable transmission link span provided the optical receiver's (Rx's) i.e., the photodiode (PD) and HLs heights were about 0-0.2 and 0.66 m, respectively. In [START_REF] Elamassie | Effect of Fog and Rain on the Performance of Vehicular Visible Light Communications[END_REF], a comprehensive channel modelling to evaluate the performance of V-VeLC employing the high beam HL as the transmitter (Tx) under the weather conditions (rain and fog) was carried out. Using advanced ray tracing a path loss model in terms of transmission range was developed, showing the link span dropping from 72 to 26 m in the presence of heavy fog at a target BER of 10 -6 . A 2×2 multiple-input multipleoutput channel under Sunlight using a market-weighted HL pattern source as the Tx was studied in [START_REF] Farahneh | Performance analysis of adaptive OFDM modulation scheme in VLC vehicular communication network in realistic noise environment[END_REF]. It was shown that, direct current biased optical orthogonal frequency division multiplexing (DCO-OFDM) offered higher data rates compared with the asymmetrically clipped optical OFDM (ACO-OFDM). with lower BER performance.

It is important to note that, most works reported on V-VeLC including the aforementioned references have considered highor low-beam HLs, which are usually on during the night or under reduced visibility conditions (i.e., rain or fog). For the HLs, the transmit power PT levels during daytime are relatively very low compared with the high-and low-beam lights used for road illumination. In [START_REF] Tseng | Characterizing link asymmetry in vehicle-to-vehicle Visible Light Communications[END_REF], an extensive optical radiation pattern measurement of a single HL and TL was carried out. Several vehicle mobility traces with two-dimensional locations were also collected. Both data were combined to perform analytical study and to further obtain experimental distributions of the received power for HL-and TL-based Txs. Consequently, the issue of link asymmetry due to the significant differences in the radiation characteristics and PT between the HL and the TL was identified. It was shown that, in 80% of the cases the received power for the link using the HL was at least 22 dB more than that of the TL-based Tx. To address the link asymmetry problem in V-VeLC systems, the paper proposed that a new system (or a protocol) design needs to be developed to improve the data throughput. In [START_REF] Memedi | Impact of Realistic Light Radiation Pattern on Vehicular Visible Light Communication[END_REF], the impact of vehicles' HL and TL illumination patterns on the communications performance between vehicles travelling on the same-and different-lanes was studied by developing a novel V-VeLC simulation model based on accurate empirical data measurements. Performance evaluation of V-VeLC was carried out based on the developed model, where the impact of the angle of incidence was analyzed based on the received signal strength, signal to noise ratio (SNR), and packet delivery ratio metrics. The authors reported that, using the TL, communications with vehicles on the adjacent lanes were possible only over a transmission range up to 10 m. From the foregoing, it is apparent that a robust Tx design is needed, which meets the requirements of the vehicular environment in terms of the communications range and the coverage area.

Some studies reported on infrared vehicular light communications (IR-VeLC) are also discussed as follows; In [START_REF] Turan | Vehicular Visible Light Communications[END_REF], a secure light communications protocol known as SecVLC, which is a cryptographic key generation/ management system, using the infrared (IR) and visible lights for link's security and data communications, respectively was proposed. In [START_REF] Fujii | Experimental research on intervehicle communication using infrared rays[END_REF], a prototype vehicular light communications (VeLC) system with the IR-VeLC Tx mounted on the roof of a vehicle was reported with the focus being on the communications protocol for relaying transmitted data between vehicles. In [START_REF] Hossain | Vehicle to Vehicle Communication Using RF and IR Technology, 2nd International Conference on Electrical & Electronic Engineering (ICEEE)[END_REF], a RF and IR vehicle to vehicle communications system prototype for sending warning signals was demonstrated. However, none of the above works considered and analyzed the use of IR transmission for improving the link's robustness to the noise or increasing the communications transmission range considering realistic intervehicle distances.

Note that, in V-VeLC system the Sunlight induced noise is the major problem during the daytime, where the illumination level can be as much as 10 mW/cm 2 compared with uW/cm 2 for the intensity-modulated HL and TL [START_REF] Căilean | Current Challenges for Visible Light Communications Usage in Vehicle Applications: A Survey[END_REF]. This high-level of ambient light can lead to the saturated optical Rx. Note that, most works reported on V-VeLC have not considered the effect of Sunlight noise. Among the few reports that have considered the impact of Sunlight noise includes [START_REF] Islim | The Impact of Solar Irradiance on Visible Light Communications[END_REF], where the impact of solar irradiance on VLC systems was investigated in terms of the BER, SNR degradation, and data rates. Results showed that, using an optical bandpass blue filter the link performance greatly improved over a short transmission span of up to 3 m. In [START_REF] Farahneh | Differential Receiver as a Denoising Scheme to Improve the Performance of V2V-VLC Systems[END_REF] the effects of Sunlight irradiance and other external light sources on V-VeLC systems were investigated with regards to BER, data rates, and SNR over different months of the year, with and without an optical blue filter. Results obtained demonstrated a significant performance improvement in the achievable data rates and the average BER, e.g., in the month of January the average BER improved from 2×10 -3 to ~3×10 -5 using an optical blue filter. In addition, different noise cancellation methods such as wavelet-based signal processing and differential Rx-based hardware were proposed. However, due to the complexity of the processing, no real-time denoising has been demonstrated successful yet [START_REF] Farahneh | Performance analysis of adaptive OFDM modulation scheme in VLC vehicular communication network in realistic noise environment[END_REF]. In [START_REF] Farahneh | Performance analysis of adaptive OFDM modulation scheme in VLC vehicular communication network in realistic noise environment[END_REF], the effect of Sunlight noise on the performance of V-VeLC at a low speed of 30 km/h was considered. Note that, the effect of Sunlight noise becomes more significant as the link span increases, considering that the received power levels decrease with the increasing transmission distance. Moreover, to increase the transmission distance in V-VeLC, the use of converging lenses has been widely adopted. However, the higher the focal length f of the lenses used at the Rx the lower the angular field of view (AFOV) of the Rx, thereby reducing vehicle's maneuverability. Consequently, in this work we have considered practical VeLC channel, Tx, PD, lenses, and filter parameters. In addition, we have carried out BER performance analysis by considering a wide range of vehicle speeds and the Sunlight induced background noise (obtained from solar irradiance measurements carried out in the city of Newcastle (N 54 o 59'44'' W 1 o 39'52'')).

It is noteworthy that, most works reported on V-VeLC are based on using a single light module, which may narrow down the conclusions drawn from the results. Therefore, in this work we characterize four TLs from different vehicles by measuring their radiation patterns and PT. We also perform a link power budget analysis to determine the feasibility of V-VeLC using these TLs as the Txs for a range of TL irradiance angles with respect to the vehicle's speeds.

The main contributions of this work are:

▪ We present a channel model for VeLC where the Tx's specific radiant intensity model can be incorporated other than Lambertian radiant intensity model.

• We provide insights on the required horizontal and vertical AFOVs of the Rx for VeLC for the first time to the authors best knowledge.

• We show AFOV obtainable based on varying the PD sizes with varying f of lens and provide insights on the Tx's coverage diameter.

• We carry out optical characterization and performance evaluation of different vehicle TLs as Txs for VeLC systems.

• We propose a novel robust IR-VeLC system considering practical and realistic parameters.

• We carry out performance analysis of the proposed IR-VeLC with realistic Sunlight noise from empirical measurements.

The rest of the paper is organized as follows. In Section II the VeLC system is described while the configuration analysis is presented in Section III. Performance evaluation of V-VeLC system using TLs as Txs is given in Section IV. Section V describes the noise and BER analysis. The performance analysis of the proposed novel IR-VeLC is presented in Section VI. Finally, conclusions are given in Section VII.

II. THE VELC SYSTEM

Figure 1(a)-(c) shows the composition of a typical VeLC system, which consists of the TL-based Tx (Vehicle 1) and the PD-based Rx (Vehicle 2). Note, for illustration purposes only a single TL is used. Including the second TL will have almost the same geometrical configuration, which results in the increased SNR at the Rx. Note, the Tx's positions with respect to the Rx and their beam profiles as well as the Rx's AFOV are very crucial in VeLC and will affect the link performance. For the line of sight (LOS) VeLC (Fig. 1(a)-(c)), the channel DC gain, which is the ratio of the received signal power at the Rx to the transmit power, can be expressed as:

𝐻 LOS = {
𝐴 PD 𝑇 𝑠 (𝜑 hor, 𝜑 ver )𝑔(𝜑 hor, 𝜑 ver )𝑅 Tx (𝜃 hor, 𝜃 ver ) 𝐿 𝑆 2 , 0 ≤ 𝜑 hor ≤ Ø hor and 0 ≤ 𝜑 ver ≤ Ø ver 0, 𝜑 hor > Ø hor or 𝜑 ver > Ø ver [START_REF] Eso | Experimental Demonstration of Vehicle to Roadside Infrastructure Visible Light Communications[END_REF] where 𝐴 PD is the active area of the PD, 𝜑 hor and 𝜑 ver are the horizontal and vertical incidence angles, respectively, 𝑅 Tx (𝜃 hor, 𝜃 ver ) is the radiation pattern (normalized beam profile) of the Tx at horizontal and vertical irradiance angles 𝜃 hor and 𝜃 ver , respectively, Ø hor and Ø ver denotes the horizontal and vertical AFOV semi angle of the Rx, 𝐿 𝑆 represents the link span, 𝑇 𝑠 (𝜑 hor, 𝜑 ver ) and 𝑔(𝜑 hor, 𝜑 ver ) are the gains of the optical filter (OF) and optical concentrator (OC), respectively. Note that, using (1) the Tx's specific radiation pattern can be incorporated, which may not be symmetrical as in Lambertian radiant intensity model. The gain of a non-imaging OC (NIOC) can be expressed as 𝐴 coll 𝐴 PD ⁄ [START_REF] Ghassemlooy | Visible Light Communications: Theory and Applications[END_REF], where 𝐴 coll is the collection area of the NIOC.

Figure 2 shows the system composition of an IR-VeLC system using an array of IR-LED as the light source at the Tx side. The OOK data stream is used for the intensity modulation of the Tx for transmission over the free space channel. At the Rx side, an OC, a narrow band optical band-pass filter (i.e., 810 -890 nm) and an optical Rx are used to the regenerated electrical signal. For the LOS link, the received signal is given by [START_REF] Kahn | Wireless infrared communications[END_REF]:

𝑦(𝑡) = ℛ𝑥(𝑡) ⊗ ℎ(𝑡) + 𝑛(𝑡), (2)
where R is the responsivity of the PD, x(t) is the modulated light signal at the Tx, h(t) is the channel impulse response while n(t) denotes the additive white Gaussian noise including the Sunlight induced shot noise, which is the dominant noise source in VeLC during the daytime, the signal and dark current related shot noise sources and the thermal noise.

III. VELC CONFIGURATION ANALYSIS

A. Analysis of horizontal/vertical semi-AFOV for VeLC with imaging OC (IOC)

Using a convergent lens (i.e., IOC) at the Rx, as in a camera, an image of the Tx is captured on the PD-based sensor provided the Tx is within the Rx's AFOV. Note that, NIOCs do not produce an image of the Tx as do IOCs. First, we analyse the required horizontal semi-AFOVs (HS-AFOVs) for the Rxs 1 and 2 based on the worst-case scenario, where vehicles are located at the other sides of the lane, see Fig. To obtain the required HS-AFOV between two vehicles travelling on the same lane, therefore we need to consider both the lane and vehicles' widths as well as the positions of the Rx and the Tx. Consequently, the required HS-AFOV for the Rx can be expressed as in ( 3)-( 6) where 𝑤 RL is the width of the road lane, 𝐿 s-hor denotes the horizontal distance between the Tx and the Rx, 𝑤 Tx , and 𝑤 Rx , are the spacing between the Txs and the Rxs and, 𝑤 v-Tx and 𝑤 v-Rx are width of the vehicles, respectively and 𝑙 Tx denotes the length of the Txs (see Figs. 1 and3). Note that, for the cases where one of the vehicles may move outside the lane, we replace 𝑤 RL by 𝑤 RL + 𝑥 in (3)-( 6), where 𝑥 represents the deviation from the edge of the lane. Furthermore, (3)-( 6) could be applied to vehicles on different lanes where 𝑤 RL becomes 2𝑤 RL or 3𝑤 RL for scenarios with one of the vehicles being on the next or the next two lanes, respectively.

Tx1

Tx2

Rx2 Rx1 𝐿 s-hor ).

(

) (4) 3
The required vertical semi-AFOV (VS-AFOV) for the case shown in Fig. 1(a) is given as:

𝜑 ver = arctan ( 𝐻 𝐿 s-hor ), (7)
where the offset between the Tx's and the Rx's vertical heights is 𝐻 = |𝐻 Tx -𝐻 Rx |. The required HS-AFOV and VS-AFOV as a function of the link span for VeLC are depicted in Fig. 4, which is generated using (3)-( 7) and the parameters given in Table I. From Fig. 4 it can be observed that, HS-AFOV exponentially drops with the link span. For example, for the Rx2 the required HS-AFOV increases by ~ 5 times as the link span decreased from 10 to 2 m. For the Rx1, the required HS-AFOV is lesser than the Rx2 due to it being closer to the Txs. Moreover, for VS-AFOV an exponential profile is also displayed with higher values for larger 𝐻 below the link span of 20 m. Note that, increasing the vertical offset between the Tx and the Rx outside the vertical AFOV of the Rx will lead to increasing the vertical AFOV in order to capture the Tx while the horizontal AFOV requires no adjustment and vice versa.

B. Semi-AFOV based on PD's size and the lens focal length

Using a convergent lens (i.e., IOC) to focus light onto the PD to increase the received optical power density results in reduced Rx's semi-AFOV, which needs investigating in terms of the PD's size and the 𝑓 of lens, to meet the required semi-AFOV in vehicular communications, see Fig. 5. The semi-AFOV in terms of 𝑓 and the PD's dimensions 𝐷 PD can be expressed as:

Ø S-AFOV = arctan ( 𝐷 PD 2𝑓 ), Ø S-AFOV = { Ø hor , 𝐷 PD = 𝑤 PD , Ø ver , 𝐷 PD = ℎ PD , Ø diag , 𝐷 PD = √ℎ PD 2 + 𝑤 PD 2 , (8) (9)
where ℎ PD and 𝑤 PD denotes the height and width of the PD and Ø hor , Ø ver and Ø diag is the horizontal, vertical and diagonal semi-AFOVs of the Rx, respectively. Fig. 6 shows Ø hor or Ø ver as a function of the PD's surface area (where 𝑤 PD = ℎ PD ) for a range of 𝑓. It can be seen that, using a convergent lens at the PD, Ø hor or Ø ver decreases with 𝑓 and increases (logarithmic) with the PD's surface area.

C. Analysis of Tx's field of view (coverage profile)

Figure 7 illustrates the Txs' coverage profile whereby 𝐿 1 depicts the horizontal distance from the Txs to the start of the overlapping light area between Txs 1 and 2, which can be expressed as:

𝐿 1 = 𝑤 Tx (tan𝜃1 2 ⁄ -in + tan𝜃1 2 ⁄ -out ⁄ ), (10)
where 𝜃1 2 ⁄ -in and 𝜃1 2 ⁄ -out are inner and outer half power angles of the Tx's beam, respectively, see Fig. 7. Note that, 𝜃1 2 ⁄ -in and 𝜃1 2 ⁄ -out of each Tx is the angle between the peak and the point on one side of the beam axis (left or right) where the received power is half the maximum. 𝐿 2 is the beam length of a single Tx and 𝐿 FOV is the coverage length of both Txs beyond 𝐿 1 , which can be expressed as: 8, which shows a logarithmic increase of the Tx's half power angle with 𝐿 FOV reaching saturation points at ~220 and ~370 m for 𝐿 𝑠-hor of 30 and 50 m, respectively. Note, the Tx's half angle decreases with the increasing link span.

𝐿 2 = 𝐿 𝑠-hor (tan𝜃1 2 ⁄ -in + tan𝜃1 2 ⁄ -out ), (11)
𝐿 FOV = 𝑤 Tx + 𝐿 𝑠-hor (tan𝜃1 2 ⁄ -in + tan𝜃1 2 ⁄ -out ). (12)

IV. PERFORMANCE EVALUATION OF V-VELC WITH TLS-

BASED TXS Comprehensive performance analysis of the use of HLs with the given real beam patterns of different vehicle brands for data transmission was reported in [START_REF] Luo | Performance analysis of a car-to-car visible light communication system[END_REF]. The results showed that, the received power level increased with the decreasing Rx's heights from the ground due to the HLs being designed for road illumination points down-ward on the road surface as illustrated in Fig. 9. Consequently, this imposes the upper bound on the

Short link span

Long link span maximum transmission link span due to the angular inclination of the light rays on the road surface and its asymmetrical beam pattern. Most works reported on the use of TLs as Txs, are based on investigating the use of a single TL, which only outlines half the story, therefore, narrowing the conclusions drawn from the results obtained for the specific vehicle type/light model. No works have been reported on V-VeLC with different TL units. Therefore, to carry out performance evaluation of V-VeLC using TLs for data transmission we characterise four LEDbased vehicle TLs for different vehicle modules.

A. Radiation patterns of the TLs

First, we need to investigate the radiation patterns of the TLs, which defines the spatial intensity distribution of the emitted light from the TLs, which is important for the analysis of signal distribution and the coverage area. For this we have used a digital optical power meter (Thorlabs PM100D with a PD power sensor S120VC) to measure the received power levels over a fixed transmission distance of 1 m for a range of irradiance angle (i.

B. Link power budget analysis

As part of the system design and implementation, we have carried out the link power budget analysis for V-VeLC using the four TLs units. For this, it is important to know the allowed inter-vehicle distances 𝐷 𝑣 for safe driving. Typically, a "two seconds" rule is recommended for 𝐷 𝑣 , whereby a driver maintains a minimum of two seconds behind the vehicle in front under the good weather condition, which is doubled to four seconds in bad weather conditions [START_REF]The two-second rule[END_REF] as depicted in Fig. 11. For a given 𝑃 𝑇 , the receiver power is given as: 𝑃 𝑟 (dBm) = 𝑃 𝑇 (dBm) + 𝐻 LOS (dB) -𝐿 sm (dB), [START_REF] Fujii | Experimental research on intervehicle communication using infrared rays[END_REF] where 𝐿 sm is the link safety margin and 𝐻 LOS is the channel DC gain for the LOS, which is given by: 𝐻 LOS (dB) = 10log 10 (𝐴 PD 𝑇 𝑠 (𝜑 hor, 𝜑 ver )𝑔(𝜑 hor, 𝜑 ver )𝑅 Tx (𝜃 hor, 𝜃 ver )/ 𝐷 𝑣 2 ),

Table III shows the key parameters used for the link power budget analysis. Figure 12 IV. Note, these achievable speeds are far lower than the typical recommended vehicle's speed limits, e.g., for cars, motorcycle, vans and buses a driving speed of 30, 60, 70 and 70 mph is approved in built-up areas, single carriage ways, dual carriage ways and motorways (mph), respectively [START_REF]Speed limits[END_REF]. Figure 13 illustrate the predicted required PT against the driving speed for cases with and without the OC at the Rx. Note, the required PT drops by 5.3, 8.1 and 11.2 dB when a NIOC with the diameter 𝑑 of 25.4, 35.0 and 50.0 mm are used at the PD, respectively.

V. NOISE AND BER ANALYSIS

A. Ambient noise

In VeLC, there are two main ambient light induced noise sources of (i) the streetlights (at night), advertising boards and other vehicle lights; and (ii) the background solar radiation (Sunlight), which is the dominant noise source. Note that, the solar irradiance 𝑃 solar (𝜆) varies by the time of the day and latitude, i.e., the position of the sun. In addition, its effect on the Fig. 12: The horizontal irradiance angle as a function of the received power and driving speed for different TLs performance of VeLC system will depend on the direction and orientation of the Rx. The photocurrent generated at the PD due to 𝑃 solar (𝜆) is given as:

𝐼 solar = 𝐴 PD 𝑔(𝜑 sun )cos(𝜑 sun )𝐺 PD ∫ 𝑃 solar (𝜆) 𝜆 𝑛 𝜆 1 𝑇 𝑓 (𝜆)ℛ(𝜆)𝑑𝜆, (15)
where 𝐴 PD and 𝐺 PD are the active area and gain of the PD, respectively, 𝜑 sun is the difference in the orientation angle between that of the measured 𝑃 solar (𝜆) and the PD, 𝜆 1 and 𝜆 𝑛 are the integration limits, i.e., the wavelength band, which are 405-690 nm and 810-890 nm for visible and IR-based systems, respectively. The gain of the OC is denoted as 𝑔(𝜑 sun ), ℛ(𝜆) is the responsivity of the PD and 𝑇 𝑓 (𝜆) is the optical band pass filter's transmittance. Note that, the daytime background radiation-induced shot noise is the dominant noise source in VeLC, which can be expressed as [START_REF] Komine | Fundamental analysis for visible-light communication system using LED lights[END_REF][START_REF] Hui | Introduction to Fiber-Optic Communication[END_REF]:

𝜎 bgr 2 = 2𝑞 𝑒 𝐼 solar 𝐵, (16)
where 𝑞 𝑒 is the electron charge and 𝐵 is the system bandwidth.

B. Thermal and shot noise sources

Thermal noise is generated due to the random motion of charge carriers [START_REF] Farahneh | Performance analysis of adaptive OFDM modulation scheme in VLC vehicular communication network in realistic noise environment[END_REF] and its variance is given as [START_REF] Hui | Introduction to Fiber-Optic Communication[END_REF][START_REF] Haddad | Channel characterization for optical extra-WBAN links considering local and global user mobility[END_REF]:

𝜎 thermal 2 = 4𝑘𝑇 𝐾 𝐵 𝑅 𝐿 , (17)
where 𝑘 is the Boltzmann's constant, 𝑇 𝐾 is the absolute temperature in Kelvin and 𝑅 𝐿 is the load resistance.

Note that, the photodetection process, which is discrete in nature, results in the signal-dependent shot noise at the PD [START_REF] Paudel | Modelling and Analysis of Free Space Optical Link for Ground-to-Train Communications[END_REF][START_REF] Hui | Fiber Optic Measurement Techniques[END_REF], with the variance given as [START_REF] Hui | Fiber Optic Measurement Techniques[END_REF]:

𝜎 shot-rs 2 = 2𝑞 𝑒 ℛ(𝜆)𝑃 𝑟 𝐵, (18)
where 𝑃 𝑟 is the average received signal power (i.e. desired signal). In addition, the PD's dark current noise variance is given as [START_REF] Hui | Introduction to Fiber-Optic Communication[END_REF]:

𝜎 dk 2 = 2𝑞 𝑒 𝐼 dk 𝐵, (19)
where 𝐼 dk is the dark current.

The total noise variance is then given as:

𝜎 𝑇 2 = 𝜎 bgr 2 + 𝜎 thermal 2 + 𝜎 shot-rs 2 + 𝜎 dk 2 . (20)

C. BER

In this work, we have adopted the intensity modulation direct detection scheme with OOK and a PD (Hamamatsu S6968) as the Rx. Once the relative positions of the Tx and the Rx are ascertained, the minimum received optical power (i.e., considering a single Tx) and the noise variances of thermal noise, ambient, signal and dark current shot noises are obtained using ( 13), ( 15)- [START_REF] Kahn | Wireless infrared communications[END_REF]. Note that, the systems bandwidth is primarily determined by the low pass filter characteristics of the Rx, which is 𝐵 = 𝑅 𝑏 /2, where 𝑅 𝑏 is the data rate [START_REF] Haddad | Channel characterization for optical extra-WBAN links considering local and global user mobility[END_REF]. Consequently, for the additive white Gaussian noise channel, the SNR at the Rx is given by [START_REF] Kahn | Wireless infrared communications[END_REF]:

SNR = (ℛ(𝜆)𝑃 𝑟 ) 2 𝜎 𝑇 2 . (21)
Thus, the BER is then given as [START_REF] Kahn | Wireless infrared communications[END_REF]:

BER = 𝑄(√SNR), (22)
where 𝑄(𝑥) is the 𝑄-function used for the calculation of the tail probability of the standard Gaussian distribution given by [START_REF] Kahn | Wireless infrared communications[END_REF]:

𝑄(𝑥) = 1 √2𝜋 ∫ 𝑒 -𝑦 2 2 𝑑𝑦 ∞ 𝑥 . (23)

VI. PERFORMANCE ANALYSIS OF IR-VELC

Here, we have used an array of IR-LED (Osram SFH 4715AS) with a symmetrical light pattern and no angular inclination towards the road surface for the vehicle IR-light Txs in order to meet the driving speed (i.e., typical inter-vehicle distances) requirements. First, we show the received power per Tx over driving speeds for a range of 𝑑 by numerical simulations using [START_REF] Fujii | Experimental research on intervehicle communication using infrared rays[END_REF] and [START_REF] Hossain | Vehicle to Vehicle Communication Using RF and IR Technology, 2nd International Conference on Electrical & Electronic Engineering (ICEEE)[END_REF]. Note, (i) only LOS is considered since the Tx is a symmetrical light source with no angular inclination towards the road, thus with no significant reflections from the road surface; and (ii) the transmit optical power level must meet the IEC 62471/2006 emission limits for eye safety, which specifies emission limit of 100 W/m 2 [START_REF]Photobiological safety of lamps and lamp systems. s.l[END_REF], whereas the proposed system in this work has a maximum of 5.92 W/m 2 (for the two front/rear Txs) at 1 m distance from the Txs. The key system parameters adopted in this work are provided in Table V.

It is important to note that, the greatest challenge in VeLC systems is to ensure link robustness under strong ambient light. Consequently, we propose an IR-VeLC system to mitigate this challenge for the following reasons: (i) Sunlight irradiance in the IR band is much lower than the visible band, which leads to improved signal to noise ratio performance. For example, from Fig. 14 (data source from [START_REF]CSIM Solar Spectral Irradiance, Time series, Lasp Interactive Solar Irradiance Datacentre[END_REF]), in the IR region at the wavelength of 850 nm, the solar irradiance is less than 50 % compare to the wavelength of 480 nm in the visible light region; and (ii) the incorporation of IR-LEDs will help to meet the required transmit power level (within safety limits) needed for longer distance transmissions, where the TLs would not be able to offer, see Section IV. Note, the high or low beam HLs, which have higher transmit powers than TLs are only used at night or when the visibility is low due to fog, heavy rain, snow, etc., thus imposing limitation in V-VeLC systems. The proposed work overcomes these issues and limitations by introducing the use of IR-LEDs in addition to HLs and TLs, to ensure link availability at all times and can come on when data is being transmitted unnoticeable to the human eyes. In addition, there are other merits of IR-LEDs such as (i) the electrical-to-optical conversion efficiency of IR-LEDs are higher than the visible blue LED-based white light sources [START_REF] Mana | Experiments in Non-Line-of-Sight Li-Fi Channels[END_REF]; and (ii) the 3 dB bandwidth of IR-LEDs are higher than the white LEDs, which is well known [START_REF] Mana | Experiments in Non-Line-of-Sight Li-Fi Channels[END_REF]. The plots of the received power against the driving speed for the case with and without an OC at the Rx is depicted in Fig. 15. It can be seen that, the received power increases and decreases with 𝑑 and the driving speed, respectively. For example, at 𝑃 𝑟 of -36 dBm without an OC and with a NIOC of 𝑑 = 25.4 mm, the driving speeds are 60 and ~100 mph, respectively. Note that, the received power increases by 5.3, 8.1 and 11.2 dB using a NIOC with 𝑑 of 25.4, 35.0 and 50.0 mm, respectively. The predicted BER performance as a function of the driving speed for the proposed IR-VeLC system using IR-LEDs and BMW TL (chosen because it has the highest 𝑃 𝑇 among the four TLs characterized) for a range of data rates is shown in Fig. 16 via numerical simulations using ( 15)-( 23). Here we have considered 𝑃 solar of 413.77 W/m 2 , NIOC with 𝑑 of 25.4 mm and a narrow bandpass filter (Thorlabs FB850-40) at the Rx. Note, a solar power meter (ISO-TECH ISM410) was used to measure the solar irradiances (wavelength range of 400-1100 nm) at the various positions with respect to the Sun. 𝑃 solar (𝜆) for the direction with the highest average value (measured at the city of Newcastle, UK, N 54 o 59'44'' W 1 o 39'52'') is used in our simulations. Note, the Rx is located on the vehicle pointing towards the vehicles on the road with no horizontal tilting angle.

As can be observed from Fig. 16, BMW TL does not meet typical driving speeds limits (i.e., inter-vehicle link spans) due to low PT. Note, only driving speeds of 7, ~6 and 5 mph (translating to a 𝐿 𝑆 of 6.3, 5.4 and 4.5 m, respectively) are achievable at 𝑅 𝑏 of 2, 6 and 10 Mbps, respectively, at the FEC BER limit of 3.8 ×10 -3 . However, the proposed system with the IR-LEDs offers driving speeds of >100, 80 and 70 mph (translating to a 𝐿 𝑆 >89, 72 and 63 m) at 𝑅 𝑏 of 2, 6 and 10 Mbps, respectively under the same conditions and a high ambient light level. Note, a sharp increase in the BER with respect to the driving speed up to ~ 60, ~70 and ~90 mph for the links with 𝑅 𝑏 of 10, 6 and 2 Mbps, respectively. For example, at 𝑅 𝑏 of 10 Mbps the BER values are 8.0×10 -8 and 3.8×10 -3 for the driving speed of 50 and ~70 mph, respectively. This is because, the received power level reduced by ~50 % (i.e., from 1.2 µW (-29.2 dBm) to 0.6 µW (-32.2 dBm)).

Moreover, to demonstrate the impact of the noise on the link performance we investigate the BER for BMW TL and the proposed IR-VeLC system by considering all noise sources as in [START_REF]The two-second rule[END_REF] without the (i) Sunlight noise 𝜎 bgr 2 ; and (ii) signal dependent shot noise 𝜎 shot-rs 2 , see Fig. 16. For example, for the proposed IR-VeLC system, the BER at a driving speed of 90 mph without and with 𝜎 bgr 2 are 5.5 × 10 -9 and 5.3 ×10 -2 , respectively. For the link using BMW TL, the BER at the speed of 8 mph without and with 𝜎 bgr 2 are 1.3 ×10 -9 and 1.7 ×10 -1 , respectively. As shown in Fig. 16, 𝜎 shot-rs 2 has negligible impact on the BER performance compared with 𝜎 bgr 2 .

VII. CONCLUSIONS

We carried out a performance evaluation study on the use of different vehicle TLs as Txs for V-VeLC systems. The results obtained showed that, the radiation characteristics and PT are not the same for different vehicle TLs, thus impacting the coverage area, signal distribution and the communication distance, which are key factors in the practical deployment of VeLC as part of ITS. Consequently, based on the obtained results we proposed the incorporation of IR-LEDs in vehicle HLs and TLs to meet the typical communication link spans in vehicular environments. We showed that, the proposed IR-VeLC system offers improved performance particularly under Sunlight compared with the visible lights-based TLs. We showed that, at the target FEC BER limit of 3.8 ×10 -3 , transmission distances up to 63, 72 and >89 m were achieved by the proposed IR-VeLC compared with 4.5, 5.4 and 6.3 m for BMW vehicle-based TL at data rates of 10, 6 and 2 Mbps, respectively. Furthermore, the proposed scheme deals with the link asymmetry highlighted in [START_REF] Tseng | Characterizing link asymmetry in vehicle-to-vehicle Visible Light Communications[END_REF] in section I, since both the front and rear vehicle's Txs will have the same PT and radiation characteristics. Moreover, we analyzed the maximum HS-AFOV and VS-AFOV required for vehicles traveling on the same lanes to establish data communication, based on the road lane width and the positions of the Txs and Rxs on the vehicles (with an imaging-based OC at the Rx).

  3. Note that, for the Rxs 1 and 2 to capture a single Tx and or two Txs the required HS-AFOV are 𝜑 12 , 𝜑 22 , 𝜑 11 , 𝜑 21 , respectively.

Fig. 1 :Fig. 3 :

 13 Fig. 1: VeLC configuration: (a) side view, (b) top view for perfect alignment scenario, and (c) top view with horizontal Tx and Rx misalignment (offset)

Fig. 4 .

 4 Fig. 4. The required HS-AFOV and VS-AFOV of Rx versus the 𝐿 s-hor for two vehicles on the same lane

Fig. 5 :

 5 Fig. 5: Relationship between 𝑓, semi-AFOV and the PD size

Fig. 7 : 2 ⁄ -in and 𝜃1 2 ⁄ 2 ⁄ -in + tan𝜃1 2 ⁄ 2 ⁄ -in = 𝜃1 2 ⁄

 7222222 Fig. 7: Tx field of view (coverage diameter)

Fig. 8 :

 8 Fig. 8: Half power angle of Tx versus 𝐿 FOV for a range of Ls-hor

Fig. 9 :

 9 Fig. 9: V-VeLC links using HLs as the Txs

2 ⁄ -in and 𝜃1 2 ⁄

 22 e., -90 o (left) to +90 o (right)) of the TLs. For comparison, we have used TLs from four popular vehicles namely: BMW F30 right side outer LED O/S TL (BMW TL), Audi A5 S5 N/S LED left outer TL facelift (Audi TL), Truck-DACA08712AM TL (Truck TL) and Nissan Qashqai right side tailgate boot lid TL 26550 4EA0A model (Nissan TL). We measured the radiation patterns for these TLs and the illuminated surface areas and estimated 𝑃 𝑇 , see TableII. As shown in TableII, the half power angle (𝜃1 -out ) varies within the range of 10 o to 75 o , with the lowest and highest number for the Truck and BMW, respectively, which corresponds to the narrow and wide beam profiles as depicted in two-dimensional (2D) polar plots in Fig.10.

Fig. 10 :

 10 Fig. 10: 2D polar plots of the normalized beam profile of TLs from empirical measurements

Fig. 11 :

 11 Fig. 11: The inter-vehicle distance as a function of driving speeds using the 2 seconds driving rule

  shows the received power (in dBm) per Tx against the vehicles' speed for a range of irradiance angle [𝜃 hor , 𝜃 ver ] of [0 o , 0 o ] to [20 o , 0 o ] (left of the TL's beam axis), for the case with no OC at the Rx. The figure reveals that, for the BMW TL the maximum driving speed is 6.4 mph (i.e., 𝐷 𝑣 = 5.7 m) for [𝜃 hor , 𝜃 ver ]= [0 o , 0 o ] and 𝑃 𝑟 of -36 dBm (i.e., for a receiver sensitivity of -36 dBm), while for Truck TL there is a sharp decrease in the achievable driving speeds from 3.6 to 1.2 mph as [𝜃 hor , 𝜃 ver ] increases from [0 o , 0 o ] to [20 o , 0 o ] due to its narrower radiation pattern. A summary of the attainable driving speeds and 𝐷 𝑣 for TLs under study are given in Table

Fig. 13 :

 13 Fig. 13: The required transmit power versus the driving speed for the system with and without a NIOC

Fig. 14 :

 14 Fig. 14: Normalized solar irradiance as a function of wavelength

Fig. 15 :

 15 Fig. 15: Received power against the driving speeds for the Rx with and without NIOC

TABLE I KEY

 I GEOMETRY PARAMETERS AND SIMULATION VALUES

	Parameter	Symbol Value
	Lane width	𝑤 RL	2.5 m
	Width of Tx vehicle	𝑤 v-Tx	1.7 m
	Width of Rx vehicle	𝑤 v-Rx	1.7 m
	Distance between Rx1 & Rx2	𝑤 Rx	1.2 m
	Distance between Tx1 & Tx2	𝑤 Tx	1.2 m
	Length of Txs	𝑙 Tx	0.1 m
	Horizontal link span	𝐿 𝑠-hor	1-50 m
	Vertical Tx and Rx offset	𝐻	0.25-0.75 m
	Lens focal lengths	𝑓	25.4-50.0 mm
	PD's surface area	𝐴 PD	0.2 -~2cm 2

TABLE II TL

 II PARAMETERS FROM EMPIRICAL MEASUREMENTS TL 𝜽𝟏

					PT
					(mW)
	BMW	75	65	124.7	110.5
	Audi	55	47	46.2	39.7
	Truck	10	10	80.0	32.4
	Nissan	27	22	38.2	9.4

𝟐 ⁄ -𝐢𝐧 ( o ) 𝜽𝟏 𝟐 ⁄ -𝐨𝐮𝐭 ( o ) Illuminated area (cm 2 )

  𝜃 h𝑜𝑟 , 𝜃 𝑣𝑒𝑟 ] INCREASES FROM [0 O , 0 O ] TO [20 O , 0 O ] [𝜽 𝐡𝐨𝐫 , 𝜽 𝐯𝐞𝐫 ] =[𝟎 𝐨 , 𝟎 𝐨 ] [𝜽 𝐡𝐨𝐫 , 𝜽 𝐯𝐞𝐫 ]= [𝟐𝟎 𝐨 , 𝟎 𝐨 ]

			TABLE III
	KEY PARAMETERS OF THE LINK POWER BUDGET ANALYSIS
	Parameter		Symbol	Value
	Link safety margin		𝐿 sm	3 dB
	Surface area of PD		𝐴 PD	1.5 cm 2
	TL transmit power Irradiance angle		𝑃 𝑇 [𝜃 hor , 𝜃 ver ]	9.4-110.5 mW [0 o , 0 o ]-[20 o , 0 o ]
	Inter-vehicle distance	𝐷 𝑣	1-~90 m
	Diameter of NIOC		𝑑	25.4 mm-50.0 mm
	Vehicle speed		S	~1-100 mph
	Gain of optical filter		𝑇 𝑠 (𝜑 hor, 𝜑 ver )	1
			TABLE IV
	SUMMARY OF ACHIEVABLE DRIVING SPEEDS AND INTER-VEHICLE
	DISTANCES AS [TL type	Speed	𝑫 𝒗	Speed	𝑫 𝒗
		(mph)	(m)	(mph) (m)
	BMW	6.4	5.7	6.2	5.5
	Audi	4.0	3.6	3.7	3.3
	Truck	3.6	3.2	1.2	1.1
	Nissan	1.7	1.5	2.2	2.0

(a)

from the European Union's Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement no.764461 (VISION). Zabih Ghassemlooy acknowledges the Engineering and Physical Sciences Research Council grant EP/P006280/1: MARVEL and the EU COST Action Newfocus on optical wireless communications (CA19111). Juna Sathian acknowledges the Royal Society International Exchange Grant IES\R3\203061 and Stanislav Zvanovec acknowledges the Czech Science Foundation Project GACR 17-17538S.


Hans-Jörg Schurr
email: hans-jorg.schurr@inria.fr

Mathias Fleury
email: mathias.fleury@jku.at

Martin Desharnais
email: martin.desharnais@unibw.de

Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant

Keywords: automatic theorem provers, proof assistants, proof verification

We present a fast and reliable reconstruction of proofs generated by the SMT solver veriT in Isabelle. The fine-grained proof format makes the reconstruction simple and efficient. For typical proof steps, such as arithmetic reasoning and skolemization, our reconstruction can avoid expensive search. By skipping proof steps that are irrelevant for Isabelle, the performance of proof checking is improved. Our method increases the success rate of Sledgehammer by halving the failure rate and reduces the checking time by 13%. We provide a detailed evaluation of the reconstruction time for each rule. It reveals that the runtime is influenced by both simple rules that appear very often and common complex rules.

Introduction

Proof assistants are used in verification, formal mathematics, and other areas to provide trustworthy, machine-checkable formal proofs of theorems. Proof automation reduces the burden of proof on proof assistant users and allows them to focus on the core of their arguments instead of technical details. A successful approach implemented by "hammers", like Sledgehammer for Isabelle [START_REF] Blanchette | Extending Sledgehammer with smt solvers[END_REF], is to heuristically selects facts from the background; use an external automatic theorem prover, such as a satisfiability modulo theories (SMT) solver [START_REF] Barrett | Satisfiability modulo theories[END_REF], to filter facts needed to discharge the goal; and to use the filtered facts to find a trusted proof.

Isabelle does not accept proofs that do not go through the assistant's inference kernel. Hence, Sledgehammer attempts to find the fastest internal method that can recreate the proof (preplay). This is often a call of the smt tactic, which runs an SMT solver, parses the proof, and reconstructs it through the kernel. This reconstruction allows the usage of external provers. The smt tactic was originally developed for the SMT solver Z3 [START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF][START_REF] De Moura | Z3: An efficient SMT solver[END_REF].

The SMT solver CVC4 [9] is one of the best solvers on Sledgehammer generated problems [START_REF] Blanchette | Semi-intelligible Isar proofs from machine-generated proofs[END_REF], but currently does not produce proofs for problems with quantifiers. To reconstruct its proofs, Sledgehammer mostly uses the smt tactic based on Z3. However, since CVC4 uses more elaborate quantifier instantiation techniques, many problems provable for CVC4 are unprovable for Z3. Therefore, Sledgehammer regularly fails to find a trusted proof and the user has to write the proofs manually. veriT [START_REF] Bouton | veriT: An open, trustable and efficient SMT-solver[END_REF] (Sect. 2) supports these techniques and we extend the smt tactic to reconstruct its proofs. With the new reconstruction (Sect. 3), more smt calls are successful. Hence, less manual labor is required of users.

We devised a very early prototype [6, Sect. 6.2, second paragraph] of the extension to validate the fine-grained proof format. We also published more details on the reconstruction method and the rules [START_REF] Fleury | Reconstructing veriT proofs in Isabelle/HOL[END_REF] without adapting veriT to ease reconstruction (Sect. 3).

The runtime of the smt method depends on the runtime of the reconstruction and the solver. To simplify the reconstruction, we do not treat veriT as a black box anymore, but extend it to produce more detailed proofs that are easier to reconstruct. We use detailed rules for simplifications with a combination of propositional, arithmetic, and quantifier reasoning. Similarly, we add additional information to avoid search, like for linear arithmetic and for term normalization. Our reconstruction method uses the newly provided information, but it also has a step skipping mode that combines some steps (Sect. 4).

We optimize the performance further by tuning the search by veriT. Multiple options influence the execution time of an SMT solver. To fine-tune veriT's search procedure, we select four different combinations of options, or strategies, by generating typical problems and selecting options with complementary performance on these problems. We extend Sledgehammer to compare these four selected strategies and suggest the fastest to the user. We then evaluate the reconstruction with Sledgehammer on a large benchmark set. Our new tactic halves the failure rate. We also study the time required to reconstruct each rule. Many simple rules occur often, showing the importance of step skipping (Sect. 5).

Finally, we discuss related work (Sect. 6). Compared to the prototype [START_REF] Fleury | Reconstructing veriT proofs in Isabelle/HOL[END_REF], the smt tactic is now thoroughly tested. We fixed all issues revealed during development and improved the performance of the reconstruction method. We integrated the work presented here into Isabelle version 2021; i.e., Sledgehammer can also suggest veriT, without user interaction. To simplify future reconstruction efforts, we document the proof format and all rules used by veriT. The resulting reference manual is part of the veriT documentation [START_REF]Proofonomicon: A reference of the veriT proof format[END_REF].

veriT and Proofs

The SMT solver veriT is an open source solver based on the CDCL(T ) calculus. In proof-production mode, it supports the theories of uninterpreted functions with equality, linear real and integer arithmetic, and quantifiers. To support quantifiers veriT uses quantifier instantiation and extensive preprocessing.

veriT's proof syntax is an extension SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2.6[END_REF] which uses S-expressions and prefix notation. The proofs are refutation proofs, i.e., proofs of K. A proof is an indexed list of steps. Each step has a conclusion clause (cl ..) and is annotated with a rule, a list of premises, and some rule-dependent arguments. veriT distinguishes 90 rules [START_REF]Proofonomicon: A reference of the veriT proof format[END_REF]. Subproofs are the key feature of the proof format. They introduce an additional context. Contexts are used to reason about binders, e.g., preprocessing steps like transformation under quantifiers.

The conclusion of rules with contexts are always equalities. The context models a substitution into the free variables of the term on the left-hand side of the equality. Consider the following proof fragment that renames the variable name x, as done during preprocessing:

(assume a0 (exists (x A) (P x)) (anchor :step t3 :args (:= x vr)) (step t1 (cl (= x vr)) :rule cong)

(step t2 (cl (= (f x) (f vr))) :rule cong) (step t3 (cl (= (exists (x A) (f vr)) (exists (vr A) (f vr))) :rule bind)
The assume command repeats input assertions or states local assumptions. Subproofs start with the anchor command that introduces a context. Semantically, the context is a shorthand for a lambda abstraction of the free variable and an application of the substituted term. Here the context is x Þ Ñ vr and the step t1 means pλx. xq vr " vr. The step is proven by congruence (rule cong). Then congruence is applied again (step t2) to prove that pλx. f xq vr " f vr and step t3 concludes the renaming.

During proof search each module of veriT appends steps onto a list. Once the proof is completed, veriT performs some cleanup before printing the proof. First, a pruning phase removes branches of the proof not connected to the root K. Second, a merge phase removes the duplicated steps. The final pass prepares the data structures for the optional term sharing via name annotations.

Overview of the veriT-Powered smt Tactic

Isabelle is a generic proof assistant based on an intuitionistic logic framework, Pure, and is almost always only used parameterized with a logic. In this work we use only Isabelle/HOL, the parameterization of Isabelle with higher-order logic with rank-1 (top level) polymorphism. Isabelle adheres to the LCF [START_REF] Gordon | Edinburgh LCF: A Mechanised Logic of Computation[END_REF] tradition. Its kernel supports only a small number of inferences. Tactics are programs that prove a goal by using only the kernel for inferences. The LCF tradition also means that external tools, like SMT solvers, are not trusted.

Nevertheless, external tools are successfully used. They provide relevant facts or a detailed proof. The Sledgehammer tool implements the former and passes the filtered facts to trusted tactics during preplay. The smt tactic implements the latter approach. The proof provided by the solver is checked by Isabelle. The focus of our work is the smt tactic, but we also extended Sledgehammer so that it also suggests the new tactic to users.

The smt tactic translates the current goal to the SMT-LIB format [START_REF] Barrett | The SMT-LIB Standard: Version 2.6[END_REF], runs an SMT solver, parses the proof, and replays it through Isabelle's kernel. To choose the smt tactic the user applies (smt (z3)) to use Z3 and (smt (verit)) to use veriT. We will refer to them as z-smt and v-smt. The proof formats of Z3 and veriT are so different that separate reconstruction modules are needed. The v-smt tactic performs four steps:

1. It negates the proof goal to have a refutation proof and also encodes the goal into first-order logic. The encoding eliminates lambda functions. To do so, it replaces each lambda function with a new function and creates app operators corresponding to function application. Then veriT is called to find a proof. 2. It parses the proof found by veriT (if one is found) and encodes it as a directed acyclic graph with K as the only conclusion. 3. It converts the SMT-LIB terms to typed Isabelle terms and also reverses the encoding used to convert higher-order into first-order terms. 4. It traverses the proof graph, checks that all input assertions match their Isabelle counterpart and then reconstructs the proof step by step using the kernel's primitives.

Tuning the Reconstruction

To improve the speed of the reconstruction method, we create small and welldefined rules for preprocessing simplifications (Sect. 4.1). Previously, veriT implicitly normalized every step; e.g., repeated literals were immediately deleted. It now produces proofs for this transformation (Sect. 4.2). Finally, the linear-arithmetic steps contain coefficients which allow Isabelle to reconstruct the step without relying on its limited arithmetic automation (Sect. 4.3). On the Isabelle side, the reconstruction module selectively decodes the first-order encoding (Sect. 4.4). To improve the performance of the reconstruction further, it also skips some proof steps (Sect. 4.5).

Preprocessing Rules

During preprocessing SMT solvers perform simplifications on the operator level which are often akin to simple calculations. For example, the term a ˆ0 ˆf pxq is replaced by the constant 0.

To capture such simplifications, we create a list of 17 new rules: one rule per arithmetic operator, one to replace boolean operators such as XOR with their definition, and one to replace n-ary operator applications with binary applications. This is a compromise: having one rule for every possible simplification would create a much longer proof and make veriT more complicated. The example above now produces a prod simplify step with the conclusion a ˆ0 ˆf pxq " 0.

Previously, a single step of the connect equiv rule collected all those simplifications and no list of simplifications performed by this rule existed. The reconstruction relied an experimentally created list of tactics to be fast enough.

On the Isabelle side, the reconstruction is fast, because we can direct the search instead of trying automated tactics that can also work on other parts of the formula. For example, the simplifier handles the numeral manipulations of the prod simplify rule and we restrict it to only use arithmetic lemmas.

Moreover, since we know the performed transformations, we can ignore some parts of the terms by generalizing, i.e., replacing them by constants [START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF]. Because generalized terms are smaller, the search is more directed and we are less likely to hit the search-depth limitation of Isabelle's auto tactic as before. Overall, the reconstruction is more robust and easier to debug.

Implicit Steps

To simplify reconstruction, we avoid any implicit normal form of conclusions. For example, a rule concluding b _ P can be used to prove P _ P . In such cases veriT automatically normalizes the conclusion P _ P to P . Without a proof of the normalization, the reconstruction has to implement special cases for most rules.

We add new proof rules for the normalization and extend veriT to use them. Instead of keeping only the normalized step, both the original and the normalized step appear in the proof. For the example above, we have the step P _ P and the normalized P . To remove a double negation t we introduce the tautology t _ t and resolve it with the original clause. Our changes do not affect any other part of veriT. The solver now also prunes the superfluous steps concluding J.

On the Isabelle side, the reconstruction becomes more regular with fewer special cases. The reconstruction method can directly reconstruct rules. To deal with the normalization, the reconstruction used to first generate the conclusion of the theorem and then ran the simplifier to match the normalized conclusion. This could not deal with tautologies. The extra step improves the reliability and the speed of the reconstruction.

We also improve the proof reconstruction of quantifier instantiation steps. One of the instantiation schemes, conflicting instances [START_REF] Barbosa | Congruence closure with free variables[END_REF][START_REF] Reynolds | Finding conflicting instances of quantified formulas in smt[END_REF], only works on implicitly clausified terms. We introduce an explicit quantified-clausification rule qnt cnf that is issued before instantiating. While this rule is not detailed, knowing when clausification is needed improves reconstruction, because it avoids clausifying unconditionally. The clausification is also shared between instantiations of the same term.

Arithmetic Reasoning

We use a proof witness to handle linear arithmetic. When the propositional model is unsatisfiable in the theory of linear real arithmetic, the solver creates la generic steps. The conclusion is a tautological clause of linear inequalities and equations and the justification of the step is a list of coefficients so that the linear combination is a trivially contradictory inequality after simplification (e.g., 0 ě 1). Farkas' lemma guarantees the existence of such coefficients for reals. Most SMT solvers, including veriT, use the simplex method [START_REF] Dutertre | Integrating simplex with DPLL(T)[END_REF] to handle linear arithmetic. It calculates the coefficients during normal operation.

The real arithmetic solver also strengthens inequalities on integer variables before adding them to the simplex method. For example, if x is an integer the inequality 2x ă 3 becomes x ď 1. The corresponding justification is the rational coefficient 1 2 . The reconstruction must replay this strengthening. The complete linear arithmetic proof step 1 ă x _ 2x ă 3 looks like

(step t11 (cl (< 1 x) (< (* 2 x) 3)) :rule la_generic :args (1 (div 1 2)))
The reconstruction of an la generic step in Isabelle starts with the goal Ž i c i where each c i is either an equality or an inequality. The reconstruction method first generalizes over the non-arithmetic parts. Then it transforms the lemma into the equivalent formulation c 1 ùñ ¨¨¨ùñ c n ùñ K and removes all negations (e.g., by replacing a ď b with b ą a).

Next, the reconstruction method multiplies the equation by the corresponding coefficient. For example, for integers, the equation A ă B, and the rational coefficient p q (with p ą 0 and q ą 0), it strengthens the equation and multiplies by p to get p ˆpA div qq `p ˆpif B mod q " 0 then 1 else 0q ď p ˆpB div qq.

The if-then-else term pif B mod q " 0 then 1 else 0q corresponds to the strengthening. If B mod q " 0, the result is an equation of the form A 1 `1 ď B 1 , i.e., A 1 ă B 1 . No strengthening is required for the corresponding theorem over reals.

Finally, we can combine all the equations by summing them while being careful with the equalities that can appear. We simplify the resulting (in)equality using Isabelle's simplifier to derive K.

To replay linear arithmetic steps, Isabelle can also use the tactic linarith as used for Z3 proofs. It searches the coefficients necessary to verify the lemma. The reconstruction used it previously [START_REF] Fleury | Reconstructing veriT proofs in Isabelle/HOL[END_REF], but the tactic can only find integer coefficients and fails if strengthening is required. Now the rule is a mechanically checkable certificate.

Selective Decoding of the First-order Encoding

Next, we consider an example of a rule that shows the interplay of the higher-order encoding and the reconstruction. To express function application, the encoding introduces the first-order function app and constants for encoded functions. The proof rule eq congruent expresses congruence on a first-order function:

pt 1 ‰ u 1 q _ . . . _ pt n ‰ u n q _ f pt 1 , . . . , t n q " f pu 1 , . . . , u n q. With the encoding it can conclude f ‰ f 1 _ x ‰ x 1 _ apppf, xq " apppf 1 , x 1 q. If the reconstruction unfolds the entire encoding, it builds the term f ‰ f 1 _ x ‰ x 1 _ f x " f 1 x 1 .
It then identifies the functions and the function arguments and uses rewriting to prove that if f " f 1 and x " x 1 , then f x " f 1 x 1 .

However, Isabelle β-reduces all terms implicitly, changing the term structure. Assume f :" λx. x " a and f 1 :" λx. a " x. After unfolding all constructs that encode higher-order terms and after β-reduction, we get pλx. x " aq ‰ pλx. a " x 1 q _ px ‰ x 1 q _ px " aq " pa " y 1 q. The reconstruction method cannot identify the functions and function arguments anymore.

Instead, the reconstruction method does not unfold the encoding including app. This eliminates the need for a special case to detect lambda functions. Such a case was used in the previous prototype, but the code was very involved and hard to test (such steps are rarely used).

Skipping Steps

The increased number of steps in the fine-grained proof format slows down reconstruction. For example, one rule only returns its premise, but accounts for more than 1% of the reconstruction time. A more involved example is skolemization from Dx. P x. The proof from Z3 uses only one step. veriT uses eight steps-first renaming it to pDx. P xq " pDv. P vq (with a subproof of at least 2 steps), then concluding the renaming to get pDv. P vq (two steps), then pDv. P vq " P p v. P vq (with a subproof of at least 2 steps), after that, ppDv. P vq ‰ P p v. P vqq _ pDv. P vq _ P p v. P vq, and finally P p v. P vq by resolution.

To reduce the number of steps, our reconstruction skips two kinds of steps. First, it replaces every usage of the or rule by its only premise. Second, it skips the renaming of bound variables. The proof format treats @x. P x and @y. P y as two different terms and requires a detailed proof of the conversion. Isabelle, however, uses De Bruijn indices and variable names are irrelevant. Hence, we replace steps of the form p@x. P xq ðñ p@y. P yq by a single application of reflexivity. Since veriT initially canonizes all variable names, this eliminates many steps.

We can also simplify the idiom "equiv pos2; th resolution". veriT generates it for each skolemization and variable renaming. Step skipping replaces it by a single step which we replay using a specialized theorem.

On proof with quantifiers, step skipping can remove more than half of the steps-only four steps remain in the skolemization example above (where two are simply reflexivity). However, with step skipping the smt method is not an independent checker that confirms the validity of every single step in a proof.

Evaluation

During development we routinely tested our proof reconstruction to find bugs. As a side effect, we produced SMT-LIB files corresponding to the calls. We measure the performance of veriT with various options on them and select five different Table 1. Options corresponding to the different veriT strategies Name Options default (no option) del insts --index-sorts --index-fresh-sorts --ccfv-breadth --inst-deletion --index-SAT-triggers --inst-deletion-loops --inst-deletion-track-var ccfv SIG --triggers-new --index-SIG --triggers-sel-rm-specific ccfv insts --triggers-new --index-sorts --index-fresh-sorts --triggers-sel-rm-specific --triggers-restrict-combine --inst-deletion-loops --index-SAT-triggers --inst-deletion-track-vars --ccfv-index=100000 --ccfv-index-full=1000 --inst-sorts-threshold=100000 --ematch-exp=10000000 --inst-deletion best --triggers-new --index-sorts --index-fresh-sorts --triggers-sel-rm-specific strategies (Sect. 5.1). We also evaluate the repartition of the tactics used by Sledgehammer for preplay (Sect. 5.2), and the impact of the rules (Sect. 5.3).

We performed the strategy selection on a computer with two Intel Xeon Gold 6130 CPUs (32 cores, 64 threads) and 192 GiB of RAM. We performed Isabelle experiments with Isabelle version 2021-RC2 on a computer with two AMD EPYC 7702 CPUs (128 cores, 256 threads) and 2 TiB of RAM.

Strategies

veriT exposes a wide range of options to fine-tune the proof search. In order to find good combinations of options (strategies), we generate problems with Sledgehammer and use them to fine-tune veriT's search behavior. Generating problems also makes it possible to test and debug our reconstruction.

We test the reconstruction by using Isabelle's Mirabelle tool. It reads theories and automatically runs Sledgehammer [START_REF] Blanchette | Semi-intelligible Isar proofs from machine-generated proofs[END_REF] on all proof steps. Sledgehammer calls various automatic provers (here the SMT solvers CVC4, veriT, and Z3 and the superposition prover E [START_REF] Schulz | E -a brainiac theorem prover[END_REF]) to filter facts and chooses the fastest tactic that can prove the goal. The tactic smt is used as a last resort.

To generate problems for tuning veriT, we use the theories from HOL-Library (an extended standard library containing various developments) and from the formalizations of Green's theorem [START_REF] Abdulaziz | An Isabelle/HOL formalisation of Green's theorem[END_REF][START_REF] Abdulaziz | An Isabelle/HOL formalisation of Green's theorem[END_REF], the Prime Number Theorem [START_REF] Eberl | The prime number theorem[END_REF], and the KBO ordering [START_REF] Becker | Formalization of Knuth-Bendix orders for lambda-free higher-order terms[END_REF]. We call Mirabelle with only veriT as a fact filter. This produces SMT files for representative problems Isabelle users want to solve and a series of calls to v-smt. For failing v-smt calls three cases are possible: veriT does not find a proof, reconstruction times out, or reconstruction fails with an error. We solved all reconstruction failures in the test theories.

To find good strategies, we determine which problems are solved by several combination of options within a two second timeout. We then choose the strategy which solves the most benchmarks and three strategies which together solve the most benchmarks. For comparison, we also keep the default strategy.

The strategies are shown in Table 1 and mostly differ in the instantiation schemes. The strategy del insts uses instance deletion [START_REF] Barbosa | Efficient instantiation techniques in SMT (work in progress[END_REF] and uses a breadthfirst algorithm to find conflicting instances. All other strategies rely on extended trigger inference [START_REF] Leino | Trigger selection strategies to stabilize program verifiers[END_REF]. The strategy ccfv SIG uses a different indexing method for instantiation. It also restricts enumerative instantiation [START_REF] Reynolds | Revisiting enumerative instantiation[END_REF], because the options --index-sorts and --index-fresh-sorts are not used. The strategy ccfv insts increases some thresholds. Finally, the strategy best uses a subset of the options used by the other strategies. It is also the strategy used by Sledgehammer for fact filtering.

We have also considered using a scheduler in Isabelle as used in the SMT competition. The advantage is that we do not need to select the strategy on the Isabelle side. However, it would make v-smt unreliable. A problem solved by only one strategy just before the end of its time slice can become unprovable on slower hardware. Issues with z-smt timeouts have been reported on the Isabelle mailing list, e.g., due to an antivirus delaying the startup [START_REF] Immler | Re[END_REF].

Improvements of Sledgehammer Results

To measure the performance of the v-smt tactic, we ran Mirabelle on the full HOL-Library, the theory Prime Distribution Elementary (PDE) [START_REF] Eberl | Elementary facts about the distribution of primes[END_REF], an executable resolution prover (RP) [START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's ordered resolution prover[END_REF], and the Simplex algorithm [START_REF] Marić | An incremental simplex algorithm with unsatisfiable core generation[END_REF]. We extended Sledgehammer's proof preplay to try all veriT strategies and added instrumentation for the time of all tried tactics. Sledgehammer and automatic provers are mostly nondeterministic programs. To reduce the variance between the different Mirabelle runs, we use the deterministic MePo fact filter [START_REF] Meng | Lightweight relevance filtering for machine-generated resolution problems[END_REF] instead of the better performing MaSh [START_REF] Kühlwein | Mash: Machine learning for Sledgehammer[END_REF] that uses machine learning (and depends on previous runs) and underuse the hardware to minimize contention. We use the default timeouts of 30 seconds for the fact filtering and one second for the proof preplay. This is similar to the Judgment Day experiments [START_REF] Böhme | Sledgehammer: Judgement day[END_REF]. The raw results are available [START_REF] Schurr | Log file for the current paper[END_REF].

Success Rate. Users are not interested in which tactics are used to prove a goal, but in how often Sledgehammer succeeds. When running it, there are three possible outcomes: (i) a successfully preplayed proof, (ii) a proof hint that failed to be preplayed, or (iii) a failure. We define the success rate as the proportion of outcome (i) over the total number of Sledgehammer calls.

Table 2 gathers the results of running Sledgehammer on all unique goals of selected formalizations and analyzing its outcome using different preplay configurations where only z-smt (the baseline) or both v-smt and z-smt are enabled. Any useful preplay tactic should increase the success rate (SR) by preplaying new proof hints provided by the fact-filter prover, reducing the preplay failure rate (PF).

Let us consider, e.g., the results when using CVC4 as fact-filter prover. The success rate of the baseline on the HOL-Library is 54.6% and its preplay failure rate is 1.5%. This means that CVC4 found a proof for 54.6%`1.5% " 56.1% of the goals, but that Isabelle's proof methods failed to preplay many of them. In such cases, Sledgehammer gives a proof hint to the user, which has to manually find a functioning proof. By enabling v-smt, the failure rate decreases by two thirds, from 1.5% to 0.5%, which directly increases the success rate by 1 percentage point: new cases where the burden of the proof is moved from the user to the proof assistant. The failure rate is reduced in similar proportions for PNT (63%), RP (63%), and Simplex (56%). For these formalizations, this improvement translates to a smaller increase of the success rate, because the baseline failure rate was smaller to begin with. This confirms that the instantiation technique conflicting instances [START_REF] Barbosa | Congruence closure with free variables[END_REF][START_REF] Reynolds | Finding conflicting instances of quantified formulas in smt[END_REF] is important for CVC4.

When using veriT or Z3 as fact-filter prover, a failure rate of zero could be expected, since the same SMT solvers are used for both fact filtering and preplaying. The observed failure rate can partly be explained by the much smaller timeout for preplay (1 second) than for fact filtering (30 seconds).

Overall, these results show that our proof reconstruction enables Sledgehammer to successfully preplay more proofs. For the user, this means that the availability of v-smt as a proof preplay tactic increases the number of goals that can be fully automatically proved, by reducing the failure rate. Saved time. Table 3 shows a different view on the same results. Instead of the raw success rate, it shows the time that is spent reconstructing proofs. Using the baseline configuration, preplaying all formalizations takes a total of 258.1 31.5 `36.0 `39.0 " 364.6 seconds. When enabling v-smt, some calls to z-smt are replaced by faster v-smt calls and the reconstruction time decreases by 13% to 218.2 `26.5 `33.4 `37.9 " 316 seconds. Note that the per-formalization improvement varies considerably: 15% for HOL-Library, 16% for PNT, 5.6% for RP, and 2.9% for Simplex.

Table 3. Preplayed proofs (Pr.) and their execution time (s) when using CVC4 as fact-filter prover. Shared proofs are found with and without v-smt and new proofs are found only with v-smt. The proofs and their associated timings are categorized in one-liners using v-smt (OLv), z-smt (OLz), or any other Isabelle proof methods (OLo). For the user, this means that enabling v-smt as a proof preplay tactic may significantly reduce the verification time of their formalizations.

Total

Impact of the Strategies. We have also studied what happens if we remove a single veriT strategy from Sledgehammer (Table 4). The most important one is best, as it solves the highest number of problems. On the contrary, default is nearly entirely covered by the other strategies. ccfv SIG and del insts have a similar number where they are faster than Z3, but the former has more unique goals and therefore, saves more time. Each strategy has some uniquely solved problems that cannot be reconstructed using any other. The results are similar for the other theories used in Table 3.

Speed of Reconstruction

To better understand what the key rules of our reconstruction are, we recorded the time used to reconstruct each rule and the time required by the solver. The reconstruction ratio shows how much slower reconstructing compared to finding a proof. For very fast proofs, Z3's concise format is better (first quartile: 2.2 for v-smt vs 1.5). The medians are similar (6.2 vs 7.1), but the third quartile (12.4 vs 22.9) shows that the detailed proof format reduces the number of slow proofs.

Fig. 1 shows the distribution of the time spent on some rules. 5 We remove the slowest and fastest 5% of the applications, because garbage collection can trigger at any moment and even trivial rules can be slow. Fig. 2 gives the sum of all reconstruction times over all proofs. We call parsing the time required to parse and convert the veriT proof into Isabelle terms.

Overall, there are two kinds of rules: (1) direct application of a sequence of theorems-e.g., equiv pos2 corresponds to the theorem pa Ø bq _ a _ band (2) calls to full-blown tactics-like qnt cnf.

First, direct application of theorems are usually fast, but they occur so often that the cumulative time is substantial. For example, cong only needs to unfold assumptions and apply reflexivity and symmetry of equality. However, it appears so often and sometimes on large terms, that it is an important rule.

Second, rules which require full-blown tactics are the slowest rules. For qnt cnf (CNF under quantifiers, see Sect. 4.2), we have not written a specialized tactic, but rely on Isabelle's tableau-based blast tactic. This rule is rather slow, but is rarely used. It is similar to the rule la generic: it is slow on average, but searching the coefficients takes even more time.

We can also see that the time required to check the simplification steps that were formerly combined into the connect equiv rule is not significant anymore.

We have performed the same experiments with the reconstruction of the SMT solver Z3. Unlike for veriT, we do not have the amount of time required for parsing. The results are shown in Figs. 3 and4. The rule distribution is very different. The nnf-neg and nnf-pos rules are the slowest rules and take a huge amount of time in the worst case. However, the coarser quantifier instantiation step is on average faster than the one produced by veriT. We suspect that reconstruction is faster because the rule, which is only an implication without choice terms, is easier to check (no equality reordering).

Related Work

The SMT solvers CVC4 [9], Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF], and veriT [START_REF] Bouton | veriT: An open, trustable and efficient SMT-solver[END_REF] produce proofs. CVC4 does not record quantifier reasoning in the proof, whereas Z3 uses some macro rules. Proofs from SMT solvers have also been used to generate unsatisfiability cores [START_REF] Déharbe | SMT solvers for Rodin[END_REF], and interpolants [START_REF] Mcmillan | Interpolants from Z3 proofs[END_REF]. They are also useful to debug the solver itself, since unsound steps often point to the origin of bugs. Our work also relates to systems like Dedukti [4] that focuses on translating proof steps, not on replaying them.

Proof reconstruction has been implemented in various systems, including CVC4 proofs in HOL Light [START_REF] Mclaughlin | Cooperating theorem provers: A case study combining HOL-Light and CVC Lite[END_REF], Z3 in HOL4 and Isabelle/HOL [START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF], and veriT [START_REF] Armand | A modular integration of SAT/SMT solvers to Coq through proof witnesses[END_REF] and CVC4 [START_REF] Ekici | SMTCoq: A plug-in for integrating SMT solvers into Coq[END_REF] in Coq. Only veriT produces detailed proofs for preprocessing and Fig. 3. Timing of some of Z3's rules sorted by median. From left to right, the lower whisker marks the 5th percentile, the lower box line the first quartile, the middle of the box the median, the upper box line the third quartile, and the upper whisker the 95th percentile. nnf-neg's 95th percentile is 32 ms. nnf-pos's 95th percentile is 86 ms. skolemization. SMTCoq [START_REF] Armand | A modular integration of SAT/SMT solvers to Coq through proof witnesses[END_REF][START_REF] Ekici | SMTCoq: A plug-in for integrating SMT solvers into Coq[END_REF] currently supports veriT's version 1 of the proof output which has different rules, does not support detailed skolemization rules, and is implemented in the 2016 version of veriT, which has worse performance. SMTCoq also supports bit vectors and arrays.

The reconstruction of Z3 proofs in HOL4 and Isabelle/HOL is one of the most advanced and well tested. It is regularly used by Isabelle users. The Z3 proof reconstruction succeeds in more than 90% of Sledgehammer benchmarks [13, Section 9] and is efficient (an older version of Z3 was used). Performance numbers are reported [START_REF] Böhme | Proving Theorems of Higher-Order Logic with SMT Solvers[END_REF][START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF] not only for problems generated by proof assistants (including Isabelle), but also for preexisting SMT-LIB files from the SMT-LIB library.

The performance study by Böhme [15,Sect. 3.4] uses version 2.15 of Z3, whereas we use version 4.4.0 which currently ships with Isabelle. Since version 2.15, the proof format changed slightly (e.g., th-lemma-arith was introduced), fulfilling some of the wishes expressed by Böhme and Weber [START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF] to simplify reconstruction. Surprisingly, the nnf rules do not appear among the five rules that used the most runtime. Instead, the th-lemma and rewrite were the slowest rule. Similarly to veriT, the cong rule was among the most used (without accounting for the most time), but it does not appear in our tests.

CVC4 follows a different philosophy from veriT and Z3: it produces proofs in a logical framework with side conditions [39]. The output can contain programs to check certain rules. The proof format is flexible in some aspects and restrictive in others. Currently CVC4 does not generate proofs for quantifiers.

Conclusion

We presented an efficient reconstruction of proofs generated by a modern SMT solver in an interactive theorem prover. Our improvements address reconstruction challenges for proof steps of typical inferences performed by SMT solvers.

By studying the time required to replay each rule, we were able to compare the reconstruction for two different proof formats with different design directions. The very detailed proof format of veriT makes the reconstruction easier to implement and allows for more specialization of the tactics. The ratio of time to reconstruct and time to find a proof is better for our more detailed format. Integrating our reconstruction in Isabelle halves the number of failures from Sledgehammer and nicely completes the existing reconstruction method with Z3.

Our work is integrated into Isabelle version 2021. Sledgehammer suggests the veriT-based reconstruction if it is the fastest tactic that finds the proof; so users profit without action required on their side. We plan to improve the reconstruction of the slowest rules and remove inconsistencies in the proof format. The developers of the SMT solver CVC4 are currently rewriting the proof generation and plan to support a similar proof format. We hope to be able to reuse the current reconstruction code by only adding support for CVC4-specific rules. Generating and reconstructing proofs from the veriT version with higher-order logic [8] could also improve the usefulness of veriT on Isabelle problems. The current proof rules [START_REF]Proofonomicon: A reference of the veriT proof format[END_REF] should accommodate the more expressive logic.

Appendix

Fig. 1 .

 1 Fig.1. Timing, sorted by the median, of a subset of veriT's rules. From left to right, the lower whisker marks the 5th percentile, the lower box line the first quartile, the middle of the box the median, the upper box line the third quartile, and the upper whisker the 95th percentile.

Fig. 2 .

 2 Fig.2. Total percentage spent on each rule for the SMT solver veriT in the same order as Fig.1. This graph maps the rules already shown in Fig.1to the total amount of time. The slowest rule are th resolution (15.4%), parsing (10.0%), and cong (9.5%).

Fig. 4 .

 4 Fig. 4. Total amount of time per rule for the SMT solver Z3.

Figure 5

 5 Figure5is the complete version of Figure1. Figure6is the complete version of Figure2.

Figure 6

 6 Figure5is the complete version of Figure1. Figure6is the complete version of Figure2.

Fig. 5 .Fig. 6 .

 56 Fig.5. Timing of veriT rules sorted by median. From left to right, the lower whisker marks the 5th percentile, the lower box line the first quartile, the middle of the box the median, the upper box line the third quartile, and the upper whisker the 95th percentile.

Table 2 .

 2 Outcome of Sledgehammer calls showing the total success rate (SR) of oneliner proof preplay, the number of suggested v-smt (OLv) and z-smt (OLz) one-liners, and the number of preplay failures (PF), in percentages of the unique goals.

	HOL-Library		PNT	RP	Simplex
	(13 562 goals)	(1 715 goals)	(1 658 goals)	(1 982 goals)
	SR OLv OLz PF SR OLv OLz PF SR OLv OLz PF SR OLv OLz PF
	Fact-filter prover: CVC4
	z-smt 54.6	2.7 1.5 32.9	3.6 0.8 65.0	1.3 0.8 51.6	1.6 0.9
	both 55.6 2.6 1.1 0.5 33.3 3.5 0.6 0.3 65.6 1.3 0.5 0.3 52.1 1.0 1.1 0.4
	Fact-filter prover: E
	z-smt 55.5	1.1 1.7 36.2	0.4 1.5 61.7	0.7 1.1 49.7	1.4 0.7
	both 56.0 0.9 0.6 1.3 36.4 0.5 0.1 1.3 62.0 0.8 0.2 0.8 49.8 0.4 1.1 0.6
	Fact-filter prover: veriT
	z-smt 48.6	1.7 1.2 26.1	1.5 0.6 58.1	0.9 0.7 46.6	1.0 1.0
	both 49.4 1.6 0.9 0.3 26.5 1.3 0.5 0.2 58.6 1.0 0.4 0.2 47.3 1.0 0.7 0.3
	Fact-filter prover: Z3
	z-smt 50.8	2.5 0.8 27.9	2.7 0.4 60.5	0.8 0.6 48.3	0.9 0.3
	both 51.3 1.8 1.1 0.3 28.2 2.4 0.6 0.1 60.9 1.1 0.1 0.2 48.4 0.4 0.6 0.2

Table 4 .

 4 Reconstruction time and number of solved goals when removing a single strategy (HOL-Library results only), using CVC4 as fact filter.

				Shared proofs		New proofs
			Total =	OLv	+	OLz	+	OLo	OLv
		Pr. Time " Time (Pr.) `Time (Pr.) `Time ( Pr. ) Time ( Pr. )
	HOL-	z-smt 7 421 258.1 "			87.5 (362) `170.6 (7 059)
	Library	both 7 559 218.2 " 28.8 (216) `18.8 (147) `170.6 (7 059) 35.0 ( 137)
	PNT	z-smt 565 31.5 " both 573 26.5 " 7.2 ( 52) `2.2 ( 10) `17.1 ( 503) 14.3 ( 62) `17.1 ( 503)	3.6 ( 8)
	RP	z-smt 1 080 36.0 " both 1 089 33.4 " 3.5 ( 13) `2.2 ( 8) `27.7 (1 059) 8.3 ( 21) `27.7 (1 059)	2.3 ( 9)
	Simplex	z-smt 1 024 39.0 " both 1 033 37.9 " 2.2 ( 11) `3.6 ( 21) `32.1 ( 992) 6.9 ( 32) `32.1 ( 992)	3.2 ( 9)
				Shared proofs		New proofs
			OLv		OLz	OLv
			Time	Proofs		Time	Proofs	Time	Proofs
	No best	17.9	125		47.3	238	24.6	91
	No ccfv SIG	27.5	201		22.0	162	33.7	127
	No ccfv threshold	28.9	215		19.0	148	34.6	133
	No del insts	27.9	203		22.1	160	32.0	125
	No default	29.2	216		18.8	147	34.5	136
	Baseline	28.8	216		18.8	147	35.0	137

Acknowledgment We would like to thank Haniel Barbosa for his support with the implementation in veriT. We also thank Haniel Barbosa, Jasmin Blanchette, Pascal Fontaine, Daniela Kaufmann, Petar Vukmirović, and the previous reviewers for many fruitful discussions and suggesting many textual improvements. The first author has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). The second author is supported by the LIT AI Lab funded by the State of Upper Austria. The training presented in this paper was carried out using the Grid'5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organizations (see https://www.grid5000.fr).


Xicong Li

Senior Member, IEEE, Fellow, OSA, Stanislav Zvanovec, Senior Member, IEEE Zabih Ghassemlooy

Member, IEEE Luis Nero Alves

An Equivalent Circuit Model of a Commercial LED with an ESD Protection Component for VLC

Keywords: VLC, LiFi, LED, impedance, equivalent circuit model, ESD, parasitics

An equivalent circuit model for a typical commercial light-emitting diode (LED) used in visible light communication (VLC) applications is proposed. The parameters of the elements in the model are extracted from the measured impedance using a vector network analyser. The model shows high accuracy in fitting the measured results and shows the effect of bonding/packaging parasitics and the electrostatic discharge (ESD) component on the LED's impedance and bandwidth. This study aims to raise the designer's awareness when designing and fabricating high-speed LED/µLED devices to achieve the optimal modulation bandwidth in the emerging VLC applications.

I. INTRODUCTION

V ISIBLE light communication (VLC)) or light fidelity (LiFi) has evolved from Mbps to Gbps in terms of the data rates with international standards supported over the past decade [START_REF] Ghassemlooy | Visible Light Communications: Theory and Applications[END_REF]. Such high-speed communication requires modulating the light intensity of light-emitting diodes (LED) or laser diodes (LD) in a wide bandwidth, imposing a high demand on the optimised fabrication process to deliver faster devices, like µLEDs [START_REF] Ferreira | High bandwidth GaN-based microleds for multi-Gb/s visible light communications[END_REF] and white lasers, for VLC applications. However, the majority of VLC/LiFi products or laboratory-based systems will have to rely on off-the-shelf devices, especially the high-power LEDs intended for illumination, for the time being and possibly for a long time. Additionally, most research works reported on high-bandwidth LED/µLED designs have been carried out by probing the chip die directly or using short bonding wires without complete packaging or electrostatic discharge (ESD) protection. Therefore, characterising the LEDs widely adopted in current VLC systems using the ac smallsignal equivalent circuit model has great significances in: (i) providing an accurate model for the LED driver/modulator design; and (ii) revealing the parasitics and their effects to provide guidance for future wideband device design.

In this letter, we propose an extended equivalent circuit model for a typical commercial phosphor-converted white LED, which includes parasitics introduced by the bonding wires/tracks and ESD protection components compared with the classical model [START_REF] Lee | Effect of junction capacitance on the rise time of LED's and on the turn-on delay of injection lasers[END_REF]. The equivalent circuit parameters are extracted from the impedance measured by a vector network analyser (VNA) with a dedicated surface-mount device (SMD) test fixture. Good agreement between the measured impedance and the extracted model is achieved. With the model, we observe that two resonance peaks are incurred at high frequencies due to the bonding wire parasitics and the ESD component, respectively. Although current commercial LEDs can rarely be modulated at that high speed, the observation raises awareness about the negative effects of parasitics introduced by bonding, packaging, and ESD components in the high-speed LED/µLED design specifically tailored for VLC applications [START_REF] Maret | Ultra-high speed optical wireless communications with gallium-nitride microLED[END_REF], [START_REF] Sujan | A review of gallium nitride LEDs for multi-gigabit-per-second visible light data communications[END_REF].

II. THEORY

The device used in our investigation is an off-the-shelf phosphor-converted white LED (Lumileds Luxeon Rebel LXML-PWC2) with a system PCB packaging. Fig. 1(a) shows the structure of the device in use. It can be seen that, in parallel with an ESD diode, the LED die is soldered on a compact PCB with bonding wires/tracks running from the top layer to the bottom layer to connect to the pads. Fig. 1(b) schematically illustrates the corresponding equivalent circuit model.

Both our previous study [START_REF] Li | Equivalent circuit model of high power LEDs for VLC systems[END_REF] and the works reported in the literature [START_REF] Linnartz | Wireless communication over an led channel[END_REF] have shown that, despite the difference in the LED packaging, the intrinsic LED model, i.e., the classical model, can fit the measurement well with good accuracy in the low-frequency range where the parasitics are not dominant. As shown in Fig. 1(b), the intrinsic LED part consists of the junction capacitor C j , the junction dynamic resistance R j , and the serial resistance R s accounting for the parasitic inside the LED die. Note that the current i through R j reflects the effective current for the intensity modulation. The second part of the circuit model represents the bonding wire/track parasitics with the serial resistance R b , the serial inductance L b , and the capacitor C b in parallel with the intrinsic LED model. As shown later, L b is the dominant component in the mid-range frequencies. To model the ESD diode, a serial RLC (i.e., a combination of R p , L p , and C p ) circuit is included [START_REF] Huang | A simple method to improve signal integrity of electrostatic discharge protection devices[END_REF]. It is worth mentioning that the ESD component is critical in protecting the LED/LD die from electrostatic discharge damage and therefore is highly essential to be integrated into mass-produced LED/LD chips. In this work, the device under investigation uses a separate Zener diode for ESD protection, while many LED devices might implement it within the die [START_REF] Chang | Improved ESD protection by combining InGaN-GaN MQW LEDs with GaN Schottky diodes[END_REF]. It will be shown that the third RLC circuit will dominate the response beyond its resonance frequency. It is worth noting that, for small-size ESD components or the ESD circuitry in the die, the RLC parasitic elements can be neglectable in the measured frequency range. Due to the introduction of the RLC circuit, the proposed model can cover a wider range of LEDs, which has been experimentally validated on more than six different LEDs with different sizes and packaging.

The analytical expression of the LED's impedance can therefore be written as:

Z LED = (R s + 1 jωC j //R j ) intrinsic model // 1 jωC b + R b + jωL b bonding parasitic // R p + 1 jωC p + jωL p ESD parasitic , (1)
where j is the imaginary unit, ω is the angular frequency, and // denotes two impedances in parallel. Using the voltage V Rj over R j to proportionally represent the current for intensity modulation [START_REF] Tucker | Microwave circuit models of semiconductor injection lasers[END_REF], the frequency response of the LED can be predicted by the following transfer function:

H(jω) = V o V s = hi V s = h R j V Rj V s , ( 2
)
where h is the gain coefficient accounting for the photodetector's responsitivity and the gain introduced by subsequent circuitry, e.g., transimpedance amplifier.

III. MEASUREMENT AND PARAMETER EXTRACTION

We measured the LED's impedance using a VNA (Keysight E5061B, 5Hz-3GHz) and its wideband bottom electrode SMD test fixture (Keysight 16197A, 3GHz) at varying bias points.

The LED mounted on the fixture was directly powered by the VNA's built-in bias-tee to avoid additional parasitics. Using the first reflection port, which connects to the LED, the impedance can be measured based on the S11 parameter. The second port of the VNA was connected to a high-speed optical receiver (Newport 1601, 30kHz-1GHz) to measure the S21 parameter for comparison with the model-predicted frequency response. All the measurements were carried out following a full calibration with fixture de-embedding was conducted to the VNA. Since the VNA is optimised with an impedance measurement function, the complex-valued impedance can be directly measured without conversion from the S11 parameter. Fig. 2(a) shows the measured and simulated impedance magnitude |Z LED | using the extracted parameters given in Table I for a range of bias currents. The parameter extraction method is briefly described as follows. In the low-frequency range as marked by zone A in Fig. 2(a), the measured impedance is used to estimate (R j + R s + R b ). The following decaying slopes in zones B and C are used to determine C j and C b , respectively. The minimum impedance points of D and E correspond to R b and R p , whereas L b and L p are estimated using the slopes in zones F and G. Additionally, the resonance frequencies, which can be clearly distinguished in zones D and E, confirm or estimate the value of C b and C p . Then the other parameters can be determined using the least-square error fitting. Since the parameters were extracted using measured |Z LED | only, the match between the measured and simulated impedance phase ∠Z LED confirms the validity of the proposed model, see Fig. 2(b). Using [START_REF] Ferreira | High bandwidth GaN-based microleds for multi-Gb/s visible light communications[END_REF] with the extracted parameters, the LED's frequency response was predicted and plotted in Fig. 3. Also shown is the measured S21 parameter after normalisation being applied. Due to the coated phosphor which converts part of the blue spectrum to longer wavelengths to produce white light for illumination, we used a blue filter to remove the slow components generated by the phosphor to obtain the real frequency response of the LED [START_REF] Stepniak | Advanced modulation formats in phosphorous LED VLC links and the impact of blue filtering[END_REF]. Fig. 3 shows a good agreement between the model-predicted and the measured S21 parameter curve at the bias current of 35.8 mA, confirming the effectiveness of our model. Here, a comparison between the model prediction and measurement was only given at the highest bias current because the blue filter and the limited gain of the receiver cannot support accurate S21 measurement at low bias currents. From the measurements and extracted parameters, it can be observed that the 3-dB bandwidth of the LED under test is mainly limited by the junction capacitance and the dynamic resistance [START_REF] Sujan | A review of gallium nitride LEDs for multi-gigabit-per-second visible light data communications[END_REF], which can be roughly estimated by f 3dB = 1/2πR j C j . As shown in Fig. 3 and confirmed by the simulated model, the bonding parasitics introduce steeper attenuation slopes in the frequency range of 50∼100 MHz, while the ESD diode introduces an additional degree of steepness to the slopes beyond 500 MHz. Note that the knee frequencies depend on the ESD parasitics and vary from device to device.

IV. CONCLUSION

We proposed a complete equivalent circuit model of an offthe-shelf LED used in VLC systems, taking into account the LED's intrinsic model and parasitics introduced by the die bonding/packaging and the ESD component. With this model and the measured impedance, parameters were extracted and we showed that there is a good agreement between the measured and the simulated results. Furthermore, we showed that the predicted frequency response matched the measured S21parameter, indicating that the bonding parasitics prevent the LED from achieving high bandwidth in the middle-frequency range while the ESD diode introduced steep attenuation slopes in the high-frequency range. The proposed method based on the equivalent circuit model and S-parameters measurement can be applicable to characterising future high-speed LED/µLED devices customised for VLC systems. Finally, experimental investigation demonstrated the effectiveness of the proposed method and provided a set of real-world data for future references.

Fig. 1 :

 1 Fig. 1: (a) A photo of the commercial LED in use; and (b) the equivalent circuit model of the LED driven by a source with an output impedance R g = 50 Ω.

Fig. 2 :

 2 Fig. 2: Measured and simulated: (a) |Z LED |, and (b) ∠Z LED .

Fig. 3 :

 3 Fig. 3: Measured and simulated S21 with and without the blue filter.

TABLE I :

 I Extracted Parameters at Varying Bias Currents

		Item		Bias current (mA) 2.1 mA 6.5 mA 22.7 mA 35.8 mA
		R j (Ω)	21.35	2.51	0.74	0.50
		C j (nF)	0.98	8.70	38	80.0
		Rs (Ω)	2.93	2.51	0.74	0.62
		R b (Ω)	0.29	0.27	0.25	0.28
		C b (nF)	13.2	14.4	14.4	14.4
		L b (nH)	2.45	2.45	2.45	2.45
		Rp (Ω)	1.72	1.72	1.72	1.72
		Cp (pF)	34.4	34.4	34.4	34.4
		Lp (nH)	0.98	0.98	0.98	0.98
		0
		-20
		-40
	Gain(dB)	-80 -60
		-100
			Measured S21 at 35.8 mA (no blue filter)
		-120	Measured S21 at 35.8 mA (blue filter)
			Estimated S21 at 35.8 mA (blue filter)
		-140
		10 4	10 5	10 6	10 7	10 8	10 9	10 10
					Frequency(Hz)