Verified Pythagorean Composition for Adaptive Cryptographic Games: Noise Flooding in Homomorphic Encryption

Verified Pythagorean Composition for Adaptive Cryptographic Games: Noise Flooding in Homomorphic Encryption Yi Lee∗

Alexandru Cojocaru†

Junyi Liu‡

Xiaodi Wu§

arXiv:2608.13846v1 [cs.CR] 14 Aug 2026

Abstract Noise flooding is a standard defense against decryption attacks on approximate homomorphic encryption, but its security proof is unusually sensitive to composition. Replacing each of q adaptive decryption answers with a statistically close simulation and applying an ordinary hybrid argument loses linearly in q. The cryptographic proof instead accumulates conditional Kullback–Leibler (KL) costs and converts to statistical distance once, giving the parameter-critical square-root loss. We machine-check this argument using Rocq and SSProve. Given any fully homomorphic encryption scheme that is approximately correct and IND-CPA secure, we formalize a reduction for every q-query IND-CPAD adversary and prove √ qn Pr[IND-CPADA = 1] ≤ β (B ) + . A,q CPA NF 2γ where n is the plaintext dimension and γ is the flooding-width multiplier. Our proof constructs a new relational program logic over SSProve semantics. Its Pythagorean judgment composes conditional KL budgets without converting them to statistical distance, and a verified trace compiler lifts a local oracle rule to arbitrary adaptive programs with a single final conversion.

1

Introduction

Ordinary encryption protects data while it is stored or transmitted, but computation typically requires exposing the plaintext. Fully homomorphic encryption (FHE) removes this boundary: a client can encrypt its data and send the ciphertexts to an untrusted server, which computes on them without the secret key and returns an encryption of the corresponding result. First envisioned in 1978 and first constructed by Gentry in 2009, FHE was a long-standing goal of cryptography [1, 2]; the LWE-based constructions that launched the modern line of efficient schemes were recognized by the 2022 Gödel Prize [3]. Modern families target complementary workloads: BGV and BFV provide packed modular arithmetic, TFHE targets Boolean computation and fast bootstrapping, and CKKS provides packed approximate numerical arithmetic [3, 4, 5, 6]. Within approximate FHE, CKKS is the dominant design and is implemented in nearly every major library offering approximate arithmetic [7]. CKKS is attractive for data-analysis and machine-learning workloads because many numerical computations can tolerate small errors. It represents values at finite precision and allows error to grow in a controlled fashion during encrypted computation, so decryption returns a value close to, rather than exactly equal to, the intended result. In some applications, however, the server can obtain decrypted results through repeated interaction with the client. An attacker who knows the inputs and the computation can then predict its mathematical result and compare that prediction with the approximate value returned ∗

Joint Center for Quantum Information and Computer Science, University of Maryland, USA. Email: ylee1228@umd.edu School of Informatics, The University of Edinburgh, United Kingdom. Email: a.cojocaru@ed.ac.uk ‡ Joint Center for Quantum Information and Computer Science, University of Maryland, USA. Email: junyiliu@umd.edu § Joint Center for Quantum Information and Computer Science, University of Maryland, USA. Email: xwu@cs.umd.edu †

1

NOISE-FLOODING INSTANTIATION Assumptions on the scheme IND-CPA security, charts, and approximate correctness

Noise-flooded construction IND-CPA and IND-CPAD games and reduction

Analysis of one decryption call Gaussian KL bound and reachable-state invariant

Adaptive replacement Replace up to q adaptively chosen calls

Checked security theorem √ βCPA (B) + qn/(2γ)

REUSABLE VERIFIED MACHINERY Discrete probability KL divergence, Pinsker, and conditionalcoordinate bounds

Pythagorean relational logic Accumulate KL costs and convert to additive error once

Discrete-Gaussian analysis Normalization, moments, and exact KL

From one call to adaptive programs Selected-call compiler and semantic correctness

Figure 1: Overview of the checked development. The upper lane specializes the reusable results in the lower lane to noise flooding and culminates in the exported security theorem. Arrows show how the mathematical and program-level results combine: orange marks assumptions, green the noise-flooding instantiation, blue reusable verified machinery, and purple the final theorem. after decryption. Li and Micciancio showed that these small discrepancies can depend on the secret key strongly enough to recover it [8]. Li and Micciancio captured the missing security guarantee with the IND-CPAD security game. It grants only restricted decryption access: the attacker may query ciphertexts produced through legitimate encryption and evaluation, and only when it already knows the mathematical result. For a perfectly correct exact scheme, such a decryption reveals nothing beyond that known result. CKKS instead reveals an approximate result, including the residual error exploited by the attack. Li, Micciancio, Schultz-Wu, and Sorrell (LMSS) subsequently showed that approximate FHE can be secured in this model by adding fresh, sufficiently wide Gaussian noise to each released result [9]. This defense, called noise flooding, masks the original secret-key-dependent error but also consumes precision, so its width must balance security against the usefulness of the decrypted result [10, 11]. The security–precision tradeoff depends critically on how the loss composes across repeated decryptions. Security proofs for adaptive cryptographic systems often reduce a global attack to a local distributional replacement: one oracle answer in the real game is replaced by a nearby simulated answer. For noise flooding, the real answer adds fresh noise around the scheme’s approximate decryption, whereas the simulated answer adds noise with the same width around the known exact result. Approximate correctness bounds the displacement between these centers. For every reachable history in which a permitted query is answered, an equal-variance discrete-Gaussian calculation then bounds the conditional KL divergence between the two answer distributions by εnf =

n , 2γ 2

where n is the noise-coordinate dimension and γ controls the flooding width [9]. An attacker may make up to q queries, choosing each one after seeing the previous answers, so the analysis must compare entire adaptive transcripts. Applying Pinsker’s inequality separately to each replacement and then adding the resulting distances with the triangle inequality gives the loss r √ εnf q n q = . 2 2γ For the sharper analysis, let P and Q be the distributions of the complete real and simulated transcripts. Because the KL bound holds conditionally after every reachable history, the KL chain rule adds the costs of the adaptively chosen answers. Pinsker’s inequality is then applied once, to the complete transcripts,

2

giving [9, 12] DKL (P ∥ Q) ≤ qεnf , r √ qn qεnf ∆(P, Q) ≤ = . 2 2γ Data processing transfers this transcript bound to the games’ output distributions and hence to their winning probabilities. Thus, for a fixed security bound, the first analysis requires flooding width growing √ linearly in q, whereas the second requires growth only as q. Because the flooding noise is added directly to the decrypted result, the sharper composition bound directly preserves numerical precision. This chain-rule composition principle predates approximate FHE. Micciancio and Walter studied cryptographic algorithms whose analyses assume access to an ideal sampler, even though a concrete implementation may only realize an approximation—for example, because it computes sampling probabilities using finite-precision floating-point arithmetic [12]. They called the resulting root-sum-of-squares behavior Pythagorean probability preservation. Thus, Pythagorean preservation is not specific to FHE: it is the general composition step connecting a one-call approximation guarantee to an adaptive computation. Although this composition step is concise on paper, it combines probability calculations, adaptive interactions with an attacker, and transformations between security games. Small omissions can be difficult to detect on paper, yet may change either the security claim or its concrete parameters. We therefore machine-check the argument. To machine-check a proof, we translate its prose and equations into a precise language understood by a specialized software system called a proof assistant. Our development uses the Rocq proof assistant together with SSProve, a Rocq library for cryptographic games. The proof remains human-written, but Rocq checks that each step follows from the stated assumptions and earlier results. When we say below that we verify a theorem, we mean that we construct such a machine-checked proof. One influential approach to machine-checking game-based security proofs represents each game as a probabilistic program. The challenger and attacker sample randomness, maintain state, and call procedures, while a proof step relates one such program to another. CertiCrypt established this codebased approach inside Coq; EasyCrypt subsequently pursued a dedicated language and greater automation [13, 14]. SSProve takes a modular approach inside Rocq: it represents games as packages that can be linked and replaced, and provides tools for comparing the procedures inside those packages [15]. Its extensibility is central to our work. We can add a new way to compare two probabilistic programs and use Rocq to prove that it gives only valid conclusions, while reusing SSProve’s existing representation of cryptographic games. This architecture fits the two levels of the LMSS proof: a reduction between complete security games and a probabilistic comparison between two implementations of a single decryption query. Our mechanization follows the two levels just described. At the cryptographic level, it checks the LMSS noise-flooding reduction under the assumptions stated below, reducing the IND-CPAD winning probability to an IND-CPA bound plus an explicit square-root loss. At the program level, it proves a reusable local-to-adaptive replacement theorem: given a conditional KL bound and a preserved invariant for one oracle call, the theorem compares complete programs containing up to q adaptively chosen calls. A verified selected-call compiler makes arbitrary SSProve adversary code compatible with this theorem by exposing the selected calls while preserving the surrounding adaptive computation. Combining the compiler with our Pythagorean judgment gives the quantitative replacement theorem. Noise flooding is the main checked application, but the replacement theorem itself does not mention FHE.

1.1

Machine-checked main theorem

Let S be an approximate-FHE scheme whose message space has local charts in Zn , let NFγ [S] be its noise-flooded transform, and let A make at most q non-failing decryption queries in the IND-CPAD game. Under the interfaces and assumptions specified in Section 2.1, the formal development constructs 3

an IND-CPA adversary BA,q and proves

√

WinProb[IND-CPADNFγ [S] (A)] ≤ βCPA (BA,q ) +

qn . 2γ

(1)

The expression βCPA is the supplied winning-probability bound for the underlying scheme. The formal theorem is given in the artifact as NoiseFloodingSecure.is_secure. The result covers adaptive oracle programs rather than adversaries prewritten as q separate query phases. Its proof isolates one lossy transition: real flooded decryption is replaced by flooding around the plaintext recorded in the challenge table. At the cryptographic level this is the single G0 → G1 hop of LMSS. The formal proof exposes this transition by opening and relinking packages, compiling calls, replacing unreachable residual decryptions, and identifying the reduction game; each of these representation changes is proved exact. The checked theorem deliberately isolates the good-execution step of the LMSS argument. It assumes deterministic decryption, approximate correctness with certainty (that is, no bad key pairs or encryptions exist), and a message space with local Zn charts. A concrete CKKS instantiation would additionally require a standard up-to-bad game hop for correctness failures and proofs that CKKS satisfies IND-CPA and the stated interface assumptions. We have not yet formalized those obligations, and therefore do not claim a verified CKKS deployment or concrete parameter set. As in SSProve generally, probabilistic polynomial time is not formalized in the Rocq semantics and remains a conventional external audit [15]. Here the standard reduction runs A once and adds oracle forwarding, table bookkeeping, and Gaussian sampling; no unusual complexity issue is hidden in the reduction.

1.2

Why a program logic?

The noise-flooding proof starts with a KL-divergence bound between two implementations of one decryption call and must end with an additive bound between two complete games containing an adaptive adversary. SSProve’s original architecture addresses this kind of local-to-global gap by connecting two proof styles: high-level equational reasoning about cryptographic packages and low-level relational reasoning about their procedures [15]. Noise flooding needs a new quantitative connection of the same kind. Concretely, an SSProve procedure is represented inside Rocq as an abstract syntax tree (AST). Its nodes record instructions to sample randomness, update state, and call procedures, but the tree is not itself a probability distribution. The probability lemmas used in the security proof instead apply to the distribution over outputs and states produced when the procedure runs. Thus a proof must connect the syntax of the game to the distributions about which its probabilistic claims are made. The conventional solution in program verification is a program logic: a collection of reusable proof rules, in a tradition dating back to Hoare logic [16]. The logic records properties of program fragments as judgments, and its rules show how these properties behave when fragments sample randomness, are run in sequence, or call procedures. Proving that these rules give correct conclusions about the program’s output distributions establishes the logic’s soundness. A relational program logic reasons about two programs at a time, making it suited to transformations between cryptographic games. Probabilistic relational program logics already underlie both EasyCrypt and SSProve [14, 15]. An ordinary approximate-equivalence judgment does not preserve the required parameter dependence. Its sequence rule adds scalar errors, so applying Pinsker at every oracle call turns a one-call cost p p ϵ/2 into q ϵ/2. Instead, we define a Pythagorean judgment, which records a tuple of conditional KL costs. Sequencing concatenates tuples, and a checked Micciancio–Walter p rule converts the accumulated tuple to additive error only once. After q calls of KL cost ϵ, this gives qϵ/2. The remaining obstacle is adaptivity: a concrete SSProve adversary is one stateful oracle program, not a syntactic list of q calls. We therefore verify a compiler that exposes selected oracle calls while preserving the surrounding control flow. Its same-package correctness theorem shows that the transformation preserves program behavior when selected and residual calls use the same implementation 4

