O Chesneau
email: olivier.chesneau@ob-azur.fr

G C Clayton

F Lykou

O De Marco

C A Hummel

F Kerber

Eric Lagadec

J Nordhaus

A A Zijlstra

A Evans

A dense disk of dust around the born

Keywords: Planetary Nebulae-Individual: Sakurai's object (V4334 Sgr) Techniques: interferometric, Techniques: high angular resolution, Stars: AGB and post-AGB, Stars: circumstellar matter, Stars: mass-loss

published or not. The documents may come

Introduction

Sakurai's Object (V4334 Sgr), first detected in 1996, is the central star of a planetary nebula (CSPN), that experienced a Very Late Thermal Pulse (VLTP), a helium-shell flash while on the white dwarf cooling track that can influence the late evolution of low-mass stars (Herwig 2001, Lawlor & MacDonald 2003, Hajduk et al. 2005). The extended very faint planetary nebula (PN) bears witness to the previous evolution of this star, confirming that the latest large mass ejection during the PN phase occurred several thousands years ago (Kerber et al. 1999). This new 'final flash', which began 12 years ago, returned the star very briefly to the Asymptotic Giant Branch (AGB) stage, explaining why these sources are often called 'Bornagain' objects. As such, a final flash is astronomically very brief (only a few tens of years), so that the observation of such an event is rare. Only the event experienced by V605 Aql can be considered as directly comparable (Clayton et al. 2006, Clayton & De Marco 1997). V605 Aql underwent a final flash in 1917 and appears today to be still embedded in a disk-like dust structure (Clayton et al. 2006, Hinkle et al. 2008).

The analysis of the very rapid evolution of the spectral energy distribution (SED) of Sakurai's Object (Eyres et al. 1999;Kerber et al. 1999;Tyne et 2002;Käufl et al. 2003;Eyres et al. 2004;Evans et al. 2006;Worters et al. 2008) has suggested that the average dust grain size has been increasing and probably the rate of dust formation has been increasing as well. The results were mainly based on modeling of radiative transfer in a spherical dust shell. Tyne et al. (2002) suggested that the source was expanding and might be resolvable by 8-10m class telescopes in the mid-IR. Kerber et al. (2002) discovered of a fast outflow from the source and suggested a bipolar morphology for the fast moving gas seen in optical spectra. Recently, it has been suspected that there is a strong asymmetry in the circumstellar shell around Sakurai's Object, but the dust shell itself had yet to be resolved in the optical or near-IR (Evans et al. 2006, van Hoof et al.(2007)).

Observations using the Very Large Telescope Interferometer are presented in Section 2. In Section 3 we derive some physical parameters of the dust shell using 2D radiative-transfer models and we discuss the results in Section 4. Calibrators: HD152334 K4III 3.99±0.07 mas, HD163376 M0III 3.79±0.12 mas, HD169916 K1III 3.75±0.04 mas, HD177716 K1III 3.72±0.07 mas.

Observations

The source was observed in June 2007 with MIDI (Leinert et al. 2003, Ratzka et al. 2003) the mid-IR recombiner of the Very Large Telescope (VLT). The MIDI/VLT Interferometer operates like a classical Michelson interferometer combining the mid-IR light (N band, 7.5-13.5 µm) from two VLT Unit Telescopes (8.2m, UTs). A typical MIDI observing sequence was followed, as described in Ratzka et al. (2007). MIDI provided single-dish acquisition images with a spatial resolution of about 250 mas at 8.7 µm, a flux-calibrated spectrum at low spectral resolution (R=30) and 6 visibility spectra from the source. The observations were performed in High Sens mode, implying that the photometry of the source is recorded subsequently to the fringes. The visibility errors range from 8% to 15%. The accuracy of the absolute flux calibration is better than 10%. The log of the observations is given in Table 1. We used two different MIDI data reduction packages: MIA, developed at the Max-Planck-Institut für Astronomie, and EWS, developed at the Leiden Observatory (MIA+EWS1 , ver.1.5.1).

The MIDI images show that the core is unresolved at 8.7 µm, implying that its angular diameter must be less than 150-200 mas. The mean level of the visibility spectra is low, indicating that the source is well resolved by MIDI/VLTI (typical scale 30 x 40 mas), but the spectral modulation indicates a complex source (see Fig. 2). Significant differential phases (±10-20 • peak-to-peak) were observed for all baselines except Sak.4 and Sak.5 (Table 1), which exhibit phases close to zero (±5 • ).

The data are complemented by two Spitzer/IRS spectra obtained in April 2005 and May 2007 (Evans et al. 2006, Evans et al. 2009, in preparation), and a continuum-subtracted [O III] image of the surrounding PN acquired in October 2002 with the instrument VLT/FORS1 (Hajduk et al. 2005)

Physical parameters of the disk

The large, spectrally dependent variations of the MIDI visibilities could be interpreted in the context of double point or ring structures. Simple models fail to account for the complex visibilities observed, although the difference between the mean level of the visibilities from the baseline UT2-UT3, compared to those obtained with UT3-UT4 suggest a flattened structure with an orientation of the major axis of approximately 110-140 • . The differential phases point to a significant asymmetry in the direction of the minor axis, i.e. ∼45 • . We made use of the continuum Monte Carlo radiative transfer code MC3D (Wolf 2003; see also Wolf et al. 1999), that solves the radiative transfer problem self-consistently. We use a classical model of a stratified disk of dust (Chesneau et al. 2006, 2007 andreferences therein). The dust density follows a 2D law (both radial and vertical):

ρ(r, z) = ρ 0 R ⋆ r α exp        - 1 2 z h(r) 2        ( 1
)
where r is the radial distance in the midplane of the disk, α is the density parameter in the midplane, R ⋆ is the stellar radius and the disk scale height, h(r), is given by h(r) = h 0 (r/R ⋆ ) β , where h 0 is the scale height of reference, and β is the vertical density parameter.

The absence of spectral features in the IR indicates that the dust is dominated by amorphous carbon grains. We assume the standard interstellar grain size distribution (Mathis et al. 1977) with spherical grain radii extending from 0.005 to 1 µm. We estimate the outer radius of the disk to be 500 AU consistent with an expansion since 1997 at a maximum velocity of 100 km s -1 . The initial parameters (T eff of the source and dust mass) were chosen following van Hoof et al. (2007). The outputs from the code are described in Chesneau et al. (2006Chesneau et al. ( , 2007)). The distance, luminosity, and temperature of the central star are uncertain by a large factor (Jacoby et al. 1998). We first fixed the distance to be 1.5 kpc, but no satisfactory models could be found. By increasing the distance, the fit of the visibility curves and the SED steadily improved and we achieved the best fit model for a distance of 3.5 kpc, a value close to the distance favored by van Hoof et al. (2007). We note, however, that we did not explore the parameter space for larger distances and that the distance chosen is by no means a strong constraint. Our priority in this study was Fig. 2. MIDI visibilities with their error bars, compared with the best model (dashed-dotted lines, see Table 2). The χ 2 values of the fits of 16.5, 7.1, 7.8, 7.6, 5.2, 4.6. The reduced χ 2 for the full data set is 8.2.

to obtain the best possible definition of the the geometry of the source, by fitting the visibility curves. We were not able to find a model with a good match to both the visibility curves and the SED. The best model, presented here, is the one showing the highest flux although it is still too low. Some models with slight modifications of the parameters provided better fits to the visibilities (best χ 2 ∼6). Given the very short timescale to form the disk, and the large scale height inferred, a stratified disk might not be the best model to account for the density profile of the dust. A slowly expanding torus (Peretto et al. 2007) should be investigated in the future.

Results and discussion

The MIDI observations provide direct evidence for a thick, highly-inclined disk or torus (which therefore efficiently screens the central source), whose parameters are described in Table 2. The orientation of the major axis of the disk (134±5 • ) coincides with the asymmetry detected in the old PN (130±8 • ). A similar orientation is also mentioned in Kerber et al. (2002). Such an alignment between the disk and PN may not be fortuitous. In the case of V605 Aql, the disk and the planetary nebula A58 share the same major axis (Hinkle et al. 2008). Of importance too, is the low level of asymmetry detected in the old PN compared to what is currently observed in the disk. Is the new mass loss more asymmetric or is the smaller asymmetry of the PN remnant due to evolution and old age? Another related object worth mentioning is A 30, a PN that suffered its own VLTP a few thousand years ago (Borkowski et al. 1995). The inner nebula exhibits a thin equatorial disk, currently being eroded by the fast wind of the central star, whereas its old PN is perfectly round.

The disk is very optically thick and at 8 µm, most of the light emerges from a small region above the North pole (see Fig. 4). The scale-height of the disk/torus is very large, limiting the opening angle of the polar regions, reminiscent of the long-lived 'wall' structure seen in the binary post-AGB HR 4049 Dominik et al. (2003). Spherical models of the dust shell explain the shift of the peak of the SED toward longer wavelengths by suggesting that the inner boundary has receded from the star (Käufl et al. 2003, Evans et al. 2006). If this indicated a cessa-tion of mass loss and dust formation, then the optical depth of dust would drop very quickly, assuming that the dust is moving radially away from the star. The estimated size of the Sakurai's Object disk from our observations in 2007 is small compared with previous estimates, and implies that the high velocities inferred from spectral lines may not be consistent with the dust expansion. If the expansion velocity were consistent with the rapid motions observed for CO and optical lines, the disk should already be resolvable by 8-m class telescope in the infrared (Eyres et al. 2004, Kerber et al. 2002, Worters et al. 2008).

The fast spectral evolution of the source toward lower temperatures, as witnessed by the Spitzer and MIDI spectra, must be interpreted by a growing opacity of the disk, whether by accumulation of new material or by grain growth. Only the continuous production of new dust and/or grain growth can explain the shift of the SED of the disk toward longer wavelengths. A more rapid expansion of the disk as an explanation for the SED evolution has been ruled out by the smaller disk size reported here. Since the dust on the inner rim of the disk is close to the sublimation temperature, and the outer radius is not well constrained by the N-band measurements, a dust expansion rate cannot be accurately estimated. Keplerian motion (i.e. with a very low radial expansion) of the dust in the disk cannot be excluded.

The discovery of a flattened structure such as a disk is of great importance to the future interpretation of the outburst of Sakurai's Object and the VLTP phenomenon, as much of the previous work is based on the assumption of a spherical ejection. Disk models may do a better job of fitting the observed parameters. A well-known consequence of applying a 1D radiative transfer code in the dust to a 2D astronomical source is that the dust is put much farther than in reality, biasing strongly all the inferred parameters.

