Code

Sparse Vector Mechanism (WIP)#67

Code

Draft

markusdemedeiros wants to merge 100 commits intoleanprover:mainleanprover/SampCert:mainfrom markusdemedeiros:SparseVectormarkusdemedeiros/SampCert:SparseVectorCopy head branch name to clipboard

+3,909-335

Commits

Commits on Oct 28, 2024

• fix adaptive composition

  markusdemedeiros

  committed
  b178344

  Copy full SHA for b178344

• fix definition

  markusdemedeiros

  committed
  d0b4650

  Copy full SHA for d0b4650

• update base proof for gaussian mechanism property

  markusdemedeiros

  committed
  7c1eac8

  Copy full SHA for 7c1eac8

• fix mono

  markusdemedeiros

  committed
  0b0370b

  Copy full SHA for 0b0370b

• fix base proof for approxDP

  markusdemedeiros

  committed
  5f6ef79

  Copy full SHA for 5f6ef79

• new zCDP proofs wrapped

  markusdemedeiros

  committed
  95be45c

  Copy full SHA for 95be45c

• stub changes to system

  markusdemedeiros

  committed
  569d44e

  Copy full SHA for 569d44e

• stub changes to noise

  markusdemedeiros

  committed
  28efc75

  Copy full SHA for 28efc75

• instance for pure DP laplace noise

  markusdemedeiros

  committed
  40ac9cc

  Copy full SHA for 40ac9cc

• pure DP system complete

  markusdemedeiros

  committed
  456514a

  Copy full SHA for 456514a

• count query complete

  markusdemedeiros

  committed
  dfc4b3f

  Copy full SHA for dfc4b3f

• tweak definitions of abstract DP for better inference

  markusdemedeiros

  committed
  dc7ee36

  Copy full SHA for dc7ee36

• cleanup bounded sum abstract proof

  markusdemedeiros

  committed
  00e2ef6

  Copy full SHA for 00e2ef6

• update bounded mean

  markusdemedeiros

  committed
  be8cfd4

  Copy full SHA for be8cfd4

• Histogram update

  markusdemedeiros

  committed
  b064656

  Copy full SHA for b064656

• historgram mean update

  markusdemedeiros

  committed
  edec416

  Copy full SHA for edec416

• instances for zCDP (except approx DP)

  markusdemedeiros

  committed
  592cdea

  Copy full SHA for 592cdea

• checkpoint

  markusdemedeiros

  committed
  e746f46

  Copy full SHA for e746f46

Commits on Oct 29, 2024

• zCDP degrade

  markusdemedeiros

  committed
  4ea177b

  Copy full SHA for 4ea177b

Commits on Oct 30, 2024

• simplify abstract DP presentation further with typeclass synonym

  markusdemedeiros

  committed
  de517ba

  Copy full SHA for de517ba

Commits on Nov 2, 2024

• shorten histogram proofs

  markusdemedeiros

  committed
  2241651

  Copy full SHA for 2241651

• histogram: move epsilons to variable

  markusdemedeiros

  committed
  dc787ef

  Copy full SHA for dc787ef

Commits on Nov 5, 2024

• define SPMF

  markusdemedeiros

  committed
  1b8cf40

  Copy full SHA for 1b8cf40

• SPMF: generic

  markusdemedeiros

  committed
  e4a2f46

  Copy full SHA for e4a2f46

• postprocessing

  markusdemedeiros

  committed
  e023a0f

  Copy full SHA for e023a0f

• update queries to be computable

  markusdemedeiros

  committed
  1b86165

  Copy full SHA for 1b86165

• move SPMF to SLang

  markusdemedeiros

  committed
  b806c8b

  Copy full SHA for b806c8b

• query tests

  markusdemedeiros

  committed
  f75fe5a

  Copy full SHA for f75fe5a

Commits on Nov 12, 2024

• rename adp -> app_dp

  markusdemedeiros

  committed
  0884bac

  Copy full SHA for 0884bac

• Countable -> DiscProbSpace

  markusdemedeiros

  committed
  6372ea0

  Copy full SHA for 6372ea0

