Érik Martin-Dorel
email: erik.martin-dorel@ens-lyon.org

Univariate and Bivariate Integral Roots Certificates Based on Hensel's Lifting

Keywords: Coq formal proofs, certifying algorithm, Hensel's lifting, integral roots, polynomials Preuves formelles Coq, algorithme certifiant, relèvement de Hensel, racines entières, polynômes

If it is quite easy to check a given integer is a root of a given polynomial with integer coefficients, verifying we know all the integral roots of a polynomial requires a different approach. In both univariate and bivariate cases, we introduce a type of integral roots certificates and the corresponding checker specification, based on Hensel's lifting. We provide a formalization of this iterative algorithm from which we deduce a formal proof of the correctness of the checkers, with the help of the Coq proof assistant along with the SSReflect extension. The ultimate goal of this work is to provide a component that will be involved in a complete certification chain for solving the Table Maker's Dilemma in an exact way.

Introduction and Motivations

The newly revised IEEE 754-2008 standard for floating-point (FP) arithmetic recommends that some mathematical functions (exp, log, x → 2 x , . . . ) should be correctly rounded (roughly speaking, the system must always return the FP number nearest to the exact mathematical result of the operation). Requiring correctly rounded functions has a number of advantages: among them, it greatly improves the portability of numerical software and it allows one to design algorithms and formal proofs of software that use this requirement. To be able to design fast programs for correctly rounded functions, we must address a problem called the Table Maker's Dilemma (TMD) [15, chap. 12]. We need to locate, for each considered function f and for each considered FP format and rounding mode, the hardest-to-round (HR) points, that is, in rounding-to-nearest, what are the FP numbers x such that f (x) is closest to the exact middle of two consecutive FP numbers. The naive method of finding these points (evaluating the function with large precision at each FP number) is far too impractical.

Two different algorithms have been designed to find these HR points:

-the Lefèvre algorithm -based on a variant of the Euclidean GCD algorithm -which made it possible to obtain HR cases in binary doubleprecision arithmetic [START_REF] Lefèvre | Worst Cases for Correct Rounding of the Elementary Functions in Double Precision[END_REF]14]; -the Stehlé-Lefèvre-Zimmermann (SLZ) algorithm -based on the lattice basis reduction algorithm LLL [START_REF] Lenstra | Factoring polynomials with rational coefficients[END_REF] -which has a better asymptotic complexity [START_REF] Stehlé | Searching Worst Cases of a One-Variable Function Using Lattice Reduction[END_REF][START_REF] Stehlé | Algorithmique de la réduction des réseaux et application à la recherche de pires cas pour l'arrondi des fonctions mathématiques[END_REF] and might allow to get HR cases in double-extended-precision.

The processes that generate these HR points are based on complex and very long calculations (years of cumulated CPU time) that inevitably cast some doubt on the correctness of their results. In the French ANR project entitled TaMaDi, we thus undertake to fully reconsider the methods used to get HR points, with a special focus on their formal validation (by enabling our programs to generate certificates that guarantee the validity of their results).

As regards the SLZ algorithm, the LLL part is the most time consuming part of the overall algorithm so that we can treat the LLL calls as an oracle and log its results in a certificate, the verification of which no longer implies LLL calls. This has the clear benefit of avoiding to have to deal with LLL formally. Still, this approach has to be validated, we need to design "good" certificates that are of reasonable size and can be easily checked, with the goal to provide a fully verified checker for these certificates, in a similar way to what was done for primality certificates in [START_REF] Grégoire | A computational approach to Pocklington certificates in type theory[END_REF][START_REF] Grégoire | A purely functional library for modular arithmetic and its application to certifying large prime numbers[END_REF][START_REF] Théry | Primality proving with elliptic curves[END_REF].

The output of the LLL algorithm contains pairs of bivariate polynomials with integer coefficients, so that we must solve the systems

     P (x, y) = 0, Q(x, y) = 0, |x| A and |y| B, for each (P, Q, A, B) that is produced by LLL (P, Q ∈ Z[X, Y ] and x, y, A, B ∈ Z).
As mentioned in [START_REF] Stehlé | On the Randomness of Bits Generated by Sufficiently Smooth Functions[END_REF], there are several ways to solve this "root-finding step" of SLZ, including Hensel's lifting. But rather than just proving formally this root-finding algorithm, we introduce a type of integral roots certificates and the corresponding checker specification, based on Hensel's lifting, which thus leads to a certifying algorithm as defined in [START_REF] Mcconnell | Certifying Algorithms[END_REF].

In this paper, we present a formalization within the Coq proof assistant [START_REF] Bertot | Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions[END_REF][START_REF]The Coq Proof Assistant: Reference Manual: version 8.2[END_REF]9] along with the SSReflect extension [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF][START_REF] Gonthier | An Ssreflect Tutorial[END_REF] of both univariate and bivariate Hensel's lifting with a uniqueness property from which we deduce a formal proof of the correctness of the integral-roots-certificates checkers.

Organization of the paper. In the upcoming Section 2 we briefly present the use of Hensel's lifting to find the integral roots of a univariate polynomial. In Section 3 we give pen-and-paper sketches of the main proofs related to Hensel's lifting in both univariate and bivariate cases, in order to highlight the required concepts for the formalization. Section 4 is devoted to the Coq formalization itself, namely a description of the Coq mechanized formal background that is common to both univariate and bivariate cases, followed by the presentation of our univariate, then bivariate integral-roots certificates with the corresponding certificate checkers. In Section 5 we discuss the advantages of the approach to design certifying algorithms we have followed, then we draw some conclusions in Section 6.

Notations. We summarize below the mathematical notations used in the sequel.

An overview of Hensel's lifting in the univariate case

The origin of Hensel's lifting is deeply linked to the introduction of the p-adic numbers by Kurt Hensel [START_REF] Hensel | Neue Grundlagen der Arithmetik[END_REF], so that it is also called the p-adic Newton iteration [START_REF] Von Zur Gathen | Modern Computer Algebra[END_REF], though in this work we will focus on statements that are fully expressed in (modular arithmetic on) Z.

A uniqueness property on the modular roots of P ∈ Z[X]

We briefly present the functioning of Hensel's lifting through the following lemma, which is actually a key result of the formalization at stake.

Lemma 1. Let P ∈ Z[X] and p ∈ P that satisfies

∀z ∈ Z, P (z) ≡ 0 (mod p) =⇒ P ′ (z) ≡ 0 (mod p), ( 1
)
where P ′ is the derivative of the polynomial P . If x ∈ Z is such that

P (x) ≡ 0 (mod p 2 m ) ( 2
)
for a given m ∈ N, then for

u 0 := x mod p, ( 3
)
the sequence (u k ) defined by the recurrence relation

∀k ∈ 0, m u k+1 := u k - P (u k ) P ′ (u k ) mod p 2 k+1 (4) satisfies: ∀k ∈ 0, m , u k = x mod p 2 k . ( 5
)
Remark 1. Note that Lemma 1 gives a necessary condition on each root of P ∈ Z[X] modulo p 2 k depending on the value of the considered root modulo p. It is somehow a uniqueness result, whereas usual results about Hensel's lifting such as the correctness theorem we can find in [2, p. 264] are existence results. We will see in Sections 4.2 and 4.3 that we specifically need this uniqueness property to prove our main theorems that deal with integral roots.

A simple bound on the univariate integral roots

We can prove the following lemma that provides more information on a possible choice of bound.

Lemma 2. For any P ∈ Z[X], if we write P in the form

d i=ν a i X i ∈ Z[X] with a ν = 0, we have ∀z ∈ Z, P (z) = 0 ⇒ |z| |a ν |. Therefore B = |a ν | = a min{k : a k =0}
is a bound on the integral roots of P .

Consequently, we can either take the generic bound given by the previous simple lemma, or choose a different bound, notably when we just want to deal with the subset of integral roots that are bounded by a specific B > 0.

The final doubling trick

If we can iterate Hensel's lifting (4) as many times as desired, in practice we can stop as soon as the considered power of p becomes greater than twice the chosen bound B on the integral roots. We explain below why this reasoning is valid.

Assuming we stop the iteration at rank k, we have the following state:

