chore: revert opaque string

TestModels/Dependencies/src/SimpleDependenciesImpl.dfy

@@ -160,7 +160,7 @@ module SimpleDependenciesImpl refines AbstractSimpleDependenciesOperations {
     returns (output: Result<SimpleExtendableResourcesTypes.GetExtendableResourceErrorsOutput, Error>)
   {
     var obj: object := new ExtendableResource.OpaqueMessage();
-    var extendableResourceError := SimpleExtendableResourcesTypes.Opaque(obj, "alt text for the message");
+    var extendableResourceError := SimpleExtendableResourcesTypes.Opaque(obj);
     var dependenciesError := Error.SimpleExtendableResources(extendableResourceError);
     return Failure(dependenciesError);
   }

TestModels/Errors/runtimes/rust/tests/simple_errors_test.rs

@@ -30,7 +30,7 @@ mod simple_errors_test {
         match result {
             Ok(_x) => assert!(false),
             Err(e) => match e {
-                Opaque { obj , ..} => assert!(obj.0.is_some()),
+                Opaque { obj } => assert!(obj.0.is_some()),
                 _ => assert!(false, "always_native_error did not return Opaque"),
             },
         }

TestModels/Errors/src/SimpleErrorsImpl.dfy

@@ -54,7 +54,7 @@ module SimpleErrorsImpl refines AbstractSimpleErrorsOperations  {
       // TODO: Rewrite this as an actual extern.
       var opaqueObject := new SomeOpaqueGeneratedTypeForTesting();
 
-      var res := Error.Opaque( obj := opaqueObject, alt_text := "Some Generated Test" );
+      var res := Error.Opaque( obj := opaqueObject );
 
       return Failure(res);
   }

TestModels/Extendable/src/ExtendableResource.dfy

@@ -140,7 +140,7 @@ module ExtendableResource {
       ensures unchanged(History)
     {
       var obj: object := new OpaqueMessage();
-      return Failure(Types.Opaque(obj, "lost in translation"));
+      return Failure(Types.Opaque(obj));
     }
   }
 }

TestModels/Extern/runtimes/net/Extern/ExternOperations.cs

@@ -27,7 +27,7 @@ public static _IResult<_IExternMustErrorOutput, _IError> ExternMustError(_IConfi
             var exception = new Exception(
                 TypeConversion
                     .FromDafny_N6_simple__N11_dafnyExtern__S20_ExternMustErrorInput__M5_value(input.dtor_value));
-            return Result<_IExternMustErrorOutput, _IError>.create_Failure(Error.create_Opaque(exception, Dafny.Sequence<char>.FromString(exception.ToString())));
+            return Result<_IExternMustErrorOutput, _IError>.create_Failure(Error.create_Opaque(exception));
         }
     }
 }
@@ -58,7 +58,7 @@ public static _IResult<ExternConstructorClass, _IError> Build(ISequence<char> in
             }
             catch (Exception ex)
             {
-                return Result<ExternConstructorClass, _IError>.create_Failure(Error.create_Opaque(ex, Dafny.Sequence<char>.FromString(ex.ToString())));
+                return Result<ExternConstructorClass, _IError>.create_Failure(Error.create_Opaque(ex));
             }
         }
 

TestModels/Extern/runtimes/net/Extern/WrappedSimpleExternService.cs

@@ -3,13 +3,11 @@
 using Wrappers_Compile;
 using Simple.DafnyExtern;
 using Simple.DafnyExtern.Wrapped;
