in releases/go/mpl/MrkAwareStrictMultiKeyring/MrkAwareStrictMultiKeyring.go [217:398]
func (_static *CompanionStruct_Default___) MrkAwareStrictMultiKeyring(generator m_Wrappers.Option, awsKmsKeys m_Wrappers.Option, clientSupplier m_AwsCryptographyMaterialProvidersTypes.IClientSupplier, grantTokens m_Wrappers.Option) m_Wrappers.Result {
var output m_Wrappers.Result = m_Wrappers.Result{}
_ = output
var _0_allStrings _dafny.Sequence
_ = _0_allStrings
var _source0 m_Wrappers.Option = generator
_ = _source0
{
{
if _source0.Is_Some() {
var _1_g _dafny.Sequence = _source0.Get_().(m_Wrappers.Option_Some).Value.(_dafny.Sequence)
_ = _1_g
_0_allStrings = _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOf(_1_g), (awsKmsKeys).UnwrapOr(_dafny.SeqOf()).(_dafny.Sequence))
goto Lmatch0
}
}
{
_0_allStrings = (awsKmsKeys).UnwrapOr(_dafny.SeqOf()).(_dafny.Sequence)
}
goto Lmatch0
}
Lmatch0:
var _2_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _2_valueOrError0
_2_valueOrError0 = (m_Seq.Companion_Default___.MapWithResult(func(coer71 func(_dafny.Sequence) m_Wrappers.Result) func(interface{}) m_Wrappers.Result {
return func(arg72 interface{}) m_Wrappers.Result {
return coer71(arg72.(_dafny.Sequence))
}
}(m_AwsArnParsing.Companion_Default___.IsAwsKmsIdentifierString), _0_allStrings)).MapFailure(func(coer72 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg73 interface{}) interface{} {
return coer72(arg73.(_dafny.Sequence))
}
}(m_AwsKmsUtils.Companion_Default___.WrapStringToError))
if (_2_valueOrError0).IsFailure() {
output = (_2_valueOrError0).PropagateFailure()
return output
}
var _3_allIdentifiers _dafny.Sequence
_ = _3_allIdentifiers
_3_allIdentifiers = (_2_valueOrError0).Extract().(_dafny.Sequence)
var _4_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _4_valueOrError1
_4_valueOrError1 = m_AwsKmsMrkAreUnique.Companion_Default___.AwsKmsMrkAreUnique(_3_allIdentifiers)
if (_4_valueOrError1).IsFailure() {
output = (_4_valueOrError1).PropagateFailure()
return output
}
var _5_generatorKeyring m_Wrappers.Option = m_Wrappers.Companion_Option_.Default()
_ = _5_generatorKeyring
var _source1 m_Wrappers.Option = generator
_ = _source1
{
{
if _source1.Is_Some() {
var _6_generatorIdentifier _dafny.Sequence = _source1.Get_().(m_Wrappers.Option_Some).Value.(_dafny.Sequence)
_ = _6_generatorIdentifier
var _7_valueOrError2 m_Wrappers.Result = m_Wrappers.Result{}
_ = _7_valueOrError2
_7_valueOrError2 = (m_AwsArnParsing.Companion_Default___.IsAwsKmsIdentifierString(_6_generatorIdentifier)).MapFailure(func(coer73 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg74 interface{}) interface{} {
return coer73(arg74.(_dafny.Sequence))
}
}(m_AwsKmsUtils.Companion_Default___.WrapStringToError))
if (_7_valueOrError2).IsFailure() {
output = (_7_valueOrError2).PropagateFailure()
return output
}
var _8_arn m_AwsArnParsing.AwsKmsIdentifier
_ = _8_arn
_8_arn = (_7_valueOrError2).Extract().(m_AwsArnParsing.AwsKmsIdentifier)
var _9_region m_Wrappers.Option
_ = _9_region
_9_region = m_AwsArnParsing.Companion_Default___.GetRegion(_8_arn)
var _10_valueOrError3 m_Wrappers.Result = m_Wrappers.Result{}
_ = _10_valueOrError3
var _out0 m_Wrappers.Result
_ = _out0
_out0 = (clientSupplier).GetClient(m_AwsCryptographyMaterialProvidersTypes.Companion_GetClientInput_.Create_GetClientInput_((_9_region).UnwrapOr(_dafny.SeqOfString("")).(_dafny.Sequence)))
_10_valueOrError3 = _out0
if (_10_valueOrError3).IsFailure() {
output = (_10_valueOrError3).PropagateFailure()
return output
}
var _11_client m_ComAmazonawsKmsTypes.IKMSClient
_ = _11_client
_11_client = m_ComAmazonawsKmsTypes.Companion_IKMSClient_.CastTo_((_10_valueOrError3).Extract())
var _12_g *m_AwsKmsMrkKeyring.AwsKmsMrkKeyring
_ = _12_g
var _nw0 *m_AwsKmsMrkKeyring.AwsKmsMrkKeyring = m_AwsKmsMrkKeyring.New_AwsKmsMrkKeyring_()
_ = _nw0
_nw0.Ctor__(_11_client, _6_generatorIdentifier, (grantTokens).UnwrapOr(_dafny.SeqOf()).(_dafny.Sequence))
_12_g = _nw0
_5_generatorKeyring = m_Wrappers.Companion_Option_.Create_Some_(_12_g)
goto Lmatch1
}
}
{
_5_generatorKeyring = m_Wrappers.Companion_Option_.Create_None_()
}
goto Lmatch1
}
Lmatch1:
var _13_children _dafny.Sequence
_ = _13_children
_13_children = _dafny.SeqOf()
var _source2 m_Wrappers.Option = awsKmsKeys
_ = _source2
{
{
if _source2.Is_Some() {
var _14_childIdentifiers _dafny.Sequence = _source2.Get_().(m_Wrappers.Option_Some).Value.(_dafny.Sequence)
_ = _14_childIdentifiers
var _hi0 _dafny.Int = _dafny.IntOfUint32((_14_childIdentifiers).Cardinality())
_ = _hi0
for _15_index := _dafny.Zero; _15_index.Cmp(_hi0) < 0; _15_index = _15_index.Plus(_dafny.One) {
var _16_childIdentifier _dafny.Sequence
_ = _16_childIdentifier
_16_childIdentifier = (_14_childIdentifiers).Select((_15_index).Uint32()).(_dafny.Sequence)
var _17_valueOrError4 m_Wrappers.Result = m_Wrappers.Result{}
_ = _17_valueOrError4
_17_valueOrError4 = (m_AwsArnParsing.Companion_Default___.IsAwsKmsIdentifierString(_16_childIdentifier)).MapFailure(func(coer74 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg75 interface{}) interface{} {
return coer74(arg75.(_dafny.Sequence))
}
}(m_AwsKmsUtils.Companion_Default___.WrapStringToError))
if (_17_valueOrError4).IsFailure() {
output = (_17_valueOrError4).PropagateFailure()
return output
}
var _18_info m_AwsArnParsing.AwsKmsIdentifier
_ = _18_info
_18_info = (_17_valueOrError4).Extract().(m_AwsArnParsing.AwsKmsIdentifier)
var _19_region m_Wrappers.Option
_ = _19_region
_19_region = m_AwsArnParsing.Companion_Default___.GetRegion(_18_info)
var _20_valueOrError5 m_Wrappers.Result = m_Wrappers.Result{}
_ = _20_valueOrError5
var _out1 m_Wrappers.Result
_ = _out1
_out1 = (clientSupplier).GetClient(m_AwsCryptographyMaterialProvidersTypes.Companion_GetClientInput_.Create_GetClientInput_((_19_region).UnwrapOr(_dafny.SeqOfString("")).(_dafny.Sequence)))
_20_valueOrError5 = _out1
if (_20_valueOrError5).IsFailure() {
output = (_20_valueOrError5).PropagateFailure()
return output
}
var _21_client m_ComAmazonawsKmsTypes.IKMSClient
_ = _21_client
_21_client = m_ComAmazonawsKmsTypes.Companion_IKMSClient_.CastTo_((_20_valueOrError5).Extract())
var _22_keyring *m_AwsKmsMrkKeyring.AwsKmsMrkKeyring
_ = _22_keyring
var _nw1 *m_AwsKmsMrkKeyring.AwsKmsMrkKeyring = m_AwsKmsMrkKeyring.New_AwsKmsMrkKeyring_()
_ = _nw1
_nw1.Ctor__(_21_client, _16_childIdentifier, (grantTokens).UnwrapOr(_dafny.SeqOf()).(_dafny.Sequence))
_22_keyring = _nw1
_13_children = _dafny.Companion_Sequence_.Concatenate(_13_children, _dafny.SeqOf(_22_keyring))
}
goto Lmatch2
}
}
{
_13_children = _dafny.SeqOf()
}
goto Lmatch2
}
Lmatch2:
var _23_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _23_valueOrError6
_23_valueOrError6 = m_Wrappers.Companion_Default___.Need(((_5_generatorKeyring).Is_Some()) || ((_dafny.IntOfUint32((_13_children).Cardinality())).Sign() == 1), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("generatorKeyring or child Keyrings needed to create a multi keyring")))
if (_23_valueOrError6).IsFailure() {
output = (_23_valueOrError6).PropagateFailure()
return output
}
var _24_keyring *m_MultiKeyring.MultiKeyring
_ = _24_keyring
var _nw2 *m_MultiKeyring.MultiKeyring = m_MultiKeyring.New_MultiKeyring_()
_ = _nw2
_nw2.Ctor__(_5_generatorKeyring, _13_children)
_24_keyring = _nw2
output = m_Wrappers.Companion_Result_.Create_Success_(_24_keyring)
return output
return output
}