(Theorem 5.1). Together, the judgment and compiler form a reusable interface: prove one invariantpreserving oracle rule, then obtain a whole-program additive bound for arbitrary well-typed adaptive code. Noise flooding is the first substantial application of this interface; Theorem 5.2 states the general quantitative theorem. The program logic is broader than the particular LMSS noise-flooding reduction formalized here. One direction for reuse returns to the original motivation of Micciancio and Walter: comparing an ideal sampler with a finite-precision implementation inside an adaptive cryptographic computation. A second remains within FHE and noise flooding, but moves to threshold protocols, where the secret key is shared and parties release partial decryptions across repeated, possibly adaptive interactions. Neither application is mechanized here; each would require a one-call conditional KL bound and invariant suited to its setting.

1.3

Contributions

We separate the cryptographic result from the machinery used to establish it. A verified noise-flooding reduction. We define the IND-CPA and IND-CPAD games, the noiseflooded construction, and a concrete reduction as SSProve packages. Rocq checks the single statistical game hop, its exact representation-level refinements, and the loss in Equation (1). The construction, game reduction, and adaptive statistical step are presented in Sections 2, 3 and 5.4; full game definitions and reduction pseudocode appear in Section A. A reusable Pythagorean program logic. We define additive-error and Pythagorean judgments, and prove several inference rules in Rocq. The logic combines unary invariant reasoning, direct coupling and additive-error rules, KL sampling rules, tuple-concatenating sequencing, and a final bridge to statistical distance. We discuss our program logic in Section 4. A verified selected-call compiler and local-to-adaptive theorem. We construct a trace-based compiler that exposes the first q calls to a chosen operation inside an arbitrary concrete SSProve program. We prove the transformation semantically exact when selected and residual calls use the same package. Combining the compiler with one invariant-preserving Pythagorean oracle judgment yields a whole-program p additive-error judgment with loss q ∥s∥1 /2. The compiler, exactness theorem, and quantitative replacement theorem are independent of FHE and are presented in Section 5. Probability analysis. We verify KL divergence and its finiteness obligations, Pinsker’s inequality, a conditional-coordinate preservation theorem, and the equal-variance KL formula for integer discrete Gaussians. These results provide the underlying mathematical foundations used in the logic. Their roles in the one-call Gaussian bound and the final Pythagorean conversion appear in Sections 2.2 and 4, respectively. Across these contributions, the Rocq formalization is organized so that games, assumptions, loss, compiler, and final theorem can be reviewed separately. The overview in Figure 1 makes the boundary between the reusable probability and program-logic results and their noise-flooding application explicit. We report the trusted base, distinguish inherited library assumptions from local proof obligations, and provide a verified replacement for the one unverified real-analysis lemma inherited through the current SSProve stack; Section 6 gives this mechanization audit. Our Rocq formalization is available at https://github.com/ethanlee515/Mending.

2

Construction, Security Setting, and Result

This section defines the construction and states the result proved later, explaining formalization-specific conventions as they arise. All distributions are discrete. Games return a Boolean, and WinProb[G] = 1P Pr[G = true]. We write ∆(P, Q) = 2 x |P (x) − Q(x)| for statistical distance and DKL (P ∥ Q) for KL divergence when the defining series is summable and P is absolutely continuous with respect to Q.

5

2.1

Approximate FHE and its flooded transform

CKKS introduced homomorphic arithmetic with approximate plaintext semantics [6]. LMSS subsequently gave a generic approximate-correctness formulation in which ciphertexts carry public error estimates [9]. Our formal scheme interface is a typed, executable presentation of that setting: S = (KeyGen, Enc, Eval1 , Eval2 , Dec). These algorithms are distribution-valued, and key generation is lossless: it returns with probability one. For bookkeeping, the formal model represents a ciphertext as either None, for an unsupported evaluation, or c = Some(c̄, e), pairing a ciphertext with its public error bound e ∈ N. This option wrapper belongs to the formal API, not to the cryptographic construction. Unary and binary evaluation gates suffice to describe arbitrary circuits while keeping the package interface small. Although the interface permits randomized decryption, the theorem specializes it to a deterministic value dec0 (sk, c) and assumes probability-one approximate correctness: for every encryption or evaluation output c = Some(c̄, e) having nonzero probability and representing m, we have d(dec0 (sk, c), m) ≤ e.

(2)

The artifact calls this support-level correctness; in cryptographic terms, the bound holds with probability one. Nonzero correctness error would require the additional up-to-bad hop discussed in Section 1.1. LMSS’s noise-flooding defense postprocesses approximate decryption with fresh Gaussian noise [9]. On a concrete plaintext ring, adding such noise to a plaintext is an ordinary algebraic operation. For an abstract message type M , however, a product discrete Gaussian is supported on Zn , not on M ; it cannot be used as message-valued noise without first supplying integer coordinates. Our formalization therefore packages the metric and the coordinates needed for noise flooding as one interface. The message space carries a distance d : M × M → N, and for each center a ∈ M it has maps Ia : M → Zn ,

J a : Zn → M

satisfying Ia (a) = 0,

d(a, b) = ∥Ia (b)∥∞ ,

Jb (v) = Ja (v + Ia (b)).

(3)

Here Ia (b) is the integer displacement from a to b, while Ja (v) interprets the integer displacement v as a message based at a. Thus Ja transports a distribution on Zn to a distribution on messages. The three laws say that the coordinates are centered, that their ℓ∞ norm agrees with message distance, and that changing the base point translates the integer coordinates. In particular, they let the proof compare flooding around two messages as centered and shifted Gaussians in one common copy of Zn . For γ > 0, noise flooding around x ∈ M is consequently the following single construction: Floode (x) : σe = max{1, e}γ, η ← DZn ,0,σe2 ,

(4)

return Jx (η). Here DZn ,0,σe2 is the product of n independent integer discrete Gaussians. The sampling step lives in Zn , and Jx makes its result a message; an arbitrary metric space without such maps would not support Equation (4). This proof-specific interface is easier to audit than committing the generic theorem to a concrete CKKS polynomial quotient ring. The noise-flooded transform NFγ [S] keeps key generation, encryption, and evaluation unchanged and decrypts a valid tagged ciphertext by a ← Dec(sk, c);

Floode (a).

On input None, decryption fails; SSProve represents this by a subdistribution of total weight zero. 6

We use the standard multi-query left-or-right IND-CPA experiment and the IND-CPAD experiment of Li and Micciancio [8]; their full definitions appear in Algorithms 1 to 3. For the discussion below, the essential difference is that IND-CPAD adds evaluation and restricted decryption: a decryption query is answered only when the two plaintexts recorded for that ciphertext agree. We write the assumed INDCPA bound as WinProb[IND-CPAS (B)] ≤ βCPA (B). Adversaries are well-typed SSProve oracle programs. Running time is not part of the semantics, so preservation of probabilistic polynomial time by the explicit reduction remains a separate inspection [15].

2.2

The one-query decryption replacement

The reduction compares two ways to answer a decryption query when the two recorded plaintexts agree. Fix a row that can occur with nonzero probability, c = Some(c̄, e).

Ti = (m, m, c),

Under deterministic decryption, the real and simulated answers are ODecreal (i) :

y ← Floode (dec0 (sk, c)); return Some(y),

ODecsim (i) :

y ← Floode (m); return Some(y).

(5)

Both versions perform the same bounds checks and counter updates, refuse the same queries, and abort in the same circumstances. The simulated answer needs neither sk nor b: the common plaintext m is already recorded in the table. The probability-one correctness assumption in Equation (2) gives d(dec0 (sk, c), m) ≤ e. By the change-of-basepoint law in Equation (3), the simulated answer can be expressed in the real answer’s chart by shifting the integer Gaussian by Idec0 (sk,c) (m). The distance law bounds the ℓ∞ norm of this shift by e, so each of its n coordinates has magnitude at most e. The equal-variance discrete-Gaussian identity
(ν − µ)2 DKL DZ,µ,σ2 ∥ DZ,ν,σ2 = . (6) 2σ 2 After fixing the adversary’s prior view, m, c, and e are fixed. The identity bounds the KL divergence ϵi between the two answer distributions for this call by ϵi ≤

ne2 ≤ ϵnf , 2 max{1, e}2 γ 2

ϵnf =

n . 2γ 2

(7)

This is a one-call statement conditioned on an arbitrary prior interaction history. The central problem is to preserve it across the adversary’s q adaptive queries without converting to statistical distance after each call. The underlying noise-flooding reduction is due to LMSS [9]. Our contribution is to express its assumptions through the interfaces in Section 2.1 and check the resulting adaptive reduction in Rocq. Theorem 2.1 (Checked noise-flooding reduction). Let S, its noise-coordinate interface, probability-one correctness proof, IND-CPA security interface, and γ > 0 satisfy the requirements of Section 2.1. For every IND-CPAD adversary A represented as a well-typed SSProve oracle program, and every q ∈ N, the formalization constructs an IND-CPA adversary BA,q with the required oracle interface and proves WinProb[IND-CPADNFγ [S],q (A)] p ≤ βCPA (BA,q ) + qϵnf /2 √ qn ≤ βCPA (BA,q ) + . 2γ The first inequality keeps the per-query bound ϵnf visible; substituting ϵnf = n/(2γ 2 ) from Equation (7) gives the second. Thus IND-CPA security is an assumption on S, while IND-CPAD security of its noise-flooded version is the conclusion. 7

3

The Reduction and Its Missing Link

Section 2.2 isolates the local change behind the LMSS reduction: replace ODecreal by the plaintextcentered ODecsim . The latter can be implemented without the secret key and hence inside an IND-CPA reduction. For one call, Equation (7) bounds the KL cost. We now lift that local comparison to the complete adaptive experiment.

3.1

Three games

Fix an IND-CPAD adversary A making at most q decryption queries. Consider the following games: G0 = IND-CPADNFγ [S],q (A), G1 = IND-CPADsim NFγ [S],q (A), G2 = IND-CPAS (BA,q ). Game G0 is the real experiment. Game G1 replaces the real decryption oracle by ODecsim from Equation (5). This simulated-decryption game is the intermediate game used by LMSS [9]. Game G2 runs the concrete reduction from Algorithm 4. The second transition is exact. Once decryption answers are centered at the common recorded plaintext, they no longer require the secret key or the hidden challenge bit. The reduction can therefore forward encryption queries to its IND-CPA oracle, perform evaluation and table bookkeeping locally, and simulate every permitted decryption query with the same distribution as G1 . Consequently, WinProb[G1 ] = WinProb[G2 ]. The entire cryptographic proof is thus the chain √ qϵnf /2 0 → G2 . G0 −−−−−→ G1 −

(8)

The first arrow is the only paid hop. Together with the assumed IND-CPA bound for G2 , it immediately implies Theorem 2.1.

3.2

The tempting one-line proof

Equation (7) bounds the conditional KL cost of every reachable decryption query whose two recorded plaintexts agree by ϵnf . The two games agree when those plaintexts differ and when an assertion fails, so those branches spend no budget. It is tempting to finish in one sentence: apply the KL chain rule over the q decryption interactions, obtain total KL cost qϵnf , and apply Pinsker once. This gives p ∆(G0 , G1 ) ≤ qϵnf /2. (9) This is the KL-composition argument used by LMSS [9]. A machine-checked proof must identify the relevant conditional distributions and establish the one-call bound after every adversarially chosen history.

3.3

Where adaptivity enters

The adversary’s decryption calls do not form a fixed product experiment. After seeing an answer, A may change its state, choose a different oracle, or decide whether and where to make its next decryption query. In SSProve, A is one stateful program with calls embedded in its control flow, not a list of q pre-existing query phases. Thus “the first q decryption calls” is a semantic notion, and the conditional KL bound must hold after every reachable history. 8

The proof also depends on a state invariant Φ relating the real and simulated executions. It records initialized, good keys; agreement of their public data and hidden challenge bits; validity of the challenge table under encryption and evaluation; and agreement of the decryption counters. In particular, for every reachable row (m0 , m1 , c) with c = Some(c̄, e), the plaintext on the selected branch b satisfies d(dec0 (sk, c), mb ) ≤ e. Initialization establishes Φ, while encryption, evaluation, and the deterministic prefix of decryption preserve it. This is what makes the one-call KL calculation available after an arbitrary adaptive history. A machine-checked proof of Equation (9) therefore needs a bridge with three properties: 1. it retains conditional KL costs instead of converting each call to statistical distance; 2. it exposes successive calls of an arbitrary adaptive oracle program; and 3. it threads Φ through the exposed calls. Section 4 develops the Pythagorean judgment and invariant rules. Section 5 verifies the selected-call compiler and proves the generic local-to-adaptive theorem independently of FHE. The instantiation in Section 5.4 combines them to derive the paid arrow in Equation (8).

4

A Program Logic for Adaptive Games

