Revert pr 496 (#798)

*Issue #, if available:*

*Description of changes:*
This PR reverts the commit for the change:
#496 since it's not
released to mpl yet.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Shubham Chaturvedi <scchatur@amazon.com>

Author: ShubhamChaturvedi7

.gitmodules

@@ -4,4 +4,4 @@
 [submodule "TestModels/dafny-dependencies/dafny"]
 	path = TestModels/dafny-dependencies/dafny
 	url = https://github.com/dafny-lang/dafny.git
-	branch = actions-and-streaming-stdlibs
+	branch = actions-and-streaming-stdlibs

TestModels/Constraints/Model/Constraints.smithy

@@ -22,7 +22,7 @@ structure SimpleConstraintsConfig {
 
 // This is just a sanity check on the smokeTests support.
 // We need to actually convert all the tests in test/WrappedSimpleConstraintsImplTest.dfy
-// to smoke tests now that https://github.com/smithy-lang/smithy-dafny/issues/278
+// to smoke tests once https://github.com/smithy-lang/smithy-dafny/issues/278
 // is fixed.
 @smithy.test#smokeTests([
   {
@@ -44,22 +44,17 @@ structure SimpleConstraintsConfig {
         success: {}
     }
   },
-  {
-    id: "GetConstraintsSuccessNoParams"
-    vendorParams: {
-      RequiredString: "foobar",
-    }
-    params: {}
-    expect: {
-        success: {}
-    }
-  },
   {
     id: "GetConstraintsFailure"
     vendorParams: {
       RequiredString: "foobar",
     }
     params: {
+      // These two always have to be present because of https://github.com/smithy-lang/smithy-dafny/issues/278,
+      // because otherwise they are interpreted as 0.
+      OneToTen: 5,
+      GreaterThanOne: 2,
+      // This is the member that's actually invalid
       NonEmptyBlob: ""
     }
     expect: {

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

@@ -46,13 +46,6 @@ private boolean isGeneratedInSdk(final ShapeId shapeId) {
   }
 
   @Override
-  protected String baseTypeForMember(final MemberShape memberShape) {
-    // The AWS SDK uses primitive types for required members.
-    return memberShapeIsOptional(memberShape)
-      ? super.baseTypeForMember(memberShape)
-      : baseTypeForShape(memberShape.getTarget());
-  }
-
   protected String baseTypeForEnum(final EnumShape enumShape) {
     if (isGeneratedInSdk(enumShape.getId())) {
       return "%s.%s".formatted(

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

@@ -82,11 +82,7 @@ public TokenTree generateExtractOptionalMember(MemberShape memberShape) {
     final String propertyName = nameResolver.classPropertyForStructureMember(
       memberShape
     );
-    return TokenTree.of(
-      type,
-      varName,
-      "= (%s)value.%s;".formatted(type, propertyName)
-    );
+    return TokenTree.of(type, varName, "= value.%s;".formatted(propertyName));
   }
 
   @Override

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

@@ -412,8 +412,9 @@ protected String baseTypeForUnion(final UnionShape unionShape) {
   }
 
   protected String baseTypeForMember(final MemberShape memberShape) {
-    // We always use nullable types for safety.
-    return baseTypeForOptionalMember(memberShape);
+    final String baseType = baseTypeForShape(memberShape.getTarget());
+    final boolean isOptional = memberShapeIsOptional(memberShape);
+    return isOptional ? baseTypeForOptionalMember(memberShape) : baseType;
   }
 
   protected String baseTypeForOptionalMember(final MemberShape memberShape) {

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

@@ -797,6 +797,20 @@ public TypeConverter generateMemberConverter(final MemberShape memberShape) {
       TO_DAFNY
     );
 
+    if (!nameResolver.memberShapeIsOptional(memberShape)) {
+      final TokenTree fromDafnyBody = Token.of(
+        "return %s(value);".formatted(targetFromDafnyConverterName)
+      );
+      final TokenTree toDafnyBody = Token.of(
+        "return %s(value);".formatted(targetToDafnyConverterName)
+      );
+      return buildConverterFromMethodBodies(
+        memberShape,
+        fromDafnyBody,
+        toDafnyBody
+      );
+    }
+
     String cSharpTypeUnModified;
     if (
       StringUtils.equals(
@@ -814,23 +828,6 @@ public TypeConverter generateMemberConverter(final MemberShape memberShape) {
         cSharpTypeUnModified.substring(0, (cSharpTypeUnModified.length() - 1));
     }
 
-    if (!nameResolver.memberShapeIsOptional(memberShape)) {
-      final TokenTree fromDafnyBody = Token.of(
-        "return %s(value);".formatted(targetFromDafnyConverterName)
-      );
-      final TokenTree toDafnyBody = Token.of(
-        "return %s((%s)value);".formatted(
-            targetToDafnyConverterName,
-            cSharpTypeUnModified
-          )
-      );
-      return buildConverterFromMethodBodies(
-        memberShape,
-        fromDafnyBody,
-        toDafnyBody
-      );
-    }
-
     final String cSharpType = cSharpTypeUnModified;
     final String cSharpOptionType;
     if (
@@ -903,8 +900,6 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
           .map(memberShape -> {
             final String propertyName =
               nameResolver.classPropertyForStructureMember(memberShape);
-            final String propertyType =
-              nameResolver.classPropertyTypeForStructureMember(memberShape);
             final String memberFromDafnyConverterName = typeConverterForShape(
               memberShape.getId(),
               FROM_DAFNY
@@ -935,9 +930,8 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
               .append(
                 TokenTree
                   .of(
-                    "converted.%s = (%s)(%s(concrete.dtor_%s));".formatted(
+                    "converted.%s = %s(concrete.dtor_%s);".formatted(
                         propertyName,
-                        propertyType,
                         memberFromDafnyConverterName,
                         destructorValue
                       ),

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

@@ -32,6 +32,7 @@
 import software.amazon.smithy.model.shapes.Shape;
 import software.amazon.smithy.model.shapes.ShapeId;
 import software.amazon.smithy.model.shapes.ShapeType;
+import software.amazon.smithy.model.traits.BoxTrait;
 import software.amazon.smithy.model.traits.EnumTrait;
 import software.amazon.smithy.model.traits.StreamingTrait;
 
@@ -75,13 +76,13 @@ public class Native extends NameResolver {
     NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE =
       Map.ofEntries(
         Map.entry(ShapeType.BLOB, ClassName.get(ByteBuffer.class)),
-        Map.entry(ShapeType.BOOLEAN, TypeName.BOOLEAN.box()),
-        Map.entry(ShapeType.BYTE, TypeName.BYTE.box()),
-        Map.entry(ShapeType.SHORT, TypeName.SHORT.box()),
-        Map.entry(ShapeType.INTEGER, TypeName.INT.box()),
-        Map.entry(ShapeType.LONG, TypeName.LONG.box()),
-        Map.entry(ShapeType.FLOAT, TypeName.FLOAT.box()),
-        Map.entry(ShapeType.DOUBLE, TypeName.DOUBLE.box()),
+        Map.entry(ShapeType.BOOLEAN, TypeName.BOOLEAN),
+        Map.entry(ShapeType.BYTE, TypeName.BYTE),
+        Map.entry(ShapeType.SHORT, TypeName.SHORT),
+        Map.entry(ShapeType.INTEGER, TypeName.INT),
+        Map.entry(ShapeType.LONG, TypeName.LONG),
+        Map.entry(ShapeType.FLOAT, TypeName.FLOAT),
+        Map.entry(ShapeType.DOUBLE, TypeName.DOUBLE),
         // TODO: AWS SDK V2 uses Instant, not Date
         Map.entry(ShapeType.TIMESTAMP, ClassName.get(Date.class)),
         Map.entry(ShapeType.BIG_DECIMAL, ClassName.get(BigDecimal.class)),
@@ -143,14 +144,21 @@ public TypeName typeForShape(final ShapeId shapeId) {
     }
 
     return switch (shape.getType()) {
-      // All primitives are boxed for safety, even if @required
-      case BOOLEAN,
-        BYTE,
-        SHORT,
-        INTEGER,
-        LONG,
-        FLOAT,
-        DOUBLE -> NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE.get(shape.getType());
+      case BOOLEAN, BYTE, SHORT, INTEGER, LONG, FLOAT, DOUBLE -> {
+        /* From the Smithy Docs:
+         * "Boolean, byte, short, integer, long, float, and double shapes
+         * are only considered boxed if they are marked with the box trait.
+         * All other shapes are always considered boxed."
+         * https://smithy.io/1.0/spec/core/type-refinement-traits.html#box-trait
+         * While Smithy Models SHOULD use Smithy Prelude shapes to avoid this confusion,
+         * they do not have to.
+         * Hence, the need to check if these shapes have the box trait
+         */
+        final TypeName typeName = NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE.get(
+          shape.getType()
+        );
+        yield shape.hasTrait(BoxTrait.class) ? typeName.box() : typeName;
+      }
       // For supported simple shapes, just map to native types
       case BLOB,
         TIMESTAMP,

codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/Constants.java

@@ -11,10 +11,10 @@ class Constants {
   static String RANGE_TRAIT_INTEGER_BUILD_EXPECTED =
     """
     %s {
-      if (Objects.nonNull(this.zeroToTen()) && this.zeroToTen() < 0) {
+      if (this._zeroToTenSet && this.zeroToTen() < 0) {
         throw new IllegalArgumentException("`zeroToTen` must be greater than or equal to 0");
       }
-      if (Objects.nonNull(this.zeroToTen()) && this.zeroToTen() > 10) {
+      if (this._zeroToTenSet && this.zeroToTen() > 10) {
         throw new IllegalArgumentException("`zeroToTen` must be less than or equal to 10.");
       }
       %s