Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version) Tetsuya Sato✉∗ sato_tetsuya@iwate-pu.ac.jp Iwate Prefectural University Sugo, Takizawa, Iwate, Japan

arXiv:2610.25636v1 [cs.CR] 19 Oct 2026

Abstract

theorems allow decomposing the evaluation of the privacy guarantee of complex databases into their components’ ones. In the study of machine learning algorithms, privacypreserving learning algorithms with noise sampled from Gaussian distributions have attracted both industry and academia. To evaluate DP of such Gaussian mechanisms rigorously, variants of differential privacy based on Rényi divergence have become increasingly important. Abadi et al. introduced gradient descent algorithms with Gaussian noise and discussed their moment accountants, which can be captured with Rényi divergences [1]; Bun et al. introduced zero-concentrated differential privacy [20]; Mironov introduced Rényi differential privacy(RDP) [52]. There are many studies on DP and RDP mechanisms. In general, evaluating DP and RDP for databases is cumbersome. A few, even one-line, changes to database programs can break their differential privacy [49, Sec. 3]. In addition, RDP is much more complicated than DP, and evaluating it is not obvious, even understanding the proofs (For example, the original proof of Lemma 3.12 is complicated). Formal verification of RDP is more important and more complex than that of DP. For these reasons, formal verification of DP and RDP has been studied for over a decade. The first approach is based on Benton’s relational Hoare logic [17]. Starting from Barthe et al.’s relational program logic for reasoning about DP [14], many variants are studied [11–13], and extended to support RDP and more general divergences [15, 54, 55]. The second is reformulating DP as the sensitivity of functions between metric spaces. Based on this approach, Gaboardi et al. introduced a linear dependent type system for reasoning about differential privacy [23, 35]. It was applied for automated reasoning [60] and verification of integrity [53]. The third approach is formalizing DP and RDP directly in proof assistants. Tristan et al. proposed the library SampCert for verified implementations of DP and RDP using Lean [24, 61]. It contains the formalization of DP and RDP in the discrete setting and the discrete-Laplace and discrete-Gaussian mechanisms (see also [21]). Feng formalized functions of the OpenDP library [33] in Lean.

Differential privacy (DP) is a gold-standard definition of privacy designed to evaluate the privacy guarantee of databases. Rényi differential privacy (RDP) is an important variant of DP that gives tight evaluations of machine learning algorithms. These formulations are easy to understand, but evaluating privacy for actual databases is complicated. Even a small change in the database can break its privacy, and evaluations of DP and RDP themselves are complicated. In particular, RDP evaluations in recent studies have become much harder. Therefore, formal verification of them has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing Rényi differential privacy in a general setting. We first formalize RDP for continuous distributions. As a technical basis, we formalize several properties of convex functions and 𝑓 -divergences for nonnegative convex functions. We formalize basic properties of RDP, conversion laws from RDP to DP, the moment accountants in DP, and the Gaussian mechanism and its RDP. Finally, we discuss the stochastic gradient descent mechanism with Gaussian noise and formalize a rough evaluation of its RDP and DP. Keywords: Differential Privacy, 𝑓 -divergence, Rényi divergence, Isabelle/HOL, program verification

1

Introduction

Differential privacy(DP) is a de facto standard definition of privacy for databases with large amounts of individuals’ private data [26, 28]. It is already applied in the real world, such as iOS, Google Maps, and the United States census [5, 37, 38]. As notable strengths of DP, it guarantees robustness against any kind of statistical attack, and its composition Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. Conference acronym ’XX, Woodstock, NY © 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 978-1-4503-XXXX-X/2018/06 https://doi.org/XXXXXXX.XXXXXXX

Motivation. To our knowledge, RDP based on the continuous model of probabilistic programs has not been formalized yet. In this paper, we propose an Isabelle/HOL library for semantic-level formal verification of RDPs supporting 1

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

T. Sato

continuous probability distributions, including Gaussian distributions. First, the continuous setting is more general than the discrete one. Moreover, Isabelle/HOL’s discrete probability distributions are implemented as measures on discrete spaces. Second, even in the study of differential privacy in the discrete setting, we might need continuous models. For example, Mironov uses the continuous “ideal mechanism” to verify a secure floating-point implementation1 of the Laplace mechanism [51]. In addition, many pencil-and-paper proofs on RDP are written in the continuous setting. It is natural and convenient for us to implement them directly. Finally, the author thought that it must not be so hard to formalize it in the continuous setting. We later formalize that 𝑓 -divergences (hence RDP) in the continuous setting can be approximated with ones in the discrete setting.

𝑥 ∈ |𝑋 |. As an abuse of notation, we write R for the measurable spaces with the Borel algebra, the least 𝜎-algebra containing all open intervals. A measurable function 𝑓 : 𝑋 → 𝑌 is a function 𝑓 : |𝑋 | → |𝑌 | satisfying 𝑓 −1 (𝑆) ∈ Σ𝑋 for each 𝑆 ∈ Σ𝑋 . A measure 𝜇 on a measurable space 𝑋 is a function 𝜇 : Σ𝑋 → [0, ∞] having the countable additivity. A measure 𝜇 on 𝑋 is called a probability measure if 𝜇 (𝑋 ) = 1 respectively. We define the sum 𝜇1 + 𝜇 2 of two measures 𝜇1, 𝜇2 on 𝑋 by (𝜇 1 + 𝜇 2 ) (𝑆) = 𝜇1 (𝑆) + 𝜇 2 (𝑆), and the scaling 𝑎𝜇 of measure 𝜇 on 𝑋 with 0 ≤ 𝑎 by 𝑎𝜇 (𝑆) = 𝑎 𝜇¤ (𝑆). Giry monad. For a measurable space 𝑋 , we define the measurable space P (𝑋 ) as follows: |P (𝑋 )| is the set of probability measures on 𝑋 , and Σ P (𝑋 ) is the coarsest 𝜎-algebra making each evaluation mappling 𝜇 ↦→ 𝜇 (𝐴) (𝐴 ∈ Σ𝑋 ) a measurable function of type P (𝑋 ) → [0, ∞]. The constructor P forms a monad (P, return, >>=) called the Giry monad[36]. The unit return is defined by return(𝑥) = d𝑥 where d𝑥 is the Dirac measure on 𝑋 centered at 𝑥 ∈ 𝑋 2 . For any 𝑓 : 𝑋 → P (𝑌∫) and 𝜇 ∈ P (𝑋 ), (𝜇 >>=𝑓 ) ∈ P (𝑌 ) is defined by (𝜇 >>=𝑓 ) (𝐴) = 𝑓 (𝑥) (𝐴) 𝑑𝜇 (𝑥). We can interpret a probabilistic program as a measurable function 𝑐 : 𝑋 → P (𝑌 ). The sequential composition of 𝑐 : 𝑋 → P (𝑌 ) and 𝑐 ′ : 𝑌 → P (𝑍 ) can be interpreted by (𝜆𝑥 .𝑐 (𝑥) >>= 𝑐 ′ ).

Contribution. In this paper, we give an Isabelle/HOL library for Rényi differential privacy in the continuous setting, and give a formalization of the stochastic gradient descent (SGD) mechanism with Gaussian noise and Poisson subsampling. For a technical basis, we formalize 𝑓 -divergence, which is a class of statistical divergences generated by convex functions. We first give formal proofs of several basic properties of convex real functions, such as left and right derivatives and piecewise monotonicity. Then we formalize 𝑓 -divergence for nonnegative generator functions, and its basic properties such as postprocessing inequality and joint convexity. Furthermore, we formalize an approximation property of 𝑓 divergences called approximability, which is a technical basis of the composition theorem of Rényi differential privacy in the general setting. We then formalize basic properties of RDP, conversion laws from RDP to DP, the moment accountants in DP, and the Gaussian mechanism and its RDP. Finally, we formalize a rough evaluation of RDP and DP of Gaussian SGD.

2

Do notation. For better readability, we introduce the syntactic sugars called do notation: {𝑥 ← 𝜇; 𝑓 (𝑥)} = (𝜇 >>= 𝑓 ) {𝑥 ← 𝜇 1 ; 𝑦 ← 𝜇2 (𝑥); ...} = {𝑥 ← 𝜇1 ; {𝑦 ← 𝜇2 (𝑥); ...}} We notice that the Giry monad is commutative. Using do notation, the commutativity is written as follows: for 𝜇1 ∈ P (𝑋 ), 𝜇 2 ∈ P (𝑌 ), and measurable 𝑓 : 𝑋 × 𝑌 → P (𝑍 ), {𝑥 ← 𝜇1 ; 𝑦 ← 𝜇2 ; 𝑓 (𝑥, 𝑦)} = {𝑦 ← 𝜇2 ; 𝑥 ← 𝜇1 ; 𝑓 (𝑥, 𝑦)}. 2.2

The Isabelle/HOL’s standard library contains the formalizations of measure theory and the Giry monad. The type ′a measure is the type of measure space, that is, the triple (|𝑋 |, Σ𝑋 , 𝜇) consisting of a measurable space (|𝑋 |, Σ𝑋 ) and a measure 𝜇 on it. The standard library provides the projections of these components:

Preliminaries

Throughout this paper, we write R and N for the sets of real numbers and natural numbers, respectively. We write (0, ∞), [0, ∞), and [0, ∞] for the sets of positive reals, and nonnegative reals and nonnegative extended reals respectively. 2.1

Measure theory in Isabelle/HOL

space :: ′a measure ⇒ ′a set sets :: ′a measure ⇒ ′a set set

Measure theory

emeasure :: ′a measure ⇒ ′a set ⇒ ennreal

A measurable space 𝑋 = (|𝑋 |, Σ𝑋 ) is a set |𝑋 | with a 𝜎-algebra Σ𝑋 over |𝑋 | which is a nonempty family of subsets of |𝑋 | closed under countable unions and complelemts. For a measurable space 𝑋 , we write |𝑋 | and Σ𝑋 for the underlying set and 𝜎-algebra, respectively. For simplicity, we often write just 𝑋 for the underlying set |𝑋 |. For example, 𝑥 ∈ 𝑋 means

Here, ennreal is the type for [0, ∞], and ′a set is the type of all subsets with elements of type ′a. The type ′a measure is used for both measurable spaces and measures. We sometimes need to distinguish them. For example, borel::real measure is used for the Borel space R, and lborel::real measure is for the Lebesgue measure3 on R. 2 It is defined by d (𝐴) = 1 if 𝑥 ∈ 𝑆 and d (𝐴) = 0 otherwise 𝑥 𝑥 3 Precisely, the Lebesgue measure is completion lborel.

1 It is different from discrete-Laplace mechanism given in [21]

2

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

The set of measurable functions from X to Y is given by X →𝑀 Y, hence measurability of f is denoted by f ∈ X →𝑀 Y. For a measure M :: ′a measure and f ∈ M →𝑀 (borel::real measure) 4 , the integration of f with ∫ ∫ measure M (over a set A) is denoted by x. f x 𝜕M (resp. x∈A. f x 𝜕M). Isabelle/HOL’s standard library contains the formalization of the Giry monad and its commutativity. The components in (P, return, >>=) are provided as the following constants.

A key feature of DP is the composition theorems, which are a compatibility condition for compositions. For example, we have the following proposition theorem. Proposition 3.2 (Adaptive composition [30, Thm. B.1]). If 𝑐 1 : 𝑋 → P (𝑌 ) is (𝜀 1, 𝛿 1 )-DP and 𝑐 2 : 𝑋 × 𝑌 → P (𝑍 ) satisfies that for any 𝑦 ∈ 𝑌 , (𝜆𝑥 .𝑐 2 (𝑥, 𝑦)) : 𝑋 → P (𝑌 ) is (𝜀 2, 𝛿 2 )-DP. then (𝜆𝑥 .{𝑦 ← 𝑐 1 (𝑥); 𝑐 2 (𝑥, 𝑦)}) is (𝜀 1 + 𝜀 2, 𝛿 1 + 𝛿 2 )-DP. Divergence for DP. The indistinguishability in DP can be reformulated equvalently by a statistical divergence, which is a “distance” between probability distributions. We recall DP𝑋𝜀 : |P (𝑋 )| × |P (𝑋 )| → [0, ∞) showed in [15, 54, 55]:

prob_algebra :: ′a measure ⇒ ′a measure measure return :: ′a measure ⇒ ′a ⇒ ′a measure >>= :: ′a measure ⇒ ( ′a ⇒ ′ b measure ) ⇒ ′b measure

3

DP𝑋𝜀 (𝜇 1, 𝜇2 ) = max (𝜇 1 (𝑆) − exp(𝜀)𝜇 2 (𝑆)).

Differential Privacy

𝑆 ∈Σ𝑋

Differential privacy(DP) is a statistical definition of privacy introduced by Dwork et al.[26, 28]. Later, Mironov introduced Rényi differential privacy(RDP) [52] in the line of studies about moment accountants in DP to make tight privacy guarantees for Gaussian mechanisms [1, 20]. In this work, we use both kinds of differential privacy. In this section, we give a crash course on differential privacy and the prior study for the formalization of DP in Isabelle/HOL [56, 57]. A basic approach to differential privacy is to prevent distinguishing between a dataset and the dataset plus an individual’s data entry 𝑥. Thus, differential privacy is based on the adjacency of datasets. For a basic example, 𝐷 1 and 𝐷 2 are adjacent if 𝐷 2 is made by insertion of an entry 𝑥 to 𝐷 1 (i.e. 𝐷 2 = 𝐷 1 ∪ {𝑥 }). For another example, two datasets 𝐷 1 and 𝐷 2 are adjacent if they are different only in one record, namely, their Hamming distance is 1 (i.e. 𝑑𝐻 (𝐷 1, 𝐷 2 ) = 1). Moreover, for datasets of user-related events, we can discuss two kinds of differential privacy: user-level and event-level (see [29, Sec. 1]). Generally speaking, adjacency can be captured by an adjacency relation 𝑅adj between datasets. Differential privacy assumes queries with noise-adding anonymization and is designed to measure the indistinguishability of noisy outputs from two adjacent datasets. Hence, we formulate a noisy database mechanism as a measurable function 𝑐 : 𝑋 → P (𝑌 ) where 𝑋 and 𝑌 are the domains of inputs and outputs, respectively. We now give the standard definition of differential privacy (cf. [27]).