SSProve combines high-level algebraic reasoning about packages with a relational program logic for their low-level procedures [15]. Its central bridge turns per-procedure exact judgments into perfect indistinguishability of packages. We retain that two-level architecture but add the quantitative judgments needed by noise flooding: they carry conditional KL costs through program composition and convert them to additive error only once. This section develops those judgments independently of the FHE instantiation. The verified compiler in Section 5 then lifts the resulting one-call rule to complete adaptive oracle programs. The development introduces no new programming language and takes no new logic rules as axioms. It defines semantic judgments over SSProve’s existing semantics, then verifies the soundness of every rule below. The Pythagorean judgment retains the conditional KL information required by Section 3.2, while unary Hoare reasoning maintains the invariant from Section 3.3. An additive-error judgment records the ordinary game-hop bound after the final conversion. We use SSProve’s existing language of typed oracle programs, packages, heaps, linking, and discrete subdistribution semantics; Appendix B recalls the precise fragment used here.

4.1

Completed semantics and three judgments

Because SSProve programs may fail, their denotations are subdistributions and may have weight below one. For a subdistribution µ on X, define its completion on X ∪ {⊥} by X µ(x). Comp (µ) (x) = µ(x), Comp (µ) (⊥) = 1 − x

Completion makes assertion failure observable. Without this, it becomes tedious (and sometimes tricky) to write down couplings for subdistributions and then estimate the probabilities of postconditions. The unary judgment ⊨ Hoare{P } c {Q} is the standard Hoare triple over the SSProve code. It states that whenever the precondition P is satisfied, the postcondition Q is satisfied with probability one. The additive-error judgment ⊨ AE{P } cL ≈δ cR {Q} 9

and its inference rules are heavily inspired by EasyCrypt style “up-to-bad” arguments. It states that, from any pair of initial configurations satisfying P , the completed outputs of cL and cR admit a coupling in which Q fails with probability at most δ. For equality postconditions, this is the ordinary statisticaldistance bound. Unlike EasyCrypt, SSProve allows its users to supply soundness proofs; here we verify consequence, sequencing with loss δ1 + δ2 , triangle, projection, and direct-coupling rules. We next present our Pythagorean judgment formally. Definition 4.1 (Pythagorean judgment). Let cL : XL → code(Y ) and cR : XR → code(Y ), and let s = (s1 , . . . , sk ) be a nonempty tuple of real numbers. For a configuration ρ = (x, m), write JcK⊥ ρ = Comp (Jc(x)K(m)), and let Ω = (Y × M) ∪ {⊥} be the completed output/heap space. We write ⊨ Pyth{P } cL ≈s cR {Q} (10) if every si is nonnegative and, for every pair ρL = (xL , mL ) and ρR = (xR , mR ) satisfying P (ρL , ρR ), there exist weight-one joint transcript distributions P, Q ∈ Distr(Ωk ) such that

Pk = JcL K⊥ ρL , Qk = JcR K⊥ ρR , ∀i ∈ {1, . . . , k}, ∀a ∈ Ωi−1 . ∀i ∈ {1, . . . , k}, ∀a ∈ Ω

i−1

finiteKL(Pi | a, Qi | a) ,

. DKL (Pi | a ∥ Qi | a) ≤ si ,

∀z ∈ suppJcL (xL )K(mL ).

Q(z),

∀z ∈ suppJcR (xR )K(mR ).

Q(z).

This definition captures the Micciancio–Walter [12] Pythagorean prerequisites for KL divergence. The transcript is semantic rather than a list of syntactic sampling sites: it may record a whole program fragment as one coordinate, or expose multiple coordinates for composition. This judgment deliberately stores more information than an immediate statistical-distance bound. Its sequence rule concatenates tuples (i.e. s ++ s0 ) rather than adding square roots, allowing one nonlinear conversion after the full adaptive transcript has been constructed.

4.2

Core proof rules

Figure 2 shows the rules that drive the generic development. They are schematic and suppress most SSProve typing, full-mass, support, and heap side conditions; the artifact contains their concrete statements. For completeness, Figure 4 in the appendix collects every rule used by the noise flooding security analysis, including the Hoare, additive-error, derived Gaussian, and compiler rules omitted here. KL-SAMPLE embeds a distribution-level KL bound as a program judgment. PYTH-REFL relates a program to itself at zero cost. PYTH-SEQ is the essential rule: its proof constructs a joint transcript for semantic bind and proves conditional bounds for both valid and zero-mass prefixes. The development also contains a shared-continuation rule, consequence rules, variants for fully linked programs, and the additive-error rules mentioned above. The mixed Hoare/Pythagorean rules have been useful in practice. Deterministic prefixes, table operations, other oracle calls, and postprocessing are proved to preserve an invariant with the unary Hoare logic and inserted as zero-cost coordinates in the Pythagorean judgment. Only the sampling fragment whose distribution changes consumes KL budget. In the noise-flooding application of Section 5.4, this decomposition produces the tuple (0, ϵnf , 0).

10

finiteKL(DL , DR ) DKL (DL ∥ DR ) ≤ ϵ weight(DL ) = weight(DR ) = 1 ∀x ∈ supp(DL ) ∪ supp(DR ), Q(x) KL-SAMPLE ⊨ Pyth{P } x ← DL ≈[ϵ] x ← DR {Q} P =⇒ xL = xR ∧ mL = mR 0 ≤ si for every i PYTH-REFL ⊨ Pyth{P } c ≈s c {Q} ⊨ Pyth{P } cL ≈s cR {M } ⊨ Pyth{M = } kL ≈t kR {Q} PYTH-SEQ ⊨ Pyth{P } (x ← cL ; kL (x)) ≈s++t (x ← cR ; kR (x)) {Q} ⊨ Hoare{P } c {M } ⊨ Pyth{M = } kL ≈s kR {Q} SHARED-PREFIX ⊨ Pyth{P } (x ← c; kL (x)) ≈[0]++s (x ← c; kR (x)) {Q} ⊨ Pyth{P } cL ≈s cR {Q} MICCIANCIO–WALTER ⊨ AE{P } cL ≈√∥s∥ /2 cR {oL = oR } 1

Figure 2: Representative checked rules. Here M = requires equal intermediate values and heaps satisfying M , and ++ denotes tuple concatenation. The Rocq theorems additionally expose further typing, support, invariant, and nonnegativity premises.

4.3

The Micciancio-Walter Probability Lemma

The MICCIANCIO–WALTER rule in Figure 2 rests on the following distribution-level theorem. Let P, Q be joint distributions on Ωk , and write Pi | a for coordinate i conditioned on prefix a ∈ Ωi−1 . Theorem 4.2 (Conditional-coordinate preservation). Suppose P, Q have weight one and, for every coordinate i and prefix a, the conditional KL divergence is finite and DKL (Pi | a ∥ Qi | a) ≤ si , Then their final-coordinate marginals satisfy

s

∆(Pk , Qk ) ≤

si ≥ 0.

Pk

i=1 si

2

.

At paper level, the proof expands joint mass as prefix mass times conditional mass P and groups the log likelihood ratio by coordinate. The resulting chain bound gives DKL (P ∥ Q) ≤ i si . Pinsker bounds the transcript distance, and data processing gives the displayed final-marginal bound. The Rocq proof makes explicit absolute continuity, conditional zero-mass prefixes, summability of positive and negative parts, and exchanges between finite coordinate sums and countable support sums. We further discuss this proof in the Appendix Section D. Our MICCIANCIO–WALTER rule instantiates this theorem with the transcripts from Definition 4.1, then uses maximal coupling to obtain the additive-error equality judgment. As with all of our inference rules, we verify it to be sound with respect to SSProve’s program semantics.

4.4

A derived discrete-Gaussian rule

For center µ ∈ Z and σ > 0, we denote the discrete Gaussian distribution by DZ,µ,σ2 (x) = P

exp(−(x − µ)2 /(2σ 2 )) . 2 2 z∈Z exp(−(z − µ) /(2σ ))

The development proves normalization, translation invariance of the normalizer, summability, the centered first moment, full support, and the equal-variance KL identity in Equation (6). The calculation 11

expands the logarithm of the ratio; equal variances cancel both normalizers, and symmetry of the centered distribution cancels the linear moment. We again defer the proof details until Section D. These facts yield a reusable program rule for vector sampling. If u, v ∈ Zn , σ > 0, and every coordinate satisfies (vi − ui )2 ≤ ϵ, 2σ 2 then the n-fold product sampler satisfies a Pythagorean judgment with budget [nϵ]. The analysis first constructs an n-coordinate transcript, proves the scalar bound coordinatewise, and then transports and aggregates it into the program-level sampling rule. The noise-flooding proof instantiates ϵ = 1/(2γ 2 ), obtaining ϵnf = n/(2γ 2 ) without introducing any unverified assumptions.

4.5

Why the extra judgment is necessary

The additive-error layer remains essential for exact hops, up-to-bad arguments, and the final triangle calculation. Its ordinary sequence rule, p however, maps δ1 , δ2 to δ1 + δ2 . Applying Pinsker inside each decrypt p proof would therefore pay q ϵnf /2. The Pythagorean layer delays that nonlinear conversion and obtains qϵnf /2. It provides a verified relational interface for carrying parameter-critical KL information across stateful program composition.

5

A Verified Compiler for Adaptive Oracle Programs

The rules above compose a sequence of sampling operations. An oracle program does not provide such a sequence: the location and arguments of its next call may depend on previous answers. Our compiler is the verified adapter between these views. It exposes a bounded number of calls to one selected operation without restricting the surrounding program’s control flow, and it comes with both a same-package correctness theorem and a generic quantitative replacement theorem.

5.1

A trace-based selected-call transformation

Given a program A and a chosen operation p, a paper proof can simply say: run A until its next call to p, answer that call, and resume. In SSProve, the code after a call is represented by a Rocq function from the answer to the rest of the program. Such arbitrary functions cannot be serialized into SSProve program data. The compiler therefore records a trace of the intervening calls, heap operations, and samples. When it reaches p, it returns the query without executing the call. The driver obtains an answer from a chosen implementation Ps , adds it to the trace, replays the recorded results through A to recover the code after the call, and repeats this process up to q times. Write Exposeq (A, p; Ps ) for the raw-code transformation that exposes the first q calls made by A to operation p and resolves them with Ps . Its factoring phase is trace-valued, but replay restores the residual program, so the complete transformation has the same result type as A. Write Compileq (A, p; Ps , Pr ) for Exposeq (A, p; Ps ) linked with residual package Pr .

5.2

Same-package correctness

The transformation inserts trace bookkeeping, so before linking its syntax differs from that of A. If both the exposed calls and the residual calls are implemented by P , however, each call receives the same answer as in the original linked program, and trace replay reconstructs the same remaining code. The compiler therefore preserves behavior in the same-package case. Theorem 5.1 (Same-package compilation). Subject to code and package validity and the presence of the selected operation, for every initial heap, Compileq (A, p; P, P ) have identical SSProve output/heap semantics. 12

and

Link(A, P )

The proof is an induction over the selected-call traversal. At each step, the recorded result is supplied to the corresponding continuation of the original program, while validity rules out malformed traces. Consequently, the compiled and original programs induce the same output–heap distribution.

5.3

A generic local-to-adaptive replacement theorem

The following theorem is the main program-logic bridge. Theorem 5.2 (Replace q calls). Let PI synchronize equal operation inputs and equal heaps satisfying I. Suppose two implementations P, P 0 of an operation p satisfy the one-call Pythagorean judgment ⊨ Pyth{PI } P.p ≈s P 0 .p {I} for a nonnegative tuple s, preserve I, and meet the compiler’s typing, footprint, and memory-separation conditions. For every concrete SSProve program A, replacing its first q selected calls yields ⊨ AE{PI } Compileq (A, p; P, P ) Compile (A, p; P 0 , P ) {oL = oR }, ≈√ qksk1 /2

q

Proof sketch. We first show that Compileq (A, p; P, P ) and Compileq (A, p; P 0 , P ) satisfy the expected Pythagorean judgment with q concatenated copies of the tuple s, by induction on q and the Pythagorean sequence rule. Each exposed call contributes s and preserves the invariant I. After q calls, the accumulated tuple has norm q ∥s∥1 ; MICCIANCIO–WALTER is applied once, giving the desired additive error bound. The theorem is generic in the program, packages, selected oracle, invariant, and budget tuple. The noise-flooding game supplies only the one-call premise proved in Section 5.4; the program logic and compiler then handle adversarial control flow. Combined with Theorem 5.1, this is our quantitative counterpart of SSProve’s local relational reasoning for package indistinguishability.

5.4

Instantiating the compiler for noise flooding open

