Isolate assertions attribute (#5247)

### Description
Add `{:isolate_assertions}` attribute, that has the same meaning as
`{:vcs_split_on_every_assert}`

### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet test` -->

<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/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1927,6 +1927,8 @@ public static bool RewriteInExpr(Expression s, bool aggressive) {
  return false;
  }
 
+ private static readonly Dictionary<string, string> NullaryAttributesToTranslate;
+
  private static readonly HashSet<string> NullaryAttributesToCopy = new(new[] {
  "focus",
  "ignore",
@@ -1958,6 +1960,15 @@ public static bool RewriteInExpr(Expression s, bool aggressive) {
  "error"
  });
 
+ static ExpressionTranslator() {
+ NullaryAttributesToTranslate = new() {
+ {
+ "isolate_assertions",
+ "vcs_split_on_every_assert"
+ }
+ };
+ }
+
  private QKeyValue TrBooleanAttribute(string name, Expression arg, QKeyValue rest) {
  var boolArg = RemoveLit(TrExpr(arg));
  return boolArg is Boogie.LiteralExpr { IsTrue: true } or Boogie.LiteralExpr { IsFalse: true }
@@ -1995,7 +2006,9 @@ public QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) {
  continue;
  }
 
- if (NullaryAttributesToCopy.Contains(name) && attr.Args.Count == 0) {
+ if (NullaryAttributesToTranslate.ContainsKey(name) && attr.Args.Count == 0) {
+ kv = new QKeyValue(attr.tok, NullaryAttributesToTranslate[name], new List<object>(), kv);
+ } else if (NullaryAttributesToCopy.Contains(name) && attr.Args.Count == 0) {
  kv = new QKeyValue(attr.tok, name, new List<object>(), kv);
  } else if (BooleanAttributesToCopy.Contains(name) && attr.Args.Count == 1) {
  kv = TrBooleanAttribute(name, attr.Args[0], kv);

Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs

@@ -134,7 +134,7 @@ public async Task DiagnosticsForVerificationTimeoutHasNameAsRange() {
  [Fact]
  public async Task NoFlickeringWhenMixingCorrectAndErrorBatches() {
  var source = @"
-method {:vcs_split_on_every_assert} Foo(x: int) {
+method {:isolate_assertions} Foo(x: int) {
  if (x == 0) {
  assert true;
  } else if (x == 1) {
@@ -158,7 +158,7 @@ public async Task NoFlickeringWhenMixingCorrectAndErrorBatches() {
  [Fact]
  public async Task IncrementalBatchDiagnostics() {
  var source = @"
-method {:vcs_split_on_every_assert} Foo(x: int) {
+method {:isolate_assertions} Foo(x: int) {
  if (x == 0) {
  assert false;
  } else {

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -26,7 +26,7 @@ public class HoverVerificationTest : ClientBasedLanguageServerTest {
  [Fact(Timeout = MaxTestExecutionTimeMs)]
  public async Task HoverPutsErrorsFirst() {
  var documentItem = await GetDocumentItem(@"
-method {:vcs_split_on_every_assert} Test(x: int, y: int)
+method {:isolate_assertions} Test(x: int, y: int)
  requires x < y
 {
  var callIt := giveIt(x, y);
@@ -118,7 +118,7 @@ await SetUp(o => {
  // LineVerificationStatusOption.Instance.Set(o, true);
  });
  var documentItem = await GetDocumentItem(@"
-method {:vcs_split_on_every_assert} f(x: int) {
+method {:isolate_assertions} f(x: int) {
  assert x >= 2; // Hover #1
  assert x >= 1; // Hover #2
 }

Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy

@@ -746,7 +746,7 @@ abstract module {:options "/functionSyntax:4"} Dafny {
  }
  }
 
- method {:tailrecursion} {:vcs_split_on_every_assert} AppendOptimized<T>(builder: Vector<T>, e: Sequence<T>, stack: Vector<Sequence<T>>)
+ method {:tailrecursion} {:isolate_assertions} AppendOptimized<T>(builder: Vector<T>, e: Sequence<T>, stack: Vector<Sequence<T>>)
  requires e.Valid()
  requires builder.Valid()
  requires stack.Valid()

Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy

@@ -1281,7 +1281,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
  }
  }
 
- lemma {:vcs_split_on_every_assert} LemmaModNegNeg(x: int, d: int)
+ lemma {:isolate_assertions} LemmaModNegNeg(x: int, d: int)
  requires 0 < d
  ensures x % d == (x * (1 - d)) % d
  {

Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/DivInternals.dfy

@@ -108,7 +108,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivInternals {
  (-n <= z < 0 && (x - y) / n == x / n - y / n - 1)
  }
 
- lemma {:vcs_split_on_every_assert} LemmaDivAutoAuxPlus(n: int)
+ lemma {:isolate_assertions} LemmaDivAutoAuxPlus(n: int)
  requires n > 0 && ModAuto(n)
  ensures DivAutoPlus(n)
  {
@@ -137,7 +137,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivInternals {
  }
  }
 
- lemma {:vcs_split_on_every_assert} LemmaDivAutoAuxMinusHelper(n: int)
+ lemma {:isolate_assertions} LemmaDivAutoAuxMinusHelper(n: int)
  requires n > 0 && ModAuto(n)
  ensures forall i, j ::
  && (j >= 0 && DivMinus(n, i, j) ==> DivMinus(n, i, j + n))

Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternals.dfy

@@ -76,7 +76,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.ModInternals {
  }
  }
 
- lemma {:vcs_split_on_every_assert} LemmaDivAddDenominator(n: int, x: int)
+ lemma {:isolate_assertions} LemmaDivAddDenominator(n: int, x: int)
  requires n > 0
  ensures (x + n) / n == x / n + 1
  {
@@ -96,7 +96,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.ModInternals {
  }
  }
 
- lemma {:vcs_split_on_every_assert} LemmaDivSubDenominator(n: int, x: int)
+ lemma {:isolate_assertions} LemmaDivSubDenominator(n: int, x: int)
  requires n > 0
  ensures (x - n) / n == x / n - 1
  {
@@ -116,7 +116,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.ModInternals {
  }
  }
 
- lemma {:vcs_split_on_every_assert} LemmaModAddDenominator(n: int, x: int)
+ lemma {:isolate_assertions} LemmaModAddDenominator(n: int, x: int)
  requires n > 0
  ensures (x + n) % n == x % n
  {
@@ -136,7 +136,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.ModInternals {
  }
  }
 
- lemma {:vcs_split_on_every_assert} LemmaModSubDenominator(n: int, x: int)
+ lemma {:isolate_assertions} LemmaModSubDenominator(n: int, x: int)
  requires n > 0
  ensures (x - n) % n == x % n
  {
@@ -193,7 +193,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.ModInternals {
  }
 
  /* proves the quotient remainder theorem */
- lemma {:vcs_split_on_every_assert} LemmaQuotientAndRemainder(x: int, q: int, r: int, n: int)
+ lemma {:isolate_assertions} LemmaQuotientAndRemainder(x: int, q: int, r: int, n: int)
  requires n > 0
  requires 0 <= r < n
  requires x == q * n + r

Source/DafnyStandardLibraries/src/Std/Arithmetic/LittleEndianNat.dfy

@@ -50,7 +50,7 @@ abstract module {:disableNonlinearArithmetic} Std.Arithmetic.LittleEndianNat {
  }
 
  /* Given the same sequence, ToNatRight and ToNatLeft return the same nat. */
- lemma {:vcs_split_on_every_assert} LemmaToNatLeftEqToNatRight(xs: seq<digit>)
+ lemma {:isolate_assertions} LemmaToNatLeftEqToNatRight(xs: seq<digit>)
  ensures ToNatRight(xs) == ToNatLeft(xs)
  {
  reveal ToNatRight();
@@ -177,7 +177,7 @@ abstract module {:disableNonlinearArithmetic} Std.Arithmetic.LittleEndianNat {
 
  /* The nat representation of a sequence can be calculated using the nat
  representation of its prefix. */
- lemma {:vcs_split_on_every_assert} LemmaSeqPrefix(xs: seq<digit>, i: nat)
+ lemma {:isolate_assertions} LemmaSeqPrefix(xs: seq<digit>, i: nat)
  requires 0 <= i <= |xs|
  ensures ToNatRight(xs[..i]) + ToNatRight(xs[i..]) * Pow(BASE(), i) == ToNatRight(xs)
  {
@@ -228,7 +228,7 @@ abstract module {:disableNonlinearArithmetic} Std.Arithmetic.LittleEndianNat {
 
  /* Two sequences do not have the same nat representations if their prefixes
  do not have the same nat representations. Helper lemma for LemmaSeqNeq. */
- lemma {:vcs_split_on_every_assert} LemmaSeqPrefixNeq(xs: seq<digit>, ys: seq<digit>, i: nat)
+ lemma {:isolate_assertions} LemmaSeqPrefixNeq(xs: seq<digit>, ys: seq<digit>, i: nat)
  requires 0 <= i <= |xs| == |ys|
  requires ToNatRight(xs[..i]) != ToNatRight(ys[..i])
  ensures ToNatRight(xs) != ToNatRight(ys)
@@ -524,7 +524,7 @@ abstract module {:disableNonlinearArithmetic} Std.Arithmetic.LittleEndianNat {
 
  /* SeqAdd returns the same value as converting the sequences to nats, then
  adding them. */
- lemma {:vcs_split_on_every_assert} LemmaSeqAdd(xs: seq<digit>, ys: seq<digit>, zs: seq<digit>, cout: nat)
+ lemma {:isolate_assertions} LemmaSeqAdd(xs: seq<digit>, ys: seq<digit>, zs: seq<digit>, cout: nat)
  requires |xs| == |ys|
  requires SeqAdd(xs, ys) == (zs, cout)
  ensures ToNatRight(xs) + ToNatRight(ys) == ToNatRight(zs) + cout * Pow(BASE(), |xs|)
@@ -581,7 +581,7 @@ abstract module {:disableNonlinearArithmetic} Std.Arithmetic.LittleEndianNat {
 
  /* SeqSub returns the same value as converting the sequences to nats, then
  subtracting them. */
- lemma {:vcs_split_on_every_assert} LemmaSeqSub(xs: seq<digit>, ys: seq<digit>, zs: seq<digit>, cout: nat)
+ lemma {:isolate_assertions} LemmaSeqSub(xs: seq<digit>, ys: seq<digit>, zs: seq<digit>, cout: nat)
  requires |xs| == |ys|
  requires SeqSub(xs, ys) == (zs, cout)
  ensures ToNatRight(xs) - ToNatRight(ys) + cout * Pow(BASE(), |xs|) == ToNatRight(zs)

Source/DafnyStandardLibraries/src/Std/Base64.dfy

@@ -98,7 +98,7 @@ module Std.Base64 {
  else (c - 65 as char) as index
  }
 
- lemma {:resource_limit 2000000} {:vcs_split_on_every_assert} CharToIndexToChar(c: char)
+ lemma {:resource_limit 2000000} {:isolate_assertions} CharToIndexToChar(c: char)
  requires IsBase64Char(c)
  ensures IndexToChar(CharToIndex(c)) == c
  {
@@ -122,7 +122,7 @@ module Std.Base64 {
  }
  }
 
- lemma {:vcs_split_on_every_assert} IndexToCharToIndex(i: index)
+ lemma {:isolate_assertions} IndexToCharToIndex(i: index)
  ensures (IndexToCharIsBase64(i); CharToIndex(IndexToChar(i)) == i)
  {
  // TODO: reduce resource use, brittleness
@@ -263,7 +263,7 @@ module Std.Base64 {
  IndexSeqToBV24ToIndexSeq(s);
  }
 
- opaque function {:vcs_split_on_every_assert} DecodeRecursively(s: seq<index>): (b: seq<bv8>)
+ opaque function {:isolate_assertions} DecodeRecursively(s: seq<index>): (b: seq<bv8>)
  requires |s| % 4 == 0
  decreases |s|
  {
@@ -326,7 +326,7 @@ module Std.Base64 {
  }
  }
 
- opaque function {:vcs_split_on_every_assert} EncodeRecursively(b: seq<bv8>): (s: seq<index>)
+ opaque function {:isolate_assertions} EncodeRecursively(b: seq<bv8>): (s: seq<index>)
  requires |b| % 3 == 0
  {
  if |b| == 0 then []
@@ -677,7 +677,7 @@ module Std.Base64 {
  }
  }
 
- lemma {:vcs_split_on_every_assert} DecodeEncode1Padding(s: seq<char>)
+ lemma {:isolate_assertions} DecodeEncode1Padding(s: seq<char>)
  requires Is1Padding(s)
  ensures Encode1Padding(Decode1Padding(s)) == s
  {
@@ -1449,7 +1449,7 @@ module Std.Base64 {
  seq(|b|, i requires 0 <= i < |b| => b[i] as uint8)
  }
 
- lemma {:vcs_split_on_every_assert} {:resource_limit 1000000000} UInt8sToBVsToUInt8s(u: seq<uint8>)
+ lemma {:isolate_assertions} {:resource_limit 1000000000} UInt8sToBVsToUInt8s(u: seq<uint8>)
  ensures BVsToUInt8s(UInt8sToBVs(u)) == u
  {
  // TODO: reduce resource use

Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy

@@ -530,7 +530,7 @@ module Std.Collections.Seq {
  /* Flattening sequences of sequences is distributive over concatenation. That is, concatenating
  the flattening of two sequences of sequences is the same as flattening the
  concatenation of two sequences of sequences. */
- lemma {:vcs_split_on_every_assert} LemmaFlattenConcat<T>(xs: seq<seq<T>>, ys: seq<seq<T>>)
+ lemma {:isolate_assertions} LemmaFlattenConcat<T>(xs: seq<seq<T>>, ys: seq<seq<T>>)
  ensures Flatten(xs + ys) == Flatten(xs) + Flatten(ys)
  {
  if |xs| == 0 {
@@ -781,7 +781,7 @@ module Std.Collections.Seq {
  /* Filtering a sequence is distributive over concatenation. That is, concatenating two sequences
  and then using "Filter" is the same as using "Filter" on each sequence separately, and then
  concatenating the two resulting sequences. */
- lemma {:vcs_split_on_every_assert}
+ lemma {:isolate_assertions}
  LemmaFilterDistributesOverConcat<T(!new)>(f: (T ~> bool), xs: seq<T>, ys: seq<T>)
  requires forall i {:trigger xs[i]}:: 0 <= i < |xs| ==> f.requires(xs[i])
  requires forall j {:trigger ys[j]}:: 0 <= j < |ys| ==> f.requires(ys[j])

Source/DafnyStandardLibraries/src/Std/JSON/Deserializer.dfy

@@ -69,7 +69,7 @@ module Std.JSON.Deserializer {
  hd as uint16
  }
 
- function {:tailrecursion} {:vcs_split_on_every_assert} Unescape(str: seq<uint16>, start: nat := 0, prefix: seq<uint16> := []): DeserializationResult<seq<uint16>>
+ function {:tailrecursion} {:isolate_assertions} Unescape(str: seq<uint16>, start: nat := 0, prefix: seq<uint16> := []): DeserializationResult<seq<uint16>>
  decreases |str| - start
  { // Assumes UTF-16 strings
  if start >= |str| then Success(prefix)

Source/DafnyStandardLibraries/src/Std/JSON/Serializer.dfy

@@ -64,7 +64,7 @@ module Std.JSON.Serializer {
  Failure(o.error)
  }
 
- function {:vcs_split_on_every_assert} {:resource_limit 1000000} Number(dec: Values.Decimal): Result<jnumber> {
+ function {:isolate_assertions} {:resource_limit 1000000} Number(dec: Values.Decimal): Result<jnumber> {
  var minus: jminus := Sign(dec.n);
  var num: jnum :- Int(Math.Abs(dec.n));
  var frac: Maybe<jfrac> := Empty();