From 0e28d3cb93e59068cfd2c5ac181b4a3e2c3871af Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 09:50:28 -0400 Subject: [PATCH 01/31] SampCert submodule and build --- .gitmodules | 3 + SampCert | 1 + scripts/build.sh | 10 ++ src/DafnyVMCTrait.dfy | 233 ------------------------------------------ 4 files changed, 14 insertions(+), 233 deletions(-) create mode 160000 SampCert delete mode 100644 src/DafnyVMCTrait.dfy diff --git a/.gitmodules b/.gitmodules index 12b39b25..14670cbe 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,3 +4,6 @@ [submodule "docs/py/Benchmarks/differential-privacy-library"] path = docs/py/Benchmarks/differential-privacy-library url = https://github.com/IBM/differential-privacy-library/ +[submodule "SampCert"] + path = SampCert + url = git@github.com:leanprover/SampCert.git diff --git a/SampCert b/SampCert new file mode 160000 index 00000000..58a1041c --- /dev/null +++ b/SampCert @@ -0,0 +1 @@ +Subproject commit 58a1041c3f404617fd011dd2bc7393a0e0cf2ad1 diff --git a/scripts/build.sh b/scripts/build.sh index 28feac69..7ecdea90 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -14,6 +14,16 @@ then exit 1 fi +if [ ! -d SampCert ] +then + echo "Missing SampCert submodule" + exit 1 +fi + +pushd SampCert +lake build VMC +popd + if [ "$TARGET_LANG" = "java" ] then $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy deleted file mode 100644 index e188c943..00000000 --- a/src/DafnyVMCTrait.dfy +++ /dev/null @@ -1,233 +0,0 @@ - -module DafnyVMCTrait { - - import UniformPowerOfTwo - - import FisherYates - - import Uniform - - import opened Pos - - trait {:termination false} RandomTrait extends UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait, Uniform.Interface.Trait { - - method {:verify false} UniformSample (n: pos) - returns (o: nat) - modifies this - decreases * - { - var x := UniformPowerOfTwoSample(2 * n); - while ! (x < n) - decreases * - { - x := UniformPowerOfTwoSample(2 * n); - } - var r := x; - o := r; - } - - method {:verify false} BernoulliSample (num: nat, den: pos) - returns (o: bool) - requires num <= den - modifies this - decreases * - { - var d := UniformSample(den); - o := d < num; - } - - method {:verify false} BernoulliExpNegSampleUnitLoop (num: nat, den: pos, state: (bool,pos)) - returns (o: (bool,pos)) - requires num <= den - modifies this - decreases * - { - var A := BernoulliSample(num, state.1 * den); - o := (A,state.1 + 1); - } - - method {:verify false} BernoulliExpNegSampleUnitAux (num: nat, den: pos) - returns (o: nat) - requires num <= den - modifies this - decreases * - { - var state := (true,1); - while state.0 - decreases * - { - state := BernoulliExpNegSampleUnitLoop(num, den, state); - } - var r := state; - o := r.1; - } - - method {:verify false} BernoulliExpNegSampleUnit (num: nat, den: pos) - returns (o: bool) - requires num <= den - modifies this - decreases * - { - var K := BernoulliExpNegSampleUnitAux(num, den); - if K % 2 == 0 { - o := true; - } else { - o := false; - } - } - - method {:verify false} BernoulliExpNegSampleGenLoop (iter: nat) - returns (o: bool) - modifies this - decreases * - { - if iter == 0 { - o := true; - } else { - var B := BernoulliExpNegSampleUnit(1, 1); - if ! (B == true) { - o := B; - } else { - var R := BernoulliExpNegSampleGenLoop(iter - 1); - o := R; - } - } - } - - method {:verify false} BernoulliExpNegSample (num: nat, den: pos) - returns (o: bool) - modifies this - decreases * - { - if num <= den { - var X := BernoulliExpNegSampleUnit(num, den); - o := X; - } else { - var gamf := num / den; - var B := BernoulliExpNegSampleGenLoop(gamf); - if B == true { - var num := num - gamf * den; - var X := BernoulliExpNegSampleUnit(num, den); - o := X; - } else { - o := false; - } - } - } - - method {:verify false} DiscreteLaplaceSampleLoopIn1Aux (t: pos) - returns (o: (nat,bool)) - modifies this - decreases * - { - var U := UniformSample(t); - var D := BernoulliExpNegSample(U, t); - o := (U,D); - } - - method {:verify false} DiscreteLaplaceSampleLoopIn1 (t: pos) - returns (o: nat) - modifies this - decreases * - { - var x := DiscreteLaplaceSampleLoopIn1Aux(t); - while ! (x.1) - decreases * - { - x := DiscreteLaplaceSampleLoopIn1Aux(t); - } - var r1 := x; - o := r1.0; - } - - method {:verify false} DiscreteLaplaceSampleLoopIn2Aux (num: nat, den: pos, K: (bool,pos)) - returns (o: (bool,pos)) - requires num <= den - modifies this - decreases * - { - var A := BernoulliExpNegSampleUnit(num, den); - o := (A,K.1 + 1); - } - - method {:verify false} DiscreteLaplaceSampleLoopIn2 (num: nat, den: pos) - returns (o: pos) - modifies this - decreases * - { - var K := (true,1); - while K.0 - decreases * - { - K := DiscreteLaplaceSampleLoopIn2Aux(1, 1, K); - } - var r2 := K; - o := r2.1; - } - - method {:verify false} DiscreteLaplaceSampleLoop (num: pos, den: pos) - returns (o: (bool,nat)) - modifies this - decreases * - { - var U := DiscreteLaplaceSampleLoopIn1(num); - var v := DiscreteLaplaceSampleLoopIn2(1, 1); - var V := v - 2; - var X := U + num * V; - var Y := X / den; - var B := BernoulliSample(1, 2); - o := (B,Y); - } - - method {:verify false} DiscreteLaplaceSample (num: pos, den: pos) - returns (o: int) - modifies this - decreases * - { - var x := DiscreteLaplaceSampleLoop(num, den); - while ! (! (x.0 == true && x.1 == 0)) - decreases * - { - x := DiscreteLaplaceSampleLoop(num, den); - } - var r := x; - var Z := if r.0 == true then - (r.1) else r.1; - o := Z; - } - - method {:verify false} DiscreteGaussianSampleLoop (num: pos, den: pos, t: pos) - returns (o: (int,bool)) - modifies this - decreases * - { - var Y := DiscreteLaplaceSample(t, 1); - var y := (if Y < 0 then -Y else Y); - var n := (y * t * den - num) * (y * t * den - num); - var d := 2 * num * (t) * (t) * den; - var C := BernoulliExpNegSample(n, d); - o := (Y,C); - } - - method {:verify false} DiscreteGaussianSample (num: pos, den: pos) - returns (o: int) - modifies this - decreases * - { - var ti := num / den; - var t := ti + 1; - var num := (num) * (num); - var den := (den) * (den); - var x := DiscreteGaussianSampleLoop(num, den, t); - while ! (x.1) - decreases * - { - x := DiscreteGaussianSampleLoop(num, den, t); - } - var r := x; - o := r.0; - } - - - } - -} From 5ab0a4fadaea92b7ed8155979eae3f727ed040cd Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 09:55:20 -0400 Subject: [PATCH 02/31] Modified prep --- scripts/prep.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index cf6e48f2..aece15e9 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -3,4 +3,9 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0-x64-ubuntu-20.04.zip wget $VERSION -unzip `basename $VERSION` \ No newline at end of file +unzip `basename $VERSION` + +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 From d6e159bd38af3d5d063baf089da8918a688614b4 Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 09:58:30 -0400 Subject: [PATCH 03/31] changed elan install --- scripts/prep.sh | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index aece15e9..7458a907 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -5,7 +5,4 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0 wget $VERSION unzip `basename $VERSION` -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 +curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh From 249a15eda990547fb55440b666b63acb2a5833fb Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 10:00:42 -0400 Subject: [PATCH 04/31] changed elan install --- scripts/prep.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index 7458a907..38ac278a 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -5,4 +5,4 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0 wget $VERSION unzip `basename $VERSION` -curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh +curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf -y | sh From 43f5ee545411367da95ace2131a0e1c4af3edec6 Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 10:03:28 -0400 Subject: [PATCH 05/31] changed elan install --- .github/workflows/build_java.yml | 6 ++++++ scripts/prep.sh | 1 - 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build_java.yml b/.github/workflows/build_java.yml index 0138e326..b2f484e8 100644 --- a/.github/workflows/build_java.yml +++ b/.github/workflows/build_java.yml @@ -9,6 +9,12 @@ jobs: build-java: 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 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh diff --git a/scripts/prep.sh b/scripts/prep.sh index 38ac278a..fa48ac1a 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -5,4 +5,3 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0 wget $VERSION unzip `basename $VERSION` -curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf -y | sh From 9ad672e101a4e204d4461b32b00a8e61585403c9 Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 10:04:45 -0400 Subject: [PATCH 06/31] changed elan install --- .github/workflows/build_java.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/build_java.yml b/.github/workflows/build_java.yml index b2f484e8..6263cc6c 100644 --- a/.github/workflows/build_java.yml +++ b/.github/workflows/build_java.yml @@ -15,6 +15,8 @@ jobs: 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 + - name: run elan + run: elan default stable - uses: actions/checkout@v4 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh From 941e9dc8b14e7d38197b53bf8416a41e86b22e94 Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 10:29:48 -0400 Subject: [PATCH 07/31] build script works --- .github/workflows/build_java.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/build_java.yml b/.github/workflows/build_java.yml index 6263cc6c..b2f484e8 100644 --- a/.github/workflows/build_java.yml +++ b/.github/workflows/build_java.yml @@ -15,8 +15,6 @@ jobs: 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 - - name: run elan - run: elan default stable - uses: actions/checkout@v4 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh From 3396e2b3a212b4c463a3f4f7c56e60a3a230a49e Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 10:30:21 -0400 Subject: [PATCH 08/31] build script works --- scripts/prep.sh | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index fa48ac1a..4d81bf36 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -4,4 +4,3 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0 wget $VERSION unzip `basename $VERSION` - From 9a539db94f8e6ac0bee23e98beef0a317c0f0f36 Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 10:30:55 -0400 Subject: [PATCH 09/31] build script works --- scripts/prep.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index 4d81bf36..cf6e48f2 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -3,4 +3,4 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0-x64-ubuntu-20.04.zip wget $VERSION -unzip `basename $VERSION` +unzip `basename $VERSION` \ No newline at end of file From 893f7f6c4c5bcfcdc12e001f97c7763be1690b5c Mon Sep 17 00:00:00 2001 From: jtristan Date: Wed, 24 Apr 2024 10:31:46 -0400 Subject: [PATCH 10/31] build script works --- .github/workflows/build_java.yml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/.github/workflows/build_java.yml b/.github/workflows/build_java.yml index b2f484e8..0138e326 100644 --- a/.github/workflows/build_java.yml +++ b/.github/workflows/build_java.yml @@ -9,12 +9,6 @@ jobs: build-java: 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 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh From aff71e7d0bd8a9dccc3b5ed61ec23c97114c3340 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:22:30 -0400 Subject: [PATCH 11/31] Trying Lean4 install --- scripts/prep.sh | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index cf6e48f2..e740c15d 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -3,4 +3,10 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0-x64-ubuntu-20.04.zip wget $VERSION -unzip `basename $VERSION` \ No newline at end of file +unzip `basename $VERSION` + +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 + From c6ebcd7ca183269bed77ad9314a74dab224e3493 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:24:33 -0400 Subject: [PATCH 12/31] Trying Lean4 install --- scripts/prep.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/prep.sh b/scripts/prep.sh index e740c15d..66ade823 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -10,3 +10,6 @@ curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_ ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> $GITHUB_PATH +pushd SampCert +lake build VMC +popd \ No newline at end of file From 890140c86a6461d5dcfcb9f5f23fe44d92629c6c Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:26:53 -0400 Subject: [PATCH 13/31] Trying Lean4 install --- scripts/prep.sh | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index 66ade823..b9eeddee 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -5,10 +5,12 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0 wget $VERSION unzip `basename $VERSION` -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 +# 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 + +wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile pushd SampCert lake build VMC From d0aeab39bd599de6e83ba72c1160dba035644088 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:28:45 -0400 Subject: [PATCH 14/31] Trying Lean4 install --- scripts/prep.sh | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index b9eeddee..45c568d0 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -5,13 +5,12 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0 wget $VERSION unzip `basename $VERSION` -# 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 - -wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile - pushd SampCert +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 lake build VMC -popd \ No newline at end of file +popd + + From 24d9e4a5476940ef5658346c4bd900685fbf0af0 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:31:41 -0400 Subject: [PATCH 15/31] Trying Lean4 install --- scripts/prep.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/prep.sh b/scripts/prep.sh index 45c568d0..f56b230b 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -9,6 +9,7 @@ pushd SampCert 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 +elan toolchain install leanprover/lean4:v4.7.0 echo "$HOME/.elan/bin" >> $GITHUB_PATH lake build VMC popd From f6300b4ba89824447043aa7605de0ac1ecddb8fd Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:35:18 -0400 Subject: [PATCH 16/31] Trying Lean4 install --- scripts/prep.sh | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index f56b230b..6daaa2fa 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -8,8 +8,7 @@ unzip `basename $VERSION` pushd SampCert 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 -elan toolchain install leanprover/lean4:v4.7.0 +./elan-init -y --default-toolchain leanprover/lean4:v4.7.0 echo "$HOME/.elan/bin" >> $GITHUB_PATH lake build VMC popd From 617d7b045517b5e8fecfae6ab28b2ef497d59051 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:37:07 -0400 Subject: [PATCH 17/31] Trying Lean4 install --- scripts/prep.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/prep.sh b/scripts/prep.sh index 6daaa2fa..aa22367f 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -9,6 +9,7 @@ pushd SampCert 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 leanprover/lean4:v4.7.0 +ls "$HOME/.elan/bin" echo "$HOME/.elan/bin" >> $GITHUB_PATH lake build VMC popd From 049abfd44db373ced50fdc2f9e9f628909f79290 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:39:43 -0400 Subject: [PATCH 18/31] Trying Lean4 install --- scripts/prep.sh | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index aa22367f..a969e843 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -10,8 +10,7 @@ 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 leanprover/lean4:v4.7.0 ls "$HOME/.elan/bin" -echo "$HOME/.elan/bin" >> $GITHUB_PATH -lake build VMC +PATH=$PATH:./.elab/bin/ lake build VMC popd From 4ff05b2344dfadbe79c971e25567f0782d521961 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:41:03 -0400 Subject: [PATCH 19/31] Trying Lean4 install --- scripts/prep.sh | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index a969e843..c4e21407 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -9,8 +9,7 @@ pushd SampCert 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 leanprover/lean4:v4.7.0 -ls "$HOME/.elan/bin" -PATH=$PATH:./.elab/bin/ lake build VMC +.elan/bin/lake build VMC popd From 5ff5ea4b39abf55382a5ce13da60e4f928f791a0 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:44:05 -0400 Subject: [PATCH 20/31] Trying Lean4 install --- scripts/prep.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index c4e21407..cb6b28ee 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -9,7 +9,10 @@ pushd SampCert 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 leanprover/lean4:v4.7.0 -.elan/bin/lake build VMC +ls .elan/bin +ls .elan/bin/lake +cp .elan/bin/* ./ +lake build VMC popd From c4710bf76e1c73879f2e839469dff9786d7ca2e7 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:46:55 -0400 Subject: [PATCH 21/31] Trying Lean4 install --- scripts/prep.sh | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index cb6b28ee..2c38d7c2 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -9,9 +9,7 @@ pushd SampCert 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 leanprover/lean4:v4.7.0 -ls .elan/bin -ls .elan/bin/lake -cp .elan/bin/* ./ +cp $HOME/.elan/bin/* ./ lake build VMC popd From 3f0453954f2570319b03b0721d1ae7525de2081b Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:47:50 -0400 Subject: [PATCH 22/31] Trying Lean4 install --- scripts/prep.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/prep.sh b/scripts/prep.sh index 2c38d7c2..766cb65e 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -9,8 +9,8 @@ pushd SampCert 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 leanprover/lean4:v4.7.0 -cp $HOME/.elan/bin/* ./ -lake build VMC +ls $HOME/.elan/bin/lake +$HOME/.elan/bin/lake build VMC popd From 4ec6a05bd7ce4da3014f61bbc43f4eacca00c331 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:50:23 -0400 Subject: [PATCH 23/31] Trying Lean4 install --- scripts/prep.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/prep.sh b/scripts/prep.sh index 766cb65e..9c54045f 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -10,6 +10,7 @@ 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 leanprover/lean4:v4.7.0 ls $HOME/.elan/bin/lake +ls $HOME/.elan/bin/lake build VMC popd From 8abf5b1bd761286bb63831b5497bc8eaf3ba2ab1 Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 09:54:14 -0400 Subject: [PATCH 24/31] Trying Lean4 install --- .github/workflows/test_py.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/test_py.yml b/.github/workflows/test_py.yml index a9be19d7..f7cfa5e9 100644 --- a/.github/workflows/test_py.yml +++ b/.github/workflows/test_py.yml @@ -10,5 +10,7 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/test.sh From e5036ae3fd598774da3b1de6e82348555ae9ceec Mon Sep 17 00:00:00 2001 From: jtristan Date: Thu, 25 Apr 2024 11:04:13 -0400 Subject: [PATCH 25/31] Trying Lean4 install --- .github/workflows/audit.yml | 2 ++ .github/workflows/build_java.yml | 2 ++ .github/workflows/build_py.yml | 2 ++ .github/workflows/format.yml | 2 ++ .github/workflows/test_java.yml | 2 ++ .github/workflows/verify.yml | 2 ++ scripts/prep.sh | 2 -- 7 files changed, 12 insertions(+), 2 deletions(-) diff --git a/.github/workflows/audit.yml b/.github/workflows/audit.yml index a2277891..4afb1c12 100644 --- a/.github/workflows/audit.yml +++ b/.github/workflows/audit.yml @@ -10,6 +10,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: 'true' - run: bash scripts/prep.sh - run: cp audit.log audit_.log - run: DAFNY=dafny/dafny bash scripts/audit.sh diff --git a/.github/workflows/build_java.yml b/.github/workflows/build_java.yml index 0138e326..66906244 100644 --- a/.github/workflows/build_java.yml +++ b/.github/workflows/build_java.yml @@ -10,6 +10,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh - run: build/java/run_samplers.sh diff --git a/.github/workflows/build_py.yml b/.github/workflows/build_py.yml index 229aacbe..03f3f5ae 100644 --- a/.github/workflows/build_py.yml +++ b/.github/workflows/build_py.yml @@ -10,6 +10,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/build.sh - run: build/py/run_samplers.sh diff --git a/.github/workflows/format.yml b/.github/workflows/format.yml index ab037c80..15f03f5a 100644 --- a/.github/workflows/format.yml +++ b/.github/workflows/format.yml @@ -10,5 +10,7 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny bash scripts/checkformat.sh diff --git a/.github/workflows/test_java.yml b/.github/workflows/test_java.yml index 44b0cdff..3825ae1b 100644 --- a/.github/workflows/test_java.yml +++ b/.github/workflows/test_java.yml @@ -10,5 +10,7 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/test.sh diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 5ae83d1d..16578c92 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -10,5 +10,7 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny bash scripts/verify.sh diff --git a/scripts/prep.sh b/scripts/prep.sh index 9c54045f..f149926d 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -9,8 +9,6 @@ pushd SampCert 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 leanprover/lean4:v4.7.0 -ls $HOME/.elan/bin/lake -ls $HOME/.elan/bin/lake build VMC popd From cefe0f6248f3c00214cb5355e1bb5e45a1c3d92c Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 25 Apr 2024 16:47:38 +0100 Subject: [PATCH 26/31] small changes --- .github/workflows/trait.yml | 19 +++ scripts/prep.sh | 11 +- scripts/sampcert.sh | 6 + src/DafnyVMCTrait.dfy | 228 ++++++++++++++++++++++++++++++++++++ 4 files changed, 254 insertions(+), 10 deletions(-) create mode 100644 .github/workflows/trait.yml create mode 100644 scripts/sampcert.sh create mode 100644 src/DafnyVMCTrait.dfy diff --git a/.github/workflows/trait.yml b/.github/workflows/trait.yml new file mode 100644 index 00000000..f4fc65ae --- /dev/null +++ b/.github/workflows/trait.yml @@ -0,0 +1,19 @@ +name: 'Verify DafnyVMCTrait.dfy' +on: + workflow_dispatch: + pull_request: + push: + branches: + - 'main' +jobs: + audit: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + submodules: 'true' + - run: bash scripts/prep.sh + - run: cp src/DafnyVMCTrait.dfy.log src/DafnyVMCTrait.dfy_.log + - run: DAFNY=dafny/dafny bash scripts/sampcert.sh + - run: cat src/DafnyVMCTrait.dfy.log + - run: diff src/DafnyVMCTrait.dfy.log src/DafnyVMCTrait.dfy_.log diff --git a/scripts/prep.sh b/scripts/prep.sh index f149926d..cf6e48f2 100755 --- a/scripts/prep.sh +++ b/scripts/prep.sh @@ -3,13 +3,4 @@ VERSION=https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0-x64-ubuntu-20.04.zip wget $VERSION -unzip `basename $VERSION` - -pushd SampCert -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 leanprover/lean4:v4.7.0 -$HOME/.elan/bin/lake build VMC -popd - - +unzip `basename $VERSION` \ No newline at end of file diff --git a/scripts/sampcert.sh b/scripts/sampcert.sh new file mode 100644 index 00000000..3e8873dc --- /dev/null +++ b/scripts/sampcert.sh @@ -0,0 +1,6 @@ +pushd SampCert +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 leanprover/lean4:v4.7.0 +$HOME/.elan/bin/lake build VMC +popd \ No newline at end of file diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy new file mode 100644 index 00000000..cb4a63d5 --- /dev/null +++ b/src/DafnyVMCTrait.dfy @@ -0,0 +1,228 @@ + +module DafnyVMCTrait { + + import UniformPowerOfTwo + + import FisherYates + + import opened Pos + + import Uniform + + trait {:termination false} RandomTrait extends UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait, Uniform.Interface.Trait { + + method {:verify false} UniformSample (n: pos) + returns (o: nat) + modifies this + decreases * + { + var x := UniformPowerOfTwoSample(2 * n); + while ! (x < n) + decreases * + { + x := UniformPowerOfTwoSample(2 * n); + } + var r := x; + o := r; + } + + method {:verify false} BernoulliSample (num: nat, den: pos) + returns (o: bool) + requires num <= den + modifies this + decreases * + { + var d := UniformSample(den); + o := d < num; + } + + method {:verify false} BernoulliExpNegSampleUnitLoop (num: nat, den: pos, state: (bool,pos)) + returns (o: (bool,pos)) + requires num <= den + modifies this + decreases * + { + var A := BernoulliSample(num, state.1 * den); + o := (A,state.1 + 1); + } + + method {:verify false} BernoulliExpNegSampleUnitAux (num: nat, den: pos) + returns (o: nat) + requires num <= den + modifies this + decreases * + { + var state := (true,1); + while state.0 + decreases * + { + state := BernoulliExpNegSampleUnitLoop(num, den, state); + } + var r := state; + o := r.1; + } + + method {:verify false} BernoulliExpNegSampleUnit (num: nat, den: pos) + returns (o: bool) + requires num <= den + modifies this + decreases * + { + var K := BernoulliExpNegSampleUnitAux(num, den); + if K % 2 == 0 { + o := true; + } else { + o := false; + } + } + + method {:verify false} BernoulliExpNegSampleGenLoop (iter: nat) + returns (o: bool) + modifies this + decreases * + { + if iter == 0 { + o := true; + } else { + var B := BernoulliExpNegSampleUnit(1, 1); + if ! (B == true) { + o := B; + } else { + var R := BernoulliExpNegSampleGenLoop(iter - 1); + o := R; + } + } + } + + method {:verify false} BernoulliExpNegSample (num: nat, den: pos) + returns (o: bool) + modifies this + decreases * + { + if num <= den { + var X := BernoulliExpNegSampleUnit(num, den); + o := X; + } else { + var gamf := num / den; + var B := BernoulliExpNegSampleGenLoop(gamf); + if B == true { + var X := BernoulliExpNegSampleUnit(num % den, den); + o := X; + } else { + o := false; + } + } + } + + method {:verify false} DiscreteLaplaceSampleLoopIn1Aux (t: pos) + returns (o: (nat,bool)) + modifies this + decreases * + { + var U := UniformSample(t); + var D := BernoulliExpNegSample(U, t); + o := (U,D); + } + + method {:verify false} DiscreteLaplaceSampleLoopIn1 (t: pos) + returns (o: nat) + modifies this + decreases * + { + var x := DiscreteLaplaceSampleLoopIn1Aux(t); + while ! (x.1) + decreases * + { + x := DiscreteLaplaceSampleLoopIn1Aux(t); + } + var r1 := x; + o := r1.0; + } + + method {:verify false} DiscreteLaplaceSampleLoopIn2Aux (num: nat, den: pos, K: (bool,nat)) + returns (o: (bool,nat)) + modifies this + decreases * + { + var A := BernoulliExpNegSample(num, den); + o := (A,K.1 + 1); + } + + method {:verify false} DiscreteLaplaceSampleLoopIn2 (num: nat, den: pos) + returns (o: nat) + modifies this + decreases * + { + var K := (true,0); + while K.0 + decreases * + { + K := DiscreteLaplaceSampleLoopIn2Aux(num, den, K); + } + var r2 := K; + o := r2.1; + } + + method {:verify false} DiscreteLaplaceSampleLoop (num: pos, den: pos) + returns (o: (bool,nat)) + modifies this + decreases * + { + var v := DiscreteLaplaceSampleLoopIn2(den, num); + var V := v - 1; + var B := BernoulliSample(1, 2); + o := (B,V); + } + + method {:verify false} DiscreteLaplaceSample (num: pos, den: pos) + returns (o: int) + modifies this + decreases * + { + var x := DiscreteLaplaceSampleLoop(num, den); + while ! (! (x.0 == true && x.1 == 0)) + decreases * + { + x := DiscreteLaplaceSampleLoop(num, den); + } + var r := x; + var Z := if r.0 == true then - (r.1) else r.1; + o := Z; + } + + method {:verify false} DiscreteGaussianSampleLoop (num: pos, den: pos, t: pos) + returns (o: (int,bool)) + modifies this + decreases * + { + var Y := DiscreteLaplaceSample(t, 1); + var y := (if Y < 0 then -Y else Y); + var n := ((if y * t * den - num < 0 then -y * t * den - num else y * t * den - num)) * ((if y * t * den - num < 0 then -y * t * den - num else y * t * den - num)); + var d := 2 * num * (t) * (t) * den; + var C := BernoulliExpNegSample(n, d); + o := (Y,C); + } + + method {:verify false} DiscreteGaussianSample (num: pos, den: pos) + returns (o: int) + modifies this + decreases * + { + var ti := num / den; + var t := ti + 1; + var num := (num) * (num); + var den := (den) * (den); + var x := DiscreteGaussianSampleLoop(num, den, t); + while ! (x.1) + decreases * + { + x := DiscreteGaussianSampleLoop(num, den, t); + } + var r := x; + o := r.0; + } + + +} + +} From eda2c8385140a54924e73151ec2736ab0a3b3b0f Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 25 Apr 2024 16:52:44 +0100 Subject: [PATCH 27/31] Remove submodule requirement --- .github/workflows/audit.yml | 2 -- .github/workflows/build_java.yml | 2 -- .github/workflows/build_py.yml | 4 +--- .github/workflows/format.yml | 2 -- .github/workflows/test_java.yml | 2 -- .github/workflows/test_py.yml | 2 -- .github/workflows/verify.yml | 2 -- scripts/build.sh | 10 ---------- 8 files changed, 1 insertion(+), 25 deletions(-) diff --git a/.github/workflows/audit.yml b/.github/workflows/audit.yml index 4afb1c12..a2277891 100644 --- a/.github/workflows/audit.yml +++ b/.github/workflows/audit.yml @@ -10,8 +10,6 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - with: - submodules: 'true' - run: bash scripts/prep.sh - run: cp audit.log audit_.log - run: DAFNY=dafny/dafny bash scripts/audit.sh diff --git a/.github/workflows/build_java.yml b/.github/workflows/build_java.yml index 66906244..0138e326 100644 --- a/.github/workflows/build_java.yml +++ b/.github/workflows/build_java.yml @@ -10,8 +10,6 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - with: - submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/build.sh - run: build/java/run_samplers.sh diff --git a/.github/workflows/build_py.yml b/.github/workflows/build_py.yml index 03f3f5ae..453f015a 100644 --- a/.github/workflows/build_py.yml +++ b/.github/workflows/build_py.yml @@ -9,9 +9,7 @@ jobs: build-python: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 - with: - submodules: 'true' + - uses: actions/checkout@v4 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/build.sh - run: build/py/run_samplers.sh diff --git a/.github/workflows/format.yml b/.github/workflows/format.yml index 15f03f5a..ab037c80 100644 --- a/.github/workflows/format.yml +++ b/.github/workflows/format.yml @@ -10,7 +10,5 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - with: - submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny bash scripts/checkformat.sh diff --git a/.github/workflows/test_java.yml b/.github/workflows/test_java.yml index 3825ae1b..44b0cdff 100644 --- a/.github/workflows/test_java.yml +++ b/.github/workflows/test_java.yml @@ -10,7 +10,5 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - with: - submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=java bash scripts/test.sh diff --git a/.github/workflows/test_py.yml b/.github/workflows/test_py.yml index f7cfa5e9..a9be19d7 100644 --- a/.github/workflows/test_py.yml +++ b/.github/workflows/test_py.yml @@ -10,7 +10,5 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - with: - submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/test.sh diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 16578c92..5ae83d1d 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -10,7 +10,5 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - with: - submodules: 'true' - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny bash scripts/verify.sh diff --git a/scripts/build.sh b/scripts/build.sh index 7ecdea90..28feac69 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -14,16 +14,6 @@ then exit 1 fi -if [ ! -d SampCert ] -then - echo "Missing SampCert submodule" - exit 1 -fi - -pushd SampCert -lake build VMC -popd - if [ "$TARGET_LANG" = "java" ] then $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify From e06a18bd48914634a778bb5dedcb14dcff5af12d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 25 Apr 2024 16:54:02 +0100 Subject: [PATCH 28/31] Remove empty space --- .github/workflows/build_py.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build_py.yml b/.github/workflows/build_py.yml index 453f015a..229aacbe 100644 --- a/.github/workflows/build_py.yml +++ b/.github/workflows/build_py.yml @@ -9,7 +9,7 @@ jobs: build-python: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v4 - run: bash scripts/prep.sh - run: DAFNY=dafny/dafny TARGET_LANG=py bash scripts/build.sh - run: build/py/run_samplers.sh From 375cd657b700798b5f5d6cf75359e3e604fbfd82 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 25 Apr 2024 16:55:36 +0100 Subject: [PATCH 29/31] Fix naming --- .github/workflows/trait.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/trait.yml b/.github/workflows/trait.yml index f4fc65ae..59fcbc2a 100644 --- a/.github/workflows/trait.yml +++ b/.github/workflows/trait.yml @@ -13,7 +13,7 @@ jobs: with: submodules: 'true' - run: bash scripts/prep.sh - - run: cp src/DafnyVMCTrait.dfy.log src/DafnyVMCTrait.dfy_.log + - run: cp src/DafnyVMCTrait.dfy src/DafnyVMCTrait_.dfy - run: DAFNY=dafny/dafny bash scripts/sampcert.sh - - run: cat src/DafnyVMCTrait.dfy.log - - run: diff src/DafnyVMCTrait.dfy.log src/DafnyVMCTrait.dfy_.log + - run: cat src/DafnyVMCTrait.dfy + - run: diff src/DafnyVMCTrait.dfy src/DafnyVMCTrait_.dfy From 6e1628f8ee3f3aca98f84f9d6439a7fa456c97e5 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 25 Apr 2024 16:56:28 +0100 Subject: [PATCH 30/31] Verify -> Compare --- .github/workflows/trait.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/trait.yml b/.github/workflows/trait.yml index 59fcbc2a..345ed9c3 100644 --- a/.github/workflows/trait.yml +++ b/.github/workflows/trait.yml @@ -1,4 +1,4 @@ -name: 'Verify DafnyVMCTrait.dfy' +name: 'Compare DafnyVMCTrait.dfy' on: workflow_dispatch: pull_request: From 1f3f8debf48adca7a578993c02d9a56fcadb754f Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 25 Apr 2024 19:40:49 +0100 Subject: [PATCH 31/31] Change github job name --- .github/workflows/trait.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/trait.yml b/.github/workflows/trait.yml index 345ed9c3..bb5bc0d9 100644 --- a/.github/workflows/trait.yml +++ b/.github/workflows/trait.yml @@ -6,7 +6,7 @@ on: branches: - 'main' jobs: - audit: + compare-trait: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4