From 74155912cc5bf28cfd13218891ebfd5595e34246 Mon Sep 17 00:00:00 2001
From: olivier-aws <obouisso@amazon.com>
Date: Fri, 8 Nov 2024 10:59:02 -0500
Subject: [PATCH] Fix issue 5554 soundness (#5874)

### Description
This PR updates the Dafny CS runtime to use BigIntegers instead of int32
when retrieving the number of elements in a multiset. As this number may
be over INT_MAX, this change avoids potential overflows. This is similar
to what is done in the Java runtime.

### How has this been tested?
A test was added:
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy

<small>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).</small>
---
 Source/DafnyRuntime/DafnyRuntime.cs                 |  4 +++-
 .../LitTests/LitTest/git-issues/git-issue-5554.dfy  | 13 +++++++++++++
 .../LitTest/git-issues/git-issue-5554.dfy.expect    |  1 +
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect

diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
index 675bd4155e3..a8023c7886f 100755
--- a/Source/DafnyRuntime/DafnyRuntime.cs
+++ b/Source/DafnyRuntime/DafnyRuntime.cs
@@ -547,7 +547,9 @@ public override string ToString() {
       return s + "}";
     }
     public static bool IsProperSubsetOf(IMultiSet<T> th, IMultiSet<T> other) {
-      return th.Count < other.Count && IsSubsetOf(th, other);
+      // Be sure to use ElementCount to avoid casting into 32 bits
+      // integers that could lead to overflows (see https://github.com/dafny-lang/dafny/issues/5554)
+      return th.ElementCount < other.ElementCount && IsSubsetOf(th, other);
     }
     public static bool IsSubsetOf(IMultiSet<T> th, IMultiSet<T> other) {
       var a = FromIMultiSet(th);
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy
new file mode 100644
index 00000000000..95b3830b33b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy
@@ -0,0 +1,13 @@
+// RUN:  %dafny -compile:4 -compileTarget:cs "%s"
+
+datatype MultisetContainer = EmptySet | BooleanMultiset(containerSet: multiset<bool>)
+
+method Main() {
+    var initialMultiset := multiset{false};
+    
+    for iteration := 0 to 31 {
+        var multisetInstance := BooleanMultiset(initialMultiset); 
+        initialMultiset := initialMultiset + multisetInstance.containerSet;  
+    }
+    print initialMultiset > initialMultiset;
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect
new file mode 100644
index 00000000000..c508d5366f7
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5554.dfy.expect
@@ -0,0 +1 @@
+false