func()

in releases/go/encryption-sdk/EncryptDecryptHelpers/EncryptDecryptHelpers.go [508:608]

• 101 lines of code
• 14 McCabe index (conditional complexity)

func (_static *CompanionStruct_Default___) BuildHeaderForEncrypt(messageId _dafny.Sequence, suite m_AwsCryptographyMaterialProvidersTypes.AlgorithmSuiteInfo, encryptionContext _dafny.Map, requiredEncryptionContextKeys _dafny.Sequence, encryptedDataKeys _dafny.Sequence, frameLength uint32, derivedDataKeys m_KeyDerivation.ExpandedKeyMaterial, crypto *m_AtomicPrimitives.AtomicPrimitivesClient) m_Wrappers.Result {
	var res m_Wrappers.Result = m_Wrappers.Result{}
	_ = res
	var _0_reqKeySet _dafny.Set
	_ = _0_reqKeySet
	_0_reqKeySet = func() _dafny.Set {
		var _coll0 = _dafny.NewBuilder()
		_ = _coll0
		for _iter2 := _dafny.Iterate((requiredEncryptionContextKeys).Elements()); ; {
			_compr_0, _ok2 := _iter2()
			if !_ok2 {
				break
			}
			var _1_k _dafny.Sequence
			_1_k = interface{}(_compr_0).(_dafny.Sequence)
			if m_UTF8.Companion_ValidUTF8Bytes_.Is_(_1_k) {
				if _dafny.Companion_Sequence_.Contains(requiredEncryptionContextKeys, _1_k) {
					_coll0.Add(_1_k)
				}
			}
		}
		return _coll0.ToSet()
	}()
	var _2_storedEncryptionContext _dafny.Map
	_ = _2_storedEncryptionContext
	_2_storedEncryptionContext = func() _dafny.Map {
		var _coll1 = _dafny.NewMapBuilder()
		_ = _coll1
		for _iter3 := _dafny.Iterate(((encryptionContext).Subtract(_0_reqKeySet)).Keys().Elements()); ; {
			_compr_1, _ok3 := _iter3()
			if !_ok3 {
				break
			}
			var _3_f _dafny.Sequence
			_3_f = interface{}(_compr_1).(_dafny.Sequence)
			if m_UTF8.Companion_ValidUTF8Bytes_.Is_(_3_f) {
				if ((encryptionContext).Subtract(_0_reqKeySet)).Contains(_3_f) {
					_coll1.Add(_3_f, (encryptionContext).Get(_3_f).(_dafny.Sequence))
				}
			}
		}
		return _coll1.ToMap()
	}()
	var _4_canonicalStoredEncryptionContext _dafny.Sequence
	_ = _4_canonicalStoredEncryptionContext
	_4_canonicalStoredEncryptionContext = m_EncryptionContext.Companion_Default___.GetCanonicalEncryptionContext(_2_storedEncryptionContext)
	var _5_body m_HeaderTypes.HeaderBody
	_ = _5_body
	var _out0 m_HeaderTypes.HeaderBody
	_ = _out0
	_out0 = Companion_Default___.BuildHeaderBody(messageId, suite, _4_canonicalStoredEncryptionContext, encryptedDataKeys, frameLength, (derivedDataKeys).Dtor_commitmentKey())
	_5_body = _out0
	var _6_requiredEncryptionContextMap _dafny.Map
	_ = _6_requiredEncryptionContextMap
	_6_requiredEncryptionContextMap = func() _dafny.Map {
		var _coll2 = _dafny.NewMapBuilder()
		_ = _coll2
		for _iter4 := _dafny.Iterate((_0_reqKeySet).Elements()); ; {
			_compr_2, _ok4 := _iter4()
			if !_ok4 {
				break
			}
			var _7_r _dafny.Sequence
			_7_r = interface{}(_compr_2).(_dafny.Sequence)
			if m_UTF8.Companion_ValidUTF8Bytes_.Is_(_7_r) {
				if (_0_reqKeySet).Contains(_7_r) {
					_coll2.Add(_7_r, (encryptionContext).Get(_7_r).(_dafny.Sequence))
				}
			}
		}
		return _coll2.ToMap()
	}()
	var _8_canonicalReqEncryptionContext _dafny.Sequence
	_ = _8_canonicalReqEncryptionContext
	_8_canonicalReqEncryptionContext = m_EncryptionContext.Companion_Default___.GetCanonicalEncryptionContext(_6_requiredEncryptionContextMap)
	var _9_serializedReqEncryptionContext _dafny.Sequence
	_ = _9_serializedReqEncryptionContext
	_9_serializedReqEncryptionContext = m_EncryptionContext.Companion_Default___.WriteEmptyEcOrWriteAAD(_8_canonicalReqEncryptionContext)
	var _10_rawHeader _dafny.Sequence
	_ = _10_rawHeader
	_10_rawHeader = m_Header.Companion_Default___.WriteHeaderBody(_5_body)
	var _11_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_HeaderTypes.Companion_HeaderAuth_.Default())
	_ = _11_valueOrError0
	var _out1 m_Wrappers.Result
	_ = _out1
	_out1 = Companion_Default___.BuildHeaderAuthTag(suite, (derivedDataKeys).Dtor_dataKey(), _10_rawHeader, _9_serializedReqEncryptionContext, crypto)
	_11_valueOrError0 = _out1
	if (_11_valueOrError0).IsFailure() {
		res = (_11_valueOrError0).PropagateFailure()
		return res
	}
	var _12_headerAuth m_HeaderTypes.HeaderAuth
	_ = _12_headerAuth
	_12_headerAuth = (_11_valueOrError0).Extract().(m_HeaderTypes.HeaderAuth)
	var _13_header m_Header.HeaderInfo
	_ = _13_header
	_13_header = m_Header.Companion_HeaderInfo_.Create_HeaderInfo_(_5_body, _10_rawHeader, encryptionContext, suite, _12_headerAuth)
	res = m_Wrappers.Companion_Result_.Create_Success_(_13_header)
	return res
	return res
}