clutch.gen_diffpriv.examples.laplace_tapes

Tape-based Laplace example, ported from diffpriv.examples.laplace_tapes onto gen_prob_lang / gen_diffpriv. Demonstrates the presampling interface: allocate Laplace tapes on both sides, couple them (shifting the spec draw by k), then read the presampled values deterministically. A client only declares the signature Slap and a SampleIn instance; the Laplace tape API (AllocTapeLaplace, ↪L/↪Lₛ, wp_couple_tapes_laplace) comes from lib.laplace_tapes. Note the #[global] Opaque sample_idx: in a *concrete* signature the index projection sample_idx is convertible to a numeral, and wp_pures/tp_pures would reduce it — after which the tape predicates (↪L, written with the sample_idx projection) no longer *syntactically* iFrame against the reduced hypotheses. Sealing sample_idx keeps the projection folded so the generic sample-tape tactics' output frames against the Laplace tape views.

The differentially-private use of tapes: presample-couple the two tapes so the spec draw equals the impl draw (shift k = 0) at error |loc − loc'|·ε, then read both off deterministically.