clutch.gen_diffpriv.lib.trunc_laplace

Reusable TRUNCATED discrete-Laplace library for the generic DP logic — the metric approximate-DP client. This mirrors lib.laplace but for the bounded-support truncated discrete Laplace family trunc_laplace_family (see gen_prob_lang/families.v), whose per-distance coupling prob/trunc_laplace.v.DPcoupl_trunc_lap is the EXACT group-bound profile (s·ε, δ₁·grp ε s) (with ε = num/den, δ₁ = exp(-ε·A)/Z_A, shift s). Importing this file and providing a SampleIn trunc_laplace_family S instance makes the TruncLaplace surface notation and the wp_couple_trunc_laplace mechanism rule available at WHATEVER index the family occupies in the signature S. The truncation half-width A is a genuine RUNTIME sample parameter (the fourth Z of trunc_laplace_family's (A,num,den,loc) interface), NOT a Coq-level family index — so A is chosen at sample time, and the side-conditions 0 <= A (and the regime 0 <= s <= A) that DPcoupl_trunc_lap requires are HYPOTHESES on the runtime A. The family's sample at param (A,num,den,loc) is trunc_lap_rat (Z.max 0 A) num den loc; at runtime A >= 0 the clamp is the identity (Z.max 0 A = A), connecting it to DPcoupl_trunc_lap's trunc_lap_rat A via a small Z.max_r rewrite. Unlike lib.laplace, the draw coupling carries a NONZERO additive error δ = tlap_delta, so we go through wp_couple_sample_gen_dp (the δ-carrying program-couple seam) rather than wp_couple_sample_gen. The mechanism is packaged as a hoare_diffpriv_metric instance — the validating example for the group-bound metric approximate-DP definition.

TruncLaplace A num den mean tape samples the truncated discrete Laplace family at parameter (A,num,den,mean) — with A the RUNTIME truncation half-width — using sample tape tape (#() for a direct, tape-less sample). As in lib.laplace, the family's index in the ambient signature is recovered from the SampleIn instance — NOT hardcoded. The value parameter is the nested pair (A, (num, (den, mean))) matching trunc_laplace_family's (A,num,den,loc) mkZNoise4 encoding.

Value-form of TruncLaplace (direct, tape-less): the nested (A, (num, (den, mean))) parameter already reduced to a PairV tree, as it appears AFTER wp_pures/tp_pures. The coupling rule wp_couple_trunc_laplace is stated on this shape so its precondition matches post-reduction goals; the couple_trunc_laplace tactic relies on it. Mirrors LaplaceV/ExpV, but with the extra leading truncation half-width A.

The fixed additive boundary mass δ₁ = exp(-ε·A)/Z_A. Independent of the location (the normaliser tlap_Z is shift-invariant), so we pin loc = 0.

tlap_delta factors as tlap_del · grp ε |s| — the group-bound shape. Now over the two-sided shift: tlap_delta depends only on |s|.

The family's clamped sample equals trunc_lap_rat A … for runtime A >= 0 (Z.max 0 A = A). This is what connects trunc_laplace_family's sample to DPcoupl_trunc_lap's trunc_lap_rat A. Holds DEFINITIONALLY up to the Z.max clamp, which the 0 <= A hypothesis discharges via Z.max_r.

The core truncated-Laplace draw coupling, on the family's outcome type Z: for a TWO-SIDED shift s (UNCONDITIONALLY — no |s| ≤ A), sampling at loc (impl) couples to sampling at loc+s (spec) along the DIAGONAL (z = z') at cost (|s| · ε) multiplicative AND tlap_delta A num den loc s additive. Family-level fact, discharged by the reusable two-sided (now unconditional) DPcoupl_trunc_lap after the Z.max 0 A = A clamp rewrite (sf_sample_trunc, needs 0 <= A).

The TIGHT truncated-Laplace draw coupling, on the family's outcome type Z: for a TWO-SIDED shift s (UNCONDITIONALLY), sampling at loc (impl) couples to sampling at loc+s (spec) along the DIAGONAL (z = z') at cost (|s| · ε) multiplicative AND the OPTIMAL additive error tlap_tail A num den |s| (the uncovered bad-set tail mass). Family-level fact, discharged by the tight reusable DPcoupl_trunc_lap_tight after the Z.max 0 A = A clamp rewrite (sf_sample_trunc, needs 0 <= A). At adjacency (|s| ≤ 1) this gives the TIGHT δ expressed by hoare_diffpriv_classic.

The truncated-Laplace mechanism at the WP level: sampling at location loc (impl) vs loc+s (spec), TWO-SIDED (UNCONDITIONAL — no |s| ≤ A), couples to EQUAL outputs at multiplicative cost |s|·ε and additive cost tlap_delta A num den loc s. Obtained by instantiating the δ-carrying prog-couple seam wp_couple_sample_gen_dp with the single (now unconditional) draw coupling DPcoupl_trunc_lap_draw — at the recovered index sample_idx. A is a RUNTIME Z argument with 0 <= A a hypothesis.

