proof of ResultsIndependent and brittleness of fisher-yates

dafny-lang · Mar 5, 2024 · 59913bf · 59913bf
1 parent bf5ddee
commit 59913bf
Show file tree

Hide file tree

Showing 3 changed files with 73 additions and 20 deletions.
diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy
@@ -43,4 +43,8 @@ module Uniform.Model {
     SampleBound(b-a, s);
   }
 
+  lemma {:axiom} IntervalSampleIsMeasurePreserving(a: int, b: int)
+    requires a < b
+    ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => IntervalSample(a, b)(s).rest)
+
 }
diff --git a/src/ProbabilisticProgramming/Independence.dfy b/src/ProbabilisticProgramming/Independence.dfy
@@ -40,6 +40,7 @@ module Independence {
   )
     requires hIndep: IsIndepFunction(h)
     requires bMeasurable: bSeeds in Rand.eventSpace
+    requires hIsMeasurePreserving: Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest)
     ensures Rand.prob(Monad.BitstreamsWithValueIn(h, aSet) * Monad.BitstreamsWithRestIn(h, bSeeds)) == Rand.prob(Monad.BitstreamsWithValueIn(h, aSet)) * Rand.prob(bSeeds)
   {
     var aSeeds := Monad.BitstreamsWithValueIn(h, aSet);
@@ -52,7 +53,16 @@ module Independence {
       assert Measures.AreIndepEvents(Rand.eventSpace, Rand.prob, aSeeds, restBSeeds);
     }
     assert Rand.prob(restBSeeds) == Rand.prob(bSeeds) by {
-      assume {:axiom} false; // TODO
+      calc {
+        Rand.prob(restBSeeds);
+        Rand.prob(Monad.BitstreamsWithRestIn(h, bSeeds));
+        { assert Monad.BitstreamsWithRestIn(h, bSeeds) == iset s | h(s).rest in bSeeds; }
+        Rand.prob(iset s | h(s).rest in bSeeds);
+        { assert (iset s | h(s).rest in bSeeds) == Measures.PreImage(s => h(s).rest, bSeeds); }
+        Rand.prob(Measures.PreImage(s => h(s).rest, bSeeds));
+        { reveal bMeasurable; reveal hIsMeasurePreserving; }
+        Rand.prob(bSeeds);
+      }
     }
   }
 

diff --git a/src/Util/FisherYates/Correctness.dfy b/src/Util/FisherYates/Correctness.dfy
@@ -150,6 +150,9 @@ module FisherYates.Correctness {
     var e := iset s | Model.Shuffle(xs, i)(s).value[i..] == p[i..];
     assert |xs| > i + 1;
     var h := Uniform.Model.IntervalSample(i, |xs|);
+    assert hIsMeasurePreserving: Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest) by {
+      Uniform.Model.IntervalSampleIsMeasurePreserving(i, |xs|);
+    }
     assert HIsIndependent: Independence.IsIndepFunction(h) by {
       Uniform.Correctness.IntervalSampleIsIndep(i, |xs|);
       Independence.IsIndepImpliesIsIndepFunction(h);
@@ -238,33 +241,68 @@ module FisherYates.Correctness {
     assert DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
       DecomposeE(xs, ys, p, i, j, h, A, e, e');
     }
+
     assert CorrectnessPredicate(xs, p, i) by {
       reveal DecomposeE;
       reveal HIsIndependent;
       reveal BitStreamsInA;
-      assert e' in Rand.eventSpace && Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) by {
-        assert e' in Rand.eventSpace by {
-          assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; }
-          assert e' == CorrectnessConstructEvent(ys, p, i+1);
-        }
-        calc {
-          Rand.prob(e');
-          { assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; }
-            assert e' == CorrectnessConstructEvent(ys, p, i+1); }
-          1.0 / (NatArith.FactorialTraditional(|ys|-(i+1)) as real);
-          { assert |xs| == |ys|;
-            assert |ys|-(i+1) == |xs|-(i+1);
-            assert NatArith.FactorialTraditional(|ys|-(i+1)) == NatArith.FactorialTraditional(|xs|-(i+1));
-            assert (NatArith.FactorialTraditional(|ys|-(i+1)) as real) == (NatArith.FactorialTraditional(|xs|-(i+1)) as real); }
-          1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real);
-        }
+      reveal InductionHypothesis;
+      reveal hIsMeasurePreserving;
+      CorrectnessFisherYatesUniqueElementsGeneralGreater1Helper(xs, ys, p, i, j, h, A, e, e');
+    }
+
+  }
+
+  lemma CorrectnessFisherYatesUniqueElementsGeneralGreater1Helper<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
+    decreases |xs| - i
+    requires i <= |xs|
+    requires i <= |p|
+    requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
+    requires |xs| == |p|
+    requires multiset(p[i..]) == multiset(xs[i..])
+    requires |xs[i..]| > 1
+    requires i <= j < |xs| && xs[j] == p[i]
+    requires |xs| == |ys|
+    requires ys == Model.Swap(xs, i, j)
+    requires e == CorrectnessConstructEvent(xs, p, i)
+    requires e' == CorrectnessConstructEvent(ys, p, i+1)
+    requires DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') 
+    requires HIsIndependent: Independence.IsIndepFunction(h)
+    requires BitStreamsInA: Monad.BitstreamsWithValueIn(h, A) == (iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j))
+    requires InductionHypothesis: CorrectnessPredicate(ys, p, i+1)
+    requires hIsMeasurePreserving: Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest)
+    ensures CorrectnessPredicate(xs, p, i)
+  {
+    reveal DecomposeE;
+    reveal HIsIndependent;
+    reveal BitStreamsInA;
+    assert e' in Rand.eventSpace && Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) by {
+      assert e' in Rand.eventSpace by {
+        assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; }
+        assert e' == CorrectnessConstructEvent(ys, p, i+1);
       }