• prelim

  markusdemedeiros

  committed
  7d9ba57

  Copy full SHA for 7d9ba57

• checkpoint

  markusdemedeiros

  committed
  cabf7a2

  Copy full SHA for cabf7a2

• checkpoint sv2

  markusdemedeiros

  committed
  0f89042

  Copy full SHA for 0f89042

• checkpoint sv2->sv3

  markusdemedeiros

  committed
  c5e7ee0

  Copy full SHA for c5e7ee0

• checkpoint

  markusdemedeiros

  committed
  4d58b9d

  Copy full SHA for 4d58b9d

• constancy inside the cone of possibility

  markusdemedeiros

  committed
  845ba9f

  Copy full SHA for 845ba9f

• cone_below_zero

  markusdemedeiros

  committed
  4edd572

  Copy full SHA for 4edd572

• external_to_cone_zero

  markusdemedeiros

  committed
  d9c5505

  Copy full SHA for d9c5505

• reduce sv2_eq_sv3 to cone_left_edge_constancy

  markusdemedeiros

  committed
  120b2d7

  Copy full SHA for 120b2d7

• close cone_constancy

  markusdemedeiros

  committed
  3b30b10

  Copy full SHA for 3b30b10

• checkpoint

  markusdemedeiros

  committed
  f030596

  Copy full SHA for f030596

• checkpoint

  markusdemedeiros

  committed
  f38b2ae

  Copy full SHA for f38b2ae

• so close yet so far

  markusdemedeiros

  committed
  7a30a61

  Copy full SHA for 7a30a61

• closer (not really)

  markusdemedeiros

  committed
  b94fd5b

  Copy full SHA for b94fd5b

• explicit presampling is promising

  markusdemedeiros

  committed
  7e33b89

  Copy full SHA for 7e33b89

• checkpoint

  markusdemedeiros

  committed
  8612d16

  Copy full SHA for 8612d16

• sv6 experiment

  markusdemedeiros

  committed
  6a89720

  Copy full SHA for 6a89720

• checkpoint

  markusdemedeiros

  committed
  cde6978

  Copy full SHA for cde6978

• checkpoint

  markusdemedeiros

  committed
  ff23721

  Copy full SHA for ff23721

• sv5 sv6 base case

  markusdemedeiros

  committed
  b32b153

  Copy full SHA for b32b153

• checkpoint explorations into sv6

  markusdemedeiros

  committed
  0a12c1f

  Copy full SHA for 0a12c1f

• work on sv3 admits

  markusdemedeiros

  committed
  82bebcc

  Copy full SHA for 82bebcc

• so close

  markusdemedeiros

  committed
  93ec8f8

  Copy full SHA for 93ec8f8

• sv5 sv6 victory

  markusdemedeiros

  committed
  267c61f

  Copy full SHA for 267c61f

• sketch sv7

  markusdemedeiros

  committed
  6e17ff4

  Copy full SHA for 6e17ff4

• sv8 (definition of G from the paper)

  markusdemedeiros

  committed
  5f3e10e

  Copy full SHA for 5f3e10e

• cleanup

  markusdemedeiros

  committed
  b86c6e0

  Copy full SHA for b86c6e0

• skeleton of privacy argument

  markusdemedeiros

  committed
  b1f7b98

  Copy full SHA for b1f7b98

• sparse vector main proof

  markusdemedeiros

  committed
  44c9e7d

  Copy full SHA for 44c9e7d

• extra sensitivity lemmas

  markusdemedeiros

  committed
  1f7254a

  Copy full SHA for 1f7254a

• checkpoint

  markusdemedeiros

  committed
  7c1d1ae

  Copy full SHA for 7c1d1ae

• base case

  markusdemedeiros

  committed
  85b9a4b

  Copy full SHA for 85b9a4b

• checkpoint

  markusdemedeiros

  committed
  b41d701

  Copy full SHA for b41d701

• Fix build

  markusdemedeiros

  committed
  1489ded

  Copy full SHA for 1489ded

• move executable code to a new file

  markusdemedeiros

  committed
  60c7b74

  Copy full SHA for 60c7b74

