diff --git a/AwsEncryptionSDK/project.properties b/AwsEncryptionSDK/project.properties
new file mode 100644
index 000000000..55d988fe1
--- /dev/null
+++ b/AwsEncryptionSDK/project.properties
@@ -0,0 +1,4 @@
+# This file stores the top level dafny version information.
+# All elements of the project need to agree on this version.
+dafnyVersion=4.9.0
+dafnyRuntimeJavaVersion=4.9.0
diff --git a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
index 1328f1cc6..2be2a1ce7 100644
--- a/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
+++ b/AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
@@ -139,6 +139,10 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith
 			if enumVal == nativeInput {
 				break
 			}
+			if index == len(nativeInput.Values()) {
+				panic("Input value did not found in enum values")
+			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -208,6 +212,10 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input
 			if enumVal == input {
 				break
 			}
+			if index == len(input.Values()) {
+				panic("Input value did not found in enum values")
+			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -255,6 +263,7 @@ func Aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input
 			if enumVal == *input {
 				break
 			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -309,6 +318,10 @@ func Aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input
 			if enumVal == input {
 				break
 			}
+			if index == len(input.Values()) {
+				panic("Input value did not found in enum values")
+			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -346,6 +359,7 @@ func Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDa
 			if enumVal == *input {
 				break
 			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -379,6 +393,7 @@ func Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy
 			if enumVal == *input {
 				break
 			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
diff --git a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
index 1328f1cc6..2be2a1ce7 100644
--- a/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
+++ b/AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated/to_dafny.go
@@ -139,6 +139,10 @@ func NetV4_0_0_RetryPolicy_ToDafny(nativeInput awscryptographyencryptionsdksmith
 			if enumVal == nativeInput {
 				break
 			}
+			if index == len(nativeInput.Values()) {
+				panic("Input value did not found in enum values")
+			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -208,6 +212,10 @@ func Aws_cryptography_encryptionSdk_DecryptOutput_algorithmSuiteId_ToDafny(input
 			if enumVal == input {
 				break
 			}
+			if index == len(input.Values()) {
+				panic("Input value did not found in enum values")
+			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -255,6 +263,7 @@ func Aws_cryptography_encryptionSdk_EncryptInput_algorithmSuiteId_ToDafny(input
 			if enumVal == *input {
 				break
 			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -309,6 +318,10 @@ func Aws_cryptography_encryptionSdk_EncryptOutput_algorithmSuiteId_ToDafny(input
 			if enumVal == input {
 				break
 			}
+			if index == len(input.Values()) {
+				panic("Input value did not found in enum values")
+			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKAlgorithmSuiteId_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -346,6 +359,7 @@ func Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_commitmentPolicy_ToDa
 			if enumVal == *input {
 				break
 			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyMaterialProvidersTypes.CompanionStruct_ESDKCommitmentPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
@@ -379,6 +393,7 @@ func Aws_cryptography_encryptionSdk_AwsEncryptionSdkConfig_netV4_0_0_RetryPolicy
 			if enumVal == *input {
 				break
 			}
+
 		}
 		var enum interface{}
 		for allEnums, i := dafny.Iterate(AwsCryptographyEncryptionSdkTypes.CompanionStruct_NetV4__0__0__RetryPolicy_{}.AllSingletonConstructors()), 0; i < index; i++ {
diff --git a/mpl b/mpl
index 80e28f3f7..d3e79168a 160000
--- a/mpl
+++ b/mpl
@@ -1 +1 @@
-Subproject commit 80e28f3f7816e99ed22120cca6a81628a3ae4892
+Subproject commit d3e79168a23381973fab90e0c11e5ec0fb8a37fd
diff --git a/project.properties b/project.properties
index 44810c894..dca3891c3 100644
--- a/project.properties
+++ b/project.properties
@@ -4,6 +4,6 @@ dafnyVersion=4.9.0
 dafnyVerifyVersion=4.9.0
 dafnyFormatVersion=4.9.0
 projectJavaVersion=4.1.0
-mplDependencyJavaVersion=1.9.0-SNAPSHOT
+mplDependencyJavaVersion=1.10.1-SNAPSHOT
 dafnyRuntimeJavaVersion=4.9.0
 smithyDafnyJavaConversionVersion=0.1.1