Merge pull request #4 from leanprover/ConcentratedBound

workflow update for testing extraction

.github/workflows/lean_build.yml

@@ -1,8 +1,10 @@
 on:
   push:
+    branches:
+      - 'main'
   pull_request:
 
-name: ci
+name: Verify
 
 jobs:
   build:
@@ -21,3 +23,4 @@ jobs:
       - name: build std
         id: build
         run: lake build -Kwerror
+

.github/workflows/test.yml

@@ -0,0 +1,34 @@
+on:
+  push:
+    branches:
+      - 'main'
+  pull_request:
+
+name: Extract, build, run
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - uses: actions/checkout@v4
+
+      - name: build std
+        id: build
+        run: lake build -Kwerror FastExtract
+
+      - name: install Dafny
+        run: wget https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0-x64-ubuntu-20.04.zip ; unzip dafny-4.4.0-x64-ubuntu-20.04.zip
+
+      - name: build Python version of SampCert
+        run: dafny/dafny build --target:py Tests/SampCert.dfy Tests/Random.py Tests/Test.py -o Tests/SampCert.dfy 
+
+      - name: run Test
+        run: python3 Tests/SampCert-py/Test.py

FastExtract.lean

@@ -0,0 +1,7 @@
+/-
+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.Extraction

SampCert.lean

@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.Extraction
+import SampCert.Samplers.Gaussian.Basic
 import SampCert.DiffPrivacy.ConcentratedBound

SampCert/Extractor/Extension.lean

@@ -29,7 +29,7 @@ inductive Entry where
 def addEntry (s : State) (e : Entry) : State :=
   match e with
   | .addDecl key val => { s with map := s.map.insert key val }
-  | .toExport decl => { s with decls := decl :: s.decls }
+  | .toExport decl => { s with decls := decl.replace "SLang." "" :: s.decls }
   | .addInline name => { s with inlines := name.toString :: s.inlines }
   | .addFunc key val => { s with glob := s.glob.insert key val}
 

SampCert/Extractor/Print.lean

@@ -11,7 +11,7 @@ open System IO.FS
 
 namespace Lean.ToDafny
 
-def destination : String := "/tmp/DafnyVMCTrait.dfy"
+def destination : String := "Tests/SampCert.dfy"
 
 def writeLn (ln : String) : IO Unit := do
   let h ← Handle.mk destination Mode.append
@@ -21,17 +21,27 @@ def writeLn (ln : String) : IO Unit := do
 
 elab "#print_dafny_exports" : command => do
   writeFile destination ""
-  writeLn "module DafnyVMCTrait {"
-  writeLn "  import UniformPowerOfTwo"
-  writeLn "  import FisherYates"
-  writeLn "  import opened Pos"
-  writeLn "  import Uniform"
 
-  writeLn "  trait {:termination false} RandomTrait extends  UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait, Uniform.Interface.Trait {\n"
+  writeLn "module {:extern} Random {"
+  writeLn "  class {:extern} Random {"
+  writeLn "    static method {:extern \"UniformPowerOfTwoSample\"} ExternUniformPowerOfTwoSample(n: nat) returns (u: nat)"
+  writeLn "  }"
+  writeLn "}"
+
+  writeLn "module {:extern} SampCert {"
+  writeLn "  import Random"
+  writeLn "  type pos = x: nat | x > 0 witness 1"
+
+  writeLn "  class SLang {\n"
+
+  writeLn "    method UniformPowerOfTwoSample(n: nat) returns (u: nat)"
+  writeLn "      requires n >= 1"
+  writeLn "    {"
+  writeLn "      u := Random.Random.ExternUniformPowerOfTwoSample(n);"
+  writeLn "    }"
 
   let { decls, .. } := extension.getState (← getEnv)
   for decl in decls.reverse do
-    --IO.println decl
     let h ← Handle.mk destination Mode.append
     h.putStr decl
   writeLn "}"

SampCert/Samplers/Gaussian/Properties.lean

@@ -566,6 +566,9 @@ theorem summable_gauss_core (num : PNat) (den : PNat) :
   intro Y
   apply (RCLike.summable_ofReal ℂ).mp Y
 
+theorem Add1 (n : Nat) : 0 < n + 1 := by
+  simp only [add_pos_iff, zero_lt_one, or_true]
+
 @[simp]
 theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (x : ℤ) :
   (DiscreteGaussianSample num den) x =

Tests/Random.py

@@ -0,0 +1,5 @@
+import secrets
+
+class Random:
+    def UniformPowerOfTwoSample(n):
+        return secrets.randbits(n.bit_length()-1)

Tests/Test.py

@@ -0,0 +1,8 @@
+import SampCert
+
+def main():
+  r = SampCert.SLang() 
+  x = r.UniformSample(10)
+  print(x)
+
+main()

lakefile.lean

@@ -9,4 +9,5 @@ require mathlib from git
 
 @[default_target]
 lean_lib «SampCert» where
-  -- add any library configuration options here
+
+lean_lib «FastExtract» where