• add sparse vector test

  markusdemedeiros

  committed
  22f3fd2

  Copy full SHA for 22f3fd2

• tweak numbers

  markusdemedeiros

  committed
  d08f848

  Copy full SHA for d08f848

• checkpoint

  markusdemedeiros

  committed
  5408fe0

  Copy full SHA for 5408fe0

• vector_sum_singleton

  markusdemedeiros

  committed
  6f8c612

  Copy full SHA for 6f8c612

• minor

  markusdemedeiros

  committed
  45a55c7

  Copy full SHA for 45a55c7

• sv4_presample_split progress

  markusdemedeiros

  committed
  c64d2d9

  Copy full SHA for c64d2d9

• progress on presample_norm_lemma

  markusdemedeiros

  committed
  f94da17

  Copy full SHA for f94da17

• DS0

  markusdemedeiros

  committed
  1a9496a

  Copy full SHA for 1a9496a

• nit

  markusdemedeiros

  committed
  155300c

  Copy full SHA for 155300c

• move remaining sensitivity bounds out of privacy proof

  markusdemedeiros

  committed
  f9a7882

  Copy full SHA for f9a7882

• close vk sensitivity

  markusdemedeiros

  committed
  61f0672

  Copy full SHA for 61f0672

• generalize DS0->DSN

  markusdemedeiros

  committed
  e125c1a

  Copy full SHA for e125c1a

• nit

  markusdemedeiros

  committed
  d4444a4

  Copy full SHA for d4444a4

• privacy is sorry-free

  markusdemedeiros

  committed
  91a8f03

  Copy full SHA for 91a8f03

• minor cleanup

  markusdemedeiros

  committed
  414ca7b

  Copy full SHA for 414ca7b

• list get last lemma

  markusdemedeiros

  committed
  a7ff04f

  Copy full SHA for a7ff04f

• sv8_eq_sv9

  markusdemedeiros

  committed
  9377021

  Copy full SHA for 9377021

• close presample_norm_lemma

  markusdemedeiros

  committed
  572aa68

  Copy full SHA for 572aa68

• close sv6 sv7 eq

  markusdemedeiros

  committed
  2906f3e

  Copy full SHA for 2906f3e

• exactDiffSum eventually constant

  markusdemedeiros

  committed
  4a5e2c7

  Copy full SHA for 4a5e2c7

• checkpoint

  markusdemedeiros

  committed
  9cf0cbb

  Copy full SHA for 9cf0cbb

• checkpoint before deleting sv4_presample_perm

  markusdemedeiros

  committed
  b845bee

  Copy full SHA for b845bee

• sv4_presample_eval

  markusdemedeiros

  committed
  0a533de

  Copy full SHA for 0a533de

• close sv4_presample_split

  markusdemedeiros

  committed
  8173cd7

  Copy full SHA for 8173cd7

• tweak spmf

  markusdemedeiros

  committed
  35ab39e

  Copy full SHA for 35ab39e

• sv1_ub

  markusdemedeiros

  committed
  031af6f

  Copy full SHA for 031af6f

• close iSup tsum lemma

  markusdemedeiros

  committed
  324ab62

  Copy full SHA for 324ab62

• sv1_lb reduction to sv1_cdf_lb

  markusdemedeiros

  committed
  f08a18a

  Copy full SHA for f08a18a

• new attempt

  markusdemedeiros

  committed
  b8c3ea6

  Copy full SHA for b8c3ea6

• checkpoint

  markusdemedeiros

  committed
  b8d910f

  Copy full SHA for b8d910f

• checkpoint

  markusdemedeiros

  committed
  9f35e54

  Copy full SHA for 9f35e54

• skeleton

  markusdemedeiros

  committed
  2e092b3

  Copy full SHA for 2e092b3

• checkpoint

  markusdemedeiros

  committed
  1c1a02d

  Copy full SHA for 1c1a02d

• checkpoint

  markusdemedeiros

  committed
  24e345a

  Copy full SHA for 24e345a

• victory

  markusdemedeiros

  committed
  4948e24

  Copy full SHA for 4948e24