We now instantiate the generic machinery to prove the missing arrow in Equation (8). Let CA be the adversary-facing IND-CPAD game code before its oracle implementations are linked; its encryption, evaluation, and decryption calls remain unresolved. Let Preal implement the real encryption, evaluation, and flooded-decryption oracles, and let Psim differ only by flooding around the common recorded plaintext when the row’s two plaintexts agree. The selected decryption body factors into a deterministic prefix, one Gaussian sample, and deterministic postprocessing. The invariant Φ from Section 3.3 gives d(dec0 (sk, c), m) ≤ e on every reachable row whose recorded plaintexts agree. Translation of charts by Equation (3) puts the two answer distributions over the same coordinate space. Applying Equation (6) in n coordinates with σe = max{1, e}γ yields the following local judgment. Lemma 5.3 (One-call replacement). For any decryption input and paired heaps satisfying Φ, the real and simulated decryption bodies satisfy a Pythagorean relational judgment with budget tuple n (0, ϵnf , 0), ϵnf = 2 , 2γ and restore Φ. The zero entries record the shared prefix and postprocessing. Branches with differing recorded plaintexts, as well as assertion-failing branches, agree exactly. Applying Theorem 5.2 to Lemma 5.3 concatenates one such tuple for each of the first q decryption calls, preserving all dependencies between queries. The MICCIANCIO–WALTER rule is then invoked once, after the accumulated KL budget is qϵnf , proving p ∆(G0 , G1 ) ≤ qϵnf /2. 13

Data processing projects completed output/heap pairs to the returned Boolean. This proves Equation (9). From games to program representations. The Gi in Equation (8) are complete experiments: the adversary has already been linked to its oracle implementations, so no unresolved calls remain. This is the usual cryptographic view of a game, but it hides the program structure needed by Theorem 5.2. The formal proof therefore makes the linking and call-compilation steps explicit. For selected-call implementation Ps and residual implementation Pr , write open

H(Ps , Pr ) = Compileq (CA

, ODec; Ps , Pr ).

Then H0 = G0 , open

H1 = Link(CA

, Preal ),

H2 = H(Preal , Preal ), H3 = H(Psim , Preal ), H4 = H(Psim , Psim ), open

H5 = Link(CA

, Psim ),

H6 = G2 . This is an implementation-level factorization of the two arrows in Equation (8), not seven cryptographic hybrids: H0 , H1 , H2 are real-oracle representations of G0 ; H3 , H4 , H5 are simulated-oracle representations of G1 ; and H6 is the reduction game G2 . Rocq verifies √ qϵnf /2 0 0 0 0 0 → H4 − H0 − → H5 − → H1 − → H6 . (11) → H2 −−−−−→ H3 − Here H0 = H1 unfolds package linking, and H1 = H2 is same-package compiler correctness. The single paid step H2 → H3 is the application above. For H3 = H4 , the shared counter ensures that any residual decryption call after the q selected entries assertion-fails on both sides. The equality H4 = H5 removes the compiler using Theorem 5.1. Finally, H5 → H6 relates the simulated IND-CPAD presentation to the concrete IND-CPA reduction by an exact heap invariant; the artifact factors this relation through auxiliary linked programs. Collapsing the zero-cost equalities in Equation (11) recovers the three-game chain in Equation (8); only H2 → H3 changes a distribution. Triangle composition of Equation (11), followed by the assumed IND-CPA bound at H6 , proves Theorem 2.1.

6

Mechanization and Trusted Base

The artifact contains 27,987 lines of Rocq. Since our Rocq development is heavily AI-assisted, this line count does not accurately reflect our engineering effort. The overview in Figure 1 separates the application-specific security argument from the reusable probability and program-logic results. The mechanization contains a few layers. The scheme layer defines encryption games and the noiseflooded transform. The probability layer develops facts about countable discrete distributions, without reference to programs. The logic layer lifts those facts to SSProve code. The compiler layer implements the trace transformation and derives the generic adaptive replacement rule. Finally, the security layer instantiates the reusable logic and compiler with the decryption invariant, constructs the IND-CPA reduction, and composes the exact and quantitative game transitions. The top-level result is a functor over precisely the scheme, chart, probability-one correctness, IND-CPA security, and flooding-parameter interfaces described in Section 2.1; probability lemmas and program rules are proved dependencies.

14

6.1

Formalization of judgments and rules

We follow SSProve’s convention and engineering framework: pure computation is embedded in Rocq, while probabilistic and stateful effects are represented by SSProve’s free-monadic program syntax, packages, heaps, and linking operations [15]. The new logic does not extend Rocq with a primitive judgment or a collection of trusted proof rules. Judgments are formalized as ordinary Rocq propositions over the denotation Pr_code, and inference rules are lemmas which prove such judgments. For example, the exact definition of the additive-error judgment is shown below. Its types range over SSProve programs and heaps; complete adds an explicit outcome for missing subdistribution mass. Definition additiveErrorJudgment {inL_t inR_t outL_t outR_t : ord_choiceType} 59 (progL : inL_t -> raw_code outL_t) 60 (progR : inR_t -> raw_code outR_t) 61 (pre : pred ((inL_t * heap) * (inR_t * heap))) 62 (post : pred (option (outL_t * heap) * option (outR_t * heap))) 63 (ε : R) : Prop := 64 0 <= ε /\ 65 ∀ memL memR xL xR, pre ((xL, memL), (xR, memR)) → 66 let out1 := Pr_code (progL xL) memL in 67 let out2 := Pr_code (progR xR) memR in 68 ∃ d, coupling d (complete out1) (complete out2) ∧ 69 \P_[ d ] post >= 1 - ε. 57 58

Thus, for every related pair of inputs and initial heaps, the proposition requires a coupling of the completed output-and-heap distributions in which the postcondition holds with probability at least 1 − ε. The Pythagorean judgment is encoded in the same style. For each related input pair it existentially quantifies two full transcript distributions, requires their final marginals to equal the two completed program denotations, and requires their supports to satisfy the postcondition. Its predicate pythDist additionally imposes full mass and the coordinatewise conditional-KL bounds from Definition 4.1. To place every result type in one transcript space, the Rocq definition injectively encodes typed output/heap pairs in nat * heap and represents ⊥ by None. The rules in Figure 2 are proved implications between these definitions. For instance, the source-level statement of the final KL-to-additive-error bridge is: Lemma MicciancioWalterRule {ℓ : nat} 531 {inL_t inR_t out_t : choice_type} 532 (progL : inL_t -> raw_code out_t) 533 (progR : inR_t -> raw_code out_t) 534 (pre : pred ((inL_t * heap) * (inR_t * heap))) 535 (post : pred (out_t * heap)) 536 (s : (ℓ.+1).-tuple R) : 537 ⊨Pyth ⦃ pre ⦄ progL ≈( s ) progR ⦃ post ⦄ -> 538 let delta := pythagorean_tv_bound s in 539 ⊨AE ⦃ pre ⦄ progL ≈( delta ) progR ⦃ 540 fun outs => 541 let '(outL, outR) := outs in 542 outL == outR ⦄. 529 530

pP Here pythagorean_tv_bound s is i si /2. Its proof applies the verified probability theorem to the transcript witnesses, projects to their final marginals, and invokes the completed-distribution coupling theorem. The sampling, sequencing, mixed Hoare/Pythagorean, and compiler rules have the same status: each is a Rocq lemma proved from the program semantics. Consequently, a Rocq kernel check of the security theorem also checks the soundness chain from the distribution lemmas through the program judgments.

6.2

Compiler implementation and correctness

Figure 3 shows the traversal over SSProve’s raw_code syntax. Its result pairs the trace with a status: inl carries the encoded input of a selected call, whereas inr carries the final output of a program that 15

Fixpoint run_until_next_call_aux {T : choice_type} (prog : raw_code T) (fn : ident) ,→ (trace : trace_t) : 167 raw_code suspended_program := 168 match prog with 169 | ret v => ret (inr v, pack_trace trace) 170 | opr o x k => 171 let '(f, _) := o in 172 if f == fn then 173 ret (inl (pickle x), pack_trace trace) 174 else ( 175 y ← op o ⋅ x ;; 176 run_until_next_call_aux (k y) fn (rcons trace (call_entry (pickle y))) 177 ) 166

Figure 3: Scanning for the next call to fn: inl reports its encoded input, while inr reports program termination. terminated first. A nonselected call is executed, its result is appended to the trace, and traversal continues; heap operations and samples are handled analogously. The outer driver answers a discovered call, records the answer, and repeats. After the requested calls, trace replay reconstructs the remaining code, so the complete transformation has the original result type. The same-package correctness result is Theorem 5.1, whose Rocq theorem is compile_calls_correct. It proves equality of program semantics by induction over traversal and trace replay. The separate quantitative result is Theorem 5.2. Its call induction lifts the one-call Pythagorean judgment through the trace transformation and accumulates q copies of its KL-cost tuple; compileRule then performs the single final Micciancio–Walter conversion. The COMPILE rule in Figure 4 records its complete security-facing premises. Thus both semantic compiler correctness and adaptive quantitative replacement are checked consequences of SSProve syntax and semantics.

6.3

Probability formalization

The probability development works over MathComp’s countable discrete distributions, rather than restricting the Gaussian argument to finite support. It defines KL finiteness as absolute continuity together with summability of the KL integrand, proves Pinsker’s inequality, and proves the conditionalcoordinate chain bound used in Theorem 4.2. It also constructs completion and maximal couplings, so that a distribution-level total-variation bound yields the program-level proposition above. The distributions used here, notably the discrete Gaussians, have countably infinite support. Consequently, the KL chain rule involves infinite series. A paper proof may leave their convergence implicit; the formalization must establish it before decomposing transcript KL into conditional KL costs. It also treats histories of probability zero explicitly. These results yield the chain bound used in the square-root composition argument. For the one-call bound, the development also proves that the discrete Gaussian is normalized and has full support, that its normalizer is invariant under integer shifts, and that its centered first moment is zero. These facts yield the exact equal-variance KL identity in Equation (6) and discharge the Gaussian sampling rule. Further theorem statements and proof structure appear in Section D.

6.4

The checked theorem

At the application boundary, the functor defines the concrete reduction BA,q and makes the assumed IND-CPA bound and the statistical loss explicit: 530 531 532 533

Definition security_bound (A : nom_package) (max_queries : nat) := let B := ind_cpa_reduction A max_queries in IndCpaSecurity.security_bound B + security_loss dim max_queries gaussian_width_multiplier.

16

After proving that the constructed reduction has the IND-CPA adversary interface and deriving the completed-output inequality, the development exports the following theorem. 1953 1954 1955 1956

Theorem is_secure (A : nom_package) max_queries : Package IndCpaDSim.IndCpadAdv_import IndCpaDSim.IndCpadAdv_export A -> IndCpadGame.winning_probability max_queries A <= security_bound A max_queries.

The premise says that A is a well-typed package with the required IND-CPAD adversary interface. Unfolding security_bound and security_loss gives exactly Theorem 2.1; in particular, the right-hand √ term is the assumed IND-CPA winning-probability bound for the constructed reduction plus qn/(2γ). This source statement also makes clear where the theorem boundary lies: scheme structure, charts, probability-one correctness, IND-CPA security, and positivity of γ enter through the enclosing functor, whereas reduction validity, the discrete-Gaussian calculation, compiler correctness, and logic soundness have already been proved.

6.5

Reproducibility

The complete artifact is available at https://github.com/ethanlee515/Mending. The complete artifact checks with Rocq 9.0.1, rocq-ssprove development version at commit c6d7d4bc3a, MathComp Analysis 1.16.0, and MathComp algebra tactics 1.2.7. In a fresh switch on the authors’ machine, a clean build took about six minutes with four parallel jobs; this is a single observation for reviewer planning, not a performance claim. The manuscript’s Rocq listings are refreshed from the checked sources during its build, so the displayed propositions and theorem statements do not silently diverge from the artifact.

6.6

Trusted computing base

The trusted base includes the Rocq kernel and standard library; MathComp, MathComp Analysis, and their real-number/classical infrastructure; and SSProve’s program, heap, package, linking, and subdistribution semantics. The scheme, chart, correctness, parameter, and IND-CPA interfaces from Section 2.1 are theorem parameters and must be discharged by a concrete instantiation. The new KL, Gaussian, relational, compiler, and game-hop results contain no local Admitted. The installed dependency graph nevertheless reports MathComp Analysis’s __admitted__interchange_psum: current SSProve distribution semantics are built on these MathComp definitions and reach the upstream unproven lemma [15]. This is an inherited assumption, not an unproven axiom introduced by our security development. We independently discharge the mathematical obligation. The artifact proves the same statement as interchange_psum_proved; Print Assumptions for this replacement reports only the usual extensionality and choice principles and not the admitted upstream lemma. The proof has since been merged to MathComp Analysis’s development branch, via math-comp/analysis#2007, for inclusion in the 1.17.0 release. Before this patch eventually reaches SSProve, Print Assumptions for the top-level theorem will continue to display the admitted lemma. Besides library and classical assumptions, Print Assumptions for an instantiated theorem reports the concrete scheme, chart, correctness, and IND-CPA interfaces, together with positivity of the discreteGaussian width multiplier γ. It does not report any program-logic rule, compiler correctness theorem, or discrete-Gaussian KL identity: these are verified inside the development. Selected definitions of the scheme interface, games, transform, and reduction remain in Section E. Together with the source-level theorem above, they expose the small specification surface on which a cryptographic audit should concentrate; the Rocq kernel checks that the remaining proof terms connect that surface by the argument in Section 3. As in SSProve and EasyCrypt, running time is not part of the program semantics and must be inspected separately [14, 15]. Here the reduction runs the adversary once, forwards its oracle calls, and adds table operations and discrete-Gaussian sampling.

