Skip to content

Commit

Permalink
Reduce and limit resource usage (#88)
Browse files Browse the repository at this point in the history 
This reduces and limits the resource usage to 20M, which is still a lot,
but at least it will prevent regressions.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
@fzaiser
fzaiser authored Oct 6, 2023
1 parent 3007adf commit 580885a
Show file tree
Hide file tree
Showing 6 changed files with 57 additions and 34 deletions.
2 changes: 1 addition & 1 deletion audit.log
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ src/Distributions/BernoulliExpNeg/Implementation.dfy(52,6): BernoulliExpNegSampl
src/Distributions/BernoulliExpNeg/Model.dfy(30,4): GammaReductionLoop: Definition has `assume {:axiom}` statement in body.
src/Distributions/BernoulliExpNeg/Model.dfy(60,4): GammaLe1Loop: Definition has `assume {:axiom}` statement in body.
src/Distributions/Coin/Interface.dfy(20,6): CoinSample: Definition has `assume {:axiom}` statement in body.
src/Distributions/Uniform/Correctness.dfy(157,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute.
src/Distributions/Uniform/Correctness.dfy(165,17): SampleIsIndepFn: Declaration has explicit `{:axiom}` attribute.
src/Distributions/Uniform/Implementation.dfy(43,6): UniformSample: Definition has `assume {:axiom}` statement in body.
src/Distributions/Uniform/Model.dfy(34,17): SampleTerminates: Declaration has explicit `{:axiom}` attribute.
src/Math/Exponential.dfy(11,17): EvalOne: Declaration has explicit `{:axiom}` attribute.
Expand Down
2 changes: 1 addition & 1 deletion scripts/verify.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,4 +9,4 @@ then
fi

echo Verifying the proofs...
time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesExternUniform.dfy docs/dafny/ExamplesFoundational.dfy tests/Tests.dfy tests/TestsExternUniform.dfy tests/TestsFoundational.dfy
time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesExternUniform.dfy docs/dafny/ExamplesFoundational.dfy tests/Tests.dfy tests/TestsExternUniform.dfy tests/TestsFoundational.dfy --resource-limit 20000 # 20M resource usage
30 changes: 19 additions & 11 deletions src/Distributions/Uniform/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,20 +99,26 @@ module Uniform.Correctness {
UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i);
}

lemma ProbabilityProposalAccepted(n: nat)
lemma Power2Log2Helper(n: nat)
requires n >= 1
ensures
var e := WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
RandomNumberGenerator.mu(e) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)
ensures n < Helper.Power(2, Helper.Log2Floor(2 * n))
{
var e := WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
calc {
n;
< { Helper.Power2OfLog2Floor(n); }
Helper.Power(2, Helper.Log2Floor(n) + 1);
== { Helper.Log2FloorDef(n); }
Helper.Power(2, Helper.Log2Floor(2 * n));
}
}

