clutch.gen_diffpriv.all
Aggregator for the generic differential-privacy logic — import this to get
the whole stack (language, spec, WP core, logical relation, sampling typing,
sensitivity/DP combinators). Per-distribution surface libraries (e.g.
gen_diffpriv.lib.laplace) are imported separately.
From clutch.gen_prob_lang Require Export notation tactics metatheory lang inject.
From clutch.gen_prob_lang.spec Require Export spec_rules spec_tactics.
(* WP core reused as-is from the monomorphic development *)
From clutch.diffpriv Require Export weakestpre lifting ectx_lifting.
From clutch.gen_diffpriv Require Export
primitive_laws derived_laws proofmode coupling_rules
model interp app_rel_rules rel_tactics compatibility fundamental soundness
adequacy adequacy_rel distance diffpriv_rules sample.
From clutch.gen_prob_lang.spec Require Export spec_rules spec_tactics.
(* WP core reused as-is from the monomorphic development *)
From clutch.diffpriv Require Export weakestpre lifting ectx_lifting.
From clutch.gen_diffpriv Require Export
primitive_laws derived_laws proofmode coupling_rules
model interp app_rel_rules rel_tactics compatibility fundamental soundness
adequacy adequacy_rel distance diffpriv_rules sample.