From 8a1786b58a49438d22693350e9b9a9113911f970 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Mon, 30 Oct 2023 13:51:07 -0700
Subject: [PATCH] Cleanup

---
 .../java/src/main/java/UTF8/__default.java    |  6 ------
 .../StandardLibrary/src/UTF8.dfy              | 21 ++++++++++++-------
 .../software/amazon/polymorph/CodegenCli.java |  2 +-
 3 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java b/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java
index 2e14f9592..c3171cdd8 100644
--- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java
+++ b/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<
diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy
index a52f0b5d6..ca889813e 100644
--- a/TestModels/dafny-dependencies/StandardLibrary/src/UTF8.dfy
+++ b/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,14 +46,6 @@ 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)
   }
@@ -52,6 +53,10 @@ module {:extern "UTF8"} UTF8 {
   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)
diff --git a/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java b/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java
index 036cd49ef..6a37a25e7 100644
--- a/codegen/smithy-dafny-codegen-cli/src/main/java/software/amazon/polymorph/CodegenCli.java
+++ b/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()