From 68f22869c5ef8ea7d6c380d029a8625f2d1f2b24 Mon Sep 17 00:00:00 2001
From: stefan-aws <stefanze@amazon.com>
Date: Thu, 21 Mar 2024 17:00:05 +0000
Subject: [PATCH] remove split on every assert

---
 src/Distributions/Uniform/Interface.dfy | 3 ++-
 src/Util/FisherYates/Implementation.dfy | 5 +++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy
index e71aae85..4bfa0311 100644
--- a/src/Distributions/Uniform/Interface.dfy
+++ b/src/Distributions/Uniform/Interface.dfy
@@ -40,12 +40,13 @@ module Uniform.Interface {
       ensures u < n
       ensures Model.Sample(n as nat)(old(s)) == Monad.Result(u as nat, s)
 
-    method UniformIntervalSample32(a: int32, b: int32) returns (u: int32)
+    method UniformIntervalSample32<T>(a: int32, b: int32, ghost arr: array<T>) returns (u: int32)
       modifies `s
       decreases *
       requires 0 < b as int - a as int < 0x8000_0000
       ensures a <= u < b
       ensures Model.IntervalSample(a as int, b as int)(old(s)) == Monad.Result(u as int, s)
+      ensures old(arr[..]) == arr[..]
     {
       var v := UniformSample32(b-a);
       assert Model.Sample(b as int - a as int)(old(s)) == Monad.Result(v as nat, s);
diff --git a/src/Util/FisherYates/Implementation.dfy b/src/Util/FisherYates/Implementation.dfy
index 803b3848..036b59f5 100644
--- a/src/Util/FisherYates/Implementation.dfy
+++ b/src/Util/FisherYates/Implementation.dfy
@@ -13,7 +13,7 @@ module FisherYates.Implementation {
 
   trait {:termination false} Trait extends Interface.Trait {
 
-    method {:vcs_split_on_every_assert} Shuffle<T>(a: array<T>)
+    method Shuffle<T>(a: array<T>)
       decreases *
       modifies `s, a
       requires a.Length < 0x8000_0000
@@ -26,9 +26,10 @@ module FisherYates.Implementation {
           invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) // ghost
         {
           prevI, prevASeq, prevS := i, a[..], s; // ghost
-          var j := UniformIntervalSample32(i, a.Length as nat32);
+          var j := UniformIntervalSample32(i, a.Length as nat32, a);
           assert prevASeq == a[..]; // ghost
           Swap(a, i, j);
+          assert Equivalence.LoopInvariant(prevI, i+1, a, prevASeq, old(a[..]), old(s), prevS, s); // ghost
         }
       } else {
         Equivalence.ShuffleElseClause(a, old(a[..]), old(s), s); // ghost