Remove split-on-every-assert by introducing ghost array input (#171)

Doesn't impact the compiled code.

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).

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);

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

src/interop/java/Full/Random.java

@@ -43,8 +43,8 @@ public java.math.BigInteger UniformIntervalSample(java.math.BigInteger a, java.m
     return Uniform.Interface._Companion_Trait.UniformIntervalSample(this, a, b);
   }
 
-  public int UniformIntervalSample32(int a, int b) {
-    return Uniform.Interface._Companion_Trait32.UniformIntervalSample32(this, a, b);
+  public <__T>  int UniformIntervalSample32(dafny.TypeDescriptor<__T> _td___T, int a, int b) {
+    return Uniform.Interface._Companion_Trait32.UniformIntervalSample32(_td___T, this, a, b);
   }
 
   public java.math.BigInteger UniformSample(java.math.BigInteger n) {