diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
index 705de566c..23c2e2b16 100644
--- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
+++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
@@ -159,14 +159,10 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith
 
 func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_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)
 	}()
 }
 
@@ -182,14 +178,10 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input
 
 func Aws_cryptography_encryptionSdk_DecryptOutput_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)
 	}()
 }
 
@@ -231,14 +223,10 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input
 
 func Aws_cryptography_encryptionSdk_EncryptInput_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)
 	}()
 }
 
@@ -288,14 +276,10 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(input *int6
 
 func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_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/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
index 705de566c..23c2e2b16 100644
--- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
+++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
@@ -159,14 +159,10 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith
 
 func Aws_cryptography_encryptionSdk_DecryptInput_ciphertext_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)
 	}()
 }
 
@@ -182,14 +178,10 @@ func Aws_cryptography_encryptionSdk_DecryptInput_encryptionContext_ToDafny(input
 
 func Aws_cryptography_encryptionSdk_DecryptOutput_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)
 	}()
 }
 
@@ -231,14 +223,10 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input
 
 func Aws_cryptography_encryptionSdk_EncryptInput_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)
 	}()
 }
 
@@ -288,14 +276,10 @@ func Aws_cryptography_encryptionSdk_EncryptInput_frameLength_ToDafny(input *int6
 
 func Aws_cryptography_encryptionSdk_EncryptOutput_ciphertext_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/mpl b/mpl
index f6bdd23d4..dc1678ab7 160000
--- a/mpl
+++ b/mpl
@@ -1 +1 @@
-Subproject commit f6bdd23d4ef83e3513554abb41d0ddbd3d89e8b8
+Subproject commit dc1678ab78948bee223f029df36b9f5d2cb0276d