The formation of a disk/torus could be explained by two classes of models: those involving an intrinsic asymmetry of the ejection, and those involving a binary companion. The models must also account for the asymmetry seen in the surrounding PN which implies that the same asymmetry has been acting on the mass loss for 10 000 yr. Binarity can naturally explain the disklike geometry and also the fast wind features (such as the He I λ10830 line and the hole at P.A.∼45 • ). The companion would likely be a very low-mass object which has survived the previous evolution of the system (Mullally et al. 2007). The fact that the asymmetry of the disk is much more pronounced in the recent VLTP event could be a consequence of the smaller mass of the ejecta. It is important to stress that in this scenario the original ejection might have been spherical, but with the asymmetry being enhanced by the influence of the companion. The short timescale for the disk formation is a severe constraint and may imply that the orbital period of the companion is short (i.e. typically a few months). Given their similarities, any solution to the asymmetry of the Sakurai's Object dust envelope will also apply to its twin, V605 Aql (Clayton et al. 2006). In both cases, we seem to have a thick disk of dust preventing the star from being seen directly. In both cases too, some structure in the surrounding PNe are aligned with the axis of the disk.

The small rate of expansion of the disk is a strong argument for a binary interaction. A VLTP happens in 10-20% of post-AGB stars. A companion, originally far from the pri-mary (∼5-10 AU) so to avoid mass transfer and a common envelope phase could be responsible for the outflow shaping. During the initial AGB phase, the spherical wind from the primary star interacts with the companion and is focused toward the equatorial plane. Initially the asymmetry is strong. However, after 10 4 years, the asymmetry slowly disappears as the nebula expands into the ISM. When the VLTP occurs, the resulting mass-loss also interacts with the companion and is once again focused towards the equatorial plane. Given the mass ejected, the companion might also migrate inward and may provide enough angular momentum to stabilise the ejecta in the form of a torus (Nordhaus & Blackman 2006, Peretto et al. 2007, Edgar et al. 2008). Given the disk inclination and high optical depth, the detection of such a companion will be a difficult challenge for the foreseeable future.

  Send offprint requests to: O. Chesneau ⋆ Based on observations made with the Very Large Telescope Interferometer at Paranal Observatory under program 079.D-0415

  Fig.1 shows the Spitzer and MIDI spectra which are characterized by a steeply rising flux toward the long wavelengths. The [OIII] image of the PN is shown in Fig 3. The appearance of the nebula is almost circular, with weak but significant spatial structure.

Fig. 4 .Fig. 3 .

 43 Fig. 4. Flux distribution of the model at 8, 10.5 and 13 µm. A small amount of light emerges at 8 µm while the flux comes from deeper in the disk at 13 µm.

Table 1 .

 1 Observing log

	OB	Time	Base	Projected baseline
				Length	PA
				[metre] [degrees]
	Sak-1 2007-06-29T01 U2 -U3	41.9	14.6
	Sak-2 2007-06-29T02 U2 -U3	45.9	37.1
	Sak-3 2007-06-29T06 U2 -U3	44.4	48.4
	Sak-4 2007-06-30T01 U3 -U4	51.3	101.0
	Sak-5 2007-06-30T06 U3 -U4	54.7	124.3
	Sak-6 2007-06-30T08 U3 -U4	39.2	159.5

Table 2 .

 2 Model parameters.

		Parameters Parameter range
	T eff (K)	12000	-
	Luminosity (L ⊙ )	10000	-
	Distance (kpc)	3.5	-
	Inclination ( • )	75	3
	PA angle ( • )	132	3
	Inner radius (AU)	65	10
	Outer radius (AU)	500	No constraint
	α	2.0	0.1
	β	1.0	0.1
	h 100AU (AU)	47	7
	Dust mass (M ⊙ )	6 × 10 -5	3 × 10 -5

Fig. 1. MIDI spectrum (June 2007; thick crosses) compared with the Spitzer spectra obtained in April 2005 (upper solid curve; Evans et al. 2006) and May 2007 (crosses;

Evans et al. 2009, in preparation)

. The smooth solid line is the flux from the best model assuming a distance of 3.1 kpc.

Available at http://www.strw.leidenuniv.nl/∼nevec/MIDI/index.html


Nicolas Magaud

Formally!

Keywords: projective geometry, spreads, packings, finite models, Coq

We study how to formalize in the Coq proof assistant the smallest projective space PG(3,2). We then describe formally the spreads and packings of PG(3,2), as well as some of their properties. The formalization is rather straightforward, however as the number of objects at stake increases rapidly, we need to exploit some symmetry arguments as well as smart proof techniques to make proof search and verification faster and thus tractable using the Coq proof assistant. This work can be viewed as a first step towards formalizing projective spaces of higher dimension, e.g. PG(4,2), or larger order, e.g. PG(3,3).

Introduction

Projective incidence geometry [START_REF] Coxeter | Projective Geometry[END_REF][START_REF]Handbook of Incidence Geometry[END_REF] is one of the simplest description of geometry, where only points and lines as well as their incidence properties are considered. In addition, in such a setting, we assume that two coplanar lines always meet. There exist some finite and infinite models of projective incidence geometry. Finite projective spaces have been studied extensively from a mathematical point of view (see e.g [START_REF] Hirschfeld | Finite projective spaces of three dimensions[END_REF]). Recently [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF], we started studying small finite projective planes/spaces from a computer science perspective. We formalized usual projective planes such as PG [START_REF] Betten | The packings of pg(3, 3). Designs[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF], PG [START_REF] Betten | The packings of pg(3, 3). Designs[END_REF][START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF] or PG [START_REF] Betten | The packings of pg(3, 3). Designs[END_REF][START_REF]Handbook of Incidence Geometry[END_REF] as well as the smallest projective space PG(3,2) using the Coq proof assistant [START_REF]Coq development team: The Coq Proof Assistant Reference Manual[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development, Coq'Art : The Calculus of Inductive Constructions[END_REF]. We especially focused on proving the synthetic axioms for projective geometry hold in these models. In this paper, we study some of the characteristic subsets of PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF], such as spreads of lines and packings of spreads.

In a three-dimensional setting, the number of points and lines increase rapidly with the order, as shown in Fig. 1. Thus we need to design extremely efficient proof techniques for PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF] if we want our approach to be scalable to projective spaces of higher dimension or larger order. The whole Coq formalization is available online and can be retrieved at : https://github.com/magaud/PG3q. Pointers to specific parts of the development are given throughout the paper.

This paper is organized as follows. In Sect. 2, we show how to formally describe PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF] in Coq using plain inductive types. In Sect. 3, we compute all the spreads and packings of PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF] and prove some of their properties. In Sect. 4, we present some of the proof optimization techniques we set up in order to achieve the proofs. Finally, in Sect. 5, we outline how this work can be extended to projective spaces of higher dimension or higher order. [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Bruck | The construction of translation planes from projective spaces[END_REF] 85 357 5 P G(3, q) (q 2 + 1)(q + 1) (q 2 + q + 1)(q 2 + 1)

q + 1 Fig. 1. Numbers of points, lines and points per line depending on the dimension and the order of projective planes and spaces 2 Inductive specification of PG(3,2) in Coq

Definitions and operations

We choose to use two simple inductive types to represent points and lines of PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF]. Points are represented by an inductive datatype of 15 constructors without arguments. Lines are represented in the same way using 35 constructors.

As there are three points per line, the incidence relation can be represented in a compact way using the match ... with construct of Coq specification language. In order to avoid writing too much code in Coq, we choose to build a generator (a simple C program) which takes as input the number of points, the number of lines as well as the incidence relation as a plain file (pg32.txt 1 ) which contains for each line of the projective space, the list of the points which are incident to it. Given these three elements, the system automatically builds the inductive data-type for points and lines, the incidence relation. It also defines an artificial order on points and lines based on the index of corresponding points and lines, i.e. P0 < P1 < P2 < . . . < P14. The specification generator also builds some auxiliary functions, which will be useful to prove existential statements of the form ∀l1 l2 : Line, exists P : Point, . . .. Using plain inductive data-types may seem naive. An alternative approach to specify points and lines of PG(3,2) could be to use finite types I n of ssreflect and the mathematical components library [START_REF] Gonthier | A small scale reflection extension for the coq system[END_REF]14]. However the main drawback is that ssreflect is designed for formal reasoning rather than computing. Thus checking the incidence between a point and a line is a highly expensive operation, which prevents us from carrying out proofs efficently. Using plain inductive types is much more efficient both to check incidence properties and to perform case analysis. The only drawback is that inductive data-types and functions are huge to write, but this is not that important as we manage to generate these specifications automatically. Overall, our choice is to use the main features of ssreflect, especially the small-scale reflection pattern, but with our own datatypes.

Inductive Point := | P0 | P1 | P2 | P3 | P4 | P5 | P6 | P7 | P8 | P9 | P10 | P11 | P12 | P13 | P14 . Inductive Line := | L0 | L1 | L2 | L3 | L4 | L5 | L6 | L7 | L8 | L9 | L10 | L11 | L12 | L13 | L14 | L15 | L16 | L17 | L18 | L19 | L20 | L21 | L22 | L23 | L24 | L25 | L26 | L27 | L28 | L29 | L30 | L31 | L32 | L33 | L34 .

Proofs

Once the projective space PG(3,2) is described, we check whether all the axioms for projective space geometry hold for this model. This requires proving all axioms of the module defined in https://github.com/magaud/PG3q/ blob/master/generic/pg3x_spec.v and presented in Figure 2. This is pretty straightforward and we try and make it as generic and efficient as possible so that it can be reused for other models of projective space such as PG(3,3).

3 Spreads and Packings of PG(3,2)

Definitions

A spread of PG(3,q) is a set of q 2 + 1 lines which are pairwise disjoint and thus partition the set of points. In PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF], it corresponds to some sets of 5 lines. A packing of PG(3,q) is a set of q 2 + q + 1 spreads which are pairwise disjoint and thus partition the set of lines. In PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF], it corresponds to some sets of 7 spreads. As recalled in [START_REF] Betten | The packings of pg(3, 3). Designs[END_REF][START_REF] Cole | Kirkman parades[END_REF][START_REF] Jeurissen | Special sets of lines in PG(3, 2)[END_REF], it is well known that there is only one spread (up to isomorphism) in PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF] and two packings (up to isomorphism).

Generating all Spreads and Packings of PG(3,2)

Using our external program, we automatically generate all sets of lines of PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF] which are disjoint and cover all the points. As lines contains exactly 3 points, they need to be sets of exactly 5 lines so that all the points of PG(3,2) are accounted for. We obtain 56 distinct spreads (modulo permutations of the order of the lines involved). We also generate all sets of spreads which are disjoint and cover all the lines. As before, these sets of spreads must have 7 elements, as the number of spreads multiplied by the number of lines in each spread equals the number of lines (35) of PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF]. As expected, see Theorem 17.5.6 in [START_REF] Hirschfeld | Finite projective spaces of three dimensions[END_REF], we find 240 packings, upto isomorphism. Spreads and packings are grouped in lists. The list of spreads contain 56 spreads, each of them being a list of 5 lines. The list of packings contain 240 packings, each of them being a list of 7 spreads.

Properties

In Coq, we easily check that the computed spreads and packings verify the properties of spreads and packings.

