in releases/go/mpl/StrictMultiKeyring/StrictMultiKeyring.go [205:379]
func (_static *CompanionStruct_Default___) StrictMultiKeyring(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(coer59 func(_dafny.Sequence) m_Wrappers.Result) func(interface{}) m_Wrappers.Result {
return func(arg60 interface{}) m_Wrappers.Result {
return coer59(arg60.(_dafny.Sequence))
}
}(m_AwsArnParsing.Companion_Default___.IsAwsKmsIdentifierString), _0_allStrings)).MapFailure(func(coer60 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg61 interface{}) interface{} {
return coer60(arg61.(_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_generatorKeyring m_Wrappers.Option = m_Wrappers.Companion_Option_.Default()
_ = _4_generatorKeyring
var _source1 m_Wrappers.Option = generator
_ = _source1
{
{
if _source1.Is_Some() {
var _5_generatorIdentifier _dafny.Sequence = _source1.Get_().(m_Wrappers.Option_Some).Value.(_dafny.Sequence)
_ = _5_generatorIdentifier
var _6_valueOrError1 m_Wrappers.Result = m_Wrappers.Result{}
_ = _6_valueOrError1
_6_valueOrError1 = (m_AwsArnParsing.Companion_Default___.IsAwsKmsIdentifierString(_5_generatorIdentifier)).MapFailure(func(coer61 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg62 interface{}) interface{} {
return coer61(arg62.(_dafny.Sequence))
}
}(m_AwsKmsUtils.Companion_Default___.WrapStringToError))
if (_6_valueOrError1).IsFailure() {
output = (_6_valueOrError1).PropagateFailure()
return output
}
var _7_arn m_AwsArnParsing.AwsKmsIdentifier
_ = _7_arn
_7_arn = (_6_valueOrError1).Extract().(m_AwsArnParsing.AwsKmsIdentifier)
var _8_region m_Wrappers.Option
_ = _8_region
_8_region = m_AwsArnParsing.Companion_Default___.GetRegion(_7_arn)
var _9_valueOrError2 m_Wrappers.Result = m_Wrappers.Result{}
_ = _9_valueOrError2
var _out0 m_Wrappers.Result
_ = _out0
_out0 = (clientSupplier).GetClient(m_AwsCryptographyMaterialProvidersTypes.Companion_GetClientInput_.Create_GetClientInput_((_8_region).UnwrapOr(_dafny.SeqOfString("")).(_dafny.Sequence)))
_9_valueOrError2 = _out0
if (_9_valueOrError2).IsFailure() {
output = (_9_valueOrError2).PropagateFailure()
return output
}
var _10_client m_ComAmazonawsKmsTypes.IKMSClient
_ = _10_client
_10_client = m_ComAmazonawsKmsTypes.Companion_IKMSClient_.CastTo_((_9_valueOrError2).Extract())
var _11_g *m_AwsKmsKeyring.AwsKmsKeyring
_ = _11_g
var _nw0 *m_AwsKmsKeyring.AwsKmsKeyring = m_AwsKmsKeyring.New_AwsKmsKeyring_()
_ = _nw0
_nw0.Ctor__(_10_client, _5_generatorIdentifier, (grantTokens).UnwrapOr(_dafny.SeqOf()).(_dafny.Sequence))
_11_g = _nw0
_4_generatorKeyring = m_Wrappers.Companion_Option_.Create_Some_(_11_g)
goto Lmatch1
}
}
{
_4_generatorKeyring = m_Wrappers.Companion_Option_.Create_None_()
}
goto Lmatch1
}
Lmatch1:
var _12_children _dafny.Sequence
_ = _12_children
_12_children = _dafny.SeqOf()
var _source2 m_Wrappers.Option = awsKmsKeys
_ = _source2
{
{
if _source2.Is_Some() {
var _13_childIdentifiers _dafny.Sequence = _source2.Get_().(m_Wrappers.Option_Some).Value.(_dafny.Sequence)
_ = _13_childIdentifiers
var _hi0 _dafny.Int = _dafny.IntOfUint32((_13_childIdentifiers).Cardinality())
_ = _hi0
for _14_index := _dafny.Zero; _14_index.Cmp(_hi0) < 0; _14_index = _14_index.Plus(_dafny.One) {
var _15_childIdentifier _dafny.Sequence
_ = _15_childIdentifier
_15_childIdentifier = (_13_childIdentifiers).Select((_14_index).Uint32()).(_dafny.Sequence)
var _16_valueOrError3 m_Wrappers.Result = m_Wrappers.Result{}
_ = _16_valueOrError3
_16_valueOrError3 = (m_AwsArnParsing.Companion_Default___.IsAwsKmsIdentifierString(_15_childIdentifier)).MapFailure(func(coer62 func(_dafny.Sequence) m_AwsCryptographyMaterialProvidersTypes.Error) func(interface{}) interface{} {
return func(arg63 interface{}) interface{} {
return coer62(arg63.(_dafny.Sequence))
}
}(m_AwsKmsUtils.Companion_Default___.WrapStringToError))
if (_16_valueOrError3).IsFailure() {
output = (_16_valueOrError3).PropagateFailure()
return output
}
var _17_info m_AwsArnParsing.AwsKmsIdentifier
_ = _17_info
_17_info = (_16_valueOrError3).Extract().(m_AwsArnParsing.AwsKmsIdentifier)
var _18_region m_Wrappers.Option
_ = _18_region
_18_region = m_AwsArnParsing.Companion_Default___.GetRegion(_17_info)
var _19_valueOrError4 m_Wrappers.Result = m_Wrappers.Result{}
_ = _19_valueOrError4
var _out1 m_Wrappers.Result
_ = _out1
_out1 = (clientSupplier).GetClient(m_AwsCryptographyMaterialProvidersTypes.Companion_GetClientInput_.Create_GetClientInput_((_18_region).UnwrapOr(_dafny.SeqOfString("")).(_dafny.Sequence)))
_19_valueOrError4 = _out1
if (_19_valueOrError4).IsFailure() {
output = (_19_valueOrError4).PropagateFailure()
return output
}
var _20_client m_ComAmazonawsKmsTypes.IKMSClient
_ = _20_client
_20_client = m_ComAmazonawsKmsTypes.Companion_IKMSClient_.CastTo_((_19_valueOrError4).Extract())
var _21_keyring *m_AwsKmsKeyring.AwsKmsKeyring
_ = _21_keyring
var _nw1 *m_AwsKmsKeyring.AwsKmsKeyring = m_AwsKmsKeyring.New_AwsKmsKeyring_()
_ = _nw1
_nw1.Ctor__(_20_client, _15_childIdentifier, (grantTokens).UnwrapOr(_dafny.SeqOf()).(_dafny.Sequence))
_21_keyring = _nw1
_12_children = _dafny.Companion_Sequence_.Concatenate(_12_children, _dafny.SeqOf(_21_keyring))
}
goto Lmatch2
}
}
{
_12_children = _dafny.SeqOf()
}
goto Lmatch2
}
Lmatch2:
var _22_valueOrError5 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default()
_ = _22_valueOrError5
_22_valueOrError5 = m_Wrappers.Companion_Default___.Need(((_4_generatorKeyring).Is_Some()) || ((_dafny.IntOfUint32((_12_children).Cardinality())).Sign() == 1), m_AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_AwsCryptographicMaterialProvidersException_(_dafny.SeqOfString("generatorKeyring or child Keryings needed to create a multi keyring")))
if (_22_valueOrError5).IsFailure() {
output = (_22_valueOrError5).PropagateFailure()
return output
}
var _23_keyring *m_MultiKeyring.MultiKeyring
_ = _23_keyring
var _nw2 *m_MultiKeyring.MultiKeyring = m_MultiKeyring.New_MultiKeyring_()
_ = _nw2
_nw2.Ctor__(_4_generatorKeyring, _12_children)
_23_keyring = _nw2
output = m_Wrappers.Companion_Result_.Create_Success_(_23_keyring)
return output
return output
}