Nada Kraiem

Loic Constantin

Aofei Mao

Fei Wang

Bai Cui

Jean-François Silvain

Yong Feng Lu

Study of the influence of Aluminum addition on the Laser Powder Bed Fusion of Cu-Al mixtures

Keywords: Additive manufacturing, copper, aluminum, selective laser melting

The high optical reflectivity of copper (Cu) in the near infrared (NIR) domain and its elevated heat dissipation make Cu a challenging metal for laser powder bed fusion (LPBF), even with high energy densities (EDs). In this study, we demonstrated that adding aluminum (Al) powder by as little as 0.75, 1.5, and 3 wt.% substantially enhances Cu processability, leading to denser (up to 98 %) and smoother (Ra = 3.3 μm) Cu-Al parts as compared to 95% and 18 μm, respectively, for the parts printed using pure Cu. In addition, this method reduces the ED required by a factor of two for the additive manufacturing of the Cu-based parts while maintaining a significant heat dissipation. These improvements are achieved due to the coexistence of solid Cu particles with liquid Al at the vicinity of the molten pool, accomodating the predensification of the powder mixture. The development of the semi-liquid 3D printing approach opens up a new path to easily print materials difficult to be printed for broadening their applications.

Introduction

Selective laser melting (SLM) or laser powder bed fusion (LPBF), is an additive manufacturing process that enables the possibility of creating complex three-dimensional (3D) structures, where post-processing steps are reduced [START_REF] Pal | Physical Behaviors of Materials in Selective Laser Melting Process[END_REF][START_REF] Prashanth | Selective Laser Melting: Materials and Applications[END_REF]. The diversity of the materials being processed has enabled the additive manufacturing (AM) techniques to produce functional components with ideal surface finishes and physical properties comparable to those of bulk materials [START_REF] Kruth | Part and material properties in selective laser melting of metals[END_REF]. In thermal management applications for example, Cu-based materials are ideal candidates due to their exceptional thermal properties. However, due to its high thermal conductivity (TC) and low laser absorption in the NIR region (less than 10%), high energy densities (EDs) must be applied on Cu powder beds to achieve a proper melting/solidification process [START_REF] Lingqin | Explore the feasibility of fabricating pure copper parts with low-laser energy by selective laser melting[END_REF][START_REF] Tran | 3D Printing of Highly Pure Copper[END_REF].

Over the past decades, extensive research has been devoted to efficiently print pure Cu. Jadhav et al. [START_REF] Jadhav | Influence of selective laser melting process parameters on texture evolution in pure copper[END_REF] showed the printing of high-density Cu parts (99%) using a high laser power of 800 W.

Nevertheless, the high reflection of Cu powders induces laser back reflection, leading to the damage of the laser source.

More recently, Constantin et al. [START_REF] Constantin | Laser 3D printing of complex copper structures[END_REF] have used a lower energy density with a moderate laser power of 400 W. Dense (95%) and smooth Cu parts were printed. However, the processing window is very narrow, where an insufficient or excessive energy density has a great impact on the dynamics of the molten pool, and has significanly reduced the density down to 70%. Even though dense parts were obtained, the LPBF of dense Cu parts is still challenging due to the thermal issues and reflective behaviors of Cu powders.

On the other hand, numerous studies have been carried out for the production of dense Cu alloys, such as Cu-Sn, Cu-Zn and Cu-Cr [START_REF] Zhang | Microstructure and properties of high strength and high conductivity Cu-Cr alloy components fabricated by high power selective laser melting[END_REF], where the laser absorption was improved up to 70% during the printing. However, it was noticed that the TC of the materials was severely degraded.

In this research, small amount of a lightweight metal was added to Cu powders. Having a relatively low melting point compared to Cu, it was demonstrated that Al forms a liquid metal that coexists with the solid Cu particles at the vicinity of the molten pool. Consequently, the heated Al softens the Cu particles and facilitates to create connections among them. Here, the liquid phase sintering (LPS) approach was applied during SLM to assist the densification of the Cu-Al mixtures [START_REF] Kruth | Binding mechanisms in selective laser sintering and selective laser melting[END_REF][START_REF] Lü | Selective Laser Sintering[END_REF]. It was found that high energy densities were no longer needed, and that high-density parts were successfully achieved.

Experimental procedure

Laser powder bed fusion of Cu-Al mixtures. Irregular Al (US Nano, 30 um, 99.7%) and spherical Cu powders (US Nano, 45 um, 99.5%) were added to form three mixtures of Cu with 0.75, 1.5, and 3.0 wt.% of Al, respectively (Figure 1S).

The LPBF of Cu-Al parts was carried out using a SLM 125 HL system (SLM Solutions Inc) equipped with a continuous wave (CW) fiber laser (IPG photonics, YLM, Yb: YAG, λ = 1070 nm). The laser has a maximum power of 400 W and is focused on the powder bed with a spot diameter of 70 µm. The SLM was operated under a constant argon (Ar) flow to keep the oxygen level low at 0.1%. A pressure of 18 mbar was maintained inside of the printing chamber.

Constantin et al. have shown that dense and crack-free pure Cu parts were additively manufactured at a laser power of 400 W, a scan speed of 400 mm/s and a hatch distance of 0.12 mm [START_REF] Constantin | Laser 3D printing of complex copper structures[END_REF]. Therefore, the choice of the processing parameters for the Cu-Al mixtures was based on their work. A laser power of 400 W and a layer thickness of 30 µm were used in the 3D printing experiments. The laser scan speed was varied from 300 to 800 mm/s at an increment of 100 mm/s. The hatch distance was varied from 0.06 to 0.16 mm at an increment of 0.02 mm.

The ED (J/mm 3 ) was calculated with the following equation:

, [START_REF] Pal | Physical Behaviors of Materials in Selective Laser Melting Process[END_REF] where P is the laser power (W), LT is the layer thickness (mm), h is the hatch distance (mm), and s is the scan speed (mm/s). The structures were initially drawn using Solidwork® and transferred in Magics® software to prepare the build jobs and fix the printing parameters. The parts were printed on a stainless-steel building plate (125 125 25 mm 3 ).

Characterization of the Cu-Al parts.

