func()

in releases/go/encryption-sdk/EncryptionContext/EncryptionContext.go [456:518]


func (_static *CompanionStruct_Default___) ReadAADSection(buffer m_SerializeFunctions.ReadableBuffer) m_Wrappers.Result {
	var _0_valueOrError0 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUInt16(buffer)
	_ = _0_valueOrError0
	if (_0_valueOrError0).IsFailure() {
		return (_0_valueOrError0).PropagateFailure()
	} else {
		var _1_length m_SerializeFunctions.SuccessfulRead = (_0_valueOrError0).Extract().(m_SerializeFunctions.SuccessfulRead)
		_ = _1_length
		if ((_1_length).Dtor_data().(uint16)) == (uint16(0)) {
			var _2_empty _dafny.Sequence = _dafny.SeqOf()
			_ = _2_empty
			return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_2_empty, (_1_length).Dtor_tail()))
		} else {
			var _3_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((((_1_length).Dtor_tail()).Dtor_start()).Plus(_dafny.IntOfUint16((_1_length).Dtor_data().(uint16)))).Cmp(_dafny.IntOfUint32((((_1_length).Dtor_tail()).Dtor_bytes()).Cardinality())) <= 0, m_SerializeFunctions.Companion_ReadProblems_.Create_MoreNeeded_((((_1_length).Dtor_tail()).Dtor_start()).Plus(_dafny.IntOfUint16((_1_length).Dtor_data().(uint16)))))
			_ = _3_valueOrError1
			if (_3_valueOrError1).IsFailure() {
				return (_3_valueOrError1).PropagateFailure()
			} else {
				var _4_valueOrError2 m_Wrappers.Result = m_SerializeFunctions.Companion_Default___.ReadUInt16((_1_length).Dtor_tail())
				_ = _4_valueOrError2
				if (_4_valueOrError2).IsFailure() {
					return (_4_valueOrError2).PropagateFailure()
				} else {
					var _5_verifyCount m_SerializeFunctions.SuccessfulRead = (_4_valueOrError2).Extract().(m_SerializeFunctions.SuccessfulRead)
					_ = _5_verifyCount
					if ((_1_length).Dtor_data().(uint16)) == (uint16(2)) {
						var _6_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((_5_verifyCount).Dtor_data().(uint16)) == (uint16(0)), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Encryption Context pairs count can not exceed byte length")))
						_ = _6_valueOrError3
						if (_6_valueOrError3).IsFailure() {
							return (_6_valueOrError3).PropagateFailure()
						} else {
							var _7_empty _dafny.Sequence = _dafny.SeqOf()
							_ = _7_empty
							return m_Wrappers.Companion_Result_.Create_Success_(m_SerializeFunctions.Companion_SuccessfulRead_.Create_SuccessfulRead_(_7_empty, (_5_verifyCount).Dtor_tail()))
						}
					} else {
						var _8_valueOrError4 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((uint16(0)) < ((_5_verifyCount).Dtor_data().(uint16)), m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("Encryption Context byte length exceeds pairs count.")))
						_ = _8_valueOrError4
						if (_8_valueOrError4).IsFailure() {
							return (_8_valueOrError4).PropagateFailure()
						} else {
							var _9_valueOrError5 m_Wrappers.Result = Companion_Default___.ReadAAD((_1_length).Dtor_tail())
							_ = _9_valueOrError5
							if (_9_valueOrError5).IsFailure() {
								return (_9_valueOrError5).PropagateFailure()
							} else {
								var _10_aad m_SerializeFunctions.SuccessfulRead = (_9_valueOrError5).Extract().(m_SerializeFunctions.SuccessfulRead)
								_ = _10_aad
								var _11_valueOrError6 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((((_10_aad).Dtor_tail()).Dtor_start()).Minus(((_1_length).Dtor_tail()).Dtor_start())).Cmp(_dafny.IntOfUint16((_1_length).Dtor_data().(uint16))) == 0, m_SerializeFunctions.Companion_ReadProblems_.Create_Error_(_dafny.SeqOfString("AAD Length did not match stored length.")))
								_ = _11_valueOrError6
								if (_11_valueOrError6).IsFailure() {
									return (_11_valueOrError6).PropagateFailure()
								} else {
									return m_Wrappers.Companion_Result_.Create_Success_(_10_aad)
								}
							}
						}
					}
				}
			}
		}
	}
}