Axiomatise Uniform (#159)

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).
dafny-lang · Mar 5, 2024 · 9b10413 · 9b10413
1 parent a2f6207
commit 9b10413
Show file tree

Hide file tree

Showing 6 changed files with 99 additions and 215 deletions.
diff --git a/audit.log b/audit.log
@@ -1,4 +1,6 @@
 src/DafnyVMC.dfy(28,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/Uniform/Correctness.dfy(34,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(21,33): Sample: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Analysis/Limits.dfy(126,17): Sandwich: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute. 

diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy
@@ -26,7 +26,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliSample (num: nat, den: pos)
       returns (o: bool)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -36,7 +36,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnitLoop (num: nat, den: pos, state: (bool,pos))
       returns (o: (bool,pos))
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -46,7 +46,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnitAux (num: nat, den: pos)
       returns (o: nat)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -62,7 +62,7 @@ module DafnyVMCTrait {
 
     method {:verify false} BernoulliExpNegSampleUnit (num: nat, den: pos)
       returns (o: bool)
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -140,7 +140,7 @@ module DafnyVMCTrait {
 
     method {:verify false} DiscreteLaplaceSampleLoopIn2Aux (num: nat, den: pos, K: (bool,pos))
       returns (o: (bool,pos))
-      requires num <= den 
+      requires num <= den
       modifies this
       decreases *
     {
@@ -226,6 +226,6 @@ module DafnyVMCTrait {
     }
 
 
-}
+  }
 
 }
diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy
@@ -31,108 +31,10 @@ module Uniform.Correctness {
 
   // Correctness theorem for Model.Sample
   // Equation (4.12) / PROB_BERN_UNIFORM
-  lemma UniformFullCorrectness(n: nat, i: nat)
+  lemma {:axiom} UniformFullCorrectness(n: nat, i: nat)
     requires 0 <= i < n
     ensures SampleEquals(n, i) in Rand.eventSpace
     ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real)
-  {
-    var equalsI := (x: nat) => x == i;
-
-    assert Independence.IsIndep(Model.Proposal(n)) && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Model.Proposal(n), Model.Accept(n))) by {
-      Model.SampleTerminates(n);
-    }
-
-    Loops.UntilProbabilityFraction(Model.Proposal(n), Model.Accept(n), equalsI);
-    var eventResultEqualsI := Loops.UntilLoopResultHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
-    var eventProposalAcceptedAndEqualsI := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), equalsI);
-    var proposalAccepted := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
-
-    assert Fraction: Rand.prob(eventResultEqualsI) == Rand.prob(eventProposalAcceptedAndEqualsI) / Rand.prob(proposalAccepted);
-
-    assert Eq: eventResultEqualsI == SampleEquals(n, i) by {
-      forall s ensures s in eventResultEqualsI <==> s in SampleEquals(n, i) {
-        reveal Model.Sample();
-        assert s in eventResultEqualsI <==> s in SampleEquals(n, i);
-      }
-    }
-
-    assert SampleEquals(n, i) in Rand.eventSpace by {
-      reveal Eq;
-    }
-
-    assert Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real) by {
-      calc {
-        Rand.prob(SampleEquals(n, i));
-        { reveal Eq; }
-        Rand.prob(eventResultEqualsI);
-        { reveal Fraction; }
-        Rand.prob(eventProposalAcceptedAndEqualsI) / Rand.prob(proposalAccepted);
-        { ProbabilityProposalAcceptedAndEqualsI(n, i); }
-        (1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)) / Rand.prob(proposalAccepted);
-        { ProbabilityProposalAccepted(n); }
-        (1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)) / ((n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real));
-        { RealArith.SimplifyFractions(1.0, n as real, NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real); }
-        1.0 / (n as real);
-      }
-    }
-  }
-
-  lemma ProbabilityProposalAcceptedAndEqualsI(n: nat, i: nat)
-    requires 0 <= i < n
-    ensures
-      Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i)) == 1.0 / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)
-  {
-    var e := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i);
-    var nextPowerOfTwo := NatArith.Power(2, NatArith.Log2Floor(2 * n));
-    assert iBound: i < nextPowerOfTwo by {
-      calc {
-        i;
-      <
-        n;
-      < { NatArith.NLtPower2Log2FloorOf2N(n); }
-        nextPowerOfTwo;
-      }
-    }
-    assert setEq: Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i) == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i) by {
-      forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i {
-        assert s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i;
-      }
-    }
-    calc {
-      Rand.prob(Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i));
-      { reveal setEq; }
-      Rand.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value == i);
-      { reveal iBound; UniformPowerOfTwo.Correctness.UnifCorrectness2(2 * n, i); }
-      1.0 / (nextPowerOfTwo as real);
-    }
-  }
-
-  lemma ProbabilityProposalAccepted(n: nat)
-    requires n >= 1
-    ensures
-      Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real)
-  {
-    var e := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n));
-    assert n < NatArith.Power(2, NatArith.Log2Floor(2 * n)) by { NatArith.NLtPower2Log2FloorOf2N(n); }
-    assert Equal: e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n) by {
-      forall s ensures s in e <==> UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n {
-        calc {
-          s in e;
-          Model.Accept(n)(Model.Proposal(n)(s).value);
-          UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n;
-        }
-      }
-    }
-    assert Rand.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real) by {
-      calc {
-        Rand.prob(e);
-        { reveal Equal; }
-        Rand.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n);
-        { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
-        (n as real) / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real);
-      }
-    }
-  }
 
   // Correctness theorem for Model.IntervalSample
   lemma UniformFullIntervalCorrectness(a: int, b: int, i: int)