17

7

Related Work

Approximate-FHE attacks and defenses. Li and Micciancio identified the secret-dependent approximationerror channel in CKKS-style decryption [8]. LMSS introduced the IND-CPAD formulation and used differential-privacy and noise-flooding techniques to recover security under explicit parameter conditions [9]. Subsequent work has sharpened the practical precision tradeoff [10] and revisited concrete noise-flooding parameters [11]. Attacks against exact FHE at aggressive parameters show that decryptionquery security is not confined to approximate schemes [17]. Our contribution is neither a new attack nor a better concrete parameter set: it machine-checks an existing reduction and the square-root composition mechanism on which such parameters rely. Mechanized game-based cryptography. SSProve combines state-separating package algebra with a probabilistic relational program logic in Rocq and validates the framework on encryption, KEM–DEM, and sigma-protocol case studies [15]. Its central bridge lifts invariant-preserving exact judgments for individual procedures to perfect indistinguishability of packages. Our result follows the same securityfacing pattern at a different quantitative boundary: it lifts a conditional-KL judgment for one oracle implementation to additive indistinguishability of a complete adaptive program. We retain SSProve’s syntax, package algebra, heaps, linking, and subdistribution semantics, while adding judgments and a selected-call compiler. Recent Nominal-SSProve work makes package state separation intrinsic and reports errors found in an ElGamal mechanization [18]; a further development mechanizes query-counting, multi-instance, and nested hybrid arguments [19]. Those results address exact package composition and general hybrid structure. Our compiler instead preserves an adaptive sequence of conditional KL costs and derives a sublinear statistical-distance loss. EasyCrypt is another popular framework for game-based cryptographic proofs. Adversaries are treated as opaque modules, and reflection techniques [20] can be used to extract the adversary’s semantics. Our abstraction boundary differs because SSProve adversaries are concrete program syntax: the verified trace compiler factors selected calls before the replacement theorem is applied. It is not immediately clear whether EasyCrypt’s reflection machinery suffices to formalize the FHE sub-linear security bound. We leave this matter as another interesting open question. Approximate relational logics. Approximate relational Hoare logics and approximate liftings were developed largely for differential privacy [21, 22]. They support rich (ε, δ) reasoning, but their standard sequential rules add privacy or additive-error parameters. One can instantiate general f -divergence machinery with KL divergence. The issue here is where the nonlinear conversion occurs: applying Pinsker at each command boundary loses linearly. Our semantic transcript judgment exposes conditional KL budgets to its sequence rule, concatenates them, and converts only at the final marginal. The compiler then makes that rule applicable to adaptive oracle syntax. The resulting logic is deliberately specialized to completed discrete semantics and the game-based additive conclusion used by noise flooding; it is not a general replacement for differential-privacy logics.

8

Conclusion and Future Works

Our formalization deliberately factors correctness failures from the quantitative noise-flooding argument. Its probability-one hypotheses prove the good-execution case. For an imperfectly correct FHE such as CKKS, one more standard up-to-bad game hop must be formalized before instantiation, and the probability of generating “bad” key pairs and encryptions must be carefully accounted for. The chart interface from Equation (3) also remains abstract. A concrete CKKS instantiation must connect its plaintext ring and norm to those distance-and-translation laws. Keeping that obligation separate makes the generic reduction easier to audit, but does not discharge it. Modulo the above proof engineering items, we have formally verified the central LMSS game hop [9]. That is, an IND-CPA and approximately correct FHE scheme can be made IND-CPAD through noise flooding. The natural next step then, is to verify that the CKKS scheme is indeed both IND-CPA and approximately correct. That will certainly come with its own set of other interesting challenges. For 18

instance, such an effort will no doubt contend with the use of randomized versus deterministic rounding, as well as the (difficult to formalize) heuristics involved in the deterministic case as found “in the wilds”.

Acknowledgments Y.L., J.L., X.W. are partially supported by the National Science Foundation grant CCF-1942837 (CAREER), CCF-2330974, and a Sloan Research Fellowship. A.C. acknowledges support from the National Science Foundation grant CCF-1813814, from the AFOSR under Award Number FA9550-20-1-0108 and from the Quantum Advantage Pathfinder project. OpenAI Codex was used to draft prose throughout this manuscript. The Rocq development was also substantially AI-assisted. Both have been audited and revised by the authors accordingly.

References [1] R. L. Rivest, L. Adleman, and M. L. Dertouzos, “On data banks and privacy homomorphisms,” in Foundations of Secure Computation. Academic Press, 1978, pp. 169–180. [2] C. Gentry, “Fully homomorphic encryption using ideal lattices,” in Proceedings of the 41st Annual ACM Symposium on Theory of Computing. ACM, 2009, pp. 169–178. [3] ACM SIGACT and EATCS, “The 2022 gödel prize,” 2022. [Online]. Available: //sigact.org/prizes/g%C3%B6del/citation2022.html

https:

[4] J. Fan and F. Vercauteren, “Somewhat practical fully homomorphic encryption,” Cryptology ePrint Archive, Paper 2012/144, 2012. [Online]. Available: https://eprint.iacr.org/2012/144 [5] I. Chillotti, N. Gama, M. Georgieva, and M. Izabachène, “TFHE: Fast fully homomorphic encryption over the torus,” Journal of Cryptology, vol. 33, no. 1, pp. 34–91, 2020. [6] J. H. Cheon, A. Kim, M. Kim, and Y. Song, “Homomorphic encryption for arithmetic of approximate numbers,” in International conference on the theory and application of cryptology and information security. Springer, 2017, pp. 409–437. [7] J. Takeshita, N. Koirala, C. McKechney, and T. Jung, “HEProfiler: An in-depth profiler of approximate homomorphic encryption libraries,” Journal of Cryptographic Engineering, vol. 15, no. 14, 2025. [8] B. Li and D. Micciancio, “On the security of homomorphic encryption on approximate numbers,” in Annual International Conference on the Theory and Applications of Cryptographic Techniques. Springer, 2021, pp. 648–677. [9] B. Li, D. Micciancio, M. Schultz-Wu, and J. Sorrell, “Securing approximate homomorphic encryption using differential privacy,” in Annual International Cryptology Conference. Springer, 2022, pp. 560–589. [10] A. Costache, B. R. Curtis, E. Hales, S. Murphy, T. Ogilvie, and R. Player, “On the precision loss in approximate homomorphic encryption,” in International Conference on Selected Areas in Cryptography. Springer, 2023, pp. 325–345. [11] F. Bergamaschi, A. Costache, D. Dachman-Soled, H. Kippen, L. LaBuff, and R. Tang, “Revisiting the security of approximate fhe with noise-flooding countermeasures,” in IACR International Conference on Public-Key Cryptography. Springer, 2025, pp. 102–134.

19

[12] D. Micciancio and M. Walter, “Gaussian sampling over the integers: Efficient, generic, constanttime,” in Advances in Cryptology–CRYPTO 2017: 37th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 20–24, 2017, Proceedings, Part II 37. Springer, 2017, pp. 455–485. [13] G. Barthe, B. Grégoire, and S. Zanella Béguelin, “Formal certification of code-based cryptographic proofs,” in Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2009, pp. 90–101. [14] G. Barthe, B. Grégoire, S. Heraud, and S. Zanella Béguelin, “Computer-aided security proofs for the working cryptographer,” in Advances in Cryptology—CRYPTO 2011, ser. Lecture Notes in Computer Science, vol. 6841. Springer, 2011, pp. 71–90. [15] C. Abate, P. G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Hriţcu, K. Maillard, and B. Spitters, “Ssprove: A foundational framework for modular cryptographic proofs in coq,” in 2021 IEEE 34th Computer Security Foundations Symposium (CSF). IEEE, 2021, pp. 1–15. [16] C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol. 12, no. 10, pp. 576–580, 1969. [17] J. H. Cheon, H. Choe, A. Passelègue, D. Stehlé, and E. Suvanto, “Attacks against the ind-cpad security of exact fhe schemes,” in Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024, pp. 2505–2519. [18] M. K. Larsen and C. Schürmann, “Nominal state-separating proofs,” in 2025 IEEE 38th Computer Security Foundations Symposium (CSF). IEEE, 2025, pp. 363–377. [19] M. K. Larsen and C. Schürmann, “Mechanizing nested hybrid arguments,” Cryptology ePrint Archive, Paper 2025/1122, 2025. [Online]. Available: https://eprint.iacr.org/2025/1122 [20] D. Firsov and D. Unruh, “Reflection, rewinding, and coin-toss in easycrypt,” in Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2022, pp. 166–179. [21] G. Barthe and F. Olmedo, “Beyond differential privacy: Composition theorems and relational logic for f-divergences between probabilistic programs,” in International Colloquium on Automata, Languages, and Programming. Springer, 2013, pp. 49–60. [22] G. Barthe, M. Gaboardi, B. Grégoire, J. Hsu, and P.-Y. Strub, “Proving differential privacy via probabilistic couplings,” in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, ser. LICS ’16. New York, NY, USA: ACM, 2016, pp. 749–758.

A

Security Games and Reduction Pseudocode

This appendix gives the full security experiments used in the paper and expands the reduction from Section 3 into executable-style pseudocode.

A.1

The IND-CPA experiment

IND-CPA is the standard confidentiality notion for public-key encryption. We use its multi-query left-orright formulation: the challenger samples one hidden bit b, and every encryption query selects its plaintext with that same bit. The evaluation key is public, so the adversary can evaluate ciphertexts locally without a challenger oracle.

20

Algorithm 1 Multi-query left-or-right IND-CPA experiment procedure GAME(B) b ← {0, 1} (pk, evk, sk) ← KeyGen() b∗ ← B OEncCPA (pk, evk) return (b∗ = b) end procedure procedure OEncCPA (m0 , m1 ) c ← Enc(pk, mb ) return c end procedure The adversary may choose several encryption queries adaptively. We state security in winningprobability form: the scheme’s IND-CPA assumption supplies a bound WinProb[IND-CPAS (B)] ≤ βCPA (B) for every adversary B with the required oracle interface. Equivalently, if advantage means excess winning probability over random guessing, then βCPA (B) = 21 + AdvCPA (B).

A.2

The IND-CPAD experiment

Li and Micciancio introduced IND-CPA with decryption, or IND-CPAD, to model attacks that exploit released approximate decryptions [8]. The game retains the hidden bit, encryption oracle, and final guess of IND-CPA, and adds homomorphic evaluation and restricted decryption. Its challenger maintains a table T = [(m0 , m1 , c), . . .]. Each row records the actual ciphertext c together with the plaintext it would represent in the left challenge world and in the right challenge world. Only the ciphertext for the world selected by b is sampled. The encryption oracle appends a new row. The evaluation oracle applies the same gate separately to the recorded left-world and right-world plaintexts, then stores both results alongside the evaluated ciphertext. The decryption oracle returns a plaintext only if the two recorded plaintexts agree. This restriction is what makes decryption compatible with a left-or-right game: if the two plaintexts differed, releasing the decryption could reveal the hidden bit immediately. The adversary may interleave encryption, evaluation, and decryption calls adaptively. Calls beyond the q-query decryption budget, out-of-range table indices, and other failed assertions abort that execution. In SSProve, an aborted execution contributes no probability to winning. Here SampleCurrent is instantiated by the surrounding game. For a row whose two recorded plaintexts agree, Ti = (m, m, Some(c̄, e)), the real game uses Floode (dec0 (sk, Ti .c)), whereas the simulated-decryption game uses Floode (m), exactly as in Equation (5). The formal proof factors the common prefix of ODEC from this final sampling continuation.

A.3

Reduction adversary

21

Algorithm 2 IND-CPAD Challenger Skeleton Ingredients: • An approximate homomorphic encryption scheme S = (KeyGen, Enc, Eval, Dec). • A decrypt-query bound q ∈ N. Global challenger state: • keys pk, evk, sk; • hidden challenge bit b ∈ {0, 1}; • table T ∈ (M × M × C)∗ of challenge plaintext pairs and produced ciphertexts; • decrypt counter d. procedure GAME(A) b ← {0, 1} (pk, evk, sk) ← KeyGen() T ← [] d←0 b∗ ← AOEnc,OEval,ODec (pk, evk) return (b∗ = b) end procedure

22

