in releases/go/encryption-sdk/KeyDerivation/KeyDerivation.go [450:550]
func (_static *CompanionStruct_Default___) DeriveKeys(messageId _dafny.Sequence, plaintextKey _dafny.Sequence, suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, crypto *m_AtomicPrimitives.AtomicPrimitivesClient, netV4__0__0__RetryPolicy m_AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy, onNetV4Retry bool) m_Wrappers.Result {
var res m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(Companion_ExpandedKeyMaterial_.Default())
_ = res
var _0_keys ExpandedKeyMaterial = Companion_ExpandedKeyMaterial_.Default()
_ = _0_keys
if ((suite).Dtor_messageVersion()) == (int32(2)) {
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _1_valueOrError0
_1_valueOrError0 = m_Wrappers.Companion_Default___.Need((((suite).Dtor_commitment()).Is_HKDF()) && (((suite).Dtor_kdf()).Equals((suite).Dtor_commitment())), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Suites with message version 2 must have commitment")))
if (_1_valueOrError0).IsFailure() {
res = (_1_valueOrError0).PropagateFailure()
return res
}
var _2_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _2_valueOrError1
_2_valueOrError1 = m_Wrappers.Companion_Default___.Need(((m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite)) == ((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_outputKeyLength())) && ((_dafny.IntOfUint32((plaintextKey).Cardinality())).Cmp(_dafny.IntOfInt32((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_inputKeyLength())) == 0), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Invalid Materials")))
if (_2_valueOrError1).IsFailure() {
res = (_2_valueOrError1).PropagateFailure()
return res
}
var _3_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(Companion_ExpandedKeyMaterial_.Default())
_ = _3_valueOrError2
var _out0 m_Wrappers.Result
_ = _out0
_out0 = Companion_Default___.ExpandKeyMaterial(messageId, plaintextKey, suite, crypto)
_3_valueOrError2 = _out0
if (_3_valueOrError2).IsFailure() {
res = (_3_valueOrError2).PropagateFailure()
return res
}
_0_keys = (_3_valueOrError2).Extract().(ExpandedKeyMaterial)
} else if ((suite).Dtor_messageVersion()) == (int32(1)) {
var _4_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _4_valueOrError3
_4_valueOrError3 = m_Wrappers.Companion_Default___.Need(((suite).Dtor_commitment()).Is_None(), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Suites with message version 1 must not have commitment")))
if (_4_valueOrError3).IsFailure() {
res = (_4_valueOrError3).PropagateFailure()
return res
}
var _5_valueOrError4 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _5_valueOrError4
_5_valueOrError4 = m_Wrappers.Companion_Default___.Need(func() bool {
var _source0 m_AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm = (suite).Dtor_kdf()
_ = _source0
{
if _source0.Is_IDENTITY() {
var _6_i m_AwsCryptographyMaterialProvidersTypes.IDENTITY = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm_IDENTITY).IDENTITY
_ = _6_i
return (_dafny.IntOfUint32((plaintextKey).Cardinality())).Cmp(_dafny.IntOfInt32(m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite))) == 0
}
}
{
if _source0.Is_HKDF() {
var _7_hkdf m_AwsCryptographyMaterialProvidersTypes.HKDF = _source0.Get_().(m_AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm_HKDF).HKDF
_ = _7_hkdf
return ((_dafny.IntOfUint32((plaintextKey).Cardinality())).Cmp(_dafny.IntOfInt32((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_inputKeyLength())) == 0) && (((((suite).Dtor_kdf()).Dtor_HKDF()).Dtor_outputKeyLength()) == (m_SerializableTypes.Companion_Default___.GetEncryptKeyLength(suite)))
}
}
{
var _8_None m_AwsCryptographyMaterialProvidersTypes.DerivationAlgorithm = _source0
_ = _8_None
return false
}
}(), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Suites with message version 1 must not have commitment")))
if (_5_valueOrError4).IsFailure() {
res = (_5_valueOrError4).PropagateFailure()
return res
}
if ((netV4__0__0__RetryPolicy).Equals(m_AwsCryptographyEncryptionSdkTypes.Companion_NetV4__0__0__RetryPolicy_.Create_ALLOW__RETRY_())) && (onNetV4Retry) {
var _9_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(Companion_ExpandedKeyMaterial_.Default())
_ = _9_valueOrError5
var _out1 m_Wrappers.Result
_ = _out1
_out1 = Companion_Default___.DeriveKey(messageId, plaintextKey, suite, crypto, true)
_9_valueOrError5 = _out1
if (_9_valueOrError5).IsFailure() {
res = (_9_valueOrError5).PropagateFailure()
return res
}
_0_keys = (_9_valueOrError5).Extract().(ExpandedKeyMaterial)
} else {
var _10_valueOrError6 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(Companion_ExpandedKeyMaterial_.Default())
_ = _10_valueOrError6
var _out2 m_Wrappers.Result
_ = _out2
_out2 = Companion_Default___.DeriveKey(messageId, plaintextKey, suite, crypto, false)
_10_valueOrError6 = _out2
if (_10_valueOrError6).IsFailure() {
res = (_10_valueOrError6).PropagateFailure()
return res
}
_0_keys = (_10_valueOrError6).Extract().(ExpandedKeyMaterial)
}
} else {
res = m_Wrappers.Companion_Result_.Create_Failure_(m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Unknown message version")))
return res
}
res = m_Wrappers.Companion_Result_.Create_Success_(_0_keys)
return res
return res
}