Code

Restructure definitions of DP#68

Code

Open

markusdemedeiros wants to merge 30 commits intoleanprover:mainleanprover/SampCert:mainfrom markusdemedeiros:restructure-DPmarkusdemedeiros/SampCert:restructure-DPCopy head branch name to clipboard

+478-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