∃k ∈ N,                M := p 2 k M > 2 • B u k = x (mod M ) 0 u k < M |x| B
Thanks to the presence of the coefficient 2 above, the intervals [0, B] and [M -B, M [ are disjoint, which facilitate the computation of x from u k , as shown by Figure 1. More precisely, we can prove the following disjunction:

x 0 ∧ x = u k ∧ u k B x < 0 ∧ x = u k -M ∧ u k M -B,
which enables us to decide which is the sought value of x from a single test on u k . For instance, we can just do

x = u k if u k B u k -M if u k > B to compute x. -M -B 0 B M M -B x (sought) ∈ u k (known) ∈ s → s -M

Example of use

Let us consider the polynomial P (X) := X 2 -X -42 ∈ Z[X], whose roots are -6 and 7. Its derivative is P ′ (X) = 2 • X -1. Using Lemma 2, let us choose B = 42 as a bound. If we consider the small prime number p = 2, we can see at once that the roots of P modulo 2 are 0 and 1, and that the hypothesis ( 1) is fulfilled for both roots modulo p = 2. From u 0 = 0, we compute:

     u 1 = u 0 -P (u 0 )/P ′ (u 0 ) mod 2 2 1 = 0 + 42/(-1) mod 4 = 2; u 2 = u 1 -P (u 1 )/P ′ (u 1 ) mod 2 2 2 = 2 + 40/3 mod 16 = 10; u 3 = u 2 -P (u 2 )/P ′ (u 2 ) mod 2 2 3 = 10 -48/19 mod 256 = 250,
then we stop since 256 > 2×B and the obtained root is 250-256 = -6, following the reasoning of Section 2.3. Likewise, from u 0 = 1, we compute three iterations:

     u 1 = u 0 -P (u 0 )/P ′ (u 0 ) mod 2 2 1 = 1 + 42/1 mod 4 = 3; u 2 = u 1 -P (u 1 )/P ′ (u 1 ) mod 2 2 2 = 1 + 36/5 mod 16 = 7; u 3 = u 2 -P (u 2 )/P ′ (u 2 ) mod 2 2 3 = 7 -0/13 mod 256 = 7,
and the obtained root is 7.

We notice we have found all the roots in Z of the considered univariate polynomial P , namely -6 and 7. In the sequel, we will thus focus on the formal certification of results of this kind, for both univariate and bivariate polynomials.

Pen-and-paper proofs

Before focusing on aspects strongly related to Coq, we present the pen-and-paper proofs that helped us to carry out the formalization at stake.

Pen-and-paper sketch of the proof of Lemma 1

Let us assume all the hypotheses of the theorem hold for P ∈ Z[X], p ∈ P, x ∈ Z, and (u k ) which is defined by ( 3) and (4). To shorten most of the following formulas, we will denote x mod p 2 k by x k for all integer k.

We want to show [START_REF] Gonthier | An Ssreflect Tutorial[END_REF], that is to say, ∀k ∈ N, k m ⇒ u k = x k . We prove it by induction on k:

• First, we can notice that p = p 2 0 , therefore (3) means that u 0 = x 0 , which proves the base case.

• The inductive case amounts to showing that for a given integer k < m satisfying u k = x k , we have u k+1 = x k+1 .

To start with, we can write

x k = x mod p 2 k = x mod p 2 k+1 mod p 2 k = x k+1 mod p 2 k , which implies x k+1 ≡ x k (mod p 2 k ), hence ∃λ ∈ Z, x k+1 = x k + λp 2 k .
We can now apply Taylor's theorem for the polynomial P at point x k+1 :

P (x k+1 ) = P (x k ) + λp 2 k P ′ (x k ) + deg P j=2 λp 2 k j j! P (j) (x k ).
The first member of this equality is zero modulo p 2 k+1 , since

P (x k+1 ) = P (x mod p 2 k+1 ) ≡ P (x) = 0 (mod p 2 k+1 ).
As for the last member, we can notice that

∀j 2, λp 2 k j = λ j • p 2 k j-2 • p 2 k+1 and P (j) (x k ) j! ∈ Z.
Thus all terms in the summation (for j 2) are zero modulo p 2 k+1 . Consequently, Taylor's formula becomes:

0 ≡ P (x k ) + λp 2 k P ′ (x k ) + 0 (mod p 2 k+1 ).
Furthermore, we have P (x k ) ≡ 0 (mod p), hence by (1), P ′ (x k ) ≡ 0 (mod p), and consequently P ′ (x k ) ≡ 0 (mod p 2 k+1 ), which allows us to write:

λp 2 k ≡ - P (x k ) P ′ (x k ) (mod p 2 k+1 ),
Now replacing λp 2 k with x k+1 -x k and using the induction hypothesis leads to

x k+1 ≡ u k - P (u k ) P ′ (u k ) (mod p 2 k+1 ).
Then we recognize the definition (4), which means that we have proved that

x k+1 mod p 2 k+1 = u k+1 ,
that is, thanks to the idempotence of modulo, x k+1 = u k+1 . ⊓ ⊔

Statement of the uniqueness lemma in the bivariate case

Lemma 3. Let P 1 , P 2 be two bivariate polynomials with integer coefficients, and let p be a prime that satisfies:

∀z, t ∈ Z, P 1 (z, t) ≡ 0 ≡ P 2 (z, t) (mod p) =⇒ J P1,P2 (z, t) ≡ 0 (mod p). (6) If (x, y) ∈ Z 2 is such that P 1 (x, y) ≡ P 2 (x, y) ≡ 0 (mod p 2 m ) (7)
for a given m ∈ N, then for

u 0 v 0 := x mod p y mod p , ( 8
)
the sequence (u k , v k ) k defined by the recurrence relation

∀k ∈ 0, m , u k+1 v k+1 := u k v k -J P1,P2 (u k , v k ) -1 P 1 (u k , v k ) P 2 (u k , v k ) mod p 2 k+1
(9) satisfies:

∀k ∈ 0, m , u k v k = x mod p 2 k y mod p 2 k . ( 10
)

Pen-and-paper sketch of the proof of Lemma 3

Let us assume all the hypotheses of the theorem hold for

P 1 , P 2 ∈ Z[X, Y ], p ∈ P,
x, y ∈ Z, and (u k ) , (v k ) which are defined in ( 8) and ( 9) by mutual recurrence. We consider the sequences (x k ) and (y k ) of the modular residues of the root (x, y):

∀k ∈ N, x k y k := x mod p 2 k y mod p 2 k .
We want to show [START_REF] Kahan | A Test for Correctly Rounded SQRT[END_REF], that is to say, ∀k ∈ N, k m ⇒ (u k , v k ) = (x k , y k ). We prove it by induction on k:

• First, we notice that p = p 2 0 , therefore [START_REF] Hensel | Neue Grundlagen der Arithmetik[END_REF] means that (u 0 , v 0 ) = (x 0 , y 0 ), which proves the base case.

• The inductive case amounts to showing that for a given integer k < m satisfying (u k , v k ) = (x k , y k ), we have (u k+1 , v k+1 ) = (x k+1 , y k+1 ).

We write again

x k = x mod p 2 k = [x mod p 2 k+1 ] mod p 2 k = x k+1 mod p 2 k , which implies x k+1 ≡ x k (mod p 2 k ), hence ∃λ ∈ Z, x k+1 = x k + λp 2 k .
Likewise, we obtain:

∃µ ∈ Z, y k+1 = y k + µp 2 k .
Now we can apply Taylor's theorem to each bivariate polynomial P l (l = 1, 2):

P l (x k+1 , y k+1 ) = i,j∈N 1 i!j! ∂ i+j ∂X i ∂Y j P l (x k , y k ) • λp 2 k i µp 2 k j .
The first member of this equality is zero modulo p 2 k+1 , since P l (x k+1 , y k+1 ) = P l (x mod p 2 k+1 , y mod p 2 k+1 ) ≡ P l (x, y) = 0 (mod p 2 k+1 ).

Concerning the second member, we can notice that

∀i, j ∈ N, i + j 2 =⇒ λp 2 k i µp 2 k j = λ i µ j p 2 k i+j-2 • p 2 k+1 and 1 i!j! ∂ i+j ∂X i ∂Y j P l (x k , y k ) ∈ Z,
therefore all terms in the summation such that i + j 2 are zero modulo p 2 k+1 . As a result, Taylor's formula becomes

0 ≡ P l (x k , y k ) + λp 2 k ∂ X P l (x k , y k ) + µp 2 k ∂ Y P l (x k , y k ) + 0 (mod p 2 k+1
). [START_REF] Lefèvre | Worst Cases for Correct Rounding of the Elementary Functions in Double Precision[END_REF] Note that combining both formulas for l = 1, 2, we obtain the following matrix equation:

0 0 = P 1 (x k , y k ) P 2 (x k , y k ) + J P1,P2 (x k , y k ) λp 2 k µp 2 k mod p 2 k+1 .
where the modulo operation is applied coordinatewise. Furthermore, we have P 1 (x k , y k ) ≡ 0 ≡ P 2 (x k , y k ) (mod p), hence by ( 6), J P1,P2 (x k , y k ) ≡ 0 (mod p), and consequently J P1,P2 (x k , y k ) ≡ 0 (mod p 2 k+1 ), which allows us to write

-J P1,P2 (x k , y k ) -1 p 2 k+1 P 1 (x k , y k ) P 2 (x k , y k ) ≡ λp 2 k µp 2 k (mod p 2 k+1 ).
Then, we use the induction hypothesis (x k , y k ) = (u k , v k ) after replacing λp 2 k with x k+1 -x k (resp. µp 2 k with y k+1 -y k ), and we obtain

u k v k -J P1,P2 (u k , v k ) -1 P 1 (u k , v k ) P 2 (u k , v k ) ≡ x k+1 y k+1 (mod p 2 k+1 ).
We eventually recognize the definition (9), which means we have proved that

u k+1 v k+1 = x k+1 y k+1 mod p 2 k+1 ,
that is, thanks to the idempotence of the modulo, (u k+1 , v k+1 ) = (x k+1 , y k+1 ). ⊓ ⊔

Coq formalization

Formal background for Hensel's lifting

In this section we present the various choices we have made to undertake this formalization, along with some new support results that are common to both univariate and bivariate cases.

The SSReflect extension. The Small-scale-reflection (SSReflect) extension of Coq was first used to carry out the formalization of the Four-Colour Theorem [START_REF] Gonthier | Formal Proof-The Four-Color Theorem[END_REF]. It consists of an extension of the Coq proof language as well as a set of Coq libraries developed upon this extension. We chose to use the SSReflect extension for both its tactic facilities and the Coq libraries it provides. In particular, we extensively used the following libraries that supply most of the key concepts involved in our formalization: ssrnat for boolean comparison predicates on the type nat of natural numbers, with the usual operations including exponentiation; prime for the primality predicate prime : nat -> bool; div for the divisibility predicate dvdn : nat -> nat -> bool and the modulo modn : nat -> nat -> nat on which it is based; zmodp for the ExtendedGCD-based modular inversion in Z/qZ (where q will be instantiated by p 2 k ); poly for the ring of univariate polynomials, with the polynomial evaluation, formal derivatives, and Taylor's theorem for univariate polynomials;

We also needed the bivariate version of Taylor's theorem that Laurent Théry proved in the theory bipoly mainly based on poly.

The library on binary integers from the Coq standard library. But we also needed to handle signed integers since we focus on providing certificates of integral roots (in Z). We chose to use the library ZArith on signed, binary integers from the Coq standard library whose type Z is presented below, essentially for the presence of the modulo operation Zmod : Z -> Z -> Z and for efficiency reasons, since the arithmetic operations on Z are much more efficient that those defined on the type nat of Peano, unary integers. For example, the Coq term Zneg (xO (xO (xI xH))) will represent the negative number -12, whose absolute value is 1100 in radix 2.

Polynomials with integer coefficients.

As regards the definition of polynomials, both poly and bipoly theories deal with polynomials with coefficients in a type that have to be equipped with a SSReflect decidable-equality ring structure. Therefore, to be able to talk about polynomials on Z, we first needed to prove that Z satisfies the required axioms of the SSReflect algebraic hierarchy. This is done in our theory ssrz whose first part acts as a wrapper of ZArith to be used within SSReflect. Now the terms {poly Z} and {bipoly Z} typecheck so that we can use them in the sequel to designate univariate and bivariate polynomials on Z. Then we have proved this result with the help of a number of arithmetic lemmas that are gathered in ssrz. Among these auxiliary results there is a key lemma that asserts the "compatibility" between polynomial evaluation and modular reduction:

Lemma ZmodN_horner_compat :
forall (q : nat) (z : Z) (P : {poly Z}), P.[z modN q] = P.

[z] %[ZmodN q].
where the notation P.

[z] represents the polynomial evaluation (horner P z), the notation m = n %[ZmodN q] means m modN q = n modN q, and n modN q (with a big N) is the same thing as n mod (Z_of_nat q) or (Zmod n (Z_of_nat q)).

Specification of our univariate certificates and their checker.

If it would be quite easy to verify the output of an algorithm designed for "finding an integral root x of P ∈ Z[X]" (by verifying the equality "P (x) = 0" holds), the problem we consider in this paper, namely "finding all the integral roots of P ∈ Z[X]," requires a different approach.

We follow the certificate-based approach described in [START_REF] Mcconnell | Certifying Algorithms[END_REF]. The idea is to design a so-called certifying algorithm: for a given input x, one such algorithm produces the same output (say y) as a traditional algorithm, plus a witness w that allows us to verify the result. Roughly speaking, the tuple (x, y, w) forms what we call the certificate. For the particular problem which is at stake (find all the integral roots of P ∈ Z[X]), we thus need to choose an appropriate type of certificate C, then to specify a certificate verifier v : C → B and to formally prove that if v(x, y, w) = true holds, then y is indeed the correct output corresponding to x.

As regards the kind of certifying algorithm that can be used to solve the problem at stake, it suffices to have a Hensel's lifting program that outputs p and k in addition to the list L of the computed roots corresponding to the given polynomial P and bound B.

Then, we can store these data in a form of a certificate, which will be easily checked with our verifier without the need to replay all the iterations of Hensel's lifting.

We consider the following Coq Record as the type of our univariate certificates:

Record uniCertif := UniCertif { uc_P : {poly Z}; uc_B : Z; uc_p : nat; uc_k : nat; uc_L : seq (Z * bool) }.

In other words, a univariate certificate will be a 5-tuple (P, B, p, k, L). It will be called "valid" if the following conditions are satisfied:

-P ∈ Z[X]; -p ∈ P; -replacing the binary integer B ∈ Z with |B| 0 for the sequel:

-k ∈ N such that p 2 k > 2 • B; -L ∈ (Z × B) ℓ , a list of ℓ pairs (ℓ p) such that, denoting L p = {u mod p : ∃b ∈ B, (u, b) ∈ L}, we have: • ∀s ∈ 0, p , s ∈ L p ⇐⇒ P (s) ≡ 0 (mod p);
• the ℓ elements of L p are pairwise distinct;

• ∀(u, b) ∈ L,          P ′ (u) ≡ 0 (mod p), |2 • u| p 2 k , P (u) ≡ 0 (mod p 2 k ), b = true ⇐⇒ u ∈ -B, B ∧ P (u) = 0.
Remarks on the formal verification of our univariate checker. From a formal point of view, we have derived our correctness proof of the certificate verifier specified above by rewriting twice univ_hensel_lemma (corresponding to Lemma 1). Note that the algorithm univ_hensel_iter has been specified in Coq above all for proof purposes, as a "witness" of the uniqueness of modular roots.

Certified integral roots for a pair of bivariate polynomials

Insights into the Coq formalization of Lemma 3. As mentioned in Section 3.3, we needed Taylor's theorem for bivariate polynomials, which is provided in bipoly. Concerning the definition of the type of bivariate polynomials, {bipoly Z} is actually a shortcut for {poly {poly Z}}. We start our "bivariate uniqueness" proof by induction on the integer k. The base case is solved trivially, while in the inductive case we need to invoke the bivariate Taylor's theorem.

Note that to truncate the Taylor expansion in order to retrieve the "first three terms" involved in [START_REF] Lefèvre | Worst Cases for Correct Rounding of the Elementary Functions in Double Precision[END_REF], we needed to prove an appropriate lemma trunc_biv_sum that relies on some "sum bookkeeping", highly facilitated by the bigops SSReflect library.

Finally, we follow the arguments that were presented in a "matrix fashion" at the end of Section 3.3, working coefficient by coefficient. This is accomplished with the help of half a dozen lemmas that are linked to Cramer's rule for 2-by-2 matrices. Specification of our bivariate certificates and their checker. We consider the following Coq Record as the type of our bivariate certificates:

Record bivCertif := BivCertif { bc_P : {bipoly Z}; bc_Q : {bipoly Z}; bc_A : Z; bc_B : Z; bc_p : nat; bc_k : nat; bc_L : seq (Z * Z * bool) }.

One such certificate (P, Q, A, B, p, k, L) will be valid if the following conditions are satisfied:

-P ∈ Z[X, Y ] and Q ∈ Z[X, Y ]; -p ∈ P; -A ∈ N and B ∈ N (same remark than in the univariate case); -k ∈ N such that p 2 k > 2 • A and p 2 k > 2 • B; -L ∈ (Z × Z × B) ℓ s.t., for L p = {(u mod p, v mod p) : ∃b ∈ B, (u, v, b) ∈ L}:
• the ℓ elements of L p are pairwise distinct; • ∀(s, t) ∈ 0, p 2 , (s, t) ∈ L p ⇐⇒ P (s, t) ≡ Q(s, t) ≡ 0 (mod p);

• ∀(u, v, b) ∈ L,                        J P1,P2 (u, v) ≡ 0 (mod p), |2 • u| p 2 k , |2 • v| p 2 k , P (u, v) ≡ Q(u, v) ≡ 0 (mod p 2 k ), b = true ⇐⇒      |u| A, |v| B, P (u, v) = Q(u, v) = 0.
These boolean conditions are formalized in the form of a Coq boolean function biv_check : bivCertif -> bool Remarks on the formal verification of our bivariate checker. Among the various fields involved in our bivariate certificate bivCertif, P, Q, A, B represents the data of the problem, whereas L ′ := {(u, v) : (u, v, true) ∈ L} represents the output of the problem, namely finding the integral roots (x, y) ∈ -A, A × -B, B of (P, Q).

As regards the correctness proof of the bivariate checker, we need to prove that for all certificate that is accepted by the checker, the output stored in it is valid.

To be more precise, the list {(u, v) : (u, v, true) ∈ L} can be defined in Coq in the following manner:

Definition bc_roots (bc : bivCertif) := map fst (filter snd (bc_L bc)).

Then, we derive the correctness proof of biv_check that consists of proving that for all bc : bivCertif such that (biv_check bc) holds, for all (x, y) ∈ Z × Z we have the equivalence |x| A ∧ |y| B ∧ P (x, y) = Q(x, y) = 0 ⇐⇒ (x, y) ∈ (bc_roots bc).

Discussion on the certificate-based approach

First of all, the SLZ algorithm that is the main application of our work is a very complex algorithm whose future implementations will certainly have recourse to approximated calculations as well as nasty code optimizations to save computation time. It is thereby totally excluded to formally prove the algorithm or its implementation. Hence the need to follow the certificate-based approach.

Compared to the formal verification of a traditional algorithm (for providing what we can call a certified algorithm), the certificate-based approach that relies on a certifying algorithm [START_REF] Mcconnell | Certifying Algorithms[END_REF] ensures that the computed result has not been compromised by any bug. Moreover, with this approach we do not need to verify the implemented program nor the algorithm itself. This means that we could even use a "fast-and-dirty program" to do the job, since the result can be easily checked by the certificate verifier that has been formally proved in Coq. In compensation the checker itself has to be somewhat efficient since the approach rely on the individual verification of each result.

Conclusion and Future Work

The algorithm of Hensel's lifting itself has been successfully used in the area of Computer Arithmetic, in particular [START_REF] Kahan | A Test for Correctly Rounded SQRT[END_REF] and [START_REF] Parks | Number-Theoretic Test Generation for Directed Rounding[END_REF] rely on the geometric variant of Hensel's lifting (i.e., with the moduli increasing in a geometric way), for p = 2. In this work, we have introduced some integral roots certificates whose specification is closely related to the semantics of Hensel's lifting. Then we have formally proved in the Coq system the correctness of our certificate checkers: if a certificate is declared valid by our verifier, we are sure that it describes all the integral roots of the considered polynomial(s) below the considered bound. Furthermore, the formal proof of these results relies on a uniqueness property on the modular roots produced by Hensel's lifting that is, up to our knowledge, not very discussed in the literature. Note that the use of Hensel's lifting is two-fold: it can be first used to generate "p", "k" and the corresponding roots, and it is also used in the form of a simple, non-optimized algorithm defined within Coq to reason on the uniqueness of the modular roots it produces.

If we naturally started our work with the univariate case before generalizing to pairs of bivariate polynomials, in the latest stages of the formalization some global improvement ideas actually came from the bivariate case where the efficiency of the approach becomes a central concern. For instance, at first it seemed possible to store (with a boolean) the status of all the numbers modulo p (as in practice p 17) in the univariate case, however in the bivariate case it would have forced us to systematically store p 2 values, with hundreds of superfluous values, for a single certificate. Thus in both univariate and bivariate cases, we provide an integral-roots certificate that is somewhat compact and can be quickly checked by a verifier that does not recompute the prime p nor replays all the iterations of Hensel's lifting. The code of our library will be available along with this research report as soon as it is stable.

During the formalization process, we noticed that most of the semantics of our certificate is carried by the specification of the verifier, and that some slight changes in this specification can lead to "false-negative," namely a given certificate could be wrongly denied by the verifier. We thus envisage to develop some extra proofs that demonstrate the absence of such situations, even though in the certificate-approach the most important thing is not to have "false-positive," which is asserted by our main correctness lemmas.

As said before, this work is within the scope of "certifying algorithms" as introduced by [START_REF] Mcconnell | Certifying Algorithms[END_REF]. The certifying algorithm we have presented will lead to an important component that can be plugged into the "root-finding step" of SLZ [START_REF] Stehlé | On the Randomness of Bits Generated by Sufficiently Smooth Functions[END_REF] to solve the Table Maker's Dilemma in an exact way. The safety of the result is ensured at the same time by the formal verification performed by Coq and by the certificate-based approach that makes it possible to separate the verification of the result from its (possibly intensive) computation.

-

  Z denotes the set of signed integers; -N denotes the set of nonnegative integers; -P denotes the set of prime numbers; -B denotes the set of booleans, that is B := {true, false}; -a, b (for a b in Z) denotes the set of all integers k such that a k b; in other words, a, b = Z ∩ [a, b]; -a, b (for a b in Z) denotes the set Z ∩ [a, b[ = {k ∈ Z | a k < b}; -a mod n denotes the remainder of a modulo n, taken in 0, n ; -a ≡ b (mod n) states the modular equality between a and b; in other words, a ≡ b (mod n) ⇐⇒ a mod n = b mod n. -Z[X] denotes the ring of univariate polynomials with coefficients in Z; -Z[X, Y ] denotes the ring of bivariate polynomials on Z, which can be viewed as the ring (Z[Y ]) [X].

Fig. 1 .

 1 Fig. 1. How to deduce x from u k

  Inductive Z : Set := | Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z. Inductive positive : Set := | xI : positive -> positive | xO : positive -> positive | xH : positive.

  Hypothesis P_roots_mod_p :forall (z : Z), 0 <= z < Z_of_nat p -> P.[z] = 0 %[Zmod p] -> (deriv P).[z] <> 0 %[Zmod p]. Variable x : Z. Variable m : nat. Hypothesis x_root_m : P.[x] = 0 %[ZmodN p^2^m]. Let xk := fun k : nat => x modN p^2^k. Let u0 := x modN p. Let uk := univ_hensel_iter P p_prime u0. Lemma univ_hensel_lemma : forall k : nat, k <= m -> uk k = xk k.

Acknowledgements

The author wishes to thank Guillaume Hanrot, Micaela Mayero, Jean-Michel Muller, Ioana Pasca and Laurent Théry for their precious advice and help.

Handling different definitions of the modular reduction. In this section, we will summarize why we need to use several definitions of the modular reduction in our formalization. Then we will present some lemmas that allow to move from one definition of to another.

So far, we have mentioned two different definitions of the "modular reduction" available in the considered libraries, namely modn on the type nat, and Zmod on Z. The link between modn and Zmod is provided by a key lemma Z_of_nat_moduli:

Note that these two functions differ if the second argument is zero: (modn 2 0) = 2 whereas (Zmod 2 0) = 0, But it is not that distracting since we just need modular reduction modulo q = p 2 k p 2 > 0. Furthermore, for any fixed second argument q 2, none of these functions are homomorphisms, since (m + n) mod q = (m mod q) + (n mod q) in the general case (unless we add a outermost modulo operation in the right-hand-side). However, to prove some key results such as the compatibility between the modulo operation and the polynomial evaluation on {poly Z} as well as {bipoly Z}, we need to apply lemmas that expect a morphism as argument.

Consequently, we need to specify the surjective morphism from Z onto Z/qZ, even though it is just for proving purposes. For this we use the SSReflect theory zmodp that provides a finite type 'I_q representing 0, q -1 for q 1, which becomes a (nontrivial) ring and is denoted by 'Z_q when q 2. More precisely, using the existing surjection inZp from nat onto 'I_q we define ZtoI : forall q : nat, q >= 2 -> Z -> 'Z_q and we prove it is a ring homomorphism for any fixed q 2.

For this latter proof we use extensively the following simple lemma that relate ZtoI and Zmod, and whose proof actually relies on Z_of_nat_moduli: Lemma ZtoI_Zmod : forall (q : nat) (q_gt1 : q >= 2) (z : Z), Z_of_nat (ZtoI q_gt1 z) = Zmod z (Z_of_nat q).

Certified integral roots for a univariate polynomial

Insights into the Coq formalization of Lemma


M L Martins

A S Ferreira

A Sampaio

R Vieira

J Inácio

: A Sampaio

Direct and specific identification of in biological samples using fluorescently labelled DNA probes

Fluorescence in situ hybridisation (FISH) is a suitable technique for the rapid, reliable and cultivationindependent identification of microbial pathogens. This study describes the development of fluorescently labelled rRNA-targeted oligonucleotides and a FISH assay to detect and identify Cryptococcus neoformans in culture and biological samples. All C. neoformans reference and clinical isolates gave positive signals with the specific oligonucleotide probes, whereas all non-target yeast species gave negative reactions with the same probes. The assay was also successfully applied to the detection of C. neoformans cells in cerebrospinal samples from patients with clinical diagnosis of cryptococcosis. The described FISH-based assay revealed to be practical, sensitive and specific for the detection and identification of C. neoformans yeasts.

Introduction

Cryptococcus neoformans is an encapsulated basidiomycetous yeast present in the environment worldwide. Traditionally, C. neoformans has been classified into five serotypes, i.e. A (C. neoformans var. grubii), D (C. neoformans var. neoformans), AD (hybrids of serotypes A and D which have antigens of the polysaccharide capsule related to those of the former), B and C (previously known as C. neoformans var. gattii). Currently, the members of serotypes B and C are considered to belong to a phylogenetically related but distinct species, C. gattii. The inhalation of C. neoformans sensu lato usually results in a self-limited asymptomatic pulmonary infection. However, C. neoformans can also cause disseminated disease, particularly in patients with depressed cell-mediated immunity [START_REF] Casadevall | Cryptococcus neoformans[END_REF], the meninges being the most common site of extrapulmonary infection. The diagnosis of cryptococcosis is based either on direct microscopic examination of clinical samples, such as cerebrospinal fluid (CSF), or on culture and subsequent phenotypic identification of the aetiological agent. In addition to ambiguous results, those conventional assays are time-consuming and lack sensitivity and specificity [START_REF] Casadevall | Cryptococcus neoformans[END_REF]. Fluorescence in situ hybridisation (FISH) has been widely used for the detection and identification of microorganisms, with emphasis on prokaryotic organisms, allowing the direct microscopic visualisation and quantification of individual cells in their natural environments [START_REF] Amann | Single-cell identification in microbial communities by improved fluorescence in situ hybridization techniques[END_REF][START_REF] Amann | Phylogenetic identification and in situ detection of individual microbial cells without cultivation[END_REF]. FISH has also been used to detect and identify fungal organisms, including clinically relevant yeasts such as Candida species [START_REF] Alexander | Cost savings with implementation of PNA FISH testing for identification of Candida albicans in blood cultures[END_REF][START_REF] Gherna | Identification of Candida albicans and Candida glabrata within 1.5 hours directly from positive blood culture bottles with a shortened peptide nucleic acid fluorescence in situ hybridization protocol[END_REF]. The aim of this study was to optimise and evaluate the practicability, sensitivity and specificity of a FISH-based assay for the identification of C. neoformans directly in clinical samples.

Materials and methods

Sixty-one C. neoformans and two C. gattii isolates of several origins, most of them obtained from human immunodeficiency virus (HIV)-positive patients, were used in this work (Table 1). Eighteen strains belonging to other yeasts species, including clinical isolates, were used as negative controls (Table 1). All yeasts were grown aerobically under continuous shaking in YM broth (0.3% w/v malt extract, 0.2% yeast extract, 0.5% peptone, 1% glucose) at 25°C. Cells were harvested in the exponential growth phase (optical density of 2.5 at 600 nm) by centrifugation for 5 min at 13,000 rpm. Cells were washed once with 1× phosphate-buffered saline (PBS) (130 mM sodium chloride, 10 mM sodium phosphate buffer, pH 7.2) and fixed for 4 h with 4% w/v paraformaldehyde in PBS at 4°C. After fixation, cells were washed twice with PBS, resuspended in one volume of PBS and one volume of cold absolute ethanol and stored at -20°C until use. A total of 18 CSF and 10 blood samples from HIVpositive patients with clinical diagnosis of cryptococcosis received for routine conventional testing at the Institute of Hygiene and Tropical Medicine and at the Hospital Santa Maria, both in Lisbon, were also included in this study. Additionally, negative CSF samples were artificially infected with C. neoformans PYCC 3957 T type strain (seven samples) or other clinically relevant yeasts species (seven samples) and used as positive and negative controls, respectively. Each biological sample was also examined for the presence of encapsulated budding yeast by India ink preparation using microscopy (CSF samples), for the presence of cryptococcal polysaccharide antigen by latex agglutination test (Pastorex Crypto Plus, Bio-Rad) (CSF and blood samples) and by culture on Sabouraud glucose agar (CSF samples), according to standard procedures [START_REF] Casadevall | Cryptococcus neoformans[END_REF][START_REF] Martins | Polimorfismos fenéticos e diagnóstico molecular de Cryptococcus neoformans[END_REF]. Additionally, 1 ml of each CSF sample was centrifuged at 13,000 rpm for 5 min to pellet yeast cells, which was then washed once with 500 μl of 1× PBS and fixed with 4% paraformaldehyde as described above. Blood samples were treated as previously described [START_REF] Lischewski | Detection and identification of Candida species in experimentally infected tissue and human blood by rRNA-specific fluorescent in situ hybridization[END_REF] and the resulting lysates were treated as for CSF samples. Two 26S rRNA-targeted species-specific oligonucleotide probes were designed for C. neoformans, which are also complementary to the closely related C. gattii: GTCGCGTTACTTGGGAGT). Probes EUK516 (5′-ACCA GACTTGCCCTCC), universal for eukaryotic organisms, and EUB338 (5′-GCTGCCTCCCGTAGGAGT), targeting all bacteria, were used as positive and negative hybridisation controls, respectively [START_REF] Amann | Combination of 16S rRNA-targeted oligonucleotide probes with flow cytometry for analyzing mixed microbial populations[END_REF]. All probes were labelled at their 5′end with the fluorochrome Cy3 (MWG Biotech, Ebersberg, Germany). Approximately 10 6 fixed yeast cells obtained from cultures, and whole fixed pellets obtained from clinical samples, were hybridised in 20 μl of hybridisation buffer (0.9 M NaCl, 0.01% w/v SDS, 20 mM Tris-HCl, pH 7.2 and 45% formamide for Cne448, 10% for Cne205 and 20% for EUK516 and EUB338), with 1.5 ng of Cy3-labelled probe and incubated at 46°C for 2 h. After incubation, cells were pelleted by centrifugation and resuspended in 1 ml of prewarmed washing buffer (20 mM Tris-HCl, pH 8.0, 0.01% w/v SDS, 5 mM EDTA and 400 mM NaCl for Cne448, 125 mM for Cne205 and 225 mM for EUK516 and EUB338 probes) for 30 min at 46°C. The suspension was then centrifuged and the pellet resuspended in 50 μl of 1× PBS, placed on ice and analysed within 3 h. For each sample, 10 μl of hybridised suspension was spotted onto precleaned microscopic slides and dried at 37°C for 20 min. The slides were then mounted with Vectashield solution (Vector, Burlingame, CA, USA) and examined with an Olympus BX50 microscope, fitted for epifluorescence microscopy with a U-ULH 100W mercury high-pressure bulb and a U-MA1007 filter set for the fluorochrome Cy3 (Olympus). Microphotographs were taken using a digital camera (Olympus C3030-Z00M) and edited using standard software (Adobe Photoshop 6.0, Adobe).

Cne448 (5′- C C A G C C C T TAT C C A C C G A ) a n d C n e 2 0 5 ( 5′ -

Results and discussion

Positive 2). Ten culturepositive CSF samples revealed to be also positive by FISH. Additionally, four culture-negative CSF samples revealed to be FISH-positive (two of these samples were also positive by direct microscopy with India ink; cryptococcal antigens were detected in all four). The detection limit of our Cne205 probe-based FISH assay was estimated to be 10 2 cells/ml when using serially diluted artificially spiked CSF samples (data not shown). Four CSF samples were negative by all tests performed. The detection of C. neoformans from blood samples was more difficult, with cells presenting less intense fluorescence signals (Table 2). Other groups have recently reported positive outcomes on the introduction of FISH-based assays in the routine of their clinical laboratories [START_REF] Alexander | Cost savings with implementation of PNA FISH testing for identification of Candida albicans in blood cultures[END_REF][START_REF] Peters | Faster identification of pathogens in positive blood cultures by fluorescence in situ hybridization in routine practice[END_REF]. The incorporation of these assays as part of the initial yeast laboratorial identification algorithm can result in substantial savings for hospitals [START_REF] Alexander | Cost savings with implementation of PNA FISH testing for identification of Candida albicans in blood cultures[END_REF]. FISH associates the fastness, sensitivity and specificity of molecular diagnostic methods with the observation of morphologic features of the aetiological agents of disease, contributing to a reliable identification of the pathogens directly in their substrates and leading to the consequent definition of the most appropriate treatment. To the best of our knowledge, we describe in this study the first FISHbased assay for the detection and identification of C. neoformans yeasts, which revealed to be practical, sensitive and specific when compared to the conventional methods. FISH may constitute a valuable complementary tool to conventional C. neoformans laboratory analysis, especially when using CSF samples. It can be automated and implemented in hospital laboratories with a great number of analyses per day.

Table 1

 1 List of strains and species used for the optimisation of the fluorescence in situ hybridisation (FISH) assay and respective hybridisation results

	Species	Strain	Serotype a Origin	Hybridisation results
					Cne448 Cne205 EUK516 EUB338
	Cryptococcus	CN137 T (=	D	Fermenting fruit juice	+	+	+	-
	neoformans	PYCC 3957 T ;
		CBS 132 T )
		CN4	A	CSF of an HIV 2-infected patient, Guine Bissau	+	+	+	-
				(1992)
		CN23	A	CSF of an HIV 1-infected patient, Curry Cabral's	+	+	+	-
				Hospital, Lisbon (1995)
		CN27	A	CSF of an HIV 1-infected patient, Angola (1995) +	+	+	-
		CN34	A	CSF of an HIV 1-infected patient, Military's	+	+	+	-
				Hospital, Lisbon (1995)
		CN38	AD	Blood of an HIV 1-infected patient, Santa	+	+	+	-
				Maria's Hospital, Lisbon (1996)
		CN40	AD	CSF of an HIV 1-infected patient, Santa Maria's	+	+	+	-
				Hospital, Lisbon (1996)
		CN43	A	CSF of an HIV 1-infected patient, Institute of	+	+	+	-
				Hygiene and Tropical Medicine, Lisbon (1996)
		CN48	D	Skin of an HIV 1-infected patient, Curry Cabral's	+	+	+	-
				Hospital, Lisbon (1996)
		CN52	AD	Blood of an HIV 1-infected patient, Santa Maria's	+	+	+	-
				Hospital, Lisbon (1996)
		CN54	A	CSF of an HIV 1-infected patient, Cascais's	+	+	+	-
				Hospital, Cascais, Portugal (1996)
		CN55	A	CSF of an HIV 1-infected patient, St. António's	+	+	+	-
				Hospital, Oporto, Portugal (1996)
		CN57	A	CSF of an HIV 1-infected patient, Cascais's	+	+	+	-
				Hospital, Cascais (1996)
		CN59	A	CSF of an HIV 1-infected patient, Santa Maria's	+	+	+	-
				Hospital, Lisbon (1996)
		CN65	A	CSF of an HIV 1-infected patient, St Antonio's	+	+	+	-
				Hospital, Oporto, Portugal (1996)
		CN68	D	Skin of an HIV 1-infected patient, Egas Moniz's	+	+	+	-
				Hospital, Lisbon (1996)
		CN73	AD	Skin of an HIV 1-infected patient, Curry Cabral's	+	+	+	-
				Hospital, Lisbon (1996)
		CN80	D	CSF of an HIV 1-infected patient, Institute	+	+	+	-
				Pasteur, Paris (1997)
		CN88	A	CSF of an HIV-infected patient, St. António's	+	+	+	-
				Hospital, Oporto (1997)
		CN95	A	CSF of an HIV 1-infected patient, Caxias	+	+	+	-
				Prisoner Hospital, Lisbon (1997)
		CN100	A	CSF of an HIV 1-infected patient, St. José's	+	+	+	-
				Hospital, Lisbon (1997)
		CN107	AD	CSF of an HIV 1-infected patient, S. Francisco	+	+	+	-
				Xavier's Hospital, Lisbon (1997)
		CN112	A	Pigeon faeces, Lisbon	+	+	+	-
		CN312	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN313	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN314	nd	Bronchial aspirate, St. António's Hospital,	nd	+	+	-
				Oporto (2008)
		CN315	nd	Blood, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN316	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN317	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN318	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN319	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN320	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-
		CN321	nd	CSF, St. António's Hospital, Oporto (2008)	nd	+	+	-

Table 1 (

 1

	continued)
	Species	Strain	Serotype a Origin	Hybridisation results
					Cne448 Cne205 EUK516 EUB338
	Candida	IHMT 195/98	na	Human vaginal exudate (1998)	-	-	+	-
	parapsilosis
	Cryptococcus	PYCC 2409 T	na	Atmosphere (Japan)	-	-	+	-
	albidus	(= CBS 142 T )
		CN71	na	Blood	-	-	+	-
	Cryptococcus	PYCC 3966 T	na	Palmwine (Congo)	-	-	+	-
	laurentii	(= CBS 139 T )
	Debaryomyces	CN15	na	Pigeon excreta	-	-	+	-
	hansenii
	Rhodotorula glutinis PYCC 4177 T	na	Atmosphere	-	-	+	-
		(= CBS 20 T )
	Saccharomyces	PYCC 4455 T	na	Brewer's top yeast (Netherlands)	-	-	+	-
	cerevisiae	(= CBS 1171 T )
	Sirobasidium	PYCC 5289	na	Unknown	-	-	+	-
	magnum
	Trichosporon	IHMT 256/97	na	Human vaginal exudate (1997)	-	-	+	-
	cutaneum

a According to Martins

[START_REF] Martins | Polimorfismos fenéticos e diagnóstico molecular de Cryptococcus neoformans[END_REF]

nd = not determined; na = not applicable; T = type strain; CSF = cerebrospinal fluid All strains are maintained at the Mycology Lab ('CN' and 'IHMT' strains) of the Institute of Hygiene and Tropical Medicine (IHMT/UNL), Lisbon, Portugal, at the Portuguese Yeast Culture Collection ('PYCC' strains), Caparica, Portugal, and at the Centraalbureau voor Schimmelcultures ('CBS' strains), Utrecht, The Netherlands

  hybridisation signals were determined as bright orange fluorescent yeast cells. All 61 C. neoformans and C. gattii isolates gave positive signals with Cne448 and/or Cne205 probes, whereas all non-target species gave negative reactions with the same probes (Table1). It was also possible to identify C. neoformans cells with the specific probes in mixed samples with other yeast species. All yeast species tested yielded strong fluorescent signals with the universal probe EUK516. None of the yeast cells showed any fluorescent signal with the EUB338 probe (Table1). FISH with the Cne205 probe always showed stronger fluorescent signals than with the Cne448 probe. This can be explained since the complementary target of the later probe is located in a low-accessibility rRNA region for FISH[START_REF] Inácio | In situ accessibility of Saccharomyces cerevisiae 26S rRNA to Cy3-labeled oligonucleotide probes comprising the D1 and D2 domains[END_REF]. Probe Cne205, which presented the brightest fluorescent signals, was evaluated for the detection of C. neoformans in clinical samples. A group of cerebrospinal and serum fluid samples was firstly examined and the direct identification of C. neoformans cells in all artificially infected samples was achieved. The assay was then applied in cerebrospinal and serum samples from patients with clinical diagnosis of cryptococcosis, in parallel with other conventional diagnostic methods (Table

	Table 2 List of cerebrospinal fluid (CSF) and blood samples analysed by conventional diagnostic methods and by FISH	IHMT no.	Sample	Microscopy with India ink a	Sabouraud culture b	Title of cryptococcal polysaccharide antigen c	FISH d
	with the probe Cne205
		383/97	CSF	Negative	Negative	1:10,000	+ +
		393/97	CSF	Negative	Negative	1:1,000	+ +
		397/97	CSF	Negative	Positive	1:10,000	+ +
		421/97	CSF	Positive	Negative	1:10,000	+ +
		580/97	CSF	Positive	Positive	1:1,000	+ +
		594/97	CSF	Positive	Negative	1:10,000	+ +
		600/97	CSF	Positive	Positive	1:10,000	+ +
		37/99	CSF	Positive	Positive	1:10,000	+ +
		59/99	CSF	Negative	Negative	Negative	Negative
		277/99	CSF	Positive	Positive	1:10,000	+ +
		99/01	CSF	Positive	Positive	1:2,048	+ +
		167/01	CSF	Positive	Positive	1:1,000	+ +
		186/01	CSF	Positive	Positive	1:10,000	+ +
		190/01	CSF	Negative	Negative	Negative	Negative
		197/01	CSF	Negative	Negative	Negative	Negative
	a Positive: detection of encapsulat-	202/01	CSF	Negative	Negative	Negative	Negative
	ed yeast cells on samples b Positive: Cryptococcus neofor-mans colonies detected c Positive: detection of C. neofor-mans antigen presence in the	54/02 274/02 394/97 523/97	CSF CSF Blood Blood	Positive Negative nd nd	Positive Positive nd nd	1:1,000 1:1,500 1:10,000 1:10,000	+ + + + + +
	clinical sample	525/97	Blood	nd	nd	1:10	Negative
	d Detection of fluorescent yeast	595/97	Blood	nd	nd	1:10,000	+
	cells with FISH probe Cne205: +	597/97	Blood	nd	nd	1:10,000	+
	+, bright and intense fluorescently labelled yeast cells; +, yeast cells with a faint fluorescent signal;	621/97 625/97	Blood Blood	nd nd	nd nd	1:1,000 1:1,000	+ +
	Negative, no fluorescent yeast	187/01	Blood	nd	nd	1:10,000	+
	cells detected	110/02	Blood	nd	nd	1:100	+
	CSF = cerebrospinalfluid;	275/02	Blood	nd	nd	1:1,000	Negative
	nd = not determined

two

Eur J Clin Microbiol Infect Dis (2010) 29:571-576

Acknowledgements We thank Maria José Salgado and Lurdes Monteiro (Hospital de Santa Maria, Lisbon), Zélia Saraiva and Teresa Tendeiro (Instituto Português de Oncologia, Lisbon), and Virgínia Lopes (Hospital de Santo António, Oporto) for providing the yeast isolates and/or clinical samples. The authors would also like to acknowledge Prof. Isabel Spencer-Martins, prematurely deceased on June 15th 2008, for her valuable suggestions on the present work.


Dr Richard A Ward
email: richard.a.ward@astrazeneca.com

Using Protein-Ligand Docking To Assess The Chemical Tractability Of Inhibiting A Protein Target

Keywords: Protein-Ligand Docking, Druggability, Ligandability Protein-ligand docking  Druggability  Ligandability

Assessing the difficulty of inhibiting a specific protein by a small molecule can be highly valuable in risk-assessment and prioritisation of a new target. In particular, when the disease linkage for a number of targets is broadly similar, being able to identify the most tractable can have a significant impact on informing target selection. With an increasing focus against new and novel protein classes, being able to assess the most likely targets to yield lead-like chemical start points can guide the selection and the lead-generation strategy implemented. This study exploits protein-ligand docking studies on published protein x-ray crystal structures to provide guidance on the feasibility of identifying small molecule inhibitors against a range of targets.

Response to Reviewers: 1) I am not convinced that a biased fragment library (the bias is introduced via the filter criteria for logP, MW, and other parameters) should be able to judge the tractability of any target in general. What if potent fragment binders could not idenitified via docking just because they were removed from the initial fragment collection because of the filter criteria ? This concern is somehow reflected already in Fig 7A and7B. A more general characterization of the fragment library (as expressed by the mean score of t he top 10% docking hits) is only hardly able to distinguish between druggable and "prodrug" binding sites (SP) or "prodrug" and undruggable sites (XP) . A more rigorous approach could for instance be based on a random selection of compounds rather than on a biased fragment library.

The key criteria used to build this fragment library is chemical/structural diversity (there is a reference to the details behind how this library was built). This ensures that the library covers a broad range of scaffolds and interaction types. This allows the mapping of a target binding site by fragment screening (experimentally or computationally). The reason for focusing this fragment library around the stated criteria is that fragment hits with properties in these ranges are suggested as being good chemical start points for fragment-based lead generation projects where achieving an orally bioavailable drug is the aim (i.e. a molecule largely compliant with Lipinski-like criteria). See the report below (also reference 12) from Astex on 'Rule of Three' criteria. Our fragment library, however, has not been filtered as harshly as this library as we want to maximise the information from the screen (which is to some extent addressing the issue raised by the reviewer).

12. Congreve M, Carr R, Murray C, Jhoti H A (2008) 'Rule of Three' for fragment-based lead discovery? Drug Discovery Today 8:Issue 19:876-877

The other key reason for using this library is that published fragment libraries (filtered similarly to the library I have used in this study) have been used to assess drugability using experimental screening approaches as shown in the reference 4 in the manuscript (below). Therefore there is validation for the use of libraries filtered by these criteria to assess drugability experimentally so I believe it is a suitable fragment set to assess targets computationally. Due to molecule complexity arguments (Andrew Leach's work for example) then you can sample chemical space well at the fragment level but when the compounds get larger then the coverage of chemical space is much smaller, this is the main reason why MW cut-offs have been used. So an aim of my work is to try and get similar information from this computational approach as what you get experimentally, which does mean using similar fragment sets. It is true that some targets may produce tighter binding hits with fragments outside of these criteria but these are going to be more challenging to develop into a lead series (and then a drug candidate). For example if fragments identified are more lipophillic (i.e. ClogP >3/4) then whilst the fragments are developed into a lead series the lipophillicity will further increase and it will be difficult to achieve a drug with suitable properties to show oral bioavailability. And larger fragments will not cover chemical space as efficiently. So identifying tight binding fragments with unwanted properties may not be a useful indication of drugability, although clearly this information may tell you something about what the protein 'wants'. However, as oral bioavailability may not always be the aim I agree that it would be interesting to consider fragment sets with higher and lower lipophillicity for example. This will be particularly useful for considering targets such as protein-protein interactions, and due to the possible limitations of using screening techniques on more lipophillic (and likely less soluble fragments) then it could be particularly powerful. This is beyond the scope of the work in the manuscript but something I will have a look at. I have made some modifications to the manuscript to address this comment. I believe the reasoning that using the top 10% of hits is less successful is mainly down to the differences in the profile of the docking scores across the fragment set across different targets (i.e. some have quite steep profiles, some flatter). This is also the reason for looking at the data in the form of figure 8 for an alternative view. Therefore using a rigid rule like the top 10% wasn't successful, along with other measures assessed. The mean score remains as being the most useful in capturing the information in the docking scores and giving good separation for the 'druggable' and 'undruggable' categories, which is clearly the major aim. If a random subset of the fragment set was used instead then the conclusion would be similar to the full set in most cases. However it is important to ensure that the fragment set is a sufficient size to contain good diversity and in terms of covering chemical space.

2) Secondly, even if a high (in-silico) affinity binder is found, it is not guaranteed that this fragment can be grown into a potent and drug-like lead. What is the link between an in-silico fragment affinity (docking score) and the final profile of an inhibitor ? This is of special relevance for the class of 'prodrugs / transporters'. The active principle of prodrugs very often reaches high potencies on the target level. Why should fragments bind less tight to these targets ?

There is significant literature around (and linked above) that fragments with properties in the 'Rule of 3'-like space are suitable start points for the delivery of an orally bioavailable drug. A number of the references in the manuscript address this. The ability to identify tight binding fragments for a target doesn't always mean that they can be elaborated into a candidate drug (that's the reasoning for differentiating the terms 'drugability' and 'ligandability') but the ability to find fragment hits against a target is an important first step in understanding if finding high affinity ligands may be possible. So its shown that if you can't find fragment hits then it will be very difficult to identify a candidate drug. This information helps with the risk assessment against a target. I agree that the 'prodrug/transporter' issue is less clear, this is why they have been separated in the Cheng paper and why I also kept them separate. You can clearly identify potent inhibitors against these targets, but in most cases the key functionality has to be masked due to the warhead being highly charged (or reactive) for example. So the reason why the fragments tend to bind less well to these targets is likely due to the fact that these highly charged warheads are not present in the fragment set but are required for tight binding. However simple acids, bases and charged groups are populated in the fragment set I have used. I think an alternative fragment set may be required to fully assess these targets but the fragment set I've used is still answering the key question around conventional drugability (i.e. likelihood of identifying an orally bioavailable drug against the target). I have added some text around this in the revised report, this also links in with the comments below around correlations with MW/ClogP. I have also added this reference into the manuscript. 30. Rautio J, Kumpulainen H, Heimbach T, Oliyai R, Oh D, Järvinen T, Savolainen J (2008) Prodrugs: design and clinical applications. Nature Reviews Drug Discovery 7:255-270

3) Is there any reason to skip certain targets from the Cheng study ? For a proper head-to-head comparison (which is the key point in this manuscript) the entire data set should have been investigated. In general, a statistical assessment (like for instance p values for the separation of two classes) would be important.

I have added the p-values for the key results in Figure 6 (p-Value=0.0052 for SP protocol and p-Value=0.0041 for XP) and Figure 7 (p-Value=0.0212 for SP protocol and p-Value=0.0944 for XP) . I analysed what I considered to be a reasonable number of the Cheng targets to satisfy myself that the results were largely consistent with their approach and the assessment of the target from the known inhibitors. I covered the majority of the 'undruggable' and 'transporter/prodrug' targets (which had the smallest number of targets) and sampled from the larger 'druggable' set. I did not miss any results out of my manuscript I just chose not to run them all due to other time pressures at work. In the manuscript I have looked in more detail at specific targets and in some cases considered a greater number of protein structures in the drugability assessment than in the Cheng paper. I therefore chose to look in more detail at a smaller numbers of targets, but enough to be able to perform a comparison. I am now running the approach on novel, in-house targets which I hope to publish at a later date although these are confidential at present. I have made some modifications to the manuscript to explain this further. 4) What is the conclusion from the differences between XP and SP ? If computational speed is the only factor to differentiate between both protocols, one of them can be skipped. I would then suggest to take a completely different docking protocol into account as second approach.

