in releases/go/encryption-sdk/AwsEncryptionSdkOperations/AwsEncryptionSdkOperations.go [292:476]
func (_static *CompanionStruct_Default___) Encrypt(config Config, input m_AwsCryptographyEncryptionSdkTypes.EncryptInput) m_Wrappers.Result {
var output m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyEncryptionSdkTypes.Companion_EncryptOutput_.Default())
_ = output
var _0_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(int64(0))
_ = _0_valueOrError1
if ((input).Dtor_frameLength()).Is_Some() {
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((int64(0)) < (((input).Dtor_frameLength()).Dtor_value().(int64))) && ((((input).Dtor_frameLength()).Dtor_value().(int64)) <= (int64(4294967295))), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("FrameLength must be greater than 0 and less than 2^32")))
_ = _1_valueOrError0
if (_1_valueOrError0).IsFailure() {
_0_valueOrError1 = (_1_valueOrError0).PropagateFailure()
} else {
_0_valueOrError1 = m_Wrappers.Companion_Result_.Create_Success_(((input).Dtor_frameLength()).Dtor_value().(int64))
}
} else {
_0_valueOrError1 = m_Wrappers.Companion_Result_.Create_Success_(m_EncryptDecryptHelpers.Companion_Default___.DEFAULT__FRAME__LENGTH())
}
if (_0_valueOrError1).IsFailure() {
output = (_0_valueOrError1).PropagateFailure()
return output
}
var _2_frameLength int64
_ = _2_frameLength
_2_frameLength = (_0_valueOrError1).Extract().(int64)
var _3_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _3_valueOrError2
_3_valueOrError2 = m_EncryptDecryptHelpers.Companion_Default___.ValidateEncryptionContext((input).Dtor_encryptionContext())
if (_3_valueOrError2).IsFailure() {
output = (_3_valueOrError2).PropagateFailure()
return output
}
var _4_encryptionContext _dafny.Map
_ = _4_encryptionContext
if ((input).Dtor_encryptionContext()).Is_Some() {
_4_encryptionContext = ((input).Dtor_encryptionContext()).Dtor_value().(_dafny.Map)
} else {
_4_encryptionContext = _dafny.NewMapBuilder().ToMap()
}
var _5_valueOrError3 m_Wrappers.Result = m_Wrappers.Result{}
_ = _5_valueOrError3
var _out0 m_Wrappers.Result
_ = _out0
_out0 = m_EncryptDecryptHelpers.Companion_Default___.CreateCmmFromInput((input).Dtor_materialsManager(), (input).Dtor_keyring())
_5_valueOrError3 = _out0
if (_5_valueOrError3).IsFailure() {
output = (_5_valueOrError3).PropagateFailure()
return output
}
var _6_cmm m_AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager
_ = _6_cmm
_6_cmm = m_AwsCryptographyMaterialProvidersTypes.Companion_ICryptographicMaterialsManager_.CastTo_((_5_valueOrError3).Extract())
var _7_algorithmSuiteId m_Wrappers.Option
_ = _7_algorithmSuiteId
if ((input).Dtor_algorithmSuiteId()).Is_Some() {
_7_algorithmSuiteId = m_Wrappers.Companion_Option_.Create_Some_(m_AwsCryptographyMaterialProvidersTypes.Companion_AlgorithmSuiteId_.Create_ESDK_(((input).Dtor_algorithmSuiteId()).Dtor_value().(m_AwsCryptographyMaterialProvidersTypes.ESDKAlgorithmSuiteId)))
} else {
_7_algorithmSuiteId = m_Wrappers.Companion_Option_.Create_None_()
}
if (_7_algorithmSuiteId).Is_Some() {
var _8_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.TupleOf())
_ = _8_valueOrError4
_8_valueOrError4 = (((config).Dtor_mpl()).ValidateCommitmentPolicyOnEncrypt(m_AwsCryptographyMaterialProvidersTypes.Companion_ValidateCommitmentPolicyOnEncryptInput_.Create_ValidateCommitmentPolicyOnEncryptInput_((_7_algorithmSuiteId).Dtor_value().(m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteId), m_AwsCryptographyMaterialProvidersTypes.Companion_CommitmentPolicy_.Create_ESDK_((config).Dtor_commitmentPolicy())))).MapFailure(func(coer30 func(m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} {
return func(arg31 interface{}) interface{} {
return coer30(arg31.(m_AwsCryptographyMaterialProvidersTypes.Error))
}
}(func(_9_e m_AwsCryptographyMaterialProvidersTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error {
return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsCryptographyMaterialProviders_(_9_e)
}))
if (_8_valueOrError4).IsFailure() {
output = (_8_valueOrError4).PropagateFailure()
return output
}
var _10___v0 _dafny.Tuple
_ = _10___v0
_10___v0 = (_8_valueOrError4).Extract().(_dafny.Tuple)
}
var _11_valueOrError5 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _11_valueOrError5
_11_valueOrError5 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((input).Dtor_plaintext()).Cardinality())).Cmp(m_StandardLibrary_UInt.Companion_Default___.INT64__MAX__LIMIT()) < 0, m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Plaintext exceeds maximum allowed size")))
if (_11_valueOrError5).IsFailure() {
output = (_11_valueOrError5).PropagateFailure()
return output
}
var _12_valueOrError6 m_Wrappers.Result = m_Wrappers.Result{}
_ = _12_valueOrError6
var _out1 m_Wrappers.Result
_ = _out1
_out1 = m_EncryptDecryptHelpers.Companion_Default___.GetEncryptionMaterials(_6_cmm, _7_algorithmSuiteId, _4_encryptionContext, int64(((input).Dtor_plaintext()).Cardinality()), (config).Dtor_commitmentPolicy(), (config).Dtor_mpl())
_12_valueOrError6 = _out1
if (_12_valueOrError6).IsFailure() {
output = (_12_valueOrError6).PropagateFailure()
return output
}
var _13_materials m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials
_ = _13_materials
_13_materials = (_12_valueOrError6).Extract().(m_AwsCryptographyMaterialProvidersTypes.EncryptionMaterials)
var _14_valueOrError7 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _14_valueOrError7
_14_valueOrError7 = m_Wrappers.Companion_Default___.Need((((_13_materials).Dtor_algorithmSuite()).Dtor_id()).Is_ESDK(), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Encryption materials contain incompatible algorithm suite for the AWS Encryption SDK.")))
if (_14_valueOrError7).IsFailure() {
output = (_14_valueOrError7).PropagateFailure()
return output
}
var _15_valueOrError8 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _15_valueOrError8
_15_valueOrError8 = m_EncryptDecryptHelpers.Companion_Default___.ValidateMaxEncryptedDataKeys((config).Dtor_maxEncryptedDataKeys(), (_13_materials).Dtor_encryptedDataKeys())
if (_15_valueOrError8).IsFailure() {
output = (_15_valueOrError8).PropagateFailure()
return output
}
var _16_encryptedDataKeys _dafny.Sequence
_ = _16_encryptedDataKeys
_16_encryptedDataKeys = (_13_materials).Dtor_encryptedDataKeys()
var _17_valueOrError9 m_Wrappers.Result = m_Wrappers.Result{}
_ = _17_valueOrError9
var _out2 m_Wrappers.Result
_ = _out2
_out2 = m_EncryptDecryptHelpers.Companion_Default___.GenerateMessageId((_13_materials).Dtor_algorithmSuite(), (config).Dtor_crypto())
_17_valueOrError9 = _out2
if (_17_valueOrError9).IsFailure() {
output = (_17_valueOrError9).PropagateFailure()
return output
}
var _18_messageId _dafny.Sequence
_ = _18_messageId
_18_messageId = (_17_valueOrError9).Extract().(_dafny.Sequence)
var _19_maybeDerivedDataKeys m_Wrappers.Result
_ = _19_maybeDerivedDataKeys
var _out3 m_Wrappers.Result
_ = _out3
_out3 = m_KeyDerivation.Companion_Default___.DeriveKeys(_18_messageId, ((_13_materials).Dtor_plaintextDataKey()).Dtor_value().(_dafny.Sequence), (_13_materials).Dtor_algorithmSuite(), (config).Dtor_crypto(), (config).Dtor_netV4__0__0__RetryPolicy(), false)
_19_maybeDerivedDataKeys = _out3
var _20_valueOrError10 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_KeyDerivation.Companion_ExpandedKeyMaterial_.Default())
_ = _20_valueOrError10
_20_valueOrError10 = (_19_maybeDerivedDataKeys).MapFailure(func(coer31 func(m_AwsCryptographyEncryptionSdkTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error) func(interface{}) interface{} {
return func(arg32 interface{}) interface{} {
return coer31(arg32.(m_AwsCryptographyEncryptionSdkTypes.Error))
}
}(func(_21_e m_AwsCryptographyEncryptionSdkTypes.Error) m_AwsCryptographyEncryptionSdkTypes.Error {
return m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Failed to derive data keys"))
}))
if (_20_valueOrError10).IsFailure() {
output = (_20_valueOrError10).PropagateFailure()
return output
}
var _22_derivedDataKeys m_KeyDerivation.ExpandedKeyMaterial
_ = _22_derivedDataKeys
_22_derivedDataKeys = (_20_valueOrError10).Extract().(m_KeyDerivation.ExpandedKeyMaterial)
var _23_maybeHeader m_Wrappers.Result
_ = _23_maybeHeader
var _out4 m_Wrappers.Result
_ = _out4
_out4 = m_EncryptDecryptHelpers.Companion_Default___.BuildHeaderForEncrypt(_18_messageId, (_13_materials).Dtor_algorithmSuite(), (_13_materials).Dtor_encryptionContext(), (_13_materials).Dtor_requiredEncryptionContextKeys(), _16_encryptedDataKeys, uint32(_2_frameLength), _22_derivedDataKeys, (config).Dtor_crypto())
_23_maybeHeader = _out4
var _24_valueOrError11 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _24_valueOrError11
_24_valueOrError11 = m_Wrappers.Companion_Default___.Need((_23_maybeHeader).Is_Success(), m_AwsCryptographyEncryptionSdkTypes.Companion_Error_.Create_AwsEncryptionSdkException_(_dafny.SeqOfString("Failed to build header body")))
if (_24_valueOrError11).IsFailure() {
output = (_24_valueOrError11).PropagateFailure()
return output
}
var _25_header m_Header.HeaderInfo
_ = _25_header
_25_header = (_23_maybeHeader).Dtor_value().(m_Header.HeaderInfo)
var _26_valueOrError12 m_Wrappers.Result = m_Wrappers.Result{}
_ = _26_valueOrError12
var _out5 m_Wrappers.Result
_ = _out5
_out5 = m_MessageBody.Companion_Default___.EncryptMessageBody((input).Dtor_plaintext(), _25_header, (_22_derivedDataKeys).Dtor_dataKey(), (config).Dtor_crypto())
_26_valueOrError12 = _out5
if (_26_valueOrError12).IsFailure() {
output = (_26_valueOrError12).PropagateFailure()
return output
}
var _27_framedMessage m_MessageBody.FramedMessageBody
_ = _27_framedMessage
_27_framedMessage = (_26_valueOrError12).Extract().(m_MessageBody.FramedMessageBody)
var _28_maybeSignedMessage m_Wrappers.Result
_ = _28_maybeSignedMessage
var _out6 m_Wrappers.Result
_ = _out6
_out6 = Companion_Default___.SignAndSerializeMessage(config, _25_header, _27_framedMessage, _13_materials)
_28_maybeSignedMessage = _out6
output = _28_maybeSignedMessage
return output
}