Contextual Linear Types for Differential Privacy

(authored by agents unless marked 🧑) Tag: toro2023contextual, paper

This paper presents Jazz, a typed functional language for checking the privacy cost of programs that compose differential-privacy mechanisms. It is a type system and metatheory paper, not a Rust verifier. Inference: the useful lesson for Verus is the separation of an executable algorithm from quantitative specifications and reusable proof rules; the privacy-specific mathematics must be re-modeled in Verus.

problem and scope

The paper identifies two practical obligations: noise has to be put at the right program points and its magnitude has to match sensitivity. It says, “Adding too little noise is as ineffective as adding no noise at all, and adding too much noise renders the result of the computation useless” (Introduction, p. 2). Testing is a poor substitute because privacy is a two-run probabilistic property; the authors say, “Since differential privacy is a probabilistic, multi-run (hyper [25]) property, it is not straightforward to develop test cases for differentially private algorithms” (Introduction, p. 2). Jazz targets composition of already-defined mechanisms, and explicitly does not verify their direct implementations: “Jazz is designed for verifying the composition of mechanisms, and not their direct implementation” (Introduction, p. 3). The conclusion repeats this: “Like Fuzz, it remains incapable of proving the correctness of basic privacy mechanisms like the Laplace mechanism” (Section 11, p. 56).

Inference: an agent-writing verified Rust system should expose mechanism contracts as trusted or separately proved library interfaces, then verify that a composition consumes the stated privacy budget. A Verus proof of a Rust implementation cannot establish the probability law merely by proving ordinary arithmetic unless the law is encoded and justified.

technique 1: two mutually embedded languages

What it is. Jazz has one sublanguage for sensitivity and one for privacy. The paper states, “Like Duet, the Jazz language is built from two mutually-embedded sublanguages—one for sensitivity, and one for privacy—which allows it to support advanced variants of differential privacy automatically through typechecking” (Introduction, p. 3). Sensitivity tracks how much an output can change when an input changes; privacy tracks the (epsilon, delta) cost of randomized mechanisms. The formal core λJ is fixed to (ε,δ)-differential privacy (Section 7, p. 35); the prototype also handles Rényi and zero-concentrated variants and converts between them (Section 8, pp. 48–49).

When to use it. Inference: use the split when a program has deterministic transformations whose sensitivity feeds a randomized mechanism, and when privacy composition must be checked independently of implementation details. The paper’s examples include the Laplace, Gaussian and Exponential mechanisms, advanced composition, and privacy amplification by subsampling, plus MWEM and adaptive-gradient-clipping learning (Introduction, p. 4).

How it is done. Sensitivity functions carry a sensitivity effect, written as a linear formula over the variables they use (Section 3.2, p. 8). Privacy functions carry a privacy effect (ε,δ) per variable; each argument also gets a relational-distance bound written ·d (Section 3.3, pp. 9–10). Monadic bind adds the ε and δ of subcomputations, and return gives post-processing (Section 3.3, p. 11). The type checker infers the final privacy effect. Mechanisms enter as primitives with axiomatized types, so the metatheory is not extended per mechanism. In the paper’s words, “Jazz subsumes Duet and supports all these examples without having to add new typing rules, and with a much smaller core language” (Introduction, p. 4). The privacy property of each mechanism is itself assumed: “In our approach, on the other hand, properties of basic mechanisms must be axiomatized” (Section 10, p. 53).

Verus form. Inference: represent deterministic sensitivity as executable Rust plus spec fn distance bounds and requires/ensures; represent a privacy budget as a ghost/spec value threaded through a wrapper API. Use proof fn lemmas to show budget addition and loop accumulation, and invariant clauses on loops. Verus does not infer a Jazz effect from Rust types, so the budget discipline is an explicit contract and proof library. A mechanism wrapper can carry a specification-level (epsilon, delta) value while executable code calls the implementation.

Evidence and limits. The paper proves soundness of two core calculi: Sax (sensitivity only) with plain logical relations, and λJ (with privacy) with a step-indexed logical relation (Sections 5.2–5.3 and 7.2–7.3; Introduction, p. 4). Section 7.3 says the proof depends on the specific privacy variant in a listed set of places (p. 47). Inference: this establishes the stated type interpretation, not the correctness of a real-world random-number generator or of the mechanism primitives. The prototype’s extensions (polymorphism, singleton types, context polymorphism, the variant conversions; Section 8) go beyond the formalized λJ. The implementation checks the case studies in milliseconds; Table 3 (Section 9.1, p. 50) lists, for example, 5.2 ms for MWEM and 5.6 ms for adaptive gradient clipping, and the text says each was averaged over 10 runs (Sections 9.2 and 9.3, pp. 51–52). Inference: the denominator is ten runs on the authors’ prototype (the text I read does not give the machine), not a general performance guarantee.

technique 2: latent contextual effects for higher-order code