The TIGHT truncated-Laplace WP rule: sampling at location loc (impl) vs loc+s (spec), TWO-SIDED (UNCONDITIONAL), couples to EQUAL outputs at multiplicative cost |s|·ε and the OPTIMAL additive cost tlap_tail A num den |s|. Same wp_couple_sample_gen_dp seam as wp_couple_trunc_laplace, but the draw coupling is the tight DPcoupl_trunc_lap_draw_tight. This is what powers the TIGHT classic adjacency instance hoare_trunc_laplace_diffpriv_classic.

grp ε · is monotone in the distance (for ε > 0): the numerator exp(c·ε)-1 is increasing in c and the denominator exp ε - 1 > 0.

The TRUNCATED-LAPLACE MECHANISM as a group-bound metric approximate-DP program over PLAIN dZ — the validating CLIENT for hoare_diffpriv_metric. At base rate ε = num/den and additive base mass tlap_del A num den, for inputs at distance dZ x x' ≤ c the mechanism demands ↯m (c·ε) AND ↯ (tlap_del · grp ε c), and the two output draws agree — exactly the hoare_diffpriv_metric precondition shape with eps := ε, del := tlap_del A num den. A is a RUNTIME Z argument with 0 <= A a hypothesis. TWO-SIDED AND UNCONDITIONAL. Thanks to the now-unconditional coupling DPcoupl_trunc_lap / wp_couple_trunc_laplace (the old |s| ≤ A regime restriction is GONE), the group-bound budget ↯ (tlap_del · grp ε c) is valid at EVERY distance c — so this is a bare hoare_diffpriv_metric instance over the PLAIN metric dZ, with NO truncated-metric (dZ_trunc) scaffolding and NO range split. (Beyond the half-width the group bound is sound but strictly LOOSE; the TIGHT adjacency δ is reported by the classic instance hoare_trunc_laplace_diffpriv_classic below.) PROOF. The SAME single-coupling structure as lib.laplace's hoare_laplace_diffpriv: tp_pures/wp_pures then tp_bind/wp_bind the Sample, apply the value-form wp_couple_trunc_laplace at the actual shift s = x'-x (so impl loc x, spec loc x + s = x'), and weaken its (|s|·ε, tlap_delta x s) = (|s|·ε, tlap_del·grp ε |s|) profile DOWN from the demanded (c·ε, tlap_del·grp ε c) credits — multiplicative via ecm_weaken (|s| ≤ c); additive via ec_weaken and grp_mono (grp ε |s| ≤ grp ε c).

tlap_tail is monotone in the bad-set radius Δ: the indicator A - Δ < z grows as Δ grows, so the (nonneg) tail mass only increases. Used to weaken the consumed adjacency δ (at |s| ≤ 1) up to the reported tight value tlap_tail A num den 1.

The TIGHT classic-adjacency instance.

The TRUNCATED-LAPLACE MECHANISM as a TEXTBOOK (ε, δ)-DP program at adjacency — the validating CLIENT for hoare_diffpriv_classic. At base rate ε = num/den and the TIGHT adjacency additive mass δ = tlap_tail A num den 1 (the optimal bad-set tail at a unit shift, tlap_tail_one = (1−α)·α^A / (1+α−2·α^{A+1}) with α = exp(−ε)), for inputs at adjacency dZ x x' ≤ 1 the two output draws agree consuming exactly ↯m ε and ↯ δ. A is a RUNTIME Z argument with 0 ≤ A a hypothesis. This δ is STRICTLY tighter than the group-bound metric instance's adjacency value tlap_del A num den (which equals tlap_delta x s at the unit shift): the tail mass tlap_tail is the OPTIMAL additive error, while tlap_delta is its un-clamped geometric over-approximation. Only the classic form (no grp scaling) can express this tight δ. PROOF. Same single-coupling structure, but via the TIGHT wp_couple_trunc_laplace_tight at the actual shift s = x'-x (so |s| ≤ 1 from dZ x x' ≤ 1). Consumed multiplicative |s|·ε ≤ ε (ecm_weaken) and additive tlap_tail A num den |s| ≤ tlap_tail A num den 1 (ec_weaken + tlap_tail_mono, as |s| ≤ 1).

