fix: Nightly build (#779)

Rust can build with the latest nightly now (and the CI isn't building from source any more so it can't specify a commit any more)

Doesn't fully fix the nightly build but will once dafny-lang/dafny#6090 is addressed.

Author: robin-aws

.github/actions/build_dafny_from_source/action.yml

@@ -1,3 +1,4 @@
+# TODO: Replace this with the setup-dafny-action version when it is working.
 name: "Build Dafny from source"
 description: "Builds the given branch of Dafny from source"
 inputs:

.github/workflows/nightly_dafny.yml

@@ -31,10 +31,7 @@ jobs:
     if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
-      # Rust currently depends on building Dafny from source,
-      # so we can't rely on setup-dafny-action's support for "nightly-latest"
-      # (until https://github.com/dafny-lang/setup-dafny-action/issues/24 is done at least)
-      dafny: "master"
+      dafny: "nightly-latest"
   dafny-nightly-python:
     if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
     uses: ./.github/workflows/test_models_python_tests.yml

.github/workflows/pull.yml

@@ -51,7 +51,7 @@ jobs:
       fail-fast: false
       matrix:
         # Rust code generation is under development and depends on pending changes to the
-        # Dafny Rust code generation, so we test on a specific unreleased commit instead.
+        # Dafny Rust code generation, so we test on a specific prerelease instead.
         dafny-version:
           - nightly-2025-01-30-7db1e5f
     uses: ./.github/workflows/test_models_rust_tests.yml

SmithyDafnyMakefile.mk

@@ -378,6 +378,8 @@ _polymorph_dafny: INPUT_DAFNY=\
 		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_dafny: _polymorph
 
+dafny: polymorph_dafny verify
+
 # Generates dotnet code for all namespaces in this project
 .PHONY: polymorph_dotnet
 polymorph_dotnet: POLYMORPH_LANGUAGE_TARGET=dotnet

TestModels/Constraints/test/Helpers.dfy

@@ -9,7 +9,7 @@ module Helpers {
   import opened Wrappers
 
   // UTF-8 encoded "aws-kms"
-  const PROVIDER_ID: UTF8.ValidUTF8Bytes :=
+  const {:vcs_split_on_every_assert} PROVIDER_ID: UTF8.ValidUTF8Bytes :=
     var s := [0x61, 0x77, 0x73, 0x2D, 0x6B, 0x6D, 0x73];
     assert UTF8.ValidUTF8Range(s, 0, 7);
     s

TestModels/Dependencies/test/SimpleDependenciesImplTest.dfy

@@ -13,6 +13,7 @@ module SimpleDependenciesImplTest {
     import SimpleResourcesTypes
     import opened Wrappers
 
+
     method{:test} TestDependenciesWithDefaultConfig()
     {        
         var client :- expect SimpleDependencies.SimpleDependencies();