chore: Remove Dafny trigger warnings (#160)

This removes Dafny warnings around `forall` statments lacking a `{trigger}`

.github/workflows/reusable-tests.yml

@@ -45,8 +45,8 @@ jobs:
       - name: Generate Report
         run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-resource-count 40000000
 
-      - uses: actions/upload-artifact@v2  # upload test results
+      - uses: actions/upload-artifact@v4  # upload test results
         with:
-          name: verification-results
+          name: verification-results-${{ inputs.dafny-version }}
           path: '**/TestResults/*.trx'
           if-no-files-found: error

src/NonlinearArithmetic/DivMod.dfy

@@ -209,7 +209,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)}
               :: 0 < d &&  R == a%d + b%d - (a+b)%d ==> d*((a+b)/d) - R == d*(a/d) + d*(b/d)
   {
-    forall (a: int, b: int, d: int, R: int | 0< d &&  R == a%d + b%d - (a+b)%d)
+    forall (a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)} | 0< d &&  R == a%d + b%d - (a+b)%d)
       ensures d*((a+b)/d) - R == d*(a/d) + d*(b/d)
     {
       LemmaDividingSums(a, b, d, R);
@@ -724,7 +724,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, a: int, d: int {:trigger a / d, x * d, x * a}
               :: 0 < x && 0 <= a && 0 < d ==> 0 < x * d  &&  a / d == (x * a) / (x * d)
   {
-    forall x: int, a: int, d: int | 0 < x && 0 <= a && 0 < d
+    forall x: int, a: int, d: int {:nowarn} | 0 < x && 0 <= a && 0 < d
       ensures 0 < x * d  &&  a / d == (x * a) / (x * d)
     {
       LemmaDivMultiplesVanishQuotient(x, a, d);
@@ -747,7 +747,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall a: int, r: int, d: int {:trigger d * ((a + r) / d)}
               :: 0 < d && a % d == 0 && 0 <= r < d ==> a == d * ((a + r) / d)
   {
-    forall a: int, r: int, d: int | 0 < d && a % d == 0 && 0 <= r < d
+    forall a: int, r: int, d: int {:trigger d * ((a + r) / d)} | 0 < d && a % d == 0 && 0 <= r < d
       ensures a == d * ((a + r) / d)
     {
       LemmaRoundDown(a, r, d);
@@ -770,7 +770,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, b: int, d: int {:trigger (d * x + b) / d}
               :: 0 < d && 0 <= b < d ==> (d * x + b) / d == x
   {
-    forall x: int, b: int, d: int | 0 < d && 0 <= b < d
+    forall x: int, b: int, d: int {:trigger (d * x + b) / d} | 0 < d && 0 <= b < d
       ensures (d * x + b) / d == x
     {
       LemmaDivMultiplesVanishFancy(x, b, d);
@@ -936,7 +936,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall a: int, b: int, c: int {:trigger b * (a / b) % (b * c)}
               :: 0 <= a && 0 < b && 0 < c ==> 0 < b * c && (b * (a / b) % (b * c)) <= b * (c - 1)
   {
-    forall a: int, b: int, c: int | 0 <= a && 0 < b && 0 < c
+    forall a: int, b: int, c: int {:nowarn} | 0 <= a && 0 < b && 0 < c
       ensures 0 < b * c && (b * (a / b) % (b * c)) <= b * (c - 1)
     {
       LemmaPartBound1(a, b, c);
@@ -1205,7 +1205,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, y: int, m: int {:trigger (x + y) % m}
               :: 0 < m ==> (x + (y % m)) % m == (x + y) % m
   {
-    forall x: int, y: int, m: int | 0 < m
+    forall x: int, y: int, m: int {:trigger (x + y) % m} | 0 < m
       ensures (x + (y % m)) % m == (x + y) % m
     {
       LemmaAddModNoopRight(x, y, m);
@@ -1243,7 +1243,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, y: int, m: int {:trigger (x - y) % m}
               :: 0 < m ==> (x - (y % m)) % m == (x - y) % m
   {
-    forall x: int, y: int, m: int | 0 < m
+    forall x: int, y: int, m: int {:trigger (x - y) % m} | 0 < m
       ensures (x - (y % m)) % m == (x - y) % m
     {
       LemmaSubModNoopRight(x, y, m);
@@ -1306,7 +1306,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, d: int, q: int, r: int {:trigger q * d + r, x % d}
               :: d != 0 && 0 <= r < d && x == q * d + r ==> q == x / d && r == x % d
   {
-    forall x: int, d: int, q: int, r: int | d != 0 && 0 <= r < d && x == q * d + r
+    forall x: int, d: int, q: int, r: int {:nowarn} | d != 0 && 0 <= r < d && x == q * d + r
       ensures q == x / d && r == x % d
     {
       LemmaFundamentalDivModConverse(x, d, q, r);
@@ -1499,7 +1499,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, k: int, d: int {:trigger x % (d * k)}
               :: 1 < d && 0 < k ==> 0 < d * k && x % d <= x % (d * k)
   {
-    forall x: int, k: int, d: int | 1 < d && 0 < k
+    forall x: int, k: int, d: int {:nowarn} | 1 < d && 0 < k
       ensures d * k > 0 && x % d <= x % (d * k)
     {
       LemmaModOrdering(x, k, d);
@@ -1563,7 +1563,7 @@ module {:options "-functionSyntax:4"} DivMod {
     ensures forall x: int, y: int, z: int {:trigger y * z, x % y}
               :: 0 <= x && 0 < y && 0 < z ==> y * z > 0 && (x % y) % (y * z) < y
   {
-    forall x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z
+    forall x: int, y: int, z: int {:nowarn} | 0 <= x && 0 < y && 0 < z
       ensures y * z > 0 && (x % y) % (y * z) < y
     {
       LemmaPartBound2(x, y, z);