From 34b84d995990428a1e6201270fed738610e01149 Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Tue, 30 Jan 2024 18:17:39 +0000
Subject: [PATCH] InductionHypothesisPrecondition2 proof

---
 audit.log                            |  5 +--
 src/Util/FisherYates/Correctness.dfy | 63 ++++++++++------------------
 2 files changed, 25 insertions(+), 43 deletions(-)

diff --git a/audit.log b/audit.log
index a2ea568f..ebcd3758 100644
--- a/audit.log
+++ b/audit.log
@@ -46,6 +46,5 @@ src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure:
 src/ProbabilisticProgramming/RandomSource.dfy(54,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(67,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
-src/Util/FisherYates/Correctness.dfy(104,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
-src/Util/FisherYates/Correctness.dfy(113,12): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
-src/Util/FisherYates/Correctness.dfy(147,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
+src/Util/FisherYates/Correctness.dfy(109,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
+src/Util/FisherYates/Correctness.dfy(99,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
diff --git a/src/Util/FisherYates/Correctness.dfy b/src/Util/FisherYates/Correctness.dfy
index 0ab59b09..0e040c0f 100644
--- a/src/Util/FisherYates/Correctness.dfy
+++ b/src/Util/FisherYates/Correctness.dfy
@@ -74,12 +74,7 @@ module FisherYates.Correctness {
       Rand.ProbIsProbabilityMeasure();
       assert Measures.IsProbability(Rand.eventSpace, Rand.prob);
     } else {
-      calc {
-        true;
-        |xs[i..]| > 1;
-        |xs| - i > 1;
-        |xs| > i + 1;
-      }
+      assert |xs| > i + 1;
       var h := Uniform.Model.IntervalSample(i, |xs|);
       assert HIsIndependent: Independence.IsIndepFunction(h) by {
         Uniform.Correctness.IntervalSampleIsIndep(i, |xs|);
@@ -106,41 +101,8 @@ module FisherYates.Correctness {
       var ys := Model.Swap(xs, i, j);
       var e' := iset s | Model.Shuffle(ys, i+1)(s).Result? && Model.Shuffle(ys, i+1)(s).value[i+1..] == p[i+1..];
       assert InductionHypothesis: e' in Rand.eventSpace && Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) by {
-        assert forall a, b | i+1 <= a < b < |ys| :: ys[a] != ys[b] by {
-          forall a, b | i+1 <= a < b < |ys|
-            ensures ys[a] != ys[b]
-          {
-            assume {:axiom} false;
-             /* if x == ys[i] {
-              calc {
-                multiset(ys[i+1..])[x];
-                multiset(ys[i..])[x] - multiset([ys[i]])(x);
-                multiset(ys[i..])[x] - 1;
-
-              }
-            }
-
-            calc {
-              1;
-            <= { assert x in ys[i+1..]; }
-              multiset(ys[i+1..])[x];
-            }
-            calc {
-              multiset(ys[i+1..])[x];
-            ==
-              (multiset(ys) - multiset(ys[..i]))[x];
-            ==
-              multiset(ys)[x] - multiset(ys[..i])[x];
-            ==
-              multiset(xs)[x] - multiset(xs[..i])[x];
-            == { }
-              1 - multiset(ys[..i])[x];
-            <=
-              1
-            } */
-          }
-        }
         InductionHypothesisPrecondition1(xs, ys, p, i, j);
+        InductionHypothesisPrecondition2(xs, ys, p, i, j);
         CorrectnessFisherYatesUniqueElementsGeneral(ys, p, i+1);
       }
       assert DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
@@ -228,6 +190,27 @@ module FisherYates.Correctness {
     }
   }
 
+  lemma InductionHypothesisPrecondition2<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat)
+    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 i <= j < |xs| && xs[j] == p[i]
+    requires ys == Model.Swap(xs, i, j)
+    requires |xs[i..]| > 1
+    ensures forall a, b | i+1 <= a < b < |ys| :: ys[a] != ys[b]
+  {
+    assert forall a, b | i+1 <= a < b < |ys| :: ys[a] != ys[b] by {
+      forall a, b | i+1 <= a < b < |ys|
+        ensures ys[a] != ys[b]
+      {
+        if a == i+1 {
+        }
+      }
+    }
+  }
+
   lemma EInEventSpace<T(!new)>(xs: seq<T>, p: seq<T>, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
     requires |xs| == |p|
     requires DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e')