The truncated-discrete-Laplace coupling tactics follow the consolidated design of lib.laplace: TWO tactics — the bundled couple_trunc_laplace and the apply-only couple_trunc_laplace_apply — built from the family-agnostic couple_bind (defined in gen_diffpriv.proofmode) plus the thin family-specific couple_trunc_laplace_iapply and the trunc-local discharge batteries below. The old couple_trunc_laplace_cost is subsumed by couple_trunc_laplace: the routed (non-exact cost) regime is selected by the caller's \"[$Hr Hε Hδ]\" pattern, not by a separate tactic. Two family wrinkles keep the discharge batteries trunc-LOCAL rather than the family-agnostic couple_discharge/couple_discharge_apply: (1) this coupling is built over the δ-carrying seam wp_couple_sample_gen_dp, so its precondition threads THREE resources — the spec ⤇, the multiplicative credit ↯m ε' AND the additive credit ↯ δ' — hence the 3-way pattern \"[$Hr $Hε $Hδ]\" (vs the 2-way pattern of laplace/exp); and (2) the regime side-condition Hs can take the conjunctive form 0 ≤ s ≤ A, which needs the split; lia alternative the shared batteries omit. couple_trunc_laplace_iapply A s pat — the family-specific apply step shared by couple_trunc_laplace and couple_trunc_laplace_apply. unshelve (the tactical, not the Unshelve command) turns ONLY the goals THIS iApply shelves — the regime HA/Hs and equational Hε/εpos/Hε'/Hδ' side- conditions — into regular front goals.

couple_trunc_discharge — the bundled-tactic battery (trunc analogue of the shared couple_discharge, with the extra split; lia for the conjunctive regime 0 ≤ s ≤ A). Pins the regime HA/Hs and equational Hε/εpos/Hε'/Hδ' side-conditions; the |- R => fail-guarded assumption stops a bare real-valued value-evar from being instantiated with an in-context c : R at routed (cost) sites, where the two residual credit goals ↯m (s·ε) / ↯ δ' (both iProps) survive for the caller's ecm_*.

couple_trunc_discharge_apply — the slimmer apply-only battery (trunc analogue of the shared couple_discharge_apply): same guarded shape without the simpl; lra framed-closer, so the interleaved apply sites' hand-written residual closers are left untouched.

couple_trunc_laplace A s with "[…]" — the ergonomic coupling step for the truncated discrete Laplace. Focuses the Sample on both sides (couple_bind) and applies the value-form wp_couple_trunc_laplace inferring loc/num/den/ε/ε'/δ'/K/E from the goal — the author supplies only the runtime truncation half-width A and the forward shift s (so impl loc loc, spec loc loc+s), together with the 3-way resource pattern. Subsumes the old exact-cost couple_trunc_laplace (eager-frame the credits, \"[$Hr $Hε $Hδ]\") and the non-exact couple_trunc_laplace_cost (route the credits unframed, \"[$Hr Hε Hδ]\", leaving ↯m (s·ε) / ↯ δ' for ecm_eq/ecm_weaken); the regime is chosen by the resource pattern.

couple_trunc_laplace_apply A s with "[$Hr Hε Hδ]" — the APPLY-ONLY variant, for INTERLEAVED coupling sites where essential setup happens BETWEEN focusing the Sample and applying the coupling rule. PRECONDITION: the caller has ALREADY focused the Sample on both sides (its own couple_bind-equivalent) and done any interleaved setup; this tactic runs ONLY the unshelve (iApply …) + the slimmer couple_trunc_discharge_apply battery, leaving the two credit goals and the hand-closed residual goals (and postcondition) for the caller.

CANARY: two surface-form TruncLaplace #A #num #den #loc #() draws couple to EQUAL outputs, at multiplicative cost s·(num/den) and additive cost tlap_delta A num den loc s — driven entirely by the couple_trunc_laplace tactic. Stated over the TruncLaplace notation (i.e. expr, with the un-reduced nested Pair param) so it exercises the surface path a program takes; the THREE resources (spec ⤇, multiplicative ↯m and additive ↯) are threaded by the 3-way pattern, demonstrating the δ-carrying convenience layer end to end. The regime side-conditions 0 ≤ A and 0 ≤ s ≤ A are passed as hypotheses and closed by the tactic via assumption/lia.

CANARY for the NON-EXACT cost regime of the MERGED couple_trunc_laplace: identical statement to the framed canary above, but BOTH credits are ROUTED (unframed Hε/Hδ, pattern \"[$Hr Hε Hδ]\") into their residual ↯m (s·ε) / ↯ δ' goals rather than $-framed. Here the costs are exact so the residual goals are closed by simply re-framing Hε/Hδ; a real cost-reconciliation site would instead run iApply ecm_eq; … / iApply ecm_weaken; … there. Exercises that the SAME couple_trunc_laplace tactic, when handed a routed pattern, elaborates, auto-discharges the regime/equational side-conditions, and leaves the two credit goals clean (the old separate couple_trunc_laplace_cost is now subsumed).

CANARY for the APPLY-ONLY couple_trunc_laplace_apply: identical statement, but the caller does the wp_bind/tp_bind MANUALLY (mimicking an interleaved site) before calling the apply-only tactic — exercising that couple_trunc_laplace_apply does NOT itself re-bind the Sample and works once the caller has focused both sides. BOTH credits are ROUTED (unframed Hε/Hδ, pattern \"[$Hr Hε Hδ]\") into their residual goals; here the costs are exact so the residuals are closed by re-framing.