@@ -160,16 +62,7 @@ module Uniform.Correctness {
   lemma SampleIsIndep(n: nat)
     requires n > 0
     ensures Independence.IsIndep(Model.Sample(n))
-  {
-    assert Independence.IsIndep(Model.Proposal(n)) by {
-      UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
-    }
-    assert Loops.UntilTerminatesAlmostSurely(Model.Proposal(n), Model.Accept(n)) by {
-      Model.SampleTerminates(n);
-    }
-    Loops.UntilIsIndep(Model.Proposal(n), Model.Accept(n));
-    reveal Model.Sample();
-  }
+  {}
 
   lemma IntervalSampleIsIndep(a: int, b: int)
     requires a < b

diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
@@ -18,24 +18,10 @@ module Uniform.Model {
   ************/
 
   // Definition 49
-  opaque ghost function Sample(n: nat): Monad.Hurd<nat>
+  opaque ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd<nat>)
     requires n > 0
-  {
-    SampleTerminates(n);
-    Loops.Until(Proposal(n), Accept(n))
-  }
-
-  function Proposal(n: nat): Monad.Hurd<nat>
-    requires n > 0
-  {
-    UniformPowerOfTwo.Model.Sample(2 * n)
-  }
-
-  function Accept(n: nat): nat -> bool
-    requires n > 0
-  {
-    (m: nat) => m < n
-  }
+    ensures Independence.IsIndep(h)
+    ensures forall s :: h(s).Result? ==> 0 <= h(s).value < n
 
   ghost function IntervalSample(a: int, b: int): (f: Monad.Hurd<int>)
     requires a < b
@@ -47,62 +33,11 @@ module Uniform.Model {
    Lemmas
   *******/
 
-  lemma SampleTerminates(n: nat)
-    requires n > 0
-    ensures
-      && Independence.IsIndep(Proposal(n))
-      && Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n)))
-      && Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n))
-  {
-    assert Independence.IsIndep(Proposal(n)) by {
-      UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
-    }
-    var e := iset s | Loops.ProposalIsAccepted(Proposal(n), Accept(n))(s);
-    assert e in Rand.eventSpace by {
-      var ltN := iset m: nat | m < n;
-      var resultsLtN := Monad.ResultsWithValueIn(ltN);
-      assert e == Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN);
-      assert Measures.PreImage(UniformPowerOfTwo.Model.Sample(2 * n), resultsLtN) in Rand.eventSpace by {
-        assert Independence.IsIndep(UniformPowerOfTwo.Model.Sample(2 * n)) by {
-          UniformPowerOfTwo.Correctness.SampleIsIndep(2 * n);
-        }
-        assert Measures.IsMeasurable(Rand.eventSpace, Monad.natResultEventSpace, UniformPowerOfTwo.Model.Sample(2 * n)) by {
-          Independence.IsIndepImpliesMeasurableNat(UniformPowerOfTwo.Model.Sample(2 * n));
-        }
-        assert resultsLtN in Monad.natResultEventSpace by {
-          Monad.LiftInEventSpaceToResultEventSpace(ltN, Measures.natEventSpace);
-        }
-      }
-    }
-    assert Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n))) by {
-      assert Rand.prob(e) > 0.0 by {
-        assert e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).value < n);
-        assert n <= NatArith.Power(2, NatArith.Log2Floor(2 * n)) by {
-          NatArith.NLtPower2Log2FloorOf2N(n);
-        }
-        calc {
-          Rand.prob(e);
-        == { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); }
-          n as real / (NatArith.Power(2, NatArith.Log2Floor(2 * n)) as real);
-        >
-          0.0;
-        }
-      }
-    }
-    assert Loops.UntilTerminatesAlmostSurely(Proposal(n), Accept(n)) by {
-      Loops.EnsureUntilTerminates(Proposal(n), Accept(n));
-    }
-  }
-
   lemma SampleBound(n: nat, s: Rand.Bitstream)
     requires n > 0
     requires Sample(n)(s).Result?
     ensures 0 <= Sample(n)(s).value < n
-  {
-    reveal Sample();
-    SampleTerminates(n);
-    Loops.UntilResultIsAccepted(Proposal(n), Accept(n), s);
-  }
+  {}
 
   lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream)
     requires a < b