Merge branch 'master' into assignSuchThatByBlock

.github/workflows/doc-tests.yml

@@ -32,12 +32,6 @@ jobs:
       uses: actions/setup-dotnet@v4
       with:
         dotnet-version: 8.0.x
-    # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason
-    # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460
-    - name: Setup dotnet
-      uses: actions/setup-dotnet@v4
-      with:
-        dotnet-version: 6.0.x
     - name: Checkout Dafny
       uses: actions/checkout@v4
       with:

.github/workflows/integration-tests-reusable.yml

@@ -19,7 +19,7 @@ on:
         default: ""
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
   # This job is used to dynamically calculate the matrix dimensions.

.github/workflows/msbuild.yml

@@ -12,7 +12,7 @@ concurrency:
 
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
   check-deep-tests:

.github/workflows/publish-release-reusable.yml

@@ -30,7 +30,7 @@ on:
         required: false
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
 

.github/workflows/publish-release.yml

@@ -7,7 +7,7 @@ on:
       - 'v*'
 
 env:
-  dotnet-version: 6.0.x # SDK Version for building Dafny
+  dotnet-version: 8.0.x # SDK Version for building Dafny
 
 jobs:
   deep-integration-tests:

.github/workflows/refman.yml

@@ -28,7 +28,7 @@ jobs:
     - name: Setup dotnet
       uses: actions/setup-dotnet@v4
       with:
-        dotnet-version: 6.0.x
+        dotnet-version: 8.0.x
     - name: Checkout Dafny
       uses: actions/checkout@v4
       with:

.github/workflows/release-downloads-nuget.yml

@@ -17,7 +17,7 @@ on:
   workflow_dispatch:
 
 env:
-  dotnet-version: 6.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
+  dotnet-version: 8.0.x # SDK Version for running Dafny (TODO: should this be an older version?)
   z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
 
 concurrency:

.github/workflows/runtime-tests.yml

@@ -31,12 +31,6 @@ jobs:
         uses: actions/setup-dotnet@v4
         with:
           dotnet-version: 8.0.x
-      # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason
-      # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460
-      - name: Setup dotnet
-        uses: actions/setup-dotnet@v4
-        with:
-          dotnet-version: 6.0.x
       - name: Set up JDK 18
         uses: actions/setup-java@v4
         with:

.github/workflows/xunit-tests-reusable.yml

@@ -73,7 +73,7 @@ jobs:
     - name: Setup .NET
       uses: actions/setup-dotnet@v4
       with:
-        dotnet-version: 6.0.x
+        dotnet-version: 8.0.x
     - name: Install dependencies
       run: |
         dotnet restore ${{env.solutionPath}}

CONTRIBUTING.md

