in releases/go/mpl/AwsKmsEcdhKeyring/AwsKmsEcdhKeyring.go [382:544]
func (_this *AwsKmsEcdhKeyring) OnEncrypt_k(input m_AwsCryptographyMaterialProvidersTypes.OnEncryptInput) m_Wrappers.Result {
{
var res m_Wrappers.Result = m_Wrappers.Result{}
_ = res
var _0_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _0_valueOrError0
_0_valueOrError0 = m_Wrappers.Companion_Default___.Need(!(((_this).KeyAgreementScheme()).Is_KmsPublicKeyDiscovery()), Companion_Default___.E(_dafny.SeqOfString("KmsPublicKeyDiscovery Key Agreement Scheme is forbidden on encrypt.")))
if (_0_valueOrError0).IsFailure() {
res = (_0_valueOrError0).PropagateFailure()
return res
}
var _1_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _1_valueOrError1
_1_valueOrError1 = m_Wrappers.Companion_Default___.Need(((_this).SenderKmsKeyId()).Is_Some(), Companion_Default___.E(_dafny.SeqOfString("Keyring MUST be configured with a sender KMS Key ID")))
if (_1_valueOrError1).IsFailure() {
res = (_1_valueOrError1).PropagateFailure()
return res
}
var _2_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _2_valueOrError2
_2_valueOrError2 = m_Wrappers.Companion_Default___.Need(((_this).SenderPublicKey()).Is_Some(), Companion_Default___.E(_dafny.SeqOfString("Keyring MUST be configured with a senderPublicKey")))
if (_2_valueOrError2).IsFailure() {
res = (_2_valueOrError2).PropagateFailure()
return res
}
var _3_senderKmsKeyId _dafny.Sequence
_ = _3_senderKmsKeyId
_3_senderKmsKeyId = ((_this).SenderKmsKeyId()).Dtor_value().(_dafny.Sequence)
var _4_materials m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials
_ = _4_materials
_4_materials = (input).Dtor_materials()
var _5_suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo
_ = _5_suite
_5_suite = ((input).Dtor_materials()).Dtor_algorithmSuite()
var _6_valueOrError3 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptyMap)
_ = _6_valueOrError3
_6_valueOrError3 = m_AwsKmsUtils.Companion_Default___.StringifyEncryptionContext(((input).Dtor_materials()).Dtor_encryptionContext())
if (_6_valueOrError3).IsFailure() {
res = (_6_valueOrError3).PropagateFailure()
return res
}
var _7_stringifiedEncCtx _dafny.Map
_ = _7_stringifiedEncCtx
_7_stringifiedEncCtx = (_6_valueOrError3).Extract().(_dafny.Map)
var _8_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _8_valueOrError4
var _out0 m_Wrappers.Result
_ = _out0
_out0 = Companion_Default___.DeriveSharedSecret((_this).Client(), _3_senderKmsKeyId, (_this).RecipientPublicKey(), (_this).GrantTokens())
_8_valueOrError4 = _out0
if (_8_valueOrError4).IsFailure() {
res = (_8_valueOrError4).PropagateFailure()
return res
}
var _9_sharedSecret _dafny.Sequence
_ = _9_sharedSecret
_9_sharedSecret = (_8_valueOrError4).Extract().(_dafny.Sequence)
var _10_operationCompressedSenderPublicKey _dafny.Sequence
_ = _10_operationCompressedSenderPublicKey
if ((_this).CompressedSenderPublicKey()).Is_None() {
_10_operationCompressedSenderPublicKey = _dafny.SeqOf()
} else {
_10_operationCompressedSenderPublicKey = ((_this).CompressedSenderPublicKey()).Dtor_value().(_dafny.Sequence)
}
var _11_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_UTF8.Companion_ValidUTF8Bytes_.Witness())
_ = _11_valueOrError5
_11_valueOrError5 = (m_UTF8.Encode(m_RawECDHKeyring.Companion_Default___.CurveSpecTypeToString((_this).CurveSpec()))).MapFailure(func(coer118 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg119 interface{}) interface{} {
return coer118(arg119.(_dafny.Sequence))
}
}(m_AwsKmsUtils.Companion_Default___.WrapStringToError))
if (_11_valueOrError5).IsFailure() {
res = (_11_valueOrError5).PropagateFailure()
return res
}
var _12_curveSpecUtf8 _dafny.Sequence
_ = _12_curveSpecUtf8
_12_curveSpecUtf8 = (_11_valueOrError5).Extract().(_dafny.Sequence)
var _13_valueOrError6 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _13_valueOrError6
_13_valueOrError6 = m_CanonicalEncryptionContext.Companion_Default___.EncryptionContextToAAD(((input).Dtor_materials()).Dtor_encryptionContext())
if (_13_valueOrError6).IsFailure() {
res = (_13_valueOrError6).PropagateFailure()
return res
}
var _14_canonicalizedEC _dafny.Sequence
_ = _14_canonicalizedEC
_14_canonicalizedEC = (_13_valueOrError6).Extract().(_dafny.Sequence)
var _15_fixedInfo _dafny.Sequence
_ = _15_fixedInfo
_15_fixedInfo = m_EcdhEdkWrapping.Companion_Default___.SerializeFixedInfo(m_Constants.Companion_Default___.ECDH__KDF__UTF8(), _12_curveSpecUtf8, _10_operationCompressedSenderPublicKey, (_this).CompressedRecipientPublicKey(), _14_canonicalizedEC, Companion_Default___.AWS__KMS__ECDH__KEYRING__VERSION())
var _16_ecdhGenerateAndWrap *m_EcdhEdkWrapping.EcdhGenerateAndWrapKeyMaterial
_ = _16_ecdhGenerateAndWrap
var _nw0 *m_EcdhEdkWrapping.EcdhGenerateAndWrapKeyMaterial = m_EcdhEdkWrapping.New_EcdhGenerateAndWrapKeyMaterial_()
_ = _nw0
_nw0.Ctor__(_9_sharedSecret, _15_fixedInfo, (_this).CryptoPrimitives())
_16_ecdhGenerateAndWrap = _nw0
var _17_ecdhWrap *m_EcdhEdkWrapping.EcdhWrapKeyMaterial
_ = _17_ecdhWrap
var _nw1 *m_EcdhEdkWrapping.EcdhWrapKeyMaterial = m_EcdhEdkWrapping.New_EcdhWrapKeyMaterial_()
_ = _nw1
_nw1.Ctor__(_9_sharedSecret, _15_fixedInfo, (_this).CryptoPrimitives())
_17_ecdhWrap = _nw1
var _18_valueOrError7 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_EdkWrapping.Companion_WrapEdkMaterialOutput_.Default(m_EcdhEdkWrapping.Companion_EcdhWrapInfo_.Default()))
_ = _18_valueOrError7
var _out1 m_Wrappers.Result
_ = _out1
_out1 = m_EdkWrapping.Companion_Default___.WrapEdkMaterial(_4_materials, _17_ecdhWrap, _16_ecdhGenerateAndWrap)
_18_valueOrError7 = _out1
if (_18_valueOrError7).IsFailure() {
res = (_18_valueOrError7).PropagateFailure()
return res
}
var _19_wrapOutput m_EdkWrapping.WrapEdkMaterialOutput
_ = _19_wrapOutput
_19_wrapOutput = (_18_valueOrError7).Extract().(m_EdkWrapping.WrapEdkMaterialOutput)
var _20_symmetricSigningKeyList m_Wrappers.Option
_ = _20_symmetricSigningKeyList
if ((_19_wrapOutput).Dtor_symmetricSigningKey()).Is_Some() {
_20_symmetricSigningKeyList = m_Wrappers.Companion_Option_.Create_Some_(_dafny.SeqOf(((_19_wrapOutput).Dtor_symmetricSigningKey()).Dtor_value().(_dafny.Sequence)))
} else {
_20_symmetricSigningKeyList = m_Wrappers.Companion_Option_.Create_None_()
}
var _21_valueOrError8 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _21_valueOrError8
_21_valueOrError8 = m_Wrappers.Companion_Default___.Need((m_RawECDHKeyring.Companion_Default___.ValidCompressedPublicKeyLength(_10_operationCompressedSenderPublicKey)) && (m_RawECDHKeyring.Companion_Default___.ValidCompressedPublicKeyLength((_this).CompressedRecipientPublicKey())), Companion_Default___.E(_dafny.SeqOfString("Invalid compressed public key length.")))
if (_21_valueOrError8).IsFailure() {
res = (_21_valueOrError8).PropagateFailure()
return res
}
var _22_edk m_AwsCryptographyMaterialProvidersTypes.EncryptedDataKey
_ = _22_edk
_22_edk = m_AwsCryptographyMaterialProvidersTypes.Companion_EncryptedDataKey_.Create_EncryptedDataKey_(m_Constants.Companion_Default___.KMS__ECDH__PROVIDER__ID(), m_RawECDHKeyring.Companion_Default___.SerializeProviderInfo(_10_operationCompressedSenderPublicKey, (_this).CompressedRecipientPublicKey()), (_19_wrapOutput).Dtor_wrappedMaterial())
if (_19_wrapOutput).Is_GenerateAndWrapEdkMaterialOutput() {
var _23_valueOrError9 m_Wrappers.Result = m_Wrappers.Result{}
_ = _23_valueOrError9
_23_valueOrError9 = m_Materials.Companion_Default___.EncryptionMaterialAddDataKey(_4_materials, (_19_wrapOutput).Dtor_plaintextDataKey(), _dafny.SeqOf(_22_edk), _20_symmetricSigningKeyList)
if (_23_valueOrError9).IsFailure() {
res = (_23_valueOrError9).PropagateFailure()
return res
}
var _24_result m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials
_ = _24_result
_24_result = (_23_valueOrError9).Extract().(m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials)
res = m_Wrappers.Companion_Result_.Create_Success_(m_AwsCryptographyMaterialProvidersTypes.Companion_OnEncryptOutput_.Create_OnEncryptOutput_(_24_result))
return res
} else if (_19_wrapOutput).Is_WrapOnlyEdkMaterialOutput() {
var _25_valueOrError10 m_Wrappers.Result = m_Wrappers.Result{}
_ = _25_valueOrError10
_25_valueOrError10 = m_Materials.Companion_Default___.EncryptionMaterialAddEncryptedDataKeys(_4_materials, _dafny.SeqOf(_22_edk), _20_symmetricSigningKeyList)
if (_25_valueOrError10).IsFailure() {
res = (_25_valueOrError10).PropagateFailure()
return res
}
var _26_result m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials
_ = _26_result
_26_result = (_25_valueOrError10).Extract().(m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials)
res = m_Wrappers.Companion_Result_.Create_Success_(m_AwsCryptographyMaterialProvidersTypes.Companion_OnEncryptOutput_.Create_OnEncryptOutput_(_26_result))
return res
}
return res
}
}