feat: simple mwem

SampCert/DifferentialPrivacy/Pure/Mechanism/Code.lean

@@ -20,3 +20,5 @@ def privNoisedQueryPure (query : List T → ℤ) (Δ : ℕ+) (ε₁ ε₂ : ℕ+
   DiscreteLaplaceGenSamplePMF (Δ * ε₂) ε₁ (query l)
 
 end SLang
+
+end

SampCert/DifferentialPrivacy/Queries/MWEM/Basic.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import SampCert.DifferentialPrivacy.Queries.MWEM.Code
+import SampCert.DifferentialPrivacy.Queries.MWEM.Properties

SampCert/DifferentialPrivacy/Queries/MWEM/Code.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import SampCert.DifferentialPrivacy.Abstract
+import SampCert.DifferentialPrivacy.Pure.System
+import SampCert.DifferentialPrivacy.Queries.ReportNoisyMax.Code
+
+/-!
+# MWEM mechanism (Hardt 2012)
+
+Each round selects a query via Report-Noisy-Max, releases a noisy answer via the
+Laplace mechanism, and post-processes the synthetic state. The synthetic state
+type and update rule are abstracted as a `SyntheticUpdater`, so the privacy
+proof works uniformly over any choice of updater (real-valued multiplicative
+weights, rational, integer, identity, etc.).
+-/
+
+noncomputable section
+
+namespace SLang
+
+variable {X : Type}
+
+structure SyntheticUpdater (X : Type) (n : ℕ) (Δ : ℕ+) (State : Type) (init : State) where
+  queries      : Fin (n+1) → List X → ℤ
+  scoreFn      : State → Fin (n+1) → List X → ℤ
+  update       : State → Fin (n+1) → ℤ → State
+  queries_sens : ∀ i, sensitivity (queries i) Δ
+  scoreFn_sens : ∀ A i, sensitivity (scoreFn A i) Δ
+
+variable {n : ℕ} {Δ : ℕ+} {State : Type} {init : State}
+
+def mwemRound (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) (A : State) :
+    Mechanism X (Fin (n+1) × ℤ) :=
+  privComposeAdaptive
+    (privReportNoisyMax n (U.scoreFn A) Δ ε₁ ε₂)
+    (fun i => privNoisedQueryPure (U.queries i) Δ ε₁ ε₂)
+
+def mwem (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) :
+    ℕ → State → Mechanism X (List (Fin (n+1) × ℤ))
+  | 0,     _ => privConst []
+  | T+1,   A =>
+    privPostProcess
+      (privComposeAdaptive (mwemRound U ε₁ ε₂ A)
+        (fun im => mwem U ε₁ ε₂ T (U.update A im.1 im.2)))
+      (fun (im, hist) => im :: hist)
+
+end SLang
+
+end
+
+namespace SLang
+
+variable {X : Type} {n : ℕ} {Δ : ℕ+} {State : Type} {init : State}
+
+def mwemRoundSLang (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) (A : State)
+    (l : List X) : SLang (Fin (n+1) × ℤ) := do
+  let i ← privReportNoisyMaxSLang n (U.scoreFn A) Δ ε₁ ε₂ l
+  let m ← DiscreteLaplaceGenSample (Δ * ε₂) ε₁ (U.queries i l)
+  return (i, m)
+
+def mwemSLang (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) :
+    ℕ → State → List X → SLang (List (Fin (n+1) × ℤ))
+  | 0, _, _ => probPure []
+  | T+1, A, l =>
+    probBind
+      (probBind (mwemRoundSLang U ε₁ ε₂ A l) (fun im =>
+        probBind (mwemSLang U ε₁ ε₂ T (U.update A im.1 im.2) l) (fun hist =>
+          probPure (im, hist))))
+      (fun p => probPure (p.1 :: p.2))
+
+theorem mwemRoundSLang_eq (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) (A : State)
+    (l : List X) :
+    mwemRoundSLang U ε₁ ε₂ A l = ((mwemRound U ε₁ ε₂ A l : SPMF _) : SLang _) := by
+  show probBind (privReportNoisyMaxSLang n (U.scoreFn A) Δ ε₁ ε₂ l) _ = _
+  rw [privReportNoisyMaxSLang_eq]
+  rfl
+
+theorem mwemSLang_eq (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) :
+    ∀ (T : ℕ) (A : State) (l : List X),
+      mwemSLang U ε₁ ε₂ T A l = ((mwem U ε₁ ε₂ T A l : SPMF _) : SLang _) := by
+  intro T
+  induction T with
+  | zero => intro A l; rfl
+  | succ T IH =>
+    intro A l
+    show probBind (probBind (mwemRoundSLang U ε₁ ε₂ A l) _) _ = _
+    rw [mwemRoundSLang_eq]
+    show probBind (probBind _
+      (fun im : Fin (n+1) × ℤ =>
+        probBind (mwemSLang U ε₁ ε₂ T (U.update A im.1 im.2) l) _)) _ = _
+    conv_lhs => enter [1, 2, im]; rw [IH]
+    rfl
+
+def mwemSPMF (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) (T : ℕ) (A : State)
+    (l : List X) : SPMF (List (Fin (n+1) × ℤ)) :=
+  ⟨ mwemSLang U ε₁ ε₂ T A l, mwemSLang_eq U ε₁ ε₂ T A l ▸ (mwem U ε₁ ε₂ T A l).2 ⟩
+
+end SLang

SampCert/DifferentialPrivacy/Queries/MWEM/Properties.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import SampCert.DifferentialPrivacy.Queries.MWEM.Code
+import SampCert.DifferentialPrivacy.Queries.ReportNoisyMax.Basic
+import SampCert.DifferentialPrivacy.Pure.System
+
+/-!
+# Privacy of MWEM
+
+Each round of MWEM is `2(ε₁/ε₂)`-DP by adaptive composition of Report-Noisy-Max
+and the Laplace mechanism, both `(ε₁/ε₂)`-DP under the sensitivity hypotheses
+of `SyntheticUpdater`. The synthetic state update is post-processing of the
+selection-and-measurement transcript, so it adds no privacy cost. By induction
+over `T` rounds, MWEM is `2T(ε₁/ε₂)`-DP.
+-/
+
+noncomputable section
+
+open Classical Nat Int Real ENNReal
+
+namespace SLang
+
+variable {X : Type} {n : ℕ} {Δ : ℕ+} {State : Type} {init : State}
+
+instance : MeasurableSpace (Fin (n+1) × ℤ) := ⊤
+instance : DiscreteMeasurableSpace (Fin (n+1) × ℤ) where
+  forall_measurableSet _ := .congr trivial rfl
+
+instance : MeasurableSpace (List (Fin (n+1) × ℤ)) := ⊤
+instance : DiscreteMeasurableSpace (List (Fin (n+1) × ℤ)) where
+  forall_measurableSet _ := .congr trivial rfl
+
+theorem mwemRound_DP (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) (ε : NNReal)
+    (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) (A : State) :
+    PureDPSystem.prop (mwemRound U ε₁ ε₂ A) (ε + ε) :=
+  PureDPSystem.adaptive_compose_prop
+    (privReportNoisyMax_DP n (U.scoreFn A) Δ ε₁ ε₂ ε HN (U.scoreFn_sens A))
+    (fun i => privNoisedQueryPure_DP (U.queries i) Δ ε₁ ε₂ ε HN (U.queries_sens i))
+    rfl
+
+theorem mwem_DP (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) (ε : NNReal)
+    (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) (T : ℕ) (A : State) :
+    PureDPSystem.prop (mwem U ε₁ ε₂ T A) (T * (ε + ε)) := by
+  induction T generalizing A with
+  | zero => exact PureDPSystem.const_prop (by push_cast; ring)
+  | succ T IH =>
+    refine PureDPSystem.postprocess_prop <|
+      PureDPSystem.adaptive_compose_prop (mwemRound_DP U ε₁ ε₂ ε HN A)
+        (fun im => IH (U.update A im.1 im.2)) ?_
+    push_cast; ring
+
+theorem mwemSPMF_DP (U : SyntheticUpdater X n Δ State init) (ε₁ ε₂ : ℕ+) (ε : NNReal)
+    (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) (T : ℕ) (A : State) :
+    PureDPSystem.prop (mwemSPMF U ε₁ ε₂ T A) (T * (ε + ε)) := by
+  have heq : (fun l => mwemSPMF U ε₁ ε₂ T A l) = (fun l => (mwem U ε₁ ε₂ T A l : SPMF _)) := by
+    funext l
+    apply Subtype.ext
+    exact mwemSLang_eq U ε₁ ε₂ T A l
+  rw [show mwemSPMF U ε₁ ε₂ T A = _ from heq]
+  exact mwem_DP U ε₁ ε₂ ε HN T A
+
+end SLang
+
+end

SampCert/DifferentialPrivacy/Queries/MWEM/Updaters/Float.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import SampCert.DifferentialPrivacy.Queries.MWEM.Code
+
+/-!
+# Float-valued multiplicative-weights updater
+
+Hardt's MWEM (Hardt, Ligett, McSherry 2012, Algorithm 1) with the synthetic
+state implemented in IEEE-754 doubles. This is the representation used by
+deployed systems (SmartNoise, etc.).
+
+The synthetic state lives in `Fin numBins → Float`. Following Figure 1 of the
+paper:
+
+* `A_0` is the uniform distribution scaled by `n` (dataset size), so each bin
+  starts with mass `n / numBins` and the total is `n`.
+* The update rule for each round `i` is
+    `A_i(x) ∝ A_{i-1}(x) · exp( q_i(x) · (m_i - q_i(A_{i-1})) / (2n) )`
+  with renormalization to fixed total `n`.
+
+Privacy comes from the Laplace mechanism in the measurement step, which uses
+exact integer arithmetic. The Float update is post-processing of the integer
+transcript and contributes no privacy cost. Lean's Float type has essentially
+no axiomatic theory, but the privacy proof requires only that the update be a
+total function of its arguments.
+
+The score function uses `Float.toInt32` to produce an integer constant (in `D`)
+for sensitivity reasons; its specific value depends on IEEE-754 semantics but
+is irrelevant to the sensitivity bound.
+-/
+
+open Classical Nat Int Real ENNReal
+
+namespace SLang
+
+variable {numBins : ℕ+} {n : ℕ} {Δ : ℕ+}
+
+def intToFloat (n : ℤ) : Float :=
+  match n with
+  | .ofNat k => k.toUInt64.toFloat
+  | .negSucc k => -((k + 1).toUInt64.toFloat)
+
+def floatToInt (x : Float) : ℤ := x.toInt32.toInt
+
+def floatLinearQuery (q : Fin numBins → ℤ) (D : List (Fin numBins)) : ℤ :=
+  (D.map q).sum
+
+def floatLinearQueryFloat (q : Fin numBins → ℤ) (A : Fin numBins → Float) : Float :=
+  ((List.finRange numBins).map (fun b => intToFloat (q b) * A b)).foldr (· + ·) 0.0
+
+def floatScore (q : Fin numBins → ℤ) (A : Fin numBins → Float) (D : List (Fin numBins)) : ℤ :=
+  |floatLinearQuery q D - floatToInt (floatLinearQueryFloat q A)|
+
+def floatMWUpdate (n : ℕ) (q : Fin numBins → ℤ) (m : ℤ) (A : Fin numBins → Float) :
+    Fin numBins → Float :=
+  let nF : Float := intToFloat (n : ℤ)
+  let err : Float := (intToFloat m - floatLinearQueryFloat q A) / (2.0 * nF)
+  let unnorm : Fin numBins → Float := fun b => A b * Float.exp (intToFloat (q b) * err)
+  let total : Float :=
+    ((List.finRange numBins).map unnorm).foldr (· + ·) 0.0
+  fun b => unnorm b * nF / total
+
+def floatInit (n : ℕ) (numBins : ℕ+) : Fin numBins → Float :=
+  fun _ => intToFloat (n : ℤ) / intToFloat (numBins.val : ℤ)
+
+theorem floatLinearQuery_sens (q : Fin numBins → ℤ)
+    (Hbound : ∀ b, |q b| ≤ (Δ : ℤ)) : sensitivity (floatLinearQuery q) Δ := by
+  intro l₁ l₂ Hn
+  have qnat : ∀ k : Fin numBins, (q k).natAbs ≤ (Δ : ℕ) := fun k => by
+    have := Hbound k; rw [Int.abs_eq_natAbs] at this; exact_mod_cast this
+  cases Hn with
+  | @Addition a b k h1 h2 => subst h1 h2; simp [floatLinearQuery]; exact qnat _
+  | @Deletion a b k h1 h2 => subst h1 h2; simp [floatLinearQuery]; exact qnat _
+
+lemma natAbs_abs_sub_abs_le' {a b : ℤ} : (|a| - |b|).natAbs ≤ (a - b).natAbs := by
+  zify; exact abs_abs_sub_abs_le_abs_sub a b
+
+theorem floatScore_sens (q : Fin numBins → ℤ) (A : Fin numBins → Float)
+    (Hbound : ∀ b, |q b| ≤ (Δ : ℤ)) : sensitivity (floatScore q A) Δ := by
+  intro l₁ l₂ Hn
+  have hQ : (floatLinearQuery q l₁ - floatLinearQuery q l₂).natAbs ≤ (Δ : ℕ) :=
+    floatLinearQuery_sens (Δ := Δ) q Hbound l₁ l₂ Hn
+  set c : ℤ := floatToInt (floatLinearQueryFloat q A)
+  show (|floatLinearQuery q l₁ - c| - |floatLinearQuery q l₂ - c|).natAbs ≤ (Δ : ℕ)
+  refine le_trans natAbs_abs_sub_abs_le' ?_
+  rw [show floatLinearQuery q l₁ - c - (floatLinearQuery q l₂ - c) =
+        floatLinearQuery q l₁ - floatLinearQuery q l₂ from by ring]
+  exact hQ
+
+def floatMWUpdater (nData : ℕ) (q : Fin (n+1) → Fin numBins → ℤ)
+    (Hbound : ∀ i b, |q i b| ≤ (Δ : ℤ)) :
+    SyntheticUpdater (Fin numBins) n Δ (Fin numBins → Float) (floatInit nData numBins) where
+  queries i := floatLinearQuery (q i)
+  scoreFn A i := floatScore (q i) A
+  update A i m := floatMWUpdate nData (q i) m A
+  queries_sens i := floatLinearQuery_sens (q i) (Hbound i)
+  scoreFn_sens A i := floatScore_sens (q i) A (Hbound i)
+
+end SLang

SampCert/DifferentialPrivacy/Queries/MWEM/Updaters/Real.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import SampCert.DifferentialPrivacy.Queries.MWEM.Code
+
+/-!
+# Real-valued multiplicative-weights updater
+
+Hardt's MWEM (Hardt, Ligett, McSherry 2012, Algorithm 1) with the synthetic
+state in `Fin numBins → NNReal`. This is the textbook reference instantiation;
+not extractable to executable code (uses `Real.exp` and real arithmetic).
+
+Following Figure 1 of the paper:
+
+* `A_0(x) = n / numBins` for all `x` (uniform with total mass `n`).
+* The update for round `i` is
+    `A_i(x) ∝ A_{i-1}(x) · exp( q_i(x) · (m_i - q_i(A_{i-1})) / (2n) )`
+  with renormalization to fixed total `n`.
+
+If the renormalization total degenerates to zero, the updater returns the zero
+histogram. The privacy proof does not depend on non-degeneracy.
+-/
+
+noncomputable section
+
+open Classical Nat Int Real ENNReal NNReal
+
+namespace SLang
+
+variable {numBins : ℕ+} {n : ℕ} {Δ : ℕ+}
+
+def realLinearQuery (q : Fin numBins → ℤ) (D : List (Fin numBins)) : ℤ :=
+  (D.map q).sum
+
+def realLinearQueryReal (q : Fin numBins → ℤ) (A : Fin numBins → NNReal) : ℝ :=
+  ∑ b, (q b : ℝ) * (A b : ℝ)
+
+def realScore (q : Fin numBins → ℤ) (A : Fin numBins → NNReal) (D : List (Fin numBins)) : ℤ :=
+  |realLinearQuery q D - ⌊realLinearQueryReal q A⌋|
+
+def realMWUpdate (n : ℕ) (q : Fin numBins → ℤ) (m : ℤ) (A : Fin numBins → NNReal) :
+    Fin numBins → NNReal :=
+  let nR : ℝ := (n : ℝ)
+  let err : ℝ := ((m : ℝ) - realLinearQueryReal q A) / (2 * nR)
+  let unnorm : Fin numBins → ℝ := fun b => (A b : ℝ) * Real.exp ((q b : ℝ) * err)
+  let total : ℝ := ∑ b, unnorm b
+  fun b => Real.toNNReal (unnorm b * nR / total)
+
+def realInit (n : ℕ) (numBins : ℕ+) : Fin numBins → NNReal :=
+  fun _ => Real.toNNReal ((n : ℝ) / (numBins.val : ℝ))
+
+theorem realLinearQuery_sens (q : Fin numBins → ℤ)
+    (Hbound : ∀ b, |q b| ≤ (Δ : ℤ)) : sensitivity (realLinearQuery q) Δ := by
+  intro l₁ l₂ Hn
+  have qnat : ∀ k : Fin numBins, (q k).natAbs ≤ (Δ : ℕ) := fun k => by
+    have := Hbound k; rw [Int.abs_eq_natAbs] at this; exact_mod_cast this
+  cases Hn with
+  | @Addition a b k h1 h2 => subst h1 h2; simp [realLinearQuery]; exact qnat _
+  | @Deletion a b k h1 h2 => subst h1 h2; simp [realLinearQuery]; exact qnat _
+
+lemma natAbs_abs_sub_abs_le {a b : ℤ} : (|a| - |b|).natAbs ≤ (a - b).natAbs := by
+  zify; exact abs_abs_sub_abs_le_abs_sub a b
+
+theorem realScore_sens (q : Fin numBins → ℤ) (A : Fin numBins → NNReal)
+    (Hbound : ∀ b, |q b| ≤ (Δ : ℤ)) : sensitivity (realScore q A) Δ := by
+  intro l₁ l₂ Hn
+  have hQ : (realLinearQuery q l₁ - realLinearQuery q l₂).natAbs ≤ (Δ : ℕ) :=
+    realLinearQuery_sens (Δ := Δ) q Hbound l₁ l₂ Hn
+  set c : ℤ := ⌊realLinearQueryReal q A⌋
+  show (|realLinearQuery q l₁ - c| - |realLinearQuery q l₂ - c|).natAbs ≤ (Δ : ℕ)
+  refine le_trans natAbs_abs_sub_abs_le ?_
+  rw [show realLinearQuery q l₁ - c - (realLinearQuery q l₂ - c) =
+        realLinearQuery q l₁ - realLinearQuery q l₂ from by ring]
+  exact hQ
+
+def realMWUpdater (nData : ℕ) (q : Fin (n+1) → Fin numBins → ℤ)
+    (Hbound : ∀ i b, |q i b| ≤ (Δ : ℤ)) :
+    SyntheticUpdater (Fin numBins) n Δ (Fin numBins → NNReal) (realInit nData numBins) where
+  queries i := realLinearQuery (q i)
+  scoreFn A i := realScore (q i) A
+  update A i m := realMWUpdate nData (q i) m A
+  queries_sens i := realLinearQuery_sens (q i) (Hbound i)
+  scoreFn_sens A i := realScore_sens (q i) A (Hbound i)
+
+end SLang
+
+end

SampCert/DifferentialPrivacy/Queries/ReportNoisyMax/Basic.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import SampCert.DifferentialPrivacy.Queries.ReportNoisyMax.Code
+import SampCert.DifferentialPrivacy.Queries.ReportNoisyMax.Properties