We then have that 𝑐 : 𝑋 → P (𝑌 ) is (𝜀, 𝛿)-DP if and only if DP𝑋𝜀 (𝑐 (𝐷 1 ), 𝑐 (𝐷 2 )) ≤ 𝛿 holds for all (𝐷 1, 𝐷 2 ) ∈ 𝑅adj . The above composition theorem and the stability for postprocesses are derived from the below composability: Proposition 3.3 (Composability). Let 𝜇1, 𝜇2 ∈ P (𝑋 ) and 𝑐 1, 𝑐 2 : 𝑋 → P (𝑌 ). If DP𝑋𝜀1 (𝜇 1, 𝜇2 ) ≤ 𝛿 1 and DP𝑌𝜀2 (𝑐 1 (𝑥), 𝑐 2 (𝑥)) ≤ 𝛿 2 for any 𝑥 ∈ 𝑋 then DP𝑌𝜀1 +𝜀2 (𝜇1 >>= 𝑐 1, 𝜇2 >>= 𝑐 2 ) ≤ 𝛿 1 + 𝛿 2 . 3.1

Rényi differential privacy

Noise-adding mechanisms with Gaussian distributions (called Gaussian mechanism) are an essential component of privacypreserving data analysis. However, we cannot avoid errors in its DP evaluations. The Gaussian distribution N (𝑚, 𝜎 2 ) with average 𝑚 and variance 𝜎 2 is given by the following probability density function   (𝑥 − 𝑚) 2 1 exp − . 𝑓 N (𝑚,𝜎 2 ) (𝑥) = √ 2𝜎 2 2𝜋𝜎 2 The noise adding mechanism with 𝑚𝑎𝑡ℎ𝑐𝑎𝑙𝑁 (0, 𝜎 2 ) can be written by (𝜆𝑥 .{𝑧 ← N (0, 𝜎 2 ); return(𝑥 + 𝑧)}). By the shift property of Gaussian distributions, it is (𝜆𝑥 .N (𝑥, 𝜎 2 )). For 𝑥 ≠ 𝑦, we evaluate the indistinguishability of N (𝑥, 𝜎 2 ) and N (𝑦, 𝜎 2 ) for (𝜀, 𝛿)-DP. If 𝛿 = 0 then 𝜀 must be ∞, where the ratio between 𝑓 N (𝑦,𝜎 2 ) (𝑧) and 𝑓 N (𝑥,𝜎 2 ) (𝑧) is unbounded. Rényi differential privacy(RDP) is a variant of differential privacy introduced by Mironov [52]. Replacing the divergence DP𝜀 for DP with the Rényi divergence (of order 𝛼) defined as follows, we obtain RDP.  ∫  𝑝 1 (𝑥) 𝛼 1 𝛼 𝐷𝑋 (𝜇1, 𝜇2 ) = log 𝑝 2 (𝑥) 𝑑𝜋 (𝑥) (1 < 𝛼). 𝛼 −1 𝑝 2 (𝑥)

Definition 3.1 (Differential Privacy(DP) [30, Def. 2.4]). Let 𝑅adj ⊆ 𝑋 ×𝑋 be an adjacency relation, and let 0 ≤ 𝜀 and 0 ≤ 𝛿. A database mechanism 𝑐 : 𝑋 → P (𝑌 ) is (𝜀, 𝛿)-differentially private(DP) if for two adjacent datasets (𝐷 1, 𝐷 2 ) ∈ 𝑅adj ,

Here, 𝑝 1 (𝑥) and 𝑝 2 (𝑥) are density functions of 𝜇1 and 𝜇2 with respect to a base measure 𝜋.

∀𝑆 ∈ Σ𝑌 . Pr[𝑆 ∈ 𝑐 (𝐷 1 )] ≤ exp(𝜀) Pr[𝑆 ∈ 𝑐 (𝐷 2 )] + 𝛿. Intuitively, 𝜀 is an upper bound of probability ratio between 𝑐 (𝐷 1 ) and 𝑐 (𝐷 2 ), and 𝛿 is an error. When 𝜀 and 𝛿 are small, 𝑐 (𝐷 1 ) and 𝑐 (𝐷 2 ) are hard to distinguish5 .

Definition 3.4 (Rényi Differential privacy(RDP) [52, Def. 4]). Let 𝑅adj ⊆ 𝑋 × 𝑋 be an adjacency relation, and let 1 < 𝛼 and 0 ≤ 𝜌. A database mechanism 𝑐 : 𝑋 → P (𝑌 ) is (𝛼, 𝜌)-Rényi differentially private(RDP) if 𝐷𝑋𝛼 (𝑐 (𝐷 1 ), 𝑐 (𝐷 2 )) holds for any adjacent datasets (𝐷 1, 𝐷 2 ) ∈ 𝑅adj .

4 Here, M is also used for the underlying measurable space on M. 5 In particular, if (𝜀, 𝛿 ) = (0, 0) then 𝑐 (𝐷 ) = 𝑐 (𝐷 ). 1 2

3

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

T. Sato

Rényi divergence satisfies 𝐷𝑋𝛼 (𝜇, 𝜇) = 0 for all 𝜇 ∈ P (𝑋 ), and has the composability.

This conversion law is the best one we know, but the proof is much harder than the previous two lemmas. We formalize all these conversion laws by using the privacy regions for DP and RDP [10, 44] and reducing the conversion of divergences to the inclusion of privacy regions. We see the details later.

Lemma 3.5 (Composability [54, Thm. 7]). Let 𝜇1, 𝜇2 ∈ P (𝑋 ) and 𝑐 1, 𝑐 2 : 𝑋 → P (𝑌 ). If 𝐷𝑋𝛼 (𝜇 1, 𝜇2 ) ≤ 𝜌 1 and for any 𝑥 ∈ 𝑋 , 𝐷𝑌𝛼 (𝑐 1 (𝑥), 𝑐 2 (𝑥)) ≤ 𝜌 2 then 𝐷𝑌𝛼 (𝜇 1 >>= 𝑐 1, 𝜇2 >>= 𝑐 2 ) ≤ 𝜌 1 + 𝜌 2 .

Moment accountants in DP. Rényi divergence 𝐷 𝛼 (𝜇1, 𝜇2 ) 𝑝 (𝑥 ) of order 𝛼 gives 𝛼-moment of random variable 𝑝 12 (𝑥 ) (𝑥 ∼ 𝜇 2 ), which is privacy loss random variable when 𝜇𝑖 = 𝑐 (𝐷𝑖 ). Roughly speaking, Rényi divergence can access higher-order moments of privacy loss random variables. Using this, we obtain a tighter DP bound than just applying conversion laws (for fixed 𝛼) or advanced composition theorems in DP.

Postprocessing inequality 𝐷𝑌𝛼 (𝜇 1 >>=𝑐, 𝜇 2 >>=𝑐) ≤ 𝐷𝑋𝛼 (𝜇 1, 𝜇2 ) is just an application of this lemma for 𝑐 1 = 𝑐 2 and 𝜌 2 = 0. The Rényi divergence of Gaussian distributions is simple. Lemma 3.6 ([52, Prop. 7], modified). For 1 < 𝛼 and 0 < 𝜎, 𝛼 (𝑥 − 𝑦) 2 . 2𝜎 2 Basic properties of RDP. From these facts, we obtain basic properties for RDP. We have the composition theorem and the stability for postprocessing. 𝐷𝑋𝛼 (N (𝑥, 𝜎 2 ), N (𝑦, 𝜎 2 )) =

Lemma 3.13 ([2, Sec 3.2],[6, Sec.√︁IV]). Assume 0 < 𝛿 < 1, 0 < 𝜀, and 𝐾 ≤ 𝜀 + 2 log(1/𝛿) − 2 (𝜀 + log(1/𝛿)) log(1/𝛿). If 𝑐 is (𝛼, 𝛼𝐾)-RDP for any 1 < 𝛼 then 𝑐 is (𝜀, 𝛿)-DP.

Proposition 3.7 (Composition theorem [52, Prop. 1]). If 𝑐 1 : 𝑋 → P (𝑌 ) is (𝛼, 𝜌 1 )-RDP and 𝑐 2 : 𝑋 ×𝑌 → P (𝑍 ) satisfies that for any 𝑦 ∈ 𝑌 , (𝜆𝑥 .𝑐 2 (𝑥, 𝑦)) : 𝑋 → P (𝑌 ) is (𝛼, 𝜌 2 )-RDP. then (𝜆𝑥 .{𝑦 ← 𝑐 1 (𝑥); 𝑐 2 (𝑥, 𝑦)}) is (𝛼, 𝜌 1 + 𝜌 2 )-RDP.

