From 5141a19364d78a8fd13d0892ed9e9dbc670da5ac Mon Sep 17 00:00:00 2001 From: John Tristan Date: Thu, 16 May 2024 11:54:00 -0400 Subject: [PATCH] Update README.md --- README.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/README.md b/README.md index b1650297..d971dcc7 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,6 @@ # SampCert -A verified implementation using [Lean](https://github.com/leanprover/lean4) and [Mathlib](https://github.com/leanprover-community/mathlib4) of [the discrete Gaussian sampler for differential privacy](https://arxiv.org/abs/2004.00010). - -We prove that the sampling algorithm has the appropriate mass function. +A verified implementation using [Lean](https://github.com/leanprover/lean4) and [Mathlib](https://github.com/leanprover-community/mathlib4) of [the discrete Gaussian sampler for differential privacy](https://arxiv.org/abs/2004.00010), the composition and postprocessing of zero concentrated differential privacy, and some simple queries. The Lean implementation is not computable because algorithms that terminate with probability 1 are defined using a combinator. However, the code can be extracted to [Dafny](https://dafny.org/) and used as part of the [VMC library](https://github.com/dafny-lang/Dafny-VMC).