-using TypeConversion = Simple.DafnyExtern.TypeConversion;
+using TypeConversion = Simple.DafnyExtern.TypeConversion ;
 namespace simple.dafnyextern.internaldafny.wrapped
 {
-    public partial class __default
-    {
-        public static _IResult<types.ISimpleExternClient, types._IError> WrappedSimpleExtern(types._ISimpleExternConfig config)
-        {
+    public partial class __default {
+        public static _IResult<types.ISimpleExternClient, types._IError> WrappedSimpleExtern(types._ISimpleExternConfig config) {
             var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_dafnyExtern__S18_SimpleExternConfig(config);
             var impl = new SimpleExtern(wrappedConfig);
             var wrappedClient = new SimpleExternShim(impl);

TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/ExternConstructor.py

@@ -21,6 +21,6 @@ def Build(input):
       try:
         return Wrappers.Result_Success(ExternConstructorClass(input))
       except Exception as e:
-        return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(e, repr(e)))
+        return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(e))
 
-simple_dafnyextern.internaldafny.generated.ExternConstructor.ExternConstructorClass = ExternConstructorClass
+simple_dafnyextern.internaldafny.generated.ExternConstructor.ExternConstructorClass = ExternConstructorClass

TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/SimpleExternImpl.py

@@ -18,7 +18,7 @@ def GetExtern(config, input):
 @staticmethod
 def ExternMustError(config, input):
   exception = Exception(input)
-  return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(exception, repr(input)))
+  return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(exception))
 
 default__.GetExtern = GetExtern
-default__.ExternMustError = ExternMustError
+default__.ExternMustError = ExternMustError

TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs

@@ -8,7 +8,7 @@ pub fn to_opaque_error<E: std::error::Error + 'static>(value: E) ->
     )));
   ::std::rc::Rc::new(
     crate::r#language::specific::logic::internaldafny::types::Error::Opaque {
-        obj: error_obj, alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo")
+        obj: error_obj,
     },
   )
 }

TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs

@@ -9,7 +9,7 @@ pub fn to_dafny_error(
 {
     match value {
     crate::operation::get_runtime_information::GetRuntimeInformationError::Unhandled(unhandled) =>
-      ::std::rc::Rc::new(crate::r#language::specific::logic::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)), alt_text: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") })
+      ::std::rc::Rc::new(crate::r#language::specific::logic::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) })
   }
 }
 

TestModels/LanguageSpecificLogic/runtimes/rust/src/deps.rs

@@ -1,3 +1,3 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
-// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.

TestModels/Refinement/runtimes/rust/src/conversions/get_refinement.rs

@@ -8,7 +8,7 @@ pub fn to_dafny_error(
 ) -> ::std::rc::Rc<crate::r#simple::refinement::internaldafny::types::Error> {
     match value {
     crate::operation::get_refinement::GetRefinementError::Unhandled(unhandled) =>
-      ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") })
+      ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) })
   }
 }
 

TestModels/Refinement/runtimes/rust/src/conversions/only_input.rs

@@ -11,7 +11,7 @@ pub fn to_dafny_error(
             crate::r#simple::refinement::internaldafny::types::Error::Opaque {
                 obj: ::dafny_runtime::upcast_object()(
                     ::dafny_runtime::object::new(unhandled),
-                ), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo")
+                ),
             },
         ),
     }

TestModels/Refinement/runtimes/rust/src/conversions/only_output.rs

@@ -11,7 +11,7 @@ pub fn to_dafny_error(
             crate::r#simple::refinement::internaldafny::types::Error::Opaque {
                 obj: ::dafny_runtime::upcast_object()(
                     ::dafny_runtime::object::new(unhandled),
-                ), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo")
+                ),
             },
         ),
     }

TestModels/Refinement/runtimes/rust/src/conversions/readonly_operation.rs

@@ -8,7 +8,7 @@ pub fn to_dafny_error(
 ) -> ::std::rc::Rc<crate::r#simple::refinement::internaldafny::types::Error> {
     match value {
     crate::operation::readonly_operation::ReadonlyOperationError::Unhandled(unhandled) =>
-      ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") })
+      ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) })
   }
 }
 

TestModels/Refinement/runtimes/rust/src/deps.rs

@@ -1,3 +1,3 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
-// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.

TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy

