func()

in releases/go/mpl/AwsKmsDiscoveryKeyring/AwsKmsDiscoveryKeyring.go [311:417]


func (_this *AwsKmsDiscoveryKeyring) OnDecrypt_k(input m_AwsCryptographyMaterialProvidersTypes.OnDecryptInput) m_Wrappers.Result {
	{
		var res m_Wrappers.Result = m_Wrappers.Result{}
		_ = res
		var _0_materials m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials
		_ = _0_materials
		_0_materials = (input).Dtor_materials()
		var _1_encryptedDataKeys _dafny.Sequence
		_ = _1_encryptedDataKeys
		_1_encryptedDataKeys = (input).Dtor_encryptedDataKeys()
		var _2_suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo
		_ = _2_suite
		_2_suite = ((input).Dtor_materials()).Dtor_algorithmSuite()
		var _3_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
		_ = _3_valueOrError0
		_3_valueOrError0 = m_Wrappers.Companion_Default___.Need(m_Materials.Companion_Default___.DecryptionMaterialsWithoutPlaintextDataKey(_0_materials), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Keyring received decryption materials that already contain a plaintext data key.")))
		if (_3_valueOrError0).IsFailure() {
			res = (_3_valueOrError0).PropagateFailure()
			return res
		}
		var _4_edkFilter *AwsKmsEncryptedDataKeyFilter
		_ = _4_edkFilter
		var _nw0 *AwsKmsEncryptedDataKeyFilter = New_AwsKmsEncryptedDataKeyFilter_()
		_ = _nw0
		_nw0.Ctor__((_this).DiscoveryFilter())
		_4_edkFilter = _nw0
		var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
		_ = _5_valueOrError1
		var _out0 m_Wrappers.Result
		_ = _out0
		_out0 = m_Actions.Companion_Default___.FilterWithResult(_4_edkFilter, _1_encryptedDataKeys)
		_5_valueOrError1 = _out0
		if (_5_valueOrError1).IsFailure() {
			res = (_5_valueOrError1).PropagateFailure()
			return res
		}
		var _6_matchingEdks _dafny.Sequence
		_ = _6_matchingEdks
		_6_matchingEdks = (_5_valueOrError1).Extract().(_dafny.Sequence)
		var _7_edkTransform *AwsKmsEncryptedDataKeyTransformer
		_ = _7_edkTransform
		var _nw1 *AwsKmsEncryptedDataKeyTransformer = New_AwsKmsEncryptedDataKeyTransformer_()
		_ = _nw1
		_nw1.Ctor__()
		_7_edkTransform = _nw1
		var _8_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
		_ = _8_valueOrError2
		var _out1 m_Wrappers.Result
		_ = _out1
		_out1 = m_Actions.Companion_Default___.DeterministicFlatMapWithResult(_7_edkTransform, _6_matchingEdks)
		_8_valueOrError2 = _out1
		if (_8_valueOrError2).IsFailure() {
			res = (_8_valueOrError2).PropagateFailure()
			return res
		}
		var _9_edksToAttempt _dafny.Sequence
		_ = _9_edksToAttempt
		_9_edksToAttempt = (_8_valueOrError2).Extract().(_dafny.Sequence)
		if (_dafny.IntOfUint32((_9_edksToAttempt).Cardinality())).Sign() == 0 {
			var _10_valueOrError3 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq.SetString())
			_ = _10_valueOrError3
			_10_valueOrError3 = m_ErrorMessages.Companion_Default___.IncorrectDataKeys((input).Dtor_encryptedDataKeys(), ((input).Dtor_materials()).Dtor_algorithmSuite(), _dafny.SeqOfString(""))
			if (_10_valueOrError3).IsFailure() {
				res = (_10_valueOrError3).PropagateFailure()
				return res
			}
			var _11_errorMessage _dafny.Sequence
			_ = _11_errorMessage
			_11_errorMessage = (_10_valueOrError3).Extract().(_dafny.Sequence)
			res = m_Wrappers.Companion_Result_.Create_Failure_(m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_11_errorMessage))
			return res
		}
		var _12_decryptAction *AwsKmsEncryptedDataKeyDecryptor
		_ = _12_decryptAction
		var _nw2 *AwsKmsEncryptedDataKeyDecryptor = New_AwsKmsEncryptedDataKeyDecryptor_()
		_ = _nw2
		_nw2.Ctor__(_0_materials, (_this).Client(), (_this).GrantTokens())
		_12_decryptAction = _nw2
		var _13_outcome m_Wrappers.Result
		_ = _13_outcome
		var _out2 m_Wrappers.Result
		_ = _out2
		_out2 = m_Actions.Companion_Default___.ReduceToSuccess(_12_decryptAction, _9_edksToAttempt)
		_13_outcome = _out2
		var _source0 m_Wrappers.Result = _13_outcome
		_ = _source0
		{
			{
				if _source0.Is_Success() {
					var _14_mat m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials = _source0.Get_().(m_Wrappers.Result_Success).Value.(m_AwsCryptographyMaterialProvidersTypes.DecryptionMaterials)
					_ = _14_mat
					res = m_Wrappers.Companion_Result_.Create_Success_(m_AwsCryptographyMaterialProvidersTypes.Companion_OnDecryptOutput_.Create_OnDecryptOutput_(_14_mat))
					goto Lmatch0
				}
			}
			{
				var _15_errors _dafny.Sequence = _source0.Get_().(m_Wrappers.Result_Failure).Error.(_dafny.Sequence)
				_ = _15_errors
				res = m_Wrappers.Companion_Result_.Create_Failure_(m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_CollectionOfErrors_(_15_errors, _dafny.SeqOfString("No Configured KMS Key was able to decrypt the Data Key. The list of encountered Exceptions is available via `list`.")))
			}
			goto Lmatch0
		}
	Lmatch0:
		return res
		return res
	}
}