fix: Nightly build

.github/workflows/test_models_rust_tests.yml

@@ -59,7 +59,7 @@ jobs:
       - name: Set up Rust
         uses: actions-rust-lang/setup-rust-toolchain@v1
         with:
-          toolchain: "1.81.0"
+          toolchain: "1.82.0"
           rustflags: ""
           components: rustfmt
 

SmithyDafnyMakefile.mk

@@ -80,6 +80,8 @@ ENABLE_EXTERN_PROCESSING?=
 #    ensures DAFNY_PROCESSES(cpus) * Z3_PROCESSES(cpus) <= cpus
 #  {}
 
+ENFORCE_DETERMINISM_OPTION := $(shell cd $(CODEGEN_CLI_ROOT); \
+	./../gradlew run -q --args="if-dafny-at-least --dafny-version 4.8 --text --enforce-determinism")
 
 # Verify the entire project
 verify:Z3_PROCESSES=$(shell echo $$(( $(CORES) >= 3 ? 2 : 1 )))
@@ -90,6 +92,7 @@ verify:DAFNY_OPTIONS=--allow-warnings
 verify:
 	find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny verify \
 		--cores $(Z3_PROCESSES) \
+		$(ENFORCE_DETERMINISM_OPTION) \
 		--unicode-char false \
 		--function-syntax 3 \
 		--log-format csv \
@@ -106,6 +109,7 @@ verify_single:DAFNY_OPTIONS=--allow-warnings
 verify_single:
 	dafny verify \
 		--cores $(CORES) \
+		$(ENFORCE_DETERMINISM_OPTION) \
 		--unicode-char false \
 		--function-syntax 3 \
 		--log-format text \
@@ -122,6 +126,7 @@ verify_service:
 	@: $(if ${SERVICE},,$(error You must pass the SERVICE to generate for));
 	dafny verify \
 		--cores $(CORES) \
+		$(ENFORCE_DETERMINISM_OPTION) \
 		--unicode-char false \
 		--function-syntax 3 \
 		--log-format text \
@@ -201,6 +206,7 @@ transpile_implementation:
 		--stdin \
 		--no-verify \
 		--cores:$(CORES) \
+		$(ENFORCE_DETERMINISM_OPTION) \
 		--optimize-erasable-datatype-wrapper:false \
 		--unicode-char:false \
 		--function-syntax:3 \
@@ -241,6 +247,7 @@ transpile_test:
 		--stdin \
 		--no-verify \
 		--cores:$(CORES) \
+		$(ENFORCE_DETERMINISM_OPTION) \
 		--optimize-erasable-datatype-wrapper:false \
 		--unicode-char:false \
 		--function-syntax:3 \

TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml

