diff --git a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go
index 88e1ce273f..07daa0b7e9 100644
--- a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go
+++ b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go
@@ -292,12 +292,7 @@ func Aws_cryptography_keyStore_BranchKeyMaterials_branchKey_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_keyStore_GetBeaconKeyInput_branchKeyIdentifier_FromDafny(input interface{}) string {
@@ -345,12 +340,7 @@ func Aws_cryptography_keyStore_BeaconKeyMaterials_beaconKey_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_keyStore_BeaconKeyMaterials_hmacKeys_FromDafny(input interface{}) map[string][]byte {
@@ -382,12 +372,7 @@ func Aws_cryptography_keyStore_HmacKeyMap_value_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_keyStore_GetBranchKeyVersionInput_branchKeyIdentifier_FromDafny(input interface{}) string {
diff --git a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go
index 7bceb4391b..d064ebb012 100644
--- a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go
+++ b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go
@@ -886,12 +886,7 @@ func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_send
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_recipientPublicKey_FromDafny(input interface{}) []byte {
@@ -899,12 +894,7 @@ func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_reci
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_curveSpec_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1392,12 +1382,7 @@ func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_publicKey_Fr
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_kmsKeyId_FromDafny(input interface{}) string {
@@ -1526,12 +1511,7 @@ func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingAlg_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AesWrappingAlg {
@@ -1585,12 +1565,7 @@ func Aws_cryptography_materialProviders_PublicKeyDiscoveryInput_recipientStaticP
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_RawPrivateKeyToStaticPublicKey_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.RawPrivateKeyToStaticPublicKeyInput {
@@ -1603,12 +1578,7 @@ func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_send
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_recipientPublicKey_FromDafny(input interface{}) []byte {
@@ -1616,12 +1586,7 @@ func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_reci
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_EphemeralPrivateKeyToStaticPublicKey_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.EphemeralPrivateKeyToStaticPublicKeyInput {
@@ -1632,12 +1597,7 @@ func Aws_cryptography_materialProviders_EphemeralPrivateKeyToStaticPublicKeyInpu
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRawEcdhKeyringInput_curveSpec_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1699,12 +1659,7 @@ func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_publicKey_FromD
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_privateKey_FromDafny(input interface{}) []byte {
@@ -1712,12 +1667,7 @@ func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_privateKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRequiredEncryptionContextCMMInput_requiredEncryptionContextKeys_FromDafny(input interface{}) []string {
@@ -1814,12 +1764,7 @@ func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_binaryId_FromDafny(in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_messageVersion_FromDafny(input interface{}) int32 {
@@ -2173,12 +2118,7 @@ func Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_FromDafny(input interface{}) []byte {
@@ -2186,12 +2126,7 @@ func Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_FromDafny(input interface{}) []byte {
@@ -2199,12 +2134,7 @@ func Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteInfo {
@@ -2267,12 +2197,7 @@ func Aws_cryptography_materialProviders_EncryptedDataKey_keyProviderInfo_FromDaf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptedDataKey_ciphertext_FromDafny(input interface{}) []byte {
@@ -2280,12 +2205,7 @@ func Aws_cryptography_materialProviders_EncryptedDataKey_ciphertext_FromDafny(in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_FromDafny(input interface{}) []string {
@@ -2304,12 +2224,7 @@ func Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_FromDafny(input interface{}) []byte {
@@ -2317,12 +2232,7 @@ func Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_FromDafny(input interface{}) [][]byte {
@@ -2344,12 +2254,7 @@ func Aws_cryptography_materialProviders_SymmetricSigningKeyList_member_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_GetAlgorithmSuiteInfoInput_binaryId_FromDafny(input interface{}) []byte {
@@ -2357,12 +2262,7 @@ func Aws_cryptography_materialProviders_GetAlgorithmSuiteInfoInput_binaryId_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId {
@@ -2460,12 +2360,7 @@ func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_signi
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_verificationKey_FromDafny(input interface{}) []byte {
@@ -2473,12 +2368,7 @@ func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_verif
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnDecryptInput_algorithm_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId {
@@ -2677,12 +2567,7 @@ func Aws_cryptography_materialProviders_DeleteCacheEntryInput_identifier_FromDaf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_GetCacheEntryInput_identifier_FromDafny(input interface{}) []byte {
@@ -2690,12 +2575,7 @@ func Aws_cryptography_materialProviders_GetCacheEntryInput_identifier_FromDafny(
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_GetCacheEntryInput_bytesUsed_FromDafny(input interface{}) *int64 {
@@ -2803,12 +2683,7 @@ func Aws_cryptography_materialProviders_PutCacheEntryInput_identifier_FromDafny(
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_PutCacheEntryInput_materials_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.Materials {
@@ -2881,12 +2756,7 @@ func Aws_cryptography_materialProviders_UpdateUsageMetadataInput_identifier_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_UpdateUsageMetadataInput_bytesUsed_FromDafny(input interface{}) int32 {
diff --git a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go
index 88e1ce273f..07daa0b7e9 100644
--- a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go
+++ b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographykeystoresmithygenerated/to_native.go
@@ -292,12 +292,7 @@ func Aws_cryptography_keyStore_BranchKeyMaterials_branchKey_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_keyStore_GetBeaconKeyInput_branchKeyIdentifier_FromDafny(input interface{}) string {
@@ -345,12 +340,7 @@ func Aws_cryptography_keyStore_BeaconKeyMaterials_beaconKey_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_keyStore_BeaconKeyMaterials_hmacKeys_FromDafny(input interface{}) map[string][]byte {
@@ -382,12 +372,7 @@ func Aws_cryptography_keyStore_HmacKeyMap_value_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_keyStore_GetBranchKeyVersionInput_branchKeyIdentifier_FromDafny(input interface{}) string {
diff --git a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go
index 7bceb4391b..d064ebb012 100644
--- a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go
+++ b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderssmithygenerated/to_native.go
@@ -886,12 +886,7 @@ func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_send
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_recipientPublicKey_FromDafny(input interface{}) []byte {
@@ -899,12 +894,7 @@ func Aws_cryptography_materialProviders_KmsPrivateKeyToStaticPublicKeyInput_reci
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateAwsKmsEcdhKeyringInput_curveSpec_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1392,12 +1382,7 @@ func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_publicKey_Fr
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateAwsKmsRsaKeyringInput_kmsKeyId_FromDafny(input interface{}) string {
@@ -1526,12 +1511,7 @@ func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRawAesKeyringInput_wrappingAlg_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AesWrappingAlg {
@@ -1585,12 +1565,7 @@ func Aws_cryptography_materialProviders_PublicKeyDiscoveryInput_recipientStaticP
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_RawPrivateKeyToStaticPublicKey_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.RawPrivateKeyToStaticPublicKeyInput {
@@ -1603,12 +1578,7 @@ func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_send
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_recipientPublicKey_FromDafny(input interface{}) []byte {
@@ -1616,12 +1586,7 @@ func Aws_cryptography_materialProviders_RawPrivateKeyToStaticPublicKeyInput_reci
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_RawEcdhStaticConfigurations_EphemeralPrivateKeyToStaticPublicKey_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.EphemeralPrivateKeyToStaticPublicKeyInput {
@@ -1632,12 +1597,7 @@ func Aws_cryptography_materialProviders_EphemeralPrivateKeyToStaticPublicKeyInpu
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRawEcdhKeyringInput_curveSpec_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1699,12 +1659,7 @@ func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_publicKey_FromD
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_privateKey_FromDafny(input interface{}) []byte {
@@ -1712,12 +1667,7 @@ func Aws_cryptography_materialProviders_CreateRawRsaKeyringInput_privateKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_CreateRequiredEncryptionContextCMMInput_requiredEncryptionContextKeys_FromDafny(input interface{}) []string {
@@ -1814,12 +1764,7 @@ func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_binaryId_FromDafny(in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_AlgorithmSuiteInfo_messageVersion_FromDafny(input interface{}) int32 {
@@ -2173,12 +2118,7 @@ func Aws_cryptography_materialProviders_DecryptionMaterials_plaintextDataKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_FromDafny(input interface{}) []byte {
@@ -2186,12 +2126,7 @@ func Aws_cryptography_materialProviders_DecryptionMaterials_verificationKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_FromDafny(input interface{}) []byte {
@@ -2199,12 +2134,7 @@ func Aws_cryptography_materialProviders_DecryptionMaterials_symmetricSigningKey_
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_algorithmSuite_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteInfo {
@@ -2267,12 +2197,7 @@ func Aws_cryptography_materialProviders_EncryptedDataKey_keyProviderInfo_FromDaf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptedDataKey_ciphertext_FromDafny(input interface{}) []byte {
@@ -2280,12 +2205,7 @@ func Aws_cryptography_materialProviders_EncryptedDataKey_ciphertext_FromDafny(in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_requiredEncryptionContextKeys_FromDafny(input interface{}) []string {
@@ -2304,12 +2224,7 @@ func Aws_cryptography_materialProviders_EncryptionMaterials_plaintextDataKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_FromDafny(input interface{}) []byte {
@@ -2317,12 +2232,7 @@ func Aws_cryptography_materialProviders_EncryptionMaterials_signingKey_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_EncryptionMaterials_symmetricSigningKeys_FromDafny(input interface{}) [][]byte {
@@ -2344,12 +2254,7 @@ func Aws_cryptography_materialProviders_SymmetricSigningKeyList_member_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_GetAlgorithmSuiteInfoInput_binaryId_FromDafny(input interface{}) []byte {
@@ -2357,12 +2262,7 @@ func Aws_cryptography_materialProviders_GetAlgorithmSuiteInfoInput_binaryId_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_InitializeDecryptionMaterialsInput_algorithmSuiteId_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId {
@@ -2460,12 +2360,7 @@ func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_signi
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_verificationKey_FromDafny(input interface{}) []byte {
@@ -2473,12 +2368,7 @@ func Aws_cryptography_materialProviders_InitializeEncryptionMaterialsInput_verif
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_ValidateCommitmentPolicyOnDecryptInput_algorithm_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.AlgorithmSuiteId {
@@ -2677,12 +2567,7 @@ func Aws_cryptography_materialProviders_DeleteCacheEntryInput_identifier_FromDaf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_GetCacheEntryInput_identifier_FromDafny(input interface{}) []byte {
@@ -2690,12 +2575,7 @@ func Aws_cryptography_materialProviders_GetCacheEntryInput_identifier_FromDafny(
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_GetCacheEntryInput_bytesUsed_FromDafny(input interface{}) *int64 {
@@ -2803,12 +2683,7 @@ func Aws_cryptography_materialProviders_PutCacheEntryInput_identifier_FromDafny(
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_PutCacheEntryInput_materials_FromDafny(input interface{}) awscryptographymaterialproviderssmithygeneratedtypes.Materials {
@@ -2881,12 +2756,7 @@ func Aws_cryptography_materialProviders_UpdateUsageMetadataInput_identifier_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProviders_UpdateUsageMetadataInput_bytesUsed_FromDafny(input interface{}) int32 {
diff --git a/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go b/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go
index 7bc7d231b5..ec894cacb2 100644
--- a/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go
+++ b/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go
@@ -380,12 +380,7 @@ func Aws_cryptography_primitives_AESDecryptInput_key_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_cipherTxt_FromDafny(input interface{}) []byte {
@@ -393,12 +388,7 @@ func Aws_cryptography_primitives_AESDecryptInput_cipherTxt_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_authTag_FromDafny(input interface{}) []byte {
@@ -406,12 +396,7 @@ func Aws_cryptography_primitives_AESDecryptInput_authTag_FromDafny(input interfa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_iv_FromDafny(input interface{}) []byte {
@@ -419,12 +404,7 @@ func Aws_cryptography_primitives_AESDecryptInput_iv_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_aad_FromDafny(input interface{}) []byte {
@@ -432,12 +412,7 @@ func Aws_cryptography_primitives_AESDecryptInput_aad_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptOutput_plaintext_FromDafny(input interface{}) []byte {
@@ -445,12 +420,7 @@ func Aws_cryptography_primitives_AESDecryptOutput_plaintext_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_encAlg_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.AES_GCM {
@@ -464,12 +434,7 @@ func Aws_cryptography_primitives_AESEncryptInput_iv_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_key_FromDafny(input interface{}) []byte {
@@ -477,12 +442,7 @@ func Aws_cryptography_primitives_AESEncryptInput_key_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_msg_FromDafny(input interface{}) []byte {
@@ -490,12 +450,7 @@ func Aws_cryptography_primitives_AESEncryptInput_msg_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_aad_FromDafny(input interface{}) []byte {
@@ -503,12 +458,7 @@ func Aws_cryptography_primitives_AESEncryptInput_aad_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptOutput_cipherText_FromDafny(input interface{}) []byte {
@@ -516,12 +466,7 @@ func Aws_cryptography_primitives_AESEncryptOutput_cipherText_FromDafny(input int
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptOutput_authTag_FromDafny(input interface{}) []byte {
@@ -529,12 +474,7 @@ func Aws_cryptography_primitives_AESEncryptOutput_authTag_FromDafny(input interf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AesKdfCtrInput_ikm_FromDafny(input interface{}) []byte {
@@ -542,12 +482,7 @@ func Aws_cryptography_primitives_AesKdfCtrInput_ikm_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AesKdfCtrInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -561,12 +496,7 @@ func Aws_cryptography_primitives_AesKdfCtrInput_nonce_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AesKdfCtrOutput_okm_FromDafny(input interface{}) []byte {
@@ -574,12 +504,7 @@ func Aws_cryptography_primitives_AesKdfCtrOutput_okm_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_CompressPublicKeyInput_publicKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey {
@@ -590,12 +515,7 @@ func Aws_cryptography_primitives_ECCPublicKey_der_FromDafny(input interface{}) [
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_CompressPublicKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -621,12 +541,7 @@ func Aws_cryptography_primitives_CompressPublicKeyOutput_compressedPublicKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DecompressPublicKeyInput_compressedPublicKey_FromDafny(input interface{}) []byte {
@@ -634,12 +549,7 @@ func Aws_cryptography_primitives_DecompressPublicKeyInput_compressedPublicKey_Fr
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DecompressPublicKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -689,12 +599,7 @@ func Aws_cryptography_primitives_ECCPrivateKey_pem_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DeriveSharedSecretInput_publicKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey {
@@ -705,12 +610,7 @@ func Aws_cryptography_primitives_DeriveSharedSecretOutput_sharedSecret_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DigestInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -736,12 +636,7 @@ func Aws_cryptography_primitives_DigestInput_message_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DigestOutput_digest_FromDafny(input interface{}) []byte {
@@ -749,12 +644,7 @@ func Aws_cryptography_primitives_DigestOutput_digest_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSASignInput_signatureAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDSASignatureAlgorithm {
@@ -780,12 +670,7 @@ func Aws_cryptography_primitives_ECDSASignInput_signingKey_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSASignInput_message_FromDafny(input interface{}) []byte {
@@ -793,12 +678,7 @@ func Aws_cryptography_primitives_ECDSASignInput_message_FromDafny(input interfac
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSASignOutput_signature_FromDafny(input interface{}) []byte {
@@ -806,12 +686,7 @@ func Aws_cryptography_primitives_ECDSASignOutput_signature_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyInput_signatureAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDSASignatureAlgorithm {
@@ -837,12 +712,7 @@ func Aws_cryptography_primitives_ECDSAVerifyInput_verificationKey_FromDafny(inpu
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyInput_message_FromDafny(input interface{}) []byte {
@@ -850,12 +720,7 @@ func Aws_cryptography_primitives_ECDSAVerifyInput_message_FromDafny(input interf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyInput_signature_FromDafny(input interface{}) []byte {
@@ -863,12 +728,7 @@ func Aws_cryptography_primitives_ECDSAVerifyInput_signature_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyOutput_success_FromDafny(input interface{}) bool {
@@ -957,12 +817,7 @@ func Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_verificationKey
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_signingKey_FromDafny(input interface{}) []byte {
@@ -970,12 +825,7 @@ func Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_signingKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateRandomBytesInput_length_FromDafny(input interface{}) int32 {
@@ -989,12 +839,7 @@ func Aws_cryptography_primitives_GenerateRandomBytesOutput_data_FromDafny(input
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateRSAKeyPairInput_lengthBits_FromDafny(input interface{}) int32 {
@@ -1019,12 +864,7 @@ func Aws_cryptography_primitives_RSAPublicKey_pem_FromDafny(input interface{}) [
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateRSAKeyPairOutput_privateKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.RSAPrivateKey {
@@ -1043,12 +883,7 @@ func Aws_cryptography_primitives_RSAPrivateKey_pem_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1098,12 +933,7 @@ func Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyOutput_publicKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GetRSAKeyModulusLengthInput_publicKey_FromDafny(input interface{}) []byte {
@@ -1111,12 +941,7 @@ func Aws_cryptography_primitives_GetRSAKeyModulusLengthInput_publicKey_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GetRSAKeyModulusLengthOutput_length_FromDafny(input interface{}) int32 {
@@ -1148,12 +973,7 @@ func Aws_cryptography_primitives_HkdfInput_salt_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfInput_ikm_FromDafny(input interface{}) []byte {
@@ -1161,12 +981,7 @@ func Aws_cryptography_primitives_HkdfInput_ikm_FromDafny(input interface{}) []by
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfInput_info_FromDafny(input interface{}) []byte {
@@ -1174,12 +989,7 @@ func Aws_cryptography_primitives_HkdfInput_info_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -1193,12 +1003,7 @@ func Aws_cryptography_primitives_HkdfOutput_okm_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExpandInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1224,12 +1029,7 @@ func Aws_cryptography_primitives_HkdfExpandInput_prk_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExpandInput_info_FromDafny(input interface{}) []byte {
@@ -1237,12 +1037,7 @@ func Aws_cryptography_primitives_HkdfExpandInput_info_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExpandInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -1256,12 +1051,7 @@ func Aws_cryptography_primitives_HkdfExpandOutput_okm_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExtractInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1287,12 +1077,7 @@ func Aws_cryptography_primitives_HkdfExtractInput_salt_FromDafny(input interface
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExtractInput_ikm_FromDafny(input interface{}) []byte {
@@ -1300,12 +1085,7 @@ func Aws_cryptography_primitives_HkdfExtractInput_ikm_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExtractOutput_prk_FromDafny(input interface{}) []byte {
@@ -1313,12 +1093,7 @@ func Aws_cryptography_primitives_HkdfExtractOutput_prk_FromDafny(input interface
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HMacInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1344,12 +1119,7 @@ func Aws_cryptography_primitives_HMacInput_key_FromDafny(input interface{}) []by
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HMacInput_message_FromDafny(input interface{}) []byte {
@@ -1357,12 +1127,7 @@ func Aws_cryptography_primitives_HMacInput_message_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HMacOutput_digest_FromDafny(input interface{}) []byte {
@@ -1370,12 +1135,7 @@ func Aws_cryptography_primitives_HMacOutput_digest_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1401,12 +1161,7 @@ func Aws_cryptography_primitives_KdfCtrInput_ikm_FromDafny(input interface{}) []
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -1420,12 +1175,7 @@ func Aws_cryptography_primitives_KdfCtrInput_purpose_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrInput_nonce_FromDafny(input interface{}) []byte {
@@ -1433,12 +1183,7 @@ func Aws_cryptography_primitives_KdfCtrInput_nonce_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrOutput_okm_FromDafny(input interface{}) []byte {
@@ -1446,12 +1191,7 @@ func Aws_cryptography_primitives_KdfCtrOutput_okm_FromDafny(input interface{}) [
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ParsePublicKeyInput_publicKey_FromDafny(input interface{}) []byte {
@@ -1459,12 +1199,7 @@ func Aws_cryptography_primitives_ParsePublicKeyInput_publicKey_FromDafny(input i
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ParsePublicKeyOutput_publicKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey {
@@ -1493,12 +1228,7 @@ func Aws_cryptography_primitives_RSADecryptInput_privateKey_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSADecryptInput_cipherText_FromDafny(input interface{}) []byte {
@@ -1506,12 +1236,7 @@ func Aws_cryptography_primitives_RSADecryptInput_cipherText_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSADecryptOutput_plaintext_FromDafny(input interface{}) []byte {
@@ -1519,12 +1244,7 @@ func Aws_cryptography_primitives_RSADecryptOutput_plaintext_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSAEncryptInput_padding_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.RSAPaddingMode {
@@ -1550,12 +1270,7 @@ func Aws_cryptography_primitives_RSAEncryptInput_publicKey_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSAEncryptInput_plaintext_FromDafny(input interface{}) []byte {
@@ -1563,12 +1278,7 @@ func Aws_cryptography_primitives_RSAEncryptInput_plaintext_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSAEncryptOutput_cipherText_FromDafny(input interface{}) []byte {
@@ -1576,12 +1286,7 @@ func Aws_cryptography_primitives_RSAEncryptOutput_cipherText_FromDafny(input int
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ValidatePublicKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1607,12 +1312,7 @@ func Aws_cryptography_primitives_ValidatePublicKeyInput_publicKey_FromDafny(inpu
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ValidatePublicKeyOutput_success_FromDafny(input interface{}) bool {
diff --git a/AwsCryptographyPrimitives/runtimes/go/TestsFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go b/AwsCryptographyPrimitives/runtimes/go/TestsFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go
index 7bc7d231b5..ec894cacb2 100644
--- a/AwsCryptographyPrimitives/runtimes/go/TestsFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go
+++ b/AwsCryptographyPrimitives/runtimes/go/TestsFromDafny-go/awscryptographyprimitivessmithygenerated/to_native.go
@@ -380,12 +380,7 @@ func Aws_cryptography_primitives_AESDecryptInput_key_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_cipherTxt_FromDafny(input interface{}) []byte {
@@ -393,12 +388,7 @@ func Aws_cryptography_primitives_AESDecryptInput_cipherTxt_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_authTag_FromDafny(input interface{}) []byte {
@@ -406,12 +396,7 @@ func Aws_cryptography_primitives_AESDecryptInput_authTag_FromDafny(input interfa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_iv_FromDafny(input interface{}) []byte {
@@ -419,12 +404,7 @@ func Aws_cryptography_primitives_AESDecryptInput_iv_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptInput_aad_FromDafny(input interface{}) []byte {
@@ -432,12 +412,7 @@ func Aws_cryptography_primitives_AESDecryptInput_aad_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESDecryptOutput_plaintext_FromDafny(input interface{}) []byte {
@@ -445,12 +420,7 @@ func Aws_cryptography_primitives_AESDecryptOutput_plaintext_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_encAlg_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.AES_GCM {
@@ -464,12 +434,7 @@ func Aws_cryptography_primitives_AESEncryptInput_iv_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_key_FromDafny(input interface{}) []byte {
@@ -477,12 +442,7 @@ func Aws_cryptography_primitives_AESEncryptInput_key_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_msg_FromDafny(input interface{}) []byte {
@@ -490,12 +450,7 @@ func Aws_cryptography_primitives_AESEncryptInput_msg_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptInput_aad_FromDafny(input interface{}) []byte {
@@ -503,12 +458,7 @@ func Aws_cryptography_primitives_AESEncryptInput_aad_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptOutput_cipherText_FromDafny(input interface{}) []byte {
@@ -516,12 +466,7 @@ func Aws_cryptography_primitives_AESEncryptOutput_cipherText_FromDafny(input int
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AESEncryptOutput_authTag_FromDafny(input interface{}) []byte {
@@ -529,12 +474,7 @@ func Aws_cryptography_primitives_AESEncryptOutput_authTag_FromDafny(input interf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AesKdfCtrInput_ikm_FromDafny(input interface{}) []byte {
@@ -542,12 +482,7 @@ func Aws_cryptography_primitives_AesKdfCtrInput_ikm_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AesKdfCtrInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -561,12 +496,7 @@ func Aws_cryptography_primitives_AesKdfCtrInput_nonce_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_AesKdfCtrOutput_okm_FromDafny(input interface{}) []byte {
@@ -574,12 +504,7 @@ func Aws_cryptography_primitives_AesKdfCtrOutput_okm_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_CompressPublicKeyInput_publicKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey {
@@ -590,12 +515,7 @@ func Aws_cryptography_primitives_ECCPublicKey_der_FromDafny(input interface{}) [
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_CompressPublicKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -621,12 +541,7 @@ func Aws_cryptography_primitives_CompressPublicKeyOutput_compressedPublicKey_Fro
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DecompressPublicKeyInput_compressedPublicKey_FromDafny(input interface{}) []byte {
@@ -634,12 +549,7 @@ func Aws_cryptography_primitives_DecompressPublicKeyInput_compressedPublicKey_Fr
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DecompressPublicKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -689,12 +599,7 @@ func Aws_cryptography_primitives_ECCPrivateKey_pem_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DeriveSharedSecretInput_publicKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey {
@@ -705,12 +610,7 @@ func Aws_cryptography_primitives_DeriveSharedSecretOutput_sharedSecret_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DigestInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -736,12 +636,7 @@ func Aws_cryptography_primitives_DigestInput_message_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_DigestOutput_digest_FromDafny(input interface{}) []byte {
@@ -749,12 +644,7 @@ func Aws_cryptography_primitives_DigestOutput_digest_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSASignInput_signatureAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDSASignatureAlgorithm {
@@ -780,12 +670,7 @@ func Aws_cryptography_primitives_ECDSASignInput_signingKey_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSASignInput_message_FromDafny(input interface{}) []byte {
@@ -793,12 +678,7 @@ func Aws_cryptography_primitives_ECDSASignInput_message_FromDafny(input interfac
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSASignOutput_signature_FromDafny(input interface{}) []byte {
@@ -806,12 +686,7 @@ func Aws_cryptography_primitives_ECDSASignOutput_signature_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyInput_signatureAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDSASignatureAlgorithm {
@@ -837,12 +712,7 @@ func Aws_cryptography_primitives_ECDSAVerifyInput_verificationKey_FromDafny(inpu
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyInput_message_FromDafny(input interface{}) []byte {
@@ -850,12 +720,7 @@ func Aws_cryptography_primitives_ECDSAVerifyInput_message_FromDafny(input interf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyInput_signature_FromDafny(input interface{}) []byte {
@@ -863,12 +728,7 @@ func Aws_cryptography_primitives_ECDSAVerifyInput_signature_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ECDSAVerifyOutput_success_FromDafny(input interface{}) bool {
@@ -957,12 +817,7 @@ func Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_verificationKey
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_signingKey_FromDafny(input interface{}) []byte {
@@ -970,12 +825,7 @@ func Aws_cryptography_primitives_GenerateECDSASignatureKeyOutput_signingKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateRandomBytesInput_length_FromDafny(input interface{}) int32 {
@@ -989,12 +839,7 @@ func Aws_cryptography_primitives_GenerateRandomBytesOutput_data_FromDafny(input
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateRSAKeyPairInput_lengthBits_FromDafny(input interface{}) int32 {
@@ -1019,12 +864,7 @@ func Aws_cryptography_primitives_RSAPublicKey_pem_FromDafny(input interface{}) [
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GenerateRSAKeyPairOutput_privateKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.RSAPrivateKey {
@@ -1043,12 +883,7 @@ func Aws_cryptography_primitives_RSAPrivateKey_pem_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1098,12 +933,7 @@ func Aws_cryptography_primitives_GetPublicKeyFromPrivateKeyOutput_publicKey_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GetRSAKeyModulusLengthInput_publicKey_FromDafny(input interface{}) []byte {
@@ -1111,12 +941,7 @@ func Aws_cryptography_primitives_GetRSAKeyModulusLengthInput_publicKey_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_GetRSAKeyModulusLengthOutput_length_FromDafny(input interface{}) int32 {
@@ -1148,12 +973,7 @@ func Aws_cryptography_primitives_HkdfInput_salt_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfInput_ikm_FromDafny(input interface{}) []byte {
@@ -1161,12 +981,7 @@ func Aws_cryptography_primitives_HkdfInput_ikm_FromDafny(input interface{}) []by
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfInput_info_FromDafny(input interface{}) []byte {
@@ -1174,12 +989,7 @@ func Aws_cryptography_primitives_HkdfInput_info_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -1193,12 +1003,7 @@ func Aws_cryptography_primitives_HkdfOutput_okm_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExpandInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1224,12 +1029,7 @@ func Aws_cryptography_primitives_HkdfExpandInput_prk_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExpandInput_info_FromDafny(input interface{}) []byte {
@@ -1237,12 +1037,7 @@ func Aws_cryptography_primitives_HkdfExpandInput_info_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExpandInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -1256,12 +1051,7 @@ func Aws_cryptography_primitives_HkdfExpandOutput_okm_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExtractInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1287,12 +1077,7 @@ func Aws_cryptography_primitives_HkdfExtractInput_salt_FromDafny(input interface
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExtractInput_ikm_FromDafny(input interface{}) []byte {
@@ -1300,12 +1085,7 @@ func Aws_cryptography_primitives_HkdfExtractInput_ikm_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HkdfExtractOutput_prk_FromDafny(input interface{}) []byte {
@@ -1313,12 +1093,7 @@ func Aws_cryptography_primitives_HkdfExtractOutput_prk_FromDafny(input interface
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HMacInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1344,12 +1119,7 @@ func Aws_cryptography_primitives_HMacInput_key_FromDafny(input interface{}) []by
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HMacInput_message_FromDafny(input interface{}) []byte {
@@ -1357,12 +1127,7 @@ func Aws_cryptography_primitives_HMacInput_message_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_HMacOutput_digest_FromDafny(input interface{}) []byte {
@@ -1370,12 +1135,7 @@ func Aws_cryptography_primitives_HMacOutput_digest_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrInput_digestAlgorithm_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.DigestAlgorithm {
@@ -1401,12 +1161,7 @@ func Aws_cryptography_primitives_KdfCtrInput_ikm_FromDafny(input interface{}) []
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrInput_expectedLength_FromDafny(input interface{}) int32 {
@@ -1420,12 +1175,7 @@ func Aws_cryptography_primitives_KdfCtrInput_purpose_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrInput_nonce_FromDafny(input interface{}) []byte {
@@ -1433,12 +1183,7 @@ func Aws_cryptography_primitives_KdfCtrInput_nonce_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_KdfCtrOutput_okm_FromDafny(input interface{}) []byte {
@@ -1446,12 +1191,7 @@ func Aws_cryptography_primitives_KdfCtrOutput_okm_FromDafny(input interface{}) [
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ParsePublicKeyInput_publicKey_FromDafny(input interface{}) []byte {
@@ -1459,12 +1199,7 @@ func Aws_cryptography_primitives_ParsePublicKeyInput_publicKey_FromDafny(input i
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ParsePublicKeyOutput_publicKey_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECCPublicKey {
@@ -1493,12 +1228,7 @@ func Aws_cryptography_primitives_RSADecryptInput_privateKey_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSADecryptInput_cipherText_FromDafny(input interface{}) []byte {
@@ -1506,12 +1236,7 @@ func Aws_cryptography_primitives_RSADecryptInput_cipherText_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSADecryptOutput_plaintext_FromDafny(input interface{}) []byte {
@@ -1519,12 +1244,7 @@ func Aws_cryptography_primitives_RSADecryptOutput_plaintext_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSAEncryptInput_padding_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.RSAPaddingMode {
@@ -1550,12 +1270,7 @@ func Aws_cryptography_primitives_RSAEncryptInput_publicKey_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSAEncryptInput_plaintext_FromDafny(input interface{}) []byte {
@@ -1563,12 +1278,7 @@ func Aws_cryptography_primitives_RSAEncryptInput_plaintext_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_RSAEncryptOutput_cipherText_FromDafny(input interface{}) []byte {
@@ -1576,12 +1286,7 @@ func Aws_cryptography_primitives_RSAEncryptOutput_cipherText_FromDafny(input int
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ValidatePublicKeyInput_eccCurve_FromDafny(input interface{}) awscryptographyprimitivessmithygeneratedtypes.ECDHCurveSpec {
@@ -1607,12 +1312,7 @@ func Aws_cryptography_primitives_ValidatePublicKeyInput_publicKey_FromDafny(inpu
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_primitives_ValidatePublicKeyOutput_success_FromDafny(input interface{}) bool {
diff --git a/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go b/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go
index c250ed82ac..a87741d1a4 100644
--- a/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go
+++ b/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go
@@ -1586,14 +1586,10 @@ func Com_amazonaws_dynamodb_AttributeValue_N_ToDafny(input string) Wrappers.Opti
 
 func Com_amazonaws_dynamodb_AttributeValue_B_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -1667,14 +1663,10 @@ func Com_amazonaws_dynamodb_AttributeValue_BS_ToDafny(input [][]byte) Wrappers.O
 
 func Com_amazonaws_dynamodb_BinarySetAttributeValue_member_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
diff --git a/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go b/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go
index 971c510f59..9a00147ea7 100644
--- a/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go
+++ b/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go
@@ -2139,12 +2139,7 @@ func Com_amazonaws_dynamodb_AttributeValue_B_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_dynamodb_AttributeValue_SS_FromDafny(input interface{}) []string {
@@ -2216,12 +2211,7 @@ func Com_amazonaws_dynamodb_BinarySetAttributeValue_member_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_dynamodb_AttributeValue_M_FromDafny(input interface{}) map[string]types.AttributeValue {
diff --git a/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go b/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go
index c250ed82ac..a87741d1a4 100644
--- a/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go
+++ b/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_dafny.go
@@ -1586,14 +1586,10 @@ func Com_amazonaws_dynamodb_AttributeValue_N_ToDafny(input string) Wrappers.Opti
 
 func Com_amazonaws_dynamodb_AttributeValue_B_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -1667,14 +1663,10 @@ func Com_amazonaws_dynamodb_AttributeValue_BS_ToDafny(input [][]byte) Wrappers.O
 
 func Com_amazonaws_dynamodb_BinarySetAttributeValue_member_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
diff --git a/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go b/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go
index 971c510f59..9a00147ea7 100644
--- a/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go
+++ b/ComAmazonawsDynamodb/runtimes/go/TestsFromDafny-go/comamazonawsdynamodbsmithygenerated/to_native.go
@@ -2139,12 +2139,7 @@ func Com_amazonaws_dynamodb_AttributeValue_B_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_dynamodb_AttributeValue_SS_FromDafny(input interface{}) []string {
@@ -2216,12 +2211,7 @@ func Com_amazonaws_dynamodb_BinarySetAttributeValue_member_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_dynamodb_AttributeValue_M_FromDafny(input interface{}) map[string]types.AttributeValue {
diff --git a/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go b/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go
index 2b6f83e896..909666c4f7 100644
--- a/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go
+++ b/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go
@@ -2814,14 +2814,10 @@ func Com_amazonaws_kms_XksKeyConfigurationType_Id_ToDafny(input *string) Wrapper
 
 func Com_amazonaws_kms_DecryptRequest_CiphertextBlob_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -2928,14 +2924,10 @@ func Com_amazonaws_kms_RecipientInfo_KeyEncryptionAlgorithm_ToDafny(input types.
 
 func Com_amazonaws_kms_RecipientInfo_AttestationDocument_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -2965,14 +2957,10 @@ func Com_amazonaws_kms_DecryptResponse_KeyId_ToDafny(input *string) Wrappers.Opt
 
 func Com_amazonaws_kms_DecryptResponse_Plaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3003,14 +2991,10 @@ func Com_amazonaws_kms_DecryptResponse_EncryptionAlgorithm_ToDafny(input types.E
 
 func Com_amazonaws_kms_DecryptResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3101,14 +3085,10 @@ func Com_amazonaws_kms_DeriveSharedSecretRequest_KeyAgreementAlgorithm_ToDafny(i
 
 func Com_amazonaws_kms_DeriveSharedSecretRequest_PublicKey_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -3161,27 +3141,19 @@ func Com_amazonaws_kms_DeriveSharedSecretResponse_KeyId_ToDafny(input *string) W
 
 func Com_amazonaws_kms_DeriveSharedSecretResponse_SharedSecret_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_DeriveSharedSecretResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3716,14 +3688,10 @@ func Com_amazonaws_kms_EncryptRequest_KeyId_ToDafny(input *string) dafny.Sequenc
 
 func Com_amazonaws_kms_EncryptRequest_Plaintext_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -3790,14 +3758,10 @@ func Com_amazonaws_kms_EncryptRequest_DryRun_ToDafny(input *bool) Wrappers.Optio
 
 func Com_amazonaws_kms_EncryptResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3937,27 +3901,19 @@ func Com_amazonaws_kms_GenerateDataKeyRequest_DryRun_ToDafny(input *bool) Wrappe
 
 func Com_amazonaws_kms_GenerateDataKeyResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyResponse_Plaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3978,14 +3934,10 @@ func Com_amazonaws_kms_GenerateDataKeyResponse_KeyId_ToDafny(input *string) Wrap
 
 func Com_amazonaws_kms_GenerateDataKeyResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4076,40 +4028,28 @@ func Com_amazonaws_kms_GenerateDataKeyPairRequest_DryRun_ToDafny(input *bool) Wr
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_PrivateKeyCiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_PrivateKeyPlaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4155,14 +4095,10 @@ func Com_amazonaws_kms_GenerateDataKeyPairResponse_KeyPairSpec_ToDafny(input typ
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4244,27 +4180,19 @@ func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextRequest_DryRun_ToDafny
 
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextResponse_PrivateKeyCiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4395,14 +4323,10 @@ func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextRequest_DryRun_ToDafny(inp
 
 func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4423,14 +4347,10 @@ func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextResponse_KeyId_ToDafny(inp
 
 func Com_amazonaws_kms_GenerateMacRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -4499,14 +4419,10 @@ func Com_amazonaws_kms_GenerateMacRequest_DryRun_ToDafny(input *bool) Wrappers.O
 
 func Com_amazonaws_kms_GenerateMacResponse_Mac_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4585,27 +4501,19 @@ func Com_amazonaws_kms_GenerateRandomRequest_Recipient_ToDafny(input *types.Reci
 
 func Com_amazonaws_kms_GenerateRandomResponse_Plaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateRandomResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4829,27 +4737,19 @@ func Com_amazonaws_kms_GetParametersForImportResponse_KeyId_ToDafny(input *strin
 
 func Com_amazonaws_kms_GetParametersForImportResponse_ImportToken_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GetParametersForImportResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4915,14 +4815,10 @@ func Com_amazonaws_kms_GetPublicKeyResponse_KeyId_ToDafny(input *string) Wrapper
 
 func Com_amazonaws_kms_GetPublicKeyResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -5060,27 +4956,19 @@ func Com_amazonaws_kms_ImportKeyMaterialRequest_KeyId_ToDafny(input *string) daf
 
 func Com_amazonaws_kms_ImportKeyMaterialRequest_ImportToken_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
 func Com_amazonaws_kms_ImportKeyMaterialRequest_EncryptedKeyMaterial_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -5977,14 +5865,10 @@ func Com_amazonaws_kms_PutKeyPolicyRequest_BypassPolicyLockoutSafetyCheck_ToDafn
 
 func Com_amazonaws_kms_ReEncryptRequest_CiphertextBlob_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -6119,14 +6003,10 @@ func Com_amazonaws_kms_ReEncryptRequest_DryRun_ToDafny(input *bool) Wrappers.Opt
 
 func Com_amazonaws_kms_ReEncryptResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -6558,14 +6438,10 @@ func Com_amazonaws_kms_SignRequest_KeyId_ToDafny(input *string) dafny.Sequence {
 
 func Com_amazonaws_kms_SignRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -6659,14 +6535,10 @@ func Com_amazonaws_kms_SignResponse_KeyId_ToDafny(input *string) Wrappers.Option
 
 func Com_amazonaws_kms_SignResponse_Signature_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -7012,14 +6884,10 @@ func Com_amazonaws_kms_VerifyRequest_KeyId_ToDafny(input *string) dafny.Sequence
 
 func Com_amazonaws_kms_VerifyRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -7050,14 +6918,10 @@ func Com_amazonaws_kms_VerifyRequest_MessageType_ToDafny(input types.MessageType
 
 func Com_amazonaws_kms_VerifyRequest_Signature_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -7158,14 +7022,10 @@ func Com_amazonaws_kms_VerifyResponse_SigningAlgorithm_ToDafny(input types.Signi
 
 func Com_amazonaws_kms_VerifyMacRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -7211,14 +7071,10 @@ func Com_amazonaws_kms_VerifyMacRequest_MacAlgorithm_ToDafny(input types.MacAlgo
 
 func Com_amazonaws_kms_VerifyMacRequest_Mac_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
diff --git a/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_native.go b/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_native.go
index e8bcb00496..066a9eae95 100644
--- a/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_native.go
+++ b/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/comamazonawskmssmithygenerated/to_native.go
@@ -3066,12 +3066,7 @@ func Com_amazonaws_kms_DecryptInput_CiphertextBlob_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DecryptInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -3175,12 +3170,7 @@ func Com_amazonaws_kms_RecipientInfo_AttestationDocument_FromDafny(input interfa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DecryptInput_DryRun_FromDafny(input interface{}) *bool {
@@ -3208,12 +3198,7 @@ func Com_amazonaws_kms_DecryptOutput_Plaintext_FromDafny(input interface{}) []by
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DecryptOutput_EncryptionAlgorithm_FromDafny(input interface{}) types.EncryptionAlgorithmSpec {
@@ -3242,12 +3227,7 @@ func Com_amazonaws_kms_DecryptOutput_CiphertextForRecipient_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeleteAliasInput_AliasName_FromDafny(input interface{}) *string {
@@ -3305,12 +3285,7 @@ func Com_amazonaws_kms_DeriveSharedSecretInput_PublicKey_FromDafny(input interfa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeriveSharedSecretInput_GrantTokens_FromDafny(input interface{}) []string {
@@ -3365,12 +3340,7 @@ func Com_amazonaws_kms_DeriveSharedSecretOutput_SharedSecret_FromDafny(input int
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeriveSharedSecretOutput_CiphertextForRecipient_FromDafny(input interface{}) []byte {
@@ -3378,12 +3348,7 @@ func Com_amazonaws_kms_DeriveSharedSecretOutput_CiphertextForRecipient_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeriveSharedSecretOutput_KeyAgreementAlgorithm_FromDafny(input interface{}) types.KeyAgreementAlgorithmSpec {
@@ -3837,12 +3802,7 @@ func Com_amazonaws_kms_EncryptInput_Plaintext_FromDafny(input interface{}) []byt
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_EncryptInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -3914,12 +3874,7 @@ func Com_amazonaws_kms_EncryptOutput_CiphertextBlob_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_EncryptOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4051,12 +4006,7 @@ func Com_amazonaws_kms_GenerateDataKeyOutput_CiphertextBlob_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyOutput_Plaintext_FromDafny(input interface{}) []byte {
@@ -4064,12 +4014,7 @@ func Com_amazonaws_kms_GenerateDataKeyOutput_Plaintext_FromDafny(input interface
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4087,12 +4032,7 @@ func Com_amazonaws_kms_GenerateDataKeyOutput_CiphertextForRecipient_FromDafny(in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -4180,12 +4120,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_PrivateKeyCiphertextBlob_FromDa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairOutput_PrivateKeyPlaintext_FromDafny(input interface{}) []byte {
@@ -4193,12 +4128,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_PrivateKeyPlaintext_FromDafny(i
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairOutput_PublicKey_FromDafny(input interface{}) []byte {
@@ -4206,12 +4136,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_PublicKey_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4250,12 +4175,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_CiphertextForRecipient_FromDafn
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -4332,12 +4252,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_PrivateKeyCiphe
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_PublicKey_FromDafny(input interface{}) []byte {
@@ -4345,12 +4260,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_PublicKey_FromD
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4471,12 +4381,7 @@ func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextOutput_CiphertextBlob_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4494,12 +4399,7 @@ func Com_amazonaws_kms_GenerateMacInput_Message_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateMacInput_KeyId_FromDafny(input interface{}) *string {
@@ -4559,12 +4459,7 @@ func Com_amazonaws_kms_GenerateMacOutput_Mac_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateMacOutput_MacAlgorithm_FromDafny(input interface{}) types.MacAlgorithmSpec {
@@ -4634,12 +4529,7 @@ func Com_amazonaws_kms_GenerateRandomOutput_Plaintext_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateRandomOutput_CiphertextForRecipient_FromDafny(input interface{}) []byte {
@@ -4647,12 +4537,7 @@ func Com_amazonaws_kms_GenerateRandomOutput_CiphertextForRecipient_FromDafny(inp
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetKeyPolicyInput_KeyId_FromDafny(input interface{}) *string {
@@ -4826,12 +4711,7 @@ func Com_amazonaws_kms_GetParametersForImportOutput_ImportToken_FromDafny(input
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetParametersForImportOutput_PublicKey_FromDafny(input interface{}) []byte {
@@ -4839,12 +4719,7 @@ func Com_amazonaws_kms_GetParametersForImportOutput_PublicKey_FromDafny(input in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetParametersForImportOutput_ParametersValidTo_FromDafny(input interface{}) *time.Time {
@@ -4904,12 +4779,7 @@ func Com_amazonaws_kms_GetPublicKeyOutput_PublicKey_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetPublicKeyOutput_CustomerMasterKeySpec_FromDafny(input interface{}) types.CustomerMasterKeySpec {
@@ -5036,12 +4906,7 @@ func Com_amazonaws_kms_ImportKeyMaterialInput_ImportToken_FromDafny(input interf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ImportKeyMaterialInput_EncryptedKeyMaterial_FromDafny(input interface{}) []byte {
@@ -5049,12 +4914,7 @@ func Com_amazonaws_kms_ImportKeyMaterialInput_EncryptedKeyMaterial_FromDafny(inp
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ImportKeyMaterialInput_ValidTo_FromDafny(input interface{}) *time.Time {
@@ -5830,12 +5690,7 @@ func Com_amazonaws_kms_ReEncryptInput_CiphertextBlob_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ReEncryptInput_SourceEncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -5963,12 +5818,7 @@ func Com_amazonaws_kms_ReEncryptOutput_CiphertextBlob_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ReEncryptOutput_SourceKeyId_FromDafny(input interface{}) *string {
@@ -6329,12 +6179,7 @@ func Com_amazonaws_kms_SignInput_Message_FromDafny(input interface{}) []byte {
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_SignInput_MessageType_FromDafny(input interface{}) types.MessageType {
@@ -6417,12 +6262,7 @@ func Com_amazonaws_kms_SignOutput_Signature_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_SignOutput_SigningAlgorithm_FromDafny(input interface{}) types.SigningAlgorithmSpec {
@@ -6659,12 +6499,7 @@ func Com_amazonaws_kms_VerifyInput_Message_FromDafny(input interface{}) []byte {
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyInput_MessageType_FromDafny(input interface{}) types.MessageType {
@@ -6693,12 +6528,7 @@ func Com_amazonaws_kms_VerifyInput_Signature_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyInput_SigningAlgorithm_FromDafny(input interface{}) types.SigningAlgorithmSpec {
@@ -6791,12 +6621,7 @@ func Com_amazonaws_kms_VerifyMacInput_Message_FromDafny(input interface{}) []byt
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyMacInput_KeyId_FromDafny(input interface{}) *string {
@@ -6830,12 +6655,7 @@ func Com_amazonaws_kms_VerifyMacInput_Mac_FromDafny(input interface{}) []byte {
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyMacInput_GrantTokens_FromDafny(input interface{}) []string {
diff --git a/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go b/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go
index 2b6f83e896..909666c4f7 100644
--- a/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go
+++ b/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_dafny.go
@@ -2814,14 +2814,10 @@ func Com_amazonaws_kms_XksKeyConfigurationType_Id_ToDafny(input *string) Wrapper
 
 func Com_amazonaws_kms_DecryptRequest_CiphertextBlob_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -2928,14 +2924,10 @@ func Com_amazonaws_kms_RecipientInfo_KeyEncryptionAlgorithm_ToDafny(input types.
 
 func Com_amazonaws_kms_RecipientInfo_AttestationDocument_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -2965,14 +2957,10 @@ func Com_amazonaws_kms_DecryptResponse_KeyId_ToDafny(input *string) Wrappers.Opt
 
 func Com_amazonaws_kms_DecryptResponse_Plaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3003,14 +2991,10 @@ func Com_amazonaws_kms_DecryptResponse_EncryptionAlgorithm_ToDafny(input types.E
 
 func Com_amazonaws_kms_DecryptResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3101,14 +3085,10 @@ func Com_amazonaws_kms_DeriveSharedSecretRequest_KeyAgreementAlgorithm_ToDafny(i
 
 func Com_amazonaws_kms_DeriveSharedSecretRequest_PublicKey_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -3161,27 +3141,19 @@ func Com_amazonaws_kms_DeriveSharedSecretResponse_KeyId_ToDafny(input *string) W
 
 func Com_amazonaws_kms_DeriveSharedSecretResponse_SharedSecret_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_DeriveSharedSecretResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3716,14 +3688,10 @@ func Com_amazonaws_kms_EncryptRequest_KeyId_ToDafny(input *string) dafny.Sequenc
 
 func Com_amazonaws_kms_EncryptRequest_Plaintext_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -3790,14 +3758,10 @@ func Com_amazonaws_kms_EncryptRequest_DryRun_ToDafny(input *bool) Wrappers.Optio
 
 func Com_amazonaws_kms_EncryptResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3937,27 +3901,19 @@ func Com_amazonaws_kms_GenerateDataKeyRequest_DryRun_ToDafny(input *bool) Wrappe
 
 func Com_amazonaws_kms_GenerateDataKeyResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyResponse_Plaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -3978,14 +3934,10 @@ func Com_amazonaws_kms_GenerateDataKeyResponse_KeyId_ToDafny(input *string) Wrap
 
 func Com_amazonaws_kms_GenerateDataKeyResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4076,40 +4028,28 @@ func Com_amazonaws_kms_GenerateDataKeyPairRequest_DryRun_ToDafny(input *bool) Wr
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_PrivateKeyCiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_PrivateKeyPlaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4155,14 +4095,10 @@ func Com_amazonaws_kms_GenerateDataKeyPairResponse_KeyPairSpec_ToDafny(input typ
 
 func Com_amazonaws_kms_GenerateDataKeyPairResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4244,27 +4180,19 @@ func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextRequest_DryRun_ToDafny
 
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextResponse_PrivateKeyCiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4395,14 +4323,10 @@ func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextRequest_DryRun_ToDafny(inp
 
 func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4423,14 +4347,10 @@ func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextResponse_KeyId_ToDafny(inp
 
 func Com_amazonaws_kms_GenerateMacRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -4499,14 +4419,10 @@ func Com_amazonaws_kms_GenerateMacRequest_DryRun_ToDafny(input *bool) Wrappers.O
 
 func Com_amazonaws_kms_GenerateMacResponse_Mac_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4585,27 +4501,19 @@ func Com_amazonaws_kms_GenerateRandomRequest_Recipient_ToDafny(input *types.Reci
 
 func Com_amazonaws_kms_GenerateRandomResponse_Plaintext_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GenerateRandomResponse_CiphertextForRecipient_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4829,27 +4737,19 @@ func Com_amazonaws_kms_GetParametersForImportResponse_KeyId_ToDafny(input *strin
 
 func Com_amazonaws_kms_GetParametersForImportResponse_ImportToken_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
 func Com_amazonaws_kms_GetParametersForImportResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -4915,14 +4815,10 @@ func Com_amazonaws_kms_GetPublicKeyResponse_KeyId_ToDafny(input *string) Wrapper
 
 func Com_amazonaws_kms_GetPublicKeyResponse_PublicKey_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -5060,27 +4956,19 @@ func Com_amazonaws_kms_ImportKeyMaterialRequest_KeyId_ToDafny(input *string) daf
 
 func Com_amazonaws_kms_ImportKeyMaterialRequest_ImportToken_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
 func Com_amazonaws_kms_ImportKeyMaterialRequest_EncryptedKeyMaterial_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -5977,14 +5865,10 @@ func Com_amazonaws_kms_PutKeyPolicyRequest_BypassPolicyLockoutSafetyCheck_ToDafn
 
 func Com_amazonaws_kms_ReEncryptRequest_CiphertextBlob_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -6119,14 +6003,10 @@ func Com_amazonaws_kms_ReEncryptRequest_DryRun_ToDafny(input *bool) Wrappers.Opt
 
 func Com_amazonaws_kms_ReEncryptResponse_CiphertextBlob_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -6558,14 +6438,10 @@ func Com_amazonaws_kms_SignRequest_KeyId_ToDafny(input *string) dafny.Sequence {
 
 func Com_amazonaws_kms_SignRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -6659,14 +6535,10 @@ func Com_amazonaws_kms_SignResponse_KeyId_ToDafny(input *string) Wrappers.Option
 
 func Com_amazonaws_kms_SignResponse_Signature_ToDafny(input []byte) Wrappers.Option {
 	return func() Wrappers.Option {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return Wrappers.Companion_Option_.Create_None_()
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqFromArray(v, false))
+		return Wrappers.Companion_Option_.Create_Some_(dafny.SeqOfBytes(input))
 	}()
 }
 
@@ -7012,14 +6884,10 @@ func Com_amazonaws_kms_VerifyRequest_KeyId_ToDafny(input *string) dafny.Sequence
 
 func Com_amazonaws_kms_VerifyRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -7050,14 +6918,10 @@ func Com_amazonaws_kms_VerifyRequest_MessageType_ToDafny(input types.MessageType
 
 func Com_amazonaws_kms_VerifyRequest_Signature_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -7158,14 +7022,10 @@ func Com_amazonaws_kms_VerifyResponse_SigningAlgorithm_ToDafny(input types.Signi
 
 func Com_amazonaws_kms_VerifyMacRequest_Message_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
@@ -7211,14 +7071,10 @@ func Com_amazonaws_kms_VerifyMacRequest_MacAlgorithm_ToDafny(input types.MacAlgo
 
 func Com_amazonaws_kms_VerifyMacRequest_Mac_ToDafny(input []byte) dafny.Sequence {
 	return func() dafny.Sequence {
-		v := make([]interface{}, 0, len(input))
 		if input == nil {
 			return nil
 		}
-		for _, e := range input {
-			v = append(v, e)
-		}
-		return dafny.SeqFromArray(v, false)
+		return dafny.SeqOfBytes(input)
 	}()
 }
 
diff --git a/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_native.go b/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_native.go
index e8bcb00496..066a9eae95 100644
--- a/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_native.go
+++ b/ComAmazonawsKms/runtimes/go/TestsFromDafny-go/comamazonawskmssmithygenerated/to_native.go
@@ -3066,12 +3066,7 @@ func Com_amazonaws_kms_DecryptInput_CiphertextBlob_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DecryptInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -3175,12 +3170,7 @@ func Com_amazonaws_kms_RecipientInfo_AttestationDocument_FromDafny(input interfa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DecryptInput_DryRun_FromDafny(input interface{}) *bool {
@@ -3208,12 +3198,7 @@ func Com_amazonaws_kms_DecryptOutput_Plaintext_FromDafny(input interface{}) []by
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DecryptOutput_EncryptionAlgorithm_FromDafny(input interface{}) types.EncryptionAlgorithmSpec {
@@ -3242,12 +3227,7 @@ func Com_amazonaws_kms_DecryptOutput_CiphertextForRecipient_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeleteAliasInput_AliasName_FromDafny(input interface{}) *string {
@@ -3305,12 +3285,7 @@ func Com_amazonaws_kms_DeriveSharedSecretInput_PublicKey_FromDafny(input interfa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeriveSharedSecretInput_GrantTokens_FromDafny(input interface{}) []string {
@@ -3365,12 +3340,7 @@ func Com_amazonaws_kms_DeriveSharedSecretOutput_SharedSecret_FromDafny(input int
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeriveSharedSecretOutput_CiphertextForRecipient_FromDafny(input interface{}) []byte {
@@ -3378,12 +3348,7 @@ func Com_amazonaws_kms_DeriveSharedSecretOutput_CiphertextForRecipient_FromDafny
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_DeriveSharedSecretOutput_KeyAgreementAlgorithm_FromDafny(input interface{}) types.KeyAgreementAlgorithmSpec {
@@ -3837,12 +3802,7 @@ func Com_amazonaws_kms_EncryptInput_Plaintext_FromDafny(input interface{}) []byt
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_EncryptInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -3914,12 +3874,7 @@ func Com_amazonaws_kms_EncryptOutput_CiphertextBlob_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_EncryptOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4051,12 +4006,7 @@ func Com_amazonaws_kms_GenerateDataKeyOutput_CiphertextBlob_FromDafny(input inte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyOutput_Plaintext_FromDafny(input interface{}) []byte {
@@ -4064,12 +4014,7 @@ func Com_amazonaws_kms_GenerateDataKeyOutput_Plaintext_FromDafny(input interface
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4087,12 +4032,7 @@ func Com_amazonaws_kms_GenerateDataKeyOutput_CiphertextForRecipient_FromDafny(in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -4180,12 +4120,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_PrivateKeyCiphertextBlob_FromDa
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairOutput_PrivateKeyPlaintext_FromDafny(input interface{}) []byte {
@@ -4193,12 +4128,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_PrivateKeyPlaintext_FromDafny(i
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairOutput_PublicKey_FromDafny(input interface{}) []byte {
@@ -4206,12 +4136,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_PublicKey_FromDafny(input inter
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4250,12 +4175,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairOutput_CiphertextForRecipient_FromDafn
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextInput_EncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -4332,12 +4252,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_PrivateKeyCiphe
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_PublicKey_FromDafny(input interface{}) []byte {
@@ -4345,12 +4260,7 @@ func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_PublicKey_FromD
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyPairWithoutPlaintextOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4471,12 +4381,7 @@ func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextOutput_CiphertextBlob_From
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateDataKeyWithoutPlaintextOutput_KeyId_FromDafny(input interface{}) *string {
@@ -4494,12 +4399,7 @@ func Com_amazonaws_kms_GenerateMacInput_Message_FromDafny(input interface{}) []b
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateMacInput_KeyId_FromDafny(input interface{}) *string {
@@ -4559,12 +4459,7 @@ func Com_amazonaws_kms_GenerateMacOutput_Mac_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateMacOutput_MacAlgorithm_FromDafny(input interface{}) types.MacAlgorithmSpec {
@@ -4634,12 +4529,7 @@ func Com_amazonaws_kms_GenerateRandomOutput_Plaintext_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GenerateRandomOutput_CiphertextForRecipient_FromDafny(input interface{}) []byte {
@@ -4647,12 +4537,7 @@ func Com_amazonaws_kms_GenerateRandomOutput_CiphertextForRecipient_FromDafny(inp
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetKeyPolicyInput_KeyId_FromDafny(input interface{}) *string {
@@ -4826,12 +4711,7 @@ func Com_amazonaws_kms_GetParametersForImportOutput_ImportToken_FromDafny(input
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetParametersForImportOutput_PublicKey_FromDafny(input interface{}) []byte {
@@ -4839,12 +4719,7 @@ func Com_amazonaws_kms_GetParametersForImportOutput_PublicKey_FromDafny(input in
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetParametersForImportOutput_ParametersValidTo_FromDafny(input interface{}) *time.Time {
@@ -4904,12 +4779,7 @@ func Com_amazonaws_kms_GetPublicKeyOutput_PublicKey_FromDafny(input interface{})
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_GetPublicKeyOutput_CustomerMasterKeySpec_FromDafny(input interface{}) types.CustomerMasterKeySpec {
@@ -5036,12 +4906,7 @@ func Com_amazonaws_kms_ImportKeyMaterialInput_ImportToken_FromDafny(input interf
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ImportKeyMaterialInput_EncryptedKeyMaterial_FromDafny(input interface{}) []byte {
@@ -5049,12 +4914,7 @@ func Com_amazonaws_kms_ImportKeyMaterialInput_EncryptedKeyMaterial_FromDafny(inp
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ImportKeyMaterialInput_ValidTo_FromDafny(input interface{}) *time.Time {
@@ -5830,12 +5690,7 @@ func Com_amazonaws_kms_ReEncryptInput_CiphertextBlob_FromDafny(input interface{}
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ReEncryptInput_SourceEncryptionContext_FromDafny(input interface{}) map[string]string {
@@ -5963,12 +5818,7 @@ func Com_amazonaws_kms_ReEncryptOutput_CiphertextBlob_FromDafny(input interface{
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_ReEncryptOutput_SourceKeyId_FromDafny(input interface{}) *string {
@@ -6329,12 +6179,7 @@ func Com_amazonaws_kms_SignInput_Message_FromDafny(input interface{}) []byte {
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_SignInput_MessageType_FromDafny(input interface{}) types.MessageType {
@@ -6417,12 +6262,7 @@ func Com_amazonaws_kms_SignOutput_Signature_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence).(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_SignOutput_SigningAlgorithm_FromDafny(input interface{}) types.SigningAlgorithmSpec {
@@ -6659,12 +6499,7 @@ func Com_amazonaws_kms_VerifyInput_Message_FromDafny(input interface{}) []byte {
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyInput_MessageType_FromDafny(input interface{}) types.MessageType {
@@ -6693,12 +6528,7 @@ func Com_amazonaws_kms_VerifyInput_Signature_FromDafny(input interface{}) []byte
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyInput_SigningAlgorithm_FromDafny(input interface{}) types.SigningAlgorithmSpec {
@@ -6791,12 +6621,7 @@ func Com_amazonaws_kms_VerifyMacInput_Message_FromDafny(input interface{}) []byt
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyMacInput_KeyId_FromDafny(input interface{}) *string {
@@ -6830,12 +6655,7 @@ func Com_amazonaws_kms_VerifyMacInput_Mac_FromDafny(input interface{}) []byte {
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Com_amazonaws_kms_VerifyMacInput_GrantTokens_FromDafny(input interface{}) []string {
diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go b/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go
index 355ea9b522..83b38ba636 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go
+++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go
@@ -870,12 +870,7 @@ func Aws_cryptography_materialProvidersTestVectorKeys_GetKeyDescriptionInput_jso
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProvidersTestVectorKeys_GetKeyDescriptionOutput_keyDescription_FromDafny(input interface{}) awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription {
@@ -1041,12 +1036,7 @@ func Aws_cryptography_materialProvidersTestVectorKeys_SerializeKeyDescriptionOut
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProvidersTestVectorKeys_KeyVectorException_message_FromDafny(input interface{}) string {
diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go b/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go
index 355ea9b522..83b38ba636 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go
+++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/awscryptographymaterialproviderstestvectorkeyssmithygenerated/to_native.go
@@ -870,12 +870,7 @@ func Aws_cryptography_materialProvidersTestVectorKeys_GetKeyDescriptionInput_jso
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProvidersTestVectorKeys_GetKeyDescriptionOutput_keyDescription_FromDafny(input interface{}) awscryptographymaterialproviderstestvectorkeyssmithygeneratedtypes.KeyDescription {
@@ -1041,12 +1036,7 @@ func Aws_cryptography_materialProvidersTestVectorKeys_SerializeKeyDescriptionOut
 		if input == nil {
 			return nil
 		}
-		a := input.(dafny.Sequence).ToArray().(dafny.GoNativeArray)
-		b := make([]byte, 0, a.Length())
-		for i := uint32(0); i < a.Length(); i++ {
-			b = append(b, a.Select(i).(byte))
-		}
-		return b
+		return dafny.ToByteArray(input.(dafny.Sequence))
 	}()
 }
 func Aws_cryptography_materialProvidersTestVectorKeys_KeyVectorException_message_FromDafny(input interface{}) string {
diff --git a/smithy-dafny b/smithy-dafny
index 8ac2c09112..7683a61028 160000
--- a/smithy-dafny
+++ b/smithy-dafny
@@ -1 +1 @@
-Subproject commit 8ac2c09112187d7819088e8300d713a7ab3de83c
+Subproject commit 7683a6102832aef39bcfb517b2ec44c512767abf