Prune assumptions

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "Test/libraries"]
 	path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
 	url = https://github.com/dafny-lang/libraries.git
+[submodule "boogie"]
+	path = boogie
+	url = [email protected]:keyboardDrummer/boogie.git

Source/Dafny.sln

@@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -138,5 +164,17 @@ Global
 		SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
+		{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
 	EndGlobalSection
 EndGlobal

Source/DafnyCore/DafnyCore.csproj

@@ -34,7 +34,17 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.1.6" />
+      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Graph\Graph.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Model\Model.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCExpr\VCExpr.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCGeneration\VCGeneration.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Provers\SMTLib\SMTLib.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Houdini\Houdini.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency.csproj" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/Options/DafnyCommands.cs

@@ -71,6 +71,8 @@ static DafnyCommands() {
     Snippets.ShowSnippets,
     DeveloperOptionBag.PrintOption,
     DeveloperOptionBag.ResolvedPrint,
+    DeveloperOptionBag.SplitPrint,
+    DeveloperOptionBag.PassivePrint,
     DeveloperOptionBag.BoogiePrint,
     Printer.PrintMode,
     CommonOptionBag.AllowWarnings,

Source/DafnyCore/Options/DeveloperOptionBag.cs

@@ -6,6 +6,22 @@ namespace Microsoft.Dafny;
 
 public class DeveloperOptionBag {
 
+  public static readonly Option<string> SplitPrint = new("--sprint",
+    @"
+Print Boogie splits translated from Dafny
+(use - as <file> to print to console)".TrimStart()) {
+    IsHidden = true,
+    ArgumentHelpName = "file",
+  };
+
+  public static readonly Option<string> PassivePrint = new("--pprint",
+    @"
+Print passified Boogie program translated from Dafny
+(use - as <file> to print to console)".TrimStart()) {
+    IsHidden = true,
+    ArgumentHelpName = "file",
+  };
+
   public static readonly Option<string> BoogiePrint = new("--bprint",
   @"
 Print Boogie program translated from Dafny
@@ -48,13 +64,27 @@ static DeveloperOptionBag() {
         options.FileTimestamp);
     });
 
+    DafnyOptions.RegisterLegacyBinding(PassivePrint, (options, f) => {
+      options.PrintPassiveFile = f;
+      options.ExpandFilename(options.PrintPassiveFile, x => options.PrintPassiveFile = x, options.LogPrefix,
+        options.FileTimestamp);
+    });
+
     DafnyOptions.RegisterLegacyBinding(BoogiePrint, (options, f) => {
       options.PrintFile = f;
       options.ExpandFilename(options.PrintFile, x => options.PrintFile = x, options.LogPrefix,
         options.FileTimestamp);
     });
+
+    DafnyOptions.RegisterLegacyBinding(SplitPrint, (options, f) => {
+      options.PrintSplitFile = f;
+      options.ExpandFilename(options.PrintSplitFile, x => options.PrintSplitFile = x, options.LogPrefix,
+        options.FileTimestamp);
+    });
 
+    DooFile.RegisterNoChecksNeeded(PassivePrint, false);
     DooFile.RegisterNoChecksNeeded(BoogiePrint, false);
+    DooFile.RegisterNoChecksNeeded(SplitPrint, false);
     DooFile.RegisterNoChecksNeeded(PrintOption, false);
     DooFile.RegisterNoChecksNeeded(ResolvedPrint, false);
     DooFile.RegisterNoChecksNeeded(Bootstrapping, false);

Source/DafnyDriver/Commands/MeasureComplexityCommand.cs

@@ -3,33 +3,42 @@
 using System.CommandLine;
 using System.Linq;
 using System.Reactive.Subjects;
+using System.Threading;
 using System.Threading.Tasks;
 using DafnyCore;
 using DafnyDriver.Commands;
+using Microsoft.Boogie;
+using VC;
 
 namespace Microsoft.Dafny;
 
 static class MeasureComplexityCommand {
   public static IEnumerable<Option> Options => new Option[] {
     Iterations,
     RandomSeed,
+    TopX,
     VerifyCommand.FilterSymbol,
     VerifyCommand.FilterPosition,
   }.Concat(DafnyCommands.VerificationOptions).
-    Concat(DafnyCommands.ResolverOptions);
+    Concat(DafnyCommands.ResolverOptions).
+    Concat(DafnyCommands.ConsoleOutputOptions);
 
   static MeasureComplexityCommand() {
     DafnyOptions.RegisterLegacyBinding(Iterations, (o, v) => o.RandomizeVcIterations = (int)v);
     DafnyOptions.RegisterLegacyBinding(RandomSeed, (o, v) => o.RandomSeed = (int)v);
 
     DooFile.RegisterNoChecksNeeded(Iterations, false);
     DooFile.RegisterNoChecksNeeded(RandomSeed, false);
+    DooFile.RegisterNoChecksNeeded(TopX, false);
   }
 
+  private static readonly Option<uint> TopX = new("--worst-amount", () => 10U,
+    $"Configures the amount of worst performing verification tasks that are reported.");
+
   private static readonly Option<uint> RandomSeed = new("--random-seed", () => 0U,
     $"Turn on randomization of the input that Dafny passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Dafny proofs are complex in the sense that changes to the proof that preserve its meaning may cause its verification result to change. This option simulates meaning-preserving changes to the proofs without requiring the user to actually make those changes. The proof changes are renaming variables and reordering declarations in the SMT input passed to the solver, and setting solver options that have similar effects.");
 
-  private static readonly Option<uint> Iterations = new("--iterations", () => 10U,
+  private static readonly Option<uint> Iterations = new("--iterations", () => 1U,
     $"Attempt to verify each proof n times with n random seeds, each seed derived from the previous one. {RandomSeed.Name} can be used to specify the first seed, which will otherwise be 0.") {
     ArgumentHelpName = "n"
   };
@@ -62,7 +71,7 @@ private static async Task<int> Execute(DafnyOptions options) {
       // For error diagnostics, we should group duplicates and say how often they occur.
       // Performance data of individual verification tasks (VCs) should be grouped by VcNum (the assertion batch).
       VerifyCommand.ReportVerificationDiagnostics(compilation, verificationResults);
-      var summaryReported = VerifyCommand.ReportVerificationSummary(compilation, verificationResults);
+      var summaryReported = ReportResourceSummary(compilation, verificationResults);
       var proofDependenciesReported = VerifyCommand.ReportProofDependencies(compilation, resolution, verificationResults);
       var verificationResultsLogged = VerifyCommand.LogVerificationResults(compilation, resolution, verificationResults);
 
@@ -75,13 +84,47 @@ private static async Task<int> Execute(DafnyOptions options) {
     return await compilation.GetAndReportExitCode();
   }
 
+  public static async Task ReportResourceSummary(
+    CliCompilation cliCompilation,
+    IObservable<CanVerifyResult> verificationResults) {
+
+    PriorityQueue<VerificationTaskResult, int> worstPerformers = new();
+
+    var totalResources = 0;
+    var worstAmount = cliCompilation.Options.Get(TopX);
+    verificationResults.Subscribe(result => {
+      foreach (var taskResult in result.Results) {
+        var runResult = taskResult.Result;
+        totalResources += runResult.ResourceCount;
+        worstPerformers.Enqueue(taskResult, runResult.ResourceCount);
+        if (worstPerformers.Count > worstAmount) {
+          worstPerformers.Dequeue();
+        }
+      }
+    });
+    await verificationResults.WaitForComplete();
+    var output = cliCompilation.Options.OutputWriter;
+    var decreasingWorst = new Stack<VerificationTaskResult>();
+    while (worstPerformers.Count > 0) {
+      decreasingWorst.Push(worstPerformers.Dequeue());
+    }
+
+    await output.WriteLineAsync($"The total consumed resources are {totalResources}");
+    await output.WriteLineAsync($"The most demanding {worstAmount} verification tasks consumed these resources:");
+    foreach (var performer in decreasingWorst) {
+      var location = ((IToken)performer.Task.Token).TokenToString(cliCompilation.Options);
+      await output.WriteLineAsync($"{location}: {performer.Result.ResourceCount}");
+    }
+  }
+
   private static async Task RunVerificationIterations(DafnyOptions options, CliCompilation compilation,
     IObserver<CanVerifyResult> verificationResultsObserver) {
     int iterationSeed = (int)options.Get(RandomSeed);
     var random = new Random(iterationSeed);
-    foreach (var iteration in Enumerable.Range(0, (int)options.Get(Iterations))) {
+    var iterations = (int)options.Get(Iterations);
+    foreach (var iteration in Enumerable.Range(0, iterations)) {
       await options.OutputWriter.WriteLineAsync(
-        $"Starting verification of iteration {iteration} with seed {iterationSeed}");
+        $"Starting verification of iteration {iteration + 1}/{iterations} with seed {iterationSeed}");
       try {
         await foreach (var result in compilation.VerifyAllLazily(iterationSeed)) {
           verificationResultsObserver.OnNext(result);

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -138,8 +138,8 @@ await AssertVerificationHoverMatches(documentItem, (0, 36),
 
 - Total resource usage: ??? RU  
 - Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches):  
-  - #???/??? with 1 assertion  at line ???, ??? RU  
-  - #???/??? with 1 assertion  at line ???, ??? RU  "
+  - #???/??? with 1 assertion at line ???, ??? RU  
+  - #???/??? with 1 assertion at line ???, ??? RU"
       );
     }
 

Source/DafnyLanguageServer/LanguageServer.cs

@@ -28,6 +28,8 @@ public class LanguageServer {
         DafnyLangSymbolResolver.UseCaching,
         ProjectManager.UpdateThrottling,
         CachingProjectFileOpener.ProjectFileCacheExpiry,
+        DeveloperOptionBag.SplitPrint,
+        DeveloperOptionBag.PassivePrint,
         DeveloperOptionBag.BoogiePrint,
         CommonOptionBag.EnforceDeterminism,
         InternalDocstringRewritersPluginConfiguration.UseJavadocLikeDocstringRewriterOption,

Source/IntegrationTests/TestFiles/LitTests/LitTest/VSI-Benchmarks/b4.dfy.expect

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

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy

@@ -0,0 +1,20 @@
+// RUN: %exits-with 4 %baredafny measure-complexity --show-snippets false --use-basename-for-filename --isolate-assertions --worst-amount 100 "%s" > %t.raw
+// RUN: %sed 's#\): \d+#): <redacted>#g' %t.raw > %t.raw2
+// RUN: %sed 's#are \d+#are <redacted>#g' %t.raw2 > %t
+// RUN: %diff "%s.expect" "%t"
+method Foo() {
+  assert Ack(0,0) == 10;
+  assert Ack(1,3) == 10;
+  assert Ack(3,3) == 10;
+  assert Ack(3,4) == 10;
+}
+
+function Ack(m: nat, n: nat): nat
+{
+  if m == 0 then
+    n + 1
+  else if n == 0 then
+    Ack(m - 1, 1)
+  else
+    Ack(m - 1, Ack(m, n - 1))
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect

@@ -0,0 +1,30 @@
+Starting verification of iteration 1/1 with seed 0
+measure-complexity.dfy(6,18): Error: assertion might not hold
+The total consumed resources are <redacted>
+The most demanding 100 verification tasks consumed these resources:
+measure-complexity.dfy(19,4): <redacted>
+measure-complexity.dfy(9,18): <redacted>
+measure-complexity.dfy(19,4): <redacted>
+measure-complexity.dfy(19,4): <redacted>
+measure-complexity.dfy(8,18): <redacted>
+measure-complexity.dfy(7,18): <redacted>
+measure-complexity.dfy(19,10): <redacted>
+measure-complexity.dfy(6,18): <redacted>
+measure-complexity.dfy(19,15): <redacted>
+measure-complexity.dfy(17,4): <redacted>
+measure-complexity.dfy(17,4): <redacted>
+measure-complexity.dfy(17,4): <redacted>
+measure-complexity.dfy(19,15): <redacted>
+measure-complexity.dfy(19,15): <redacted>
+measure-complexity.dfy(19,24): <redacted>
+measure-complexity.dfy(17,10): <redacted>
+measure-complexity.dfy(15,6): <redacted>
+measure-complexity.dfy(8,15): <redacted>
+measure-complexity.dfy(9,15): <redacted>
+measure-complexity.dfy(9,13): <redacted>
+measure-complexity.dfy(7,13): <redacted>
+measure-complexity.dfy(17,15): <redacted>
+measure-complexity.dfy(8,13): <redacted>
+measure-complexity.dfy(7,15): <redacted>
+measure-complexity.dfy(6,15): <redacted>
+measure-complexity.dfy(6,13): <redacted>

Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/09-CounterNoStateMachine.dfy.expect

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

Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/10-SequenceInvariant.dfy.expect

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

Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/12-MutexLifetime-short.dfy.expect

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

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect

@@ -22,4 +22,4 @@ Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreas
 Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 
-Dafny program verifier finished with 112 verified, 23 errors
+Dafny program verifier finished with 108 verified, 23 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect

@@ -23,4 +23,4 @@ Termination.dfy(923,2): Error: cannot prove termination; try supplying a decreas
 Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 
-Dafny program verifier finished with 111 verified, 24 errors
+Dafny program verifier finished with 107 verified, 24 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/MoreInduction.dfy.expect

@@ -7,4 +7,4 @@ MoreInduction.dfy(87,10): Related location: this is the postcondition that could
 MoreInduction.dfy(93,0): Error: a postcondition could not be proved on this return path
 MoreInduction.dfy(92,21): Related location: this is the postcondition that could not be proved
 
-Dafny program verifier finished with 28 verified, 4 errors
+Dafny program verifier finished with 26 verified, 4 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy

@@ -214,11 +214,18 @@ ghost function IntRange(lo: nat, len: nat): set<nat>
   S
 }
 
+lemma BoundedSetSize(xs: set<nat>, lower: nat, upper: nat)
+  requires forall x <- xs :: lower <= x && x < upper
+  ensures |xs| <= upper - lower
+
 // ----- Proofs of alternative versions
 
 lemma {:isolate_assertions} SMN'_Correct(xs: List<nat>, n: nat, len: nat)
   requires NoDuplicates(xs)
+// a
   requires forall x :: x in Elements(xs) ==> n <= x
+// b
+// c
   requires len == Length(xs)
   ensures var s := SMN'(xs, n, len);
     n <= s <= n + len &&
@@ -239,6 +246,16 @@ lemma {:isolate_assertions} SMN'_Correct(xs: List<nat>, n: nat, len: nat)
       SMN'_Correct(L, n, llen);
     } else {
       var s := SMN'(R, n + llen, len - llen);
+      // at worst the elements in L are consecutive, and then the lower bound of R is n + llen
+      // elements in R are bigger than those in L
+      // the biggest element in L is n + half
+      // assert llen >= half;
+
+      assert llen == half by {
+        BoundedSetSize(Elements(L), n, n + half);
+        assert |Elements(L)| <= (n + half) - n;
+        assert |Elements(L)| <= half;    
+      }
       SMN'_Correct(R, n + llen, len - llen);
       forall x | n <= x < s
         ensures x in Elements(xs)
@@ -274,6 +291,12 @@ lemma {:isolate_assertions} SMN''_Correct(xs: List<nat>, n: nat, len: nat)
       SMN''_Correct(L, n, llen);
     } else {
       var s := SMN''(R, n + llen, len - llen);
+
+      assert llen == half by {
+        BoundedSetSize(Elements(L), n, n + half);
+        assert |Elements(L)| <= (n + half) - n;
+        assert |Elements(L)| <= half;    
+      }
       SMN''_Correct(R, n + llen, len - llen);
       forall x | n <= x < s
         ensures x in Elements(xs)