clutch.gen_diffpriv.lib.laplace_tapes

Tape-based discrete-Laplace library for the generic DP logic. This adds the *presampling* (tape) interface for the Laplace family on top of lib.laplace:

• surface program syntax AllocTapeLaplace num den mean and the typed tape views α ↪L (num, den, mean; zs) (impl) / α ↪Lₛ (num, den, mean; zs) (spec), both sugar over the *one* generic tape map at the family's index sample_idx (recovered from SampleIn laplace_family S, never hardcoded);
• the deterministic read wp_laplace_tape and allocator wp_alloc_tape_laplace (derived from the generic wp_sample_tape / wp_alloc_sample_tape);
• the presampling coupling wp_couple_tapes_laplace, obtained by feeding the single Laplace draw coupling DPcoupl_laplace_draw into the generic state-step seam wp_couple_tapes_family.

As with lib.laplace, a client only provides Definition Slap + SampleIn laplace_family Slap and works in a diffprivGS Slap-development.

AllocTapeLaplace num den mean allocates a fresh presampling tape for the Laplace family at parameter (num, den, mean). The family's index is read off the ambient SampleIn laplace_family _ instance.

Typed tape views: a Laplace tape holding presampled outcomes zs : list Z, on the impl (↪L) and spec (↪Lₛ) tape maps respectively. Both are sugar over the generic tape predicate at index sample_idx. The parameter is written in the *explicit* value form PairV #num (PairV #den #mean) — i.e. exactly the shape the proof-mode tactics read off a reduced Sample redex — so wp_alloc_sample_tape/wp_sample_tape/tp_* match it syntactically. (This form is definitionally sf_param_to_val laplace_family (num,den,mean); the bridge is laplace_param_to_val below, used inside the coupling rule.)

The two representations of a Laplace parameter / outcome coincide definitionally; these reflexivity lemmas let us rewrite between the family-level form (produced by wp_couple_tapes_family) and the explicit value form (used by the tape views and proof-mode tactics).

Allocate a fresh Laplace tape (empty). The Pair parameter reduces by wp_pures to a value, then the generic allocator fires.

Read the head presampled outcome off a non-empty Laplace tape (deterministic). The Pair parameter reduces by wp_pures, then the generic wp_sample_tape fires.

The *reduced-form* (value-parameter) Laplace tape read. This is the same deterministic read as wp_laplace_tape, but stated on the Sample redex with its parameter ALREADY reduced to a value PairV … and the tape label as a value Val #lbl:α — i.e. exactly the goal left behind after wp_pures has reduced the surface Laplace #num #den #mean (#lbl:α) notation. The surface rule no longer wp_apply-matches that reduced goal (the parameter is a PairV, not a Pair); this rule does. No wp_pures is needed in the proof: the generic wp_sample_tape fires directly. This mirrors the surface-vs-reduced split between hoare_couple_laplace (surface) and wp_couple_laplace (reduced) in lib.laplace.

The presampling (tape) Laplace coupling: advancing two Laplace tapes with a shared draw shifts the spec draw by k at multiplicative error |k'|·ε, provided the two means differ by at most k' after the shift. This is the generic wp_couple_tapes_family instantiated with the single Laplace draw coupling DPcoupl_laplace_draw — at the index sample_idx, so one rule serves every signature containing laplace_family.