fix: Remove multiset cardinality cap in Python (#4014)

Fixes #4012.

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -1410,7 +1410,10 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool
         ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
       switch (op) {
         case ResolvedUnaryOp.Cardinality:
-          TrParenExpr("len", expr, wr, inLetExprBody, wStmts);
+          var multiset = expr.Type.AsMultiSetType != null;
+          if (!multiset) { wr.Write("len"); }
+          TrParenExpr(expr, wr, inLetExprBody, wStmts);
+          if (multiset) { wr.Write(".cardinality"); }
           break;
         case ResolvedUnaryOp.BitwiseNot:
           TrParenExpr("~", expr, wr, inLetExprBody, wStmts);

Source/DafnyRuntime/DafnyRuntime.py

@@ -238,7 +238,8 @@ class MultiSet(Counter):
     def __dafnystr__(self) -> str:
         return 'multiset{' + ', '.join(map(string_of, self.elements())) + '}'
 
-    def __len__(self):
+    @property
+    def cardinality(self):
         return reduce(lambda acc, key: acc + self[key], self, 0)
 
     def union(self, other):
@@ -272,7 +273,7 @@ def issubset(self, other):
         return all(self[key] <= other[key] for key in frozenset(self).union(frozenset(other)))
 
     def ispropersubset(self, other):
-        return self.issubset(other) and len(self) < len(other)
+        return self.issubset(other) and self.cardinality < other.cardinality
 
     def set(self, key, value):
         set = Counter(self)

Test/git-issues/git-issue-4012.dfy

@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:4 /compileTarget:py "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+    var x: multiset<int> := multiset{};
+    x := x[1 := 18446744073709551616];
+    print |x|, "\n";
+}

Test/git-issues/git-issue-4012.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+18446744073709551616

docs/dev/news/4014.fix

@@ -0,0 +1 @@
+Remove multiset cardinality cap in Python