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)
}
}
}
}
}
}
}
}
}