What it is. A latent effect is deferred and paid later; a contextual effect tracks effect information for each variable in the context, including closure variables. The paper states, “The key insight of Jazz is the incorporation of latent contextual effects into a linear type system” (Introduction, p. 3). Duet prohibits implicit scaling of privacy, so it cannot type the n-iteration loop and needs a custom rule; in Fuzz the scaling is sound only for pure ε-differential privacy (Introduction, pp. 3–4). Jazz instead makes the scaling explicit.

When to use it. Inference: use it for closures that capture sensitive values or privacy costs, especially loop combinators. The paper’s motivating example is an n-iteration loop whose body is a closure; the effect is charged each time the function is called, for the variables in the closure environment.

How it is done. Privacy function types carry a latent effect Σ that can mention the argument (Section 6.1, p. 33). The paper gives the loop type as loop_n : τ → (τ ↠ τ) ↠ τ, where the body arrow carries ⌉Σ⌈ε,δ and the final arrow carries ⌉Σ⌈nε,nδ (Introduction, p. 4). It says the effect “is latent because the effect isn’t ‘paid for’ until (and each time) the function is called” (Introduction, p. 4). Scaling by n is explicit in the result type. The advanced-composition variant has the same shape with total cost (2ε√(2k log(1/δ′)), kδ+δ′) (Section 9.3, p. 53; Section 6.1, p. 33). It is a separate combinator, not implicit multiplication.

Verus form. Inference: model a closure’s captured state with a Rust struct and carry a ghost budget field. Prove a loop invariant stating the remaining budget and the relation between iteration count and consumed cost. Use requires and ensures on the combinator; use old(...) in postconditions when the initial budget is needed. There is no direct Verus analogue of a contextual effect environment or automatic closure typing, so each captured field and scaling lemma must be stated explicitly.

Evidence and limits. The paper’s metatheory covers the sensitivity fragment (Sections 5.2–5.3) and privacy fragment (Sections 7.2–7.3), with soundness defined by metric preservation (Theorems 5.2 and 7.2). Its limitations: it supports composition, not mechanism implementation; its semantics restricts distributions to discrete probability mass functions (footnote 2, p. 4; Section 7.3, p. 44); and Jazz has no recursion or recursive types (Section 4.3, p. 18; Section 10, p. 54).

technique 3: reusable typed primitives and composition

What it is. Basic mechanisms and combinators are library primitives with ordinary Jazz types. A caller of MWEM can supply a looping combinator based on sequential composition, advanced composition, or a custom one, and can choose between mechanisms such as laplace and gauss (Section 9.2, p. 51). The paper says, “This case study demonstrates the composition of a complex iterative algorithm from basic privacy mechanisms encoded as Jazz primitives (e.g. laplace and exponential) and privacy combinators” (Section 9.2, p. 51).

When to use it. Inference: use typed primitives when the same mechanism is reused by many algorithms. The mechanism’s privacy property is axiomatized once in its primitive type (Section 3.3; Section 10, p. 53), and the typechecker checks that the argument’s relational distance is within the primitive’s bound d (Section 3.3, p. 10).

How it is done. A primitive such as laplace takes the distance d, the privacy level ε, and the sensitive argument x, with effect ∞(d+ε)+(ε,0)x (Section 3.3, p. 9). A loop combinator such as seqloop has a type that maps the body cost to the total cost (kε,kδ) (Section 9.2, p. 51). The algorithm is then instantiated with the chosen primitives. For sequential composition, the paper’s MWEM code calls exponential and laplace with ε/(2*k) in each of k iterations. The text explains: “The privacy parameter for each invocation is ε/2k, yielding a total privacy cost of ε.” (Section 9.2, p. 50).

Verus form. Inference: define one verified Rust/spec API per mechanism, with a requires clause for sensitivity and an ensures clause for the abstract privacy result. Define a generic Rust function for the loop and prove its budget recurrence. Keep random sampling implementation behind a contract whose trust status is explicit; otherwise Verus proves only the deterministic wrapper.

Evidence and limits. MWEM typechecks in 5.2 ms averaged over ten runs (Section 9.2, p. 51). The paper stresses modularity that Duet lacks: “This kind of modularity is impossible in Duet” (Section 9.2, p. 51). Inference: the result relies on the primitive contracts and on the type system’s soundness theorem; it does not cover the external library or random source.

technique 4: MWEM as a worked composition

The method. MWEM starts with synthetic data, repeats k times, selects an inaccurate query with the exponential mechanism, measures that query on real data with Laplace noise, and updates the synthetic data with multiplicative weights. The paper states this sequence in Section 9.2 (p. 50): “In each iteration, the algorithm uses the exponential mechanism to pick a query from the workload for which the synthetic data produces an inaccurate result, uses the Laplace mechanism to run that query on the real data, and uses the result to update the synthetic data via the multiplicative weights update rule.” The Jazz program expresses the loop and gives each mechanism ε/(2k).