lemma ProbabilityProposalAccepted(n: nat)
requires n >= 1
ensures
RandomNumberGenerator.mu(WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)
{
var e := WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
assert n < Helper.Power(2, Helper.Log2Floor(2 * n)) by { Power2Log2Helper(n); }
assert Equal: e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n) by {
forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n {
calc {
Expand All @@ -122,12 +128,14 @@ module Uniform.Correctness {
}
}
}
calc {
RandomNumberGenerator.mu(e);
{ reveal Equal; }
RandomNumberGenerator.mu(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n);
{ UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
(n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real);
assert RandomNumberGenerator.mu(WhileAndUntil.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) by {
calc {
RandomNumberGenerator.mu(e);
{ reveal Equal; }
RandomNumberGenerator.mu(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n);
{ UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
(n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real);
}
}
}

Expand Down
34 changes: 19 additions & 15 deletions src/Distributions/UniformPowerOfTwo/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,9 +256,9 @@ module UniformPowerOfTwo.Correctness {
==
Model.UnifStep(a)(s').1;
==
Monad.Bind(Monad.Deconstruct, (b: bool) => Monad.Return(if b then 2*a + 1 else 2*a))(s').1;
Monad.Bind(Monad.Deconstruct, (b: bool) => Monad.Return((if b then 2*a + 1 else 2*a) as nat))(s').1;
==
Monad.Return(if b then 2*a + 1 else 2*a)(s'').1;
Monad.Return((if b then 2*a + 1 else 2*a) as nat)(s'').1;
==
s'';
==
Expand All @@ -273,11 +273,11 @@ module UniformPowerOfTwo.Correctness {
ensures
var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0;
var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0;
(iset s | Model.Sample(n)(s).0 == m) == (iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m)
(iset s | Model.Sample(n)(s).0 == m) == (iset s | 2*a_of(s) + Helper.boolToNat(b_of(s)) == m)
{
var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0;
var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0;
forall s ensures Model.Sample(n)(s).0 == m <==> (2 * a_of(s) + (if b_of(s) then 1 else 0) == m) {
forall s ensures Model.Sample(n)(s).0 == m <==> (2 * a_of(s) + Helper.boolToNat(b_of(s)) == m) {
var (a, s') := Model.Sample(n / 2)(s);
var (b, s'') := Monad.Deconstruct(s');
calc {
Expand All @@ -287,9 +287,9 @@ module UniformPowerOfTwo.Correctness {
==
Model.UnifStep(a)(s').0;
==
Monad.Bind(Monad.Deconstruct, b => Monad.Return(if b then 2*a + 1 else 2*a))(s').0;
Monad.Bind(Monad.Deconstruct, b => Monad.Return((if b then 2*a + 1 else 2*a) as nat))(s').0;
==
Monad.Return(if b then 2*a + 1 else 2*a)(s'').0;
Monad.Return((if b then 2*a + 1 else 2*a) as nat)(s'').0;
==
if b then 2*a + 1 else 2*a;
}
Expand All @@ -300,22 +300,26 @@ module UniformPowerOfTwo.Correctness {
requires n >= 2
ensures RandomNumberGenerator.mu(iset s | Model.Sample(n)(s).0 == m) == RandomNumberGenerator.mu(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0
{
var a_of := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0;
var b_of := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0;
var A: iset<nat> := (iset x | x == m / 2);
var E: iset<RandomNumberGenerator.RNG> := (iset s | m % 2 == if Monad.Deconstruct(s).0 then 1 else 0);
var a_of: RandomNumberGenerator.RNG -> nat := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).0;
var b_of: RandomNumberGenerator.RNG -> bool := (s: RandomNumberGenerator.RNG) => Monad.Deconstruct(Model.Sample(n / 2)(s).1).0;
var A: iset<nat> := (iset x: nat | x == m / 2);
var E: iset<RandomNumberGenerator.RNG> := (iset s | m % 2 as nat == Helper.boolToNat(Monad.Deconstruct(s).0));
var f := (s: RandomNumberGenerator.RNG) => Model.Sample(n / 2)(s).1;

var e1 := (iset s | Model.Sample(n / 2)(s).1 in E);
var e2 := (iset s | Model.Sample(n / 2)(s).0 in A);
var e3 := (iset s | 2*a_of(s) + (if b_of(s) then 1 else 0) == m);
var e3 := (iset s | 2*a_of(s) + Helper.boolToNat(b_of(s)) == m);

assert SplitEvent: e3 == e1 * e2 by {
forall s ensures s in e3 <==> s in e1 && s in e2 {
var a: nat := a_of(s);
var b: nat := Helper.boolToNat(b_of(s));
assert b < 2;
calc {
s in e3;
2*a_of(s) + (if b_of(s) then 1 else 0) == m;
(m % 2 == if b_of(s) then 1 else 0) && a_of(s) == m / 2;
2 * a + b == m;
m == a * 2 + b;
(a == m / 2) && (b == m % 2);
s in e1 && s in e2;
}
}
Expand Down Expand Up @@ -356,7 +360,7 @@ module UniformPowerOfTwo.Correctness {
Independence.AreIndepEventsConjunctElimination(e1, e2);
}

assert ProbE1: 0.5 == RandomNumberGenerator.mu(e1) by {
assert ProbE1: RandomNumberGenerator.mu(e1) == 0.5 by {
calc {
0.5;
==
Expand All @@ -376,7 +380,7 @@ module UniformPowerOfTwo.Correctness {
RandomNumberGenerator.mu(e1 * e2);
== { reveal Indep; }
RandomNumberGenerator.mu(e1) * RandomNumberGenerator.mu(e2);
== { reveal ProbE1; }
== { reveal ProbE1; Helper.Congruence(RandomNumberGenerator.mu(e1), 0.5, x => x * RandomNumberGenerator.mu(e2)); }
0.5 * RandomNumberGenerator.mu(e2);
==
RandomNumberGenerator.mu(e2) / 2.0;
Expand Down
10 changes: 6 additions & 4 deletions src/Distributions/UniformPowerOfTwo/Model.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,17 +122,19 @@ module UniformPowerOfTwo.Model {
Sample(Helper.Power(2, m + l))(s);
}
} else {
assert Ineq1: Helper.Power(2, l) >= 1 by { Helper.PowerGreater0(2, l); }
assert Helper.Power(2, m) >= 1 by { Helper.PowerGreater0(2, m); }
assert LGreaterZero: Helper.Power(2, l) >= 1 by { Helper.PowerGreater0(2, l); }
assert MGreaterZero: Helper.Power(2, m) >= 1 by { Helper.PowerGreater0(2, m); }
assert L1GreaterZero: Helper.Power(2, l - 1) >= 1 by { Helper.PowerGreater0(2, l - 1); }
calc {
Monad.Bind(Sample(Helper.Power(2, m)), (u: nat) => SampleTailRecursive(Helper.Power(2, l), u))(s);
(var (u, s') := Sample(Helper.Power(2, m))(s); SampleTailRecursive(Helper.Power(2, l), u)(s'));
{ reveal Ineq1; }
{ reveal LGreaterZero; }
(var (u, s') := Sample(Helper.Power(2, m))(s);
SampleTailRecursive(Helper.Power(2, l) / 2, if Monad.Head(s') then 2 * u + 1 else 2 * u)(Monad.Tail(s')));
{ assert Helper.Power(2, m + 1) / 2 == Helper.Power(2, m); }
{ assert Helper.Power(2, l) / 2 == Helper.Power(2, l - 1); reveal L1GreaterZero; }
(var (u', s') := Monad.Bind(Sample(Helper.Power(2, m)), UnifStep)(s);
SampleTailRecursive(Helper.Power(2, l - 1), u')(s'));
{ assert Helper.Power(2, m + 1) / 2 == Helper.Power(2, m); }
(var (u', s') := Sample(Helper.Power(2, m + 1))(s);
SampleTailRecursive(Helper.Power(2, l - 1), u')(s'));
Monad.Bind(Sample(Helper.Power(2, m + 1)), (u: nat) => SampleTailRecursive(Helper.Power(2, l - 1), u))(s);
Expand Down
13 changes: 11 additions & 2 deletions src/Math/Helper.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,11 +31,19 @@ module Helper {
ensures Log2Floor(2 * n) == Log2Floor(n) + 1
{}

function boolToNat(b: bool): nat {
if b then 1 else 0
}

/*******
Lemmas
*******/

lemma Congruence<T, U>(x: T, y: T, f: T -> U)
requires x == y
ensures f(x) == f(y)
{}

lemma DivisionSubstituteAlternativeReal(x: real, a: real, b: real)
requires a == b
requires x != 0.0
Expand All @@ -51,9 +59,10 @@ module Helper {
assert 0 == m * zp + ((n + m) % m) - (n % m);
}

lemma DivModIsUnique(n: nat, m: nat, a: nat, b: nat)
lemma DivModIsUnique(n: int, m: int, a: int, b: int)
requires n >= 0
requires m > 0
requires b < m
requires 0 <= b < m
requires n == a * m + b
ensures a == n / m
ensures b == n % m
Expand Down

0 comments on commit 580885a

Please sign in to comment.