Going forwards I would use the SP protocol routinely. I have made this more obvious in the manuscript. 5) Is there a correlation between MW or logP and the docking score for any particular target ? Even if this is not the case -were ligand efficiencies considered as criterion to distinguish druggable from nondruggable sites ?

I had looked at this, none of the targets showed any convincing trend between MW and ClogP. I had reported the mean scored across all targets (Figure 2) to try and show this. Interestingly, any targets tested in future which do show a significant correlation with MW or ClogP may suggest that fragments with higher affinity may be found outside this property space, linking in with some of the comments above. I have added some additional comments around this in the manuscript. I did also looked at ligand efficiencies (docking score/heavy atoms) but the separation between the 'drugable' and 'undrugable' categories using this measure was made worse. Plot shown below for SP protocol data.

SEE ATTACHED FILE FOR GRAPH.

6) How do the docking scores (say for the top fragment) compare to the hightest experimental affinity that is known for each target ? This would be more meaningful than a comparison with the Cheng model.

The issue I have with this method is that it uses the docking score of a single fragment against a target to represent the ligandability for that target. Docking scores are not robust or accurate enough to allow the score for a single fragment to be able to represent a target. This is why a diverse fragment set was docked and the mean score used to allow differentiation of targets. The plots below show the results of doing this analysis of the top fragment against the highest experimental efficiency, clearly there is no correlation. I also believe that the specific choice of fragments screened would then be more important for this method to work, which was one of the concerns raised in the first point.

