SampCert - GitLite

KO | EN

gitlite — search

#react #typescript #llm #golang #machine-learning #deep-learning #macos #nodejs #cli #kubernetes #awesome-list #security #pytorch #mcp

SampCert

(★ 103)

SampCert : Verified Differential Privacy

File Explorer

Download Latest Version (.zip)

- - ffitest.yml
  - lean_build.yml
  - static.yml
- - Abstract.lean
  - Generic.lean
  - Neighbours.lean
  - RenyiDivergence.lean
  - Sensitivity.lean
- - Align.lean
  - Dafny.lean
  - Export.lean
  - Extension.lean
  - IR.lean
  - IRToDafny.lean
  - Print.lean
  - Translate.lean
  - VMC.lean
- - Auto.lean
  - Basic.lean
  - Monad.lean
  - UniformByte.lean
  - UniformP2.lean
  - Until.lean
  - While.lean
- - Log.lean
  - Shift.lean
  - Util.lean
  - UtilMathlib.lean
- Extraction.lean
- SLang.lean
- benchmarks.py
- discretegauss.py
- IBM
- Load.py
- Random.py
- README.md
- run_benchmark.sh
- testing-kolmogorov-discretegaussian.py
- testing-kolmogorov-discretelaplace.py
.gitignore
.gitmodules
CITATION.cff
CONTRIBUTING.md
Dockerfile
FastExtract.lean
ffi.cpp
index.html
lake-manifest.json
lakefile.lean
lean-toolchain
LICENSE
paper_mapping.md
pbuild.sh
README.md
REPRODUCING.md
SampCert.lean
SampCertCheck.lean
Test.lean
VMC.lean

# Installation Guide

1. Get the code

git clone https://github.com/leanprover/SampCert

Downloads the entire project code from GitHub to your computer.

cd SampCert

Moves into the project folder you just downloaded.

2. Docker

Easy Recommended

Prerequisites

Git Needed to download the project code from GitHub.
Docker Desktop Needed to build and run containers. Install it and keep it running in the background.

docker build -t sampcert .

Builds a runnable image based on the Dockerfile.

docker run -p 8080:80 sampcert

Runs the built image as an actual container.

✅ Run docker compose ps to check the containers are Up. If the README mentions a port, open http://localhost:PORT in your browser.

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# SampCert

A verified implementation using [Lean](https://github.com/leanprover/lean4) and [Mathlib](https://github.com/leanprover-community/mathlib4) of randomized algorithms including [the discrete Gaussian sampler for differential privacy](https://arxiv.org/abs/2004.00010), key results in [zero concentrated differential privacy](https://arxiv.org/abs/1605.02065), and [some verified (unbounded) private queries](https://arxiv.org/pdf/1909.01917).

SampCert is deployed and used in the [AWS Clean Rooms Differential Privacy service](https://docs.aws.amazon.com/clean-rooms/latest/userguide/differential-privacy.html#dp-overview). SampCert proves deep properties about some of its randomized algorithm and makes heavy use of Mathlib. For example, we use theorems such as [the Poisson summation formula](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Fourier/PoissonSummation.html#Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay).

The principal developer of SampCert is [Jean-Baptiste Tristan](https://jtristan.github.io/). It is also developed by [Markus de Medeiros](https://www.markusde.ca/).

Other people have contributed important ideas or tools for deployment including (in no particular order): Leo de Moura, Anjali Joshi, Joseph Tassarotti, Stefan Zetzsche, Aws Albharghouti, Muhammad Naveed, Tristan Ravitch, Fabian Zaiser, Tomas Skrivan.

To cite SampCert you can currently use the following reference:
```
@software{Tristan_SampCert_Verified_2024,
author = {Tristan, Jean-Baptiste},
doi = {10.5281/zenodo.11204806},
month = may,
title = {{SampCert : Verified Differential Privacy}},
url = {https://github.com/leanprover/SampCert},
version = {1.0.0},
year = {2024}
}
```