Algorithm 3 IND-CPAD Oracles The oracles share the challenger state from Algorithm 2. procedure OENC(m0 , m1 ) c ← Enc(pk, mb ) T ← T ++ [(m0 , m1 , c)] return c end procedure procedure OEVAL(f, I) ⃗r ← (Ti )i∈I m00 ← f ((r.m0 )r∈⃗r ) m01 ← f ((r.m1 )r∈⃗r ) c0 ← Eval(f, (r.c)r∈⃗r ) T ← T ++ [(m00 , m01 , c0 )] return c0 end procedure procedure ODEC(i) assert d < q d←d+1 assert i < |T | if Ti .m0 ̸= Ti .m1 then return None else y ← SampleCurrent(Ti ) return Some(y) end if end procedure

23

Algorithm 4 IND-CPA reduction adversary BA,q This is the conventional reduction endpoint used in the main proof. It stores the same logical table as the IND-CPAD challenger, but obtains challenge encryptions from the outer IND-CPA encryption oracle. 1: procedure Flood(m, e) 2: σe ← max{1, e}γ 3: η ← DZn ,0,σe2 4: return Jm (η) 5: end procedure 6: procedure BA,q (pk, evk)

T ← [] 8: d←0 9: b∗ ← AOEncB ,OEvalB ,ODecB (pk, evk) 10: return b∗ 11: end procedure 7:

12: procedure OEncB (m0 , m1 )

c ← OEncCPA (m0 , m1 ) T ← T ++ [(m0 , m1 , c)] 15: return c 16: end procedure

▷ outer IND-CPA encryption oracle

13: 14:

17: procedure OEvalB (f, I)

⃗r ← (Ti )i∈I 19: m00 ← f ((r.m0 )r∈⃗r ) 20: m01 ← f ((r.m1 )r∈⃗r ) 21: c0 ← Eval(f, (r.c)r∈⃗r ) 22: T ← T ++ [(m00 , m01 , c0 )] 23: return c0 24: end procedure 18:

25: procedure ODecB (i)

assert d < q d←d+1 28: assert i < |T | 29: (m0 , m1 , c) ← Ti 30: if m0 ̸= m1 then 31: return None 32: end if 33: assert c = Some(_, e) 34: y ← Flood(m0 , e) 35: return Some(y) 36: end procedure 26: 27:

24

The reduction does not know the IND-CPA challenge bit. This is harmless for decryption queries that return a value: the simulator only returns a flooded plaintext when the two recorded plaintexts agree, m0 = m1 , so there is no bit-dependent plaintext choice left to make.

B

SSProve Syntax and Semantics

This appendix recalls the fragment of SSProve on which the program logic is built [15]. SSProve embeds pure expressions shallowly in Rocq and represents effects by a free monad. Fix a result type A. Its raw code has the following constructors: c ::= return(a) | call(p, x, κ) | get(ℓ, κ) | put(ℓ, v, c) | sample(D, κ).

(12)

Here a : A. An operation signature p : S → T contains a procedure identifier as well as its argument and result types; a call has x : S and κ : T → RawCode(A). A typed location ℓ : Tℓ is read into a continuation κ : Tℓ → RawCode(A), or updated with v : Tℓ . Finally, sampling takes D ∈ SD(X) and κ : X → RawCode(A), where SD(X) denotes discrete subdistributions on X. Continuations are Rocq functions, so conditionals, pure local computation, and structurally terminating loops are supplied by the ambient language rather than by additional constructors. Monadic bind recursively pushes a continuation through this syntax. We use the customary notations x ← c1 ; c2 ≡ bind(c1 , λx.c2 ), x ← p(a); c ≡ call(p, a, λx.c), x ← get ℓ; c ≡ get(ℓ, λx.c),

(13)

put ℓ := v; c ≡ put(ℓ, v, c), x ← D; c ≡ sample(D, λx.c). An interface is a finite set of typed operation signatures. The checked type CodeL,I (A) pairs raw code with a proof that every accessed location belongs to the footprint L and every external call belongs to the import interface I. A package P : I → E is a finite map from the procedure names in its export interface E to well-scoped implementations S → CodeL,I (T ). Sequential composition P ◦ Q links P ’s calls to procedures implemented by Q. At code level, the essential clause is codeLink(call(p, a, κ), Q) = x ← Q.p(a); codeLink(κ(x), Q),

(14)

with codeLink acting recursively on the remaining constructors. Parallel composition combines disjoint export interfaces, while the identity package forwards every call. Package validity tracks the import, export, and memory-footprint side conditions used by these operations. Each location carries a type and a default initial value. A heap h maps locations to values of their declared types; lookup of an unset location returns its default. After linking has eliminated external calls, fully linked code denotes a state-transforming subdistribution JcK : Heap −→ SD(A × Heap).

(15)

Writing δz for the point distribution at z, its defining equations are Jreturn(a)Kh = δ(a,h) , Jget(ℓ, κ)Kh = Jκ(h(ℓ))Kh , Jput(ℓ, v, c)Kh = JcKh[ℓ7→v] , X D(x) Jκ(x)Kh . Jsample(D, κ)Kh = x

25

(16)

The sums are pointwise sums of subdistributions. In particular, semantic bind threads both the returned value and the updated heap: X Jx ← c; κ(x)Kh = JcKh (a, h0 ) Jκ(a)Kh′ . (17) (a,h′ )

SSProve defines failure by sampling the null subdistribution, and assert(b) as return(()) when b holds and failure otherwise. Thus failed assertions have the zero subdistribution and their continuations are not run. A fully linked game, with no unresolved oracle calls, is evaluated by resolving its Run procedure, starting from the default heap, and projecting the result component of Equation (15).

C

Checked Rules Used by the Security Proof

Figure 4 gives the complete program-logic interface used directly by the proofs under theories/Security. This interface consists of the exported lemmas in theories/ProgramLogics whose names end in Rule and that the security development invokes. The figure remains schematic: it suppresses SSProve type indices and writes µcx,h = Jc(x)Kh , wt(µ) for distribution weight, and Eq for equality of completed output–heap pairs (including failure). We use E# D for the pushforward of D by E, and supp(µ) ⊆ Q to mean that Q holds throughout the support. The assertion M = requires equal values and heaps satisfying M , as in Figure 2; Q= similarly requires Q on the left output–heap pair and equality of both pairs. All displayed side conditions are pointwise over inputs satisfying the precondition. The raw additive-error judgment. This is a convenience wrapper around the completed judgment, not a second coupling semantics. For a postcondition Q on ordinary output–heap pairs, define b Q(Some(z L ), Some(zR )) = Q(zL , zR ), b zL , zbR ) = false otherwise. Q(b Then the judgment ⊨ AEraw {P } cL ≈ϵ cR {Q} is defined to mean

b ⊨ AE{P } cL ≈ϵ cR {Q}.

Thus any failure outcome is bad, and the good event supplies concrete intermediate values and heaps to a continuation. The security proof uses this judgment only for the lossless, zero-error challengeinitialization prefix: AE-RAW-TVD establishes its invariant, AE-RAW-CONSEQ reshapes that invariant, and AE-SEQ immediately composes the result with the completed additive-error judgment for the rest of the game. This is an interface-level inventory, rather than a list of every helper lemma in the compiler proof. Several displayed rules are derived from the core rules in Figure 2: DG-VECTOR uses KL-SAMPLE; the two mixed rules use PYTH-SEQ and PYTH-REFL; and COMPILE uses PYTH-SEQ throughout the call induction before one final MICCIANCIO–WALTER conversion.

26

Unary Hoare and additive-error rules P (x, h) =⇒ Q(f (x), h) ⊨ Hoare{P } return(f (x)) {Q} 0≤ϵ

c

HOARE-RET c

L

R

L

L

R

c

c

L

L

R

supp(µxL ,h ) ⊆ Q

R

L

L

⊨ AEraw {P } cL ≈ cR {Q } Q =⇒ Q′

ϵ ≤ ϵ′

⊨ AE{P } cL ≈ cR {Q}

′

⊨ AE{P } cL ≈′ cR {Q′ } P ′ =⇒ P

Q =⇒ Q′

ϵ ≤ ϵ′

⊨ AEraw {P } cL ≈ cR {Q}

⊨ AEraw {P ′ } cL ≈′ cR {Q′ } P =⇒ xL = xR ∧ hL = hR

⊨ AE{P } cL ≈ cM {Eq}

AE-RAW-CONSEQ

⊨ AE{P } cM ≈′ cR {Eq}

⊨ AE{M } kL ≈′ kR {Q}

⊨ AE{P } (y ← cL ; kL (y)) ≈+′ (y ← cR ; kR (y)) {Q}

AE-RAW-TVD

AE-CONSEQ

⊨ AE{P } cL ≈+′ cR {Eq} ⊨ AEraw {P } cL ≈ cR {M }

AE-TVD

c

∆(µxL ,h , µxR ,h ) ≤ ϵ

R

=

P ′ =⇒ P

R

⊨ AE{P } cL ≈ cR {Eq}

wt(µxL ,h ) = wt(µxR ,h ) = 1 L

( ) ( ) c c ∆(Comp µxL ,h , Comp µxR ,h ) ≤ ϵ

0≤ϵ

AE-TRIANGLE

AE-SEQ

Pythagorean and derived sampling rules

0<σ

E injective 0≤ϵ (vi − ui )2 ≤ ϵ for every i P =⇒ h = h P =⇒ Q(y, hL ) ∧ Q(y, hR ) L R 2σ 2 n 2 ⊨ Pyth{P } z ← E# DG (u, σ ) ≈[n] z ← E# DGn (v, σ 2 ) {Q} P =⇒ xL = xR ∧ hL = hR

0 ≤ si

for every i

supp(µcxL ,hL ) ⊆ Q

⊨ Pyth{P } c ≈s c {Q} ⊨ Pyth{P } cL ≈s cR {M }

⊨ Hoare{M } k {Q}

⊨ Pyth{P } (y ← cL ; k(y)) ≈s++[0] (y ← cR ; k(y)) {Q} P =⇒ xL = xR ∧ hL = hR ∧ P0 (xL , hL )

⊨ Hoare{P0 } c {M }

for every y

DG-VECTOR

PYTH-REFL

SHARED-CONTINUATION

⊨ Pyth{M = } kL ≈s kR {Q}

⊨ Pyth{P } (y ← c; kL (y)) ≈[0]++s (y ← c; kR (y)) {Q}

SHARED-PREFIX

Adaptive-call compiler rule ValidSeparatePreserving(A, p, P, P ′ , I) ⊨ AE{I = } Compile (A, p; P, P ) ≈√ q

⊨ Pyth{I = } P.p ≈s P ′ .p {I}

q∥s∥1 /2

Compileq (A, p; P ′ , P ) {Eq}

COMPILE

Figure 4: Complete inventory of checked program-logic rules invoked directly by the security development. The labels correspond respectively to the Rocq theorems hoareRetRule, additiveErrorSameOutputTvdEqRule, additiveErrorRawTvdEqPostTotalRule, additiveErrorConseqRule, additiveErrorRawConseqRule, additiveErrorSameOutputTriangleRule, additiveErrorSeqRule, klDgNRule, pythReflRule, pythAeSeqRule, pythHoareSeqRule, and compileRule. Typing, support, and footprint premises are summarized as in Figure 2; ValidSeparatePreserving groups the compiler’s validity, memory-separation, invariant-dependence, and invariant-preservation premises.

D

Additional Probability Details

This appendix records the distribution-level results behind the program rules used in Section 4. It complements that section’s program-level account: here we state the probability facts available to the logic, while Section 4 explains how SSProve programs consume them.

27

D.1

Kullback-Leibler Infrastructure

For MathComp distributions, the formalization defines KL divergence, absolute continuity, and a predicate finiteKL(P, Q) combining absolute continuity with summability of the KL integrand. The summability component matters in Rocq because many of the distributions in the development are countable rather than finite. The core library also proves the log-sum inequality, KL preservation under injective pushforwards, and the summability facts used by the chain-rule proof.

D.2

Pinsker and Pythagorean Preservation

The formalization proves Pinsker’s inequality for MathComp distributions. Lemma D.1 (Pinsker’s inequality). For all full distributions P and Q satisfying finiteKL(P, Q), we have r DKL (P ∥ Q) ∆(P, Q) ≤ . (18) 2 The proof reduces total variation to a binary event, proves the binary quadratic Pinsker inequality by real analysis, and combines it with the data-processing/log-sum argument for that event. We also prove the chain-rule for the conditional-coordinate KL bound. This is the result used by Pythagorean probability preservation. Lemma D.2. Let P and Q be distributions over n-tuples. Assume • The distributions are lossless: dweight(P) = dweight(Q) = 1. • The relevant KL divergences are all finite: ∀i, a. finiteKL(Pi | a, Qi | a) • For all coordinate i and history a, we have the following bound: DKL (Pi | a ∥ Qi | a) ≤ εi We then have DKL (P ∥ Q) ≤