@@ -85,7 +85,7 @@ Subsequent CI runs should pick up the successful `deep-tests` run and make the `
 ### How can I write portions of Dafny in Dafny itself?
 
 Since https://github.com/dafny-lang/dafny/pull/2399, it is possible to add \*.dfy files next to other source files.
-The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net6.0/GeneratedFromDafny.cs`
+The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net8.0/GeneratedFromDafny.cs`
 that is automatically included in the build process. This file contains also the Dafny run-time in C#.
 One example of such file is `Source/DafnyCore/AST/Formatting.dfy`, and you can use it as a starting point.
 

Scripts/use-local-boogie.sh

@@ -2,5 +2,5 @@ BOOGIE_PATH="boogie/"
 allDlls=("Boogie.AbstractInterpretation.dll" "Boogie.BaseTypes.dll" "Boogie.CodeContractsExtender.dll" "Boogie.Concurrency.dll" "Boogie.Core.dll" "Boogie.ExecutionEngine.dll" "Boogie.Graph.dll" "Boogie.Houdini.dll" "Boogie.Model.dll" "Boogie.Predication.dll" "Boogie.Provers.SMTLib.dll" "Boogie.VCExpr.dll" "Boogie.VCGeneration.dll" "BoogieDriver.dll" "System.Configuration.ConfigurationManager.dll" "System.Runtime.Caching.dll" "System.Security.Cryptography.ProtectedData.dll" "System.Security.Permissions.dll")
 for t in "${allDlls[@]}"
 do
-	cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net6.0/${t}" Binaries/
+	cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net8.0/${t}" Binaries/
 done

Source/AutoExtern.Test/AutoExtern.Test.csproj

@@ -2,7 +2,6 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
     <IsPackable>false</IsPackable>

Source/AutoExtern.Test/Minimal/Library.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
   <PropertyGroup>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
   </PropertyGroup>

Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj

@@ -2,9 +2,9 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
-    <NoWarn>CS3021; CS0162</NoWarn>
+    <NoWarn>CS8981; CS3021; CS0162</NoWarn>
     <!-- <Nullable>enable</Nullable> -->
   </PropertyGroup>
 

Source/AutoExtern.Test/Tutorial/Library/Library.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
   <PropertyGroup>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
   </PropertyGroup>

Source/AutoExtern/AutoExtern.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>

Source/Dafny/Dafny.csproj

@@ -5,7 +5,6 @@
       <AssemblyName>Dafny</AssemblyName>
       <GenerateAssemblyInfo>true</GenerateAssemblyInfo>
       <DefineConstants>TRACE</DefineConstants>
-      <TargetFramework>net6.0</TargetFramework>
       <RollForward>Major</RollForward>
       <OutputPath>..\..\Binaries\</OutputPath>
       <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
@@ -16,7 +15,7 @@
       <PackageReadmeFile>README.md</PackageReadmeFile>
   </PropertyGroup>
 
-  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net6.0|AnyCPU'">
+  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net8.0|AnyCPU'">
     <AppendTargetFrameworkToOutputPath>false</AppendTargetFrameworkToOutputPath>
     <AppendRuntimeIdentifierToOutputPath>false</AppendRuntimeIdentifierToOutputPath>
   </PropertyGroup>

Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj

@@ -1,7 +1,6 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
     <PropertyGroup>
-        <TargetFramework>net6.0</TargetFramework>
         <RollForward>Major</RollForward>
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>enable</Nullable>

Source/DafnyCore.Test/DafnyCore.Test.csproj

@@ -1,7 +1,6 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
     <PropertyGroup>
-        <TargetFramework>net6.0</TargetFramework>
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>enable</Nullable>
 

Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -62,7 +62,7 @@ public byte[] MyHash {
             Concat(TotalArrowTypeDecls.Keys.OrderBy(x => x)).
             Concat(tupleInts.OrderBy(x => x));
         var bytes = ints.SelectMany(BitConverter.GetBytes).ToArray();
-        hash = HashAlgorithm.Create("SHA256")!.ComputeHash(bytes);
+        hash = SHA256.Create()!.ComputeHash(bytes);
       }
 
       return hash;

Source/DafnyCore/Backends/CSharp/CsharpBackend.cs

@@ -92,7 +92,7 @@ public override string GetCompileName(bool isDefaultModule, string moduleName, s
 
   <PropertyGroup>
     <OutputType>{outputType}</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
     <NoWarn>CS8600;CS8603;CS8604;CS8605;CS8625;CS8629;CS8714;CS8765;CS8769;CS8981</NoWarn>

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -67,7 +67,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
       wr.WriteLine("// To recompile, you will need the libraries");
       wr.WriteLine("//     System.Runtime.Numerics.dll System.Collections.Immutable.dll");
-      wr.WriteLine("// but the 'dotnet' tool in net6.0 should pick those up automatically.");
+      wr.WriteLine("// but the 'dotnet' tool in .NET should pick those up automatically.");
       wr.WriteLine("// Optionally, you may want to include compiler switches like");
       wr.WriteLine("//     /debug /nowarn:162,164,168,183,219,436,1717,1718");
       wr.WriteLine();

Source/DafnyCore/DafnyCore.csproj

@@ -17,11 +17,12 @@
     <GenerateAssemblyInfo>true</GenerateAssemblyInfo>
     <OutputPath>..\..\Binaries\</OutputPath>
     <DefineConstants>TRACE</DefineConstants>
-    <TargetFramework>net6.0</TargetFramework>
     <RollForward>Major</RollForward>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
 
-    <NoWarn>$(NoWarn);NU5104</NoWarn> <!-- Required because System.CommandLine is in beta. -->
+    <NoWarn>$(NoWarn);NU5104;CS8981</NoWarn>
+    <!-- NU5104 required because System.CommandLine is in beta. -->
+    <!-- CS8981 required because Dafny code can use lowercase type names -->
     <IsPackable>true</IsPackable>
   </PropertyGroup>
 
@@ -35,7 +36,7 @@
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
       <PackageReference Include="Boogie.ExecutionEngine" Version="3.4.3" />
-      <PackageReference Include="Tomlyn" Version="0.16.2" />
+      <PackageReference Include="Tomlyn" Version="0.17.0" />
   </ItemGroup>
 
   <ItemGroup>

Source/DafnyCore/DafnyGeneratedFromDafny.sh

@@ -4,7 +4,7 @@
 # 1. Delete the file GeneratedFromDafny.cs
 # 2. Add a dependency to 
 #      <PackageReference Include="dafny.msbuild" Version="1.0.0" />
-# That's it! The same file will now be automatically generated as obj/Debug/net6.0/GeneratedFromDafny.cs
+# That's it! The same file will now be automatically generated as obj/Debug/net8.0/GeneratedFromDafny.cs
 # 3. Remove the following dependencies that are being taken care by dafny-msbuild
 #       <PackageReference Include="Microsoft.Build.Framework" Version="16.5.0" PrivateAssets="All" />
 #       <PackageReference Include="Microsoft.Build.Utilities.Core" Version="16.5.0" PrivateAssets="All" />

Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/DAST.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/Defs.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/Formatting.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/RAST.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718
 

Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs

@@ -1,7 +1,7 @@
 // Dafny program the_program compiled into C#
 // To recompile, you will need the libraries
 //     System.Runtime.Numerics.dll System.Collections.Immutable.dll
-// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// but the 'dotnet' tool in .NET should pick those up automatically.
 // Optionally, you may want to include compiler switches like
 //     /debug /nowarn:162,164,168,183,219,436,1717,1718