fix: Add missing triggers to Map#Card axioms in Boogie prelude (dafny…

…-lang#2417)

Closes dafny-lang#2380.

@atomb , can you show me how to run a performance regression run on
this? I'm not sure how it will impact our customers.

Co-authored-by: Mikaël Mayer <[email protected]>

Source/DafnyCore/DafnyPrelude.bpl

@@ -1207,13 +1207,13 @@ axiom (forall<U, V> m: Map U V ::
   m == Map#Empty() || (exists k, v: Box :: Map#Items(m)[$Box(#_System._tuple#2._#Make2(k, v))]));
 
 axiom (forall<U, V> m: Map U V ::
-  { Set#Card(Map#Domain(m)) }
+  { Set#Card(Map#Domain(m)) } { Map#Card(m) }
   Set#Card(Map#Domain(m)) == Map#Card(m));
 axiom (forall<U, V> m: Map U V ::
-  { Set#Card(Map#Values(m)) }
+  { Set#Card(Map#Values(m)) } { Map#Card(m) }
   Set#Card(Map#Values(m)) <= Map#Card(m));
 axiom (forall<U, V> m: Map U V ::
-  { Set#Card(Map#Items(m)) }
+  { Set#Card(Map#Items(m)) } { Map#Card(m) }
   Set#Card(Map#Items(m)) == Map#Card(m));
 
 // The set of Values of a Map can be obtained by the function Map#Values, which is

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

@@ -0,0 +1,32 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M0(t: map<int, int>, k: int)
+  requires k in t
+{
+  if * {
+    assert |t| == |t - {k}| + 1;
+  } else if * {
+    assume t.Items == {(1, 2), (3, 4)};
+    assert |t| == 2;
+  } else {
+    assume t.Values == {2, 3, 4};
+    assert |t| >= 2;
+  }
+}
+
+method M0'(t: map<int, int>, k: int)
+  requires k in t
+{
+  if * {
+    var _ := |(t - {k}).Keys|;
+    assert |t| == |t - {k}| + 1;
+  } else if * {
+    assume t.Items == {(1, 2), (3, 4)};
+    var _ := |t.Items|;
+    assert |t| == 2;
+  } else {
+    assume t.Values == {2, 3, 4};
+    assert |t.Values| >= 2;
+  }
+}

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

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