in releases/go/mpl/IntermediateKeyWrapping/IntermediateKeyWrapping.go [198:337]
func (_static *CompanionStruct_Default___) IntermediateUnwrap(unwrap m_MaterialWrapping.UnwrapMaterial, wrappedMaterial _dafny.Sequence, algorithmSuite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, encryptionContext _dafny.Map) m_Wrappers.Result {
var res m_Wrappers.Result = m_Wrappers.Result{}
_ = res
var _0_maybeCrypto m_Wrappers.Result
_ = _0_maybeCrypto
var _out0 m_Wrappers.Result
_ = _out0
_out0 = m_AtomicPrimitives.Companion_Default___.AtomicPrimitives(m_AtomicPrimitives.Companion_Default___.DefaultCryptoConfig())
_0_maybeCrypto = _out0
var _1_valueOrError0 m_Wrappers.Result = m_Wrappers.Result{}
_ = _1_valueOrError0
_1_valueOrError0 = (_0_maybeCrypto).MapFailure(func(coer38 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg39 interface{}) interface{} {
return coer38(arg39.(m_AwsCryptographyPrimitivesTypes.Error))
}
}(func(_2_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyMaterialProvidersTypes.Error {
return m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_2_e)
}))
if (_1_valueOrError0).IsFailure() {
res = (_1_valueOrError0).PropagateFailure()
return res
}
var _3_cryptoPrimitivesX m_AwsCryptographyPrimitivesTypes.IAwsCryptographicPrimitivesClient
_ = _3_cryptoPrimitivesX
_3_cryptoPrimitivesX = (_1_valueOrError0).Extract().(*m_AtomicPrimitives.AtomicPrimitivesClient)
var _4_cryptoPrimitives *m_AtomicPrimitives.AtomicPrimitivesClient
_ = _4_cryptoPrimitives
_4_cryptoPrimitives = _3_cryptoPrimitivesX.(*m_AtomicPrimitives.AtomicPrimitivesClient)
var _5_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(Companion_DeserializedIntermediateWrappedMaterial_.Default())
_ = _5_valueOrError1
_5_valueOrError1 = Companion_Default___.DeserializeIntermediateWrappedMaterial(wrappedMaterial, algorithmSuite)
if (_5_valueOrError1).IsFailure() {
res = (_5_valueOrError1).PropagateFailure()
return res
}
var _6_deserializedWrapped DeserializedIntermediateWrappedMaterial
_ = _6_deserializedWrapped
_6_deserializedWrapped = (_5_valueOrError1).Extract().(DeserializedIntermediateWrappedMaterial)
var _let_tmp_rhs0 DeserializedIntermediateWrappedMaterial = _6_deserializedWrapped
_ = _let_tmp_rhs0
var _7_encryptedPdk _dafny.Sequence = _let_tmp_rhs0.Get_().(DeserializedIntermediateWrappedMaterial_DeserializedIntermediateWrappedMaterial).EncryptedPdk
_ = _7_encryptedPdk
var _8_providerWrappedIkm _dafny.Sequence = _let_tmp_rhs0.Get_().(DeserializedIntermediateWrappedMaterial_DeserializedIntermediateWrappedMaterial).ProviderWrappedIkm
_ = _8_providerWrappedIkm
var _9_valueOrError2 m_Wrappers.Result = m_Wrappers.Result{}
_ = _9_valueOrError2
var _out1 interface{}
_ = _out1
_out1 = (unwrap).Invoke(m_MaterialWrapping.Companion_UnwrapInput_.Create_UnwrapInput_(_8_providerWrappedIkm, algorithmSuite, encryptionContext))
_9_valueOrError2 = _out1.(m_Wrappers.Result)
if (_9_valueOrError2).IsFailure() {
res = (_9_valueOrError2).PropagateFailure()
return res
}
var _10_unwrapOutput m_MaterialWrapping.UnwrapOutput
_ = _10_unwrapOutput
_10_unwrapOutput = (_9_valueOrError2).Extract().(m_MaterialWrapping.UnwrapOutput)
var _let_tmp_rhs1 m_MaterialWrapping.UnwrapOutput = _10_unwrapOutput
_ = _let_tmp_rhs1
var _11_intermediateMaterial _dafny.Sequence = _let_tmp_rhs1.Get_().(m_MaterialWrapping.UnwrapOutput_UnwrapOutput).UnwrappedMaterial
_ = _11_intermediateMaterial
var _12_unwrapInfo interface{} = _let_tmp_rhs1.Get_().(m_MaterialWrapping.UnwrapOutput_UnwrapOutput).UnwrapInfo
_ = _12_unwrapInfo
var _13_valueOrError3 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(Companion_PdkEncryptionAndSymmetricSigningKeys_.Default())
_ = _13_valueOrError3
var _out2 m_Wrappers.Result
_ = _out2
_out2 = Companion_Default___.DeriveKeysFromIntermediateMaterial(_11_intermediateMaterial, algorithmSuite, encryptionContext, _4_cryptoPrimitives)
_13_valueOrError3 = _out2
if (_13_valueOrError3).IsFailure() {
res = (_13_valueOrError3).PropagateFailure()
return res
}
var _14_derivedKeys PdkEncryptionAndSymmetricSigningKeys
_ = _14_derivedKeys
_14_derivedKeys = (_13_valueOrError3).Extract().(PdkEncryptionAndSymmetricSigningKeys)
var _let_tmp_rhs2 PdkEncryptionAndSymmetricSigningKeys = _14_derivedKeys
_ = _let_tmp_rhs2
var _15_pdkEncryptionKey _dafny.Sequence = _let_tmp_rhs2.Get_().(PdkEncryptionAndSymmetricSigningKeys_PdkEncryptionAndSymmetricSigningKeys).PdkEncryptionKey
_ = _15_pdkEncryptionKey
var _16_symmetricSigningKey _dafny.Sequence = _let_tmp_rhs2.Get_().(PdkEncryptionAndSymmetricSigningKeys_PdkEncryptionAndSymmetricSigningKeys).SymmetricSigningKey
_ = _16_symmetricSigningKey
var _17_iv _dafny.Sequence
_ = _17_iv
_17_iv = _dafny.SeqCreate((_dafny.IntOfInt32(m_AlgorithmSuites.Companion_Default___.GetEncryptIvLength(algorithmSuite))).Uint32(), func(coer39 func(_dafny.Int) uint8) func(_dafny.Int) interface{} {
return func(arg40 _dafny.Int) interface{} {
return coer39(arg40)
}
}(func(_18___v0 _dafny.Int) uint8 {
return uint8(0)
}))
var _19_tagIndex _dafny.Int
_ = _19_tagIndex
_19_tagIndex = (_dafny.IntOfUint32((_7_encryptedPdk).Cardinality())).Minus(_dafny.IntOfInt32(m_AlgorithmSuites.Companion_Default___.GetEncryptTagLength(algorithmSuite)))
var _20_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _20_valueOrError4
_20_valueOrError4 = m_CanonicalEncryptionContext.Companion_Default___.EncryptionContextToAAD(encryptionContext)
if (_20_valueOrError4).IsFailure() {
res = (_20_valueOrError4).PropagateFailure()
return res
}
var _21_aad _dafny.Sequence
_ = _21_aad
_21_aad = (_20_valueOrError4).Extract().(_dafny.Sequence)
var _22_decInput m_AwsCryptographyPrimitivesTypes.AESDecryptInput
_ = _22_decInput
_22_decInput = m_AwsCryptographyPrimitivesTypes.Companion_AESDecryptInput_.Create_AESDecryptInput_(((algorithmSuite).Dtor_encrypt()).Dtor_AES__GCM(), _15_pdkEncryptionKey, (_7_encryptedPdk).Take((_19_tagIndex).Uint32()), (_7_encryptedPdk).Drop((_19_tagIndex).Uint32()), _17_iv, _21_aad)
var _23_decOutR m_Wrappers.Result
_ = _23_decOutR
var _out3 m_Wrappers.Result
_ = _out3
_out3 = (_4_cryptoPrimitives).AESDecrypt(_22_decInput)
_23_decOutR = _out3
var _24_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _24_valueOrError5
_24_valueOrError5 = (_23_decOutR).MapFailure(func(coer40 func(m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg41 interface{}) interface{} {
return coer40(arg41.(m_AwsCryptographyPrimitivesTypes.Error))
}
}(func(_25_e m_AwsCryptographyPrimitivesTypes.Error) m_AwsCryptographyMaterialProvidersTypes.Error {
return m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographyPrimitives_(_25_e)
}))
if (_24_valueOrError5).IsFailure() {
res = (_24_valueOrError5).PropagateFailure()
return res
}
var _26_plaintextDataKey _dafny.Sequence
_ = _26_plaintextDataKey
_26_plaintextDataKey = (_24_valueOrError5).Extract().(_dafny.Sequence)
var _27_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _27_valueOrError6
_27_valueOrError6 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_26_plaintextDataKey).Cardinality())).Cmp(_dafny.IntOfInt32(m_AlgorithmSuites.Companion_Default___.GetEncryptKeyLength(algorithmSuite))) == 0, m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("Unexpected AES_GCM Decrypt length")))
if (_27_valueOrError6).IsFailure() {
res = (_27_valueOrError6).PropagateFailure()
return res
}
res = m_Wrappers.Companion_Result_.Create_Success_(Companion_IntermediateUnwrapOutput_.Create_IntermediateUnwrapOutput_(_26_plaintextDataKey, _16_symmetricSigningKey, _12_unwrapInfo))
return res
return res
}