We formalize this lemma using Lemma 3.10. A better (and more challenging to mechanize) bound is given in [6, Sec. IV] using Lemma 3.12. Tracking the proof of Lemma 3.13. It ˆ 𝛼𝐾)-RDP ˆ is enough to see (𝛼, for √︁ log(1/𝛿) + (𝜀 + log(1/𝛿)) log(1/𝛿) 𝛼ˆ = 1 + . 𝜀

Proposition 3.8 (Postprocessing). If 𝑐 : 𝑋 → P (𝑌 ) is (𝛼, 𝜌)RDP then for any 𝑔 : 𝑌 → P (𝑍 ), the composition (𝜆𝑥 .{𝑦 ← 𝑐 (𝑥); 𝑔(𝑦)}) : 𝑋 → P (𝑍 ) is (𝛼, 𝜌)-RDP.

Lemma 3.14 (Explicit ver.). Assume that 𝜀, 𝛿, 𝐾 satisfy the ˆ 𝛼𝐾)-RDP ˆ condition in Lemma 3.13. If 𝑐 is (𝛼, then 𝑐 is (𝜀, 𝛿)-DP.

We also state the RDP of Gaussian mechanism. Lemma 3.9. Let 1 < 𝛼 and 0 < 𝜎, and 𝑓 : 𝑋 → R. The 2 Gaussian mechanism (𝜆𝑥 .N (𝑥, 𝜎 2 )) : R → P (R) is (𝛼, 𝛼𝑟 )2𝜎 2 RDP, where 𝑟 = sup{∥ 𝑓 (𝐷 1 ) − 𝑓 (𝐷 2 ) ∥ 2 | (𝐷 1, 𝐷 2 ) ∈ 𝑅adj }.

4

This can be extended easily to multi-dimensional Gaussian mechanism (𝜆𝑥®.N (𝑥, ® 𝜎 2 𝐼 )) : R𝑛 → P (R𝑛 ). It is 𝑛 applications of 1-dimensional Gaussian mechanism 𝑥𝑖 ↦→ N (𝑥𝑖 , 𝜎 2 ). Conversions from RDP to DP. We can convert RDP to DP, comparing the divergences DP𝑋𝜀 (𝜇1, 𝜇2 ) and 𝐷𝑋𝛼 (𝜇 1, 𝜇2 ). We give formal proofs of the following conversion laws.

Density functions of two measures. In general, in theories on DP and RDP, we often need density functions. For example, as we have seen, Rényi divergence requires a base measure 𝜋 and density functions 𝑝 1, 𝑝 2 of 𝜇1, 𝜇2 ∈ P (𝑋 ) with respect to 𝜋. They can be formulated as Radon-Nikodým derivatives 𝑑𝜇 1 /𝑑𝜋 and 𝑑𝜇2 /𝑑𝜋 where 𝜋 is a sigma-finite measure dominating6 both the 𝜇1 and 𝜇2 . We remark that the sum 𝜋 = 𝜇 1 + 𝜇 2 is always such a base measure. The library Differetial_Privacy contains the locales for density functions of two measures, and several propreties of them. It supports density functions between two probability measures and finite measures, but not subprobability measures. To formalize Rényi divergence instead of DP, we need to overhaul this part (thus we enclose the modified copy of Differetial_Privacy in the supplementary material).

Lemma 3.10 ([52,  Prop. 3]).  Assume that 𝑐 is (𝛼, 𝜌)-RDP. For log 𝛿 0 < 𝛿 < 1, 𝑐 is 𝜌 − 𝛼 −1 , 𝛿 -DP. Lemma 3.11  ([10, Thm. 20], fixed in
[6]). If 𝑐 is (𝛼, 𝜌)-RDP log 𝛿+log 𝛼 then it is (𝜌 − 𝛼 −1 + log 𝛼𝛼−1 , 𝛿 -DP for 0 < 𝛿 < 1. +

Here, (. . .)+ is the nonnegative part max(0, . . .). The term
log 𝛿+log 𝛼 𝜌 − 𝛼 −1 + log 𝛼𝛼−1 can be negative, but in that case, we can set 𝜀 = 0. This conversion is known as a standard one. Lemma 3.12 ([6, Lemma 1]). Assume that 𝑐 is (𝛼, 𝜌)-RDP. For 0 < 𝛿 < 1, 𝑐 is (𝜀, 𝛿)-DP where 𝜀 is defined by  (𝜌 + log(1 1 < 𝛼𝛿    − 𝛿))+ 
   log 𝛿+log 𝛼 𝛼 −1 𝜀= © (𝜌 −  𝛼 −1 + log 𝛼  + ,ª  min ­ 1 ® 𝛼𝛿 ≤ 1  exp(𝜌 (𝛼 −1) ) −1   log + 1 𝛼𝛿  « 𝛼 −1 ¬

DP in Isabelle/HOL

This work rely highly on the formalization of DP in the continuous setting [56, 57]. The library Differetial_Privacy contains not only the formalization of DP, but also important constructions for the formalization of statistical divergences. In this work, we use the following three constructions:

6 Let 𝜇 and 𝜇 be (sigma-)finite measures on 𝑋 . We say that 𝜈 dominates

𝜇 , or 𝜇 is absolutely continuous with respect to 𝜈 (written 𝜇 ≪ 𝜈) if ∀𝑆 ∈ Σ𝑋 .𝜈 (𝑆 ) = 0 =⇒ 𝜇 (𝑆 ) = 0. 4

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

Measurable spaces of lists. The theory List_Space of Differetial_Privacy contains the construction of measurable spaces of finite lists and measurability proofs of list operations. This library contains the constructor

Here, Rényi divergence can be reformulated by 𝐷𝑋𝛼 (𝜇 1, 𝜇2 ) =

(1 < 𝛼)

where the generator function is given by 𝑓 𝛼 (𝑡) = 𝑡 𝛼 . In this paper, we formalize 𝑓 -divergences for nonnegative generator functions (∀𝑡 ∈ (0, ∞).0 ≤ 𝑓 (𝑡)). It is enough to formalize Rényi divergences since 𝑓 (𝑡) = 𝑡 𝛼 (1 < 𝛼) is nonnegative. It is easier to mechanize; we can skip partitioning the positive and negative parts in the integral in Δ𝑋𝑓 (𝜇1, 𝜇2 ). For probability measures, without loss of generality, we then assume that the generator function is nonnegative. For two convex functions 𝑓 , 𝑔 : (0, ∞) → R, if ∀𝑡 ∈ (0, ∞).𝑔(𝑡) = 𝑓 (𝑡) + 𝑐 (𝑡 − 1) then Δ𝑋𝑓 (𝜇 1, 𝜇2 ) = Δ𝑔𝑋 (𝜇1, 𝜇2 ). For a general convex 𝑓 , we can choose 𝑐 such that 𝑔(𝑡) = 𝑓 (𝑡) + 𝑐 (𝑡 − 1) is nonnegative. Therefore, if needed, we can extend basic results of 𝑓 -divergences for nonnegative generator functions to general ones. In this section, we formalize 𝑓 -divergences for nonnegative generator functions as follows: we first formalize basic results for generator functions. Then, we formalize 𝑓 divergences for nonnegative generator functions and give formal proofs of their basic properties and special properties of 𝑓 -divergences, which we call continuity and approximability, used in the composability of Rényi divergence.

listM :: ′a measure ⇒ ′a list measure making a measurable space M to the one listM M of lists over M. For example, the space R∗ of lists of real numbers is denoted by listM borel. This library contains measurability of list operations. For example, measurability foldl is, lemma measurable-foldl [measurable]: Ë assumes [measurable]:(𝜆(x,y). F yË x) ∈ (M 𝑀 N →𝑀 N ) shows (𝜆 (T,xs). foldl F T xs) ∈ N 𝑀 (listM M) →𝑀 N

Furthermore, measurability of Cons, map, (@), foldr, foldl, fold, take, drop and nth are provided in similar ways. Formalization of DP. The library, of course, contains formalizations of DP in the continuous setting. Moreover, it first gives the formalization of divergence DP𝑋𝜀 (𝜇, 𝜈) and its basic properties, and then formalizes DP. definition DP-divergence where DP-divergence M N 𝜀 = Sup {ereal(measure M A − (exp 𝜀) ∗ measure N A) | A:: ′a set. A ∈ (sets M)} definition DP-inequality where DP-inequality M N 𝜀 𝛿 ≡ (∀ A ∈ sets M. measure M A ≤ (exp 𝜀) ∗ measure N A + 𝛿) definition differential-privacy where differential-privacy M adj 𝜀 𝛿 ≡ ∀ (d1,d2)∈adj. DP-inequality (M d1) (M d2) 𝜀 𝛿 ∧ DP-inequality (M d2) (M d1) 𝜀 𝛿

5.1

Convex real functions

We formalize generator functions 𝑓 : (0, ∞) → R and their basic results. For example, such 𝑓 is piecewisely monotone:

Here, differential-privacy M adj 𝜀 𝛿 means that a mechanism M is (𝜀,𝛿)-DP with respect to the adjacency relation adj. In the library, formalizations of the Laplace mechanism and Report-Noisy-Max mechanism are given. However, the Gaussian mechanism and RDP in the continuous setting are not formalized yet. In this paper, we propose a library for the Gaussian mechanism and RDP, and give a formalization of the gradient descent mechanism with subsampling.

5

1 𝑓𝛼 log Δ𝑋 (𝜇1, 𝜇2 ) 𝛼 −1

1. 𝑓 is monotone increasing on (0, ∞), 2. 𝑓 is monotone decreasing on (0, ∞), or 3. There is 𝑧 ∈ (0, ∞) such that 𝑓 is monotone decreasing on (0, 𝑧] and 𝑓 is monotone increasing on [𝑧, ∞). We need it to formalize the well-definedness of the extension 𝑓 (0) = lim𝑡 →+0 𝑓 (𝑡). If 𝑓 were two-sided differentiable everywhere on (0, ∞), the proof of piecewise monotonicity would be easy, but it is not in general. Thus, to prove it, we use left and right derivatives instead of two-sided derivatives. We formalize the existence of left and right derivatives of a convex function 𝑓 : 𝐼 → R (𝐼 is a convex open subset of R), their monotonicity, and inequalities about them. For 𝑓 (𝑡 ) −𝑓 (𝑣) 𝑓 (𝑤 ) −𝑓 (𝑣) example, 𝐷 𝐿 𝑓 (𝑣) = lim𝑡 →𝑣+0 𝑡 −𝑣 ≤ (𝑣 < 𝑤): 𝑤−𝑣

𝑓 -divergence in Isabelle/HOL

We formalize a class of divergences called 𝑓 -divergences [22, 46] as a technical basis of Rényi divergence. For a given convex function 𝑓 : (0, ∞) → R, called a generator function, we define the Δ 𝑓 as follows: for any measurable space 𝑋 and probability measures 𝜇 1, 𝜇2 ∈ P (𝑋 ),   ∫ 𝑝 1 (𝑥) Δ𝑋𝑓 (𝜇1, 𝜇2 ) = 𝑓 𝑝 2 (𝑥) 𝑑𝜋 (𝑥). 𝑝 2 (𝑥)

abbreviation slope-of f a b ≡ (f a − f b) / (a − b) lemma convex-right-deriv-slope-upper: fixes f :: real ⇒ real assumes convex-on I f and v ∈ I and w ∈ I and (f has-field-derivative Dv) (at-right v) and v < w shows Dv ≤ slope-of f w v

Here, 𝑝 1 (𝑥) and 𝑝 2 (𝑥) are density functions of 𝜇1 and 𝜇2 with respect to a base measure 𝜋. The divergence Δ𝑋𝑓 (𝜇1, 𝜇2 ) may not be integrable (it can be ∞). Technically speaking, the generator function 𝑓 inside the integtal is extended by 𝑓 (0) = lim𝑡 →+0 𝑓 (𝑡) and 0𝑓 (𝑎/0) = 𝑎𝑓 ∗ (0) where 𝑓 ∗ (𝑡) = 𝑡 𝑓 (1/𝑡) is the convex conjugate of 𝑓 .

We then formalize the piecewise motonicity. theorem convex-piecewise-monotone: fixes f :: real ⇒ real assumes convex-on I f and open I shows (∃ v ∈ I . antimono-on (I ∩ {..v}) f ∧ mono-on (I ∩ {v..}) f ) ∨ (mono-on I f ) ∨ (antimono-on I f ) 5

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

T. Sato

definition extend-frac-F :: (real ⇒ real) ⇒ (real ⇒ real ⇒ ereal) where extend-frac-F f a b = (if a < 0 then undefined else if b < 0 then undefined else if a = 0 then b ∗ (extend-F f 0) else if b = 0 then a ∗ (extend-F (conj-F f ) 0) else b ∗ f (a/b))

From these lemmas and the Froda theorem (formalized as mono_on_ctble_discont_open in the standard library), every convex real function is differentiable almost everywhere. lemma convex-differentialble-AE: fixes f :: real ⇒ real assumes cvxf :convex-on I f and open I shows AE x ∈ I in lborel. f differentiable (at x)

For 𝑎, 𝑏 ∉ [0, ∞) extend-frac-F a b returns undefined.

Countable version of Jensen inequality. We also prove a countable version of Jensen inequality: The finite version (𝐶: finite) is already formalized in isabelle/HOL’s standard library. We want to support countable infinite 𝐶.

Extension of countable Jensen inequality. We formalize a variant of Jensen inequality Í  ∑︁   Í 𝑥𝑖 𝑖 ∈𝐶 𝑥𝑖 ( 𝑖 ∈𝐶 𝑎𝑖 ) 𝑓 Í (∀𝑖 ∈ 𝐶.0 ≤ 𝑎𝑖 , 𝑥𝑖 ) ≤ 𝑎𝑖 𝑓 𝑎𝑖 𝑖 ∈𝐶 𝑎𝑖 𝑖 ∈𝐶

lemma convex-on-infsum-real: fixes a :: ′a ⇒ real and y :: ′a ⇒ real and f :: real ⇒ real assumes convex-on I f and open I and (a has-sum 1) C Í and (𝜆i. a i ∗ y i) summable-on C ( ∞ i∈C. a i ∗ y i) ∈ I and (𝜆i. a i ∗ f (y i)) summable-on C and ∀ i∈C. a i ≥ 0 and ∀ i∈C. y i ∈ I Í Í shows f ( ∞ i∈C. a i ∗ y i) ≤ ( ∞ i∈C. a i ∗f (y i))

using the extension extend-frac-F. lemma extend-frac-F-convex-on-frac-infsum: fixes a :: ′a ⇒ real and y :: ′a ⇒ real assumes gf : generator-F f and suma: a summable-on C and sumy: y summable-on C and ∀ i∈C. a i ≥ 0 and ∀ i∈C. y i ≥ 0 Í shows extend-frac-F f (infsum y C) (infsum a C) ≤ ( ∞ i∈C. extend-frac-F f (y i) (a i))

Í Here, we choose suminf ( ∞ ) for countable sums instead of Í infsum, because suminf supports any type of sum 𝑖 ∈𝐶 𝑎𝑖 though it needs the convergence (written summable), while infsum supports only sums indexed by natural numbers. 5.2

We use this lemma to formalize approximations of 𝑓 -divergences, which are important for formalizing Rényi divergence. The formal proof is done by partitioning 𝐶 into {𝑖 ∈ 𝐶 | 𝑎𝑖 = 0} and {𝑖 ∈ 𝐶 | 0 < 𝑎𝑖 }, and extending the convexity of 𝑓 : (0, ∞) → R to ones of 𝑓¯ and 𝐹 𝑓 .

Basics of generator function and extension

We formalize a generator function for 𝑓 -divergences: definition generator-F :: (real ⇒ real) ⇒ bool where generator-F f ←→ (convex-on {0<..} f )

5.3

Thanks to the piecewise monotonicity, the extension of the generator function by 𝑓 (0) = lim𝑡 →+0 𝑓 (𝑡) is well-defined.

Basics of 𝑓 -divergence

We now formalize the 𝑓 -divergence Δ 𝑓 for a nonnegative generator function 𝑓 . We use the extension 𝐹 𝑓 instead of 𝑓 . ∫ 𝑓 Δ𝑋 (𝜇 1, 𝜇2 ) = 𝐹 𝑓 𝑝 1 (𝑥) 𝑝 2 (𝑥) 𝑑𝜋 (𝑥).

lemma gf-converge-to-0: assumes generator-F f shows ∃ f0:: ereal. ((ereal o f ) −−−→ f0) (at-right 0) ∧ −∞ < f0

We now define the extension 𝑓¯ : [0, ∞) → [−∞, ∞] of 𝑓 by 𝑓¯(𝑡) = 𝑓 (𝑡) for 0 < 𝑡 and 𝑓¯(0) = lim𝑡 →+0 𝑓 (𝑡), and formalize it as follows:

definition f-div-pos∫ where f-div-pos f L M N = + x. e2ennreal ((extend-frac-F f ) (real-RN-deriv L M x) (real-RN-deriv L N x)) 𝜕L

definition extend-F :: (real ⇒ real) ⇒ (real ⇒ ereal) where extend-F f x = (if x < 0 then 0 else if x = 0 then SOME f0. ((ereal o f ) −−−→ f0) (at-right 0) else ereal (f x))

Here, L, M, N are 𝜋, 𝜇1 and 𝜇2 respectively. We use extend-frac-F to formalize 𝐹 𝑓 . real-RN-deriv is construction of density functions (real-valued Radon-Nikodým derivatives) of 𝑀 and 𝑁 . We also formalize the 𝑓 -divergences over a subset 𝐴 ∈ Σ𝑋 . ∫ Δ𝑋𝑓 |𝐴 (𝜇1, 𝜇2 ) = 𝐹 𝑓 𝑝 1 (𝑥) 𝑝 2 (𝑥) 𝑑𝜋 (𝑥).

The definition of extend_F requires the existence of a limit, which we have already proved. For inputs of negative values (outside of [0, ∞)), we set a dummy value of 0. Next we formalize the extension 0𝑓 (𝑎/0) = 𝑎𝑓 ∗ (0) (𝑎 ∈ [0, ∞)). We give the convex conjugate 𝑓 ∗ (𝑡) = 𝑡 𝑓 (1/𝑡).

𝐴

definition conj-F :: (real ⇒ real) ⇒ (real ⇒ real) where conj-F f = (𝜆t. t ∗ f (1 / t))

definition f-div-pos-sub where ∫ f-div-pos-sub f L M N A = ( + x∈A. e2ennreal ((extend-frac-F f ) (real-RN-deriv L M x) (real-RN-deriv L N x)) 𝜕L)

We then introduce a new function 𝐹 𝑓 : [0, ∞) → [0, ∞) → [−∞, ∞] with two arguments for 𝑎 and 𝑏 to formalize the term 𝑏 𝑓 (𝑎/𝑏) including the case of 𝑏 = 0. Isabelle HOL’s standard library defines 𝑎/0 = 0 to totalize the division operator (/). It is normal in many proof assistants, but not suitable for formalizing 0𝑓 (𝑎/0). In the definition of 𝑓 -divergence, we use the extension 𝐹 𝑓 instead of the original 𝑓 . We define 𝐹 𝑓 𝑎 𝑏 = 𝑏 𝑓¯(𝑎/𝑏) (0 < 𝑏) and 𝐹 𝑓 𝑎 0 = 𝑎𝑓 ∗ (0), and formalize it is as follows:

lemma f-div-pos-sub-sp: shows f-div-pos f L M N = f-div-pos-sub f L M N (space L)

In the formalization of basic properties of Δ𝑋𝑓 , we often formalize ones of Δ𝑋𝑓 |𝐴 . The nonnegativity 0 ≤ Δ𝑋𝑓 ((𝜇 1, 𝜇2 ) is obvious: we consider nonnegative 𝑓 , and density functions are nonnegative. We ∗ also formalizet the reversal law Δ𝑋𝑓 ((𝜇 1, 𝜇2 ) = Δ𝑋𝑓 ((𝜇2, 𝜇1 ). 6

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

Well-defiinedness. We formalize the well-definedness with respect to base measures. The formal proof is based on the following facts. If 𝜇1, 𝜇2 ≪ 𝜋 then 𝜇1 + 𝜇2 ≪ 𝜋. Hence 𝑑𝜇𝑘 𝑑𝜇𝑘 𝑑 (𝜇1 +𝜇 2 ) . This implies that 𝑓 -divergence with 𝑑𝜋 = 𝑑 (𝜇 1 +𝜇 2 ) 𝑑𝜋 base measure 𝜋 is equal to the one with base measure 𝜇1 + 𝜇2 .

shows f-div-pos-sub-partition f L M N A = f-div-pos-sub f L M N A

A sketch of formal proof. The formal proof is almost an interpretation of the proof of [54, Thm. 4]. It is combining the piecewise monotonicity of 𝑓 and the following facts. Í 𝑓 𝑓 Lemma 5.1. 𝑖 ∈𝐼 Δ𝑋 |𝐴𝑖 (𝜇 1, 𝜇2 ) = Δ𝑋 | ( Ð𝑖 ∈𝐼 𝐴𝑖 ) (𝜇 1, 𝜇2 ) holds for countable disjoint family of measurable sets {𝐴𝑖 }𝑖 ∈𝐼 .

lemma (in densities-two-measures-finite) f-div-pos-well-defined ′: assumes gf : generator-F f and posf : ∀ x > 0. f x ≥ 0 shows f-div-pos f (sum-measure M N ) M N = f-div-pos f L M N

𝑓

Lemma 5.2. Δ𝑋 |𝐴 = Δ𝑋𝑓 |𝐴 if 𝐴 ⊆ 𝑝 1−1 (0) or 𝐴 ⊆ 𝑝 2−1 (0).

Here, the locale densities-two-measures-finite is to give a situation to construct density functions of M and N with respect to L. sum-measure M N is the sum of M and N.

Lemma 5.3. If 𝑎, 𝑏, 𝑐, 𝑑 ∈ R and 𝐶 ∈ Σ𝑋 satisfies 0 < 𝑎, 0 ≤ 𝑐, ∀𝑥 ∈ 𝐶.𝑝 1 (𝑥)/𝑝 2 (𝑥) ∈ [𝑎, 𝑏] ∧ 𝑓 (𝑝 1 (𝑥)/𝑝 2 (𝑥)) ∈ [𝑐, 𝑑] and 𝑓 is either monotone increasing or decreasing on [𝑎, 𝑏] then 𝑓 Δ𝑋𝑓 |𝐶 (𝜇1, 𝜇2 ) ≤ Δ𝑋 |𝐶 (𝜇 1, 𝜇2 ) ≤ Δ𝑋𝑓 |𝐶 (𝜇 1, 𝜇2 ) + (𝑑 − 𝑐)𝜇2 (𝐶).

𝑓 -divergence between the same distributions. We have Δ𝑋𝑓 (𝜇, 𝜇) = 𝑓 (1) for any 𝜇 ∈ P (𝑋 ). We formalize Δ𝑋𝑓 |𝐴 (𝜇, 𝜇) = 𝑓 (1)𝜇 (𝐴) for finite mesure 𝜇 on 𝑋 and 𝐴 ∈ Σ𝑋 , where apply the fact 𝐹 𝑓 𝑧 𝑧 = (if 𝑧 = 0 then 0 else 𝑓 (1)). Then we formalize 𝐷𝑋𝛼 (𝜇, 𝜇) = 0 by applying 𝑓 𝛼 (1) = 1.

The overall formal proof spans about 3,300 lines, including 𝑓 formalization of measurable partitions, Δ𝑋 |𝐴 and exchange between integral and countable sums written in infsum. We also formalize the following trivial equality

lemma f-div-pos-sub-refl: fixes a::real assumes f10: f 1 = a and [measurable]: A ∈ sets L and sigma-finite-measure L absolutely-continuous L M finite-measure M sets M = sets L shows f-div-pos-sub f L M M A = a ∗ emeasure M A

𝑓

Δ𝑋 (𝜇 1, 𝜇2 ) =

sup

Δ𝐼𝑓 (P (ℎ) (𝜇 1 ), P (ℎ) (𝜇2 ))

𝐼 :finite,ℎ : 𝑋 →𝐼

where P (ℎ) (𝜇𝑘 ) is 𝜇𝑘 >>= (𝜆𝑥 . return ℎ(𝑥)) (𝑘 = 1, 2). Due to the type system of Isabelle/HOL, we restrict 𝐼 to subset of N.

Joint convexity. We formalize the joint convexity of Δ 𝑓 .

5.5

Δ𝑋𝑓 ((1 − 𝑞)𝜇 1 + 𝑞𝜈 1, (1 − 𝑞)𝜇 2 + 𝑞𝜈 2 ) ≤ (1 − 𝑞)Δ𝑋𝑓 (𝜇 1, 𝜇2 ) + 𝑞Δ𝑋𝑓 (𝜈 1, 𝜈 2 )

To prove the composition theorem of RDP, density functions of 𝑐 1 (𝑥) and 𝑐 2 (𝑥) for ℎ, 𝑘 : 𝑋 → P (𝑌 ) and 𝑥 ∈ 𝑋 might be problematic. For example if 𝑋 = 𝑌 = R and ℎ = return, there is no 𝜎-finite measue dominating all ℎ(𝑥) (𝑥 ∈ R). To avoid this problem, we approximate ℎ, 𝑘 : 𝑋 → P (𝑌 ). From Δ𝑌𝑓 (𝜈 1, 𝜈 2 ) = sup𝐼 :finite,ℎ : 𝑌 →𝐼 Δ𝐼𝑓 (ℎ(𝜈 1 ), ℎ(𝜈 2 )), 𝑌 can be reduced to finite setting. To reduce the domain 𝑋 , the study [54] shows the following property on 𝑓 -divergence, called approximability.

(0 ≤ 𝑞 ≤ 1).

abbreviation conv-measure a M N ≡ sum-measure (scale-measure (ennreal a) M) (scale-measure (ennreal (1 − a)) N ) lemma f-div-pos-joint-convex: fixes a::real assumes gf : generator-F f and posf : ∀ x > 0. 0 ≤ f x and cont1: densities-two-measures-finite L M1 N1 and cont2: densities-two-measures-finite L M2 N2 and a: 0 ≤ a a ≤ 1 shows f-div-pos f L (conv-measure a M1 M2) (conv-measure a N1 N2) ≤ a ∗ f-div-pos f L M1 N1 + (1−a) ∗ f-div-pos f L M2 N2

5.4

Approximation on two probabity kernels

Lemma 5.4. Let ℎ, 𝑘 : 𝑋 → P (𝐼 ) where 𝐼 is finite. There is a family of finite sets 𝐽𝑖 and measurable functions 𝑛𝑖 : 𝑋 → 𝐽𝑖 and 𝑚𝑖 : 𝐽𝑖 → 𝑋 (𝑖 ∈ N) such that Δ𝐼𝑓 (𝜇1 >>= (ℎ ◦ 𝑚𝑖 ◦ 𝑛𝑖 ), 𝜇2 >>= (𝑘 ◦ 𝑚𝑖 ◦ 𝑛𝑖 ))

Approximation by measurable partitions

−→ Δ𝐼𝑓 (𝜇1 >>= ℎ, 𝜇2 >>= 𝑘) as 𝑖 −→ ∞ We show two kinds of approximations of 𝑓 -divergences. First, 𝑓 -divergences (over 𝐴 ∈ Σ𝑋 ) can be approximated using Again, due to the type system of Isabelle/HOL, we adjust finite measurable partitions. In [54], this is called continuity. each 𝐽𝑖 to subset of N when we formalize this lemma. ( ) ∑︁ lemma f-div-pos-sub-approximable: {𝐴𝑖 }𝑖 ∈𝐼 : 𝑓 Δ𝑋 |𝐴 (𝜇 1, 𝜇2 ) = sup 𝐹 𝑓 𝜇1 (𝐴𝑖 ) 𝜇2 (𝐴𝑖 ) fixes h k:: ′a ⇒ nat measure and X M N :: ′a measure and I ::nat set fin. m’ble part. of 𝐴

assumes finI : finite I and A: A ⊆ I and gf : generator-F f and posf : ∀ x > 0. 0 ≤ f x and meas[measurable]: h ∈ X →𝑀 subprob-algebra (count-space I ) k ∈ X →𝑀 subprob-algebra (count-space I ) and subprob: M ∈ space (subprob-algebra X ) N ∈ space (subprob-algebra X ) shows ∃ J::nat ⇒ nat set. ∃ n::nat ⇒ ′a ⇒ nat. ∃ m::nat ⇒ (nat ⇒ ′a). (∀ i. finite (J i)) ∧ (∀ i. (n i) ∈ X →𝑀 (count-space (J i))) ∧ (∀ i. (m i) ∈ (count-space (J i)) →𝑀 X ) ∧ ((𝜆i::nat. (f-div-pos-sub f (count-space I ) (M>>=(𝜆x. h((m i)(n i x)))) (N >>=(𝜆x. k((m i)(n i x))))) A) −−−−−→ (f-div-pos-sub f (count-space I ) (M>>=h) (N >>=k)) A)

𝑖 ∈𝐼 𝑓 We write Δ𝑋 |𝐴 (𝜇 1, 𝜇2 ) for the right-hand side, and similary 𝑓 we can define Δ𝑋 (𝜇 1, 𝜇2 ) . We formalize the above equality.

definition f-div-pos-sub-partition where f-div-pos-sub-partition f L M N A Í = Sup {( C ∈ S. e2ennreal ((extend-frac-F f ) (measure M C) (measure N C))) | S. S ∈ measurable-partition L A } lemma (in densities-two-measures-finite) f-div-pos-sub-eq-f-div-pos-sub-partition: fixes f ::real ⇒ real assumes A[measurable]: A ∈ sets L and gf : generator-F f and posf : ∀ x > 0. f x ≥ 0 7

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

T. Sato

A sketch of formal proof. We adjust the proof in [54] to the type system of Isabelle/HOL. First, for measurable functions ℎ, 𝑘 : 𝑋 → [0, 𝑅] with 𝑅 ∈ (0, ∞), and given 0 < 𝜀, we define 𝐽 ⊆ N × N and measurable 𝑛 : 𝑋 → 𝐽 and 𝑚 : 𝐽 → 𝑋 by 𝑛(𝑥) = ( ⌈ℎ(𝑥)/𝜀⌉, ⌈𝑘 (𝑥)/𝜀⌉), 𝐽 = 𝑛(𝑋 ) and 𝑚(𝑡 1, 𝑡 2 ) ∈ 𝑛 −1 (𝑡 1, 𝑡 2 ). By the definition of 𝑛, ℎ(𝑚(𝑛(𝑥))) = 0 ⇔ ℎ(𝑥) = 0 and 𝑘 (𝑚(𝑛(𝑥))) = 0 ⇔ 𝑘 (𝑥) = 0 hold. Second, we extend this result to a family ℎ𝑖 , 𝑘𝑖 : 𝑋 → [0, 𝑅] (𝑖 ∈ Î 𝐼 ) for finite 𝐼 ⊆ N. Intuitively we take a product 𝐽 ≃ 𝑖 ∈𝐼 𝐽𝑖 where each 𝐽𝑖 is given by the first step for ℎ𝑖 , 𝑘𝑖 . Third, measurable functions ℎ, 𝑘 : 𝑋 → P (𝐼 ) can be converted to a family (𝜆𝑥 .ℎ(𝑥) ( 𝑗)), (𝜆𝑥 .𝑘 (𝑥) ( 𝑗)) : 𝑋 → [0, 1] (𝑗 ∈ 𝐼 ). By applying the second construction with 𝜀 = 1/(𝑖+1) for each 𝑖 ∈ N, we obtain (𝐽𝑖 , 𝑛𝑖 , 𝑚𝑖 ) such that (𝑓 ◦ 𝑚𝑖 ◦ 𝑛𝑖 ) and (𝑔 ◦ 𝑚𝑖 ◦ 𝑛𝑖 ) converge uniformly to 𝑓 and 𝑔 respectively. We then convert each 𝐽𝑖 ⊆ (𝐼 → N × N) to 𝐽𝑖′ ⊆ N and modify 𝑚𝑖 and 𝑛𝑖 as expected. Fourth, we show that for each 𝐴 ⊆ 𝐼 , (𝜇1 >>= (𝑓 ◦ 𝑚𝑖 ◦ 𝑛𝑖 )) (𝐴) and (𝜇2 >>= (𝑔 ◦𝑚𝑖 ◦𝑛𝑖 )) (𝐴) converge to (𝜇1 >>= 𝑓 ) (𝐴) and (𝜇 2 >>= 𝑔) (𝐴) respectively. We then conclude the main statement easily, because if these limits are 0 then the limiting sequences is 0, 0, . . . by construction of 𝑛𝑖 . The overall formal proof spans about 1,500 lines.

numbers and set by log(0) = 0 at 0. To formalize Rényi divergence, we need to introduce the extension 𝛼 1−1 log(∞) = ∞. We also introduce 𝛼 1−1 log(0) = −∞ to capture Rényi divergence between subprobability measures, and it is convenient 1 log(𝑡) is then monotone and that the mapping 𝑡 ↦→ 𝛼 −1 bijective. The inverse is, abbreviation inv-Renyi-log-part 𝛼 ≡ (𝜆z::ereal. if (z = −∞) then 0 else if (z < ∞) then ennreal(exp((real-of-ereal z) ∗ (𝛼−1))) else ∞)

From the well-definedness of Δ𝑋𝑓 , the base measure is dropped from the formalization: 𝛼

abbreviation Renyi-div ≡ (𝜆𝛼 M N . Renyi-divergence 𝛼 (sum-measure M N) M N )

6.2

definition Renyi-differential-privacy :: ( ′a ⇒ ′b measure) ⇒ ( ′a rel) ⇒ real ⇒ real ⇒ bool where Renyi-differential-privacy M adj 𝛼 r ≡ ∀ (d1,d2)∈adj. Renyi-div 𝛼 (M d1) (M d2) ≤ r ∧ Renyi-div 𝛼 (M d2) (M d1) ≤ r

Basic properties. We formalize basic properties: zero property, postprocessing inequality (Lemma 3.8), and composition theorem (Lemma 3.7). For example we formalize the composition theorem as follows:

Postprocessing inequality. Postprocessing inequality is formalized from the ones of approximabiliy, continuity, and (finite) Jensen inequality for extension 𝐹 𝑓 .

proposition Renyi-differential-privacy-composition-adaptive: assumes 1 < 𝛼 and measM: M ∈ X →𝑀 (subprob-algebra Y ) and RDPM: Renyi-differential-privacy M adj 𝛼 r Ë and measN : N ∈ (X 𝑀 Y ) →𝑀 (subprob-algebra Z) and RDPN : ∀ y ∈ space Y . Renyi-differential-privacy (𝜆 x. N (x,y)) adj 𝛼 r ′ and adj ⊆ (space X ) × (space X ) shows Renyi-differential-privacy (𝜆x. do{y ← M x; N (x, y)}) adj 𝛼 (r + r ′)

lemma f-div-pos-postprocessing: assumes gf : generator-F f and posf : ∀ x > 0. 0 ≤ f x and h[measurable]: h ∈ L →𝑀 subprob-algebra K and cont1: densities-two-measures-subprobabilistic L M N and cont2: densities-two-measures K (M >>= h) (N >>= h) shows f-div-pos f K (M>>=h)(N >>=h) ≤ f-div-pos f L M N

We remark here that K does not need to dominate each (h x). It suffices to dominate only two measures M >>= h and N >>= h. This implies that the formalization supports general settings: we may replace base measures by sums of appropriate measures.

6

RDP in Isabelle/HOL

6.1

Rényi divergence

RDP in Isabelle/HOL

We now fomalize the predicates for RDP in the same way as the formalization of DP [56, 57].

They are proved formalzation of the postprocessing inequality and the composability (Lemma 3.5). The formal proof of the composability is based on the proof given in [54]. From the continuity and appriximablity of 𝑓 -divergences, it 𝛼 suffices to formalize the composability of Δ 𝑓 in the finite discrete setting. 6.3

Gaussian mechanism

We formalize Rényi divergence, based on the reformulation We formalize 1-dimentional Gaussian mechanism. 1 𝑓 log Δ𝑋𝛼 (𝜇1, 𝜇2 ) (1 < 𝛼). 𝛼 −1 We recall that the generator function is 𝑓𝛼 (𝑡) = 𝑡 𝛼 .

definition Gaussian-dist :: real ⇒ real ⇒ real measure where Gaussian-dist 𝜎 x = (if 𝜎 ≤ 0 then return borel x else density lborel (normal-density x 𝜎))

definition Renyi-divergence where Renyi-divergence 𝛼 L M N = Renyi-log-part 𝛼 (f-div-pos (𝜆t. t powr 𝛼) L M N ) abbreviation Renyi-log-part 𝛼 ≡ (𝜆z::ennreal. if (z = 0) then −∞ else if (z < ∞) then ereal(ln (enn2real z) / (𝛼−1)) else ∞)

Here, density lborel (normal-density x 𝜎) is a formalization of N (𝑥, 𝜎 2 ). To show the measurability of it, we apply the continuity of cumulative distribution functions formalized in the AFP entry Error_Function [31]. Formalization of its RDP is rather straightforward.

1 Here, Renyi-log-part 𝛼 is the mapping 𝑡 ↦→ 𝛼 −1 log(𝑡). In Isabelle’s standard formalization, log is defined only for real

lemma Renyi-divergence-Gaussian-dist: fixes x y 𝜎 ::real assumes [arith]: 0 < 𝜎 and a: 1 < (𝛼::real)

𝐷𝑋𝛼 (𝜇 1, 𝜇2 ) =

8

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

shows Renyi-divergence 𝛼 lborel (Gaussian-dist 𝜎 x) (Gaussian-dist 𝜎 y) = (𝛼 ∗ (x − y) 2 / (2 ∗ 𝜎 2 ))

Proof of Lemmas 3.10 and 3.11 are done by taking lines near the boundary of 𝑅(𝛼, 𝜌) to show the inclusions 𝑅(𝛼, 𝜌) ⊆ 𝑅(𝜀 ∗, 𝛿) (𝜀 ∗ is determined by conversions). They are rather straightforward interpretations of existing proofs. The proof of Lemma 3.12 given in the original paper [7] is rather complex, but we found that we can rewrite it to proofs using privacy regions, while the authors mentioned that their approach is completely different from Balle et al.’ s [10]. Their approach can be understood as follows: instead of showing 𝑅(𝛼, 𝜌) ⊆ 𝑅(𝜀 ∗, 𝛿) directly, they prove the inclusion:

Multi-dimensional mechanism. We formalize the multidimensional Gaussian mechanism (𝜆𝑥®.N (𝑥, ® 𝜎 2 𝐼 )) : R𝑛 → 𝑛 P (R ) by the following induction. primrec Gaussian-vec :: nat ⇒ (nat ⇒ real) ⇒ (nat ⇒ real) measure where Gaussian-vec 0 f = return (count-space {𝜆-. undefined}) (𝜆-. undefined) | Gaussian-vec (Suc k) f = do{ g ← Gaussian-vec k f ; v ← Gaussian-dist 𝜎 (f k); return (Π𝑀 x∈{0..k}. borel) (g(k := v))}

[0, 1] × [0, 1] \ 𝑅(𝜀 ∗, 𝛿) ⊆ [0, 1] × [0, 1] \ 𝑅(𝛼, 𝜌).

Formalization of its RDP is just iterating ones of 1-dimensional Gaussian mechanism. We omit it in this paper. 6.4

They start the proof from the boundary of 𝑅(𝜀 ∗, 𝛿) (just lines) and enable finer evaluations. Our formal proof is based on this fact, which we borrow evaluations in the original proof.

Conversion to DP

We formalize the three conversion laws from RDP to DP, given by Mironov [52](Lemma 3.10), Balle et atl. [10](Lemma 3.11) and Asoodeh et al. [6](Lemma 3.12).

6.4.1 Moment Accoutants. We here formalize Lemma 3.13 where we also formalize Lemma 3.14 (explicit verision). lemma Renyi-differential-privacy-moments: assumes 0 ≤ K and K ≤ 𝜀 − 2 ∗ ln 𝛿 − 2 ∗ sqrt ( (𝜀 − ln 𝛿)∗ ln(1/𝛿) ) and 0 < 𝛿 𝛿 < 1 and 0 < 𝜀 and adj: adj ⊆ (space X ) × (space X ) and RDPM: ∀ 𝛼 > 1. Renyi-differential-privacy M adj 𝛼 (𝛼 ∗ K) and measM [measurable]: M ∈ X →𝑀 (prob-algebra Y ) shows differential-privacy M adj 𝜀 𝛿

lemma Renyi-differential-privacy-to-DP: assumes 1 < 𝛼 and RDPM: Renyi-differential-privacy M adj 𝛼 r and measM [measurable]: M ∈ X →𝑀 (prob-algebra Y ) and adj: adj ⊆ (space X ) × (space X ) and 0 < 𝛿 𝛿 < 1 shows differential-privacy M adj (if 1 ≤ 𝛼 ∗ 𝛿 then max 0 (r + ln (1 − 𝛿)) else min (max 0 (r + ln ((𝛼 − 1) / 𝛼) − (ln 𝛿 + ln 𝛼) / (𝛼 − 1))) (ln ((exp (r ∗ (𝛼 − 1)) − 1) / (𝛼 ∗ 𝛿) + 1) / (𝛼 − 1))) 𝛿 and differential-privacy M adj (max 0 (r + ln ((𝛼 − 1) / 𝛼) − (ln 𝛿 + ln 𝛼) / (𝛼 − 1))) 𝛿 and differential-privacy M adj (r − ln 𝛿 / (𝛼 − 1)) 𝛿

7

Rough Evaluation of Gaussian SGD

In this section, we formalize the following algorithm, known as the stochastic gradient descent (SGD) mechanism with Gaussian noise. Here is a typical formulation of such Gaussian SGD with subsampling (cf. [1, Alg. 1] and [7, Alg. 1]):

First two conversions are formalized based on the proofs given in [7, 10]. We first formalize the following privacy regions (cf. [44]) for divergences DP𝜀 and 𝐷 𝛼 .   𝑥 ≤ exp(𝜀) (1 − 𝑦) + 𝛿, 𝑅(𝜀, 𝛿) = (𝑥, 𝑦) ∈ [0, 1] 2 , 𝑦 ≤ exp(𝜀) (1 − 𝑥) + 𝛿 ( ) 𝑥 𝛼 (1 − 𝑦) 1−𝛼 + (1 − 𝑥) 𝛼 𝑦 1−𝛼 2 𝑅(𝛼, 𝜌) = (𝑥, 𝑦) ∈ [0, 1] . ≤ exp((𝛼 − 1)𝜌)

Algorithm 1 Gaussian SGD (∇𝜃 𝑙, 𝜃, 𝜂, 𝜎 2, 𝐶, 𝐷, 𝐿, 𝑁 ,𝑇 ) 1: for 𝑘 ← {1, . . . ,𝑇 } do 2: 𝐷 𝐿 ← PoissonSampling(𝐷, 𝐿/𝑁 ) 3: for 𝑥𝑖 ← 𝐷 𝐿 do 4: 𝑔 ← ∇𝜃 𝑙 (𝜃, 𝑥𝑖 )

Since 01−𝛼 = 0 in Isabelle/HOL’s standard library (we must have 01−𝛼 = ∞), we need case analyses with 𝑦 = 0, 1 to formalize 𝑅(𝛼, 𝜌) .

𝑔′ ← ∥𝑔𝐶 ∥ · 𝑔 6: 𝑧 ← N (𝑔′, 𝜎 2 𝐼 ) 7: 𝜃 ← 𝜃 − 𝜂 · 1/𝐿 · 𝑧 8: end for 9: end for 10: return 𝜃 5:

definition Region-Renyi :: real ⇒ real ⇒ (real × real) set where Region-Renyi 𝛼 r = {(x,y) |x y::real. ¬(y = 1 ∧ 0 < x ∨ y = 0 ∧ x < 1) ∧ (x powr 𝛼 ∗ (1 − y) powr (1 − 𝛼) + (1 − x) powr 𝛼 ∗ y powr (1 − 𝛼)) ≤ exp (r ∗ (𝛼 − 1))} ∩ {0..1}×{0..1}

We have a core of conversions ([10, Sec. 5.1]): 𝑅(𝛼, 𝜌) ⊆ 𝑅(𝜀, 𝛿)

Here, ∇𝜃 𝑙 is gradient of loss function 𝑙 (𝜃, −); 𝜃 is an initial parameter; 0 < 𝜂 is learning rate; 𝜎 2 is variance of Gaussian noise; 0 < 𝐶 is length-limit of gradient; 𝐷 ∈ (R𝑚 ) ∗ is a dataset; 𝑁 ∈ N is the size of data; 𝐿 ∈ N is expected batch size for subsampling; 𝑇 ∈ N is a number of loops. The subroutine PoissonSampling(𝐷, 𝐿/𝑁 ) samples each entry 𝑥𝑖 in the dataset 𝐷 independently with probability 𝐿/𝑁 . We remark that 𝑧 ← N (𝑔′, 𝜎 2 𝐼 ) is a random sampling.

=⇒ ∀𝑋 : measurable space, ∀𝜇1, 𝜇2 ∈ P (𝑋 ) (𝐷𝑋𝛼 (𝜇1, 𝜇2 ) ≤ 𝜌 ⇒ DP𝑋𝜀 (𝜇 1, 𝜇2 ) ≤ 𝛿). In the formal proofs of conversion laws, we use this fact inside the proofs. In fact the converse ( ⇐= ) also holds, but due to the type system of Isablle/HOL, it is hard to formalize, because of the universal quantifier ∀𝑋 running over all measurable spaces. 9

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

7.1

T. Sato

An issue on formalizing tight bounds

above, we can calculate the resulting Rényi divergences:

This paper gives only a rough evaluation of this mechanism. Our privacy evaluation is probably not tight. We have not formalized a well-known tight evaluation. We try to explain an obstacle to the formalization of a tight privacy guarantee. The tight evaluations of Gaussian SGD in many prior studies are based on the following lemma.

𝐷 𝛼 (d0, (1 − 𝑞)d0 + 𝑞N (𝑓 (𝑥), 𝜎 2 ))   ∫ 1 0 = 𝑑𝑦 log (1 − 𝑞) 1−𝛼 + 𝑞 𝛼 −1 𝛼 −1 R\{0} 𝑓 N (𝑓 (𝑥 1 ),𝜎 2 ) (𝑦) = − log(1 − 𝑞) 𝐷 𝛼 ((1 − 𝑞)d0 + 𝑞N (𝑓 (𝑥), 𝜎 2 ), d0 )   ∫ 𝑓 N (𝑓 (𝑥 1 ),𝜎 2 ) (𝑦) 𝛼 1 𝛼 = log (1 − 𝑞) + 𝑞 𝑑𝑦 𝛼 −1 0𝛼 −1 R\{0} 1 log ((1 − 𝑞) 𝛼 + 𝑞∞) = ∞ = 𝛼 −1

Lemma 7.1 ([1, Sec. B, Lem. 3]). Let 𝑓 : 𝑋 → R𝑑 with ∥𝑓 (𝑥) ∥ 2 ≤ 1, and 𝐽 be a sample from [𝑛] = {0, . . . , 𝑛 − 1} where each 𝑖 ∈ [𝑛] is chosen independently with probability 𝑞. Suppose 1 ≤ 𝜎, 𝑞 < 1/16𝜎, 𝛼 ≤ 𝜎 2 log(1/𝑞𝜎), and that 1 < 𝛼 is integer. Then the mechanism Í| 𝐽 | 𝜆𝐷.{𝑧 1 ← N (0, 𝜎 2 ); · · · ; 𝑧 | 𝐽 | ← N (0, 𝜎 2 ); 𝑘=1 𝑧𝑘 + 𝑓 (𝐷𝑖𝑘 )}

Therefore, for both definitions of adjacency, (𝛼, 𝑞 2𝛼/(1 − 𝑞)𝜎 2 +𝑂 (𝑞 3 ))-RDP fails when the datasets are too small, and the initial value is fixed. The original proof of Lemma 7.1 is based on showing the following inequality:

is (𝛼, 𝑞 2𝛼/(1 − 𝑞)𝜎 2 + 𝑂 (𝑞 3 ))-RDP. We could not formalize this lemma in this form yet. Moreover, for small datasets, we can give a counterexample in a corner case. Suppose 𝑑 = 1 and 𝑛 = 1, and adjacency is determined by Hamming distance. Then adjacent datasets 𝐷 1 and 𝐷 2 will be singleton lists [𝑥 1 ] and [𝑥 2 ] with 𝑥 1 ≠ 𝑥 2 . Then the results of this mechanism for the datasets 𝐷𝑘 (𝑘 = 1, 2) are the following convex sum of probability measures.

𝐷 𝛼 (N (0, 𝜎 2 ), (1 − 𝑞)N (0, 𝜎 2 ) + 𝑞N (1, 𝜎 2 )) ≤ 𝑞 2𝛼/(1 − 𝑞)𝜎 2 + 𝑂 (𝑞 3 )). We must assume a mixture distribution of two Gaussian distributions with the same variance 𝜎 2 , to cancel the terms of order 𝑂 (𝑞 1 )) in the evaluation of the divergence. However, showing the above inequality does not connect well to the evaluation of the entire mechanism, even if we assume that the initial value is also sampled from a Gaussian distribution. Intuitively, for the insertion adjacency 𝐷 2 = 𝐷 1 ∪ {𝑥 }, the distribution N (0, 𝜎 2 ) in the above inequality indicates the branch that the differing element 𝑥 was not sampled in 𝐽 , and N (1, 𝜎 2 ) indicates the one that 𝑥 was sampled. In the second branch, from the element 𝑥, a new random sampling 𝑧𝑥 ← N (𝑥, 𝜎∗2 ) must be added to the total, other than 𝑧𝑥 . Hence, the variance of the second branch must be greater than the first one by 𝜎∗2 . Hence, what we need to evaluate is

𝑀 (𝐷𝑘 ) = (1 − 𝑞)d0 + 𝑞N (𝑓 (𝑥𝑘 ), 𝜎 2 ). Here, d0 is Dirac distribution centered at 0 on R. We also assume |𝑓 (𝑥 1 ) − 𝑓 (𝑥 2 )| = 1. Then we evaluate the Rényi divergence between them: 𝐷 𝛼 ((1 − 𝑞)d0 + 𝑞N (𝑓 (𝑥 1 ), 𝜎 2 ), (1 − 𝑞)d0 + 𝑞N (𝑓 (𝑥 2 ), 𝜎 2 ))   ∫ 𝑓 N ( 𝑓 (𝑥 1 ),𝜎 2 ) (𝑦) 𝛼 1 = log (1 − 𝑞) + 𝑞 𝑑𝑦 𝛼 −1 𝛼 −1 R\{0} 𝑓 N ( 𝑓 (𝑥 2 ),𝜎 2 ) (𝑦)     1 𝛼 = log (1 − 𝑞) + 𝑞 exp (𝛼 − 1) 2 𝛼 −1 𝜎 𝛼 ≥𝑞 2. 𝜎

𝐷 𝛼 (N (0, 𝜎12 ), (1 − 𝑞)N (0, 𝜎12 ) + 𝑞N (1, 𝜎22 )) where 𝜎12 and 𝜎22 are different (moreover 𝜎12 < 𝜎22 ). We postpone the evaluation of the Rényi divergence between such mixture distributions to future work.

Here 𝑓 N ( 𝑓 (𝑥𝑘 ),𝜎 2 ) (𝑘 = 1, 2) is the density of N (𝑓 (𝑥 1 ), 𝜎 2 ). The equations are obtained as follows: We take the density functions of 𝑀 (𝐷𝑘 ) (𝑘 = 1, 2) with respect to the sum of d0 and the Borel measure, and unfold the definition of 𝐷 𝛼 . By splitting the integral in the definition of 𝐷 𝛼 with {0} and R \ {0}, we conclude the first equation. The second equation is obtained in the same way as in Lemma 3.6. Then, the inequality is obtained by a simple calculation. Since 𝑞 is quite smaller than 1, the resulting value 𝛼𝑞/𝜎 2 is greater than 𝑞 2𝛼/(1 − 𝑞)𝜎 2 + 𝑂 (𝑞 3 ). We have this issue regardless of assumptions 1 ≤ 𝜎, 𝑞 < 1/16𝜎, 𝛼 ≤ 𝜎 2 log(1/𝑞𝜎), 1 < 𝛼 : integer. For another example, Suppose 𝑑 = 1 and 𝑛 = 1, and that the adjacency is determined by insertion 𝐷 2 = 𝐷 1 ∪ {𝑥 }. Then, we consider 𝐷 1 = {} and 𝐷 2 = {𝑥 }. In similar way as

7.2

A rule for subsampled RDP

Privacy amplification by subsampling [1, 9, 63] is an important technique for privacy-preserving mechanisms of large populations. In prior studies, these evaluations are rather complicated, hence formalizing them requires much more work. In this paper, we formalize a simpler (but rough) rule for RDP based on the joint-convexity of Rényi divergence instead. From the joint-convexity of 𝑓 -divergences, Lemma 7.2. For 𝜇, 𝜈 1, 𝜈 2 ∈ P (𝑋 ), 1 < 𝛼 and 0 < 𝑞 < 1, 𝐷 𝛼 ((1 − 𝑞)𝜇 + 𝑞𝜈 1, (1 − 𝑞)𝜇 + 𝑞𝜈 2 ) 1 log ((1 − 𝑞) + 𝑞 exp((𝛼 − 1)𝐷 𝛼 (𝜇 2, 𝜈 2 )) . ≤ 𝛼 −1 10

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

| Poisson-Sample (x#xs) = do{xs2 ← Poisson-Sample xs; c ← bern-dist ; return (listM M) (if c then x # xs2 else xs2)}

It gives an evaluation of the amplification of RDP by subsampling as follows: Intuitively, subsampling deletes differing entries 𝑥 1 ≠ 𝑥 2 in adjacent datasets 𝐷 1 and 𝐷 2 with probability 𝑞. Then the result can be formulated as (1 − 𝑞)𝜇 + 𝑞𝜈𝑘 where 𝜇 and 𝜈𝑘 are the results where 𝑥𝑘 is deleted and remains, respectively (𝑘 = 1, 2). We can determine the variance 𝜎 2 of Gaussian noise making the Gaussian SGD with Poisson subsampling (𝜀, 𝛿)-DP, by combineing Lemmas 7.2 and 3.14 and the following lemma.

abbreviation bern-dist ≡ measure-pmf (bernoulli-pmf b)

Here, M is a measurable space for the domain of data points. A dataset is formalized as space (listM M). The parameter b is the probability of sampling of each data point, and bern-dist is just the coin flip with probabilty b. We here remind another formulation of convex combinations by coin flips. lemma bern-dist-conv-measure: assumes M ∈ space (prob-algebra L) and N ∈ space (prob-algebra L) shows do{ c ← bern-dist ; if c then M else N } = conv-measure b M N

Lemma 7.3. For 𝑓 (𝑟 ) = 𝛼 1−1 log ((1 − 𝑞) + 𝑞 exp((𝛼 − 1)𝑟 ), √ √ log(1/ 𝑞) log(1 − 𝑞 + 𝑞) =⇒ 𝑓 (𝑟 ) ≤ 𝑟. 𝑟≤ √ 𝛼 −1 log(1/ 𝑞) This lemma can be proved from the convexity of 𝑓 (𝑟 ). These rules can be mechanized in Isabelle/HOL. For example, we formalize Lemma 7.2 as follows:

We then implement Lines 3–8 of Algorithm 1. definition SGD-Poisson where SGD-Poisson 𝜗 D = do{xs ← (Poisson-Sample D); SGD-batch 𝜗 xs}

lemma (in comparable-finite-measures) Renyi-div-convex-sum2: assumes a: 1 < (𝛼::real) and b ′: 0 ≤ (b::real) b ≤ 1 and M2: M2 ∈ space(prob-algebra X ) and (Renyi-div 𝛼 M N ) ≤ R shows (Renyi-div 𝛼 (conv-measure b M M2) (conv-measure b N M2)) ≤ Renyi-log-part 𝛼 (ennreal b ∗ inv-Renyi-log-part 𝛼 R + ennreal (1 − b))

7.3

Finally, we implement the entire mechanism by primrec SGD-Poisson-iter where SGD-Poisson-iter 𝜗 D 0 = (return borel 𝜗) | SGD-Poisson-iter 𝜗 D (Suc k) = do{𝜗 ′ ← SGD-Poisson 𝜗 D ; (SGD-Poisson-iter 𝜗 ′ D k)}

7.3.2 Evaluations for DP and RDP. We consider the adjacency with Hamming distance. We formalize a rough evaluation for RDP of SGD-Poisson-iter. Below, HLists is the set of Sp-lists of length N and Hdist is the Hamming distance.

A sketch of formalization

Let’s move on to our formalization. In our formalization, the ratio 𝐿/𝑁 in Algorithm 1 is abstracted as 𝑞, and 𝜂 · 1/𝐿 is simplified as 𝜂. For simplicity we fix 𝜗, since its distribution is notË given in prior studies. We fix (𝜆(𝜗, x). grad 𝜗 x) ∈ borel 𝑀 borel →𝑀 borel for formalization of ∇𝜃 𝑙.

lemma RDP-SGD-Poisson-iter: assumes a: 1 < 𝛼 and 𝜗 ∈ space Sp defines adj ≡ {(xs,ys)| xs ys. xs ∈ HLists ∧ ys ∈ HLists ∧ Hdist xs ys = 1} shows Renyi-differential-privacy (𝜆xs. SGD-Poisson-iter 𝜗 xs T ) adj 𝛼 (T ∗ (ln (b ∗ exp((2 ∗ (𝛼 ∗ C 2 ) / 𝜎 2 ) ∗ (𝛼−1)) + (1 − b)) / (𝛼−1)))

7.3.1 Implementation of programs. We consider datasets consisting of m-dimensional tuples. We formalize the space R𝑚 of m-dimensional tuples as the following Sp. abbreviation sM ≡ {0..m−1} abbreviation Sp ≡ (Π𝑀 x∈sM. (borel::real measure))

Combining this result and formalization of Lemmas 3.14 and 7.3, we can formalize a condition of 𝜎, 𝐶 and 𝑇 to guarantee (𝜀, 𝛿)-DP.

We then implement Algorithm 1. We first implement Lines 4–7 of Algorithm 1 (a loop step).

lemma DP-SGD-Poisson-iter: assumes 𝜗 ∈ space Sp and 0 < 𝛿 𝛿 < 1 and 0 < 𝜀 and cond2: 2 ∗ C 2 / 𝜎 2 ≤ − ln (sqrt b) / ((1 − ln 𝛿 / 𝜀 + sqrt ((𝜀 − ln 𝛿) ∗ − ln 𝛿) / 𝜀 − 1) ∗ (1 − ln 𝛿 / 𝜀 + sqrt ((𝜀 − ln 𝛿) ∗ − ln 𝛿) / 𝜀)) and cond1: (2 ∗ real T ∗ C 2 ) / 𝜎 2 ≤ (𝜀 − 2 ∗ ln 𝛿 − 2 ∗ sqrt ((𝜀 − ln 𝛿) ∗ ln (1 / 𝛿))) ∗ ( − ln (sqrt b) / ln (1 − b + sqrt b)) defines adj ≡ {(xs,ys)| xs ys. xs ∈ HLists ∧ ys ∈ HLists ∧ Hdist xs ys = 1} shows differential-privacy (𝜆xs. SGD-Poisson-iter 𝜗 xs T ) adj 𝜀 𝛿

definition SGD-step where SGD-step v𝜗 vx = do { let vgx = grad v𝜗 vx; let vgx2 = (if Sp-L2-set vgx > C then (𝜆k∈sM. (C/ Sp-L2-set vgx) ∗ vgx k) else vgx); vy ← Gaussian-vec 𝜎 m vgx2; let v𝜗new = (𝜆k∈sM. v𝜗 k − rate ∗ vy k); return Sp v𝜗new }

Next, we implement Lines 3–8 of Algorithm 1(batch loop).

7.3.3 Sketch of formal proof. We first evaluate RDP of a step of loop (SGD-step). It is a typical Gaussian mechanism, where calculation and clipping of gradient has sensitivity 2𝐶. We just evaluate the Rényi divergence.

primrec SGD-batch where SGD-batch 𝜗 [] = (return Sp 𝜗) | SGD-batch 𝜗 (x # xs) = (SGD-step 𝜗 x) >>= (𝜆𝜗 . SGD-batch 𝜗 xs)

lemma Renyi-div-SGD-step: assumes a: 1 < 𝛼 and v𝜗 ∈ space Sp vx1 ∈ space Sp vx2 ∈ space Sp shows Renyi-div 𝛼 (SGD-step v𝜗 vx1) (SGD-step v𝜗 vx2) ≤ (2 ∗ (𝛼 ∗ C 2 ) / 𝜎 2 )

Next, we implement the subroutine PoissonSampling(𝐷, 𝑏) (Line 2 of Algorithm 1). We assume 0 < b and b < 1. primrec Poisson-Sample where Poisson-Sample [] = return (listM M) [] 11

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

T. Sato

We next evaluate the batch loop (SGD-batch) and Poisson subsampling (Poisson-Sample). Both of them have similar structures. For 𝐷 = {𝑥 1, . . . , 𝑥𝑘 }, each of them can be reforemulated as bind-iterations of some measurable function 𝑔(𝑥𝑖 , −) : X → P (X) and distribution 𝑃 ∈ P (𝑋 ):

In recent years, Rocq has made significant progress on measure theory: Lebesgue integrations, Fubini-Tonelli theorem, Radon-Nikodým theorem, and the fundamental theorem of calculus for Lebesgue integration [4, 18, 19, 43]. In Lean, Tristan et al. developed an automated measurability prover for probabilistic programs in the continuous setting via reparametrization of the uniform distribution [62]. Also, the Lean Mathlib library is actively updated, and it contains the formalization of basic measure theory (see [50]). Recently Luccioli formalized 𝑓 -divergence in Lean 4 [48]. The Lean formalization is more elegant than ours, and it covers general generator functions for Δ 𝑓 and the postprocessing inequality of Rényi divergence. However, the composability of Rényi divergence and the approximability of 𝑓 -divergences are not included in the Lean formalization. Thus, we argue the novelty of our formalization for these results. We expect that this work will also be useful for users of these proof assistants who want to formalize DP and RDP in the continuous setting. For example, formalizations of the composability of RDP and conversion laws are useful. Also, the users might be able to learn from our formalization what fundamental libraries will be required.

𝑃 >>= 𝑔(𝑥 1, −) >>= · · · >>= 𝑔(𝑥𝑘 , −). From the associativity of the Giry monad bind, we can formalize that each of them preserves appends, hence so does their sequential composition SGD-Poisson: lemma SGD-Poisson-append: assumes xs ∈ space (listM Sp) ys ∈ space (listM Sp) 𝜗 ∈ space Sp shows SGD-Poisson 𝜗 (xs@ys) = do{𝜗 ′ ← SGD-Poisson 𝜗 xs; SGD-Poisson 𝜗 ′ ys}

We now consider the adjacency based on Hamming distance. Then adjacent datasets 𝐷 1 and 𝐷 2 are decomposed by 𝐷 1 = 𝑥𝑠@[𝑥 1 ]@𝑦𝑠 and 𝐷 2 = 𝑥𝑠@[𝑥 2 ]@𝑦𝑠 where 𝑥 1 ≠ 𝑥 2 . By combining the formalization of RDP of a step of loop, the above append law, and Lemmas 7.2 we obtain. lemma Renyi-div-SGD-Poisson-conv: assumes adjacent: xs ∈ HLists ys ∈ HLists Hdist xs ys = 1 and 𝜗 ∈ space Sp and a: 1 < 𝛼 shows Renyi-div 𝛼 (SGD-Poisson 𝜗 xs) (SGD-Poisson 𝜗 ys) ≤ Renyi-log-part 𝛼 (ennreal b ∗ inv-Renyi-log-part 𝛼 (ereal (2 ∗ (𝛼 ∗ C 2 ) / 𝜎 2 )) + ennreal (1 − b))

9

In this paper, we give an Isabelle/HOL library for Rényi differential privacy in the continuous setting, and give a formalization of the stochastic gradient descent (SGD) mechanism with Gaussian noise and Poisson subsampling. We have formalized conversion laws from RDP to DP, including Asoodeh et al.’s complicated one. For a technical basis, we formalize 𝑓 -divergences, which are a class of statistical divergences generated by nonnegative convex functions, and their basic properties. Our formalization is limited to nonnegative generator functions, but it is enough to formalize Rényi divergences. We formalize the RDP and RDP of Gaussian SGD Poisson subsampling, though the result is limited. During the trial of formalizations, we found a technical gap in a well-known central lemma for the Gaussian mechanism with subsampling. We thus took another approach and give a novel (not good but simple) evaluation of subsampling amplification of Rényi differential privacy.

Finally by applying the composition theorem of RDP 𝑇 times, we have RDP of the entire Algorithm 1 (RDP-SGD-Poisson-iter). The formalization of Poisson subsampling costs about 400 lines, and the one of the Algorithm 1 costs about 700 lines.

8

Conclusion and Future Work

Related Work

Dong et al. propose the concept of 𝑓 -differential privacy (𝑓 -DP), which are modeled with trade-off curves between Type I and Type II errors of hypothesis testing for two adjacent datasets [25]. Recently, Fernandes et al. reformulated it as a Galois connection between trade-off curves and tworow information channels, and gave a simpler proof of the composition theorem of 𝑓 -DP [34]. There are several related studies for formal verification of probabilistic programs in proof assistants. In Isabelle/HOL, Eberl et al. constructed an executable first-order functional probabilistic programming language [32]. Lochbihler formalized protocols with probabilistic oracles [47]. Basin et al. implemented a framework CryptHOL in for rigorous game-based proofs in cryptography [16]. Hirata et al. developed an extensive Isabelle/HOL library of quasi-Borel spaces [40–42], which is a model for denotational semantics of higher-order probabilistic programming languages with continuous distributions [39, 58]). In Rocq, Bagnall and Stewart embedded MLCert for formal verification of machine learning algorithms [8]. Affeldt et al. formalized probabilistic programs with continuous random samplings and conditional distributions [3] by formalizing the semantic model based on s-finite kernels [59].

Overview. We show overview of our formalization in Table 1. We use 18,043 lines in total, including comments. Future work. A topic of future work is to finish the formalization of 𝑓 -divergences for general generator functions. The formalization of 𝑓 -divergence is not novel because of the existing Lean formalization [48], but it might be meaningful to enrich Isabelle/HOL’s library. For another topic, we plan to improve the formalization of the privacy of Gaussian SGD. Our current formalization 12

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

Table 1. Overview of formalization (Lines of Code). Category Lines Modification of Differential_Privacy about 400 Miscellaneous lemmas 862 2,361 Convex functions 𝑓 -divergences for nonnegative generators 8,178 3,203 Rényi divergence and its composability Gaussian Mechanism, Gaussian SGD 2,739 Total 18,043

Conversion and Applications. IEEE Journal on Selected Areas in Information Theory 2, 1 (2021), 208–222. doi:10.1109/JSAIT.2021.3054692 [8] Alexander Bagnall and Gordon Stewart. 2019. Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. Proceedings of the AAAI Conference on Artificial Intelligence 33 (2019), 2662–2669. doi:10.1609/aaai.v33i01.33012662 [9] Borja Balle, Gilles Barthe, and Marco Gaboardi. 2018. Privacy amplification by subsampling: tight analyses via couplings and divergences. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (Montréal, Canada) (NIPS’18). Curran Associates Inc., Red Hook, NY, USA, 6280–6290. [10] Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Tetsuya Sato. 2020. Hypothesis Testing Interpretations and Renyi Differential Privacy. In Proceedings of the Twenty Third International Conference on Artificial Intelligence and Statistics (AISTATS 2020) (Proceedings of Machine Learning Research, Vol. 108), Silvia Chiappa and Roberto Calandra (Eds.). PMLR, Online, 2496–2506. http://proceedings.mlr.press/ v108/balle20a.html [11] Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Advanced Probabilistic Couplings for Differential Privacy. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (Vienna, Austria) (CCS ’16). ACM, New York, NY, USA, 55–67. doi:10.1145/2976749. 2978391 [12] Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In ACM Symposium on Principles of Programming Languages (Mumbai, India) (POPL ’15). ACM, New York, NY, USA, 55–68. doi:10. 1145/2676726.2677000 [13] Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Proving Differential Privacy via Probabilistic Couplings. In ACM/IEEE Symposium on Logic in Computer Science (New York, NY, USA) (LICS ’16). ACM, New York, NY, USA, 749–758. doi:10.1145/2933575.2934554 [14] Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago ZanellaBéguelin. 2012. Probabilistic Relational Reasoning for Differential Privacy. In ACM Symposium on Principles of Programming Languages (Philadelphia, PA, USA) (POPL ’12). ACM, New York, NY, USA, 97–110. doi:10.1145/2103656.2103670 [15] Gilles Barthe and Federico Olmedo. 2013. Beyond Differential Privacy: Composition Theorems and Relational Logic for 𝑓 -divergences between Probabilistic Programs. In Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Proceedings, Part II. Springer Berlin Heidelberg, Berlin, Heidelberg, 49–60. doi:10.1007/9783-642-39212-2_8 [16] David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar, Sefidgar. 2020. CryptHOL: Game-Based Proofs in Higher-Order Logic. Journal of Cryptology 33 (2020), 494–566. [17] Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04) (proceedings of the 31st acm sigplan-sigact symposium on principles of programming languages (popl ’04) ed.). ACM, 43. https://www.microsoft.com/en-us/research/publication/simplerelational-correctness-proofs-for-static-analyses-and-programtransformations/ [18] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. 2022. A Coq Formalization of Lebesgue Integration of Nonnegative Functions. J. Autom. Reason. 66, 2 (2022), 175–213. doi:10.1007/S10817-021-09612-0 [19] Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. 2023. A Coq Formalization of Lebesgue Induction Principle and Tonelli’s Theorem. In Formal Methods - 25th International

gives a very rough evaluation and is too simple. We recognize that there is a large room for improvement. For example, Asoodeh et al. also give a refinement of the law for moment accountants in DP [2], which is based on Lemma 3.12 [6]. For amplification of RDP by subsampling, Lemma 7.2 might give a better evaluation than [63, Thm. 9] for a large subsampling rate 𝑞 and a small RDP bound of original mechanism, although such a case is not meaningful. Formalization of [63, Thm. 9] and comparison of them is also possible future work. We also aim to formalize a variant of Gaussian SGD by Lee and Kifer [45], it changes the amount of noise according to gradients and privacy budgets already paid. It might be a good example of the high expressiveness of Isabelle/HOL.

Acknowledgments Tetsuya Sato was supported by JSPS KAKENHI Grant Number JP24K14893.

References [1] Martin Abadi, Andy Chu, Ian Goodfellow, H. Brendan McMahan, Ilya Mironov, Kunal Talwar, and Li Zhang. 2016. Deep Learning with Differential Privacy. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (Vienna, Austria) (CCS ’16). Association for Computing Machinery, New York, NY, USA, 308–318. doi:10.1145/2976749.2978318 [2] Martín Abadi, Andy Chu, Ian J. Goodfellow, H. Brendan McMahan, Ilya Mironov, Kunal Talwar, and Li Zhang. 2016. Deep Learning with Differential Privacy. In ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016. 308–318. doi:10.1145/2976749.2978318 [3] Reynald Affeldt, Cyril Cohen, and Ayumu Saito. 2023. Semantics of Probabilistic Programs Using S-Finite Kernels in Coq. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (Boston, MA, USA) (CPP 2023). Association for Computing Machinery, New York, NY, USA, 3–16. doi:10.1145/3573105.3575691 [4] Reynald Affeldt and Zachary Stone. 2024. Towards the Fundamental Theorem of Calculus for the Lebesgue Integral in Coq. In 35es Journées Francophones des Langages Applicatifs (JFLA 2024). Saint-Jacut-de-laMer, France. https://inria.hal.science/hal-04406350 [5] Apple Inc. 2017. Differential Privacy Overview. https://www.apple. com/privacy/docs/Differential_Privacy_Overview.pdf Accessed: September 12, 2024. [6] Shahab Asoodeh, Jiachun Liao, Flávio P. Calmon, Oliver Kosut, and Lalitha Sankar. 2020. Three Variants of Differential Privacy: Lossless Conversion and Applications. CoRR abs/2008.06529 (2020). arXiv:2008.06529 https://arxiv.org/abs/2008.06529 [7] Shahab Asoodeh, Jiachun Liao, Flavio P. Calmon, Oliver Kosut, and Lalitha Sankar. 2021. Three Variants of Differential Privacy: Lossless 13

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

T. Sato

Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 14000), Marsha Chechik, JoostPieter Katoen, and Martin Leucker (Eds.). Springer, 39–55. doi:10.1007/ 978-3-031-27481-7_4 [20] Mark Bun and Thomas Steinke. 2016. Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds. In Theory of Cryptography - 14th International Conference, TCC 2016-B. 635–658. doi:10.1007/978-3-662-53641-4_24 [21] Clément L. Canonne, Gautam Kamath, and Thomas Steinke. 2021. The Discrete Gaussian for Differential Privacy. arXiv:2004.00010 [cs.DS] https://arxiv.org/abs/2004.00010 [22] I. Csiszár. 1967. Information-type measures of difference of probability distributions and indirect observations. Studia Sci. Math. Hungar. 2 (1967), 299–318. [23] Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu. 2014. Really Natural Linear Indexed Type Checking. In Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages (Boston, MA, USA) (IFL ’14). Association for Computing Machinery, New York, NY, USA, Article 5, 12 pages. doi:10.1145/2746325.2746335 [24] Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, and Jean-Baptiste Tristan. 2025. Verified Foundations for Differential Privacy. 9, PLDI, Article 191 (June 2025), 25 pages. doi:10.1145/3729294 [25] Jinshuo Dong, Aaron Roth, and Weijie J. Su. 2022. Gaussian Differential Privacy. Journal of the Royal Statistical Society Series B: Statistical Methodology 84, 1 (02 2022), 3–37. doi:10.1111/rssb.12454 [26] Cynthia Dwork. 2006. Differential Privacy. In Automata, Languages and Programming, Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener (Eds.). Lecture Notes in Computer Science, Vol. 4052. Springer Berlin Heidelberg, 1–12. doi:10.1007/11787006_1 [27] Cynthia Dwork, Krishnaram Kenthapadi, Frank McSherry, Ilya Mironov, and Moni Naor. 2006. Our data, ourselves: privacy via distributed noise generation. In Proceedings of the 24th Annual International Conference on The Theory and Applications of Cryptographic Techniques (St. Petersburg, Russia) (EUROCRYPT’06). Springer-Verlag, Berlin, Heidelberg, 486–503. doi:10.1007/11761679_29 [28] Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. 2006. Calibrating Noise to Sensitivity in Private Data Analysis. In Theory of Cryptography, Shai Halevi and Tal Rabin (Eds.). LNCS, Vol. 3876. Springer Berlin Heidelberg, 265–284. doi:10.1007/11681878_14 [29] Cynthia Dwork, Moni Naor, Toniann Pitassi, and Guy N. Rothblum. 2010. Differential privacy under continual observation. In Proceedings of the Forty-Second ACM Symposium on Theory of Computing (Cambridge, Massachusetts, USA) (STOC ’10). Association for Computing Machinery, New York, NY, USA, 715–724. doi:10.1145/1806689.1806787 [30] Cynthia Dwork and Aaron Roth. 2013. The Algorithmic Foundations of Differential Privacy. Foundations and Trends® in Theoretical Computer Science 9, 3-4 (2013), 211–407. doi:10.1561/0400000042 [31] Manuel Eberl. 2018. The Error Function. Archive of Formal Proofs (February 2018). https://isa-afp.org/entries/Error_Function.html, Formal proof development. [32] Manuel Eberl, Johannes Hölzl, and Tobias Nipkow. 2015. A Verified Compiler for Probability Density Functions. In European Symposium on Programming (ESOP 2015) (LNCS, Vol. 9032). Springer, 80–104. doi:10. 1007/978-3-662-46669-8_4 [33] Amy Feng. 2026. Verification of OpenDP Transformations. https: //dash.harvard.edu/handle/1/42743980 [34] Natasha Fernandes, Annabelle McIver, and Parastoo Sadeghi. 2026. Composition Theorems for f-Differential Privacy. In Foundations of Software Science and Computation Structures, Nathalie Bertrand and Stefan Milius (Eds.). Springer Nature Switzerland, Cham, 462–483. doi:10.1007/978-3-032-22730-0_22

[35] Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear dependent types for differential privacy. In ACM Symposium on Principles of Programming Languages (POPL’13). 357–370. http://dl.acm.org/citation.cfm?id=2429113 [36] Michèle Giry. 1982. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, B. Banaschewski (Ed.). Lecture Notes in Mathematics, Vol. 915. Springer Berlin Heidelberg, 68–85. doi:10.1007/BFb0092872 [37] Ruobin Gong, Erica L. Groshen, and Salil Vadhan. 2022. Harnessing the Known Unknowns: Differential Privacy and the 2020 Census. Harvard Data Science Review Special Issue 2 (jun 24 2022). https://hdsr.mitpress.mit.edu/pub/fgyf5cne. [38] Miguel Guevara. 2019. Enabling developers and organizations to use differential privacy. (5 September 2019). https://developers.googleblog.com/en/enabling-developers-andorganizations-to-use-differential-privacy/ Accessed: September 12, 2024. [39] C. Heunen, O. Kammar, S. Staton, and H. Yang. 2017. A convenient category for higher-order probability theory. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–12. doi:10. 1109/LICS.2017.8005137 [40] Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. 2022. Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL. In Functional and Logic Programming, Michael Hanus and Atsushi Igarashi (Eds.). Springer International Publishing, Cham, 57–74. [41] Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. 2022. QuasiBorel Spaces. Archive of Formal Proofs (February 2022). https://isaafp.org/entries/Quasi_Borel_Spaces.html, Formal proof development. [42] Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. 2023. Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. In 14th International Conference on Interactive Theorem Proving (ITP 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 268), Adam Naumowicz and René Thiemann (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 18:1– 18:18. doi:10.4230/LIPIcs.ITP.2023.18 [43] Yoshihiro Ishiguro and Reynald Affeldt. 2023. A Progress Report on Formalization of Measure Theory with MathComp-Analysis. In 25th Workshop on Programming and Programming Languages (PPL2023), Nagoya University, March 6–8, 2023. https://staff.aist.go.jp/reynald. affeldt/documents/measure-ppl2023.pdf Conference website: https: //jssst-ppl.org/workshop/2023/. [44] Peter Kairouz, Sewoong Oh, and Pramod Viswanath. 2015. The Composition Theorem for Differential Privacy. In Proceedings of the 32nd International Conference on Machine Learning, ICML 2015, Lille, France, 6-11 July 2015. 1376–1385. http://jmlr.org/proceedings/papers/v37/ kairouz15.html [45] Jaewoo Lee and Daniel Kifer. 2018. Concentrated Differentially Private Gradient Descent with Adaptive per-Iteration Privacy Budget. In Proceedings of the 24th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining (London, United Kingdom) (KDD ’18). Association for Computing Machinery, New York, NY, USA, 1656–1665. doi:10.1145/3219819.3220076 [46] Friedrich Liese and Igor Vajda. 2006. On Divergences and Informations in Statistics and Information Theory. IEEE Transactions on Information Theory 52, 10 (Oct 2006), 4394–4412. doi:10.1109/TIT.2006.881731 [47] Andreas Lochbihler. 2016. Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. In Programming Languages and Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 503–531. doi:10.1007/ 978-3-662-49498-1_20 [48] Lorenzo Luccioli. 2024. Formalizing information theory in Lean 4: divergences, hypothesis testing and the data processing inequality. https://amslaurea.unibo.it/id/eprint/32676/ [49] Min Lyu, Dong Su, and Ninghui Li. 2017. Understanding the sparse vector technique for differential privacy. Proc. VLDB Endow. 10, 6 (feb 14

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Conference acronym ’XX, June 03–05, 2018, Woodstock, NY

2017), 637–648. doi:10.14778/3055330.3055331 [50] The mathlib Community. 2024. API Documentation of Lean 4. https:// leanprover-community.github.io/mathlib4_docs/ Accessed: September 12, 2024. [51] Ilya Mironov. 2012. On significance of the least significant bits for differential privacy. In Proceedings of the 2012 ACM Conference on Computer and Communications Security (Raleigh, North Carolina, USA) (CCS ’12). Association for Computing Machinery, New York, NY, USA, 650–661. doi:10.1145/2382196.2382264 [52] Ilya Mironov. 2017. Rényi Differential Privacy. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 263–275. doi:10. 1109/CSF.2017.11 [53] Arjun Narayan, Ariel Feldman, Antonis Papadimitriou, and Andreas Haeberlen. 2015. Verifiable differential privacy. In Proceedings of the Tenth European Conference on Computer Systems (Bordeaux, France) (EuroSys ’15). Association for Computing Machinery, New York, NY, USA, Article 28, 14 pages. doi:10.1145/2741948.2741978 [54] Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Shinya Katsumata. 2019. Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. IEEE, 1–14. doi:10.1109/LICS.2019.8785668 [55] Tetsuya Sato and Shin-ya Katsumata. 2023. Divergences on monads for relational program logics. Mathematical Structures in Computer Science 33, 4–5 (2023), 427–485. doi:10.1017/S0960129523000245 [56] Tetsuya Sato and Yasuhiko Minamide. 2025. Differential Privacy. Archive of Formal Proofs (January 2025). https://isa-afp.org/entries/ Differential_Privacy.html, Formal proof development. [57] Tetsuya Sato and Yasuhiko Minamide. 2025. Formalization of Differential Privacy in Isabelle/HOL. In Proceedings of the 14th ACM SIGPLAN

International Conference on Certified Programs and Proofs (Denver, CO, USA) (CPP ’25). Association for Computing Machinery, New York, NY, USA, 67–82. doi:10.1145/3703595.3705875 [58] Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani. 2017. Denotational Validation of Higher-order Bayesian Inference. Proc. ACM Program. Lang. 2, POPL, Article 60 (Dec. 2017), 29 pages. doi:10.1145/3158148 [59] Sam Staton. 2017. Commutative Semantics for Probabilistic Programming. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 855–879. [60] Matías Toro, David Darais, Chike Abuah, Joseph P. Near, Damián Árquez, Federico Olmedo, and Éric Tanter. 2023. Contextual Linear Types for Differential Privacy. ACM Trans. Program. Lang. Syst. 45, 2, Article 8 (may 2023), 69 pages. doi:10.1145/3589207 [61] Jean-Baptiste Tristan. 2024. SampCert : Verified Differential Privacy. doi:10.5281/zenodo.11204806 Accessed: August 22, 2024. [62] Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, and Anindya Banerjee. 2020. Verification of ML Systems via Reparameterization. arXiv:2007.06776 [cs.LG] [63] Yu-Xiang Wang, Borja Balle, and Shiva Prasad Kasiviswanathan. 2019. Subsampled Renyi Differential Privacy and Analytical Moments Accountant. In Proceedings of the Twenty-Second International Conference on Artificial Intelligence and Statistics (Proceedings of Machine Learning Research, Vol. 89), Kamalika Chaudhuri and Masashi Sugiyama (Eds.). PMLR, 1226–1235. https://proceedings.mlr.press/v89/wang19b.html

Received 20 February 2007; revised 12 March 2009; accepted 5 June 2009

15

Related documents

• Novel assay format permitting the prolonged usenext term of regeneration-based sensor chip technology#641856
• Intelligent computer decision systems#381995
• Impermissive Bayesianism#752555
• An Itinerary in the Theory of Product Differentiation. An Interview with Jacques-François Thisse#454574
• A Bayesian Framework for Multivariate Differential Analysis#1063698