SEE ATTACHED FILE FOR GRAPH.

Additionally, reflecting how experimental druggability data is used to assess a target although the most potent fragment identified is of interest the hit rate and numbers of fragments with measurable binding is also key to fully assess drugability. Therefore the protocol I have used of considering the mean fragment score from the docking to represent docking is probably the most comparable to this, along with giving the best separation between 'drugable' and 'undrugable' categories.

Introduction

It has been reported that 60% of small-molecule drug discovery projects fail due to the lack of suitable leads [START_REF] Brown | Rediscovering the sweet spot in drug discovery[END_REF]. The term 'druggability' has subsequently been used to capture the feasibility of inhibiting a specific target with an orally bioavailable small molecule [START_REF] Hajduk | Druggability indices for protein targets derived from NMR-based screening data[END_REF]. Some estimates indicate that only 10% of genes in the human genome are 'druggable' and only 5% are druggable and relevant to disease [START_REF] Hopkins | The druggable genome[END_REF]. The druggability of a target is currently assessed in a number of ways, this includes studying known inhibitors from the gene family and fragment/subset screening [START_REF] Hajduk | Predicting protein druggability[END_REF]. Fragment and subset screening have be deployed against targets to identify the ease of finding small molecule binders which can then indicate the likelihood of success by HTS and or random screening. The data from these studies is encouraging although some targets may not be suitable for such screening campaigns and also significant resource is required to carry out this work on a set of proposed targets in a timely fashion. Analyses of a target binding site can also be exploited where suitable crystal structures are available [START_REF] Burgoyne | Predicting protein interaction sites: binding hot-spots in protein-protein and protein-ligand interfaces[END_REF][START_REF] Fuller | Predicting druggable binding sites at the protein-protein interface[END_REF]. Such analyses can utilize information on the size, concavity and electrostatic nature of a pocket; one such recent report translates this information into a Maximal Affinity Model [START_REF] Cheng | Structure-based maximal affinity model predicts small-molecule druggability[END_REF]. This study highlights how a target with a well-defined pocket with a suitable balance of properties will score more highly than an open and feature-less pocket which can be observed in some protein-protein interactions. This approach is restricted to targets which have suitable protein crystal structures but encouragingly new and novel xray crystal structures continue to be published [START_REF] Jhoti | High-throughput structural proteomics using x-rays[END_REF]. Protein movement and flexibility is also an issue as some pockets are only fully formed when a ligand is bound [START_REF] Koshland | Application of a Theory of Enzyme Specificity to Protein Synthesis[END_REF]. Finally, analysis of the protein family or class can be used to estimate druggability. So for example if a proposed novel target is a kinase and a related family member has been shown to be tractable you might assume the druggability is likely to be comparable [START_REF] Whitty | Between a rock and a hard place?[END_REF]. Clearly if a novel protein family or target class is being assessed there may be little information in the literature to provide this guidance.

