in releases/go/mpl/AwsCryptographyKeyStoreOperations/AwsCryptographyKeyStoreOperations.go [211:363]
func (_static *CompanionStruct_Default___) CreateKey(config Config, input m_AwsCryptographyKeyStoreTypes.CreateKeyInput) m_Wrappers.Result {
var output m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyKeyStoreTypes.Companion_CreateKeyOutput_.Default())
_ = output
var _0_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _0_valueOrError0
_0_valueOrError0 = m_Wrappers.Companion_Default___.Need(!(((input).Dtor_branchKeyIdentifier()).Is_Some()) || ((((input).Dtor_encryptionContext()).Is_Some()) && (((((input).Dtor_encryptionContext()).Dtor_value().(_dafny.Map)).Cardinality()).Sign() == 1)), m_AwsCryptographyKeyStoreTypes.Companion_Error_.Create_KeyStoreException_(m_KeyStoreErrorMessages.Companion_Default___.CUSTOM__BRANCH__KEY__ID__NEED__EC()))
if (_0_valueOrError0).IsFailure() {
output = (_0_valueOrError0).PropagateFailure()
return output
}
var _1_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _1_valueOrError1
_1_valueOrError1 = m_Wrappers.Companion_Default___.Need(m_KMSKeystoreOperations.Companion_Default___.HasKeyId((config).Dtor_kmsConfiguration()), m_AwsCryptographyKeyStoreTypes.Companion_Error_.Create_KeyStoreException_(m_KeyStoreErrorMessages.Companion_Default___.DISCOVERY__CREATE__KEY__NOT__SUPPORTED()))
if (_1_valueOrError1).IsFailure() {
output = (_1_valueOrError1).PropagateFailure()
return output
}
var _2_branchKeyIdentifier _dafny.Sequence = _dafny.EmptySeq.SetString()
_ = _2_branchKeyIdentifier
if ((input).Dtor_branchKeyIdentifier()).Is_None() {
var _3_maybeBranchKeyId m_Wrappers.Result
_ = _3_maybeBranchKeyId
var _out0 m_Wrappers.Result
_ = _out0
_out0 = m_UUID.GenerateUUID()
_3_maybeBranchKeyId = _out0
var _4_valueOrError2 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq.SetString())
_ = _4_valueOrError2
_4_valueOrError2 = (_3_maybeBranchKeyId).MapFailure(func(coer19 func(_dafny.Sequence) m_AwsCryptographyKeyStoreTypes.Error) func(interface{}) interface{} {
return func(arg19 interface{}) interface{} {
return coer19(arg19.(_dafny.Sequence))
}
}(func(_5_e _dafny.Sequence) m_AwsCryptographyKeyStoreTypes.Error {
return m_AwsCryptographyKeyStoreTypes.Companion_Error_.Create_KeyStoreException_(_5_e)
}))
if (_4_valueOrError2).IsFailure() {
output = (_4_valueOrError2).PropagateFailure()
return output
}
_2_branchKeyIdentifier = (_4_valueOrError2).Extract().(_dafny.Sequence)
} else {
var _6_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _6_valueOrError3
_6_valueOrError3 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((((input).Dtor_branchKeyIdentifier()).Dtor_value().(_dafny.Sequence)).Cardinality())).Sign() == 1, m_AwsCryptographyKeyStoreTypes.Companion_Error_.Create_KeyStoreException_(_dafny.SeqOfString("Custom branch key id can not be an empty string.")))
if (_6_valueOrError3).IsFailure() {
output = (_6_valueOrError3).PropagateFailure()
return output
}
_2_branchKeyIdentifier = ((input).Dtor_branchKeyIdentifier()).Dtor_value().(_dafny.Sequence)
}
var _7_timestamp_q m_Wrappers.Result
_ = _7_timestamp_q
var _out1 m_Wrappers.Result
_ = _out1
_out1 = m__Time.GetCurrentTimeStamp()
_7_timestamp_q = _out1
var _8_valueOrError4 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq.SetString())
_ = _8_valueOrError4
_8_valueOrError4 = (_7_timestamp_q).MapFailure(func(coer20 func(_dafny.Sequence) m_AwsCryptographyKeyStoreTypes.Error) func(interface{}) interface{} {
return func(arg20 interface{}) interface{} {
return coer20(arg20.(_dafny.Sequence))
}
}(func(_9_e _dafny.Sequence) m_AwsCryptographyKeyStoreTypes.Error {
return m_AwsCryptographyKeyStoreTypes.Companion_Error_.Create_KeyStoreException_(_9_e)
}))
if (_8_valueOrError4).IsFailure() {
output = (_8_valueOrError4).PropagateFailure()
return output
}
var _10_timestamp _dafny.Sequence
_ = _10_timestamp
_10_timestamp = (_8_valueOrError4).Extract().(_dafny.Sequence)
var _11_maybeBranchKeyVersion m_Wrappers.Result
_ = _11_maybeBranchKeyVersion
var _out2 m_Wrappers.Result
_ = _out2
_out2 = m_UUID.GenerateUUID()
_11_maybeBranchKeyVersion = _out2
var _12_valueOrError5 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq.SetString())
_ = _12_valueOrError5
_12_valueOrError5 = (_11_maybeBranchKeyVersion).MapFailure(func(coer21 func(_dafny.Sequence) m_AwsCryptographyKeyStoreTypes.Error) func(interface{}) interface{} {
return func(arg21 interface{}) interface{} {
return coer21(arg21.(_dafny.Sequence))
}
}(func(_13_e _dafny.Sequence) m_AwsCryptographyKeyStoreTypes.Error {
return m_AwsCryptographyKeyStoreTypes.Companion_Error_.Create_KeyStoreException_(_13_e)
}))
if (_12_valueOrError5).IsFailure() {
output = (_12_valueOrError5).PropagateFailure()
return output
}
var _14_branchKeyVersion _dafny.Sequence
_ = _14_branchKeyVersion
_14_branchKeyVersion = (_12_valueOrError5).Extract().(_dafny.Sequence)
var _15_unwrapEncryptionContext _dafny.Map
_ = _15_unwrapEncryptionContext
_15_unwrapEncryptionContext = ((input).Dtor_encryptionContext()).UnwrapOr(_dafny.NewMapBuilder().ToMap()).(_dafny.Map)
var _16_encodedEncryptionContext _dafny.Set
_ = _16_encodedEncryptionContext
_16_encodedEncryptionContext = func() _dafny.Set {
var _coll0 = _dafny.NewBuilder()
_ = _coll0
for _iter7 := _dafny.Iterate((_15_unwrapEncryptionContext).Keys().Elements()); ; {
_compr_0, _ok7 := _iter7()
if !_ok7 {
break
}
var _17_k _dafny.Sequence
_17_k = interface{}(_compr_0).(_dafny.Sequence)
if m_UTF8.Companion_ValidUTF8Bytes_.Is_(_17_k) {
if (_15_unwrapEncryptionContext).Contains(_17_k) {
_coll0.Add(_dafny.TupleOf(m_UTF8.Decode(_17_k), m_UTF8.Decode((_15_unwrapEncryptionContext).Get(_17_k).(_dafny.Sequence)), _17_k))
}
}
}
return _coll0.ToSet()
}()
var _18_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _18_valueOrError6
_18_valueOrError6 = m_Wrappers.Companion_Default___.Need(_dafny.Quantifier((_16_encodedEncryptionContext).Elements(), true, func(_forall_var_0 _dafny.Tuple) bool {
var _19_i _dafny.Tuple
_19_i = interface{}(_forall_var_0).(_dafny.Tuple)
return !((_16_encodedEncryptionContext).Contains(_19_i)) || ((((((*(_19_i).IndexInt(0)).(m_Wrappers.Result)).Is_Success()) && (((*(_19_i).IndexInt(1)).(m_Wrappers.Result)).Is_Success())) && (m_ComAmazonawsDynamodbTypes.Companion_Default___.IsValid__AttributeName(_dafny.Companion_Sequence_.Concatenate(m_Structure.Companion_Default___.ENCRYPTION__CONTEXT__PREFIX(), ((*(_19_i).IndexInt(0)).(m_Wrappers.Result)).Dtor_value().(_dafny.Sequence))))) && (func(_pat_let1_0 m_Wrappers.Result) bool {
return func(_20_encoded m_Wrappers.Result) bool {
return ((_20_encoded).Is_Success()) && (_dafny.Companion_Sequence_.Equal((*(_19_i).IndexInt(2)).(_dafny.Sequence), (_20_encoded).Dtor_value().(_dafny.Sequence)))
}(_pat_let1_0)
}(m_UTF8.Encode(((*(_19_i).IndexInt(0)).(m_Wrappers.Result)).Dtor_value().(_dafny.Sequence)))))
}), m_AwsCryptographyKeyStoreTypes.Companion_Error_.Create_KeyStoreException_(m_KeyStoreErrorMessages.Companion_Default___.UTF8__ENCODING__ENCRYPTION__CONTEXT__ERROR()))
if (_18_valueOrError6).IsFailure() {
output = (_18_valueOrError6).PropagateFailure()
return output
}
var _out3 m_Wrappers.Result
_ = _out3
_out3 = m_CreateKeys.Companion_Default___.CreateBranchAndBeaconKeys(_2_branchKeyIdentifier, func() _dafny.Map {
var _coll1 = _dafny.NewMapBuilder()
_ = _coll1
for _iter8 := _dafny.Iterate((_16_encodedEncryptionContext).Elements()); ; {
_compr_1, _ok8 := _iter8()
if !_ok8 {
break
}
var _21_i _dafny.Tuple
_21_i = interface{}(_compr_1).(_dafny.Tuple)
if (_16_encodedEncryptionContext).Contains(_21_i) {
_coll1.Add(((*(_21_i).IndexInt(0)).(m_Wrappers.Result)).Dtor_value().(_dafny.Sequence), ((*(_21_i).IndexInt(1)).(m_Wrappers.Result)).Dtor_value().(_dafny.Sequence))
}
}
return _coll1.ToMap()
}(), _10_timestamp, _14_branchKeyVersion, (config).Dtor_ddbTableName(), (config).Dtor_logicalKeyStoreName(), (config).Dtor_kmsConfiguration(), (config).Dtor_grantTokens(), (config).Dtor_kmsClient(), (config).Dtor_ddbClient())
output = _out3
return output
}