Isolate assertions attribute

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1927,6 +1927,8 @@ public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap)
  return false;
  }
 
+ private static readonly Dictionary<string, string> NullaryAttributesToTranslate;
+
  private static readonly HashSet<string> NullaryAttributesToCopy = new(new[] {
  "focus",
  "ignore",
@@ -1958,6 +1960,15 @@ public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap)
  "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 ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap)
  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 @@ import Producer
  [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 @@ import Producer
  [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 @@ ensures Q(x)
  // 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();