in releases/go/mpl/AwsCryptographyMaterialProvidersOperations/AwsCryptographyMaterialProvidersOperations.go [1145:1314]
func (_static *CompanionStruct_Default___) CreateRawEcdhKeyring(config Config, input m_AwsCryptographyMaterialProvidersTypes.CreateRawEcdhKeyringInput) m_Wrappers.Result {
var output m_Wrappers.Result = m_Wrappers.Result{}
_ = output
var _0_recipientPublicKey _dafny.Sequence = _dafny.EmptySeq
_ = _0_recipientPublicKey
var _1_senderPrivateKey m_Wrappers.Option = m_Wrappers.Companion_Option_.Default()
_ = _1_senderPrivateKey
var _2_senderPublicKey m_Wrappers.Option = m_Wrappers.Companion_Option_.Default()
_ = _2_senderPublicKey
var _3_compressedSenderPublicKey m_Wrappers.Option = m_Wrappers.Companion_Option_.Default()
_ = _3_compressedSenderPublicKey
var _source0 m_AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations = (input).Dtor_KeyAgreementScheme()
_ = _source0
{
{
if _source0.Is_RawPrivateKeyToStaticPublicKey() {
var _4_rawPrivateKeyToStaticPublicKey m_AwsCryptographyMaterialProvidersTypes.RawPrivateKeyToStaticPublicKeyInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations_RawPrivateKeyToStaticPublicKey).RawPrivateKeyToStaticPublicKey
_ = _4_rawPrivateKeyToStaticPublicKey
{
_0_recipientPublicKey = (_4_rawPrivateKeyToStaticPublicKey).Dtor_recipientPublicKey()
_1_senderPrivateKey = m_Wrappers.Companion_Option_.Create_Some_((_4_rawPrivateKeyToStaticPublicKey).Dtor_senderStaticPrivateKey())
var _5_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _5_valueOrError0
var _out0 m_Wrappers.Result
_ = _out0
_out0 = m_Utils.Companion_Default___.GetPublicKey((input).Dtor_curveSpec(), m_AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Create_ECCPrivateKey_((_1_senderPrivateKey).Dtor_value().(_dafny.Sequence)), (config).Dtor_crypto())
_5_valueOrError0 = _out0
if (_5_valueOrError0).IsFailure() {
output = (_5_valueOrError0).PropagateFailure()
return output
}
var _6_reproducedPublicKey _dafny.Sequence
_ = _6_reproducedPublicKey
_6_reproducedPublicKey = (_5_valueOrError0).Extract().(_dafny.Sequence)
var _7_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _7_valueOrError1
var _out1 m_Wrappers.Result
_ = _out1
_out1 = m_RawECDHKeyring.Companion_Default___.ValidatePublicKey((config).Dtor_crypto(), (input).Dtor_curveSpec(), _6_reproducedPublicKey)
_7_valueOrError1 = _out1
if (_7_valueOrError1).IsFailure() {
output = (_7_valueOrError1).PropagateFailure()
return output
}
var _8___v10 bool
_ = _8___v10
_8___v10 = (_7_valueOrError1).Extract().(bool)
_2_senderPublicKey = m_Wrappers.Companion_Option_.Create_Some_(_6_reproducedPublicKey)
var _9_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _9_valueOrError2
var _out2 m_Wrappers.Result
_ = _out2
_out2 = m_RawECDHKeyring.Companion_Default___.CompressPublicKey(m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(_6_reproducedPublicKey), (input).Dtor_curveSpec(), (config).Dtor_crypto())
_9_valueOrError2 = _out2
if (_9_valueOrError2).IsFailure() {
output = (_9_valueOrError2).PropagateFailure()
return output
}
var _10_compressedSenderPublicKey_q _dafny.Sequence
_ = _10_compressedSenderPublicKey_q
_10_compressedSenderPublicKey_q = (_9_valueOrError2).Extract().(_dafny.Sequence)
_3_compressedSenderPublicKey = m_Wrappers.Companion_Option_.Create_Some_(_10_compressedSenderPublicKey_q)
}
goto Lmatch0
}
}
{
if _source0.Is_EphemeralPrivateKeyToStaticPublicKey() {
var _11_ephemeralPrivateKeyToStaticPublicKey m_AwsCryptographyMaterialProvidersTypes.EphemeralPrivateKeyToStaticPublicKeyInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations_EphemeralPrivateKeyToStaticPublicKey).EphemeralPrivateKeyToStaticPublicKey
_ = _11_ephemeralPrivateKeyToStaticPublicKey
{
_0_recipientPublicKey = (_11_ephemeralPrivateKeyToStaticPublicKey).Dtor_recipientPublicKey()
_1_senderPrivateKey = m_Wrappers.Companion_Option_.Create_None_()
_2_senderPublicKey = m_Wrappers.Companion_Option_.Create_None_()
_3_compressedSenderPublicKey = m_Wrappers.Companion_Option_.Create_None_()
}
goto Lmatch0
}
}
{
var _12_publicKeyDiscovery m_AwsCryptographyMaterialProvidersTypes.PublicKeyDiscoveryInput = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.RawEcdhStaticConfigurations_PublicKeyDiscovery).PublicKeyDiscovery
_ = _12_publicKeyDiscovery
{
var _13_valueOrError3 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _13_valueOrError3
var _out3 m_Wrappers.Result
_ = _out3
_out3 = m_Utils.Companion_Default___.GetPublicKey((input).Dtor_curveSpec(), m_AwsCryptographyPrimitivesTypes.Companion_ECCPrivateKey_.Create_ECCPrivateKey_((_12_publicKeyDiscovery).Dtor_recipientStaticPrivateKey()), (config).Dtor_crypto())
_13_valueOrError3 = _out3
if (_13_valueOrError3).IsFailure() {
output = (_13_valueOrError3).PropagateFailure()
return output
}
var _14_reproducedPublicKey _dafny.Sequence
_ = _14_reproducedPublicKey
_14_reproducedPublicKey = (_13_valueOrError3).Extract().(_dafny.Sequence)
_0_recipientPublicKey = _14_reproducedPublicKey
_1_senderPrivateKey = m_Wrappers.Companion_Option_.Create_None_()
_2_senderPublicKey = m_Wrappers.Companion_Option_.Create_None_()
_3_compressedSenderPublicKey = m_Wrappers.Companion_Option_.Create_None_()
}
}
goto Lmatch0
}
Lmatch0:
var _15_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _15_valueOrError4
var _out4 m_Wrappers.Result
_ = _out4
_out4 = m_RawECDHKeyring.Companion_Default___.CompressPublicKey(m_AwsCryptographyPrimitivesTypes.Companion_ECCPublicKey_.Create_ECCPublicKey_(_0_recipientPublicKey), (input).Dtor_curveSpec(), (config).Dtor_crypto())
_15_valueOrError4 = _out4
if (_15_valueOrError4).IsFailure() {
output = (_15_valueOrError4).PropagateFailure()
return output
}
var _16_compressedRecipientPublicKey _dafny.Sequence
_ = _16_compressedRecipientPublicKey
_16_compressedRecipientPublicKey = (_15_valueOrError4).Extract().(_dafny.Sequence)
var _17_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _17_valueOrError5
var _out5 m_Wrappers.Result
_ = _out5
_out5 = m_RawECDHKeyring.Companion_Default___.ValidatePublicKey((config).Dtor_crypto(), (input).Dtor_curveSpec(), _0_recipientPublicKey)
_17_valueOrError5 = _out5
if (_17_valueOrError5).IsFailure() {
output = (_17_valueOrError5).PropagateFailure()
return output
}
var _18___v11 bool
_ = _18___v11
_18___v11 = (_17_valueOrError5).Extract().(bool)
if (_2_senderPublicKey).Is_Some() {
var _19_valueOrError6 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(false)
_ = _19_valueOrError6
var _out6 m_Wrappers.Result
_ = _out6
_out6 = m_RawECDHKeyring.Companion_Default___.ValidatePublicKey((config).Dtor_crypto(), (input).Dtor_curveSpec(), (_2_senderPublicKey).Dtor_value().(_dafny.Sequence))
_19_valueOrError6 = _out6
if (_19_valueOrError6).IsFailure() {
output = (_19_valueOrError6).PropagateFailure()
return output
}
var _20___v12 bool
_ = _20___v12
_20___v12 = (_19_valueOrError6).Extract().(bool)
var _21_valueOrError7 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _21_valueOrError7
_21_valueOrError7 = m_Wrappers.Companion_Default___.Need(m_RawECDHKeyring.Companion_Default___.ValidPublicKeyLength((_2_senderPublicKey).Dtor_value().(_dafny.Sequence)), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Invalid sender public key length")))
if (_21_valueOrError7).IsFailure() {
output = (_21_valueOrError7).PropagateFailure()
return output
}
}
var _22_valueOrError8 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _22_valueOrError8
_22_valueOrError8 = m_Wrappers.Companion_Default___.Need(m_RawECDHKeyring.Companion_Default___.ValidPublicKeyLength(_0_recipientPublicKey), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Invalid recipient public key length")))
if (_22_valueOrError8).IsFailure() {
output = (_22_valueOrError8).PropagateFailure()
return output
}
var _23_keyring *m_RawECDHKeyring.RawEcdhKeyring
_ = _23_keyring
var _nw0 *m_RawECDHKeyring.RawEcdhKeyring = m_RawECDHKeyring.New_RawEcdhKeyring_()
_ = _nw0
_nw0.Ctor__((input).Dtor_KeyAgreementScheme(), (input).Dtor_curveSpec(), _1_senderPrivateKey, _2_senderPublicKey, _0_recipientPublicKey, _3_compressedSenderPublicKey, _16_compressedRecipientPublicKey, (config).Dtor_crypto())
_23_keyring = _nw0
output = m_Wrappers.Companion_Result_.Create_Success_(_23_keyring)
return output
return output
}