From cefe0f6248f3c00214cb5355e1bb5e45a1c3d92c Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 25 Apr 2024 16:47:38 +0100 Subject: [PATCH] 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; + } + + +} + +}