nocfbot-0022-Document-the-get_reduced_frame_status-cascade-inv.txt

From 35fd6edcd5769a45a3071d5da6e75117631ede0b Mon Sep 17 00:00:00 2001
From: Henson Choi <assam258@gmail.com>
Date: Fri, 29 May 2026 17:51:37 +0900
Subject: [PATCH 22/26] Document the get_reduced_frame_status cascade invariant
 per Jian He's review

The RF_* classifier is an early-return cascade whose branches are not
mutually exclusive, so reordering them changes the result.  This is the
standard cascade idiom -- each branch is a minimal test premised on the
negations the preceding returns have established -- not a logic flaw, but
the structure left the contract implicit.

update_reduced_frame() records the match as exactly one of three
(rpr_match_matched, rpr_match_length) shapes: (false, 1), (true, 0), or
(true, >= 1).  Spell that out in the header, add the missing RF_EMPTY_MATCH
return value, and annotate each branch with a "by here" note stating the
running invariant -- notably why the empty match must be classified before
the range test.  No behavior change.
---
 src/backend/executor/nodeWindowAgg.c | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/backend/executor/nodeWindowAgg.c b/src/backend/executor/nodeWindowAgg.c
index 99858d22dad..4cf1a9ac67b 100644
--- a/src/backend/executor/nodeWindowAgg.c
+++ b/src/backend/executor/nodeWindowAgg.c
@@ -4306,6 +4306,16 @@ clear_reduced_frame(WindowAggState *winstate)
  *   RF_FRAME_HEAD      pos is the start of the current match
  *   RF_SKIPPED         pos is inside the current match but not the start
  *   RF_UNMATCHED       pos is processed but not part of any match
+ *   RF_EMPTY_MATCH     pos is the start of an empty (zero-length) match
+ *
+ * update_reduced_frame() records the current match as exactly one of three
+ * (rpr_match_matched, rpr_match_length) shapes: (false, 1) for unmatched,
+ * (true, 0) for an empty match, and (true, >= 1) for a real match.  The
+ * tests below form a cascade with early returns: each is a minimal check
+ * that relies on the negations the preceding returns have already
+ * established, so their order is significant.  The "by here" notes spell
+ * out the running invariant; reordering a test would misclassify one of
+ * the three shapes.
  */
 static int
 get_reduced_frame_status(WindowAggState *winstate, int64 pos)
@@ -4316,17 +4326,31 @@ get_reduced_frame_status(WindowAggState *winstate, int64 pos)
 	if (!winstate->rpr_match_valid)
 		return RF_NOT_DETERMINED;
 
-	/* Empty match: covers only the start position */
+	/*
+	 * By here the record is valid and holds one of the three shapes above.
+	 *
+	 * The empty match (true, 0) must be classified first: it has length 0, so
+	 * the range test below would compute start + length == start and reject
+	 * its own start position as out of range.
+	 */
 	if (pos == start && winstate->rpr_match_matched && length == 0)
 		return RF_EMPTY_MATCH;
 
-	/* Outside the result range */
+	/*
+	 * By here length >= 1 -- the only zero-length record, the empty match,
+	 * has been handled -- so [start, start + length) is a well-formed range.
+	 */
 	if (pos < start || pos >= start + length)
 		return RF_NOT_DETERMINED;
 
+	/*
+	 * By here pos lies within [start, start + length).  An unmatched record
+	 * is (false, 1), so this returns for its single in-range position.
+	 */
 	if (!winstate->rpr_match_matched)
 		return RF_UNMATCHED;
 
+	/* By here the match is real (true, >= 1) and pos is one of its rows. */
 	if (pos == start)
 		return RF_FRAME_HEAD;
 
-- 
2.50.1 (Apple Git-155)