clutch.gen_diffpriv.lib.expmech

Reusable discrete-EXPONENTIAL-MECHANISM library for the generic DP logic — the expmech analogue of lib.laplace / lib.exponential. Importing this file and providing a SampleIn expmech_family S instance makes the ExpMech surface notation and the wp_couple_expmech mechanism rule available at WHATEVER index the family occupies in S (recovered from SampleIn via sample_idx, never hardcoded). As with lib.laplace, a client needs only: Definition Sem : Sig := ...; expmech_family; .... [global] Instance : SampleIn expmech_family Sem := ltac:(solve_SampleIn). Section foo. Context `{!diffprivGS Sem Σ}. and then writes [ExpMech num den scores] in programs and applies [wp_couple_expmech]. Unlike the noise mechanisms (Laplace / one-sided exponential), the exponential mechanism does NOT couple two outputs by a SHIFT: its underlying coupling [DPcoupl_expmech] is along plain equality ([eq]) with a fixed multiplicative cost [2·(num/den)] (and zero additive slack), valid for any two score vectors of equal length whose coordinates differ by at most [1]. This is exactly the textbook exponential-mechanism guarantee, here repackaged as a WP coupling rule by lifting [DPcoupl_expmech] through the family's [sf_inj] with [DPcoupl_map] / [DPcoupl_mono] and plugging it into the generic prog-couple seam [wp_couple_sample_gen].

ExpMech num den scores tape samples the exponential-mechanism family at parameter (num, den, scores) using sample tape tape (#() for a direct, tape-less sample). Same 4-argument surface form as Laplace / Exp, but the third argument is a *list of scores* (a value carrying the Inject_list encoding) rather than a single location; the family's index in the ambient signature is recovered from SampleIn expmech_family _.

The core exponential-mechanism draw coupling, on the family's outcome type Z (the chosen index): sampling at scores scores (impl) vs scores' (spec) is coupled along plain equality at multiplicative cost 2·(num/den) whenever the score vectors have equal length and per-coordinate sensitivity 1. Family-level fact (independent of S), discharged by the reusable DPcoupl_expmech.

The exponential mechanism is ε-DP at the WP level (for ε = 2·(num/den), δ = 0): sampling at scores scores (impl) vs scores' (spec) couples to EQUAL chosen indices, at multiplicative error 2·(num/den), under equal length and per-coordinate sensitivity 1. Obtained by instantiating the GENERIC prog-couple seam wp_couple_sample_gen with DPcoupl_expmech_draw at index sample_idx (so this one rule serves every signature containing expmech_family). The parameters are written with explicit pair (rather than (.,.)) to keep the tuple in Coq's term scope: inside the Sample/Val notation the surface (a, b) would parse as a program-level Pair.

The surface-form exponential-mechanism coupling rule, stated on the ExpMech notation (with the (num,den,scores) parameter as an un-reduced Pair and the scores list as an injected value $scores). The proof reduces the Pair params on both sides (wp_pures/tp_pures) and then applies the reduced-form wp_couple_expmech.

The exact (error-free) coupling: identical score vectors couple perfectly along the diagonal at zero cost (the reflexive coupling ARcoupl_eq lifted to DPcoupl). No sensitivity hypothesis needed here.

couple_expmech Δ with "[…]" — the ergonomic coupling step for the discrete exponential mechanism. It reduces the Pair params to a PairV (wp_pures/tp_pures), focuses the Sample on both sides (wp_bind/tp_bind), and applies the value-form wp_couple_expmech inferring num/den/scores/scores'/ε'/K/E from the goal — the author supplies only the per-coordinate sensitivity bound Δ and the resource pattern. Unlike the noise mechanisms (couple_laplace/couple_exp), the exponential mechanism couples the two chosen indices along plain EQUALITY (no shift argument), at the fixed multiplicative cost 2·Δ·(num/den) and zero additive slack — so the precondition is the SAME two-resource ⤇ ∗ ↯m shape and the pattern is the 2-way \"[$Hr $Hε]\". The remaining side-conditions are DATA-dependent rather than arithmetic: alongside the trivial HΔ : 1 ≤ Δ, Hpos, Hε' (closed by lia/assumption/reflexivity), the score-vector obligations Hlen : length scores = length scores' and Hadj : ∀ k, |scores!!!k − scores'!!!k| ≤ Δ must come from in-context hypotheses (assumption) — they cannot be synthesised by the tactic and are left as goals when no matching hypothesis is in scope.

CANARY: two surface-form ExpMech #num #den $scores #() draws over adjacent score vectors couple to EQUAL chosen indices, at multiplicative cost 2·Δ·(num/den) — driven entirely by the couple_expmech tactic. Stated over the ExpMech notation (i.e. expr, with an un-reduced Pair param and the scores list injected as a value) so it exercises the surface path a program takes; demonstrates the (equality-coupling, no-shift) convenience layer end to end. The data-dependent side-conditions Hlen/Hadj are passed as hypotheses and closed by the tactic via assumption.