Spreads can be specified using the following definitions is partition and is spread5. The function forall Point is a finite universal quantification, and forall Point (fun t => X t) stands for X P0 && X P1 && X P2 . . . && X P14. Definition is_partition (p q r s t: list Point) :bool := (forall_Point (fun x => inb x p || inb x q || inb x r || inb x s || inb x t)) && (forall_Point (fun x => negb (inb x p && inb x q && inb x r && inb x s && inb x t))).

Definition is_spread5 (l1 l2 l3 l4 l5:Line) : bool := disj_5l l1 l2 l3 l4 l5 && is_partition (all_points_of_line l1) (all_points_of_line l2) (all_points_of_line l3) (all_points_of_line l4) (all_points_of_line l5).

Once these definitions are set, we can prove that the spreads of PG(3,2) are exactly the ones automatically generated by our external program.

Lemma is_spread_descr : forall l1 l2 l3 l4 l5, (is_spread5 l1 l2 l3 l4 l5) <-> In [l1;l2;l3;l4;l5] spreads.

In addition, we can prove that all 56 spreads of PG(3,2) are isomorphic. It can be expressed by stating that there exists a collineation, i.e. an automorphism of PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF] which respects incidence, between any two spreads of PG [START_REF] Braun | Formalizing Some "Small" Finite Models of Projective Geometry in Coq[END_REF][START_REF] Betten | The packings of pg(3, 3). Designs[END_REF].

Lemma all_isomorphic_lemma : forall t1 t2 : list Line, In t1 spreads -> In t2 spreads -> are_isomorphic t1 t2.

To prove this statement, we show it is equivalent to simply proving that there exists a collineation (we actually build it) from the n-th element of the list to the (n + 1 mod 56)-th element of the list2 .

It is more challenging to check that there are (up to isomorphism) only two packings.

Proof Engineering Techniques

Using bool instead of Prop

As we work with finite types, equality and the other relations that we use are decidable. We can directly implement such relations as operations producing elements of the boolean datatype bool. This is more convenient than defining them as operations producing elements of type Prop together with a decidability property: ∀ x y, {x = y} + {¬x = y}. This practical approach is inspired by the ssreflect [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF] and the mathematical components [14] libraries.

In this setting, logical reasoning (eliminating conjunctions or disjunctions) is a bit more technical. However this makes most proofs much easier to complete by simply computing a boolean value and checking that it is equal to true.

Without Loss of Generality

Most proofs are highly branching. For instance, performing case analysis on all three lines to prove the lemma a3 3 leads to 353 = 42875 cases. In order to make the proof more tractable, we use a tactic named wlog 3 , which implements the without loss of generality principle, as it is described in [START_REF] Harrison | Without loss of generality[END_REF].

This allows to reduce the number of cases to solve explicitly. To use it, we build a virtual order on the points and lines, simply mapping point Pi (resp. line Li) to the value i of its index and extends our statement of the form ∀l1, l2 : Line, . . . to ∀l1, l2 : Line, l1 < l2 → . . . . Surprisingly, using the without loss of generality tactic forces us to generalize our statement for Pasch's axiom to accommodate all cases, depending on the order in which we consider points A, B, C, and D, as shown in Fig. 3.

The usual conclusion of Pasch's axiom (exists I:Point, incid lp I lAB && incid lp I lCD) -> exists J:Point, incid lp J lAC && incid lp J lBD.

is transformed into a conjunction of two existential properties The tactic wlog was also extremely useful when dealing with spreads and trying to determine inside Coq which sets of lines are actual spreads.

Producing Witnesses for Existential Proofs

In the specification generator, we use a form of skolemisation to write functions which compute the existential variable from the other arguments. For instance, to achieve the proof of lemma a3 3, we automatically build a Coq function f a3 3 which, given three lines l 1 , l 2 and l 3 computes a line l 4 as well as its three intersection points to lines l 1 , l 2 and l 3 .

f_a3_3

: Line -> Line -> Line -> Line * (Point * Point * Point)

Optimizing proofs