X

εi .

i

The proof is the technical heart of the probability development: it decomposes the KL integrand pointwise over tuple prefixes, controls both positive and negative parts of the resulting series, and then reassembles the bound. The value-level inequality and the summability obligation are proved in parallel. Both use the same grouping step: for each coordinate, traces are grouped by their prefix and current coordinate value, while the suffix is summed away. For the value theorem this produces an expectation of conditional KL divergences; for summability the same grouping is applied to finite positive-part sums, with one negative-part slack term per coordinate. Combining this chain bound with Pinsker gives the main preservation theorem. Lemma D.3 (Pythagorean probability preservation). Let P, Q ∈ Distr(An ) be distributions of weight one, and let s = (s1 , . . . , sn ) be a tuple of nonnegative real numbers. If, for every coordinate i and every prefix a ∈ Ai−1 , finiteKL(Pi | a, Qi | a), DKL (Pi | a ∥ Qi | a) ≤ si , then

rP

i si . 2 The same part of the formalization packages this lemma into a reusable Pythagorean distribution predicate, proves reflexivity and singleton-trace lemmas, and defines the call-error tuples used by the trace-compiler theorem.

∆(P, Q) ≤

28

D.3

Discrete Gaussian Facts

The discrete-Gaussian development is now one ingredient of the KL story rather than the whole story. It proves the equal-variance KL formula used in Equation (6): Lemma D.4 (KL Divergence between discrete Gaussians). Let σ ∈ R be positive. For all µ, ν ∈ Z, we have
(ν − µ)2 DKL DZ,µ,σ2 ∥ DZ,ν,σ2 = . 2σ 2 The proof is completely internal to the development. It first exposes the normalized mass function, proves integer-shift invariance of the Gaussian weight, derives symmetry of the centered distribution, and then uses the zero-centered first moment to evaluate the remaining expectation. The moment summability needed for that expectation is proved as well; it is no longer a side caveat. The development also includes geometric upper bounds for events of the form   Pr |x − µ| ≥ k . x←DZ,µ,σ2

These tail bounds are useful for future cryptographic applications, but the current Pythagorean program logic primarily consumes the Lemma D.4 through the discrete-Gaussian sampling rule. Thus the probability layer supplies three kinds of facts to the program logic: ordinary distributionlevel KL bounds such as the discrete-Gaussian theorem, global KL-to-TVD conversion via Pinsker and the chain rule, and completion/coupling lemmas that turn TVD bounds into additive-error judgments over SSProve semantics. The additive-error probability layer defines completion of a subdistribution by adding an explicit failure point, constructs overlap and residual distributions, and proves a maximalcoupling theorem from a TVD bound: ∆(µ, ν) ≤ ε

=⇒ ∃d. Cpl(d; µ, ν) ∧

Pr [x = y] ≥ 1 − ε.

(x,y)←d

The program-level additive-error rules use this theorem after packing SSProve outputs and heaps into a common completed output space.

E

Formal Interface Excerpts

This appendix records selected Rocq excerpts that determine the meaning of the main theorem. They are not intended to replace the full artifact; rather, they expose the small specification surface that a cryptographic reader should be able to audit independently.

E.1

Approximate Homomorphic Encryption Scheme Interface

Module Type ApproxFheScheme. Parameter pk_t : choice_type. 27 Parameter evk_t : choice_type. 28 Parameter sk_t : choice_type. 29 Parameter message : choice_type. 30 Parameter encryption : choice_type. 31 (* Here we consider "tagged ciphertexts". 32 * That is, an encryption together with an error bound. 33 * 34 * The `None` ciphertext should *only* come from evaluating unsupported ,→ operations. 35 * e.g. out of circuit depth. *) 36 Definition ciphertext := 'option (encryption × 'nat). 37 (* We assume the homomorphic encryption operates over arithmetic circuits. 38 * We therefore have a set of gates for building such circuits. *) 39 Parameter unary_gate : choice_type. 40 Parameter binary_gate : choice_type. 25 26

29

41 42 43 44 45 46 47 48 49 50

E.2

Parameter interpret_unary : unary_gate → message → message. Parameter interpret_binary : binary_gate → message → message → message. (* Now, the "usual" 4-tuple (keygen, enc, eval, dec). *) Parameter keygen : distr R (pk_t × evk_t × sk_t). Axiom keygen_lossless : dweight keygen = 1. Parameter encrypt : pk_t → message → distr R ciphertext. Parameter eval1 : evk_t → unary_gate → ciphertext → distr R ciphertext. Parameter eval2 : evk_t → binary_gate → ciphertext → ciphertext → distr R ciphertext. Parameter decrypt : sk_t → ciphertext → distr R message.

Metric Charts

Module Type ApproxFheMetric(Import Scheme: ApproxFheScheme). Parameter metric : message → message → nat. 107 Parameter dim : nat. 108 (* We only care about metrics that are locally isometric to Z^n. 109 * e.g., polynomials of some fixed degree whose coefficients belong to a finite ,→ field. *) 110 (* Charts are origin-centered: each chosen center maps to the zero vector. *) 111 Parameter isometry : message -> message -> dim.-tuple int. 112 Parameter inverse_isometry : message -> dim.-tuple int -> message. 113 Axiom isometry_center0 : 114 forall (center : message), isometry center center = ivec_zero. 115 Axiom metric_chartE : 116 forall (center m : message), 117 metric center m = ivec_dist ivec_zero (isometry center m). 118 Axiom inverse_isometry_shift : 119 forall (centerL centerR : message) (v : dim.-tuple int), 120 inverse_isometry centerR v = 121 inverse_isometry centerL (ivec_add v (isometry centerL centerR)). 105 106

E.3

Probability-One (Support-Level) Correctness

Module Type ApproxCorrectnessPerfect (Import Scheme: ApproxFheScheme) (Import M: ApproxFheMetric(Scheme)). 193 (* For simplicity, we consider only pure and deterministic decryption. *) 194 Parameter (deterministic_dec : sk_t → ciphertext → message). 195 Axiom deterministic_dec_correct : 196 ∀ sk c, \P_[ decrypt sk c ] (fun dec_out => ((dec_out == (deterministic_dec sk ,→ c)) : bool)) = 1. 197 Definition is_underlying_plaintext sk (c : ciphertext) m := 198 match c with 199 | None => false 200 | Some (data, error_bound) => Order.le (metric (deterministic_dec sk c) m) ,→ error_bound 201 end. 202 Parameter (good_keys : pk_t → evk_t → sk_t → bool). 203 Axiom keygen_perfect_correct : 204 let bad_keys (keys : pk_t × evk_t × sk_t) := 205 let '(pk, evk, sk) := keys in ~~ (good_keys pk evk sk) 206 in 207 \P_[ keygen ] bad_keys = 0. 208 Axiom encrypt_perfect_correct : 209 ∀ pk evk sk m, 210 good_keys pk evk sk → 211 let bad_encryption c := 212 ~~ (is_underlying_plaintext sk c m) 213 in 214 \P_[ encrypt pk m ] bad_encryption = 0. 215 Axiom eval1_perfect_correct : 216 ∀ pk evk sk op c m, 217 good_keys pk evk sk → 218 is_underlying_plaintext sk c m → 219 let bad_eval eval_out := 220 ~~ (is_underlying_plaintext sk eval_out (interpret_unary op m)) in 221 \P_[ eval1 evk op c ] bad_eval = 0. 222 Axiom eval2_perfect_correct : 223 ∀ pk evk sk op c1 c2 m1 m2, 224 good_keys pk evk sk → 225 is_underlying_plaintext sk c1 m1 → 226 is_underlying_plaintext sk c2 m2 → 227 let bad_eval eval_out :=

191 192

30

228 229 230

E.4

~~ (is_underlying_plaintext sk eval_out (interpret_binary op m1 m2)) in \P_[ eval2 evk op c1 c2 ] bad_eval = 0.

Discrete-Gaussian Distribution and KL Formula

The following excerpts pin down the sampler’s mass function. In particular, the distribution is not an abstract parameter: it is the normalized exponential weight below (and is the null subdistribution when the standard deviation is nonpositive). (* Unnormalized Gaussian function *) Definition gaussian (s : R) (x : int) : R := 29 expR (- (x%:~R / s) ^ 2 / 2). 27 28

(* Works "as expected" if s > 0. * null distribution otherwise. *) 197 Definition gaussian_pdf (s : R) (x : int) : R := 198 if s > 0 then 199 gaussian s x / sum (gaussian s) 200 else 0. 195 196

226 227

Lemma isdistr_gaussian (s : R) : isdistr (gaussian_pdf s).

278

Definition centered_discrete_gaussian s : distr R int := mkdistr (isdistr_gaussian s).

279 280 281 282

Definition discrete_gaussian center s : distr R int := dmargin (GRing.add center) (centered_discrete_gaussian s).

The equal-variance KL identity consumed by the program logic is itself a proved theorem, rather than an additional Gaussian assumption. Theorem kl_discrete_gaussian (mu nu : int) (s : R) : s > 0 -> 223 δ_KL (discrete_gaussian mu s) (discrete_gaussian nu s) = 224 ((nu - mu)%:~R) ^+ 2 / (2 * s ^ 2). 221 222

E.5

Product Samplers and SSProve Bridge

The construction folds the one-coordinate distribution into an independent tuple. Fixpoint dtuple {n : nat} {t: choiceType} : n.-tuple (distr R t) -> distr R (n.-tuple t) := 16 match n with 17 | 0 => fun _ => dunit [tuple] 18 | S i => fun ds => 19 \dlet_(x <- thead ds) 20 \dlet_(xs <- (dtuple (behead_tuple ds))) 21 dunit (cons_tuple x xs) 22 end. 14 15

23

Definition nfold_distr (n : nat) {t: choiceType} (d: distr R t) : distr R (n.-tuple t) := 26 dtuple (nseq_tuple n d). 24 25

23 24

Definition n_dg (n : nat) (s : R) : distr R (n.-tuple int) := nfold_distr n (centered_discrete_gaussian s).

The reduction uses SSProve’s integer and vector types. Its adapter transports the same one-dimensional distribution into that integer type, then samples the vector recursively. 21 22