The study detailed in this paper uses a test-set of 950 diverse fragment-sized molecules [START_REF] Albert | An Integrated Approach to Fragment-Based Lead Generation:Philosophy, Strategy and Case Studies from AstraZeneca's Drug Discovery Programmes[END_REF] to allow an in silico druggability prediction through docking against a target binding site. This can be considered as the computational equivalent of a fragment screen, but where a specific pocket is targeted by each run. These fragments have been filtered using previously reported criteria and largely consistent with reported fragment library characteristics [START_REF] Albert | An Integrated Approach to Fragment-Based Lead Generation:Philosophy, Strategy and Case Studies from AstraZeneca's Drug Discovery Programmes[END_REF][START_REF] Congreve | Rule of Three' for fragment-based lead discovery?[END_REF].

Although docking scores do not consistently show a correlation with ligand binding affinities [START_REF] Kim | Assessment of programs for ligand binding affinity prediction[END_REF], the expectation is that a druggable binding site is likely to score fragments more highly when productive hydrogen bonding and lipophillic interactions with the protein can be identified. This measure of assessing the druggability of a binding site might be more accurately described as 'ligandability', where a protein of high ligandability is likely to bind fragments with a reasonable affinity. Identifying ligands which bind to a protein may not necessarily translate into finding a drug if the nature of the binding site does not allow the affinity of the lead to be increased whilst maintaining the required drug-like properties [14].