@@ -18,7 +18,7 @@ includes = [
 # Options that help support more values of consuming context options
 # (mostly turning on any more restrictive verification)
 track-print-effects = true
-enforce-determinism = false
+enforce-determinism = true
 reads-clauses-on-methods = true
 
 # Options that differ from Dafny's

TestModels/dafny-dependencies/StandardLibrary/Makefile

@@ -103,6 +103,7 @@ transpile_implementation:
 		--stdin \
 		--no-verify \
 		--cores:$(CORES) \
+		--enforce-determinism \
 		--optimize-erasable-datatype-wrapper:false \
 		--unicode-char:false \
 		--function-syntax:3 \
@@ -138,7 +139,7 @@ dafny_benerate: DAFNY_RUST_OUTPUT_RS_DTR=\
 dafny_benerate: DAFNY_RUST_IMPL=\
 	runtimes/rust/src/implementation_from_dafny.rs
 dafny_benerate:
-	$(DAFNY) translate rs src/Index.dfy  --emit-uncompilable-code --no-verify   --optimize-erasable-datatype-wrapper false   --include-runtime   --compile-suffix true   --unicode-char false   --function-syntax 3   --allow-warnings   --output $(DAFNY_RUST_OUTPUT)
+	$(DAFNY) translate rs src/Index.dfy  --emit-uncompilable-code --no-verify --enforce-determinism  --optimize-erasable-datatype-wrapper false   --include-runtime   --compile-suffix true   --unicode-char false   --function-syntax 3   --allow-warnings   --output $(DAFNY_RUST_OUTPUT)
 	rustfmt $(DAFNY_RUST_OUTPUT_RS)
 	# echo "Diffs remaining till code generation works:"
 	# diff -u $(DAFNY_RUST_OUTPUT_RS) $(DAFNY_RUST_IMPL) | wc -l

codegen/build.gradle.kts

@@ -58,8 +58,8 @@ subprojects {
      */
 
     when (subproject.name) {
-        "smithy-dafny-codegen-test" -> println("Skipping publish for smithy-dafny-codegen-test")
-        "smithy-python-codegen" -> println("Skipping publish for smithy-python-codegen")
+        "smithy-dafny-codegen-test" -> logger.info("Skipping publish for smithy-dafny-codegen-test")
+        "smithy-python-codegen" -> logger.info("Skipping publish for smithy-python-codegen")
         else -> {
             if (subproject.name == "smithy-dafny-codegen-cli") {
                 apply(plugin = "application")

codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java

@@ -39,13 +39,16 @@ public class CodegenCli {
   private enum Command {
     GENERATE,
     PATCH_AFTER_TRANSPILE,
+    IF_DAFNY_AT_LEAST,
   }
 
   private static final Map<Command, Options> optionsForCommand = Map.of(
     Command.GENERATE,
     getCliOptionsForBuild(),
     Command.PATCH_AFTER_TRANSPILE,
-    getCliOptionsForPatchAfterTranspile()
+    getCliOptionsForPatchAfterTranspile(),
+    Command.IF_DAFNY_AT_LEAST,
+    getCliOptionsForIfDafnyAtLeast()
   );
 
   public static void main(String[] args) {
@@ -165,6 +168,7 @@ public static void main(String[] args) {
     switch (cliArguments.command) {
       case GENERATE -> engine.run();
       case PATCH_AFTER_TRANSPILE -> engine.patchAfterTranspiling();
+      // IF_DAFNY_AT_LEAST is handled in CodegenCli.parse() instead
     }
   }
 
@@ -454,6 +458,31 @@ private static Options getCliOptionsForPatchAfterTranspile() {
       );
   }
 
+  private static Options getCliOptionsForIfDafnyAtLeast() {
+    return new Options()
+      .addOption(
+        Option.builder("h").longOpt("help").desc("print help message").build()
+      )
+      .addOption(
+        Option
+          .builder()
+          .longOpt("dafny-version")
+          .desc("Minimum Dafny version to check for")
+          .hasArg()
+          .required()
+          .build()
+      )
+      .addOption(
+        Option
+          .builder()
+          .longOpt("text")
+          .desc("Text to output if the Dafny version passes the check")
+          .hasArg()
+          .required()
+          .build()
+      );
+  }
+
   private static void printHelpMessage() {
     new HelpFormatter()
       .printHelp(
@@ -465,6 +494,11 @@ private static void printHelpMessage() {
         "smithy-dafny-codegen-cli patch-after-transpile",
         getCliOptionsForPatchAfterTranspile()
       );
+    new HelpFormatter()
+      .printHelp(
+        "smithy-dafny-codegen-cli fs-dafny-at-least",
+        getCliOptionsForIfDafnyAtLeast()
+      );
   }
 
   private record CliArguments(
@@ -497,6 +531,7 @@ private record CliArguments(
      * @return parsed arguments, or {@code Optional.empty()} if help should be printed
      * @throws ParseException if command line arguments are invalid
      */
+    @SuppressWarnings("security:S4507") // Suppressing log injection warning for makefile echo-like command
     static Optional<CliArguments> parse(String[] args) throws ParseException {
       final DefaultParser parser = new DefaultParser();
       final String commandString = args.length > 0 && !args[0].startsWith("-")
@@ -525,6 +560,28 @@ static Optional<CliArguments> parse(String[] args) throws ParseException {
         return Optional.empty();
       }
 
+      DafnyVersion dafnyVersion = null;
+      String dafnyVersionStr = commandLine.getOptionValue("dafny-version");
+      if (dafnyVersionStr != null) {
+        try {
+          dafnyVersion = DafnyVersion.parse(dafnyVersionStr.trim());
+        } catch (IllegalArgumentException ex) {
+          LOGGER.error("Could not parse --dafny-version: {}", dafnyVersionStr);
+          throw ex;
+        }
+      }
+
+      // This command doesn't need a model/codegen engine/etc.
+      if (command == Command.IF_DAFNY_AT_LEAST) {
+        String text = commandLine.getOptionValue("text");
+        if (
+          CodegenEngine.getDafnyVersionFromDafny().compareTo(dafnyVersion) >= 0
+        ) {
+          System.out.println(text);
+        }
+        System.exit(0);
+      }
+
       Path libraryRoot = Paths.get(commandLine.getOptionValue("library-root"));
 
       final Path modelPath = Path.of(commandLine.getOptionValue('m'));
@@ -591,25 +648,14 @@ static Optional<CliArguments> parse(String[] args) throws ParseException {
 
       Optional<AwsSdkVersion> javaAwsSdkVersion = Optional.empty();
       if (commandLine.hasOption("java-aws-sdk-version")) {
-        final String versionStr = commandLine
+        final String sdkVersionStr = commandLine
           .getOptionValue("java-aws-sdk-version")
           .trim()
           .toUpperCase();
         try {
-          javaAwsSdkVersion = Optional.of(AwsSdkVersion.valueOf(versionStr));
-        } catch (IllegalArgumentException ex) {
-          LOGGER.error("Unknown Java AWS SDK version {}", versionStr);
-          throw ex;
-        }
-      }
-
-      DafnyVersion dafnyVersion = null;
-      String versionStr = commandLine.getOptionValue("dafny-version");
-      if (versionStr != null) {
-        try {
-          dafnyVersion = DafnyVersion.parse(versionStr.trim());
+          javaAwsSdkVersion = Optional.of(AwsSdkVersion.valueOf(sdkVersionStr));
         } catch (IllegalArgumentException ex) {
-          LOGGER.error("Could not parse --dafny-version: {}", versionStr);
+          LOGGER.error("Unknown Java AWS SDK version {}", sdkVersionStr);
           throw ex;
         }
       }

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java

@@ -1305,7 +1305,7 @@ public CodegenEngine build() {
       // If the version has not been released yet,
       // downgrade it. Otherwise, the system will not find runtime libraries
       // with the same version.
-      // The better fix for this is for Dafny to pre-release
+      // The better fix for this is for Dafny to pre-release runtimes as well.
       if (dafnyVersion.compareTo(MAX_DAFNY_VERSION) > 0) {
         LOGGER.warn(
           "Dafny version {} appears to be unreleased, downgrading to {} to ensure runtimes are available",