Definition ssp_dg (m : 'int) (s : R) : distr R 'int := dmargin (U := 'int) Z_of_int (discrete_gaussian (int_of_Z m) s).

31

Fixpoint discrete_gaussians_aux {n : nat} (s : R) : chVec 'int n -> distr R (chVec 'int n) := 114 match n with 115 | 0 => fun _ => dunit (T := chVec 'int 0) tt 116 | S i => fun ms => 117 let '(mhead, mtail) := ms in 118 let dg := discrete_gaussians_aux s mtail in 119 \dlet_(x <- ssp_dg mhead s) 120 \dlet_(xs <- dg) 121 dunit (x, xs) 122 end. 112 113

123

Definition discrete_gaussians {n : nat} (center : chVec 'int n) (s : R) := discrete_gaussians_aux s center.

124 125

The proved bridge identifies that SSProve sampler, after conversion, with the tuple sampler used by the transformed scheme. Lemma dmargin_toIntVec_discrete_gaussians_zero (n : nat) (s : R) : dmargin (@toIntVec n) (discrete_gaussians (zeroChVec n) s) =1 n_dg n s.

205 206 207

Finally, the addition in the displayed decryption code below is coordinatewise. 22 23

E.6 53 54 55 56 57 58 59 60 61 62 63 64 65 66

Definition ivec_add {n} (v w : n.-tuple int) : n.-tuple int := [tuple (tnth v i + tnth w i) | i < n].

IND-CPA Game Definition IndCpaOracle : IndCpaOracle_t := [package IndCpa_locs ; #def #[oracle_encrypt] (messages : 'message_pair) : 'ciphertext { let (m0, m1) := messages in b ← get bit_addr ;; let m := if b then m1 else m0 in o ← get pk_addr ;; #assert isSome o as opk ;; let pk := getSome o opk in c <$ (ciphertext; encrypt pk m) ;; ret c } ].

67 68

Definition IndCpaAdv_t := package IndCpaAdv_import IndCpaAdv_export.

69 70 71 72 73 74 75 76

Definition IndCpaChallenger_t := package [interface #val #[adv_guess] : 'adv_keys → 'bool ] [interface #val #[main] : 'unit → 'bool ].

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91

Definition IndCpaChallenger : IndCpaChallenger_t := [package IndCpa_locs ; #def #[main] (_ : 'unit) : 'bool { b <$ ('bool; dflip (1 / 2)) ;; keys <$ (pk_t × evk_t × sk_t; keygen) ;; let '(pk, evk, sk) := keys in #put bit_addr := b ;; #put pk_addr := Some pk ;; #put evk_addr := Some evk ;; b' ← call [ adv_guess ] : { pk_t × evk_t ~> 'bool} (pk, evk) ;; ret (eq_op b' b) } ].

92 93 94

Definition IndCpaGame (Adv : nom_package) : nom_package := ((IndCpaChallenger ∘ Adv)%sep ∘ IndCpaOracle)%share.

95

32

96 97

Definition game_out (Adv : nom_package) : distr R bool := dfst (Pr_op (IndCpaGame Adv) (main, ('unit, 'bool)) tt empty_heap).

98

Definition winning_probability (A : nom_package) := game_out A true. 101 End IndCpa. 99

100 102

Module Type IsIndCpa(Import Scheme: ApproxFheScheme). Module IndCpaGame := IndCpa Scheme. 105 Import IndCpaGame. 106 Parameter security_bound : nom_package -> R. 107 Axiom is_secure : forall (A : nom_package), 108 Package IndCpaAdv_import IndCpaAdv_export A -> 109 winning_probability A <= security_bound A. 103 104

E.7 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121

IND-CPA with Decryption Oracle and Game Definition IndCpadOracle (max_queries : nat) : IndCpaOracle_t := [package oracle_mem_spec ; #def #[oracle_encrypt] ('(m0, m1) : 'message × 'message ) : 'ciphertext { b ← get bit_addr ;; let m := if b then m1 else m0 in o ← get pk_addr ;; #assert isSome o as opk ;; let pk := getSome o opk in c <$ (ciphertext; encrypt pk m) ;; table ← get table_addr ;; let updated_table := (table ++ [ :: (m0,m1, c)]) in #put table_addr := updated_table ;; ret c } ; #def #[oracle_eval1] ('(gate, r) : 'unary_gate × 'nat) : 'ciphertext { table ← get table_addr ;; #assert (r < length table) as r_in_range ;; let '(m0, m1, c) := nth_valid table r r_in_range in o ← get evk_addr ;; #assert isSome o as oevk ;; let evk := getSome o oevk in let m0' := interpret_unary gate m0 in let m1' := interpret_unary gate m1 in c' <$ (ciphertext; eval1 evk gate c) ;; let updated_table := (table ++ [ :: (m0', m1', c')]) in #put table_addr := updated_table ;; ret c' } ; #def #[oracle_eval2] ('((gate, ri), rj) : ('binary_gate × 'nat) × 'nat) : ,→ 'ciphertext { table ← get table_addr ;; #assert (ri < length table) as ri_in_range ;; #assert (rj < length table) as rj_in_range ;; let '(m0i, m1i, ci) := nth_valid table ri ri_in_range in let '(m0j, m1j, cj) := nth_valid table rj rj_in_range in let m0' := interpret_binary gate m0i m0j in let m1' := interpret_binary gate m1i m1j in o ← get evk_addr ;; #assert isSome o as oevk ;; let evk := getSome o oevk in c' <$ (ciphertext; eval2 evk gate ci cj) ;; let updated_table := (table ++ [ :: (m0', m1', c')]) in #put table_addr := updated_table ;; ret c' } ; #def #[oracle_decrypt] (i: 'nat) : 'option 'message { decrypt_count ← get decrypt_count_addr ;; #assert (decrypt_count < max_queries) ;; #put decrypt_count_addr := decrypt_count.+1 ;; table ← get table_addr ;; #assert (i < length table) as i_in_range ;; let '(m0, m1, c) := nth_valid table i i_in_range in if m0 == m1 then

33

o ← get sk_addr ;; #assert isSome o as osk ;; let sk := getSome o osk in m <$ (message; decrypt sk c) ;; ret (Some m) else ret None

122 123 124 125 126 127 128

}

129 130

].

138 139

Definition IndCpadAdv_t := package IndCpadAdv_import IndCpadAdv_export.

140

Definition IndCpadChallenger_t := package [interface [guess] : { pk_t × evk_t ~> 'bool } ] [interface [main] : { 'unit ~> 'bool } ].

141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162

Definition IndCpadChallenger : IndCpadChallenger_t := [package oracle_mem_spec ; #def #[main] (_ : 'unit) : 'bool { b <$ ('bool; dflip (1 / 2)) ;; keys <$ (pk_t × evk_t × sk_t; keygen) ;; let '(pk, evk, sk) := keys in #put bit_addr := b ;; #put pk_addr := Some pk ;; #put evk_addr := Some evk ;; #put sk_addr := Some sk ;; b' ← call [ guess ] : { pk_t × evk_t ~> 'bool} (pk, evk) ;; ret (eq_op b' b) } ].

163 164 165 166

Definition IndCpadGame (max_queries : nat) (Adv : nom_package) : nom_package := ((IndCpadChallenger ∘ Adv)%sep ∘ IndCpadOracle max_queries)%share.

167 168 169 170 171

Definition game_out (max_queries : nat) (Adv : nom_package) : distr R bool := dfst (Pr_op (IndCpadGame max_queries Adv) (main, ('unit, 'bool)) tt empty_heap).

172 173

Local Open Scope ring_scope.

174 175 176 177

Definition winning_probability (max_queries : nat) (A : nom_package) := game_out max_queries A true.

178 179

End IndCpad.

180 181

Local Open Scope ring_scope.

182

Module Type IsIndCpad(Import Scheme: ApproxFheScheme). Module IndCpadGame := IndCpad Scheme. 185 Import IndCpadGame. 186 (* Security bound may depend on the adversary and the decrypt-query budget. *) 187 Parameter security_bound : nom_package -> nat -> R. 188 Axiom is_secure : forall (A : nom_package) max_queries, 189 Package IndCpadAdv_import IndCpadAdv_export A -> 190 winning_probability max_queries A <= security_bound A max_queries. 183 184

E.8

Noise-Flooded Construction

Definition noise_flooding_dg_stdev (gaussian_width_multiplier : R) (error_bound : nat) : R := 260 (maxn 1 error_bound)%:~R * gaussian_width_multiplier. 258 259 261

Module Type NoiseFloodingParams. Parameter gaussian_width_multiplier : R. 264 Axiom gt0_gaussian_width_multiplier : 265 gaussian_width_multiplier > 0. 262 263

34

266

End NoiseFloodingParams.

267

Module NoiseFlooding (Import Scheme : ApproxFheScheme) 270 (Import Metric : ApproxFheMetric(Scheme)) 271 (Import Params : NoiseFloodingParams) 272 <: ApproxFheScheme. 273 Definition pk_t := Scheme.pk_t. 274 Definition evk_t := Scheme.evk_t. 275 Definition sk_t := Scheme.sk_t. 276 Definition Scheme_t := Scheme.Scheme_t. 277 Definition message := Scheme.message. 278 Definition encryption := Scheme.encryption. 279 Definition ciphertext := Scheme.ciphertext. 280 Definition unary_gate := Scheme.unary_gate. 281 Definition binary_gate := Scheme.binary_gate. 282 Definition interpret_unary := Scheme.interpret_unary. 283 Definition interpret_binary := Scheme.interpret_binary. 284 Definition keygen := Scheme.keygen. 285 Lemma keygen_lossless : dweight keygen = 1. 286 Proof. exact: Scheme.keygen_lossless. Qed. 287 Definition encrypt := Scheme.encrypt. 288 Definition eval1 := Scheme.eval1. 289 Definition eval2 := Scheme.eval2. 290 Definition dg_stdev (error_bound : nat) : R := 291 noise_flooding_dg_stdev gaussian_width_multiplier error_bound. 292 (* Invalid ciphertexts are modeled by the null subdistribution; the scheme 293 interface treats them as unsupported evaluation results. *) 294 Definition decrypt (sk: sk_t) (c: ciphertext) : distr R message := 295 match c with 296 | None => dnull 297 | Some (_, e) => 298 \dlet_(m <- Scheme.decrypt sk c) 299 \dlet_(noise <- n_dg dim (dg_stdev e)) 300 dunit (inverse_isometry m (ivec_add noise (isometry m m))) 301 end. 268

269

302

E.9 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257

Concrete IND-CPA Reduction Definition IndCpadOracle (max_queries: nat) : IndCpaSim_t := [package oracle_mem_spec ; #def #[oracle_encrypt] (messages : 'message_pair) : 'ciphertext { ready ← get ready_addr ;; #assert ready ;; c ← call [ oracle_encrypt ] : { message_pair ~> ciphertext } messages ;; table ← get table_addr ;; let '(m0, m1) := messages in let updated_table := (table ++ [ :: (m0, m1, c)]) in #put table_addr := updated_table ;; @ret ciphertext c } ; #def #[oracle_eval1] (a : 'adv_ev1) : 'ciphertext { ready ← get ready_addr ;; #assert ready ;; let (gate, r) := a in table ← get table_addr ;; #assert (r < length table) as r_in_range ;; let '(m0, m1, c) := nth_valid table r r_in_range in o ← get evk_addr ;; #assert isSome o as oevk ;; let evk := getSome o oevk in let m0' := interpret_unary gate m0 in let m1' := interpret_unary gate m1 in c' <$ (ciphertext; eval1 evk gate c) ;; let updated_table := (table ++ [ :: (m0', m1', c')]) in #put table_addr := updated_table ;; @ret ciphertext c' } ; #def #[oracle_eval2] (a : 'adv_ev2) : 'ciphertext { ready ← get ready_addr ;;

35

#assert ready ;; let '(gate, ri, rj) := a in table ← get table_addr ;; #assert (ri < length table) as ri_in_range ;; #assert (rj < length table) as rj_in_range ;; let '(m0i, m1i, ci) := nth_valid table ri ri_in_range in let '(m0j, m1j, cj) := nth_valid table rj rj_in_range in let m0' := interpret_binary gate m0i m0j in let m1' := interpret_binary gate m1i m1j in o ← get evk_addr ;; #assert isSome o as oevk ;; let evk := getSome o oevk in c' <$ (ciphertext; eval2 evk gate ci cj) ;; let updated_table := (table ++ [ :: (m0', m1', c')]) in #put table_addr := updated_table ;; @ret ciphertext c' } ; #def #[oracle_decrypt] (i: 'nat) : 'option_message { ready ← get ready_addr ;; #assert ready ;; decrypt_count ← get decrypt_count_addr ;; #assert (decrypt_count < max_queries) ;; #put decrypt_count_addr := decrypt_count.+1 ;; table ← get table_addr ;; #assert (i < length table) as i_in_range ;; let '(m0, m1, c) := nth_valid table i i_in_range in if (m0 == m1) then #assert isSome c as c_valid ;; let '(_, error_bound) := getSome c c_valid in noise <$ (chVec chInt dim; discrete_gaussians (zeroChVec dim) (noise_flooding_dg_stdev gaussian_width_multiplier error_bound)) ;; let res := inverse_isometry m0 (ivec_add (toIntVec noise) (isometry m0 ,→ m0)) in @ret ('option message) (Some res) else @ret ('option message) (None) }

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296

].

297 298 299 300 301

Definition IndCpaSimTop_t := package IndCpadAdv_export IndCpadAdv_export.

302 303 304 305 306 307 308 309 310 311 312 313 314 315

Definition IndCpaSimTop : IndCpaSimTop_t := [package oracle_mem_spec ; #def #[guess] ('(pk, evk) : 'adv_keys) : 'bool { ready ← get ready_addr ;; #assert (~~ ready) ;; #put ready_addr := true ;; #put pk_addr := Some pk ;; #put evk_addr := Some evk ;; b ← call [ guess ] : { pk_t × evk_t ~> 'bool } (pk, evk) ;; ret b } ].

316 317 318

E.10

Definition IndCpaReduction (A : nom_package) (max_queries: nat) : nom_package := ((IndCpaSimTop ∘ A)%sep ∘ IndCpadOracle max_queries)%share.

Loss Formula

Definition security_loss (dim max_queries : nat) (gaussian_width_multiplier : R) : R := 41 Num.sqrt 42 ((max_queries%:R * 43 (dim%:R / (2 * gaussian_width_multiplier ^+ 2))) / 2). 39 40

36

E.11 1783 1784 1785 1786 1787 1788

Reduction Validity (* The package-level reduction preserves the IND-CPA adversary interface. *) Lemma ind_cpa_reduction_valid (A : nom_package) max_queries : Package IndCpaDSim.IndCpadAdv_import IndCpaDSim.IndCpadAdv_export A -> Package IndCpaSecurity.IndCpaGame.IndCpaAdv_import IndCpaSecurity.IndCpaGame.IndCpaAdv_export (ind_cpa_reduction A max_queries).

37

Related documents

• KRYPTOS K4: Constraint-Based Structural Cryptanalysis from Public Anchors#191052
• Homomorphic encryption-based testing computing system — Bank Of America Corporation (US11809310B2)#607507
• Secure Conformance Checking using Token-based Replay and Homomorphic Encryption#141429
• On GPU Implementation for Multi-Precision Integer Division#259416
• SECRYPT 2010: proceedings of the International Conference on Security and Cryptography, Athens, Greece, July 26-28, 2010#226368