Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Sparse Vector Mechanism (WIP) #67

Draft
wants to merge 100 commits into
base: main
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
100 commits
Select commit Hold shift + click to select a range
b178344
fix adaptive composition
markusdemedeiros Oct 28, 2024
d0b4650
fix definition
markusdemedeiros Oct 28, 2024
7c1eac8
update base proof for gaussian mechanism property
markusdemedeiros Oct 28, 2024
0b0370b
fix mono
markusdemedeiros Oct 28, 2024
5f6ef79
fix base proof for approxDP
markusdemedeiros Oct 28, 2024
95be45c
new zCDP proofs wrapped
markusdemedeiros Oct 28, 2024
569d44e
stub changes to system
markusdemedeiros Oct 28, 2024
28efc75
stub changes to noise
markusdemedeiros Oct 28, 2024
40ac9cc
instance for pure DP laplace noise
markusdemedeiros Oct 28, 2024
456514a
pure DP system complete
markusdemedeiros Oct 28, 2024
dfc4b3f
count query complete
markusdemedeiros Oct 28, 2024
dc7ee36
tweak definitions of abstract DP for better inference
markusdemedeiros Oct 28, 2024
00e2ef6
cleanup bounded sum abstract proof
markusdemedeiros Oct 28, 2024
be8cfd4
update bounded mean
markusdemedeiros Oct 28, 2024
b064656
Histogram update
markusdemedeiros Oct 28, 2024
edec416
historgram mean update
markusdemedeiros Oct 28, 2024
592cdea
instances for zCDP (except approx DP)
markusdemedeiros Oct 28, 2024
e746f46
checkpoint
markusdemedeiros Oct 28, 2024
4ea177b
zCDP degrade
markusdemedeiros Oct 29, 2024
de517ba
simplify abstract DP presentation further with typeclass synonym
markusdemedeiros Oct 30, 2024
2241651
shorten histogram proofs
markusdemedeiros Nov 2, 2024
dc787ef
histogram: move epsilons to variable
markusdemedeiros Nov 2, 2024
1b8cf40
define SPMF
markusdemedeiros Nov 5, 2024
e4a2f46
SPMF: generic
markusdemedeiros Nov 5, 2024
e023a0f
postprocessing
markusdemedeiros Nov 5, 2024
1b86165
update queries to be computable
markusdemedeiros Nov 5, 2024
b806c8b
move SPMF to SLang
markusdemedeiros Nov 5, 2024
f75fe5a
query tests
markusdemedeiros Nov 5, 2024
0884bac
rename adp -> app_dp
markusdemedeiros Nov 12, 2024
6372ea0
Countable -> DiscProbSpace
markusdemedeiros Nov 12, 2024
7d9ba57
prelim
markusdemedeiros Sep 25, 2024
cabf7a2
checkpoint
markusdemedeiros Sep 26, 2024
0f89042
checkpoint sv2
markusdemedeiros Sep 26, 2024
c5e7ee0
checkpoint sv2->sv3
markusdemedeiros Sep 26, 2024
4d58b9d
checkpoint
markusdemedeiros Sep 26, 2024
845ba9f
constancy inside the cone of possibility
markusdemedeiros Sep 30, 2024
4edd572
cone_below_zero
markusdemedeiros Sep 30, 2024
d9c5505
external_to_cone_zero
markusdemedeiros Sep 30, 2024
120b2d7
reduce sv2_eq_sv3 to cone_left_edge_constancy
markusdemedeiros Sep 30, 2024
3b30b10
close cone_constancy
markusdemedeiros Oct 1, 2024
f030596
checkpoint
markusdemedeiros Oct 1, 2024
f38b2ae
checkpoint
markusdemedeiros Oct 6, 2024
7a30a61
so close yet so far
markusdemedeiros Oct 7, 2024
b94fd5b
closer (not really)
markusdemedeiros Oct 7, 2024
7e33b89
explicit presampling is promising
markusdemedeiros Oct 7, 2024
8612d16
checkpoint
markusdemedeiros Oct 7, 2024
6a89720
sv6 experiment
markusdemedeiros Oct 8, 2024
cde6978
checkpoint
markusdemedeiros Oct 28, 2024
ff23721
checkpoint
markusdemedeiros Nov 3, 2024
b32b153
sv5 sv6 base case
markusdemedeiros Nov 3, 2024
0a12c1f
checkpoint explorations into sv6
markusdemedeiros Nov 3, 2024
82bebcc
work on sv3 admits
markusdemedeiros Nov 3, 2024
93ec8f8
so close
markusdemedeiros Nov 4, 2024
267c61f
sv5 sv6 victory
markusdemedeiros Nov 4, 2024
6e17ff4
sketch sv7
markusdemedeiros Nov 4, 2024
5f3e10e
sv8 (definition of G from the paper)
markusdemedeiros Nov 4, 2024
b86c6e0
cleanup
markusdemedeiros Nov 4, 2024
b1f7b98
skeleton of privacy argument
markusdemedeiros Nov 4, 2024
44c9e7d
sparse vector main proof
markusdemedeiros Nov 4, 2024
1f7254a
extra sensitivity lemmas
markusdemedeiros Nov 4, 2024
7c1d1ae
checkpoint
markusdemedeiros Nov 4, 2024
85b9a4b
base case
markusdemedeiros Nov 5, 2024
b41d701
checkpoint
markusdemedeiros Nov 5, 2024
1489ded
Fix build
markusdemedeiros Nov 5, 2024
60c7b74
move executable code to a new file
markusdemedeiros Nov 5, 2024
22f3fd2
add sparse vector test
markusdemedeiros Nov 5, 2024
d08f848
tweak numbers
markusdemedeiros Nov 5, 2024
5408fe0
checkpoint
markusdemedeiros Nov 5, 2024
6f8c612
vector_sum_singleton
markusdemedeiros Nov 6, 2024
45a55c7
minor
markusdemedeiros Nov 6, 2024
c64d2d9
sv4_presample_split progress
markusdemedeiros Nov 6, 2024
f94da17
progress on presample_norm_lemma
markusdemedeiros Nov 6, 2024
1a9496a
DS0
markusdemedeiros Nov 6, 2024
155300c
nit
markusdemedeiros Nov 6, 2024
f9a7882
move remaining sensitivity bounds out of privacy proof
markusdemedeiros Nov 6, 2024
61f0672
close vk sensitivity
markusdemedeiros Nov 6, 2024
e125c1a
generalize DS0->DSN
markusdemedeiros Nov 6, 2024
d4444a4
nit
markusdemedeiros Nov 6, 2024
91a8f03
privacy is sorry-free
markusdemedeiros Nov 6, 2024
414ca7b
minor cleanup
markusdemedeiros Nov 6, 2024
a7ff04f
list get last lemma
markusdemedeiros Nov 7, 2024
9377021
sv8_eq_sv9
markusdemedeiros Nov 7, 2024
572aa68
close presample_norm_lemma
markusdemedeiros Nov 7, 2024
2906f3e
close sv6 sv7 eq
markusdemedeiros Nov 7, 2024
4a5e2c7
exactDiffSum eventually constant
markusdemedeiros Nov 7, 2024
9cf0cbb
checkpoint
markusdemedeiros Nov 7, 2024
b845bee
checkpoint before deleting sv4_presample_perm
markusdemedeiros Nov 7, 2024
0a533de
sv4_presample_eval
markusdemedeiros Nov 7, 2024
8173cd7
close sv4_presample_split
markusdemedeiros Nov 7, 2024
35ab39e
tweak spmf
markusdemedeiros Nov 8, 2024
031af6f
sv1_ub
markusdemedeiros Nov 8, 2024
324ab62
close iSup tsum lemma
markusdemedeiros Nov 8, 2024
f08a18a
sv1_lb reduction to sv1_cdf_lb
markusdemedeiros Nov 8, 2024
b8c3ea6
new attempt
markusdemedeiros Nov 8, 2024
b8d910f
checkpoint
markusdemedeiros Nov 9, 2024
9f35e54
checkpoint
markusdemedeiros Nov 9, 2024
2e092b3
skeleton
markusdemedeiros Nov 9, 2024
1c1a02d
checkpoint
markusdemedeiros Nov 9, 2024
24e345a
checkpoint
markusdemedeiros Nov 9, 2024
4948e24
victory
markusdemedeiros Nov 9, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
close sv4_presample_split
  • Loading branch information
