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
}
}