fix: Use the right bitvector comparison in ComputeLessEq

Dafny adds a free invariant on each loops that states that the loop variable is
smaller than or equal to its initial value.  For bitvectors, Dafny produced ≥
instead of ≤, possibly due to a typo?

Specifically, the issue was:

- In `Translator.TrStatement.cs` (`TrLoop`):

  ```
  // include a free invariant that says that all completed iterations so far have only decreased the termination metric
  …
  Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, initDecr, null, null, true, false);
  ```

- In `Translator.cs` (`DecreasesCheck`):

  ```
  Bpl.Expr less, atmost, eq;
  ComputeLessEq(toks[i], types0[i], types1[i], ee0[i], ee1[i], out less, out atmost, out eq, includeLowerBound);
  ```

- In `Translator.cs` (`ComputeLessEq`):

  ```
  } else if (ty0 is BitvectorType) {
    BitvectorType bv = (BitvectorType)ty0;
    eq = Bpl.Expr.Eq(e0, e1);
    less = FunctionCall(tok, "lt_bv" + bv.Width, Bpl.Type.Bool, e0, e1);
    atmost = FunctionCall(tok, "ge_bv" + bv.Width, Bpl.Type.Bool, e0, e1);
  ```

  `"ge_bv"` is wrong.

* `Source/Dafny/Verifier/Translator.cs`
  (`ComputeLessEq`): Change `ge` into `le`.
* `Test/git-issues/git-issue-2511.dfy`:
  New file, showing the issue in all places where `ComputeLessEq` was used.

Introduced in 3f899b9.

Closes #2511.

RELEASE_NOTES.md

@@ -1,5 +1,7 @@
 # Upcoming
 
+- fix: Use the right bitvector comparison in decrease checks
+  (https://github.com/dafny-lang/dafny/pull/2512)
 - fix: Don't use native division and modulo operators for non-native int-based newtypes in Java and C#.
   (https://github.com/dafny-lang/dafny/pull/2416)
 - feat: Dafny now supports disjunctive (“or”) patterns in match statements and expressions.  Cases are separated by `|` characters.  Disjunctive patterns may not appear within other patterns and may not bind variables.

Source/Dafny/Verifier/Translator.cs

@@ -9287,7 +9287,7 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
         BitvectorType bv = (BitvectorType)ty0;
         eq = Bpl.Expr.Eq(e0, e1);
         less = FunctionCall(tok, "lt_bv" + bv.Width, Bpl.Type.Bool, e0, e1);
-        atmost = FunctionCall(tok, "ge_bv" + bv.Width, Bpl.Type.Bool, e0, e1);
+        atmost = FunctionCall(tok, "le_bv" + bv.Width, Bpl.Type.Bool, e0, e1);
 
       } else if (ty0 is BigOrdinalType) {
         eq = Bpl.Expr.Eq(e0, e1);

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

@@ -0,0 +1,59 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module WhileLoops {
+  lemma false_lemma()
+    ensures false
+  {
+    var tmp: bv64 := 1;
+    while tmp != 0
+      decreases tmp
+    {
+      tmp := tmp >> 1;
+    }
+    assert false; // Assertion failure
+  }
+}
+
+module Recursion {
+  method Infloop(b: bv8)
+    requires b == 3
+    ensures false
+    decreases b
+  {
+    Infloop'(b + 1); // decreases clause might not decrease
+  }
+
+  method Infloop'(b: bv8)
+    requires b == 4
+    decreases b, 0
+    ensures false
+  {
+    Infloop(b - 1);
+  }
+
+  method Boom()
+    ensures false
+  {
+    Infloop(3);
+  }
+}
+
+module Traits {
+  trait T {
+    method Infloop(b: bv8)
+      requires b == 3
+      ensures false
+      decreases b
+  }
+
+  class C extends T {
+    method Infloop(b: bv8) // method's decreases clause must be below or equal to that in the trait
+      requires b == 3
+      ensures false
+      decreases b + 1, 0
+    {
+      (this as T).Infloop(b);
+    }
+  }
+}

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

@@ -0,0 +1,5 @@
+git-issue-2511.dfy(14,11): Error: assertion might not hold
+git-issue-2511.dfy(24,12): Error: decreases clause might not decrease
+git-issue-2511.dfy(51,11): Error: method's decreases clause must be below or equal to that in the trait
+
+Dafny program verifier finished with 3 verified, 3 errors