func()

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
}