fix(Go): Empty Blob fix (#797)

*Issue #, if available:*

*Description of changes:*
Adds the fix for empty blob, based on the test case here:
https://github.com/aws/private-aws-encryption-sdk-javascript-staging/pull/768/files

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

Diff for: TestModels/SimpleTypes/SimpleBlob/runtimes/go/TestsFromDafny-go/go.mod

@@ -10,4 +10,5 @@ require (
 )
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/SimpleTypes/SimpleBlob v0.0.0 => ../ImplementationFromDafny-go
+
 replace github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library => ../../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/

Diff for: TestModels/SimpleTypes/SimpleBlob/test/SimpleBlobImplTest.dfy

@@ -11,6 +11,7 @@ module SimpleBlobImplTest {
     method{:test} GetBlob(){
         var client :- expect SimpleBlob.SimpleBlob();
         TestGetBlob(client);
+        TestGetBlobWithEmptyBlob(client);
         TestGetBlobKnownValueTest(client);
     }
 
@@ -35,6 +36,27 @@ module SimpleBlobImplTest {
         print ret;
     }
 
+    method TestGetBlobWithEmptyBlob(client: ISimpleTypesBlobClient)
+      requires client.ValidState()
+      modifies client.Modifies
+      ensures client.ValidState()
+    {
+        var s: seq<UInt.uint8> := [];
+        var convertedBlobInput: GetBlobInput := SimpleBlob.Types.GetBlobInput(value:= Some(s));
+        SimpleBlobImpl.ValidateBlobType(convertedBlobInput.value.value);
+        // Validate values of convertedBlobInput are same as input values
+        expect convertedBlobInput.value.value == s;
+
+        var ret :- expect client.GetBlob(convertedBlobInput);
+
+        // Expect output of GetBlob has same value as input sequence
+        // i.e. GetBlob(GetBlobInput(seq)) == GetBlobInput(seq)
+        expect ret.value.UnwrapOr([0x0]) == convertedBlobInput.value.value;
+        // From above, GetBlobInput(seq) value == seq, so the below should be redundant
+        expect ret.value.UnwrapOr([0x0]) == s;
+        print ret;
+    }
+
     method TestGetBlobKnownValueTest(client: ISimpleTypesBlobClient)
       requires client.ValidState()
       modifies client.Modifies

Diff for: TestModels/SimpleTypes/SimpleBlob/test/WrappedSimpleBlobTest.dfy

@@ -10,6 +10,7 @@ module WrappedSimpleTypesBlobTest {
     method{:test} GetBlob() {
         var client :- expect WrappedSimpleTypesBlobService.WrappedSimpleBlob();
         SimpleBlobImplTest.TestGetBlob(client);
+        SimpleBlobImplTest.TestGetBlobWithEmptyBlob(client);
         SimpleBlobImplTest.TestGetBlobKnownValueTest(client);
     }
 }

Diff for: codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithygo/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java

@@ -439,6 +439,8 @@ var enum interface{}
           shape.toShapeId().getName()
         );
       }
+
+      writer.addImportFromModule(SMITHY_DAFNY_STD_LIB_GO, "UTF8");
       final var underlyingType =
         """
             func () dafny.Sequence {

Diff for: codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithygo/awssdk/shapevisitor/DafnyToAwsSdkShapeVisitor.java

@@ -133,7 +133,7 @@ public String blobShape(final BlobShape shape) {
       : dataSource;
     return """
     func () []byte {
-    var b []byte
+    b := []byte{}
     if %s == nil {
         return nil
     }
@@ -488,6 +488,7 @@ public String stringShape(final StringShape shape) {
       }
     }
 
+    writer.addImportFromModule(SMITHY_DAFNY_STD_LIB_GO, "UTF8");
     return """
     func() (%sstring) {
       %s

Diff for: codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithygo/localservice/shapevisitor/DafnyToSmithyShapeVisitor.java

@@ -1,6 +1,7 @@
 package software.amazon.polymorph.smithygo.localservice.shapevisitor;
 
 import static software.amazon.polymorph.smithygo.utils.Constants.DAFNY_RUNTIME_GO_LIBRARY_MODULE;
+import static software.amazon.polymorph.smithygo.utils.Constants.SMITHY_DAFNY_STD_LIB_GO;
 
 import java.util.LinkedHashMap;
 import java.util.Map;
@@ -286,7 +287,7 @@ public String blobShape(final BlobShape shape) {
     // Blob shape is inherently value type
     return """
     return func () []byte {
-    var b []byte
+    b := []byte{}
     if %s == nil {
         return nil
     }
@@ -666,6 +667,8 @@ public String stringShape(final StringShape shape) {
 
             s := string(dafny.ToByteArray(%s.(dafny.Sequence)))
         """.formatted(dataSource);
+    } else {
+      writer.addImportFromModule(SMITHY_DAFNY_STD_LIB_GO, "UTF8");
     }
 
     return """

Diff for: codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithygo/localservice/shapevisitor/SmithyToDafnyShapeVisitor.java

@@ -560,7 +560,10 @@ var enum interface{}
 
       if (shape.hasTrait(DafnyUtf8BytesTrait.class)) {
         writer.addUseImports(SmithyGoDependency.stdlib("unicode/utf8"));
+      } else {
+        writer.addImportFromModule(SMITHY_DAFNY_STD_LIB_GO, "UTF8");
       }
+
       final var underlyingType = shape.hasTrait(DafnyUtf8BytesTrait.class)
         ? """
             dafny.SeqOf(func () []interface{} {