Cleanup

TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java

@@ -25,12 +25,6 @@
 // and reset the coder everytime.
 public class __default extends UTF8._ExternBase___default {
 
-    private static final dafny.TypeDescriptor<DafnySequence<? extends Byte>> BYTE_SEQUENCE_TYPE_DESCRIPTOR = 
-            dafny.DafnySequence.<Byte>_typeDescriptor(dafny.TypeDescriptor.BYTE);
-    private static final dafny.TypeDescriptor<DafnySequence<? extends Character>> CHARACTER_SEQUENCE_TYPE_DESCRIPTOR =
-            dafny.DafnySequence.<Character>_typeDescriptor(dafny.TypeDescriptor.CHAR);
-
-
     // This is largely copied from Polymorph's dafny-java-conversion:
     // software.amazon.smithy.dafny.conversion.ToDafny.Simple.DafnyUtf8Bytes
     public static Result<

TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy

@@ -29,6 +29,15 @@ module {:extern "UTF8"} UTF8 {
     // If it weren't, then data would be lost.
     ensures res.Success? ==> Decode(res.value).Success? && Decode(res.value).value == s
 
+  // Decode return a Result, therefore doesn't need to require utf8 input
+  function method {:extern "Decode"} Decode(b: seq<uint8>): (res: Result<string, string>)
+    ensures res.Success? ==> ValidUTF8Seq(b)
+
+  // The next four functions are for the benefit of the extern implementation to call,
+  // avoiding direct references to generic datatype constructors
+  // since their calling pattern is different between different versions of Dafny
+  // (i.e. after 4.2, explicit type descriptors are required).
+
   function method CreateEncodeSuccess(bytes: ValidUTF8Bytes): Result<ValidUTF8Bytes, string> {
     Success(bytes)
   }
@@ -37,21 +46,17 @@ module {:extern "UTF8"} UTF8 {
     Failure(error)
   }
 
-  // Decode return a Result, therefore doesn't need to require utf8 input
-  function method {:extern "Decode"} Decode(b: seq<uint8>): (res: Result<string, string>)
-    ensures res.Success? ==> ValidUTF8Seq(b)
-
-  predicate method IsASCIIString(s: string) {
-    forall i :: 0 <= i < |s| ==> s[i] as int < 128
-  }
-
   function method CreateDecodeSuccess(s: string): Result<string, string> {
     Success(s)
   }
 
   function method CreateDecodeFailure(error: string): Result<string, string> {
     Failure(error)
   }
+
+  predicate method IsASCIIString(s: string) {
+    forall i :: 0 <= i < |s| ==> s[i] as int < 128
+  }
 
   // Encode ASCII as UTF8 in a function, to allow use in ensures clause
   function method {:opaque} {:tailrecursion} EncodeAscii(s : string) : (ret : ValidUTF8Bytes)

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

@@ -122,7 +122,7 @@ private static Options getCliOptions() {
             .build())
           .addOption(Option.builder()
             .longOpt("dafny-version")
-            .desc("<optional> Dafny version to use. Defaults to 4.1.")
+            .desc("<optional> Dafny version to use. Defaults to 4.1.0")
             .hasArg()
             .build())
           .addOption(Option.builder()