in releases/go/mpl/AwsCryptographyMaterialProvidersOperations/AwsCryptographyMaterialProvidersOperations.go [770:973]
func (_static *CompanionStruct_Default___) CreateAwsKmsEcdhKeyring(config Config, input m_AwsCryptographyMaterialProvidersTypes.CreateAwsKmsEcdhKeyringInput) m_Wrappers.Result {
var output m_Wrappers.Result = m_Wrappers.Result{}
_ = output
var _0_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _0_valueOrError0
_0_valueOrError0 = m_AwsKmsUtils.Companion_Default___.GetValidGrantTokens((input).Dtor_grantTokens())
if (_0_valueOrError0).IsFailure() {
output = (_0_valueOrError0).PropagateFailure()
return output
}
var _1_grantTokens _dafny.Sequence
_ = _1_grantTokens
_1_grantTokens = (_0_valueOrError0).Extract().(_dafny.Sequence)
var _2_recipientPublicKey _dafny.Sequence = _dafny.EmptySeq
_ = _2_recipientPublicKey
var _3_senderPublicKey m_Wrappers.Option = m_Wrappers.Companion_Option_.Default()
_ = _3_senderPublicKey
var _4_compressedSenderPublicKey m_Wrappers.Option = m_Wrappers.Companion_Option_.Default()
_ = _4_compressedSenderPublicKey
var _source0 m_AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations = (input).Dtor_KeyAgreementScheme()
_ = _source0
{
{
if _source0.Is_KmsPublicKeyDiscovery() {
var _5_kmsPublicKeyDiscovery m_AwsCryptographyMaterialProvidersTypes.KmsPublicKeyDiscoveryInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations_KmsPublicKeyDiscovery).KmsPublicKeyDiscovery
_ = _5_kmsPublicKeyDiscovery
{
var _6_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _6_valueOrError1
_6_valueOrError1 = m_AwsKmsUtils.Companion_Default___.ValidateKmsKeyId((_5_kmsPublicKeyDiscovery).Dtor_recipientKmsIdentifier())
if (_6_valueOrError1).IsFailure() {
output = (_6_valueOrError1).PropagateFailure()
return output
}
var _7___v5 _dafny.Tuple
_ = _7___v5
_7___v5 = (_6_valueOrError1).Extract().(_dafny.Tuple)
var _8_valueOrError2 m_Wrappers.Result = m_Wrappers.Result{}
_ = _8_valueOrError2
var _out0 m_Wrappers.Result
_ = _out0
_out0 = m_AwsKmsUtils.Companion_Default___.GetEcdhPublicKey((input).Dtor_kmsClient(), (_5_kmsPublicKeyDiscovery).Dtor_recipientKmsIdentifier())
_8_valueOrError2 = _out0
if (_8_valueOrError2).IsFailure() {
output = (_8_valueOrError2).PropagateFailure()
return output
}
_2_recipientPublicKey = (_8_valueOrError2).Extract().(_dafny.Sequence)
_3_senderPublicKey = m_Wrappers.Companion_Option_.Create_None_()
_4_compressedSenderPublicKey = m_Wrappers.Companion_Option_.Create_None_()
}
goto Lmatch0
}
}
{
var _9_kmsPrivateKeyToStaticPublicKey m_AwsCryptographyMaterialProvidersTypes.KmsPrivateKeyToStaticPublicKeyInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.KmsEcdhStaticConfigurations_KmsPrivateKeyToStaticPublicKey).KmsPrivateKeyToStaticPublicKey
_ = _9_kmsPrivateKeyToStaticPublicKey
{
if ((_9_kmsPrivateKeyToStaticPublicKey).Dtor_senderPublicKey()).Is_Some() {
var _10_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _10_valueOrError3
_10_valueOrError3 = m_Wrappers.Companion_Default___.Need(m_ComAmazonawsKmsTypes.Companion_Default___.IsValid__PublicKeyType(((_9_kmsPrivateKeyToStaticPublicKey).Dtor_senderPublicKey()).Dtor_value().(_dafny.Sequence)), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Invalid SenderPublicKey length.")))
if (_10_valueOrError3).IsFailure() {
output = (_10_valueOrError3).PropagateFailure()
return output
}
_3_senderPublicKey = m_Wrappers.Companion_Option_.Create_Some_(((_9_kmsPrivateKeyToStaticPublicKey).Dtor_senderPublicKey()).Dtor_value().(_dafny.Sequence))
var _11_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _11_valueOrError4
var _out1 m_Wrappers.Result
_ = _out1
_out1 = m_RawECDHKeyring.Companion_Default___.CompressPublicKey(m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_((_3_senderPublicKey).Dtor_value().(_dafny.Sequence)), (input).Dtor_curveSpec(), (config).Dtor_crypto())
_11_valueOrError4 = _out1
if (_11_valueOrError4).IsFailure() {
output = (_11_valueOrError4).PropagateFailure()
return output
}
var _12_compressedPKU _dafny.Sequence
_ = _12_compressedPKU
_12_compressedPKU = (_11_valueOrError4).Extract().(_dafny.Sequence)
_4_compressedSenderPublicKey = m_Wrappers.Companion_Option_.Create_Some_(_12_compressedPKU)
} else {
var _13_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _13_valueOrError5
_13_valueOrError5 = m_AwsKmsUtils.Companion_Default___.ValidateKmsKeyId((_9_kmsPrivateKeyToStaticPublicKey).Dtor_senderKmsIdentifier())
if (_13_valueOrError5).IsFailure() {
output = (_13_valueOrError5).PropagateFailure()
return output
}
var _14___v6 _dafny.Tuple
_ = _14___v6
_14___v6 = (_13_valueOrError5).Extract().(_dafny.Tuple)
var _15_valueOrError6 m_Wrappers.Result = m_Wrappers.Result{}
_ = _15_valueOrError6
var _out2 m_Wrappers.Result
_ = _out2
_out2 = m_AwsKmsUtils.Companion_Default___.GetEcdhPublicKey((input).Dtor_kmsClient(), (_9_kmsPrivateKeyToStaticPublicKey).Dtor_senderKmsIdentifier())
_15_valueOrError6 = _out2
if (_15_valueOrError6).IsFailure() {
output = (_15_valueOrError6).PropagateFailure()
return output
}
var _16_senderPublicKeyResponse _dafny.Sequence
_ = _16_senderPublicKeyResponse
_16_senderPublicKeyResponse = (_15_valueOrError6).Extract().(_dafny.Sequence)
var _17_valueOrError7 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _17_valueOrError7
var _out3 m_Wrappers.Result
_ = _out3
_out3 = m_RawECDHKeyring.Companion_Default___.CompressPublicKey(m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(_16_senderPublicKeyResponse), (input).Dtor_curveSpec(), (config).Dtor_crypto())
_17_valueOrError7 = _out3
if (_17_valueOrError7).IsFailure() {
output = (_17_valueOrError7).PropagateFailure()
return output
}
var _18_compressedPKU _dafny.Sequence
_ = _18_compressedPKU
_18_compressedPKU = (_17_valueOrError7).Extract().(_dafny.Sequence)
_3_senderPublicKey = m_Wrappers.Companion_Option_.Create_Some_(_16_senderPublicKeyResponse)
_4_compressedSenderPublicKey = m_Wrappers.Companion_Option_.Create_Some_(_18_compressedPKU)
}
var _19_valueOrError8 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _19_valueOrError8
_19_valueOrError8 = m_Wrappers.Companion_Default___.Need(m_ComAmazonawsKmsTypes.Companion_Default___.IsValid__PublicKeyType((_9_kmsPrivateKeyToStaticPublicKey).Dtor_recipientPublicKey()), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Invalid RecipientPublicKey length.")))
if (_19_valueOrError8).IsFailure() {
output = (_19_valueOrError8).PropagateFailure()
return output
}
_2_recipientPublicKey = (_9_kmsPrivateKeyToStaticPublicKey).Dtor_recipientPublicKey()
}
}
goto Lmatch0
}
Lmatch0:
var _20_valueOrError9 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _20_valueOrError9
var _out4 m_Wrappers.Result
_ = _out4
_out4 = m_RawECDHKeyring.Companion_Default___.ValidatePublicKey((config).Dtor_crypto(), (input).Dtor_curveSpec(), _2_recipientPublicKey)
_20_valueOrError9 = _out4
if (_20_valueOrError9).IsFailure() {
output = (_20_valueOrError9).PropagateFailure()
return output
}
var _21___v7 bool
_ = _21___v7
_21___v7 = (_20_valueOrError9).Extract().(bool)
var _22_valueOrError10 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _22_valueOrError10
var _out5 m_Wrappers.Result
_ = _out5
_out5 = m_RawECDHKeyring.Companion_Default___.CompressPublicKey(m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(_2_recipientPublicKey), (input).Dtor_curveSpec(), (config).Dtor_crypto())
_22_valueOrError10 = _out5
if (_22_valueOrError10).IsFailure() {
output = (_22_valueOrError10).PropagateFailure()
return output
}
var _23_compressedRecipientPublicKey _dafny.Sequence
_ = _23_compressedRecipientPublicKey
_23_compressedRecipientPublicKey = (_22_valueOrError10).Extract().(_dafny.Sequence)
var _24_senderKmsKeyId m_Wrappers.Option
_ = _24_senderKmsKeyId
if ((input).Dtor_KeyAgreementScheme()).Is_KmsPublicKeyDiscovery() {
_24_senderKmsKeyId = m_Wrappers.Companion_Option_.Create_None_()
} else {
_24_senderKmsKeyId = m_Wrappers.Companion_Option_.Create_Some_((((input).Dtor_KeyAgreementScheme()).Dtor_KmsPrivateKeyToStaticPublicKey()).Dtor_senderKmsIdentifier())
}
if (_24_senderKmsKeyId).Is_Some() {
var _25_valueOrError11 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _25_valueOrError11
_25_valueOrError11 = m_AwsKmsUtils.Companion_Default___.ValidateKmsKeyId((_24_senderKmsKeyId).Dtor_value().(_dafny.Sequence))
if (_25_valueOrError11).IsFailure() {
output = (_25_valueOrError11).PropagateFailure()
return output
}
var _26___v8 _dafny.Tuple
_ = _26___v8
_26___v8 = (_25_valueOrError11).Extract().(_dafny.Tuple)
}
if (_3_senderPublicKey).Is_Some() {
var _27_valueOrError12 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _27_valueOrError12
var _out6 m_Wrappers.Result
_ = _out6
_out6 = m_RawECDHKeyring.Companion_Default___.ValidatePublicKey((config).Dtor_crypto(), (input).Dtor_curveSpec(), (_3_senderPublicKey).Dtor_value().(_dafny.Sequence))
_27_valueOrError12 = _out6
if (_27_valueOrError12).IsFailure() {
output = (_27_valueOrError12).PropagateFailure()
return output
}
var _28___v9 bool
_ = _28___v9
_28___v9 = (_27_valueOrError12).Extract().(bool)
}
var _29_keyring *m_AwsKmsEcdhKeyring.AwsKmsEcdhKeyring
_ = _29_keyring
var _nw0 *m_AwsKmsEcdhKeyring.AwsKmsEcdhKeyring = m_AwsKmsEcdhKeyring.New_AwsKmsEcdhKeyring_()
_ = _nw0
_nw0.Ctor__((input).Dtor_KeyAgreementScheme(), (input).Dtor_curveSpec(), (input).Dtor_kmsClient(), _1_grantTokens, _24_senderKmsKeyId, _3_senderPublicKey, _2_recipientPublicKey, _4_compressedSenderPublicKey, _23_compressedRecipientPublicKey, (config).Dtor_crypto())
_29_keyring = _nw0
output = m_Wrappers.Companion_Result_.Create_Success_(_29_keyring)
return output
return output
}