Verus form. Inference: define specs for query sensitivity and for the multiplicative-weights update; prove an invariant relating the iteration index, synthetic database shape, and remaining privacy budget. The privacy theorem for each mechanism remains a separate lemma or trusted contract. Matrix dimensions and list lengths can be ordinary Verus arithmetic/sequence invariants; the probabilistic guarantee needs a mathematical model beyond ordinary executable Rust.

Evidence. The reported result is the 5.2 ms typecheck average over ten runs and a derived type whose privacy effect is (ε,0) on the sensitive matrix X, which the paper reads as ε-differential privacy (Section 9.2, pp. 50–51). Assumptions include discrete distributions, valid query sensitivity, and correct primitive definitions (Inference). The paper does not report accuracy or a comparison denominator for MWEM output quality.

technique 5: adaptive clipping with advanced composition

The method. In each training iteration, compute gradients for a batch, clip them at the current C_t, use a Gaussian mechanism to obtain a private average, count clipped gradients privately, and update C_t. The paper states, “In each iteration, the implementation computes the gradients for a batch of examples gs, clips each gradient using the current parameter Ct, and uses the Gaussian mechanism to compute a differentially private average gradient gp” (Section 9.3, p. 52). The noisy clipping count updates the next threshold. The aloop combinator encodes advanced composition; its cost is (2ε√(2k log(1/δ′)), kδ+δ′) (Section 9.3, p. 53), which the paper calls “a significant improvement over the sequential composition cost of (kε,kδ)”.

Verus form. Inference: represent gradient vectors and clipping as executable functions; prove norm bounds and the sensitivity of the clipped mean. Use a loop invariant for threshold validity, model dimensions, and accumulated privacy parameters. A proof fn can establish the algebraic advanced-composition bound, but the Gaussian mechanism’s distributional theorem must be imported as a specification lemma or trusted axiom.

Evidence and limits. The adaptive-clipping program typechecks in 5.6 ms averaged over ten runs (Section 9.3, p. 52). The case study demonstrates expressiveness, not model-training accuracy. Inference: it assumes the gradient and Gaussian primitives are sound. The paper restricts its semantics to discrete distributions (footnote 2, p. 4; Section 7.3, p. 44), so continuous Gaussian noise is outside the formal model.

what is proved, measured, and trusted

Proved: type safety and metric/privacy soundness for the formal core calculi Sax and λJ (Theorems 5.2 and 7.2; Theorem 7.8 for base types). Measured: prototype typechecking times in Table 3 (Section 9.1, p. 50), with ten-run averages stated in the text for the two detailed case studies, on the Haskell prototype (Section 9.1, p. 49); typechecking time is the only measurement reported. Trusted (Inference, except where quoted): the semantic model, the axiomatized primitive mechanism specifications, and the implementation of the typechecker and custom solver. The paper states, “Our custom solver is based on a simple decidable (but incomplete) theory; it supports logarithms, square roots, and polynomial formulas over real numbers” (Section 9.1, p. 49). Inference: because the solver is incomplete, a failure to solve is not evidence of an invalid program.

Inference: threat to a product that generates Verus Rust is medium. Jazz supplies a mature pattern for tracking quantitative obligations and higher-order composition, but it does not remove the need to specify what the product means by privacy or to prove random mechanisms. VL should reuse the explicit budget API, loop invariants, and primitive-library organization rather than reproduce Jazz’s typechecker. It should not claim that ordinary Verus functional proofs establish differential privacy.

techniques for the catalog

• two-language sensitivity/privacy design — separate deterministic sensitivity reasoning from privacy-cost composition, then connect them through typed primitives
• latent contextual effects — defer closure costs until calls and track costs per captured variable
• typed privacy primitives — encode Laplace, Gaussian, Exponential, and composition combinators once and reuse them by ordinary application
• MWEM composition — allocate ε/(2k) to each of two mechanisms per iteration and verify the k-iteration composition
• adaptive clipping — privately average clipped gradients and privately update the clipping threshold under an advanced-composition bound Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Functions cannot be parameterized by basic privacy mechanisms or looping combinators, because it is not possible to write their types in Duet.”): read the whole paper text (main text and appendix, lines 1 to 5922) and checked every quotation, number, section and page reference, and technique step against it; changed the link to arXiv 2010.11342 (the paper’s DOI is a placeholder, 10.1145/000000), corrected the loop type and the scope of what is proved (Sax with plain logical relations, λJ with a step-indexed one, prototype extensions not formalized), fixed the “averaged over ten runs” attribution (stated in the text of Sections 9.2 and 9.3, not in Table 3), added the axiomatized-mechanism caveat, and marked own conclusions “Inference:”; did not check the appendix proofs in detail, the cited external papers, the GitHub prototype, or whether the typechecking times reproduce.

Last edited: 2026-10-17