diff --git a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go
index cc97aab3a9..0d502826c9 100644
--- a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go
+++ b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go
@@ -552,14 +552,10 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionInp
 
 func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionUnion_header_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))
 	}()
 }
 
diff --git a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go
index fb1a93d7c4..f50a53a598 100644
--- a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go
+++ b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go
@@ -251,27 +251,19 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_AuthItem_data_ToDafny
 
 func Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_value_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 Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_typeId_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)
 	}()
 }
 
@@ -809,14 +801,10 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInp
 
 func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInput_headerBytes_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/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go
index cc97aab3a9..0d502826c9 100644
--- a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go
+++ b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go
@@ -552,14 +552,10 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionInp
 
 func Aws_cryptography_dbEncryptionSdk_dynamoDb_GetEncryptedDataKeyDescriptionUnion_header_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))
 	}()
 }
 
diff --git a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go
index fb1a93d7c4..f50a53a598 100644
--- a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go
+++ b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkstructuredencryptionsmithygenerated/to_dafny.go
@@ -251,27 +251,19 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_AuthItem_data_ToDafny
 
 func Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_value_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 Aws_cryptography_dbEncryptionSdk_structuredEncryption_StructuredDataTerminal_typeId_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)
 	}()
 }
 
@@ -809,14 +801,10 @@ func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInp
 
 func Aws_cryptography_dbEncryptionSdk_structuredEncryption_ResolveAuthActionsInput_headerBytes_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/submodules/MaterialProviders b/submodules/MaterialProviders
index f6bdd23d4e..dc1678ab78 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit f6bdd23d4ef83e3513554abb41d0ddbd3d89e8b8
+Subproject commit dc1678ab78948bee223f029df36b9f5d2cb0276d
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
index b60ee9f53a..8ac2c09112 160000
--- a/submodules/smithy-dafny
+++ b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit b60ee9f53a997838ba02510de40c609b17a3a728
+Subproject commit 8ac2c09112187d7819088e8300d713a7ab3de83c