From c0d18249f8d0832d673e76da66308cdc60149b60 Mon Sep 17 00:00:00 2001 From: John Tristan Date: Thu, 15 Aug 2024 12:46:19 -0400 Subject: [PATCH 1/3] Removing old builds --- SampCertCheck.lean | 16 ---------------- lakefile.lean | 15 --------------- 2 files changed, 31 deletions(-) delete mode 100644 SampCertCheck.lean diff --git a/SampCertCheck.lean b/SampCertCheck.lean deleted file mode 100644 index 3d88ac19..00000000 --- a/SampCertCheck.lean +++ /dev/null @@ -1,16 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jean-Baptiste Tristan --/ -import SampCert -import SampCert.SLang - --- Entry point to check properties of the FFI - -def main : IO Unit := do - -- Check if FFI is working - IO.print "Sampling bytes: " - for _ in [:10000] do - let x <- PMF.run <| SLang.probUniformByte_PMF - IO.println x diff --git a/lakefile.lean b/lakefile.lean index 47a381fa..b80606d3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,10 +15,6 @@ lean_lib «FastExtract» where lean_lib «VMC» where --- From doc-gen4 -meta if get_config? env = some "doc" then -require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" - target ffi.o pkg : FilePath := do let oFile := pkg.buildDir / "ffi.o" let srcJob ← inputTextFile <| pkg.dir / "ffi.cpp" @@ -39,14 +35,3 @@ lean_exe test where root := `Test extraDepTargets := #[`libleanffi] moreLinkArgs := #["-L.lake/build/lib", "-lleanffi"] - -lean_exe check where - root := `SampCertCheck - extraDepTargets := #[`libleanffi] - moreLinkArgs := #["-L.lake/build/lib", "-lleanffi"] - -lean_exe mk_all where - root := `mk_all - supportInterpreter := true - -- Executables which import `Lake` must set `-lLake`. - weakLinkArgs := #["-lLake"] From a1a2da4df086de476aaa85d6043e3f6c4a239723 Mon Sep 17 00:00:00 2001 From: John Tristan Date: Thu, 15 Aug 2024 15:15:09 -0400 Subject: [PATCH 2/3] Benchmarks for FFI code --- Tests/benchmarks.py | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/Tests/benchmarks.py b/Tests/benchmarks.py index 1f067787..9d980295 100644 --- a/Tests/benchmarks.py +++ b/Tests/benchmarks.py @@ -2,26 +2,23 @@ # Benchmarking the discrete Gaussian sampler -import SampCert import matplotlib.pyplot as plt import timeit import secrets import numpy as np from datetime import datetime import tqdm as tqdm -from decimal import Decimal import argparse -from diffprivlib.mechanisms.base import bernoulli_neg_exp from diffprivlib.mechanisms import GaussianDiscrete -from fractions import Fraction -from discretegauss import sample_dlaplace, sample_dgauss +from IBM.discretegauss import sample_dgauss + +from Load import samplers -sampler = SampCert.SLang() rng = secrets.SystemRandom() -def gaussian_benchmarks(mix, warmup_attempts, measured_attempts, lb ,ub, quantity): +def gaussian_benchmarks(mix, warmup_attempts, measured_attempts, lb ,ub, quantity, inv): # Values of epsilon attempted sigmas = [] @@ -45,12 +42,20 @@ def gaussian_benchmarks(mix, warmup_attempts, measured_attempts, lb ,ub, quantit num_attempts = warmup_attempts + measured_attempts - for sigma in tqdm.tqdm(np.linspace(lb+0.001,ub,quantity)): + for sigma_ in tqdm.tqdm(range(lb,ub,quantity)): + if inv: + sigma = 1.0 / float(sigma_) + sigma_num = sigma_ + sigma_denom = ub + else: + sigma = sigma_ + sigma_num = sigma_ + sigma_denom = 1 + g._scale = sigma sigmas += [sigma] - sigma_num, sigma_denom = Decimal(sigma).as_integer_ratio() sigma_squared = sigma ** 2 times = [] @@ -63,7 +68,7 @@ def gaussian_benchmarks(mix, warmup_attempts, measured_attempts, lb ,ub, quantit for m in range(len(mix)): for i in range(num_attempts): start_time = timeit.default_timer() - sampler.DiscreteGaussianSample(sigma_num, sigma_denom, mix[m]) + samplers.dgs_get(sigma_num, sigma_denom, mix[m]) elapsed = timeit.default_timer() - start_time times[m].append(elapsed) @@ -123,12 +128,13 @@ def gaussian_benchmarks(mix, warmup_attempts, measured_attempts, lb ,ub, quantit if __name__ == "__main__": parser = argparse.ArgumentParser() - parser.add_argument("--mix", nargs="+", type=int, help="mix", default=[0]) + parser.add_argument("--mix", nargs="+", type=int, help="mix", default=[7]) parser.add_argument("--warmup", type=int, help="warmup", default=0) parser.add_argument("--trials", type=int, help="trials", default=1000) parser.add_argument("--min", type=int, help="min", default=1) parser.add_argument("--max", type=int, help="max", default=500) parser.add_argument("--quantity", type=int, help="step", default=10) + parser.add_argument("--inv", default=False, action=argparse.BooleanOptionalAction) args = parser.parse_args() - gaussian_benchmarks(args.mix,args.warmup,args.trials,args.min,args.max,args.quantity) + gaussian_benchmarks(args.mix,args.warmup,args.trials,args.min,args.max,args.quantity,args.inv) From 152d997726404d2b3d81cfc873eb2a5b4a5ab37d Mon Sep 17 00:00:00 2001 From: John Tristan Date: Thu, 15 Aug 2024 15:15:44 -0400 Subject: [PATCH 3/3] Removing old dependency --- ffi.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/ffi.cpp b/ffi.cpp index 8b3775b3..2d1f1e5a 100644 --- a/ffi.cpp +++ b/ffi.cpp @@ -6,7 +6,6 @@ Authors: Jean-Baptiste Tristan #include #include #include -#include static int urandom = -1;