clutch.gen_diffpriv.proofmode

wp_* proof-mode tactic instances for the generic DP weakest precondition. Ported from diffpriv/proofmode; provides the base/bind/pure GwpTactics instances at gen_lang Sg, enough for wp_pures/wp_bind. (The heap instance needs the ↦∗ array layer from derived_laws; the sampling tape tactic class is deferred — relational sampling goes through coupling rules.)

Sample-tape tactic instance: enables wp_alloc_sample_tape/wp_sample_tape on the *raw* generic tape predicate l ↪ (i, pv, xs). As in prob_lang's GwpTacticsTapes instance, the fractional argument is ignored (reading the head consumes it, so the deterministic-read rules require full ownership); the obligations are discharged directly from wp_alloc_sample_tape and wp_sample_tape.

Signature-resolution overrides for usability parity.

The distribution signature S lives in the Wp/spec_update instance, not in the (signature-independent) expr/val syntax, so the generic wp_pure/tp_pure machinery cannot recover it by unification — leaving the S-parametric PureExec instance unresolvable. Both tactic families route S through an overridable hook (gwp_get_sig / tp_get_sig); here we redefine those hooks (globally, via ::=, so the effect is independent of later Import order) to read S off the in-context diffprivGS S _ hypothesis. After this, the *standard* wp_pures/tp_pures and every derived tactic (wp_rec, tp_load, …) work verbatim in any diffprivGS-development — achieving tactic parity with prob_lang.

Shared skeleton for the noise-family coupling tactics

The per-family convenience tactics (couple_laplace / couple_exp / couple_trunc_laplace and their _apply variants in lib.laplace / lib.exponential / lib.trunc_laplace) all share the same skeleton, which varies on only two axes: whether to focus the Sample on both sides first (couple_bind), and which best-effort side-condition battery to run after the unshelve (iApply (wp_couple_X …)) step. The two batteries below are family-agnostic; each library adds only a thin couple_*_iapply wrapping its own coupling-rule iApply, then assembles the bundled and apply-only tactics from these shared pieces. See lib.laplace for the full design rationale. couple_bind — the shared leading focus run by the bundled couple_X tactics: reduce the Pair params to a PairV tree (wp_pures/tp_pures) and focus the Sample on both sides (wp_bind/tp_bind). SKIPPED by the couple_X_apply variants, whose caller has already focused both sides (and may interleave setup between the bind and the apply).

couple_discharge — the shared best-effort battery for the bundled couple_X tactics, covering BOTH the exact-cost (framed credit, pattern \"[$Hr $Hε]\") and the non-exact cost (routed credit, pattern \"[$Hr Hε]\") regimes — which one you get is chosen by the caller's resource pattern, not by a separate tactic. It pins the equational/regime side-conditions (by reflexivity / apply Zabs_ind; lia / lia / simpl; lra) and closes genuine Prop hypotheses via the |- R => fail-guarded assumption. The guard is the crux: it stops assumption from instantiating a bare real-valued value-evar (ε/ε') with an in-context distance bound c : R at the routed (cost) sites, where the residual ↯m (k'·ε) credit goal — an iProp that none of these first-order tactics fire on — survives for the caller's ecm_eq/ecm_weaken reconciliation.

couple_discharge_apply — the slimmer battery for the apply-only couple_X_apply variants. Same guarded shape as couple_discharge but WITHOUT the simpl; lra framed-Hε' closer: the interleaved sites that drive the apply variant hand-write their own residual closers (e.g. ecm_eq / lra / iFrame bullets), so the battery must LEAVE those real-valued goals for the caller rather than greedily discharge them — closing them here would shift the caller's bullet alignment. This is the one per-family-variant difference that resists folding into a single battery.