The density of the samples was measured using the Archimedes method (Mettler Toledo AT201). The microstructures of the top surfaces of the samples as well as the Cu-Al powders were analyzed using a scanning electron microscope (SEM, FEI Quanta 200 Environmental SEM). The average surface roughness was characterized with an optical surface profiler (Zygo NewView 8000). Energy dispersive spectroscopy (EDS) was performed for chemical composition analysis using an X-Ray detector in the SEM (FEI Nova NanoSEM 450). The crystallinity of both the powders and the parts printed were analyzed by X-ray diffraction (XRD, PANalitycal X`pert PRO MPD diffractometer with a Cu Kα radiation source, λ = 0.154 nm). A high-resolution transmission electron microscopy (HR-TEM, FEI Tecnai Osiris) was used to analyze the microstructures of the parts printed.

The thermal dissipation performances of the printed gyroid structures made of pure Cu and Cu-Al at 3 wt.% Al, respectively, were also evaluated. An IR camera (FLIR E85 24°) was used during the recreation of a microelectronics thermal management situation. The parts printed were attached to an electronic chip using a thermal tape (3M™ 8815 Thermal Tape). The entire system was heated to 200 ºC. An airflow was assured by a fan placed 10 cm away from the parts.

Results and discussion

Several approaches have been implemented to achieving pore-free Cu parts by applying a moderate laser power on the powder bed. The in-situ alloying strategy in SLM was shown to be a potential method that enables a proper 3D printing of highly reflective powders such as Cu and Al [START_REF] Naeem | Laser Processing of Reflective Materials[END_REF]. However, the production of Cu-Al mixtures with a Cu-rich powder was not reported in the literature, which motivated our research to study the densification mechanism and processability of this mixture.

The optimization of the processing parameters and the evaluation of the printing quality were mainly based on the part density and surface finish. The relative density with respect to the hatch distance and scan speed are plotted in Figure 1. As can be seen on Figure 1a, the area showing high density (> 95%) of pure Cu parts was acquired within a very narrow processing window. Adding 0.75 wt.% Al in pure Cu has increased the density of the samples at scan speeds ranged between 600 and 700 mm/s, leading to a lower color contrast in Figure 1b. Note that the samples with 0.75 wt.% Al printed at a low scan speed of 300 mm/s peeled off from the building plate, and were not included in the characterization. When a high ED is applied, the liquid Cu was overheated, which generates a large thermal gradient in the solidified metal. The interlayer delamination occurred, causing the debonding of the parts from the plate [START_REF] Yakout | Influence of thermal properties on residual stresses in SLM of aerospace alloys[END_REF].

For the 1.5 wt.% Al composition, Figure 1c shows a large area where the density is above 95%, extending from 350 to 800 mm/s. However, increasing the Al content to 3 wt.% reduced the sample densities as compared with the case of 1.5 wt.% Al, indicated by the shrinkage of the zone corresponding to the density above 95%. The densification upon the melting/solidification process of the powder depends on the laser-matter interactions [START_REF] Majeed | Investigation of T4 and T6 heat treatment influences on relative density and porosity of AlSi10Mg alloy components manufactured by SLM[END_REF]. Thus, the metallurgical properties of the powder and the processing parameters, such as the laser power, the scan speed, and the hatch distance, control the dynamics of the molten pool, and hence determines the printing quality of the final parts [START_REF] Pal | Melting, fusion and solidification behaviors of Ti-6Al-4V alloy in selective laser melting at different scanning speeds[END_REF]. As can be seen, the addition of a small amount of Al has enabled the printing of dense Cu-Al parts (98%) with lower EDs than those used to print pure Cu. The Al added has improved the densification of the powders and enhanced the fusion among the Cu particles.

To further understand the previous results of the density for each Cu-Al composition, the surface morphology of the samples was studied. Figure 2 illustrates the variation of the density and the surface quality of the as-printed Cu-Al parts with respect to their Al content. As can be observed, the influence of the added Al on the part quality is noticeable. Figure 2a presents the SEM micrograph of the pure Cu at an ED of 185 J/mm 3 . The top surface of the sample exhibits pores and bumps. Dai and Gu [START_REF] Dai | Tailoring surface quality through mass and momentum transfer modeling using a volume of fluid method in selective laser melting of TiC/AlSi10Mg powder[END_REF] associated this type of defects to the balling phenomenon, that leads to an increase in the surface roughness. The modeling of the behavior of the molten pool has showed the generation of driving forces such as the thermo-capillary force and the recoil pressure caused by evaporation [START_REF] Razavykia | An Overview of Additive Manufacturing Technologies-A Review to Technical Synthesis in Numerical Study of Selective Laser Melting[END_REF]. With the heat loss, the amount of liquid metal decreases, leading to an unstable molten pool. Furthermore, applying an insufficient ED on Cu leads to a poorly melted powder, thus, to a weak wetting due to the surface tension, resulting in the formation of pores and bumps. Hence, microscale liquid droplets splash from the molten pool to form spheres [START_REF] Bai | Evolution mechanism of surface morphology and internal hole defect of 18Ni300 maraging steel fabricated by selective laser melting[END_REF][START_REF] Chen | Microstructure evolution, mechanical properties, and strengthening mechanism of TiC reinforced Inconel 625 nanocomposites fabricated by selective laser melting[END_REF]. SEM micrographs of the Cu-Al 3D printed parts with the same ED are presented in Figures 2bd. The microstructures are less porous than the pure Cu. As can be seen, with 0.75 and 1.5 wt.% Al, the surfaces are smooth and the laser tracks can be identified. With 3 wt.% Al, pores were formed on the sample surfaces. Hence, adding a small amount of Al is beneficial to reinforcing the wetting behavior and the connection among the Cu particles and hence improve their densification.

On the other hand, some studies have reported the influence of the ED on the porosity formation and defect creation during the printing process [START_REF] Donik | Influence of the Energy Density for Selective Laser Melting on the Microstructure and Mechanical Properties of Stainless Steel[END_REF]. A low ED was found to be insufficient to fully melt the powder. Medium and high EDs reduces the porosity. Nevertheless, keyholes and other defects can be observed in case of overheating. Figure 2e shows high density values for 1.5 wt.% Al at all EDs. For 0.75 and 3 wt.% Al, the densities are lower than that with 1.5 wt.% Al. As for pure Cu, the low-density values confirm the presence of voids inside the samples. Furthermore, the surface roughness of the Cu-Al parts decreased by two times compared with that of the pure Cu starting from 200 J/mm 3 as shown in Figure 2f. Nevertheless, the difference is not significant among the different Cu-Al parts.

The results have also shown a decrease in the density for the 3 wt.% Al. This can be explained by the oxidation of Al during the LPBF process (Figure 2S). Although the oxygen content inside the printing chamber is low, it is not sufficiently low to avoid a spontaneous reaction with Al.

Consequently, if Al oxide (alumina) is formed, the laser-matter interaction is reduced. The laser power applied is insufficient to melt alumina. Furthermore, alumina cannot be wetted by molten Al (contact angle > 65º from 680 to 1100 ºC) [START_REF] Bao | Wettability of Aluminum on Alumina[END_REF]. Consequently, voids are created within the samples, causing the failure of the printing [START_REF] Louvis | Selective laser melting of aluminium components[END_REF]. This reaction is likely to occur and has a significant impact on the printing process when the Al content exceeds a specific value. To better understand the powder behavior during the printing process (Figure 3d), we examined the melting mechanism of the powder more closely by applying the laser for a short time on a single-layered Cu-Al powder bed with 1.5 wt.% Al (Figure 3b). The melting/solidification of the particles in the reaction zone is illustrated in Figure 3a. The powder located at the vicinity of the molten pool was extracted and analyzed using SEM. The micrographs in Figures 3c-e show particles that are bonded and partially fused to form a larger cluster. An EDS mapping analysis was performed on the particles observed to identify their chemical compositions. Figure 3g shows a strong green color corresponding to Al, particularly at the edges of two Cu powder particles schematized by the red color (Figure 3f). In fact, the Al powder surrounding the molten pool was also heated and melted because of its low melting point (660 ºC) as compared with Cu Figure 4a provides a summary of the pre-densification mechanism induced by Al particles during the LPBF. At a time of t 1 , the laser is applied on the powder bed to instantly create a molten pool, where both Cu and Al are heated and melted. At t 2 , the heat is transferred through the surrounding powder to the surrounding zones, where a thermal gradient is created (heat diffuses from the heated to cooler areas). In 3D printing, a part of the heat generated can be dissipated from the molten zone to the vicinity, to form an intense metal vapor.

The generated heat in the vicinity is less important than in the molten zone. Therefore, the heat impact on the surrounding powder is less. Nevertheless, according to the previous EDX map analysis, Al is more likely to melt when the laser-generated heat reaches the vicinity areas. At t 3 , Al particles fused and then solidified, creating bonds among Cu particles. XRD was performed on the samples printed for crystalline and phase evaluation, as shown in Figure 4b. The diffraction peaks at 2θ = 43 º, 50 º and 75 º correspond to (111), ( 200) and (220) planes, respectively, of the face-cubic-centered Cu [START_REF] Zhang | Microstructure and nanoindentation behavior of Cu composites reinforced with graphene nanoplatelets by electroless co-deposition technique[END_REF]. Hence, this confirms that the 3D printed Cu-Al parts form a solid solution. Apart from Cu peaks, no other peaks were detected. The lattice constant for each composition was calculated via the Le-Bail method using the FullProf Suite.

The experimentally obtained values were compared to the calculated ones. The results are plotted in Figure 4c. For pure Cu and Cu with 0.75 wt.% Al, both values are close. However, the measured values measured for Cu with 1.5 and 3 wt.% Al deviates from the calculated ones. In fact, the lattice parameter and the Al content are linear up to a maximum Al concentration, upon which the calculated lattice parameter deviates from Vegard`s law at a constant temperature [START_REF] Zhang | The parametercomposition relationship of the body centered cubic uranium-niobium alloys[END_REF].

A high-resolution TEM was performed on pure Cu and Cu with 1.5 wt.% Al samples. The micrographs in Figures 4d-e show the arrangement of the atoms within the prepared slices. The interplanar distance was found to be similar for both samples. It can be noticed that adding Al has also contributed to the formation of crystallographic defects such as dislocations and reduction in the stacking fault energy [START_REF] Goswami | Severe Plastic Deformation Induced Sensitization of Cryo-milled Nanocrystalline Al-7.5 Mg[END_REF]. Next, the LPBF of triply periodic minimal surface (TPMS) heat exchangers was performed using the pure Cu powders and Cu-Al mixtures, where gyroid structures were successfully printed using the optimized parameters for each composition. This unusual geometric configuration offers the possibility to print lightweight heat sinks with a large specific surface area, that is beneficial to the heat dissipation performance [START_REF] Alketan | Functionally graded and multi-morphology sheet TPMS lattices: Design, manufacturing, and mechanical properties[END_REF][START_REF] Gawrońska | A Numerical Study of Geometry's Impact on the Thermal and Mechanical Properties of Periodic Surface Structures[END_REF][START_REF] Kaur | Flow and thermal transport characteristics of Triply-Periodic Minimal Surface (TPMS)-based gyroid and Schwarz-P cellular materials[END_REF]. As can be seen on Figure 5a, the as-obtained complex shapes have thin and smooth features forming a large specific surface area.

Note that a clear color variation was detected on the structures when increasing the Al content.

The heat dissipation performance was measured for Cu with 3 wt.% Al, and then compared to pure Cu. Figure 5b shows the experiment set up , where the heat sinks were attached on a memory card chip using a thermal tape (3M™ 8815 Thermal Tape). The whole system was placed on a hot plate heated to 200 ºC. An IR camera (FLIR E85 24°) was used to mimic a microelectronics thermal management situation to measure the temperature of the chip. The entire system was heated to 200 ºC. An airflow was provided by a fan placed 10 cm away from the parts. Note that this experimental set-up was first established by Constantin et al. [START_REF] Constantin | Laser 3D printing of complex copper structures[END_REF] for the thermal dissipation evaluation of pure Cu. Figures 5b andc show the plot of the chip temperature with respect to the Al content, and IR images of the gyroid structures at 200 ºC. As can be seen, when the chip is placed alone on the heated plate, the measured temperature was around 169 ºC. After attaching the pure Cu heat sink to the chip, the chip temperature was reduced by 36 ºC (T chip = 133 ºC). With a gyroid composition of 0.75 wt.% Al, the dissipated heat has led to a chip temperature of T chip = 138 ºC (-31 ºC). Increasing the Al content to 1.5 wt.% and 3 wt.% Al of the gyroid structures has also contributed to the thermal dissipation process, leading to a chip temperature of T chip = 141 ºC (-28 ºC) and 146 ºC (-23 ºC), respectively. Clearly, the addition of Al has maintained the chip temperature lower than 169 ºC. Also, it can be noticed that increasing Al from 0 to 3 wt.% has slightly reduced the heat dissipation performances of the Cu-Al structures. In fact, several researchers have demonstrated that, adding increased amounts of an alloying element to pure Cu contributes to gradually decreased the TC of the material due to a lower ability to conduct the heat [START_REF] Gohar | Investigation of thermal and mechanical properties of Cu-Al alloys with silver addition prepared by powder metallurgy[END_REF]. In the current research, the SLM of Cu-Al has not only allowed to produce dense and smooth parts but also it has enabled the 3D printing of intricate shapes with great heat dissipation performance.

Conclusion

In this study, the influence of adding Al powder in Cu powder on 3D printing was investigated.

Dense and smooth Cu alloys can be printed with a large process window (i.e., scan speed and hatch distance). The results show that adding small quantities of a lightweight metal, such as Al, improves the printability of Cu, where high ED are no longer required for the SLM process.

Furthermore, the as-printed Cu-Al parts were denser than the case of pure Cu, exhibiting highly smooth, flat, and pore-free surfaces. Complex Cu-Al gyroid structures with high heat performance were also achieved using the optimized parameters. The reported results show that a composition of Cu with 1.5 wt.% Al would be the best content to obtain Cu-Al parts with high printing quality.

A further improvement of the processability of reflective metals (e.g., Cu, Al, silver) and eventually ceramics would be a great benefit to additive manufacturing applications that will lead to highly advanced multi-functional materials.

Figure 1 .

 1 Figure 1. 2D maps of the relative density with respect to the hatch distance and the scan speed, a

Figure 2 .

 2 Figure 2. SEM micrographs of a pure Cu, and Cu with b 0.75, c 1.5, d 3 wt.% Al, e Density and

Figure 4 .a

 4 Figure 4. a Illustration of the effect of Al in Cu powder during the 3D printing process, b XRD

Figure 5 .a

 5 Figure 5.a Gyroid structures printed, b Illustration of the thermal dissipation measurement, c

Acknowledgment

This study was supported by the National Science Foundation (CMMI 1826392) and the Nebraska Center for Energy Sciences Research (NCESR). The research was performed in part in the Nebraska Nanoscale Facility: National Nanotechnology Coordinated Infrastructure and the Nebraska Center for Materials and Nanoscience, which are supported by the National Science Foundation under Award ECCS: 1542182, and the Nebraska Research Initiative. The authors would like to thank Jamie Eske for her help on the English editing.

Data availability

Data generated during or analyzed during the current study are included in this published article and its Supplementary Information file.

(1084 ºC) [START_REF] Ponweiser | Re-investigation of phase equilibria in the system Al-Cu and structural analysis of the high-temperature phase η1-Al1-δCu[END_REF]. Therefore, Al is rapidly fused around the Cu powders, which clearly promotes the preliminary densification. The Al particles contribute to reduce pores and voids, leading to a greater surface finish. Also, the laser energy required to 3D print dense parts was significantly reduced. As a result, the temperature within the molten pool, and the resultant thermal gradient was decreased. Unlike printing Cu, the printing process of Cu-Al materials seemed to be less violent and more stable.

AUTHOR INFORMATION Corresponding Authors

*Jean-François Silvain : jean-francois.silvain@icmcb.cnrs.fr; Yong Feng Lu :ylu2@unl.edu.

Author Contributions ‡ Mrs. Nada Kraiem and Dr. Loic Constantin contributed equally to this work. All authors approved the final version.


Xavier Denis

Jacques-Henri Jourdan

Claude Marché

Creusot: a Foundry for the Deductive Verication of Rust Programs

Keywords: Rust programming language, Deductive program verication, Aliasing and Ownership, Prophecies, Traits

Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strict ownership policy. The strong guarantees brought by this feature opens promising progress for deductive verication, which aims at proving the conformity of Rust code with respect to a specication of its intended behavior. We present the foundations of Creusot, a tool for the formal specication and deductive verication of Rust code. A rst originality comes from Creusot's specication language, which features a notion of prophecy to reason about memory mutation, working in harmony with Rust's ownership system. A second originality is how Creusot builds upon Rust trait system to provide several advanced abstraction features.

Introduction

Critical services like transportation, energy or medicine are nowadays controlled by software, and thus verifying the correctness of such software is highly important. However, systems software is often written in low-level, pointermanipulating languages such as C/C++ which make verication challenging.

The pitfalls and traps of C-family languages are well-known; a common thread among them is the unrestricted usage of mutable pointers, which allow aliasing. When two pointers are aliased, a write through one will silently change the value pointed by the other, wreaking havoc on the programmer and verication tool's understanding of the program. Much eort has been spent trying to control and reason about aliasing. Specialized logics like separation logic or dynamic frames [START_REF] Smans | Implicit dynamic frames: Combining dynamic frames and separation logic[END_REF] give a vocabulary to express these challenges. On the other side, language features like the region typing of Why3 [START_REF] Filliâtre | A pragmatic type system for deductive verication[END_REF] or the ownership typing of the Rust programming language prevent mutable aliasing altogether. Indeed, Rust promises the performance and exibility of C with none of the memory safety issues. To make good on this promise, its ownership type system guarantees that pointers are always valid and that mutable ones are unique. The ownership discipline of Rust is enforced by a static analysis called borrow checking, which infers the lifetime of every borrow (temporary pointer), and ensures that, when mutating, only one pointer can be used to access the data, which is essential for memory safety. Once a variable is mutably borrowed, a second borrow cannot be created until the lifetime expires. Alternatively, immutable borrows can be duplicated, as one cannot modify the memory they point to. This combination of features, memory safety and low-level control, has led to Rust's exploding popularity. As Rust nds usage in key systems like Firefox and the Linux kernel, it becomes important to move beyond the safety guarantees of the language.

In 2020, Matsushita et al. [START_REF] Matsushita | RustHorn: CHC-based verication for Rust programs[END_REF] proposed a notion of prophecies to reason about the functional behavior of mutable borrows of Rust. Roughly speaking, a prophecy denotes the future value a borrow will have when its lifetime ends.

Matsushita et al. developed a proof-of-concept tool RustHorn translating Rust code to Constrained Horn Clauses, making it possible to check the validity of code assertions using automated solvers. Our tool Creusot1 allows for autoactive deductive verication of Rust code. Creusot uses a prophetic translation in the lineage of RustHorn, but aims to verify real-world programs, pushing the size, scope and features of programs far beyond RustHorn. Unlike RustHorn, Creusot has a specication language, Pearlite2 , which allows users to write function contracts and loop invariants, where logic formulas can make use of a novel operator ^(pronounced nal) to denote prophecies. Creusot has the ambition of going beyond a proof-of-concept verication tool. To support a large subset of Rust, including its standard library, it is mandatory to support the notion of traits which are a key mechanism for abstraction in Rust. Creusot not only supports the verication of Rust code involving traits, but it also builds upon the trait system to provide important features: rst, the concept of resolution of prophecies is expressed as a Resolve trait; second, logical abstraction of concrete data is provided through a Model trait which is used pervasively in our case studies.

1.1

Example: a Polymorphic Sorting Function As a motivating example, let's consider a simple generic sorting routine. We use the Gnome Sort algorithm, using a single loop that swaps out of order elements successively. We provide an implementation in Fig. 1. To verify this we face two primary challenges. The rst is genericity: to compare values of a generic type in Rust we need to use the trait Ord. The traits of Rust are like the typeclasses of Haskell: here they allow us to constrain T to have an ordering relation. In Creusot, we can add the necessary logical specications to the Ord trait, formalizing its documentation [START_REF]The Rust Community: The std::cmp::Ord trait of Rust[END_REF] stating that it must implement a total order. The second challenge is the need to handle the library Vec for vectors, providing a safe interface to resizeable arrays, despite being implemented using unsafe code. Creusot does not permit the verication of unsafe code but allows the specication of safe abstractions like Vec: we choose a model for such types, representing vectors as mathematical sequences.

#[ensures(sorted_range(@^v, 0, (@^v).len()))] #[ensures((@^v).permutation_of(@*v))] fn gnome_sort<T: Ord>(v: &mut Vec<T>) { let old_v = Ghost::record(&v); This denition is written using Pearlite, the specication language of Creusot. While Pearlite has a Rust inspired syntax, it adds several constructs like quantication forall<..>, or implication ==>. Using these we can say a sequence is sorted if for any ordered pair of indices the values at those indices respect the order on T. On line 1 of Fig. 1, we use this denition with two more Pearlite operators: the model operator (@) (syntactic sugar for the Model trait), and the prophetic operator nal (^). The nal operator provides access to the value of a mutable borrow at the end of its lifetime; here we use it to talk about the value the vector pointed by v has after the function call. The second postcondition on line 2 makes use of a similar helper predicate permutation_of to require that the nal value of v is a permutation of its initial value. To prove these postconditions we provide two loop invariants (lines 6-7). The rst states that the segment of the vector before i is sorted, while the second states that the vector at each iteration is a permutation of the input. To state this invariant about permutations we make use of the Ghost type, to record a ghost value which does not exist at runtime but does during proof, allowing us to remember the original value of v. The annotated program is fed through Creusot, which translates it to Why3. In turn, Why3 generates and discharges the verication conditions in under 2 seconds using automated provers including Z3 [START_REF] De Moura | Z3, an ecient SMT solver[END_REF], CVC4 [START_REF] Barrett | CVC4[END_REF] and Alt-Ergo [6].

let mut i = 0; #[invariant(sorted_range(@*v, 0, @i))] #[invariant((@*v).permutation_of(@*@old_v))] while i < v.len() { if i == 0 || v[i -1] <= v[i] { i += 1; } else { v.swap(i -1, i); i -= 1; } } }

Contributions

Our contributions, and the structure of this paper, are summarized as follows.

In §2 we give an introduction through the Pearlite specication language and the verication process of Creusot. This section illustrates how prophecies are integrated in Pearlite. In §3, we explain how Creusot translate Rust functions into Why3 functions, this section explains how we generate the verication conditions for mutable borrows. In §4 we rst present in deeper details how Rust traits are interpreted by Creusot, and in a second step we discuss the specic Creusot traits used in borrow resolution and in data abstraction. In §5 we present an overview of the implementation of Creusot and an experimental evaluation of the tool on a set of benchmarks. We discuss related work in §6.

Notice that due to space limitations, we focus here on the original features of Creusot and refer to an extended research report [8] for more details.

Specifying and Proving Programs using Prophecies

To formally specify the intended behavior of programs, one can use so-called Behavioral Interface Specication Languages [START_REF] Hatcli | Behavioral interface specication languages[END_REF], such as JML for Java [START_REF] Cok | OpenJML: Software verication for Java 7 using JML, OpenJDK, and Eclipse[END_REF], ACSL for C [START_REF] Baudin | ACSL: ANSI/ISO C Specication Language, version 1.16[END_REF] or Spark for Ada [START_REF] Mccormick | Building High Integrity Applications with SPARK[END_REF]. Creusot follows this tradition by introducing the Pearlite specication language, where Rust functions are given contracts which specify preand postconditions: logic formulas which respectively hold at the entrance and exit of a function call.

Traditionally, specication languages introduce specic contract clauses to specify the behavior of pointers such as the assignable or assigns in ACSL and JML. Pearlite has no equivalent clause. Instead specications can refer not only to the value of a borrow at function entry but also to its value at the end of its lifetime: this is the notion of prophecies that we detail in §2.2.

Background Logic

The background logic of Pearlite is a classical, rst-order, multi-sorted logic.

Each Rust type corresponds to a sort in this logic. The logic connectives denoted by &&, || and ! mirror their Rust counterparts, but Pearlite also introduces ==> for implication, and the quantiers forall<v:t> formula and exists<v:t> formula. Atomic predicates can be built using custom logic functions and predicates, constant literals, variables and built-in symbols, a central case being the logical equality denoted by a tripled equal sign (===) and dened on any sort. This logical equality is the symbol interpreted to the set-theoretic equality in a set-based semantics. This distinguishes it from the program equality of Rust, ==, which is sugar for PartialEq::eq. Finally, Pearlite has support for logical sorts which do not exist in Rust, like Int, the unbounded mathematical integers, or like Seq<T> the generic sort of mathematical sequences. A syntactically valid formula is thus for example: A useful feature of Pearlite is the introduction of user lemmas using the so-called lemma function construction. To achieve this, one provides a contract to a logical function returning (). By proving the contract valid, one obtains a lemma stating that for all values of arguments, the preconditions imply the postconditions. This construction is even able to prove lemmas by induction.

Here is an example (detailed in [8]):

#[logic] #[requires(x >= 0)] #[variant(x)] #[ensures(sum_of_odd(x) === sqr(x))] fn sum_of_odd_is_sqr(x:Int) { if x > 0 { sum_of_odd_is_sqr(x-1) } }
This code is automatically proved conforming to its contract. Any call to this function would then add the hypothesis ∀x, x ≥ 0 ⇒ sum_of_odd(x) = x 2 in the current proof context.

Borrows and Prophecies

We illustrate the use of prophecies to specify mutable borrows in Fig. 2. The function pick returns, depending on its rst boolean parameter, either its second or third argument. We wish to show that the client pick_test returns 42. For that purpose, pick must be given an appropriate contract: namely the postcondition of lines 1 and 2. The rst part of the postcondition states that the result of pick (denoted by the identier result) is either x or y, depending on the value of t.

Importantly, when we say result === x (i.e., when t === true), we are stating that the borrow result, which is a pointer, is equal to the borrow x, not merely the values being pointed. In particular, this captures that writing through the returned pointer aect the variable pointed to by x. In pick_test, this entails that the nal value of a is 6. The second part of the post-condition is needed to state that the other borrow parameter (y when t === true) is released so the caller knows the value it points to can no longer change until the lifetime 'a ends. This is specied using a prophecy. For any mutable borrow b, one can write ^b in Pearlite to denote its nal value, the value the variable it points to will have when the lifetime expires. Prophecies act like a bridge between the lender and borrower, when a borrow is released we recover information which allows us to update the value of the lender. Releasing a mutable borrow is equivalent to stating that the current value of the borrow, *b, equals its nal value, ^b. We refer to this process as the resolution of the borrow. Thanks to the resolution, we can prove the postcondition of pick and deduce in pick_test that the value of b at line 11 is its original value 7. The nal value of a borrow is a logical artifact: it is not necessarily known at runtime when the specication mentions it, but one can prove [START_REF] Matsushita | RustHorn: CHC-based verication for Rust programs[END_REF][START_REF] Matsushita | RustHornBelt: A semantic foundation for functional verication of Rust programs with unsafe code[END_REF] that it is sound to prophesize it in the logic. Note that the rst equality (i.e., result === x when t === true) actually implies the equality ^result === ^x, as we are asserting that result and x are completely indistinguishable. This explains why the rst equality is enough to specify that a mutation through the borrow result causes a mutation of the variable pointed to by the argument x (when t === true). Since they both have the same prophecy, modications to the memory pointed to by result will aect the lender of x.

The approach is detailed and validated in prior work [START_REF] Matsushita | RustHorn: CHC-based verication for Rust programs[END_REF][START_REF] Matsushita | RustHornBelt: A semantic foundation for functional verication of Rust programs with unsafe code[END_REF].

Handling Rust Function Bodies

Creusot translates Rust programs into WhyML, the programming language of Why3. Rather than starting from source level Rust, translation begins from the Mid-Level Intermediate Representation (MIR) of the Rust compiler. MIR is a key language in the compilation of Rust and is the nal result of desugaring and type checking Rust code. Many tools that wish to consume Rust code target MIR. There are rich APIs to access, extract and manipulate MIR code. Furthermore, MIR is created after type checking and is the representation on which Rust's agship static analysis borrow checking is formulated. MIR is also the language modeled in RustHornBelt [START_REF] Matsushita | RustHornBelt: A semantic foundation for functional verication of Rust programs with unsafe code[END_REF] to prove the correctness of prophetic translation. Thus, we want to design our translation from MIR to Why3 so the generated verication conditions are as close as possible to those proved sound in RustHornBelt. MIR programs are unstructured: they are represented as a control-ow graph (CFG) whose nodes are basic blocks composed of atomic instructions (borrowing, arithmetic, dereferencing, etc.) each terminated by a function call, a goto, a switch, an abort or a return. To verify a MIR program, we nd ourselves needing to calculate the weakest-precondition (WP) of a function represented as a CFG. We achieve this using a dedicated Why3 input front-end called MLCFG, that reconstructs a structured WhyML code from a control ow graph, and then use Why3's carefully designed WP computation algorithms.

Translating Owned Pointers

The ownership discipline of Rust makes a simple translation of (mutable) owned pointers possible. Consider the case of a local variable x containing an owned pointer to the heap (i.e., of type Box<T> for some type T). Then, we know that mutating memory through x can only be observed by a read using variable x. Therefore, if t is the translation of type T, then we can translate type Box<T> to type t as well. An assignment through the pointer *x = e is simply translated to the assignment: x = e , where e is the translation of e. Using the pattern of prophecies for encoding mutable borrows into a functional language poses a diculty: when we create a borrow, we obtain a new prophetized value which comes out of thin air. We won't know anything concrete about this prophecy until the borrow is resolved at the moment it is dropped, and then at the lifetime's end the lender will have the value of this same prophecy.

In between these points there can be arbitrary control ow, ownership changes, or reborrowing. We may no longer know who the lender of a borrow was at its lifetime's end, and therefore have no way to propagate the prophecy to the lender. Our solution may be surprising: we update the lender with the prophecy at the moment of the borrow's creation, foreseeing all the mutations that will occur. This is valid because the value of the lender cannot be observed before the lifetime's end. As a result, the creation of a borrow let y : &mut T = &mut x;

is translated into y : borrow t <-{ current = x ; final = any t }; x : t <-y.final;

where any t is the WhyML non-deterministic construct which returns an arbitrary value of type t. It encodes the fact that the nal value is not yet known, it is thus prophetized. The second line gives to x the nal future value of y.

An important other case occurs when a borrow is dropped, where we insert a resolution statement: The contents of a WhyML assume clause states a fact as a trusted hypothesis for subsequent statements. Resolution corresponds to the fact that at this point the value pointed to by the borrow will not change, and therefore its prophecy has been fullled.

The simplied translation of the pick example, from Fig. 2, is given in Fig. 3. See [8] for more details. The postcondition of pick_test and pick are proven using Why3 and SMT solvers.

Support for Rust Traits

Rust makes heavy use of a trait system to implement abstractions. Like typeclasses in Haskell, traits allow functions, types or constants to be associated to specic types, and can automatically select the correct instance at each call-site.

The trait system enables ecosystem-wide modularity and many common operations are expressed using traits, such as equality in the PartialEq and Eq traits, order relations in PartialOrd and Ord, and accessing collections in the Index and IndexMut traits. Supporting Rust's trait system is necessary for a verication tool, they manifest themselves in even the most basic programs, like Fig. 1. In this section, we explain how traits can be used in Creusot to modularly verify programs. But Creusot not only veries programs using traits, it also uses traits for some of its core features: the Resolve and Model traits. The trait PartialOrd implements a heterogenous partial order: instances must provide implementations for all of lt, gt, le, ge, and partial_cmp. Additionally, the ocial documentation [START_REF]The Rust Community: The std::cmp::Ord trait of Rust[END_REF] requires that these denitions are mutually compatible, for example: if a.le(b) then a.lt(b) || a.eq(b). This is an example of a law for PartialOrd. In Creusot, laws can be included in traits using the #[law] annotation and written in the style of lemma functions (see §2.1). A particularity of trait laws is their auto-loading: whenever we use any associated item of a trait or implementation, we will bring into scope any laws from that trait.

Traits can be arranged into a hierarchy, with sub-traits rening or expanding upon their super-traits. The sub-trait Ord strengthens the specication of PartialOrd, requiring the order to be total and homogeneous. The laws of Ord constrain the behavior of functions dened in the super-trait PartialOrd. In Fig. 4 we present a simplied version of our specications for Ord (see [8] for more details). We require a denition of cmp_log and a proof of transitivity.

Each time a user makes use of a comparison operation, Creusot will load the laws of Ord, allowing us to leverage the transitivity of our order. Every implementation of a trait for a specic type must rene the contract of the trait. It must weaken preconditions and strengthen postconditions. This possibility of renement allows implementations to provide stronger contracts which leverage specic knowledge of the type the trait is being implemented for.

Whenever a trait method is used, Creusot will use the most specic contract possible. Performing the translation to Why3 of all such dierent usage of traits is indeed highly non-trivial: it relies on algorithms for construction of specic dependency graphs which are detailed in our research report [8].

The Resolve Trait

We use traits to generalize the notion of resolution discussed in §3.2, as follows.

#[trusted] trait Resolve { #[predicate] fn resolve(self) -> bool; }

Much like how Rust's Drop trait allows types to customize their program destructors, we use the Resolve trait to dene the knowledge gained from resolving a specic type. Following discussion of §3.2, the Resolve trait is given the following implementation for mutable borrows: unsafe impl<T> Resolve for &mut T { #[predicate] fn resolve(self) -> bool { pearlite! { ^self === *self } } } so indeed, when a mutable borrow r is resolved, instead of assuming ^r === *r, Creusot will assume the equivalent assertion r.resolve().

Because Resolve represents information that is assumed about a type, an incorrect implementation can introduce unsoundness to Creusot, for this reason we mark the trait as #[trusted], and require all implementations to do the same. This mirrors the notion of unsafe trait in Rust for those traits where a malicious implementation could introduce undened behavior in safe code.

The Resolve trait makes it possible to generalize the resolution mechanism to data structures containing mutable borrows, like vectors of borrows, pairs of pairs of borrows, etc. For example, when we resolve a pair p of mutable borrows, we wish to learn that both components of p are resolved, that is, *p.0 === ^p.0 && *p.1 === ^p.1. To achieve this goal, we give the following implementation of the Resolve trait for pairs: Like Drop, we need to be able to resolve a value of any type, but we don't have the benet of being a rst-class language feature of Rust. We solve this using a cutting-edge feature of Rust, specialization. This allows us to provide a generic implementation for every type T, and then provide more specic instances which specialize resolution. In practice, this means users can write x.resolve() for any value, and never need to constrain generic parameters to implement Resolve.

4.3

Specifying with Models: the Model Trait Traits provide a convenient mechanism for abstracting specications, just like in programs. When working with complex data structures we wish to treat their specications in terms of a model which abstracts away implementation details.

For example, we may wish to view a HashMap as a mathematical map between two types, or a Vec as a sequence of values. To do this, we provide a function which shows how to interpret concrete values as members of the model. In certain cases (like Vec in Creusot), we may even take the existence of this function as an axiom. This design pattern is common enough that we can capture it in a trait.

trait Model { type ModelTy; #[logic] fn model(self) -> Self::ModelTy; } Each implementation of the Model trait species the type of the model and a function to interpret itself as a value of that type. By making this a trait, we can provide convenience instances that improve ergonomics. Creusot goes further and provides syntactic sugar for this trait. Rather than using x.model(), users can write @x where appropriate. Apart from this small sugar, models purely are a library concern, Creusot as a tool has no specic awareness of them.

Experimentation and Evaluation

We evaluated the performance of Creusot on a wide range of benchmarks.

These benchmarks make heavy use of polymorphism and traits. Additionally, we improved on the benchmarks of other tools by proving additional functional properties. The evaluation shows that Creusot's approach scales well, with verication times remaining low even in complex examples. Furthermore, it provides evidence that our prophetic specications are well-suited and concise.

Implementation Like many other Rust verication tools, Creusot is implemented as an extension of the Rust compiler, and integrates easily into standard Rust workows. The total implementation including the `verication standard library' of Creusot totals 14k lines of code, published under an LGPL license, available at https://github.com/xldenis/creusot/. During execution Creusot translates Rust libraries into MLCFG and outputs the result to a le. The resulting le can then be loaded in Why3 and veried using either its IDE or command line

.

Language Support Creusot supports a large subset of safe Rust, including structs and enums, all forms of borrowing, loops and recursions. As we discussed in this paper, we also support polymorphism and traits, including associated types and functions, and super traits. Furthermore, we extend Rust with both logic functions and predicates, which can be used in the specications of functions and traits. Creusot also allows types like Vec to be axiomatized so their safe clients can still be veried. the time Why3 takes to run the provers. The Has traits? measures whether the test case has a function with a generic parameter constrained by a trait. Tests marked with † required a few manual proof steps in Why3 IDE [START_REF] Dailler | Lightweight interactive proving inside an automatic program verier[END_REF].

Has

Evaluation We measure the verication performance for programs translated with Creusot. We adapted and generalized programs from the Prusti [START_REF] Astrauskas | Leveraging Rust types for modular specication and verication[END_REF] benchmark suite, additionally strengthening the veried properties. Other examples were inspired from the Why3 gallery [START_REF] Bobot | Let's verify this with Why3[END_REF], Rosetta Code [18] or RustHorn [START_REF] Matsushita | RustHorn: CHC-based verication for Rust programs[END_REF].

Note that Why3 has support for a wide range of manual proof tactics that allow users to setup proof structure before handing o obligations to provers.

As these can dramatically help verication, we avoid them in our evaluation and instead apply a standard proof strategy to all examples. Each example is proved using Why3's Auto Level 2 strategy, a common rst step when verifying programs with Why3. One benchmark required a small number of additional manual proof steps, Sparse Array, to prove a complex lemma about injections between sequences.

Our evaluation was performed using a 2016 Macbook Pro running macOS [START_REF] Hubert | Separation analysis for deductive verication[END_REF]. Sparse

Array is an example from the VACID-0 benchmarks [START_REF] Leino | VACID-0: Verication of ample correctness of invariants of data-structures, edition 0[END_REF]. The proof involves a mathematical lemma with a few steps of manual proof [START_REF] Dailler | Lightweight interactive proving inside an automatic program verier[END_REF] before sending the sub-goals to SMT solvers. In Place List Rev. is the in-place linked-list reversal procedure, classically used as an illustration of reasoning in separation logic. It is remarkable that the Rust code for that can be veried without the need for separation logic.

Our RustHorn tests show that we maintain the verication performance of RustHorn, as these examples are rapidly veried by our provers. While some manual annotation is required, even for safety, the overhead is low, and mostly consists of stating the properties we wanted to prove in the rst place.

The Prusti examples listed here are derived from their introductory paper in 2019 [START_REF] Astrauskas | Leveraging Rust types for modular specication and verication[END_REF]. In their paper they provide two versions for their functions, the rst proving only safety while the second proves portions of functional correctness.

The dierence in verication performance is made evident by the Knapsack 0/1 example of Prusti. This example solves the 0/1-Knapsack problem using the traditional dynamic programming approach. Prusti takes over 2 minutes to verify the safety of the problem, whereas our proof of safety passes in approximately 4 seconds. This dierence in performance helps us go further, being able to rapidly check proofs allows for faster iteration, which enabled us to extend this example with a complete proof of functional correctness. Our version of the Knapsack Problem with functional correctness takes longer to verify, with the proof passing in approximately 6 seconds.

Related Work

RustHorn [START_REF] Matsushita | RustHorn: CHC-based verication for Rust programs[END_REF] laid the foundations for Creusot by developing a prophetic encoding of mutable borrows and applying it to Rust. It translates MIR programs directly to Constrained Horn Clauses where existing dedicated automated solvers can be thrown at the task. Creusot on the other hand introduces an intermediate step: we translate rst to an intermediate language which is then lowered to rst-order logic (FOL) by calculating weakest-preconditions. As a tool RustHorn remains a proof-of-concept, it supports a core fragment of Rust: algebraic data types, borrows, simple loops and arithmetic and polymorphism.

There is no support for unsafe types like Vec or for traits like Eq. Moreover, RustHorn has no specication language, it is limited to the verication of program assertions, which are by essence limited to executable boolean expressions on program variables, without any way to relate them with an abstract model. It relies entirely on automation to infer both function postconditions and loop invariants, meaning a seemingly small change can cause verication times to spiral out of control or fail unpredictably. While not an automated verier, RustHornBelt mechanizes a proof of soundness for prophetic verication of Rust [START_REF] Matsushita | RustHornBelt: A semantic foundation for functional verication of Rust programs with unsafe code[END_REF], by extending the prior RustBelt proof. The proof shows that the uniqueness and lifetimes of mutable borrows enables prophetizing their nal values, placing Creusot's approach on solid theoretical grounds. However, there remains a gap between an implementation like Creusot and the mechanization. In particular, the language of RustHornBelt λRust makes a number of simplifying assumptions when compared to MIR, like boxing function parameters or using a CPS structure for the programs. Furthermore, RustHornBelt establishes the soundness of the nal verication conditions directly but Creusot introduces an intermediate step by targeting a functional language.

Prusti [START_REF] Astrauskas | Leveraging Rust types for modular specication and verication[END_REF] is another deductive verier for Rust, based on the Viper separation logic platform. It does not use a prophetic encoding, instead modeling ownership using permissions. Like Creusot, Prusti has a specication language which can be used to give contracts and invariants. Because Prusti has no notion of prophecy, it does not use the nal operator (^) to specify mutable borrows, instead using pledges. A pledge is an assertion that is guaranteed to hold at the time when the borrow expires, which is not necessarily in the body of the function. In contrast, the nal operator of Creusot brings prophecies as rst-class objects in the specication language, to specify the future values of borrows. The semantics of Prusti specications were designed to preserve the behavior of program assertions when lifted into pure contracts. In particular, arithmetic in Prusti's specications is machine arithmetic and has to be checked for overow. Creusot takes a dierent approach by using a more abstract specications language (Pearlite), which is usually easier to reason with. A consequence of this dierence is that Pearlite logical functions cannot be executed, while Prusti's pure functions can be used in programs. While Prusti's permission system supports the common borrowing patterns of Rust, it struggles with patterns like reborrowing in a loop (e.g., All Zeros List 5), with data structures containing borrows like pairs of mutable borrows 5, or with nested borrows. In contrast, Creusot's translation of Rust types using prophecies for mutable borrows is general and compositional: we place no restrictions on the usage of mutable borrows or their position within types. Another noticeable dierence with Prusti lies in the choice of the underlying logic. Prusti encodes specications into separation logic and delegates verication to Viper, whereas Creusot encodes them into FOL and delegates verication to SMT solvers via Why3. Prusti chooses to verify Rust's ownership discipline with Viper, while Creusot depends on Rust's borrow checker for that, which means Creusot relies on the soundness of Rust's type system and of its implementation. We believe this dierence explains the signicant blow-up in verication times: on simple examples verication takes an order of magnitude more time than with Creusot. The simpler underlying logic in Creusot, allows it to benet from Why3's mature infrastructure to manage a herd of automated provers and a tactic system to provide guidance when they go astray. Both Prusti and Creusot support traits and polymorphism. However, because mutable borrows need special care in Prusti, a generic Rust function cannot be instantiated with a mutable borrow, which causes no problem in Creusot. Moreover, properties of traits in Prusti are specied using only pre-and postconditions; we use laws for specifying such properties, which we nd more exible.

Aeneas [START_REF] Ho | Aeneas: Rust verication by functional translation[END_REF] is a novel verier for Rust targeting interactive verication of programs in established proof assistants like F * or Coq. To achieve this they also translate Rust programs to functional programs in a State-Error Monad. Instead of using prophecies they use backwards functions to reconstruct the value of a lender has after the borrows expiry. This approach appears to have a deep and close link to prophecies as used by Creusot, instead of using non-determinism to pull the value out of thin air, Aeneas constructs the actual witness of this value.

The constructive approach that Aeneas takes may very well be better suited to interactive provers which traditionally prefer constructive logics. Aeneas also makes the choice of using so called extrinsic proofs, all specication and proof work is done in the prover, with no annotations present in Rust. While this allows them to leverage all the existing tools in the underlying prover, the proof engineer must manually sync these proofs and specications with the Rust code as it evolves. This attests to the dierent audiences targeted by the tools, Aeneas seeks to enable the users of existing advanced verication tools to perform more ergonomic verication using their traditional toolkits, while Creusot seeks to bring verication to regular engineers. In terms of language support, Aeneas is currently more limited than Creusot, it has no support for loops, nested borrows or traits.

Beyond the Rust ecosystem, Spark/Ada is a tool suite for deductive verication of Ada programs. For a long-time, it was restricted to a subset of Ada without pointers. Support for pointers was added in 2020 [START_REF] Jaloyan | Verication of programs with pointers in SPARK[END_REF], based on an ownership policy similar to Rust's. At the start Spark used a notion of pledges similar to Prusti's, but they have now replaced it with prophecies. Similarly to Creusot, Spark/Ada makes use of the ownership information computed by the compiler to encode specications and code into a rst-order logic, instead of relying on a separation logic.

Fig. 1 .

 1 Fig. 1. Gnome Sort and its specication.

  forall<x: Int> x >= 0 ==> exists<y: Int> y >= 0 && x * x === x + 2 * y See [8] for more technical details on the background logic. Pearlite formulas are type-checked by the front-end of the Rust compiler, but they are not borrowchecked. Hence values can be used in logic functions or predicates, even if the Rust ownership rules would forbid copying them.

#

  Fig. 2. A toy example illustrating prophecies in the specication language.

Fig. 3 .

 3 Fig. 3. Simplied translation of the projection pick example in MLCFG.

  Fig. 4. A simplied Ord trait with specications

  unsafe impl<T1: Resolve, T2: Resolve> Resolve for (T1, T2) { #[predicate] fn resolve(self) -> bool { pearlite! { self.0.resolve() && self.1.resolve() } } } Then, resolving x: (&mut T, &mut T) would expand into the resolution of each component of the pair.

  Rust variable of type &mut T is translated by Creusot as an object of type borrow t, where t is the translation of T. The Pearlite notations *x and ^x are translated into x.current and x.final.

	3.2	Translating Borrows to Prophecies in Why3

Just like in RustHornBelt, borrows are translated into pairs of a current value and a nal value. Hence, we introduce a new polymorphic record type in Why3: type borrow 'a = { current : 'a ; final : 'a } A

Table 1 .

 1

		Has	Spec. # of		Additional
	Name	generics? traits? LOC LOC VCs Time (s) Properties
	Inc Some List	25	22	4	0.98	Func. correctness
	Inc Max	12	3	2	0.53	Func. correctness
	Inc Max Many	13	3	2	0.74	Func. correctness
	Binary Search	21	20	31	2.15	Func. correctness
	Knapsack 0/1	32	52	81	3.94
	Knapsack 0/1	32	106 113	5.96	Func. correctness
	Knuth Shue	9	11	1	0.30	Permutation
	100 doors	18	6	3	1.08
	Heap Sort	30	71	125	14.6	Func. correctness
	Selection Sort	15	27	30	2.14	Func. correctness
	Gnome Sort	11	17	31	2.06	Func. correctness
	Filter Vector	21	39	6	0.98
	Sparse Array †	47	75	37	4.86	Func. behavior
	In place List Rev.	12	10	1	0.55	Func. correctness
	All Zero List	11	10	1	0.64	Func. correctness
	Swap Pair	9	3	2	0.48
	HashMap	50	111	71	5.43	Func. correctness

Selected results of our evaluation. The column LOC indicates the lines of program code (excluding blank lines) we verify. The column Spec. LOC measures the lines of specications (excluding blank) used. # of VCs measures the number of verication conditions that are sent as proof tasks to CVC4 or Z3. Time (s) measures

Le Creusot is an industrial town in the eastern France, whose economy is dominated by metallurgical companies, cf. https://en.wikipedia.org/wiki/Le_Creusot

Pearlite is a structure occurring in common grades of steels, cf https://en.wikipedia. org/wiki/Pearlite

Note to reviewers: the page at https://www.lri.fr/~xldenis/icfem2022/ provides de- tailed instructions on how to reproduce the experiments below.