Sample fam lang - #73
Merged
Merged
Conversation
dune-workspace makes dune treat clutch-samp-lang as its own root (the /workspace tree has several rocq-clutch projects). spike.v is a throwaway validating the core design: threading a distribution signature S through the language canonical structure, Option-A SampleIn resolution by reflexivity, sig_sample_at, and the mass-1 mixin via sf_mass. Compiles.
Replace per-distribution sampling primitives (Rand/Laplace/AllocTape*) with a generic Sample/AllocSampleTape over a SampleFamily signature; collapse tape state to one stapes map. Done: syntax, EqDecision/Countable, signature, eval contexts, subst, state_upd. Pending: head_step/state_step/head_step_rel + mixin + canonical. (Load temporarily renamed Deref for the rocq-mcp filter; reverts at maturity.)
Wrap the operational semantics in Section (S : Sig). Collapse prob_lang's separate uniform+Laplace head_step cases into one generic sig_sample-driven Sample/AllocSampleTape (direct / tape cons-empty-mismatch / alloc), with dzero for unsupported descriptors and a dret fallback in state_step to keep presampling mass-1. Rewrite head_step_rel (5 generic ctors: SampleNoTape/AllocSampleTape/SampleTapeCons/SampleTapeEmpty/SampleTapeOther) and state_step_rel. Type-checks through the inductives; the support-equivalence/mass/mixin proofs (which used uniform-specific tactics) are the next focused task.
All metatheory proven and compiling (rocq-mcp + dune): head_step_support_equiv_rel and state_step_support_equiv_rel rewritten for the generic constructors; state_step_head_step_not_stuck (presampling preserves reducibility) reproved via descriptor-match case analysis using mass-1 ⟹ nonempty support (SeriesC_gtz_ex); state_step_mass and head_step_mass via sig_sample_mass/dmap_mass; height/get_active ported. Full EctxiLanguageMixin (gen_lang_mixin) and S-parametric canonical structures gen_ectxi_lang/gen_ectx_lang/gen_lang : Sig -> language.
spec/spec_ra.v: generalize prob_lang's spec ghost state, collapsing heap+tapes+tapes_laplace to heap + one generic stape ghost map; one ↪ₛ notation; spec_auth/lookup/update/alloc lemmas; spec_ra_init; spec_updateGS instance parametric in S (via exact, for cfg ≡ mstate (gen_lang S)). families.v (built in parallel via subagent): uniform_family (Z, dunifP, range support), laplace_family (Z*Z*Z via laplace_rat), coin_family (bool; fair-coin placeholder — biased_coin refinement noted). All compile, no Admitted.
…e scaffolding
families.v (subagent, parallel): coin_family is now a genuine bin-weight coin (sf_param=(nat*nat) weights w1,w2; P(true)=w2/(w1+w2) via biased_coin; total since 0/0=0); RR_coin added (bias e^ε/(e^ε+1), always valid; noisy-bit source, (num/den)-DP proved later over coin⊕b). Helpers weight_coin_valid/rr_bias_valid/biased_coin_mass.
gen_diffpriv/primitive_laws.v: ghost-state setup, reusing clutch.diffpriv.{weakestpre,ectx_lifting} UNCHANGED at Λ:=gen_lang S. diffprivGS = heap + ONE generic stape ghost map (vs prob_lang's three) + specG + error credits; state_interp σ := heap_auth ∗ stapes_auth; S-parametric diffprivWpGS (gen_lang S) instance (spec_updateGS obligation discharged by spec_ra). Validates that the whole functorized WP machinery attaches to gen_lang S.
primitive_laws.v: the three sampling WP rules now compile, parametric in the distribution signature. - wp_alloc_sample_tape / wp_sample_tape (deterministic tape read) - wp_sample (direct probabilistic sampling; reducibility via mass-1 ⟹ nonempty support, SeriesC_gtz_ex) Resolved WP elaboration by declaring the gen_lang Sg canonical-structure chain (ectxi/ectx/language) in the rules section so the ectx-lifting lemmas resolve Λ. tactics.v: re-export inv_head_step / solve_distr (defined inside lang.v's Section semantics, do not survive section close) alongside the head_step hint db and solve_red. categorical.v: fully general N-weight bin sampler (bin_weight_family).
gen_diffpriv: model.v (binary logical relation) metatheory.v: the subset of prob_lang/metatheory.v that erasure needs, collapsed to the single generic stape map: det_head_step_rel/pred, is_det_head_step, det_or_prob_or_dzero (with the generic 4-shape prob_head_step_pred), head_step_dzero_upd_tapes (needs the extra sig_sample = Some hypothesis — state_step only appends to supported tapes), and the fresh_loc / upd_tape commutation lemmas. The rand-coupling lemmas are NOT ported here (they belong with the uniform family rules). notation.v: ported surface syntax; dropped rand/alloc-tape notations (no longer constructors). (background agent) model.v: binary logical relation; diffprivRGS gets the phantom Sg, lrel_tape generalized from N to (i, pv); phantom-Sg canonical structures pin the language for the WP/IntoVal/fill instances. (background agent)
types.v: dropped TAllocTape/TRand/TRandU (removed sampling constructors), Load→Deref. contextual_refinement.v: dropped CTX_AllocTape/CTX_RandL/RandR and their typed_ctx rules; ctx_refines wrapped in Section (S : Sig) and lim_exec annotated with (δ := lang_markov (gen_lang S)) since the shared expr/state don't determine the signature. (background agent)
gen_diffpriv: interp.v (type interpretation) metatheory.v: ported is_closed_expr/is_closed_val/subst_map (generic Sample/AllocSampleTape cases, Deref) + all the substitution/closedness lemmas (subst_map_*, is_closed_subst*, subst_subst*, heap_closed_alloc) needed by the relational layer. interp.v: type interpretation + bin_log_related; import swap, phantom Sg into diffprivRGS context, lrel_tape destruct patterns updated for the (i,pv) generalization. No canonical structures needed (uses closed refines/lrel from model.v).
state_step_erasable / iterM_state_step_erasable for the single generic state_step, via the full pexec induction prim_coupl_upd_tapes_dom. The per-distribution cross-product of prob_lang's ind_case_* helpers collapses to one Sample/AllocSampleTape case analysis (dunifP N → μ = sig_sample S i pv); the empty-tape descriptor-match branch is the probabilistic coupling of the fresh draw against the presampled value. Also ports the 5 DPcoupl_erasure_* lemmas (abstract erasable/rewritable hyps, needed by adequacy). No custom axioms. (ind_case_*/main induction filled by a rocq:admitted-filler-deep background agent against the prob_lang reference.)
Ported diffpriv/adequacy.v: the Section adequacy proofs are reused verbatim (the WP core spec_coupl/prog_coupl and the DPcoupl_erasure_* lemmas are language-generic). Ghost-init (wp_adequacy_exec_n) now allocates ONE generic stape map (vs tapes+tapes_laplace) and builds the phantom-Sg diffprivGS. Dropped the diffpriv_rules-dependent list/Z corollaries for now. Threading the signature Sg through the markov layer required: unique-named section canonical structures (+ a markov canonical) so the ∀S structures exported by primitive_laws don't shadow them; a local spec_updateGS instance pinned at Sg (spec_interp/spec_coupl otherwise can't recover S from the S-independent cfg); and explicit (δ := ...) annotations on the bare exec/lim_exec in the leaf lemmas.
gen_prob_lang/spec/spec_rules.v + exec_lang.v coupling_rules.v: wp_couple_tapes_gen — the REUSE SEAM. From an abstract DPcoupl μ μ' R' of the two family draws (μ = sig_sample Sg i pv), it advances two coupled tapes. The per-distribution DP content (Laplace shift, Gaussian, RR_coin) enters ONLY through that hypothesis; the tape plumbing (state_step_erasable + spec-side state step via spec_coupl_erasables_weak) is shared. Proven via state_step_unfold + DPcoupl_map/DPcoupl_mono to lift the draw-coupling to a state-step coupling. Section pins gen_lang Sg canonically + a local spec_updateGS. spec_rules.v: generic step_alloc_sample_tape / step_sample_tape over the single spec-side tape map (dropped step_rand/step_laplace/etc). exec_lang.v: generic LanguageCtx step lemmas (Sg-parametric). (background agent)
Unary WP tactic infrastructure. class_instances.v: generic Sample/ AllocSampleTape Atomic instances + the shared PureExec/IntoVal/AsVal instances (Load→Deref); solve_atomic ported. wp_tactics.v: GwpTactics Base/Bind/Pure/Heap kept; the rand/laplace tape classes collapse to one generic GwpTacticsSampleTape (tape predicate parameterized over (i,pv,xs)). tactics.v: added reshape_expr (generic Sample/AllocSampleTape eval contexts). Sections pin gen_lang S canonically (per the S-parametric language). (background agent) Note: proofmode.v will need a dq-generalized wp_sample_tape in primitive_laws to discharge GwpTacticsSampleTape's dq-general read field.
wp_alloc / wp_allocN_seq / wp_deref / wp_store (ported from diffpriv/primitive_laws, Load→Deref, explicit AllocN #1 since the Alloc notation isn't imported here). Needed by proofmode's GwpTacticsHeap instance and examples.
(match original); restore wp_rec_löb with Alloc/rec: notations The earlier "Alloc not found" / "rec: parse error" were NOT broken notations — gen primitive_laws just omitted the notation/class_instances imports that diffpriv/primitive_laws has. The gen notations are identical to prob_lang (Coercion Val/App/LitInt, Alloc, rec:). With the imports restored, wp_alloc uses the Alloc notation and wp_rec_löb compiles (its statement needed an explicit (v : val) annotation for elaboration order; the proof needs the PureExec instances from class_instances).
Derives, from the generic bridge wp_couple_tapes_gen + sig_sample_at, the family-level coupling rule: for ANY family D in the signature, a coupling of its two draws DPcoupl (sf_sample D p) (sf_sample D p') Rout (on the outcome type sf_out D) yields the tape-coupling WP rule. Adding a new distribution's coupling thus costs exactly one DPcoupl obligation — the "cheap to add a distribution" thesis, demonstrated. The val-level lifting through sf_inj is handled once via DPcoupl_map/DPcoupl_mono.
The program-step analogue of the tape bridge: directly couple two Sample i _ #() head-steps (impl + spec) via an abstract DPcoupl μ μ' R'. Mirrors hoare_couple_laplace, factored over the family draw. Proof: prog_coupl_steps_simple + DPcoupl_steps_ctx_bind_r (re-added) for the spec context; the prim-step is reduced to dmap via head_prim_step_eq (with the mass-1 reducibility witness) and coupled via DPcoupl_dbind'/DPcoupl_dret. This is what the textbook Laplace-mechanism DP example needs.
Full tp_* suite ported: tp_pures/tp_bind + all pure derivatives, tp_alloc/tp_load(Deref)/tp_store, and the generic tp_sample_tape / tp_alloc_sample_tape (replacing the dropped per-distribution tp_rand/ tp_laplace). S-parametric handling mirrors spec_rules/wp_tactics; a tp_get_sig helper reads S off the goal's spec_update since the tac_tp_* lemmas carry S as a non-conclusion argument. (background agent)
Enough for wp_pures/wp_bind on gen_lang Sg. Heap instance deferred (needs the ↦∗ array layer from derived_laws); the basic DP examples use no refs.
The first DP example on the generic language. Over the signature Slap := [laplace_family]: - DPcoupl_laplace_draw: the Laplace family's draw coupling (shift by k costs |k'|·ε), discharged by the reusable Mcoupl_laplace — the SINGLE per-distribution DP obligation. - wp_couple_laplace: the Laplace mechanism is ε-DP at the WP level, obtained by instantiating the GENERIC prog-couple seam wp_couple_sample_gen with that one coupling. No per-distribution re-clone of the program logic — the thesis, demonstrated end-to-end. (The full λ-program example needs wp_pures, which currently can't infer the signature S through the ∀S PureExec instances — a tactic-automation gap, noted for follow-up; the coupling rule itself is complete.)
Added wp_pures_gen: a signature-pinning variant of wp_pures (the generic wp_pures can't infer S for the ∀S PureExec instances — S lives in the Wp instance, not the syntax). It reads S off the in-context diffprivGS and passes it positionally to tac_wp_pure_later; wp_pure_test confirms it reduces a λ-application (with wp_value' (Λ:=...) for the value finish). This is the impl-side half of running a full λ-program DP example. The spec-side analogue (a WP-context tp_pures) is fiddlier — tp_pures pins S off a spec_update in the GOAL, absent in a WP goal, plus an ectx/ectxi fill-matching subtlety — left as tactic-engineering follow-up. The DP content (DPcoupl_laplace_draw + wp_couple_laplace) is complete.
Make the STANDARD proof-mode tactics (wp_pures/tp_pures and every derived tactic) work verbatim in concrete-signature DP developments, and land the end-to-end λ-program example proving the Laplace mechanism is ε-DP for 1-sensitive inputs — written exactly as a prob_lang proof, no _gen variants. Root cause: the distribution signature S lives in the Wp/spec_update instance, not in the (S-independent) expr/val syntax, so wp_pure/tp_pure cannot recover S by unification and the S-parametric PureExec instance is left unresolvable. Canonical structures cannot fix this (the ∀S infra canonical irrevocably owns the global expr key; Local/#[local] does not free it). Fix (import-order-independent, via late-bound Ltac hooks): - wp_tactics: route wp_pure through an overridable `gwp_get_sig` hook (default supplies a hole, preserving prob_lang-style inference). Also fix a latent port bug in wp_expr_eval (passed 9 args to the 8-arg tac_wp_expr_eval; the extra `_` misplaced `e`), which surfaced once wp_finish ran. - spec_tactics: tp_pure_at now also matches `ectxi_language.fill` — after the first tp_pure the spec context is rebuilt with that head, so multi-step reductions (nested Pairs inside a Sample argument) previously stalled. - proofmode: Export the tactic files and override `gwp_get_sig`/`tp_get_sig` (via `::=`) to read S off the in-context `diffprivGS S _` hypothesis. laplace_dp: drop the _gen band-aids; wp_pure_test now uses standard wp_pures; add wp_laplace_diffpriv (the full mechanism proof) using wp_pures + tp_pures + the per-family coupling rule. Delete the parity_test scratch file.
…t boilerplate
Usability redesign (sprint task 1). A client now "enables" a distribution in
~3 lines and writes the surface notation / coupling rules with no hardcoded
index and no canonical-structure / spec_updateGS boilerplate:
- families.v: `Hint Mode SampleIn ! -` (resolve by the named family D, recover
the signature S as output) so a signature-independent surface notation can
pin its Sample index from the unique `SampleIn D _` instance. Plus
`solve_SampleIn` (one-liner to discharge the membership obligation).
- primitive_laws.v: `diffprivGS_spec_updateGS` instance keyed off the in-context
diffprivGS — the spec layer resolves S automatically, no per-dev spec_updateGS.
- lib/laplace.v: the reusable Laplace library. `Laplace num den mean` notation
+ `wp_couple_laplace` rule, both at index `sample_idx` (from SampleIn), so one
rule serves every signature containing laplace_family. Re-exports the
client-facing layer (rules/tactics/notation/families).
- examples/laplace_dp.v: rewritten as the minimal client — `Definition Slap`,
one-line `SampleIn` instance, `Context {!diffprivGS Slap Σ}`. The
per-section canonical structures are gone (they were redundant no-ops: the ∀S
chain from class_instances already owns the expr key). Only a one-line
`Local Notation fill` remains, and only because the statement names an
explicit spec context K.
- derived_laws.v: the [array]/[↦∗] connective and offset load/store/alloc rules, ported from clutch.diffpriv.derived_laws (Λ-generic; only the diffprivGS Sg / canonical-structure setup is signature-specific). Built on the already-ported wp_alloc/wp_allocN_seq/wp_deref/wp_store heap rules. - proofmode.v: add the GwpTacticsHeap instance so wp_alloc/wp_load/wp_store work in any diffprivGS development (verified: heap tactics resolve S via the GwpTacticsBind instance — no gwp_get_sig routing needed for heap).
…couple_laplace) - gen_prob_lang/inject.v: Inject A val instances for the generic language's val (copy of clutch.common.inject retargeted) so data-as-value case studies port. - lib/laplace.v: Laplace is now a 4-arg notation (num den mean tape) matching the prob_lang Laplace constructor; add hoare_couple_laplace stated on that surface form (reduces the Pair params via wp_pures/tp_pures, then applies the reduced-form wp_couple_laplace). This matches the original diffpriv API so case studies port near-verbatim. (hoare_couple_laplace_exact deferred — used by only one example; needs a reflexive coupling.) - examples/laplace_dp.v: updated for the 4-arg Laplace notation.
…fix tp_bind ectxi - distance.v: Distance class + dZ/dnat/dtensor over gen_prob_lang's val (the prob_lang distance bundles Inject A prob_lang.val, the wrong val). list_dist /dlist deferred (language-independent; add when a list case study needs it). - diffpriv_rules.v: generic sensitivity/DP combinators (wp/hoare_sensitive, wp/hoare_diffpriv(_classic), the composition theorems, hoare_sensitive_Z). Distribution-specific Laplace lemmas moved to lib.laplace per the redesign. inject inside spec contexts uses Val (inject _) (the projected expr type of fill K doesn't trigger Inject_expr resolution). - spec_tactics.v: tp_bind_helper now also peels the ectxi_language.fill head (the spec context flips to ectxi after the first tp_* step), fixing multi-step tp_bind on a stepped spec.
Add wp_couple_sample_tape_gen, the tape-form analogue of wp_couple_sample_gen: couple two labelled samples [Sample i _ #lbl:α] whose tapes are empty. An empty tape's read collapses to a fresh draw from [sig_sample Sg i pv] regardless of the tape's stored descriptor (head_step's empty-match and descriptor-mismatch branches coincide, cf. SampleTapeEmptyS/SampleTapeOtherS), so the DPcoupl obligation is identical to the direct form and the tapes are returned unchanged. This is what makes typing the tape form of Sample sound.
The generalized type system had no rule for the Sample primitive, so the
fundamental theorem covered no program that samples. Make typing
extensible: each sampler brings its own typing rule via a SampleTyping
instance, and the logical relation accommodates them.
typing/types.v:
- ground_val: canonical value shapes at the discrete types.
- Class SampleTyping D tp to {st_eqparam; st_decode; st_out}: the
syntactic side conditions making Sample a sound LR extension.
- typed/val_typed parameterized by the signature Sg; new rules
Sample_typed (TUnit), Sample_tape_typed (TTape), AllocSampleTape_typed.
typing/contextual_refinement.v: thread Sg through typed_ctx; add
CTX_SampleL/CTX_SampleR/CTX_AllocSampleTape items + their typing rules.
interp.v: ground_of_eqtype / interp_of_ground bridge the syntactic
ground_val to the LR value relation (twins of eq_type_sound).
fundamental.v: bin_log_related_sample/_sample_tape/_alloc_sample_tape
(+ refines_alloc_sample_tape_r/l helpers), wired into fundamental and
the precongruence bin_log_related_under_typed_ctx.
families.v: SampleTyping instances for uniform (TNat -> TInt),
laplace/exp/trunc-laplace (Z-noise -> TInt), coin/RR (TInt*TInt -> TBool).
expmech is intentionally not typeable (its list-of-scores parameter is
not an EqType).
sample_typing_canary.v: end-to-end check (typing -> refines_typed;
direct, tape, and context forms).
Generalizes the c2e4e0e1 research lemma refines_sample into the syntactic
type system. All gen_diffpriv examples still build.
Two small randomized programs that compose sampling with the rest of the type system, and the soundness payoff for each: noisy_add : TInt -> TInt -- add a discrete-Laplace draw to the input collide : TNat -> TBool -- allocate a uniform tape, draw twice, test = Each is shown well-typed (exercising Sample_typed / Sample_tape_typed / AllocSampleTape_typed composed with Rec/BinOp/App/UnboxedEq), and then contextually sound against itself (ctx_refines) for free from the fundamental theorem via refines_sound -- a conclusion that was out of reach for any sampling program before this work.
Add two MIXED program-step coupling rules to coupling_rules.v: - wp_couple_sample_tape_l: impl reads an empty tape, spec samples directly - wp_couple_sample_tape_r: impl samples directly, spec reads an empty tape Both reuse the empty-tape-collapses-to-fresh-draw fact (SampleTapeEmptyS/ OtherS) on one side and the direct-draw fact (SampleNoTapeS) on the other, so the DPcoupl obligation is identical to wp_couple_sample_gen and the tape is returned unchanged. New file tape_erasure.v: over the uniform family, prove the tape-erasure equivalence tape_sampler = λ n, let α = AllocSampleTape unif n in Sample unif n α direct_sampler = λ n, Sample unif n #() - tape_refines_direct / direct_refines_tape : REL .. << .. : TNat → TInt (both directions, via the new mixed coupling rules at zero cost) - tape_sampler_ctx_le / tape_sampler_ctx_ge : ctx_refines (both directions), via refines_sound.
…list_mapi Add gwp_list_map_idx: an index-aware spec for plain list_map that is as strong as gwp_list_mapi (per-element pre/postconditions and the meta result may name the logical list index, result is mapi f l), even though list_map's runtime function never receives the index. Soundness: the i-dependence is carried by the positioned resource γ i x, so the i-th call yields f i x. Proof is by induction on the list, instantiating the IH at the index-shifted predicates (γ∘S / ψ∘S / f∘S) via two helper lemmas mapi_loop_S / mapi_cons. Refactor report_noisy_max_generic to drop list_map'/list_mapi from pass 2 of report_noisy_max_presampling, using plain list_map, and replace the two gwp_list_mapi applications in rnm_pres_diffpriv with gwp_list_map_idx (same f/γ/ψ/list arguments). rnm_pres_diffpriv and all other lemma statements are unchanged; downstream importers (report_noisy_max, report_noisy_max_exp, select_then_measure) still build.
Make the immutable-list map combinator typeable at a polymorphic type so the
fundamental theorem can give its relational free theorem, while keeping all
existing gwp-based code working byte-for-byte.
- typing/types.v: add the list type TList τ := μα. () + (τ.[ren(+1)] × α);
the shift makes unfolding compute cleanly to () + τ × TList τ.
- gwp/list.v: add a *separate*, typeable list_map_poly (Λ-thunk type
abstraction + rec_unfold coercion before the match, as the literal value
(λ:"x","x")%V definitionally equal to types.rec_unfold) and its inner loop
list_map_go. The monomorphic list_map and every gwp_list_map* proof are left
unchanged, so all callers (incl. rnm_pres_diffpriv) are unaffected.
- typing/list_typed.v: prove
list_map_poly_typed Sg :
val_typed Sg list_map_poly
(∀: ∀: (#1 → #0) → TList #1 → TList #0)
(with helpers type_unfold_compute and list_cons_typed).
- gen_diffpriv/examples/list.v: repair the semantic relational congruence
refines_list_map_vals / refines_list_map (a let:/match reduction + list_cons
unfold the prior in-progress proof was missing), completing the list_map free
theorem on the value-level list relation lrel_list.
New file rnm_idiomatic.v bridging the presampling report-noisy-max (alloc a noise tape per coordinate in pass 1, read it in pass 2) to a direct- sampling version, via a custom per-element relation and two arrow-relation lemmas that will plug into the relational list_map congruence. - tape_pair_rel : impl (x, #lbl:α) carries a fresh empty tape for family D at parameter mkp x; spec (x', ()) carries nothing; scores related at TInt. - refines_alloc_pair : pass-1 element fns related at interp TInt → tape_pair_rel (impl allocs tape via refines_alloc_sample_tape_l + inv_alloc). - refines_read : pass-2 element fns related at tape_pair_rel → interp TInt; empty-tape read coupled reflexively (zero cost) against the direct draw via wp_couple_sample_tape_l, outputs equal. - Reverse directions refines_alloc_pair' / refines_read' (tape_pair_rel', refines_alloc_sample_tape_r / wp_couple_sample_tape_r) for the eventual equivalence. Zero admits; builds.
…ist_max_index Add the parametricity "free theorems" for the list combinators that the report-noisy-max equivalence proof needs, mirroring refines_list_map: - refines_list_init: related length (lrel_nat) and related index function (lrel_nat -> A) give related score lists (lrel_list A). Proved via a Lob loop invariant over the counter, with a supporting refines_list_rev/ refines_list_rev_aux congruence (the loop reverses its accumulator). - refines_list_max_index: two lists related at lrel_list lrel_int are pointwise-equal integers, so the argmax indices agree; the result is a nat index, hence the conclusion is at lrel_nat. Proved by a Lob congruence over list_fold carrying the running (max, argmax, index) triple related at lrel_int * lrel_nat * lrel_nat in lockstep. Also add the list_max_index / list_max_index_aux definitions to this file (copied verbatim from gen_prob_lang/gwp/list, using the local list_fold). No new admits; file and the map/SVT importers build clean.
…rections)
Pure relational congruence (no fusion, no transitivity): chain the
list_init / list_map / list_max_index congruences from examples.list with
the per-element tape-erasure bridges refines_alloc_pair / refines_read
(and their primed mirrors). Adds the report_noisy_max_presampling and
rnm_direct2 programs (parametric over the abstract noise family D) and the
0-cost equivalences rnm_link1 (presampling << direct2) and rnm_link1'
(direct2 << presampling) at interp TNat, carrying the hypothesis that the
per-index query self-relates at lrel_nat → interp TInt.
The interp-TInt ↔ lrel_int coercion is definitional (interp TInt _ = lrel_int,
interp TNat _ = lrel_nat), so list_max_index's lrel_list lrel_int domain and
interp TNat codomain need no transport. Aligned refines_read/refines_read'
binders ("p" → "x_ι") to match the program's pass-2 lambda exactly.
…ass ≃ direct-1map RNM via map-map fusion
Define the idiomatic one-pass report-noisy-max [rnm_direct1] (a single direct-
sampling [list_map directsample] over the scores; no [(score,())] pairing, no
tape) and prove the FORWARD half of link (II), 0-cost, at [interp TNat]:
rnm_link2 : direct-2pass RNM << direct-1map (idiomatic) RNM.
The bridge is map-map fusion, decomposed into two stages around the
intermediate per-element relation [unit_pair_rel] (impl [(x,())] ~ spec [x']
at [interp TInt]):
* Stage A [wp_pair_pass]/[refines_pair_pass]: the impl [(score,())] pairing
pass is PURE, so it is evaluated LHS-only (via [refines_wp_l]) to a value
list related to the spec score list at [unit_pair_rel]. The [wp] strips
the [lrel_list] guard step-by-step, matching the recursion.
* Stage B [refines_read_directsample] + the [list_map] congruence: the
direct-2pass [read (x,())] and the idiomatic [directsample x'] both reduce
to the same [Sample i (mkpe x) ()] on equal scores, coupled REFLEXIVELY at
zero cost ([DPcoupl_refl_rnm]); the [list_map] congruence then relates the
outer read-map to the direct-sampling map.
[refines_directsample] (unit-form reflexive direct sample) and
[refines_map_map_fusion] (the fusion as a standalone lemma) are also proven.
Whole file compiles; .vo builds; no admits.
The REVERSE half [rnm_link2'] (direct-1map << direct-2pass) is left for a
follow-up: it needs the SPEC pairing map reduced to a value, but the recursive
spec [list_map] over the guarded-recursive [lrel_list] cannot be discharged in
the non-step-indexed [spec_update] (no later-stripping), and the relational
spec-step tactic [rel_pure_r] does not engage with an abstract impl side; there
is no [refines_wp_r] analogue of the [refines_wp_l] used for Stage A forward.
…lf-relation) The DP statements assume the query evalQ #i is Δ-sensitive (hoare_sensitive (evalQ #i) (IZR Δ) dDB dZ). Specialised at the SAME database db, the input distance dDB db db = 0 (distance_0) forces the output distance dZ b b' <= IZR Δ * 0 = 0, and dZ b b' = 0 means b = b'. So at a fixed db the query returns EQUAL integers on both runs at zero cost — exactly the lrel_nat → interp TInt self-relation Hq that the equivalence links rnm_link1/rnm_link2 require. This is the gwp→LR bridge (step 1 of the idiomatic-RNM transport plan).
…ass) Completes the bidirectional equivalence chain presampling ≃ direct2 ≃ direct1 (idiomatic). The reverse link rnm_link2' was the one direction the prompt flagged as blocked: the spec carries the two-pass structure (pairing map then read map) and the impl is a single direct-sampling map, so element-wise lockstep deadlocks (the call-by-value outer read map needs the whole inner pairing map evaluated first, but the spec-only pairing pass has no impl step to strip the lrel_list guarded-recursion later). Broken via refines_list_init_concrete: a list_init coupling that yields the score list as a CONCRETE shared list Z on both sides (rel_concrete_int, an LRel with no later) by tracking the accumulator through the loop — the per-index query returns equal integers (the Hq self-relation), and the trailing list_rev is run on the impl via wp_list_rev and on the spec via a new spec_list_rev (examples.list ships no spec mirror). With the score list concrete, the spec pairing map runs to a value via spec_list_map, and the remaining read-map vs direct-map is the ordinary list_map congruence with the reflexive draw coupling refines_directsample_read.
…pling at lim_exec) The four relational links (rnm_link1/rnm_link2 forward, rnm_link1'/ rnm_link2' reverse) cash out by adequacy into a POINTWISE lim_exec EQUALITY between the one-pass idiomatic rnm_direct1 and the two-pass report_noisy_max_presampling, for any noise family D. Each REL e << e' : interp TNat yields (refines_coupling + DPcoupl_eq_elim at ε=δ=0, exp 0 = 1) a one-directional pointwise ≤; the four links give both directions of presampling ≃ direct2 ≃ direct1, so pointwise antisymmetry (Rle_antisym + distr_ext) closes equality — no termination / mass-1 argument needed. rnm_lim_exec_le is the reusable single-link cash-out. Section renamed idiomatic (was rnm_idiomatic) so the module-qualified lemma names rnm_idiomatic.* resolve for downstream files.
Add theories/gen_diffpriv/examples/gwp_list_rel.v with lrel_list and the relational congruences refines_list_map, refines_list_init, refines_list_max_index for the gen_prob_lang.gwp.list combinators (as used by report_noisy_max_generic), distinct from the examples/list.v combinators. list_init counts DOWN from len, so its congruence is by Coq-nat induction over the loop counter (no list_rev); the loop entry folds the bare Rec to its value form before applying the loop invariant.
Port of rnm_idiomatic.v re-pointed to gen_prob_lang.gwp.list combinators
(the ones the real report_noisy_max_presampling is built from), via the
gwp_list_rel relational congruences. This commit establishes:
- the library-agnostic per-element tape bridges (refines_alloc_pair{,'},
refines_read{,'}, refines_directsample, refines_read_directsample);
- the forward equivalence links rnm_link1 / rnm_link1' (presampling vs
direct-2pass) and rnm_link2 (direct-2pass -> direct-1map);
- wp_pair_pass / refines_pair_pass / refines_map_map_fusion;
- the sensitivity-to-self-relation bridge rnm_query_self_rel.
The wp_pair_pass cons step is re-derived for gwp.list's bare-match list_map
(no rec_unfold coercion): step the head application open while keeping the
recursive call folded, then apply the Loeb IH.
Completes the four-link equivalence over gwp.list:
- refines_list_init_concrete: list_init producing a CONCRETE equal Z-list
via gwp.list's DOWN-counting loop (no spec-side list_rev needed, unlike
examples.list);
- refines_directsample_read, is_list_pair_unit_rel, unit_pair_rel';
- rnm_link2' (direct-1map -> direct-2pass): the spec pairing map is run to a
value via gwp_list_map (g := gwp_spec) (the gwp.list spec-side analogue of
examples.list's bespoke spec_list_map), with the per-element beta discharged
by tp_pures on the gwp_spec element spec.
All four links (rnm_link1/1'/2/2') now hold over the gwp.list combinators.
…mpling
Adds the idiomatic_lim_exec section:
- rnm_lim_exec_le: a single REL e << e' : interp TNat cashes out (via
refines_coupling + DPcoupl_eq_elim at zero cost) to a pointwise lim_exec <=;
- rnm_idiomatic_lim_exec_eq: the one-pass idiomatic rnm_direct1 and the REAL
report_noisy_max_generic.report_noisy_max_presampling sample mass num den
induce the SAME output distribution at every database, by Rle_antisym over
the four gwp.list links (presampling ~ direct2 ~ direct1).
Taking D := mkZNoise sample mass, the section-local presampling program is
DEFINITIONALLY the real one (Hprog by reflexivity), so the equivalence is stated
about the actual program the RNM DP theorem rnm_pres_diffpriv is about, and thus
transports the privacy guarantee to the idiomatic program.
SampleTyping_mkZNoise is only a Lemma for abstract sample/mass, so it is
registered as a Local Instance in the section.
File compiles with zero admits; dune build of the .vo target is green.
…nsport Add the headline result for the IDIOMATIC (direct one-pass sampling, no presampling tapes) Laplace report-noisy-max: report_noisy_max_idiomatic (= rnm_direct1 laplace_family) is differentially private with EXACTLY the rnm_diffpriv_presampling profile. The proof is a pure transport: diffpriv_pure sees the program only through the output-distribution family (lambda db, lim_exec (prog ... db)). rnm_idiomatic_lim_exec_eq (at sample:=laplace_rat, mass:=laplace_rat_mass) gives the pointwise lim_exec equality of the idiomatic and presampling families; functional_extensionality lifts it to a function equality, rewriting the goal to rnm_diffpriv_presampling, which we apply.
Mirror of the Laplace headline for the one-sided exponential noise family: report_noisy_max_exp_idiomatic (= rnm_direct1 exp_family) is differentially private with EXACTLY the rnm_exp_diffpriv_presampling profile. Same pure transport via rnm_idiomatic_lim_exec_eq (at sample:=exp_rat, mass:=exp_rat_mass) + functional_extensionality, reducing to rnm_exp_diffpriv_presampling.
…LR; forward (OCaml) list_init Make list_init/list_map of gen_prob_lang/gwp.list polymorphic and syntactically typeable, so their relational congruences are derived as free theorems from the fundamental theorem instead of by hand: - gwp/list.v: list_init redefined to OCaml-faithful forward/0-indexed semantics ([f 0;…;f(len-1)], evaluated left-to-right via explicit lets to defeat HeapLang's right-to-left pair evaluation). Add list_init_poly / list_map_poly (type-abstracted, rec_unfold) + poly gwp specs gwp_list_map_poly / gwp_list_map_poly_idx. - typing/list_typed.v: list_init_poly_typed at ∀α. int→(int→α)→list α. - gwp_list_rel.v: interp_TList bridge (interp (TList τ) ≡ lrel_list), then refines_list_map / refines_list_init derived for free via fundamental_val + lrel_forall/lrel_arr elimination + the bridge. - report_noisy_max_generic.v: presampling RNM ported to the poly combinators; rnm_init re-proved for the forward list_init; rwp_list_map / wp_alloc_tapes_noise ported to list_map_poly. - report_noisy_max_idiomatic.v: equivalence + refines_list_init_concrete ported to the poly combinators (forward induction). Headlines rnm_diffpriv_idiomatic (Laplace) + rnm_exp_diffpriv_idiomatic (exp) rebuild green; Print Assumptions unchanged (standard axioms only), zero admits.
rnm_idiomatic.v was the first version of the idiomatic-RNM ≡ presampling equivalence, built over examples/list.v's own list combinators rather than the gwp.list combinators the real report-noisy-max uses. When that list-library mismatch was found it was re-pointed to gwp.list as report_noisy_max_idiomatic.v (which the headlines actually use); this file was left behind, imported by nothing. Removing the dead duplication.
…ngruences, idiomatic RNM Weave the gen-prob-lang session's work into the existing README sections (not appended): the extensible per-sampler SYNTACTIC typing (SampleTyping + Sample/AllocSampleTape rules + extended FTLR, the syntactic twin of refines_sample) and the polymorphic typed list combinators whose relational congruences come free from the fundamental theorem (interp (TList τ) ≡ lrel_list); the idiomatic one-pass direct-sampling report-noisy-max, proved DP (rnm_diffpriv_idiomatic / rnm_exp_diffpriv_idiomatic) by a lim_exec equivalence to the presampling RNM built on the tape-erasure law; and the OCaml-faithful forward list_init.
Type the last hand-proved list congruence's combinator so its relational
congruence, too, comes from the fundamental theorem (matching list_map /
list_init):
- gwp/list.v: add list_fold_poly (type-abstracted + rec_unfold) and its
unary spec gwp_list_fold_poly; route list_max_index_aux through it and
insert rec_unfold into list_max_index's match. gwp_list_max_index{,_aux}
statements are unchanged (still return the nat index), so the presampling
DP proof is untouched.
- typing/list_typed.v: list_fold_poly_typed, list_max_index_aux_typed,
list_max_index_typed (list TInt -> TInt).
- gwp_list_rel.v: refines_list_max_index is now a 6-line fundamental_val
derivation (via the interp_TList bridge), replacing the ~78-line manual
coupling. Output relation weakens lrel_nat -> lrel_int (the running index
uses integer +, so the syntactic type is -> TInt); this is sound and
nothing relied on nat-ness — the sole consumer (rnm_lim_exec_le) only
needs the relation to entail eq. Header/comment updated accordingly.
- report_noisy_max_idiomatic.v: ripple interp TNat -> interp TInt through
the four links + rnm_lim_exec_le (the eq side-condition tactic is unchanged).
- README: all three list congruences now documented as free theorems.
Headlines green; Print Assumptions unchanged (standard axioms only); zero admits.
The gen_ectxi_lang/gen_ectx_lang/gen_lang(/lang_markov) canonical chain was
re-declared in essentially every section that worked over a signature. It is
genuinely load-bearing only in the foundational, write-once bare-[Context (S :
Sig)] files (class_instances/erasure/metatheory/wp_tactics/gen_weakestpre mixin/
spec), where generic ectxLanguage/markov lemmas must unify [LanguageOfEctx ?Λ] /
[mstate ?δ] back to [gen_lang S]. In any section that carries a
diffprivGS/diffprivRGS/GenWp Sg instance, [Λ = gen_lang Sg] is recovered from
that instance (and the PureExec/Atomic instances are signature-generic,
reshape_expr is purely syntactic), so the chain was vestigial.
Remove the chain from 17 such sections. Per a needs-based policy: keep
[Local Notation fill := @ectx_language.fill (gen_ectx_lang Sg)] only where [fill]
is used in the body, and a plain [Let gen_markov_X := lang_markov (gen_lang Sg)]
only where the name backs a [spec_updateGS] instance. Document the client idiom
("Working over a signature — no canonical-structure boilerplate") in
gen_diffpriv/README.md.
The chains were section-local, so the .vo interfaces are unchanged; the full
gen_prob_lang + gen_diffpriv subtree rebuilds clean.
origin/main reworked clutch.diffpriv's [spec_coupl]/[prog_coupl] around Kantorovich composition (per-configuration budget functions [E2]/[D2] in place of fixed [ε2]/[δ2] pairs). gen_diffpriv reuses that core verbatim, so three files needed porting: * adequacy.v: [wp_adequacy_spec_coupl] / [wp_adequacy_prog_coupl] now destruct the new three-case [spec_coupl] and the new [prog_coupl], and discharge the coupling via [DPcoupl_dbind_adv_kanto_s_cond] + [erasable_pexec_lim_exec]. Mirrors the new diffpriv/adequacy.v. * coupling_rules.v: [prog_coupl_steps_simple] gained a [□(∀ …, Z … 1%NNR)] premise that is unprovable when Z is the raw WP continuation of [wp_lift_step_prog_couple]. All five sample-coupling rules move to [wp_lift_prim_steps_coupl], which packages that premise. * lib/laplace_choice.v: [prog_coupl_steps] was renamed [prog_coupl_steps_choice] and likewise gained the box premise; the rule moves to [wp_lift_prim_steps_choice]. Proof content is unchanged throughout — only the plumbing around the lifting lemmas. No admits; whole project builds. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Collaborator
|
Lgtm 👍 |
haselwarter
added a commit
that referenced
this pull request
Sep 29, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a variant
gen_prob_langofprob_langthat is generic over a signature of (parametrised) sampling operations. As a case study, thediffprivlogic is ported togen_diffpriv. A few new distributions are added atgen_diffpriv/lib/. For example, the one-sided exponential mechanism is used in a variant of report-noisy-max to achieve better utility with the same privacy as the Laplacian (accuracy is not verified, only privacy). The Clutch type system is also extended to support sampling operations. As a case study, a tape-free version of report-noisy-max is proven contextually equivalent to the presampling-tape version for which the DP proof was presented in the Clutch-DP paper.See here for more detail.