@@ -1122,7 +1122,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty
 
 
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string := "")
+    | Opaque(obj: object)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractComAmazonawsDynamodbService {

TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy

@@ -439,7 +439,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"
 
 
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string := "")
+    | Opaque(obj: object)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractComAmazonawsKmsService {

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

@@ -1868,7 +1868,7 @@ public TokenTree generateModeledErrorDataType() {
         Token.of(
           "// The Opaque error, used for native, extern, wrapped or unknown errors"
         ),
-        Token.of("| Opaque(obj: object, alt_text : string := \"\")"),
+        Token.of("| Opaque(obj: object)"),
         // Helper error for use with `extern`
         Token.of("type OpaqueError = e: Error | e.Opaque? witness *")
       )

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

@@ -186,7 +186,7 @@ protected TokenTree errorToDafnyBody(
     final TokenTree unknownErrorCase = Token.of(
       """
       default:
-          return new %s(value, Dafny.Sequence<char>.FromString(value.ToString()));
+          return new %s(value);
       """.formatted(dafnyUnknownErrorType)
     );
     final TokenTree cases = TokenTree

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

@@ -1718,20 +1718,20 @@ protected TokenTree errorToDafnyBody(
         "case %1$s exception:".formatted(
             DotNetNameResolver.baseClassForUnknownError()
           ),
-        "return new %1$s(exception, Dafny.Sequence<char>.FromString(exception.ToString()));".formatted(
+        "return new %1$s(exception);".formatted(
             DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape(
               serviceShape
             )
           ),
         "case %1$s exception:".formatted(C_SHARP_SYSTEM_EXCEPTION),
-        "return new %1$s(exception, Dafny.Sequence<char>.FromString(exception.ToString()));".formatted(
+        "return new %1$s(exception);".formatted(
             DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape(
               serviceShape
             )
           ),
         "default:",
         "// The switch MUST be complete for System.Exception, so `value` MUST NOT be an System.Exception. (How did you get here?)",
-        "return new %1$s(value, Dafny.Sequence<char>.FromString(value.ToString()));".formatted(
+        "return new %1$s(value);".formatted(
             DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape(
               serviceShape
             )

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedShimCodegen.java

@@ -325,7 +325,7 @@ public TokenTree generateErrorTypeShim() {
     final TokenTree unknownErrorCase = Token.of(
       """
       default:
-          return new %s(error, Dafny.Sequence<char>.FromString(error.ToString()));
+          return new %s(error);
       """.formatted(dafnyUnknownErrorType)
     );
 

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

@@ -57,11 +57,6 @@ public class BuilderMemberSpec {
       "obj",
       "The unexpected object encountered. It MIGHT BE an Exception," +
       " but that is not guaranteed."
-    ),
-    new BuilderMemberSpec(
-      TypeName.get(String.class),
-      "altText",
-      "A best effort text representation of obj."
     )
   );
   public static final List<BuilderMemberSpec> COLLECTION_ARGS = List.of(

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java

@@ -705,7 +705,7 @@ MethodSpec generateConvertOpaqueServiceError() {
         "nativeValue"
       )
       .addStatement(
-        "return $T.create_Opaque(nativeValue, dafny.DafnySequence.asString(nativeValue.getMessage()))",
+        "return $T.create_Opaque(nativeValue)",
         subject.dafnyNameResolver.abstractClassForError()
       )
       .build();
@@ -731,7 +731,7 @@ MethodSpec generateConvertOpaqueError() {
         "Which would allow Dafny developers to treat the two differently."
       )
       .addStatement(
-        "return $T.create_Opaque(nativeValue, dafny.DafnySequence.asString(nativeValue.getMessage()))",
+        "return $T.create_Opaque(nativeValue)",
         subject.dafnyNameResolver.abstractClassForError()
       )
       .build();

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java

@@ -177,13 +177,7 @@ MethodSpec runtimeException() {
         .endControlFlow()
     );
     return method
-      .addStatement(
-        "return $T.create_Opaque($L, dafny.DafnySequence.asString(java.util.Objects.nonNull($L.getMessage()) ? $L.getMessage() : \"\"))",
-        dafnyError,
-        VAR_INPUT,
-        VAR_INPUT,
-        VAR_INPUT
-      )
+      .addStatement("return $T.create_Opaque($L)", dafnyError, VAR_INPUT)
       .build();
   }
 
@@ -197,13 +191,7 @@ MethodSpec opaqueError() {
       .returns(dafnyError)
       .addModifiers(PUBLIC_STATIC)
       .addParameter(opaqueError, VAR_INPUT)
-      .addStatement(
-        "return $T.create_Opaque($L.obj(), dafny.DafnySequence.asString(java.util.Objects.nonNull($L.altText()) ? $L.altText() : \"\"))",
-        dafnyError,
-        VAR_INPUT,
-        VAR_INPUT,
-        VAR_INPUT
-      )
+      .addStatement("return $T.create_Opaque($L.obj())", dafnyError, VAR_INPUT)
       .build();
   }
 

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/unmodeled/OpaqueError.java

@@ -93,7 +93,6 @@ static MethodSpec constructor(BuilderSpecs builderSpecs) {
         BuilderSpecs.BUILDER_VAR,
         BuilderSpecs.BUILDER_VAR
       )
-      .addStatement("this.altText = builder.altText()")
       .addStatement("this.obj = builder.obj()");
     return method.build();
   }

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/customize/AwsSdkShimFileWriter.java

@@ -86,20 +86,6 @@ def __init__(self, _impl, _region):
       );
   }
 
-  private static final String DAFNY_STRING_E =
-    """
-            _dafny.Seq(
-                "".join(
-                    [
-                        chr(int.from_bytes(pair, "big"))
-                        for pair in zip(
-                            *[iter(repr(e).encode("utf-16-be"))] * 2
-                        )
-                    ]
-                )
-            )
-    """;
-
   /**
    * Generate the method body for the `_sdk_error_to_dafny_error` method. This writes out a block to
    * convert a boto3 ClientError modelled in JSON into a Dafny-modelled error
@@ -160,33 +146,30 @@ private void generateAwsSdkErrorToDafnyErrorBlock(
       hasOpenedIfBlock = true;
     }
 
-    writer.addStdlibImport("_dafny");
     if (hasOpenedIfBlock) {
       // If `hasOpenedIfBlock` is false, then codegen never wrote any errors,
       // and this function should only cast to Opaque errors
       writer.write(
         """
-        return $L.Error_Opaque(obj=e, alt__text=$L)
+        return $L.Error_Opaque(obj=e)
         """,
         DafnyNameResolver.getDafnyPythonTypesModuleNameForShape(
           serviceShape.getId(),
           codegenContext
-        ),
-        DAFNY_STRING_E
+        )
       );
     } else {
       // If `hasOpenedIfBlock` is true, then codegen wrote at least one error,
       // and this function should only cast to Opaque error via `else`
       writer.write(
         """
         else:
-          return $L.Error_Opaque(obj=e, alt__text=$L)
+            return $L.Error_Opaque(obj=e)
         """,
         DafnyNameResolver.getDafnyPythonTypesModuleNameForShape(
           serviceShape.getId(),
           codegenContext
-        ),
-        DAFNY_STRING_E
+        )
       );
     }
   }

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/DafnyPythonLocalServiceProtocolGenerator.java

@@ -459,7 +459,7 @@ private void generateErrorResponseDeserializerSection(
             writer.write(
               """
               if error.is_Opaque:
-                  return OpaqueError(obj=error.obj, alt_text=error.alt__text)
+                  return OpaqueError(obj=error.obj)
               elif error.is_CollectionOfErrors:
                   return CollectionOfErrors(
                       message=_dafny.string_of(error.message),
@@ -496,7 +496,7 @@ private void generateErrorResponseDeserializerSection(
             writer.write(
               """
               else:
-                  return OpaqueError(obj=error, alt_text=repr(error))"""
+                  return OpaqueError(obj=error)"""
             );
           }
         );