We design some optimization techniques for generating and checking proof terms. We focus on the current goal, applying some sort of locality principle which means we try to prove a (sub-)goal the very first time we face it. This means sequences of tactics such as intros a; case a; intros H; try (exact (degen_bool )_ H). solve_goal. must be replaced by more efficient sequences like intros a; case a; intros H; solve [(exact (degen_bool )_ H |solve_goal].

In this simplified example, we try to apply the tactic (exact (degen_bool )_ H) for a subgoal and then we switch to the next subgoal. Eventually we solve the remaining subgoals using the solve_goal tactic. The idea here is to solve the goal the first time we encounter it. It is achieved by having several possibilities of tactic applications to solve the goal (this corresponds to the solve [t1|t2|t3] syntax. The order of the tactics t1, t2 and t3 can be highly significant as well: we should always call the tactic which is the most successful one on such subgoals first.

As we face a huge number of cases, we need to design extremely efficient prototype tactics on some specific subgoals and apply them automatically to all the subgoals at stake. Fine tuning the tactics rapidly is the key to making the proofs faster to complete.

Finally, Coq provides some sort of task parallelism in the form of the par tactical. It was very useful to deal with all the sub-goals of a proof, once we figure out how to prove the first one. The generic tactic proving the first goal, say mytactic can be easily applied to all sub-goals in parallel (in some cases, we have 35x35=1225 or more goals to deal with) by simply writing par: mytactic.

Conclusion

In this work, we manage to formalize in Coq the concepts of spreads and packings. In the context of PG(3,2), we build automatically all the spreads and packings. We can easily verify that these generated sets of lines (resp. spreads) are actual spreads (resp. packings). However it remains challenging to verify that they are the only ones. For spreads of PG(3,2), we face a regression issue with Coq4 which prevents our proof from being accepted at the Qed step in the current version of Coq.

During this study, we faced case analysis with a huge number of cases as well as debugging proof script with thousands of sub-goals. We propose some proof engineering techniques to make Coq process the files more easily, e.g . by directly providing witnesses for example or by pruning the proof tree by using a without loss of generality principle.

So far, we only address properties and transformations which remain in the same (projective) space. We are currently working on generating specifications of projective spaces automatically in order to easily have a formal description of two different projective spaces and thus to be able to formally describe constructions as the Bruck-Bose construction which allows to build translation planes from projective planes [START_REF] Bruck | The construction of translation planes from projective spaces[END_REF].

  Definition incid_lp (p:Point) (l:Line) : bool := match l with | L0 => match p with P0 | P1 | P2 => true | _ => false end | L1 => match p with P0 | P3 | P4 => true | _ => false end | L2 => match p with P0 | P5 | P6 => true | _ => false end | L3 => match p with P0 | P7 | P8 => true | _ => false end | L4 => match p with P0 | P10 | P9 => true | _ => false end | [...] end.

1

  https://github.com/magaud/PG3q/blob/master/pg32/pg32.txt Parameter Point, Line : Type. Parameter eqP : Point -> Point -> bool. Parameter eqL : Line -> Line -> bool. Parameter incid_lp : Point -> Line -> bool. Definition Intersect_In (l1 l2 :Line) (P:Point) := incid_lp P l1 && incid_lp P l2. Definition dist_3p (A B C :Point) : bool := (negb (eqP A B)) && (negb (eqP A C)) && (negb (eqP B C)). Definition dist_4p (A B C D:Point) : bool := (negb (eqP A B)) && (negb (eqP A C)) && (negb (eqP A D)) && (negb (eqP B C)) && (negb (eqP B D)) && (negb (eqP C D)). Definition dist_3l (A B C :Line) : bool := (negb (eqL A B)) && (negb (eqL A C)) && (negb (eqL B C)). Axiom a1_exists : forall A B : Point, {l : Line| incid_lp A l && incid_lp B l}. Axiom uniqueness : forall (A B :Point)(l1 l2:Line), incid_lp A l1 -> incid_lp B l1 -> incid_lp A l2 -> incid_lp B l2 -> A = B l1 = l2. Axiom a3_1 : forall l:Line, {A:Point & {B:Point & {C:Point | (dist_3p A B C) && (incid_lp A l && incid_lp B l && incid_lp C l)}}}. Axiom a2 : forall A B C D:Point, forall lAB lCD lAC lBD :Line, dist_4p A B C D -> incid_lp A lAB && incid_lp B lAB -> incid_lp C lCD && incid_lp D lCD -> incid_lp A lAC && incid_lp C lAC -> incid_lp B lBD && incid_lp D lBD -> (exists I:Point, incid_lp I lAB && incid_lp I lCD) -> exists J:Point, incid_lp J lAC && incid_lp J lBD. Axiom a3_2 : exists l1:Line, exists l2:Line, forall p:Point, ~(incid_lp p l1 && incid_lp p l2). Axiom a3_3 : forall l1 l2 l3:Line, dist_3l l1 l2 l3 -> exists l4 :Line, exists J1:Point, exists J2:Point, exists J3:Point, Intersect_In l1 l4 J1 && Intersect_In l2 l4 J2 && Intersect_In l3 l4 J3.

Fig. 2 .

 2 Fig. 2. Projective spaces of dimension 3: definitions and properties (pg3x spec.v)

  Definition S0 := [ L0; L19; L24; L28; L33 ]. Definition S1 := [ L0; L19; L26; L29; L32 ]. [...] Definition spreads := [ S0 ; S1 ; S2 ; ... ; S54; S55 ].

Fig. 3 .

 3 Fig. 3. An illustration of the new form of Pasch's axiom used to deal with symmetries

https://github.com/magaud/PG3q/blob/master/pg32/pg32\_spreads_ collineations.v

https://github.com/magaud/PG3q/blob/master/generic/wlog.v

https://github.com/coq/coq/issues/13834


Pierre Fraigniaud
email: pierre@lri.fr

David Ilcinkas
email: ilcinkas@lri.fr

Andrzej Pelc
email: pelc@uqo.ca

Oracle Size: a New Measure of Difficulty for Communication Tasks

Keywords: C.2.1 [Computer-Communication Networks]: Network Architecture and Design-Network communications; G.2.2 [Discrete Mathematics]: Graph Theory-Network problems Algorithms, Theory Broadcast, Wakeup, Oracle

We study the problem of the amount of knowledge about a communication network that must be given to its nodes in order to efficiently disseminate information. While previous results about communication in networks used particular partial information available to nodes, such as the knowledge of the neighborhood or the knowledge of the network topology within some radius, our approach is quantitative: we investigate the minimum total number of bits of information (minimum oracle size) that has to be available to nodes in order to perform efficient communication.

It turns out that the minimum oracle size for which a distributed task can be accomplished efficiently, can serve as a measure of the difficulty of this task. We use this measure to make a quantitative distinction between the difficulty of two apparently similar fundamental communication primitives: the broadcast and the wakeup. In both of them a distinguished node, called the source, has a message, which has to be transmitted to all other nodes of the network. In the wakeup, only nodes that already got the source message (i.e., are awake) can send messages to their neighbors, thus waking them up. In the broadcast, all nodes can send control messages even before getting the source message, thus potentially facilitating its future dissemination. In both cases we are interested in accomplishing the communication task with optimal message complexity, i.e., using a number of messages linear in the number of nodes.

We show that the minimum oracle size permitting the

INTRODUCTION 1.1 Background and related work

For many network problems (such as leader election, constructing a minimum spanning tree, exploration, wakeup, broadcast, etc.), the quality of the algorithmic solutions often depends on the amount of knowledge given to nodes of the network. For example, if every node knows the topology of the network within radius ρ of it, it is shown in [START_REF] Awerbuch | A trade-off between information and communication in broadcast protocols[END_REF] that Θ(min{m, n 1+Θ(1)/ρ }) is the minimum number of messages of bounded length permitting the wakeup of a network with n nodes and m edges. (In [START_REF] Awerbuch | A trade-off between information and communication in broadcast protocols[END_REF] the authors talk about the broadcast but their model does not permit transmissions before receiving the source message, hence it is called wakeup in our terminology). Broadcasting time in radio networks is another subject where information available to nodes significantly influences efficiency. In [START_REF] Gasieniec | Faster communication in known topology radio networks[END_REF] it is shown that if nodes have complete knowledge of the network then deterministic broadcast can be done in time O(D + log 3 n), for n-node radio networks with diameter D. (This result has been recently improved to O(D + log 2 n) in [START_REF] Kowalski | Optimal deterministic broadcasting in known topology radio networks[END_REF]). On the other hand, in [START_REF] Clementi | Selective families, superimposed codes, and broadcasting on unknown radio networks[END_REF] a lower bound of Ω(n log D) is proved on deterministic broadcast time in radio networks in which nodes know only their own identity. (An almost matching upper bound of O(n log 2 D) is proved in [START_REF] Czumaj | Broadcasting algorithms in radio networks with unknown topology[END_REF]). Another problem, in which partial information about the network significantly influences the efficiency of solutions, is network exploration by a mobile agent. For instance, it is proved in [START_REF] Bender | The power of a pebble: Exploring and mapping directed graphs[END_REF] that, if an upper bound n on the number n of nodes of an anonymous digraph is known, then a mobile agent can explore this digraph in time polynomial in n, using one pebble, while without this knowledge, Θ(log log n) pebbles are necessary and sufficient. On the other hand, in [START_REF] Dessmark | Optimal graph exploration without good maps[END_REF] the authors investigate the exploration of various types of graphs when the exploring agent is provided with an unlabeled map of the graph, and show how the cost of exploration changes when no map is available.

In fact, the impact of knowledge concerning the environment is significant in many areas of distributed computing, as witnessed by [START_REF] Fich | Hundreds of impossibility results for distributed computing[END_REF][START_REF] Lynch | A hundred impossibility proofs for distributed computing[END_REF] where hundreds of impossibility results and lower bounds for distributed computing are surveyed, many of them depending on whether or not the nodes are provided with partial knowledge of the topology of the network. Finally, notice that the amount of knowledge has also a strong impact on computing in anonymous networks (cf., e.g., [START_REF] Kameda | Computing on anonymous networks: Part I -characterizing the solvable cases[END_REF], where the impact of knowing the total number of nodes is studied in depth).

The oracle

A network is modeled as an undirected connected graph whose nodes have distinct labels, and ports at any node v of degree deg(v) are labeled 0,1,...,deg(v) -1. One distinguished node of the network is called the source. A priori, every node has only information concerning itself: it knows its own label (if any), and it knows whether it is the source or not. All additional knowledge available to the nodes of the network (in particular knowledge concerning the rest of the network), is modeled by an oracle. An oracle is a function O whose arguments are networks, and the value O(G), for a network G = (V, E), is in turn a function f : V → {0, 1} * assigning a binary string to every node v of the network. Intuitively, the oracle looks at the entire labeled network and assigns to every node some information, coded as a string of bits. The size of the oracle on a given network G is the sum of the lengths of all the strings it assigns to nodes. Hence this size is a measure of the amount of information about the network, available to its nodes.

Solving a network problem P using oracle O consists in designing an algorithm that is unaware of the network G at hand but solves the problem P for it, as long as every node v of the network G is provided with the string of bits f (v), where f = O(G). Typical distributed network problems that may be solved using an oracle are various communication tasks, such as broadcast, wakeup or gossip (information exchange among nodes), as well as, e.g., the construction of a BFS tree or a minimum spanning tree. The formulation of the problem P may include a demand on the efficiency of the solution, thus we may be interested in communicating within a prescribed time, or constructing a minimum spanning tree using at most a prescribed number of messages. Given the problem P, we ask what is the minimum size of an oracle for solving it. This minimum oracle size can be considered as a measure of the difficulty of the problem P. The novelty and significance of the use of an oracle to model knowledge about the network is that it enables asking quantitative questions about the required knowledge, regardless of what kind of knowledge is supplied. This should be contrasted with the traditional approach that assumes availability of particular items of information, such as the neighborhood of a node.

It turns out that the minimum oracle size, for which a distributed task can be accomplished efficiently, can be used to make a quantitative distinction between the difficulty of apparently similar problems. We show this for two fundamental communication primitives performing information dissemination: the broadcast and the wakeup from a single source. In both of them a distinguished node, called the source, has a message which has to be transmitted to all other nodes of the network. Nodes send messages along edges of the network. In the wakeup, only nodes that already got the source message (i.e., are awake) can send messages to their neighbors, thus waking them up. In the broadcast, all nodes can send control messages even before getting the source message, thus potentially facilitating its future dissemination. In both cases we are interested in accomplishing the communication task with optimal message complexity, i.e., using a number of messages linear in the number of nodes. We ask what is the minimum size of an oracle permitting to do that.

An approach similar to ours has been developed in the context of informative labelings. Informative labeling schemes are ways to label the nodes of a network with short labels in such a way that queries such as inter-node distance [START_REF] Gavoille | Distance labeling in graphs[END_REF], ancestor [START_REF] Abiteboul | Compact labeling schemes for ancestor queries[END_REF], connectivity [START_REF] Katz | Labeling schemes for flow and connectivity[END_REF], etc., can be answered based solely on the labels of the nodes involved in the query. The main objective in this context is to design schemes using short labels, and guaranteeing that queries can be rapidly answered. The oracle terminology is sometimes also used in the context of informative labeling (e.g., when the query can be answered in constant time [START_REF] Thorup | Approximate distance oracles[END_REF]). Conversely, the informative labeling terminology is sometimes also used for problems involving global properties [START_REF] Korman | Proof labeling schemes[END_REF].

Our point of view is to use the informative labeling terminology in the context of distributed data-structures enabling quick answers to queries, and to use the oracle terminology in the context of distributed computing when nodes have to collaborate to achieve complex tasks (e.g., broadcasting, coloring, wake-up, leader election, etc.). One reason motivating this view is, for instance, that giving the knowledge of the network size n to the nodes can hardly be seen as labeling every node by n. Also, the notion of oracle easily extends to the case when the information is not given a priori, but on line, during the execution of the protocol.

Our results

We show that the minimum oracle size permitting the wakeup with a linear number of messages in a network with at most n nodes, is Θ(n log n), while the broadcast with a linear number of messages can be achieved with an oracle of size O(n). We also show that the latter oracle size is almost optimal: no oracle of size o(n) can permit to broadcast with a linear number of messages. Thus an efficient wakeup requires strictly more information about the network than an efficient broadcast.

Our upper bounds are constructive: we show specific oracles of appropriate size and design wakeup and broadcast algorithms using them and accomplishing information dissemination with a linear number of messages. Apart from their tightness, our results have the following additional strength. Both upper bounds hold even for totally asynchronous communication, for anonymous nodes (no distinct labels), and using only bounded-size messages. On the other hand, both lower bounds hold even for synchronous communication, for labels of nodes 1,...,n, and for arbitrarily long messages.

We consider wakeup from a single source, where only one node, the source, is awake in the beginning. We choose this communication primitive due to its similarity with broadcasting, since we want to compare the amount of information needed to efficiently accomplish similar tasks. However, both the upper and the lower bound on oracle size for wakeup still hold for a more traditional formulation of the wakeup problem, where the adversary wakes up an arbitrary subset of nodes which in turn have to wake up all other nodes.

Terminology and preliminaries

We now describe broadcast algorithms using oracles, in a more detailed manner. Wakeup algorithms will be a particular type of broadcast algorithms, subject to an additional constraint. Consider a network, i.e., a connected graph G = (V, E) with a distinguished source s. Every node v of degree deg(v) has a distinct label id(v), and ports at v are labeled 0, 1, ..., deg(v)-1. The port at node v, corresponding to edge e, is denoted by port v (e). Every node v has also a bit s(v) called the status bit, which is set to 1 if the node v is the source, and to 0 otherwise. Fix an oracle O and let f = O(G) be a function f : V → {0, 1} * , assigning binary strings to nodes of G. A broadcast algorithm A using oracle O is a function A : {0, 1} * × {0, 1} × IN × IN → Σ, where IN denotes the set of non-negative integers and Σ denotes the set of broadcast schemes (to be defined below). For a given node v, algorithm A takes the quadruple (f (v), s(v), id(v), deg(v)) and returns a broadcast scheme Sv = A(f (v), s(v), id(v), deg(v)) for the node v. It remains to define what such a scheme is. Intuitively, this is a prescription whether and on which ports the node should send messages, and what messages, given a particular history of communication to date. Such a history (at node v) is a sequence H = (f (v), s(v), id(v), deg(v), (m1, p1), (m2, p2), . . . , (m k , p k )), where the prefix (f (v), s(v), id(v), deg(v)) is the knowledge of the node before the broadcast starts, and (m1, m2, . . . , m k ) are messages already received by v, where mi came to node v on port pi. Intuitively, the history describes the total knowledge of the node at a given point of the broadcast process. Given a history H at node v, a broadcast scheme Sv returns a set of couples {(m 1 , p 1 ), . . . (m r , p r )}, where 0 ≤ p i < deg(v). This means that v should send message m i on port p i , for i ≤ r. At each point of the scheme execution some nodes are informed. Intuitively, these are nodes that already got the source message. In the beginning only the source is informed. A node becomes informed after receiving a message from an informed node (indeed, the source message can be appended to any such message). Broadcast is completed when all nodes of the network are informed. Wakeup algorithms using oracles produce wakeup schemes in a similar manner as above: a wakeup scheme for v is a broadcast scheme that does not send any messages (returns the empty set) on all histories with no messages, unless v is the source. Intuitively, nodes other than the source can spontaneously transmit in the broadcast but they cannot in the wakeup. The message complexity of a broadcast or a wakeup scheme is the total number of messages that it produces.

ORACLE SIZE FOR THE WAKEUP

In this section we show that the minimum oracle size permitting the wakeup with a linear number of messages is Θ(n log n). Establishing the upper bound is easy. Fix a network G, and let T be any spanning tree of G. The value f of oracle O on the network G is defined as follows. For any node v, f (v) is a binary string coding those port numbers at v that lead to its neighbors in T . Since port numbers are integers smaller than n, there exists such a string of length at most n(v) log n + O(log log n), where n(v) is the number of neighbors of v in T . (One way of constructing such an encoding string is this. Concatenate all binary representations of the n(v) port numbers that lead to the neighbors of v in T , using exactly log n bits for each of them. Let the obtained sequence α have length x = n(v) log n . Construct another binary sequence β as follows. Let b1 . . . br be the binary representation of log n . Let β = b1b1b2b2 . . . brbr10. Finally, concatenate α to β. The obtained sequence has length x + O(log log n), and the original representations of the n(v) port numbers are easy to obtain from it.) Hence the size of the oracle is n log n+o(n log n). Given this oracle, the wakeup scheme at v tells the node to send messages on all ports coded by f (v). This scheme uses exactly 2(n -1) messages. Thus we have:

Theorem 1.
There exists an oracle of size O(n log n) permitting the wakeup with a linear number of messages of networks with at most n nodes.

The main result of this section establishes a matching lower bound on oracle size for this task.

Theorem 2. The minimum oracle size permitting the wakeup with a linear number of messages of networks with at most n nodes must have size Ω(n log n).

To prove this theorem, we use an auxiliary problem, called edge discovery, defined as follows. We denote by K * n the nnode complete graph Kn whose vertices are labeled from 1 to n, and the port number at node i of the edge leading to node j is labeled (i-j) mod (n -1). The instances of the problem edge discovery are triples (n, X, Y ) where n is a positive integer, and X and Y are two disjoint subsets of edges of K * n . In fact, the edges in X are given distinct labels between 1 and |X|. So formally, X = {(e1, 1), . . . , (e |X| , |X| )}, where i is the label of ei. The problem consists in designing a communication scheme that, given n, |X|, and Y , eventually discovers X. Whenever an edge e is traversed by a message of the communication scheme, the following information is obtained: if (e, ) ∈ X then (e, ) is revealed; otherwise it is revealed that (e, ) ∈ X for any label .

We prove the following lemma that will be used later as a key tool for proving our lower bounds. In the absence of any information about the instances, this lemma could be proved using techniques similar to those in, e.g., [START_REF] Korach | The Optimality of Distributive Constructions of Minimum Weight and Degree Restricted Spanning Trees in a Complete Network of Processors[END_REF] and [START_REF] Korach | Optimal Lower Bounds for Some Distributed Algorithms for a Complete Network of Processors[END_REF]. However, the presence of an oracle changes the setting radically.

Lemma 1. Let I be a subset of instances of edge discovery, all yielding the same input for the problem (i.e., these instances differ only in the sets X, and all these sets X have the same size). The worst-case message complexity of edge discovery restricted to I is at least log |I| |X|! .

Proof. For any given instance (n, X, Y ) of edge discovery, the edges in X are called special. Let us consider any communication scheme S solving edge discovery for all instances in I. Messages traverse edges during the execution of S. At the beginning of the execution of the scheme, all instances in I are called active. When an edge is traversed, the scheme learns whether this edge is special or not. This knowledge enables to discard instances from the set of active instances. For example, if the traversed edge e is not special, then all currently active instances in which e is special can be discarded. Conversely, if the traversed edge e is special, then all currently active instances in which e is not special can be discarded.

We describe an adversary that aims at slowing down the discovery of the special edges by S. We consider the synchronous execution of S. A set J ⊆ I of active instances, after t messages have been sent by S and r special edges have been discovered by S, for some t ≥ 0 and r ≥ 0, is said to be uniform if (1) the t first messages are sent by S through the same edges in all instances in J, and (2) the set of revealed couples (e, ), for special edges e, is the same in all instances of J. If J is uniform, then the scheme S will proceed identically at the next step of its execution in all instances of J. That is, a message is sent through edge e and this edge is the same for all instances in J. The adversary considers uniform sets of active instances, and proceeds as follows. Let J special (resp., J regular ) be the set of instances in a uniform set J, for which e is special (resp., not special). If |J special | ≥ |J regular | then the adversary decides that e is special, else it decides that e is not special. Note that |J special | ≥ 1 2 |J| in the former case, and |J regular | ≥ 1 2 |J| in the latter case. In case e is set to be special by the adversary, the label (e) remains to be set. The adversary proceeds as follows. Since r special edges have been already discovered, the label of e can take |X|r values. The adversary chooses the label l0 such that the set J (l 0 ) special of active instances in J special for which (e) = l0, has the largest size. Note that then |J

(l 0 ) special | ≥ |J | 2(|X|-r)
. We say that J regular is the regular subset of J, and J (l 0 ) special is the special subset of J. By construction, J regular , as well as all J (l) special for 1 ≤ l ≤ |X|, are uniform. Hence, we can define recursively the following sequence of sets: I0,0 = I and Proof of Theorem 2. We first prove that, for any α < 1/2, there exists > 0 such that, for any integer n greater than some constant, there exists a (2n)-node graph for which no algorithm can perform wakeup with less than (2n) log(2n) messages, if the oracle size is not more than α (2n) log(2n). Fix a positive integer n. Recall that K * n is the n-node complete graph with the following labeling. The nodes of K * n are labeled from 1 to n. The port numbers of the edges are fixed as follows: for any 1 ≤ i, j ≤ n, the port number at i of the edge {i, j} is (ij) mod (n -1).

¡ ¡ ¢ ¡ ¡ £ It+1,r = the regular subset of It,
For any n-tuple S = (e1, e2, . . . , en) of distinct edges in K * n , let Gn,S be the graph defined from K * n as follows. For any 1 ≤ i ≤ n, a node wi labeled n + i is inserted in the middle of the edge ei = {ui, vi}. The port number at ui (resp. at vi), of the edge {ui, wi} (resp. {vi, wi}), is the same as the port number at ui (resp. at vi), of the former edge {ui, vi}. Assume, without loss of generality, that the label of ui is smaller than the label of vi. Then the port number at wi of the edge {ui, wi}, (resp. {vi, wi}), is 0 (resp. 1). Other port numbers remain unchanged. Let node with label 1 be the source.

Intuitively, an oracle has to give a lot of information to help a wakeup algorithm to find the n subdivided edges with only O(n) messages. This is mainly due to the fact that there exists a lot of different graphs Gn,S. The graphs Gn,S are indeed distinct for different sets S. There are

P = n! ¤ ( n 2 )
n ¥ such (labeled) graphs, as there are ¤ n 2 ¥ edges in K * n . Let us compute a lower bound on P . First note that, for any a, b such that 1 ≤ b ≤ a, we have

¦ a b § ≥ ¨a b © b . (1)
This implies

¦ ¤ n 2 ¥ n § ≥ ¦ ¤ n 2 ¥ n § n . Moreover, we have ¤ n 2 ¥ = n(n+1) 2 ≥ n 2 /2. Hence P ≥ n! ¨n 2 © n . (2)
Consider an arbitrary wakeup algorithm using an oracle O. Assume that O has size at most q = α(2n) log(2n) on all graphs of size 2n, for some α < 1/2. We will prove that there are many graphs Gn,S for which the oracle has the same output.

Let us first compute how many different functions f an oracle O of size at most q can output for (2n)-node graphs. Let v1, . . . , v2n be the list of nodes of such a graph, in increasing order of their identifiers. Consider a function f = O(G). For any 1 ≤ i ≤ 2n, f (vi) is the (possibly empty) string given by the oracle to the node vi in the graph G. Let s be the concatenation of the strings f (vi) in increasing order of i. Let q be the size of s. By definition of q, we have q ≤ q. There are 2 q possible different strings s for a given q . Moreover, using standard combinatorial arguments, one can show that there are ¤ q +2n-1 2n-1 ¥ different ways to partition the q bits of the string s into 2n (possibly empty) substrings f (vi). To summarize, an oracle of size q can output 2 q ¤ q +2n-1 2n-1 ¥ different functions for (2n)-node graphs. Since q can be chosen between 0 and q, the oracle has exactly

Q = q q =0 ¦ 2 q ¦ q + 2n -1 2n -1 § § possible different outputs. Let us compute an upper bound on Q. Since 2 q ¤ q +2n-1 2n-1 ¥
is increasing as a function of q , it follows that Q is at most (q + 1) ¨2q ¤ q+2n-1

2n-1 ¥ © . Note that ¤ q+2n-1 2n-1 ¥ ≤ ¤ q+2n 2n ¥ because q ≥ 0. Thus we have Q ≤ (q + 1) ¦ 2 q ¦ q + 2n 2n § § (3)
Recall that q = α(2n) log(2n). Thus we have ¤ q+2n

2n ¥ = ¤ 2n(1+α log(2n)) 2n ¥ . In view of Lemma 1.6 of [18] stating that ¦ a b § ≤ ¨ae b © b (4)
for 0 < b ≤ a, we get

¦ 2n(1 + α log(2n)) 2n § ≤ ¨e ¤ 1 + α log(2n) ¥ © 2n
.

For n large enough, we have

¨e ¤ 1 + α log(2n) ¥ © 2n ≤ ¤ 6α log(2n) ¥ 2n
and thus

Q ≤ ¤ α (2n) log(2n) + 1 ¥ • 2 α (2n) log(2n) • ¤ 6α log(2n) ¥ 2n .
Take β = 1/4 + α/2. We have α < β, and thus for n large enough,

Q ≤ 2 2βn log(n/2) . (5)
The oracle can output at most Q different functions for the P different graphs Gn,S. Therefore, there exists a function f such that the oracle will output f for a set G of at least P/Q different graphs Gn,S. For all these graphs, the wakeup scheme returned by the algorithm is the same.

To any graph Gn,S ∈ G we can associate an instance (n, S, ¡ ) of the edge discovery problem, where the special edges of edge discovery are the subdivided edges of the graph Gn,S, and the label of a special edge is the rank of the subdivided edge in S. Let I be the set of instances of edge discovery obtained from all graphs in G. Clearly, I and G have the same cardinality. Performing wakeup in a graph Gn,S requires that, for any e ∈ S, at least one message be sent to the node hidden in the edge e. Moreover, this node has an identifier that corresponds to the position of e in S. Therefore, performing wakeup in a graph Gn,S requires at least the same number of messages as solving the edge discovery problem on the corresponding instance.

Combining Equations 2 and 5, we get

P/Q ≥ n! 2 (1-2β)n log(n/2) .
Since |I| ≥ P/Q, the application of Lemma 1 gives a worstcase message complexity of at least

log( n! 2 (1-2β)n log(n/2) n! ) = (1 -2β) n log(n/2) (6)
Since α < 1/2, we have β < 1/2 and thus the above message complexity is greater than (2n) log(2n) for n large enough, where is a positive constant not depending on n.

We can now conclude the proof of the theorem. Assume that the theorem does not hold. Then there exists an infinite increasing sequence of integers (ni) i≥1 , an oracle of size less than 1 4 ni log ni for the graphs with at most ni nodes, i ≥ 1, and an algorithm A using this oracle, such that the algorithm performs wakeup with a linear number of messages in any graph. Fix i ≥ 1. Let mi = ni if ni is even and mi = ni -1 otherwise. For graphs of size at most mi, the oracle has size at most 1 4 ni log ni. For i large enough, we have 1 4 ni log ni ≤ 1 3 mi log mi. Applying the previous result with α = 1/3, there exists a positive constant such that A has a worst-case message complexity of at least mi log mi on mi-node graphs, for i large enough. Thus the message complexity of A is not linear. This contradiction concludes the proof of the theorem.

Remark. In the above proof, we obtained a threshold 1/2 for α. Given an arbitrary constant integer c, a threshold c c+1 can be obtained by subdividing cn edges instead of only n edges. Hence, one can show that our upper bound n log n + o(n log n) on oracle size permitting wakeup with a linear number of messages in graphs with at most n nodes, is asymptotically optimal.

ORACLE SIZE FOR THE BROADCAST

In this section we establish almost tight bounds on the minimum oracle size permitting the broadcast with a linear number of messages. In particular, the following upper bound, together with Theorem 2, shows that an efficient wakeup requires strictly more information about the network than an efficient broadcast. Theorem 3. There exists an oracle of size O(n) permitting the broadcast with a linear number of messages in networks with at most n nodes.

Proof. We construct an oracle O and a broadcast algorithm A using it, which returns a broadcast scheme B with linear message complexity. We first describe the oracle O. Let G = (V, E) be any n-node network. Every edge e = {u, v} ∈ E is given the weight w(e) = min{port u (e), port v (e)}.

Let #2(w) be the number of bits for encoding a non-negative integer w using standard binary representation, that is #2(w) = 1 if w ≤ 1, and #2(w) = log w + 1 if w > 1. Call the number #2(w(e)) the contribution of the edge e. Claim 3.1. There exists a spanning tree T0 of G, for which ¢ e∈E(T 0 ) #2(w(e)) ≤ 4n.

We establish the claim by constructing a tree T0 that yields this contribution. The construction is a variant of Kruskal's minimum-weight spanning tree (MST) algorithm (cf. [START_REF] Cormen | Introduction to Algorithms[END_REF]), similar to the one in [START_REF] Cohen | Labeling Schemes for Tree Representation[END_REF]. It maintains a collection of trees. Initially, each node of G forms a tree on its own. The construction merges these trees into larger trees until it remains with a single tree giving the solution T0. More precisely, the construction proceeds in phases. Each phase k ≥ 1 of the construction consists of four steps. At the beginning of the phase, we identify the collection of "small" trees for the phase: T small (k) = {T : |T | < 2 k }, where |T | denotes the size (number of nodes) of a tree T . Second, for each tree T ∈ T small (k), we look at the set S(T ) of edges that connect T to G \ T , and select an edge e(T ) of minimum weight in S(T ). (Note that S(T ) = ∅ since the graph G is connected.) Third, we add these edges to the collection of trees, thus merging the trees into subgraphs. Each subgraph may contain a cycle, thus, finally, for the last of the four steps, in each subgraph we arbitrarily select one of the edges on the cycle and erase it, effectively transforming the subgraph back into a tree. This process is continued until a single tree remains, which is the desired tree T0.

To prove the claim, let us denote the collection of trees at the beginning of the kth phase, k ≥ 1, by

T (k) 1 , . . . , T (k)
q k , where q k is the number of trees maintained in phase k. We have q1 = n, and

|T (1) i | = 1 for any 1 ≤ i ≤ n. Moreover, ¢ q k i=1 |T (k) i | = n for every k ≥ 1. By induction, we easily get that |T (k) i | ≥ 2 k-1 for every k ≥ 1 and 1 ≤ i ≤ q k . Thus q k ≤ n/2 k-1 for every k ≥ 1.
In particular, the number of phases of the construction is at most log n .

Assume that, when considering a small tree T . Hence even if all of these edges are "lighter" than the edges leading outside the tree, the port number used for e(T

(k) i ) is at most |T (k) i | -1, hence w(e(T (k) i )) ≤ |T (k) i | -1. Therefore #2(w(e(T (k) i ))) = 1 if k = 1 #2(w(e(T (k) i ))) ≤ log(|T (k) i | -1) + 1 if k > 1 For T (k) i ∈ T small (k), we have log |T (k) i | < k.
Since outgoing edges are selected only for small trees, we have #2

¨w ¨e ¨T (k) i ≤ k .
Hence the total contribution C k of the edges added to the structure throughout the kth phase satisfies

C k ≤ k |T small (k)| ≤ k q k ≤ k n/2 k-1 .
Therefore, the total contribution ¢ k≥1 C k of all edges of the resulting tree T0 satisfies ¢ k≥1 C k ≤ ¢ k≥1 kn/2 k-1 ≤ 4n. This completes the proof of Claim 3.1.

For every edge e = {u, v} ∈ E(T0), the oracle O assigns the binary representation of w(e) to the extremity x ∈ {u, v} such that w(e) = port x (e), where ties are broken arbitrarily. The same node may receive binary representations of several weights w(e1), . . . , w(et), in which case they can be encoded by one binary string of length 2 ¢ t i=1 #2(w(ei)). In view of Claim 3.1, the size of the oracle is at most 8n.

Based on the strings assigned to the nodes of G by oracle O, Algorithm A constructs the broadcast scheme B defined in Figure 1. We establish the first part of the claim by combining the following properties. Clearly, the source message M as well as the "hello" messages are sent only through the n-1 edges of T0. The message M does not traverse an edge more than once because M is sent by x only through edges of Kx \ Sx, where Sx is the set of edges through which either M has been sent by x before, or M has been received by x. A "hello" message traverses an edge e of T0 in one direction only because only one extremity x of e is given the port number port x (e) by the oracle.

/*
The second part of the claim is established by induction on the distance d of a node from the source, in the tree T0. Let P (d) be the property "all nodes at distance ≤ d from the source in T0 eventually receive the message M ". P (0) clearly holds. Assume P (d) holds for d ≥ 0, and consider a node x at distance d + 1 from the source in T0. Node x is a neighbor in T0 of a node y at distance d from the source in T0. The edge e = {x, y} is eventually discovered by y because, by definition of the oracle O, either y is given port y (e), or x is given port x (e), and, in the latter case, x will eventually send a message "hello" to y, enabling e to be known by y. By the induction hypothesis, y will eventually receive the message M . Therefore the message will eventually be sent through e by y. Therefore P (d + 1) holds too, and hence B achieves broadcast. Theorem 4. Any broadcast algorithm using an oracle of size o(n) in networks with at most n nodes, cannot return a broadcast scheme of linear message complexity.

Proof. The proof uses a similar construction as for proving Theorem 2, but requires novel ideas, since the nodes can now transmit spontaneously. Recall that K * n denotes the n-node complete graph Kn whose vertices are labeled from 1 to n, and the port number at node i of the edge leading to node j is labeled (ij) mod (n -1). For any k and n such that 4k divides n, and for any (n/k)-tuple S = (e1, . . . , e n/k ) of distinct edges of K * n , let us consider the graphs obtained from K * n by replacing edge ei by a clique Hi of size k, for i = 1, . . . , n/k. More precisely, one edge {ai, bi} of the clique Hi replacing ei is removed from Hi, and ai is connected to one extremity of ei in K * n , while bi is connected to the other extremity of ei in K * n . Nodes of Hi are labeled from n + (i -1)k + 1 to n + ik, for i = 1, . . . , n/k. The port number at node n + (i -1)k + a of the edge leading to node n + (i -1)k + b is labeled (ab) mod (k -1). By abuse of notation, the edge {n + (i -1)k + a, n + (i -1)k + b} is called the edge {a, b} of Hi. The set S does not fully specify the graph resulting from the above transformation because edges {ai, bi} are not yet specified. Let

C = ¨(a 1, b1), . . . , (a n/k , b n/k ) © | (ai, bi) ∈ {1, . . . , k} 2 , ai < bi, i = 1, . . . , n/k ¡ .
Any C ∈ C (together with the set S) fully characterizes the graph as follows. For any edge ei in S, i = 1, . . . , n/k, let ei = {ui, vi}, where id(ui) < id(vi). The edge ei of K * n and the edge fi = {ai, bi} of Hi are replaced by the edges {ai, ui} and {bi, vi}. The port number at ui (resp., vi) of the edge {ai, ui} (resp., {bi, vi}) is the same as the port number at ui (resp., vi) of the edge ei. Similarly, the port number at ai (resp., bi) of the edge {ai, ui} (resp., {bi, vi}) is the same as the port number at ai (resp., bi) of the edge fi. The resulting graph is denoted by Gn,S,C . Let the node with label 1 be the source. For any pair of positive integers (n, k) such that 4k divides n, the family of graphs defined as above is denoted by G n,k . In other words, we have

G n,k = {Gn,S,C | S is a (n/k)-tuple of edges of K * n , C ∈ C } .
Note that, by construction, every graph in G n,k has 2n nodes, and in each such graph, all nodes with labels larger than n (i.e., those in the added cliques) have degree k -1.

Claim 3.3. For n and k large enough, such that k ≤ √ log n and 4k divides n, any broadcast algorithm using an oracle of size at most n 2k , for all graphs in G n,k , cannot return a broadcast scheme with message complexity less than n(k -1)/8.

To establish the claim, let us assume, for the purpose of contradiction, that there exists a broadcast algorithm A using an oracle O of size at most n 2k , for all graphs in G n,k , which produces a broadcast scheme of message complexity less than n(k -1)/8. Let σi be the sum of numbers of bits given by the oracle O to the nodes of Hi. Since Σ n/k i=1 σi ≤ n 2k , we get that at least half of the cliques do not receive any bit of information. On the other hand, if

A(¡ , 0, n + (i -1)k + a, k -1)
is not defined for some pair (i, a), where 1 ≤ i ≤ n/k and 1 ≤ a ≤ k, then at least one node of Hi requires some information from the oracle to specify its broadcast scheme, and thus the clique Hi must receive at least one bit of information. Such an index i is called heavy. Let i ∈ {1, . . . , n/k} be a non heavy index (i.e., i is such that A(¡ , 0, n + (i -1)k + a, k -1) is defined for all a = 1, . . . , k), and let us observe the behavior of the communication scheme produced by A in the clique Hi, when the oracle gives no information to the nodes of Hi. If in the synchronous execution of the scheme, all edges of Hi are eventually traversed by at least one message, then i is called internal. Otherwise, i.e., if the communication scheme leaves at least one edge of Hi not traversed by any message in the synchronous execution of the scheme, then i is called external. External indices result from the fact that the scheme exchanges messages but lets always one edge free of message, or result from the fact that the execution of the scheme reaches a point at which the action of a node is not defined (the history of the execution cannot be produced by the broadcast scheme returned by A).

For every internal index i, let us consider the synchronous execution of the scheme, and let fi = {ai, bi} be an edge of Hi that is traversed last. For every external index i, let us again consider the synchronous execution of the scheme, and let fi be any edge of Hi that is not traversed by any message. Finally, for every heavy index i, let fi be any edge of Hi. This setting of the fi's defines one (n/k)-tuple from C, denoted by C * . We will now restrict attention to those graphs in G n,k , for which S takes all possible values of (n/k)-tuples of edges of K * n , but C = C * . Fix S and consider Gn,S,C * . As observed before, at least half of the cliques in Gn,S,C * receive no information from the oracle. Let I be the corresponding set of indices. We have |I| ≥ n/(2k). Indices in I are either internal or external because cliques with heavy indices must receive at least one bit of information from the oracle. Hence I can be decomposed into two sets Iint and Iext that are subsets of internal and external indices, respectively, and such that I = Iint ∪ Iext. For all cliques Hi with i ∈ Iext, the setting of the fi's implies that the broadcast scheme generated by A has the property that, in its synchronous execution, no message goes out of Hi before a message goes into Hi from the rest of the graph. Among all cliques Hi with i ∈ Iint, some may have the property that, in the synchronous execution of the broadcast scheme, a message goes out of Hi before any message goes into Hi from the rest of the graph. Let I + int be the indices from Iint, for which this phenomenon occurs. By the setting of the fi's, for every i ∈ I + int , the message complexity of the broadcast scheme restricted to Hi is at least k(k -1)/2 since fi is one of the edges traversed last. Therefore, since the broadcast scheme generated by A has message complexity less than n(k -1)/8, we get that

|I + int | < n 4k . Thus, |I \ I + int | ≥ n 4k
. This inequality implies that the number of cliques Hi such that, in the synchronous execution of the broadcast scheme, no message goes out of Hi before a message goes into Hi from the rest of the graph, is at least n 4k . In other words, at least n 4k cliques have to be discovered from the outside, and at most 3n 4k can reveal themselves spontaneously to the rest of the graph. Therefore, the broadcast problem in Gn,S,C * is at least as hard as the auxiliary problem edge discovery with instances

where the first inequality follows from Equation 1. On the other hand, let Q be the number of possible functions output by an oracle of size at most q for the graphs of G n,k . By the same calculations as for deriving Equation 3, we get Q ≤ (q + 1)2 q ¦ 2n + q q § . It follows from Equation 4that

¦ 2n + n 2k n 2k § = ¦ n 2k (1 + 4k) n 2k § ≤ ¤ e(1 + 4k) ¥ n 2k ≤ (24k) n 2k
for n and k large enough. Since n 2k + 1 < n k , we get

Q ≤ n k 2 n 2k (24k) n 2k , if q ≤ n 2k .
Therefore, for n and k large enough,

Q ≤ (50k) n 2k . (8)
There exists a set of graphs of size at least P/Q for which the oracle returns the same function. Combining Equations 7 and 8, we conclude that there exists a set of graphs of size at least

|X|!

¨n 5000 k © n 4k

for which the oracle returns the same function. Applying Lemma 1 to this set of graphs, we get that the number of exchanged messages is at least n 4k log( n 5000 k ). For k ≤ √ log n, and for n and k large enough, this number is at least n(k -1)/8, a contradiction with the hypothesis that A produces a broadcast scheme of message complexity less than n(k -1)/8. This completes the proof of Claim 3.3.

To complete the proof of the theorem, let us consider a broadcast algorithm A using an oracle O of size f (n) in networks of at most n nodes, where f (n) is in o(n). . Let n be the largest integer smaller or equal to n and divisible by 4k (n). Note that, since n/k (n) grows to infinity, we have n ≥ n/2, for n large enough. The oracle O has size at most ¢ f (n) in networks with at most n nodes. We have

¢ f (n) = n k(n) ≤ 2n k(n) ≤ n 2 k (n) .
Therefore, O has size at most n 2 k (n) in networks with at most n nodes. By the construction of ¢ f , we get k (n) ≤ √ log n . Hence Claim 3.3 applies, and we conclude that the broadcast scheme returned by A on graphs with at most n nodes has message complexity at least n (k (n)-1)/8, which is not in O(n ). Therefore, any broadcast algorithm A using an oracle O of size f (n) in networks with at most n nodes, where f (n) is in o(n), returns a broadcast scheme that does not have a linear message complexity.

CONCLUSION

We investigated oracles: a new way of modeling knowledge that nodes have about the network. We showed that the minimum oracle size for which a task can be accomplished efficiently, can serve as a measure of difficulty of this task, and can be used to quantitatively differentiate the difficulty of related tasks. In this paper we concentrated on two similar communication tasks, broadcast and wakeup with a linear number of messages, and used oracle size to strictly separate their difficulty. However, we conjecture that oracles can be also used to assess difficulty of a broader range of distributed network problems, not only concerning information dissemination but also, e.g., spanner construction or exploration by mobile entities. Moreover, oracles could be potentially used to establish precise tradeoffs between the amount of knowledge available to nodes of a network and the efficiency (in terms of time or message complexity) of accomplishing a given task.

  kth phase, the edge e(T (k) i ) incident to some node x of T (k) i was selected. The only edges incident to node x excluded from consideration are the at most |T (k) i | -1 edges leading from x to the other nodes in T (k) i

Figure 1 :Claim 3 . 2 .

 132 Figure 1: Broadcast Scheme B Claim 3.2. The scheme B has linear message complexity, and achieves broadcast in G.

n 2 ¥

 2 (n, X, Y ) satisfying |X| = n 4k and |Y | = 3n 4k . For n, |X|, and Y fixed, there are |X|! ¦ ¤ -|Y | |X| § different instances of edge discovery. Hence, for |X| = n 4k and |Y | = 3n 4k , the number of different instances P = |X|! P satisfies

  Let ¢ f be the function defined by ¢ f (n) = max{f (n), n √ log n }. Hence A uses an oracle O of size at most ¢ f (n) in networks of at most n nodes. For any n ≥ 1, let k(n) = n/ ¢ f (n), and let k (n) = k(n)

4

 4

  As a consequence, xt,r ≥ x0,0/(2 t |X|!) for any r ≤ |X|. When the communication scheme S is completed, only one instance remains active, i.e., xt,r ≤ 1. By the previous inequality, our adversarial scenario guarantees that this cannot occur before t messages have been sent, where x0,0 (2 t |X|!) ≤ 1 .

	Since x0,0 = |I|, we conclude that t ≥ log |I| |X|! , which com-pletes the proof of Lemma 1.
	r,
	if the (t + 1)th edge is set as not special;
	It+1,r+1 = the special subset of It,r,
	if the (t + 1)th edge is set as special.
	By construction, depending on which of the cases holds, we
	have |It+1,r| ≥ |It,r|/2 or |It+1,r+1| ≥ |It,r|/(2(|X|-r)). For the above defined adversary, let xt,r denote the number of
	active instances after t messages have been sent in S, and r
	special edges have been discovered. Thus, x0,0 = |I| and xt+1,r ≥ xt,r 2 and xt+1,r+1 ≥ xt,r 2(|X| -r) .

Therefore, by simple induction on r and t, we get

xt,r ≥ x0,0 (|X|r)! 2 t |X|! .

  Broadcast Scheme B executed by node x. M is the source message. */ begin Kx ← list of port numbers given by the oracle O to x; /* Kx = incident edges known by x */ Hx ← Kx; /* Hx = incident edges through which "hello" messages may be sent */ Sx ← ∅; /* Sx = incident edges through which the message M has been transmitted */ repeat if x receives the message M via port p then Kx ← Kx ∪ {p}; Sx ← Sx ∪ {p}; if x receives the message M then send message M on all ports of Kx \ Sx;

	Sx ← Kx;
	Hx ← Hx \ Sx;
	if Hx = ∅ then
	send "hello" messages on all ports of Hx;
	Hx ← ∅;
	if x receives a "hello" message via port p / ∈ Kx then
	Kx ← Kx ∪ {p};
	endrepeat
	end

* Supported by the projects PairAPair of the ACI Masses de Données, and FRAGILE of the ACI Sécurité Informatique. Additional support from the INRIA project "Grand Large". † Supported in part by NSERC discovery grant and by the Research Chair in Distributed Computing of the Université du Québec en Outaouais.


Laurent Sauvage
email: laurent.sauvage@telecom-paristech.fr

Sylvain Guilley

Jean-Luc Danger

Yves Mathieu

Maxime Nassar

Successful Attack on an FPGA-based Automatically Placed and Routed WDDL+ Crypto Processor

Keywords: Side-Channel Analysis (SCA), Differential Power Analysis (DPA), Differential Electro-magnetic Analysis (DEMA), Wave Dynamic Differential Logic (WDDL), Field Programmable Gates Array (FPGA)

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

To defeat Side-Channel Analysis (SCAs), many solutions have been proposed since the first attack published 10 years ago [START_REF] Kocher | Differential Power Analysis[END_REF].

The Dual-rail with Precharge Logic (DPL) is a countermeasures family which try to make the power consumption independent of the manipulated data. In this family, we find the Wave Dynamic Differential Logic (WDDL) coined by Kris Tiri [START_REF] Tiri | A Logic Level Design Methodology for a Secure DPA Resistant ASIC or FPGA Implementation[END_REF]. The major advantage of this latter is the use of a standard cell flow, which facilitates the synthesis process. Moreover this enables implementation on Components Off The Shelf (COTS) such as FPGAs. Although WDDL presents a flaw [START_REF] Suzuki | Security Evaluation of DPA Countermeasures Using Dual-Rail Pre-charge Logic Style[END_REF] like the "early evaluation" bias, by now nobody exploits it to lead a complete successful attack. Whereas, Sylvain Guilley and al. stepped into the breach in [START_REF] Guilley | Evaluation of Power-Constant Dual-Rail Logic as a Protection of Cryptographic Applications in FPGAs[END_REF]: with the seminal Differential Power Analysis (DPA), they break one SBox of a FPGA-based WDDL+ DES module embedded on a "Parallax Stratix 672 Smart-Pack Board". This disproves statement that DPA on commercial FPGA development board is difficult [START_REF] Sun | Experiments in attacking FPGA-based embedded systems using differential power analysis[END_REF].

In this paper, we are going one step further by announcing the first successful attack on a FPGA-based WDDL+ DES crypto co-processor. This attack is fully non invasive: no board modifications are required as it is performed with the Differential Electro-Magnetic Analysis (DEMA). Farfield DEMA attacks have already been reported in [START_REF] Mulder | Electromagnetic Analysis Attack on an FPGA Implementation of an Elliptic Curve Cryptosystem[END_REF][START_REF] Li | A security evaluation methodology for smart cards against electromagnetic analysis[END_REF]. The strength of our new attack relies on a method whose first phase is a 2D cartography allowing the attacker to find the precise location of the targeted crypto module activity [START_REF] Sauvage | ElectroMagnetic Radiations of FPGAs: High Spatial Resolution Cartography and Attack of a Cryptographic Module[END_REF]. By carefully positioning the antenna, the number of measurements to disclose (MTD) the key of a non-protected crypto module could be hundred times smaller compared to DPA.

The rest of the paper is organized as follows: Section 2 recall some informations about the concepts applied in our experiments. The target of our attack s described in Sec. 3. Section 4 presents our results, and finally, conclusions and perspectives are given in the Sec. 5.

Related Works

WDDL

To achieve a constant power consumption, the differential DPL logic styles are used in order to "hide" the secret leakage. The logic properties are both spatial (differential logic) and temporal (two phases). A differential logic is such that every variable x is shared in two signals: the "True" x T and the "false" x F , involving a "Dual Rail" routing. Hence the calculation is done differentially with two logic networks, True and False, receiving respectively the True and the False signals. The DPL temporal property consists in splitting the calculation in two phases: precharge and evaluation. During the precharge phase the signals are forced in a state such that the number of transitions is constant when switching from the precharge to the evaluation phase, and vice versa. As the power consumption is directly related to the number of transitions in CMOS technology, the activity is constant whatever the variables values. For instance in WDDL the precharge phase is such that all the signals are reset to the value 0. This value is propagated along the logic cones as the True and False logic networks are composed with positive functions only. When switching a variable x enters the evaluation phase, either x T or x F goes from 0 to 1 but never both. DPL needs a perfect balance between the True and False networks propagation time otherwise bias like early evaluation makes attacks possible as explained in [START_REF] Suzuki | Random Switching Logic: A Countermeasure against DPA based on Transition Probability[END_REF]. Consequently the design flow needs special at the synthesis (front-end) and place and route (back-end) stages. The back-end operations are not so easy when targeting FPGA [START_REF] Guilley | Place-and-Route Impact on the Security of DPL Designs in FPGAs[END_REF][START_REF] Guilley | Shall we trust WDDL?[END_REF] where interconnects structure is imposed by the vendor. . In ASICs, back-end technique's like fat wire [START_REF] Tiri | Place and Route for Secure Standard Cell Design[END_REF] and back-end duplication [START_REF] Guilley | The "Backend Duplication" Method[END_REF] permits the generate of well balanced designs. The bias like early evaluation is difficult to mitigate. Patrick Schaumont propose a solution for FPGAs in [START_REF] Yu | Secure FPGA circuits using controlled placement and routing[END_REF]. It consists in duplicating the WDDL such a way that the True and False Networks are inverted between the two WDDL instances. This is however rather costly as the complexity is at least multiplied by 4 w.r.t. a non protected design. In ASICs some secure libraries have been developed. The one developed in [START_REF] Guilley | CMOS Structures Suitable for Secured Hardware[END_REF] relies on synchronization between signals ans offers a great level of protection. In this paper we target a WDDL implementation which has no specific effort of Placing and Routing but which remains unattacked until now.

Another bias of WDDL comes from the glitches generation if WDDL is not implemented in a proper way [START_REF] Guilley | Evaluation of Power-Constant Dual-Rail Logic as a Protection of Cryptographic Applications in FPGAs[END_REF]. The use of positive functions solves this problem and delivers what we call "Positive" WDDL (WDDL+). We evaluate in this paper the robustness of this latter.

ElectroMagnetic Cartography

The new attack takes advantage of a two-step method, whose first one consists in spotting the best location to attack. One of the first EM cartography of an integrated circuit (IC) to be reported is that of J.-J. Quisquater and D. Samyde on an 8-bit smart card processor [START_REF] Quisquater | ElectroMagnetic Analysis (EMA): Measures and Counter-Measures for Smard Cards[END_REF]. The principle is to acquire temporal traces for every point of a 2D grid covering all or only a part of the targeted chip. This grid corresponds to the set of positions of the antenna placed by means of a X-Y motor driven table. Then, a post processing has to be applied on the temporal traces to build the final map.

In the temporal domain, the post processing to attack a cryptoprocessor can be the computation of the difference between the maximum amplitude of the EM field and the mean amplitude of differential traces. In the frequency domain, the Discrete Fourier Transform (DFT) of each trace (i.e. each point) permits the detection of a specific frequency intrinsic to the attacked module.

The same exercise on other devices (for instance FPGAs) has not been reproduced, and therefore, the EM exploration of deep-sub micron device remains an open topic of research, especially in the field of trusted computing. The second step is to attack the selected location(s) by DEMA.

The FPGA-based crypto SoC

Several experiments to evaluate the security of an implementation relies on the design of only a part of a cryptographic algorithm. With no special care, when performing analysis, emerging correlations could be du to this restriction on the design, whereas we are looking for correlations du to the inside computations. For example, considering the obvious test of a single Substitution Boxes (SBoxes) of DES or AES. If the output of the SBoxes is provided outside of the chip for computation checking, correlations comes from the power consumption (or the EM field) of the I/O slots, not from the power consumption of the SBoxes logic elements.

To prevent from such problem and attack a real-life application, we design a complete System on Chip (Soc) including a master processor for I/O communication and crypto co-processors for encryption with standard algorithms such as DES, 3DES, AES. This way, total control on I/O operations is done, and none occur during computations.

The Soc includes unprotected modules which serve as reference to evaluate security of protected ones. We can see on the Fig. 1 the floorplan of the Soc, with 2 regular DES modules (references) on the top left and bottom left corners, and the WDDL+ module and the right.

The Soc is programmed in an EP1S25 "Stratix" Altera FPGA (130 nanometers technology), embedded on a "SHIX2.0", an 8-layer PCB professional board.

Experimental Results

As background material, we used antennas of the "HZ-15 Probe Set" [START_REF]HZ-15 Probe Set[END_REF] from "Rohde and Schwarz" [11], and two pre-amplifiers for an overall gain of 60 dB in the frequency range from 100 kHz to 3 GHz. The output signal of the pre-amplifiers is digitized by an 54855 Infiniium Agilent oscilloscope whose bandwidth is 6 GHz and maximal sam- ple rate is 40 GSa/s. The antenna is mounted on a 2D motorized table and moved over the FPGA through an area of 2.08 cm × 2.00 cm. The resolution is of 50 points on X and on Y. In others words, the mechanical step is equal to 40 µm. Fig. 2 is a photographic of the experimental setup, with the antenna over the most leaking point.

Spotting by Cartography

The acquisition needs no averaging or synchronization as it could be the case for a post processing exploiting the temporal characteristics. Indeed, averaging is powerful to reduce the noise and to discern pattern in a temporal traces, but as the method focus on a specific frequency, contribution of the noise on this latter is minimum because it is spread over the entire frequency range. As a consequence, this slightly reduces the number of message to be intercepted. To prove our ability to distinguish precise areas of the FPGA, we have build the map for a frequency of 100 MHz (fourth harmonic of the FPGA clock frequency of 20 MHz). The results is depicted by the Fig. 3 (left). The dashed rectangle is a landmark which delimits the ASIC of the FPGA. On the right, the scale gives the voltage dynamic range at the output of the antenna (proportional to the EM field). The highlighted area on the left bottom of the picture corresponds to the bound wires carrying the 20 MHz master clock. Now, to locate the WDDL+ co-processor, we have to guess its frequency signature. As explained is Sec. 2.1, WDDL runs in 2 phases: precharge and evaluation. In our implementation, they occur on the rising edge of the SoC clock, which frequency is 8.333 MHz. Indeed, internal frequency of the WDDL+ DES co-processor can be viewed as being equal to half of this of the SoC clock, and then equal to 4.166 MHz. The map for this latter is given by the Fig. 3 (right).

Y X Motorized FPGA board H probe X-Y table
Four area are standing out: two in the top and two in the right of the figure. The Tab. 1 gives the coordinates and the amplitude of their maximum.

Table 1. Coordinates and Amplitudes of the Maximums.

Area X [cm] Y [cm] Amplitude

EMA Attack

For all the relevant areas, a new acquisition has been performed. The acquired traces are the mean of 256 real traces grabbed by the oscilloscope with performs the averaging and is triggered by an external signal to get coherent traces. The attack on the R register has been lead after the first round of DES. On the rest of the paper, we will focus on this which gives the best results, the number 2, marked "Most leaking area". A 256 times averaged temporal trace of the EM field at this point is depicted by the Fig. 4. We can observe that the EM field is negative for the precharge, positive for the evaluation. This could be explained by the current inversion of the CMOS capacitors. At the beginning of the precharge phase, the CMOS gates of WDDL go from 1 to 0 , whereas this is the other way round when switching from the precharge phase to the evaluation phase.

Tab. 2 recalls the minimum number of MTD needed for Power Analysis.

For the regular DES module, the best results are obtained by guessing the hamming distance of 4 bits of the R register (coming from the output of each Sbox). For WDDL+, because of the precharge, the best results are obtained by guessing the hamming weight of these 4 bits. In this last case, only one Sbox is broken, which experimentally prove that WDDL+ is well suited to protect from Power Analysis. Results for the Electro-Magnetic Analysis are reported in the Tab. [START_REF] Guilley | The "Backend Duplication" Method[END_REF].

Its superiority to the C/DPA is well illustrated as the number of MTD for the regular DES module is hundred times less. For WDDL+, it enables to retrieve the secret key in less than 399,360 messages.

In dual rail logic, close bits are attended to balance their power consumption. Indeed, guessing 4 bits could be more efficiency that only one. The bottom of the Tab. 3 shows it isn't really the case.

Finally, Fig. 5 presents for each Sbox the differential traces obtained after the "CEMA -hamming weight" on the protected module.

Another stunning effect is that correlation occurs for certain Sboxes on the precharge phase.

Conclusion and Perspectives

We have reported the first successful attack on an FPGAbased automatically placed and routed WDDL+ DES crypto processor. WDDL+ is well suited against DPA, but fails against the new EMA technique presented in this paper.

Open question is the impact of the constrained place and route on the security. Some answers can be found in [START_REF] Guilley | Place-and-Route Impact on the Security of DPL Designs in FPGAs[END_REF][START_REF] Yu | Secure FPGA circuits using controlled placement and routing[END_REF], but the ultimate one would be given further with a clone of the attack presented here on well placed and routed WDDL+ module.

Figure 1 .

 1 Figure 1. Floorplan of the system-on-chip programmed in a Stratix.

Figure 2 .

 2 Figure 2. The antenna over the "SHIX2.0" board and the FPGA.

Figure 3 .

 3 Figure 3. EM field at 100 MHz (left) and 4.333 MHz (right).

Figure 4 .

 4 Figure 4. EM field at X=0.416 cm and Y=1 cm.

Figure 5 .

 5 Figure 5. Covariance factors obtained for the correct key hypothesis when attacking the first round of the WDDL+ DES module.