However, an indication that fragments can be identified for a target protein gives some confidence that the target might be tractable and or a tool compound may be identified for target validation work. Additionally, if this information could be obtained computationally it would allow a greater number of targets to be considered than using experimental approaches.

Materials and methods

Fragment set

A set of 950 diverse fragments were identified for this study. The distributions of ClogP (Version 4.3), molecular weight and rotatable bonds are shown for this fragment set below in Fig. 1.

<Figure 1>

The fragment set has a mean ClogP of 1.6 and the mean molecular weight was 188. The number of rotatable bonds in the set is centered on two, with a range between 0 and 6. The number of hydrogen bond acceptors and donors were also kept relatively low. Compounds with functionality not compatible with good fragment leads were also removed from the set.

The reasoning behind using a fragment set filtered to these criteria was to provide consistency to the druggability assessments which have been run using experimental approaches on similarly filtered fragment libraries [START_REF] Hajduk | Predicting protein druggability[END_REF].

Protein preparation

The publicly available protein structures used in this study were taken from the RSCB Protein Data Bank [START_REF] Berman | The Protein Data Bank[END_REF]. The proteins were prepared for docking and analysis using the Protein Preparation Wizard in Maestro [16]. Hydrogens were added, reflecting the likely protonation states of amino acids at pH=7.4. The hydrogen bonding environments of amino acids such as Asn and His were analyzed to ensure that the most likely conformation had been assigned [START_REF] Hooft | [END_REF]. Unless an interface between dimer/tetramer units was required for binding a single monomer unit was used for the docking. Where a suitable ligand/co-factor was present in the pocket, it was used to define the binding site for the docking. Where no ligand was present, SiteMap [START_REF] Halgren | New Method for Fast and Accurate Binding-site Identification and Analysis[END_REF] was used to identifying probable binding sites, the primary pocket was then manually defined using amino acid residues.

