From 732f5fd44e30fe05d37c6a806f6450ee4771c5b3 Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Tue, 12 Mar 2024 17:33:11 +0000
Subject: [PATCH] progress

---
 src/Util/FisherYates/Equivalence.dfy    | 10 ++++++++++
 src/Util/FisherYates/Implementation.dfy | 13 +++++++------
 src/Util/FisherYates/Interface.dfy      |  2 +-
 3 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/Util/FisherYates/Equivalence.dfy b/src/Util/FisherYates/Equivalence.dfy
index 98fbf7ba..e2602f29 100644
--- a/src/Util/FisherYates/Equivalence.dfy
+++ b/src/Util/FisherYates/Equivalence.dfy
@@ -7,6 +7,7 @@ module FisherYates.Equivalence {
   import Model
   import Rand
   import Monad
+  import opened Pos
 
   ghost predicate LoopInvariant<T>(prevI: nat, i: nat, a: array<T>, prevASeq: seq<T>, oldASeq: seq<T>, oldS: Rand.Bitstream, prevS: Rand.Bitstream, s: Rand.Bitstream)
     reads a
@@ -17,6 +18,15 @@ module FisherYates.Equivalence {
     && Model.Shuffle(prevASeq, prevI)(prevS) == Model.Shuffle(a[..], i)(s)
   }
 
+  ghost predicate LoopInvariant32<T>(prevI: nat32, i: nat32, a: array<T>, prevASeq: seq<T>, oldASeq: seq<T>, oldS: Rand.Bitstream, prevS: Rand.Bitstream, s: Rand.Bitstream)
+    reads a
+  {
+    && prevI as nat <= |prevASeq|
+    && i as nat <= a.Length - 1
+    && Model.Shuffle(oldASeq)(oldS) == Model.Shuffle(prevASeq, prevI as nat)(prevS)
+    && Model.Shuffle(prevASeq, prevI as nat)(prevS) == Model.Shuffle(a[..], i as nat)(s)
+  }
+
   lemma ShuffleElseClause<T>(a: array<T>, oldASeq: seq<T>, oldS: Rand.Bitstream, s: Rand.Bitstream)
     requires aLength: a.Length <= 1
     requires aInvariant: oldASeq == a[..]
diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy
index 0cb64e27..0ffc7385 100644
--- a/src/Util/FisherYates/Implementation.dfy
+++ b/src/Util/FisherYates/Implementation.dfy
@@ -55,15 +55,16 @@ module FisherYates.Implementation {
       requires a.Length < 0x8000_0000
       ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
     {
-      ghost var prevI, prevASeq, prevS := 0, a[..], s; // ghost
-      if a.Length > 1 {
-        for i := 0 to a.Length - 1
-          invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) // ghost
+      ghost var prevI, prevASeq, prevS := 0 as int32, a[..], s; // ghost
+
+      if (a.Length as nat32) > (1 as nat32) {
+        for i: nat32 := (0 as nat32) to (a.Length as nat32) - (1 as nat32)
+          invariant Equivalence.LoopInvariant32(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) // ghost
         {
           prevI, prevASeq, prevS := i, a[..], s; // ghost
-          var j := UniformIntervalSample32(i as int32, a.Length as int32);
+          var j := UniformIntervalSample32(i, a.Length as nat32);
           assert prevASeq == a[..]; // ghost
-          Swap32(a, i as nat32, j as nat32);
+          Swap32(a, i, j);
         }
       } else {
         Equivalence.ShuffleElseClause(a, old(a[..]), old(s), s); // ghost
diff --git a/src/Util/FisherYates/Interface.dfy b/src/Util/FisherYates/Interface.dfy
index 87cc8954..f2603bb7 100644
--- a/src/Util/FisherYates/Interface.dfy
+++ b/src/Util/FisherYates/Interface.dfy
@@ -23,7 +23,7 @@ module FisherYates.Interface {
       decreases *
       modifies `s, a
       requires a.Length < 0x8000_0000
-      ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
+      //ensures Model.Shuffle(old(a[..]))(old(s)) == Monad.Result(a[..], s)
 
   }
 }
\ No newline at end of file