-      ProbabilityOfE(xs, ys, p, i, j, h, A, e, e');
+      calc {
+        Rand.prob(e');
+        { assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; }
+          assert e' == CorrectnessConstructEvent(ys, p, i+1); }
+        1.0 / (NatArith.FactorialTraditional(|ys|-(i+1)) as real);
+        { assert |xs| == |ys|;
+          assert |ys|-(i+1) == |xs|-(i+1);
+          assert NatArith.FactorialTraditional(|ys|-(i+1)) == NatArith.FactorialTraditional(|xs|-(i+1));
+          assert (NatArith.FactorialTraditional(|ys|-(i+1)) as real) == (NatArith.FactorialTraditional(|xs|-(i+1)) as real); }
+        1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real);
+      }
+    }
+    reveal hIsMeasurePreserving;
+    assert e in Rand.eventSpace by {
       EInEventSpace(xs, p, h, A, e, e');
     }
-
+    assert Rand.prob(e) == 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real) by {
+      ProbabilityOfE(xs, ys, p, i, j, h, A, e, e');
+    }
   }
 
+
   lemma BitStreamsInA<T(!new)>(xs: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>)
     requires i <= |xs|
     requires i <= |p|
@@ -489,6 +527,7 @@ module FisherYates.Correctness {
     requires |xs| == |ys|
     requires DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e')
     requires HIsIndependent: Independence.IsIndepFunction(h)
+    requires hIsMeasurePreserving: Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest)
     requires InductionHypothesis: Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real)
     requires BitStreamsInA: Monad.BitstreamsWithValueIn(h, A) == (iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j))
     ensures
@@ -498,7 +537,7 @@ module FisherYates.Correctness {
       Rand.prob(e);
       { reveal DecomposeE; }
       Rand.prob(Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e'));
-      { reveal HIsIndependent; reveal InductionHypothesis; Independence.ResultsIndependent(h, A, e'); }
+      { reveal HIsIndependent; reveal InductionHypothesis; reveal hIsMeasurePreserving; Independence.ResultsIndependent(h, A, e'); }
       Rand.prob(Monad.BitstreamsWithValueIn(h, A)) * Rand.prob(e');
       { assert Rand.prob(Monad.BitstreamsWithValueIn(h, A)) == Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) by { reveal BitStreamsInA; } }
       Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) * Rand.prob(e');