Protein-ligand docking

The likely protonation and tautomeric states of the 950 compound set was enumerated in Leatherface [START_REF] Lyne | Identification of Compounds with Nanomolar Binding Affinity for Checkpoint Kinase-1 Using Knowledge-Based Virtual Screening[END_REF]. This produced around 1150 distinct chemical structures. A 3D-structure of each molecule was produced in CORINA [20], which was then optimized using the MMFF94 Forcefield [START_REF] Halgren | A Merck Molecular Force Field: I-V[END_REF], and the Sheffield solvent model [22]. These structures were then used as input into the docking calculations. Glide was used for the protein-ligand docking [START_REF]GLIDE (Version 50207[END_REF].

Standard precision (SP) and extra precision (XP) docking protocols were run for comparison.

The highest scoring pose for each compound (which includes the various protonation/tautomeric states) was used to represent the score for that compound against the target.

Protein structures

The following tables show the x-ray crystal structures used for the docking studies. PDB codes of proteins from the RCSB protein data bank are provided [START_REF] Berman | The Protein Data Bank[END_REF].

<Table 1>

Results and discussion

Correlations of docking score against physiochemical properties

It has been demonstrated that docking scores can correlate with the molecular size of the compounds docked [START_REF] Kim | Assessment of programs for ligand binding affinity prediction[END_REF]. To ensure that this was not the case in this study the mean docking score of each fragment was calculated across all the protein targets studied. This value was then plotted against molecular weight and ClogP from the Standard (SP) and Extra Precision (XP) docking protocols. Fig. 2 shows that there is no significant correlation with the molecular weight or ClogP of the fragment and the mean docking score across the targets.

<Figure 2>

Interestingly, the XP protocol shows a stronger trend, albeit still a weak one, between the mean docking score of a fragment across the targets and Molecular Weight/ClogP (Fig. 2D). The RSquare=0.22 for XP plotted against Molecular weight in Fig. 2D can be compared with an RSquare=0.08 with SP in Fig. 2B. The correlation of the docking scores against MW and ClogP was also examined for individual targets but there were no clear trends. Any assessed targets, which do show a significant correlation, may indicate that higher affinity fragments could be identified outside the property ranges in the fragment set.

Comparison work with maximal affinity prediction model (MAP POD )

This section of the study compared a number of the systems published in the Maximal Affinity Model (MAP POD ) method to provide an assessment of how the two approaches compare with each other. The majority of studied targets classified as 'undruggable' and 'prodrug/transporter' were analyzed as these contained relatively small numbers of enzymes.

The 'druggable' targets were then sampled from to enable a reasonable assessment against this approach. For a number of these targets additional protein structures have been considered (see Table 1) than in the approach reported by Cheng et al. [START_REF] Cheng | Structure-based maximal affinity model predicts small-molecule druggability[END_REF] to maximize the available binding site information. For this assessment, the mean docking score of all 950 fragments docked to the target protein was used as an indicator of ligandability. Where multiple protein structures were used, the mean docking score across all the structures was taken. Note that a more negative docking score shows an improvement in the predicted affinity of the fragments. To assess how the ligandability prediction from the SP and XP docking protocols compare, they are plotted against each other in Fig. 3.

<Figure 3>

The analysis demonstrates that the SP and XP protocols correlate reasonably well (RSquare=0.89) and as XP is ~10x slower than SP it may not add additional significant value.

However, it may be prudent to run both protocols as some targets may vary in their predictions and as Glide can be run using parallel processing the additional computational resource is small. Additionally, as these docking algorithms develop it is a useful crosscheck to ensure that they give a consistent view with previous observations. The SP and XP protocols were then compared to the published MAP POD [START_REF] Jhoti | High-throughput structural proteomics using x-rays[END_REF] for a subset of the previously published targets (Table 1), the MAP POD was converted into a pKd for this comparison (Fig. 4).

<Figure 4>

The comparison demonstrates that there is some consistency in how you would classify these targets based on MAP POD and the fragment docking protocol. However, the RSquare values are relatively low, 0.50 for SP and 0.55 for XP. Importantly, the lower scoring targets (PTP1B, ICE-1, IMPDH and CATK) are highlighted as difficult targets in both approaches.

One most notable outlier between the two techniques is MDM2. This has been defined as a druggable target but it is clearly a challenging one due to the target binding site being a protein-protein interaction [START_REF] Vassilev | In vivo activation of the p53 pathway by small-molecule antagonists of MDM2[END_REF]. Aldose Reductase is an example in which the fragment docking protocol predicts the target to have a higher druggability than the Maximal Affinity Model.

The consistency of the ligandability assessment across different protein structures of the same target were also analyzed (Fig. 5). Where possible multiple protein structures were used to assess the ligandability of a target. The data shows that the choice of structure does impact on the ligandability score although in most cases it wouldn't significantly change your view of the target. The protein structures chosen for these assessments were chosen to maximize structural variation to give a more realistic view of the applicability of this method. However, it is clear that for some targets where a significant conformational change is required to form the binding site this approach will not successfully predict ligandability.

<Figure 5>

To highlight the impact of the crystal structure chosen, for P38 and EGFR, an example of an active and inactive crystal structure was used. This was a DFG-in and DFG-out structure for P38 (1GF2 and 1KV2 respectively) and a c-Helix in and c-Helix out structure (1N1M and 1XKK respectively) of EGFR. In both cases the inactive structures scored slightly higher, this appears to be at least partly due to the fragments having a choice of two sub-pockets to choose from. One of these regions is at the 'hinge' region and the other is in the 'selectivity pocket' of the kinase [START_REF] Buchanan | Protein structure: discovering selective protein kinase inhibitors[END_REF]. The inactive structures also allow fragments to be buried in the deep lipophillic selectivity pocket which is often scored favorably. All scores quoted below are from the SP protocol which was shown to track well with XP for a given target. In P38, the inactive structure had a docking score of -6.6 whereas the score was -6 for the active conformation. In EGFR, the inactive structure had a score of -6.6 compared to the active structure with a score of -5.9.

For the study of Enoyl Reductase [START_REF] Roujeinikova | Crystallographic analysis of triclosan bound to enoyl reductase[END_REF], three crystal structures were used with four docking protocols. The structures 1C14 and 1ISZ both have cofactor and an inhibitor bound, the inhibitor binds to the protein-cofactor complex. In these systems the inhibitor was removed and docking carried out against the protein-cofactor complex. Fragment docking scores with the SP protocol of -6.2 (1C14) and -6.5 (1ISZ) were observed for these two structures. An additional docking calculation was run on the 1C14 structure with the cofactor and inhibitor (Triclosan) removed to assess binding to the apo-enzyme, this gave a score of -6.1. The final docking calculation was performed on the 1DFI structure which only has the cofactor bound.

In this structure a loop in not visible which is observed to close over the active site when an inhibitor is bound (as in 1C14/1ISZ), resulting in a more open active site. When the docking protocol was carried out against 1DFI, with the cofactor present, you see a lower prediction (-5.3) of ligandability, which shows that identifying the most suitable target structure can be important. The PTP1B example is also interesting, five of the protocols examining the primary binding site [START_REF] Zhang | PTP1B as a drug target: recent developments in PTP1B inhibitor discovery[END_REF]. There is also a PTP1B structure of a ligand in an allosteric pocket [START_REF] Wiesmann | Allosteric inhibition of protein tyrosine phosphatase 1B[END_REF] (1T4J) which was targeted in one run, this was the most highly scored of the structures by a small margin (-5.7 against a Mean score across the PTP1B structures of -5.2).

Assessment of docking approach against target classifications

The following assessment of the druggability of a number of targets has been suggested based on analysis of known inhibitors [START_REF] Jhoti | High-throughput structural proteomics using x-rays[END_REF]. The key observation being the potency of the known inhibitors which is used to indicate the tractability of a target. Clearly for more novel targets, data on known inhibitors can be less abundant. The docking scores for the SP and XP protocols were compared against these defined categories of 'druggable', 'undruggable' and 'prodrug/transporter'. Again, the mean score of the fragments against the specified target was used to initially assess ligandability (Fig. 6).

<Figure 6>

The docking protocol assessment demonstrated a significant separation between the 'druggable' and 'undruggable' classifications. Using the SP protocol the p-Value=0.0052 and the XP protocol produced p-Value=0.0041 when comparing the separation of these two categories by the ligandability score. However, the 'prodrug/transporter' examples spanned the mid-range of the two categories so were more difficult to differentiate. One outlier from the docking analysis was MDM2, defined as 'druggable' in the target classification. Although inhibitors are known for this target the binding site is challenging protein-protein interface so it is reasonable to expect this target to have a poorer ligandability assessment by docking.

Although the 'prodrug/transporter' targets have had potent inhibitors successfully identified, it is expected that they will score less well by ligandability assessments using docking. The reasoning for this is that the active form of the inhibitor usually has a charged (or reactive) warhead which is masked in the prodrug to improve the properties of the compound [START_REF] Rautio | Prodrugs: design and clinical applications[END_REF]. As a number of highly charged or reactive functionalities will have been removed from fragment screening sets then tight binding fragments may not be identified. An alternative fragment set containing more highly charged/reactive functionalities may be required to further probe these targets. However, the fragment set used in this study remains a useful set to assess conventional ligandability and does contain a number of simple acids, bases and other charged groups.

The ligandability prediction from the mean score of all the docked fragments against a target was compared to the prediction using the mean score from just the top 10% ranked fragments against the target. The reasoning behind this being that some tractable targets may have a small number of tight binders which may not be reflected by the mean scores across the full fragment set. However this analysis did not show improved differentiation between the targets, the separation between the druggable and undruggable classes is actually slightly reduced (p-Value=0.0212 for SP protocol and p-Value=0.0944 for XP). The results from the SP and XP docking protocols are shown in Fig. 7.

<Figure 7>

An alternative way of expressing the ligandability data is to plot the docked scores of the ranked fragments of all the targets on a single plot. This gives a visual way of assessing if some targets have small numbers of fragments with high-predicted affinity or if the range of docking scores for a target has a flatter profile. It may be expected that a flatter profile shows a less interesting pocket than a profile which has a number of fragments predicted with a high affinity. The plot in Fig. 8 supports the early observation that COX-2 and Aldose Reductase are predicted to have a high ligandability from the docking studies. Thrombin and Acetylcholinesterase appear to have a number of highly scoring fragments; these targets are both classified as prodrug/transporter. This may reflect some differences in the difficulty of finding a lead (or fragment hit) compared to being able to modify that lead/fragment into an orally bioavailable drug. For example, it may be possible to identify hits against a certain target but the nature of the binding site may make it difficult to optimize the series whilst remaining in drug-like property space [START_REF] Leeson | The influence of drug-like concepts on decisionmaking in medicinal chemistry[END_REF].

<Figure 8>

To provide further information on how targets can be compared two additional scores were utilized. The 'Mean Score Target Adjusted' and the 'Mean Score Fragment Adjusted'. The Mean Score Targeted Adjusted is the ligandability score from the docking of the fragment set (using the mean score of the fragments) subtracted by the mean score of all the targets tested. So a negative number shows a target which is has a better predicted ligandability than the mean and vice versa. So clearly the rank ordering of the targets is not affected but it gives a benchmark for the comparison of new targets. As more targets are analyzed using this method then the mean score of all targets will change, especially in the initial stages, so this can be updated. The second score (Mean Score Fragment Adjusted) assesses how well each fragment scores to a single target compared to the mean score for that fragment across all targets. So ligandability of a target but this also failed to improve the separation between 'druggable' and 'undruggable' categories.

Conclusions

The docking method detailed provides an alternative method for assessing the druggability (or ligandability) of target proteins where crystal structures are available. When using the mean docking score for the fragment set against a target the results are largely consistent with the experimental data and approaches reported previously in the literature. Further validation work is to be performed on in-house targets which have already been targeted by lead generation approach in addition to novel enzymes currently under target selection. Where there are a number of targets which could be prosecuted, of a similar strength of disease linkage, then this information may be able to prioritize targets most likely to return lead-like compounds. This approach may also help to identify the most tractable pocket of a target and may guide the Lead Generation approach (i.e. Virtual/Directed Screen, HTS, FBLG or a combination of these). Other information will be used in this decision making process, including the knowledge of known ligands/substrates/co-factors of the target and any relevant information or experience around the target class. Clearly the limitation of this approach is the requirement for crystal structures to be are available, or where there may be a structure of a close homologue. There is also an additional issue around protein flexibility which suggests that examples which have an allosteric pocket or a significant degree of conformational change in the active site will not be accurately predicted. In addition, for some targets, the primary binding site may not be clearly located so a tool like SiteMap may be required to rank potential binding sites before they are subsequently analyzed. Often, once all these factors and additional information are considered, a high throughput measure to assess large numbers of targets may not be required. However, this approach has shown that a range of targets can be analyzed using this methodology and the more chemically tractable examples can be prioritized in many cases. This approach is to be further evaluated using fragment sets with a broader range of physicochemical properties, this may be particularly valuable for proteinprotein interfaces. For druggability assessment using these fragments, computational approaches may have additional value due to the potential issues around the experimental screening of more lipophillic fragments with poor solubility. Another extension of this approach may the integration of additional methods which may consider protein flexibility.

Further work around the binding mode and subsequent affinity predictions of fragments will also be required to increase the predictive power of this methodology.

Tables

Figure captions

4 .

 4 Hajduk PJ, Huth JR, Tse C (2005) Predicting protein drugability Drug Discovery Today 10:23-24:1675-1682

Fig. 1 Fig. 2 Fig. 3 Fig. 4 Fig. 5

 12345 Fig. 1Property profile of fragment set for 'ligandability' studies using docking

Fig. 6

 6 Fig. 6Comparison of docking scores against target classification using potency of known inhibitors[START_REF] Jhoti | High-throughput structural proteomics using x-rays[END_REF]. SP protocol shown in Fig.6Aand XP protocol in Fig.6B

Fig. 7

 7 Fig. 7Comparison of ligandability scores by docking against chemical tractability guided by knowledge of known inhibitors[START_REF] Jhoti | High-throughput structural proteomics using x-rays[END_REF]. The mean docking score of the top 10% of fragments against a target defined ligandability in this study. SP protocol shown in Fig.7Aand XP protocol in Fig.7B

Fig. 8 Fig. 9

 89 Fig. 8Profile of the docked fragment scores (SP protocol) for each target in the validation set

  Figure 1 Click here to download high resolution image

Table 1 X

 1 -ray crystal structures used in ligandability assessment by docking

	Protein Name	PDB Codes
	Enoyl Reductase	1C14, 1DFI, 1ISZ
	Aldose Reductase	1PWL, 1T41, 1PWM
	CDK2	1E1X, 1H07, 1H08, 1HCK, 1KE6, 1KE8, 1KE9
	Cyclo-oxygenase 2	4COX
	EGFR	1N1M, 1XKK
	MDM2	1RV1
	P38	1KV2, 2GFS
	Acetylcholinesterase	1O86
	IMPDH	1NF7
	Thrombin	1KTS
	CATK	1MEM, 1NLJ
	ICE-1	1BMQ
	PTP1B	1GFI, 1NNY, 1ONZ, 1PTY, 1Q1M, 1T4J

Acknowledgments

I would like to acknowledge the significant background work from a number of colleagues across AstraZeneca, which is described in this study. Additional thanks to Alex Breeze for introducing the term 'ligandability'.

this allows fragments to be identified with score highly against a certain target, but reduces the score for fragments, which score well in multiple targets. The intention being that the impact of the more lipophillic and featureless fragments, which may often act as frequent hitters, do not dominate the ligandability assessment. Therefore this score is compiled by subtracting the mean score of each fragment across all targets from the score against a specific target. The mean of this corrected score for fragments against a target is now used as a prediction of ligandability. These two scores are plotted in Fig. 9 for the assessed targets. SP and XP protocols are shown on the x-and y-axis for both.

Mean

<Figure 9>

The 'Mean Score Target Adjusted' allows a clearer comparison against how a studied target compares to the predicted average level of difficulty. Therefore allowing a benchmark against known targets which have previously been the subject of Lead Generation campaigns. The 'Mean Score Fragment Adjusted' doesn't significantly change the ranking ordering of most of the targets. This suggests that the affect of lipophillic frequent hitters in the assessment by docking is minimal as we aim to remove these from a fragment screening set. This way of scoring the targets could also be misleading if the number of examples from different target classes is not well balanced. This could lead compounds from over-represented target classes, such as kinases (CDK2, EGFR, P38 have been analyzed) to be artificially scored lower if similar fragments scored well between these targets. Two further methods of exploiting the docking scores were assessed. One method used a ligand efficiency score (docking score/heavy atoms) but this reduced the separation between the 'druggable' and 'undruggable' categories. Finally the most highly scored docked fragment was used to represent the