markusdemedeiros committed Nov 12, 2024
commit 8173cd796abd2964dec57b6a633666bf779b74d5
152 changes: 96 additions & 56 deletions SampCert/DifferentialPrivacy/Queries/UnboundedMax/Properties.lean
Original file line number Diff line number Diff line change
@@ -717,6 +717,11 @@ lemma sv4_presample_eval (ε₁ ε₂ : ℕ+) (n : ℕ) (s : { l : List ℤ // L
rw [mul_comm]
simp

lemma sv4_presample_eval' (ε₁ ε₂ : ℕ+) (n : ℕ) (s : { l : List ℤ // List.length l = n }) :
sv4_presample ε₁ ε₂ n s = List.foldl (fun acc b => acc * (privNoiseGuess ε₁ ε₂ b)) 1 (List.reverse s) := by
have X := sv4_presample_eval ε₁ ε₂ n ⟨ List.reverse s, by simp ⟩
simp only [List.reverse_reverse, Subtype.coe_eta] at X
trivial



@@ -886,71 +891,106 @@ def sv4_presample_split (ε₁ ε₂ : ℕ+) (point : ℕ) :
rw [vector_sum_merge]
rw [vector_sum_merge]

-- Bots sums are singletons


sorry


/-
-- Both sums are singletons
simp [vsm_rest, vsm_0]
symm
rw [ENNReal.tsum_eq_add_tsum_ite final_state]
-- rcases final_state with ⟨ f, Hf ⟩
-- simp
conv =>
rhs
rw [<- (zero_add (tsum _))]
conv =>
lhs
rw [add_comm]
congr 1
· simp
intro A B C D
exfalso
rcases final_state with ⟨ f, Hf ⟩
simp_all
apply C
rw [list_lemma_1 ?G1]
intro K
simp_all

-- There is a bijection here
apply @tsum_eq_tsum_of_ne_zero_bij
case i => exact fun x => ⟨ vsm_last x.1 :: vsm_init x.1 , by simp ⟩
· simp [Function.Injective]
intro A B C D E F H I J K
simp_all [vsm_rest, vsm_init]
rw [<- @list_lemma_1 E ?G1]
case G1 => intro K; simp [K] at F
rw [<- @list_lemma_1 A ?G1]
case G1 => intro K; simp [K] at B
cases C
symm
congr 1
· simp [Function.support, Set.range, DFunLike.coe]
rw [ENNReal.tsum_eq_add_tsum_ite ⟨[vsm_last final_state] ++ (vsm_init final_state), by simp ⟩ ]
conv =>
lhs
rw [<- (add_zero (@ite _ _ _ _ _))]
rw [add_comm]
conv =>
rhs
rw [add_comm]
congr 1
· symm
simp
intro A B C D
exfalso
rcases final_state with ⟨ f, Hf ⟩
exists f
simp_all [vsm_rest, vsm_0, vsm_last, vsm_init]
apply C
rw [List.getLastI_eq_getLast?]
unfold Option.iget
simp
exists Hf
apply And.intro
· apply And.intro
· rw [list_lemma_1]
intro K
simp_all
· intro K
apply D
sorry
-- rw [<- K]
-- congr
-- cases C
-- · sorry
-- · sorry
· cases C
simp [vsm_last, vsm_rest, vsm_init]
cases A
· simp at B
simp
rename_i A0 A1
rw [List.getLastI_eq_getLast?]
rw [List.getLast?_concat]
simp [Function.support]
intro A B ⟨ C, D ⟩
simp [vsm_init, vsm_last]
rw [list_lemma_1]
intro K
simp_all

-- Apply the closed form to evaluate
rcases final_state with ⟨ f, Hf ⟩
simp_all
simp [vsm_rest, vsm_0, vsm_last, vsm_init]
rw [sv4_presample_eval']
rw [sv4_presample_eval']
simp only []

have Hfoldl_eq :
(List.foldl (fun acc b => acc * (privNoiseGuess ε₁ ε₂) b) 1 (f.tail ++ [f.headI]).reverse =
List.foldl (fun acc b => acc * (privNoiseGuess ε₁ ε₂) b) 1 (f.dropLast ++ [f.getLastI]).reverse):= by
apply List.Perm.foldl_eq
· intro A B C
simp
rw [mul_assoc]
rw [mul_assoc]
congr 1
rw [mul_comm]
· conv =>
lhs
simp
have H1 : (f.headI :: f.tail.reverse).Perm (f.headI :: f.tail) := by
apply List.Perm.cons f.headI
apply List.reverse_perm
trans
· apply H1
rw [list_lemma_1 ?G2]
case G2 => intro _ ; simp_all
rw [list_lemma_2 ?G2]
case G2 => intro _ ; simp_all
apply List.Perm.symm
apply List.reverse_perm
rw [Hfoldl_eq]
clear Hfoldl_eq
generalize HX : List.foldl (fun acc b => acc * (privNoiseGuess ε₁ ε₂) b) 1 (f.dropLast ++ [f.getLastI]).reverse = X
clear HX

-- Both of the conditionals are true
split
· congr 2
sorry
· sorry
-/




· split
· rfl
· exfalso
rename_i A B
apply B
rw [list_lemma_2]
intro K
simp [K] at Hf
· split
· exfalso
rename_i A B
apply A
rw [list_lemma_1]
intro K
simp [K] at Hf
· rfl