From a38a1e52b94d0195d8e9ed3bc19c2bdbf57b31ea Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 21:47:59 -0700 Subject: [PATCH 01/13] Draft proposal: document and test anchored linearity invariant Draft for internal Invoca review before filing upstream against prometheus/prometheus and/or prometheus/proposals. Proposes formalizing and testing the compositional invariant that anchored + increase satisfies: increase(m[D12] anchored) @ T2 + increase(m[D23] anchored) @ T3 = increase(m[D13] anchored) @ T3 This property is the design goal of Invoca's yrate family (cited as prior art in PROM-52) and the "composability" goal PROM-52 mentions but never states or tests. Includes a proof sketch, proposed doc/test additions, and reviewer notes on tone, scope, venue, and timing. Made-with: Cursor --- .../proposals/anchored-linearity-invariant.md | 88 +++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 docs/proposals/anchored-linearity-invariant.md diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md new file mode 100644 index 00000000000..1da14109c65 --- /dev/null +++ b/docs/proposals/anchored-linearity-invariant.md @@ -0,0 +1,88 @@ +# `anchored`: document and test the linearity invariant that makes adjacent ranges compose + +> **Status:** Draft for internal Invoca review. Target repo once finalized: +> `prometheus/prometheus` (new issue) and/or `prometheus/proposals` +> (amendment to [`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md)). +> +> **Proposed labels (upstream):** `kind/enhancement`, `kind/documentation`, `component/promql` + +--- + +## Summary + +PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By specifying left-open / right-closed range semantics `(start, end]` plus "last sample at or before `start` as the boundary anchor," `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: + +> For any series `m`, times `T₁ ≤ T₂ ≤ T₃`, and durations `Δ₁₂ = T₂−T₁`, `Δ₂₃ = T₃−T₂`, `Δ₁₃ = T₃−T₁`: +> +> ```promql +> increase(m[Δ₁₂] anchored) @ T₂ +> + +> increase(m[Δ₂₃] anchored) @ T₃ +> = +> increase(m[Δ₁₃] anchored) @ T₃ +> ``` +> +> (assuming `Δ₁₂ ≤ lookback_delta` so the anchor lookup succeeds). + +This invariant is what makes anchored `increase` safely composable across contiguous time windows — splitting a wider range into adjacent sub-ranges and summing the results gives the same answer as asking for the wider range directly. Plain `rate`/`increase` doesn't satisfy this; the proposal itself notes on line 119 that *"two consecutive range selectors therefore fail to capture the increase."* + +## Why it matters + +This is the formal expression of the "composability" goal the proposal mentions on line 147 ("offer greater composability and flexibility") and line 222 ("Improved composability across range boundaries"), but neither of those phrasings is pinned down. Making it explicit: + +- Gives users a precise, testable reason to prefer `anchored` for any workflow that splits or stitches time ranges (recording rules that roll up, alerts on windowed counter increases, dashboards that zoom between panel ranges, etc.). +- Locks the invariant into the engine's contract via tests so future refactors can't silently regress it. +- Resolves a subtle ambiguity at the `T₂` boundary: because the range is `(T₁, T₂]`, a sample whose timestamp equals `T₂` is attributed to the earlier range, and the same sample is returned by `anchor(T₂)` for the later range. That symmetry is what makes additivity exact — not a rounding coincidence. + +## Why `anchored` satisfies it + +
+Proof sketch + +Let `last_in(T_a, T_b]` denote the latest sample whose timestamp lies in `(T_a, T_b]`, `anchor(T)` the latest sample with timestamp `≤ T` within the lookback delta, and `resets(T_a, T_b]` the counter-reset correction accumulated from samples in `(T_a, T_b]`. + +Under `anchored + increase`: + +``` +f(T₁, T₂] = last_in(T₁, T₂] − anchor(T₁) + resets(T₁, T₂] +f(T₂, T₃] = last_in(T₂, T₃] − anchor(T₂) + resets(T₂, T₃] +f(T₁, T₃] = last_in(T₁, T₃] − anchor(T₁) + resets(T₁, T₃] +``` + +Adding the first two gives the third iff all of: + +1. `resets(T₁, T₂] + resets(T₂, T₃] = resets(T₁, T₃]` — holds because `(T₁, T₂]` and `(T₂, T₃]` partition `(T₁, T₃]`; every reset is counted exactly once. +2. `last_in(T₁, T₂] = anchor(T₂)` — both expressions denote "the latest sample with `t ≤ T₂`." The right-closed boundary on `(T₁, T₂]` includes `T₂` itself; the anchor definition "at or before `T₂`" matches. Provided `Δ₁₂ ≤ lookback_delta` (so `anchor(T₂)` doesn't fall back to the first in-range sample), these coincide. +3. `last_in(T₂, T₃] = last_in(T₁, T₃]` — trivially true when at least one sample exists in `(T₂, T₃]`; handled by the empty-range convention otherwise. + +The proposal's partial-dataset example (lines 231–237) — *"The first window slightly underestimates while the second window slightly overestimates the actual increase"* — is this invariant in action. The per-window numbers aren't coincidentally canceling; they're composing. + +
+ +## Related prior art + +This property is the design goal of the Invoca `yrate` family (referenced in the PROM-52 "Other docs or links" as [Prometheus y-rate](https://docs.google.com/document/d/1CF5jhyxSD437c2aU2wHcvg88i8CjSPO3kMHsEaDRe2w/edit)). Invoca has run `yrate`-semantics in production for ~5 years with this invariant as a documented contract; `anchored + increase` converges on the same behavior via a cleaner modifier-based syntax that avoids function proliferation. + +## Proposed additions + +1. **User-facing docs** (`docs/feature_flags.md` and the `anchored` entry under `docs/querying/functions.md`): a short callout stating the invariant. +2. **Proposal amendment** (`prometheus/proposals#…`): one paragraph under "How" linking the invariant to the "composability" goal. +3. **Regression tests** (`promql/promqltest/testdata/…`): paired-window cases asserting the invariant across: + - Regular scrape cadence, boundary timestamps aligned with sample cadence + - Same, but shifted off-cadence (to exercise the `last_in` / `anchor` coincidence) + - Ranges containing counter resets on both sides of `T₂` + - Partial datasets with missing scrapes straddling `T₂` + +## Happy to contribute + +I can split this into two PRs — docs first for quick review, then tests — and port test-data patterns from our internal `yrate` suite that have exercised this invariant for years. Please let me know if a proposal amendment is preferred before or after the docs/tests land. + +--- + +## Reviewer notes (Invoca-internal, strip before sending upstream) + +- **Tone:** aiming for "colleague flagging a missing piece," not "outsider demanding a spec change." Happy to soften or sharpen. +- **Attribution:** we can lean harder into the `yrate`-as-prior-art framing, or pull it back to just a link — depending on how forward we want to be about our involvement. +- **Scope:** current draft bundles docs + tests + proposal amendment. Could split into a pure docs issue first to test reception before offering code. +- **Venue:** open as an issue on `prometheus/prometheus` (lower friction, invites discussion) vs. open as a proposal amendment PR on `prometheus/proposals` (more formal, commits us to a spec change). My recommendation is the issue first, referencing PROM-52, and let maintainers route it. +- **Timing:** `anchored` is still behind `promql-extended-range-selectors` as of 3.11.2. Filing before GA gives us a chance to shape the contract before it solidifies; filing after GA lets us point at existing production adoption. Leaning toward "before GA." From 370b43e613cc9477260a1182bc4cdad2cb7cdb13 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 22:01:25 -0700 Subject: [PATCH 02/13] Clarify: range membership vs. anchor lookup are distinct MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The previous wording ("left-open / right-closed range semantics plus 'last sample at or before start as the boundary anchor'") conflated two separate concepts and read as if the anchor implied left-closed range semantics. Reword to make the distinction explicit: - Range membership is (start, end] — left-open, right-closed. A sample at t = start is NOT a member of the range. - The anchor is a separate lookup OUTSIDE the range, reaching backward from start up to lookback_delta, returning the latest sample with t <= start. Also sharpen the boundary-ambiguity discussion and proof-sketch item (2) to spell out that a sample at t = T2 plays a dual role (last member of the earlier range AND anchor for the later one) without ever being a member of both ranges. That dual role — not double-membership — is what makes the additivity exact. Made-with: Cursor --- docs/proposals/anchored-linearity-invariant.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md index 1da14109c65..eeb444c2a51 100644 --- a/docs/proposals/anchored-linearity-invariant.md +++ b/docs/proposals/anchored-linearity-invariant.md @@ -10,7 +10,7 @@ ## Summary -PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By specifying left-open / right-closed range semantics `(start, end]` plus "last sample at or before `start` as the boundary anchor," `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: +PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By combining a left-open / right-closed range `(start, end]` with a separate baseline *anchor* — the latest sample with timestamp `≤ start`, fetched from outside the range within `lookback_delta` — `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: > For any series `m`, times `T₁ ≤ T₂ ≤ T₃`, and durations `Δ₁₂ = T₂−T₁`, `Δ₂₃ = T₃−T₂`, `Δ₁₃ = T₃−T₁`: > @@ -32,7 +32,7 @@ This is the formal expression of the "composability" goal the proposal mentions - Gives users a precise, testable reason to prefer `anchored` for any workflow that splits or stitches time ranges (recording rules that roll up, alerts on windowed counter increases, dashboards that zoom between panel ranges, etc.). - Locks the invariant into the engine's contract via tests so future refactors can't silently regress it. -- Resolves a subtle ambiguity at the `T₂` boundary: because the range is `(T₁, T₂]`, a sample whose timestamp equals `T₂` is attributed to the earlier range, and the same sample is returned by `anchor(T₂)` for the later range. That symmetry is what makes additivity exact — not a rounding coincidence. +- Resolves a subtle ambiguity at the `T₂` boundary: a sample whose timestamp equals `T₂` is a *member* of the earlier range `(T₁, T₂]` (right-closed) but is *not* a member of the later range `(T₂, T₃]` (left-open). The same sample is nonetheless reached by `anchor(T₂)` for the later range — the anchor lookup ("latest sample with `t ≤ T₂`") reaches backward from, and including, the range's left boundary, even though the boundary itself is not in the range. That dual role — "last in the earlier range" *and* "anchor of the later range," rather than double-membership — is what makes additivity exact. ## Why `anchored` satisfies it @@ -52,7 +52,7 @@ f(T₁, T₃] = last_in(T₁, T₃] − anchor(T₁) + resets(T₁, T₃] Adding the first two gives the third iff all of: 1. `resets(T₁, T₂] + resets(T₂, T₃] = resets(T₁, T₃]` — holds because `(T₁, T₂]` and `(T₂, T₃]` partition `(T₁, T₃]`; every reset is counted exactly once. -2. `last_in(T₁, T₂] = anchor(T₂)` — both expressions denote "the latest sample with `t ≤ T₂`." The right-closed boundary on `(T₁, T₂]` includes `T₂` itself; the anchor definition "at or before `T₂`" matches. Provided `Δ₁₂ ≤ lookback_delta` (so `anchor(T₂)` doesn't fall back to the first in-range sample), these coincide. +2. `last_in(T₁, T₂] = anchor(T₂)` — these are *different* lookups that agree in value. `last_in(T₁, T₂]` is the latest sample *in* the range `(T₁, T₂]` (right-closed membership, so a sample at exactly `T₂` qualifies). `anchor(T₂)` is a separate lookup *outside* the later range `(T₂, T₃]`: the latest sample with `t ≤ T₂`, within `lookback_delta`. A sample at exactly `t = T₂` is reached by both — as the last member of the earlier range, and as the anchor for the later one — without ever being a member of both ranges. Provided `Δ₁₂ ≤ lookback_delta` (so the anchor lookup doesn't time-out before reaching it), these values coincide. 3. `last_in(T₂, T₃] = last_in(T₁, T₃]` — trivially true when at least one sample exists in `(T₂, T₃]`; handled by the empty-range convention otherwise. The proposal's partial-dataset example (lines 231–237) — *"The first window slightly underestimates while the second window slightly overestimates the actual increase"* — is this invariant in action. The per-window numbers aren't coincidentally canceling; they're composing. From 83c637037dc9ce1786ee810f0f9d35bce0740ce9 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 22:05:16 -0700 Subject: [PATCH 03/13] Use r (range) notation to match Prometheus terminology Replace the delta symbol with r_ij for range durations, matching Prometheus/PromQL's canonical term ("range selector", "range vector", "--query.lookback-delta"). lookback_delta stays as-is since it is literal Prometheus terminology. No semantic changes; pure notational cleanup so readers don't mentally translate from physics/math notation to Prometheus terminology while parsing the invariant. Made-with: Cursor --- docs/proposals/anchored-linearity-invariant.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md index eeb444c2a51..42f1ec74e72 100644 --- a/docs/proposals/anchored-linearity-invariant.md +++ b/docs/proposals/anchored-linearity-invariant.md @@ -12,17 +12,17 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By combining a left-open / right-closed range `(start, end]` with a separate baseline *anchor* — the latest sample with timestamp `≤ start`, fetched from outside the range within `lookback_delta` — `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: -> For any series `m`, times `T₁ ≤ T₂ ≤ T₃`, and durations `Δ₁₂ = T₂−T₁`, `Δ₂₃ = T₃−T₂`, `Δ₁₃ = T₃−T₁`: +> For any series `m`, times `T₁ ≤ T₂ ≤ T₃`, and range durations `r₁₂ = T₂−T₁`, `r₂₃ = T₃−T₂`, `r₁₃ = T₃−T₁`: > > ```promql -> increase(m[Δ₁₂] anchored) @ T₂ +> increase(m[r₁₂] anchored) @ T₂ > + -> increase(m[Δ₂₃] anchored) @ T₃ +> increase(m[r₂₃] anchored) @ T₃ > = -> increase(m[Δ₁₃] anchored) @ T₃ +> increase(m[r₁₃] anchored) @ T₃ > ``` > -> (assuming `Δ₁₂ ≤ lookback_delta` so the anchor lookup succeeds). +> (assuming `r₁₂ ≤ lookback_delta` so the anchor lookup succeeds). This invariant is what makes anchored `increase` safely composable across contiguous time windows — splitting a wider range into adjacent sub-ranges and summing the results gives the same answer as asking for the wider range directly. Plain `rate`/`increase` doesn't satisfy this; the proposal itself notes on line 119 that *"two consecutive range selectors therefore fail to capture the increase."* @@ -52,7 +52,7 @@ f(T₁, T₃] = last_in(T₁, T₃] − anchor(T₁) + resets(T₁, T₃] Adding the first two gives the third iff all of: 1. `resets(T₁, T₂] + resets(T₂, T₃] = resets(T₁, T₃]` — holds because `(T₁, T₂]` and `(T₂, T₃]` partition `(T₁, T₃]`; every reset is counted exactly once. -2. `last_in(T₁, T₂] = anchor(T₂)` — these are *different* lookups that agree in value. `last_in(T₁, T₂]` is the latest sample *in* the range `(T₁, T₂]` (right-closed membership, so a sample at exactly `T₂` qualifies). `anchor(T₂)` is a separate lookup *outside* the later range `(T₂, T₃]`: the latest sample with `t ≤ T₂`, within `lookback_delta`. A sample at exactly `t = T₂` is reached by both — as the last member of the earlier range, and as the anchor for the later one — without ever being a member of both ranges. Provided `Δ₁₂ ≤ lookback_delta` (so the anchor lookup doesn't time-out before reaching it), these values coincide. +2. `last_in(T₁, T₂] = anchor(T₂)` — these are *different* lookups that agree in value. `last_in(T₁, T₂]` is the latest sample *in* the range `(T₁, T₂]` (right-closed membership, so a sample at exactly `T₂` qualifies). `anchor(T₂)` is a separate lookup *outside* the later range `(T₂, T₃]`: the latest sample with `t ≤ T₂`, within `lookback_delta`. A sample at exactly `t = T₂` is reached by both — as the last member of the earlier range, and as the anchor for the later one — without ever being a member of both ranges. Provided `r₁₂ ≤ lookback_delta` (so the anchor lookup doesn't time-out before reaching it), these values coincide. 3. `last_in(T₂, T₃] = last_in(T₁, T₃]` — trivially true when at least one sample exists in `(T₂, T₃]`; handled by the empty-range convention otherwise. The proposal's partial-dataset example (lines 231–237) — *"The first window slightly underestimates while the second window slightly overestimates the actual increase"* — is this invariant in action. The per-window numbers aren't coincidentally canceling; they're composing. From 2c26bcf9c84221ca5efb590288f216892b202617 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 22:11:54 -0700 Subject: [PATCH 04/13] Use PromQL-native notation: @ T instants + range durations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reframe the invariant statement and proof in terms Prometheus already uses natively: - Range selectors m[r_a], m[r_b], m[r_a + r_b] — PromQL syntax. - @ T_a, @ T_b — the @ modifier that users already know. - The only time arithmetic is addition (T_b = T_a + r_b), expressing that the two anchored windows are adjacent. The previous notation defined range durations as timestamp subtractions (r_ij = T_j - T_i), which read as physics/math shorthand rather than PromQL. Drop that in favor of taking ranges as primitives and deriving the later evaluation instant via addition. Proof sketch refactor: - Rename generic-range placeholders from (T_a, T_b] to (s, e] so they don't collide with the evaluation-instant variables. - Introduce T_start = T_a - r_a locally as the left boundary of the combined window; the three anchored windows then cover (T_start, T_a], (T_a, T_b], and (T_start, T_b]. - Rename the three `f`-terms to f_earlier/f_later/f_combined (descriptive, matches the framing of "earlier + later = combined"). - Fix two straggler T_2 references in the regression-tests section. Pure notational change; invariant, proof, and scope are unchanged. Made-with: Cursor --- .../proposals/anchored-linearity-invariant.md | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md index 42f1ec74e72..e3934dbcf2c 100644 --- a/docs/proposals/anchored-linearity-invariant.md +++ b/docs/proposals/anchored-linearity-invariant.md @@ -12,17 +12,17 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By combining a left-open / right-closed range `(start, end]` with a separate baseline *anchor* — the latest sample with timestamp `≤ start`, fetched from outside the range within `lookback_delta` — `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: -> For any series `m`, times `T₁ ≤ T₂ ≤ T₃`, and range durations `r₁₂ = T₂−T₁`, `r₂₃ = T₃−T₂`, `r₁₃ = T₃−T₁`: +> For any series `m`, ranges `r_a` and `r_b`, and evaluation instants `T_a, T_b` with `T_b = T_a + r_b` (so the two anchored windows are adjacent, no gap and no overlap): > > ```promql -> increase(m[r₁₂] anchored) @ T₂ +> increase(m[r_a] anchored) @ T_a > + -> increase(m[r₂₃] anchored) @ T₃ +> increase(m[r_b] anchored) @ T_b > = -> increase(m[r₁₃] anchored) @ T₃ +> increase(m[r_a + r_b] anchored) @ T_b > ``` > -> (assuming `r₁₂ ≤ lookback_delta` so the anchor lookup succeeds). +> (assuming `r_a ≤ lookback_delta` so the anchor lookup at the left boundary succeeds). This invariant is what makes anchored `increase` safely composable across contiguous time windows — splitting a wider range into adjacent sub-ranges and summing the results gives the same answer as asking for the wider range directly. Plain `rate`/`increase` doesn't satisfy this; the proposal itself notes on line 119 that *"two consecutive range selectors therefore fail to capture the increase."* @@ -32,28 +32,28 @@ This is the formal expression of the "composability" goal the proposal mentions - Gives users a precise, testable reason to prefer `anchored` for any workflow that splits or stitches time ranges (recording rules that roll up, alerts on windowed counter increases, dashboards that zoom between panel ranges, etc.). - Locks the invariant into the engine's contract via tests so future refactors can't silently regress it. -- Resolves a subtle ambiguity at the `T₂` boundary: a sample whose timestamp equals `T₂` is a *member* of the earlier range `(T₁, T₂]` (right-closed) but is *not* a member of the later range `(T₂, T₃]` (left-open). The same sample is nonetheless reached by `anchor(T₂)` for the later range — the anchor lookup ("latest sample with `t ≤ T₂`") reaches backward from, and including, the range's left boundary, even though the boundary itself is not in the range. That dual role — "last in the earlier range" *and* "anchor of the later range," rather than double-membership — is what makes additivity exact. +- Resolves a subtle ambiguity at the shared boundary `T_a`: a sample whose timestamp equals `T_a` is a *member* of the earlier range (right-closed) but is *not* a member of the later range `(T_a, T_b]` (left-open). The same sample is nonetheless reached by `anchor(T_a)` for the later range — the anchor lookup ("latest sample with `t ≤ T_a`") reaches backward from, and including, the range's left boundary, even though the boundary itself is not in the range. That dual role — "last in the earlier range" *and* "anchor of the later range," rather than double-membership — is what makes additivity exact. ## Why `anchored` satisfies it
Proof sketch -Let `last_in(T_a, T_b]` denote the latest sample whose timestamp lies in `(T_a, T_b]`, `anchor(T)` the latest sample with timestamp `≤ T` within the lookback delta, and `resets(T_a, T_b]` the counter-reset correction accumulated from samples in `(T_a, T_b]`. +Let `last_in(s, e]` denote the latest sample whose timestamp lies in `(s, e]`, `anchor(t)` the latest sample with timestamp `≤ t` within `lookback_delta`, and `resets(s, e]` the counter-reset correction accumulated from samples in `(s, e]`. -Under `anchored + increase`: +Let `T_start = T_a − r_a` be the left boundary of the combined range. The three anchored windows in the invariant cover `(T_start, T_a]`, `(T_a, T_b]`, and `(T_start, T_b]`, respectively. So: ``` -f(T₁, T₂] = last_in(T₁, T₂] − anchor(T₁) + resets(T₁, T₂] -f(T₂, T₃] = last_in(T₂, T₃] − anchor(T₂) + resets(T₂, T₃] -f(T₁, T₃] = last_in(T₁, T₃] − anchor(T₁) + resets(T₁, T₃] +f_earlier = last_in(T_start, T_a] − anchor(T_start) + resets(T_start, T_a] +f_later = last_in(T_a, T_b] − anchor(T_a) + resets(T_a, T_b] +f_combined = last_in(T_start, T_b] − anchor(T_start) + resets(T_start, T_b] ``` -Adding the first two gives the third iff all of: +`f_earlier + f_later = f_combined` iff all of: -1. `resets(T₁, T₂] + resets(T₂, T₃] = resets(T₁, T₃]` — holds because `(T₁, T₂]` and `(T₂, T₃]` partition `(T₁, T₃]`; every reset is counted exactly once. -2. `last_in(T₁, T₂] = anchor(T₂)` — these are *different* lookups that agree in value. `last_in(T₁, T₂]` is the latest sample *in* the range `(T₁, T₂]` (right-closed membership, so a sample at exactly `T₂` qualifies). `anchor(T₂)` is a separate lookup *outside* the later range `(T₂, T₃]`: the latest sample with `t ≤ T₂`, within `lookback_delta`. A sample at exactly `t = T₂` is reached by both — as the last member of the earlier range, and as the anchor for the later one — without ever being a member of both ranges. Provided `r₁₂ ≤ lookback_delta` (so the anchor lookup doesn't time-out before reaching it), these values coincide. -3. `last_in(T₂, T₃] = last_in(T₁, T₃]` — trivially true when at least one sample exists in `(T₂, T₃]`; handled by the empty-range convention otherwise. +1. `resets(T_start, T_a] + resets(T_a, T_b] = resets(T_start, T_b]` — holds because `(T_start, T_a]` and `(T_a, T_b]` partition `(T_start, T_b]`; every reset is counted exactly once. +2. `last_in(T_start, T_a] = anchor(T_a)` — these are *different* lookups that agree in value. `last_in(T_start, T_a]` is the latest sample *in* the earlier range (right-closed membership, so a sample at exactly `T_a` qualifies). `anchor(T_a)` is a separate lookup *outside* the later range `(T_a, T_b]`: the latest sample with `t ≤ T_a`, within `lookback_delta`. A sample at exactly `t = T_a` is reached by both — as the last member of the earlier range, and as the anchor for the later one — without ever being a member of both ranges. Provided `r_a ≤ lookback_delta` (so the anchor lookup doesn't time-out before reaching `T_start`), these values coincide. +3. `last_in(T_a, T_b] = last_in(T_start, T_b]` — trivially true when at least one sample exists in `(T_a, T_b]`; handled by the empty-range convention otherwise. The proposal's partial-dataset example (lines 231–237) — *"The first window slightly underestimates while the second window slightly overestimates the actual increase"* — is this invariant in action. The per-window numbers aren't coincidentally canceling; they're composing. @@ -70,8 +70,8 @@ This property is the design goal of the Invoca `yrate` family (referenced in the 3. **Regression tests** (`promql/promqltest/testdata/…`): paired-window cases asserting the invariant across: - Regular scrape cadence, boundary timestamps aligned with sample cadence - Same, but shifted off-cadence (to exercise the `last_in` / `anchor` coincidence) - - Ranges containing counter resets on both sides of `T₂` - - Partial datasets with missing scrapes straddling `T₂` + - Ranges containing counter resets on both sides of `T_a` + - Partial datasets with missing scrapes straddling `T_a` ## Happy to contribute From 417c3fc6fd25b7d70c364a3f7333b376dd68d060 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 22:19:08 -0700 Subject: [PATCH 05/13] Restore numeric subscripts; drop underscore placeholder names Previous commit introduced T_a / T_b / r_a / r_b via ASCII-underscore notation, which is visually noisier than Unicode subscripts and lost the numeric-subscript convention the earlier drafts used. Revert to: - Statement: T_1, T_2, r_1, r_2 (Unicode subscripts), with the adjacency constraint T_2 = T_1 + r_2. - Proof: introduce T_0 = T_1 - r_1 as the left boundary of the combined window; three anchored windows cover (T_0, T_1], (T_1, T_2], (T_0, T_2]. - Function values: f_01, f_12, f_02 (Unicode subscript pairs consistent with the interval notation) instead of the ASCII-underscore descriptive names f_earlier / f_later / f_combined. - Regression-test bullets: T_1 instead of T_a. Generic range-placeholder names (s, e] in the proof sketch are kept unchanged; they are short, descriptive, and collision-free with the concrete T_i subscripts. No change to the invariant itself or the proof structure. Made-with: Cursor --- .../proposals/anchored-linearity-invariant.md | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md index e3934dbcf2c..5d86f0a99dd 100644 --- a/docs/proposals/anchored-linearity-invariant.md +++ b/docs/proposals/anchored-linearity-invariant.md @@ -12,17 +12,17 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By combining a left-open / right-closed range `(start, end]` with a separate baseline *anchor* — the latest sample with timestamp `≤ start`, fetched from outside the range within `lookback_delta` — `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: -> For any series `m`, ranges `r_a` and `r_b`, and evaluation instants `T_a, T_b` with `T_b = T_a + r_b` (so the two anchored windows are adjacent, no gap and no overlap): +> For any series `m`, ranges `r₁` and `r₂`, and evaluation instants `T₁, T₂` with `T₂ = T₁ + r₂` (so the two anchored windows are adjacent, no gap and no overlap): > > ```promql -> increase(m[r_a] anchored) @ T_a +> increase(m[r₁] anchored) @ T₁ > + -> increase(m[r_b] anchored) @ T_b +> increase(m[r₂] anchored) @ T₂ > = -> increase(m[r_a + r_b] anchored) @ T_b +> increase(m[r₁ + r₂] anchored) @ T₂ > ``` > -> (assuming `r_a ≤ lookback_delta` so the anchor lookup at the left boundary succeeds). +> (assuming `r₁ ≤ lookback_delta` so the anchor lookup at the left boundary succeeds). This invariant is what makes anchored `increase` safely composable across contiguous time windows — splitting a wider range into adjacent sub-ranges and summing the results gives the same answer as asking for the wider range directly. Plain `rate`/`increase` doesn't satisfy this; the proposal itself notes on line 119 that *"two consecutive range selectors therefore fail to capture the increase."* @@ -32,7 +32,7 @@ This is the formal expression of the "composability" goal the proposal mentions - Gives users a precise, testable reason to prefer `anchored` for any workflow that splits or stitches time ranges (recording rules that roll up, alerts on windowed counter increases, dashboards that zoom between panel ranges, etc.). - Locks the invariant into the engine's contract via tests so future refactors can't silently regress it. -- Resolves a subtle ambiguity at the shared boundary `T_a`: a sample whose timestamp equals `T_a` is a *member* of the earlier range (right-closed) but is *not* a member of the later range `(T_a, T_b]` (left-open). The same sample is nonetheless reached by `anchor(T_a)` for the later range — the anchor lookup ("latest sample with `t ≤ T_a`") reaches backward from, and including, the range's left boundary, even though the boundary itself is not in the range. That dual role — "last in the earlier range" *and* "anchor of the later range," rather than double-membership — is what makes additivity exact. +- Resolves a subtle ambiguity at the shared boundary `T₁`: a sample whose timestamp equals `T₁` is a *member* of the earlier range (right-closed) but is *not* a member of the later range `(T₁, T₂]` (left-open). The same sample is nonetheless reached by `anchor(T₁)` for the later range — the anchor lookup ("latest sample with `t ≤ T₁`") reaches backward from, and including, the range's left boundary, even though the boundary itself is not in the range. That dual role — "last in the earlier range" *and* "anchor of the later range," rather than double-membership — is what makes additivity exact. ## Why `anchored` satisfies it @@ -41,19 +41,19 @@ This is the formal expression of the "composability" goal the proposal mentions Let `last_in(s, e]` denote the latest sample whose timestamp lies in `(s, e]`, `anchor(t)` the latest sample with timestamp `≤ t` within `lookback_delta`, and `resets(s, e]` the counter-reset correction accumulated from samples in `(s, e]`. -Let `T_start = T_a − r_a` be the left boundary of the combined range. The three anchored windows in the invariant cover `(T_start, T_a]`, `(T_a, T_b]`, and `(T_start, T_b]`, respectively. So: +Let `T₀ = T₁ − r₁` be the left boundary of the combined range. The three anchored windows in the invariant cover `(T₀, T₁]`, `(T₁, T₂]`, and `(T₀, T₂]`, respectively. So: ``` -f_earlier = last_in(T_start, T_a] − anchor(T_start) + resets(T_start, T_a] -f_later = last_in(T_a, T_b] − anchor(T_a) + resets(T_a, T_b] -f_combined = last_in(T_start, T_b] − anchor(T_start) + resets(T_start, T_b] +f₀₁ = last_in(T₀, T₁] − anchor(T₀) + resets(T₀, T₁] +f₁₂ = last_in(T₁, T₂] − anchor(T₁) + resets(T₁, T₂] +f₀₂ = last_in(T₀, T₂] − anchor(T₀) + resets(T₀, T₂] ``` -`f_earlier + f_later = f_combined` iff all of: +`f₀₁ + f₁₂ = f₀₂` iff all of: -1. `resets(T_start, T_a] + resets(T_a, T_b] = resets(T_start, T_b]` — holds because `(T_start, T_a]` and `(T_a, T_b]` partition `(T_start, T_b]`; every reset is counted exactly once. -2. `last_in(T_start, T_a] = anchor(T_a)` — these are *different* lookups that agree in value. `last_in(T_start, T_a]` is the latest sample *in* the earlier range (right-closed membership, so a sample at exactly `T_a` qualifies). `anchor(T_a)` is a separate lookup *outside* the later range `(T_a, T_b]`: the latest sample with `t ≤ T_a`, within `lookback_delta`. A sample at exactly `t = T_a` is reached by both — as the last member of the earlier range, and as the anchor for the later one — without ever being a member of both ranges. Provided `r_a ≤ lookback_delta` (so the anchor lookup doesn't time-out before reaching `T_start`), these values coincide. -3. `last_in(T_a, T_b] = last_in(T_start, T_b]` — trivially true when at least one sample exists in `(T_a, T_b]`; handled by the empty-range convention otherwise. +1. `resets(T₀, T₁] + resets(T₁, T₂] = resets(T₀, T₂]` — holds because `(T₀, T₁]` and `(T₁, T₂]` partition `(T₀, T₂]`; every reset is counted exactly once. +2. `last_in(T₀, T₁] = anchor(T₁)` — these are *different* lookups that agree in value. `last_in(T₀, T₁]` is the latest sample *in* the earlier range (right-closed membership, so a sample at exactly `T₁` qualifies). `anchor(T₁)` is a separate lookup *outside* the later range `(T₁, T₂]`: the latest sample with `t ≤ T₁`, within `lookback_delta`. A sample at exactly `t = T₁` is reached by both — as the last member of the earlier range, and as the anchor for the later one — without ever being a member of both ranges. Provided `r₁ ≤ lookback_delta` (so the anchor lookup doesn't time-out before reaching `T₀`), these values coincide. +3. `last_in(T₁, T₂] = last_in(T₀, T₂]` — trivially true when at least one sample exists in `(T₁, T₂]`; handled by the empty-range convention otherwise. The proposal's partial-dataset example (lines 231–237) — *"The first window slightly underestimates while the second window slightly overestimates the actual increase"* — is this invariant in action. The per-window numbers aren't coincidentally canceling; they're composing. @@ -70,8 +70,8 @@ This property is the design goal of the Invoca `yrate` family (referenced in the 3. **Regression tests** (`promql/promqltest/testdata/…`): paired-window cases asserting the invariant across: - Regular scrape cadence, boundary timestamps aligned with sample cadence - Same, but shifted off-cadence (to exercise the `last_in` / `anchor` coincidence) - - Ranges containing counter resets on both sides of `T_a` - - Partial datasets with missing scrapes straddling `T_a` + - Ranges containing counter resets on both sides of `T₁` + - Partial datasets with missing scrapes straddling `T₁` ## Happy to contribute From 688461e2f52762bb2fee62a28314659313accbb2 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 22:23:57 -0700 Subject: [PATCH 06/13] =?UTF-8?q?Define=20T=E2=82=81=20and=20T=E2=82=82=20?= =?UTF-8?q?independently;=20derive=20r=E2=82=82=20from=20the=20interval?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Previous wording "T₂ = T₁ + r₂" made T₂ look like a derived quantity. In practice T₁ and T₂ are both primary — they are the two evaluation instants a user would pick — and r₂ is what gets determined by choosing them. Reorder the definitions to make that explicit: - T₁ < T₂: two independent evaluation instants. - r₁: any range duration bounded by lookback_delta (free choice). - r₂: the length of the interval (T₁, T₂], described in prose rather than as T₂ − T₁, keeping with the earlier decision to avoid timestamp arithmetic in the statement. The adjacency condition ("later window's left boundary falls exactly on T₁, no gap and no overlap") is now stated directly rather than implied by an equation. The precondition "r₁ ≤ lookback_delta" migrates from a trailing parenthetical into r₁'s own definition line, since it is a constraint on r₁ specifically. No change to the invariant, proof, or scope. Made-with: Cursor --- docs/proposals/anchored-linearity-invariant.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md index 5d86f0a99dd..ed9308daf95 100644 --- a/docs/proposals/anchored-linearity-invariant.md +++ b/docs/proposals/anchored-linearity-invariant.md @@ -12,7 +12,12 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By combining a left-open / right-closed range `(start, end]` with a separate baseline *anchor* — the latest sample with timestamp `≤ start`, fetched from outside the range within `lookback_delta` — `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: -> For any series `m`, ranges `r₁` and `r₂`, and evaluation instants `T₁, T₂` with `T₂ = T₁ + r₂` (so the two anchored windows are adjacent, no gap and no overlap): +> For any series `m` and any two evaluation instants `T₁ < T₂`, with: +> +> - `r₁` — any range duration (the earlier window's length), subject to `r₁ ≤ lookback_delta` +> - `r₂` — the length of the interval `(T₁, T₂]` (so the two anchored windows below are adjacent: the later window's left boundary falls exactly on `T₁`, giving no gap and no overlap) +> +> then: > > ```promql > increase(m[r₁] anchored) @ T₁ @@ -21,8 +26,6 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/promethe > = > increase(m[r₁ + r₂] anchored) @ T₂ > ``` -> -> (assuming `r₁ ≤ lookback_delta` so the anchor lookup at the left boundary succeeds). This invariant is what makes anchored `increase` safely composable across contiguous time windows — splitting a wider range into adjacent sub-ranges and summing the results gives the same answer as asking for the wider range directly. Plain `rate`/`increase` doesn't satisfy this; the proposal itself notes on line 119 that *"two consecutive range selectors therefore fail to capture the increase."* From 89209200bdce6255d199e159584e976a49ba73bb Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 22:26:50 -0700 Subject: [PATCH 07/13] State the invariant in terms of three primary timestamps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Promote T₀ to a first-class timestamp alongside T₁ and T₂, so the setup reads naturally as "pick three timestamps, the ranges are the lengths of the two adjacent intervals." That makes clear upfront what intervals r₁ and r₂ cover without forcing the reader to derive them. New setup: - T₀ < T₁ < T₂ — three timestamps. - r₁ = length of (T₀, T₁], bounded by lookback_delta. - r₂ = length of (T₁, T₂]. Added a small table showing which interval each anchored window covers; the table pairs window expression with interval in a way that leaves no room for ambiguity about which range is which. Proof sketch simplifies correspondingly: the "Let T₀ = T₁ − r₁" definition line is dropped since T₀ is now primary. The three f terms and partition/anchor identities already referenced T₀, so no other changes were needed there. No change to the invariant itself or the proof structure. Made-with: Cursor --- docs/proposals/anchored-linearity-invariant.md | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md index ed9308daf95..2de7af52acf 100644 --- a/docs/proposals/anchored-linearity-invariant.md +++ b/docs/proposals/anchored-linearity-invariant.md @@ -12,12 +12,20 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/prometheus/proposals/blob/main/proposals/0052-extended-range-selectors-semantics.md), implemented in [prometheus/prometheus#16457](https://github.com/prometheus/prometheus/pull/16457), released in 3.7 behind `promql-extended-range-selectors`) introduces `anchored` and `smoothed`. By combining a left-open / right-closed range `(start, end]` with a separate baseline *anchor* — the latest sample with timestamp `≤ start`, fetched from outside the range within `lookback_delta` — `anchored + increase/rate/delta` has an important mathematical property that the proposal demonstrates informally but never states or tests: -> For any series `m` and any two evaluation instants `T₁ < T₂`, with: +> For any series `m` and any three timestamps `T₀ < T₁ < T₂`, let: > -> - `r₁` — any range duration (the earlier window's length), subject to `r₁ ≤ lookback_delta` -> - `r₂` — the length of the interval `(T₁, T₂]` (so the two anchored windows below are adjacent: the later window's left boundary falls exactly on `T₁`, giving no gap and no overlap) +> - `r₁` = the length of `(T₀, T₁]`, subject to `r₁ ≤ lookback_delta` +> - `r₂` = the length of `(T₁, T₂]` > -> then: +> Then the three anchored windows cover exactly the intervals their names suggest: +> +> | Window | Covers | +> |---|---| +> | `m[r₁] anchored @ T₁` | `(T₀, T₁]` | +> | `m[r₂] anchored @ T₂` | `(T₁, T₂]` | +> | `m[r₁ + r₂] anchored @ T₂` | `(T₀, T₂]` | +> +> and: > > ```promql > increase(m[r₁] anchored) @ T₁ @@ -44,7 +52,7 @@ This is the formal expression of the "composability" goal the proposal mentions Let `last_in(s, e]` denote the latest sample whose timestamp lies in `(s, e]`, `anchor(t)` the latest sample with timestamp `≤ t` within `lookback_delta`, and `resets(s, e]` the counter-reset correction accumulated from samples in `(s, e]`. -Let `T₀ = T₁ − r₁` be the left boundary of the combined range. The three anchored windows in the invariant cover `(T₀, T₁]`, `(T₁, T₂]`, and `(T₀, T₂]`, respectively. So: +The three anchored windows in the invariant cover `(T₀, T₁]`, `(T₁, T₂]`, and `(T₀, T₂]`, respectively. So: ``` f₀₁ = last_in(T₀, T₁] − anchor(T₀) + resets(T₀, T₁] From 449739623c0fc3289e59a09a112e5962f379dd36 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Sat, 18 Apr 2026 22:31:45 -0700 Subject: [PATCH 08/13] Explain that @ is always the right edge of an anchored range MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a one-line "PromQL rule of thumb" reminder before the windows-vs-intervals table: `m[duration] anchored @ T` covers (T − duration, T], so the @ instant is always the right edge and the range extends backward from it. Without this reminder, readers who aren't fluent in the @ modifier may wonder why the combined window uses `@ T₂` rather than `@ T₀` or `@ T₁` — the only way to get a range ending at T₂ is to evaluate it @ T₂, independent of how far back the range extends. Everything else unchanged. Made-with: Cursor --- docs/proposals/anchored-linearity-invariant.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-linearity-invariant.md index 2de7af52acf..2d732faa8bf 100644 --- a/docs/proposals/anchored-linearity-invariant.md +++ b/docs/proposals/anchored-linearity-invariant.md @@ -17,7 +17,7 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/promethe > - `r₁` = the length of `(T₀, T₁]`, subject to `r₁ ≤ lookback_delta` > - `r₂` = the length of `(T₁, T₂]` > -> Then the three anchored windows cover exactly the intervals their names suggest: +> Then the three anchored windows cover exactly the intervals their names suggest. (Recall the PromQL rule: `m[duration] anchored @ T` covers `(T − duration, T]` — the `@` instant is always the *right* edge, and the range extends backward from it.) > > | Window | Covers | > |---|---| From 04fe2a9b7d4ca7f16bb2ec361003e18ee7aded27 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Mon, 11 May 2026 08:32:33 -0700 Subject: [PATCH 09/13] Rename proposal to use "composability" instead of "linearity" Adopt the term composability for the upstream-facing draft, with additivity over adjacent ranges as the precise mathematical anchor. Rationale: * PROM-52 already names "composability" as a stated goal twice (lines 147 and 222) but never pins it down. Meeting upstream at their own vocabulary makes the proposal a definition of an existing concept rather than an introduction of a new one -- lower-stakes and easier to land. * Strict "linearity" overclaims; the property at issue is finite additivity over a partition of adjacent intervals, not full linearity over a vector space. A measure-theory-literate reviewer would flag the term, and the substance of the proposal should not get derailed into that pedantic objection. * Internal Invoca terminology (branch names, commit messages, the yrate code comments, and the yrate design doc) continues to use "linearity" -- that shorthand has years of established cache among engineers who already know what it means. The branch name and PR remain on "linearity"; only the artifact destined for upstream consumption uses "composability". The body of the proposal already used "composability" and "additivity" appropriately, so the only edit needed was the H1 title and the filename. Co-authored-by: Cursor --- ...linearity-invariant.md => anchored-composability-invariant.md} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename docs/proposals/{anchored-linearity-invariant.md => anchored-composability-invariant.md} (100%) diff --git a/docs/proposals/anchored-linearity-invariant.md b/docs/proposals/anchored-composability-invariant.md similarity index 100% rename from docs/proposals/anchored-linearity-invariant.md rename to docs/proposals/anchored-composability-invariant.md From 1f4bc92725f5b6256bd59d67d4440815f7be0e8c Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Mon, 11 May 2026 08:33:21 -0700 Subject: [PATCH 10/13] Retitle proposal: 'composability invariant for adjacent ranges' Co-authored-by: Cursor --- docs/proposals/anchored-composability-invariant.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/proposals/anchored-composability-invariant.md b/docs/proposals/anchored-composability-invariant.md index 2d732faa8bf..0d95a88f02b 100644 --- a/docs/proposals/anchored-composability-invariant.md +++ b/docs/proposals/anchored-composability-invariant.md @@ -1,4 +1,4 @@ -# `anchored`: document and test the linearity invariant that makes adjacent ranges compose +# `anchored`: document and test the composability invariant for adjacent ranges > **Status:** Draft for internal Invoca review. Target repo once finalized: > `prometheus/prometheus` (new issue) and/or `prometheus/proposals` From 03a763419fa09ee44d8b6ee86924d3822f10a1f1 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Mon, 11 May 2026 10:21:35 -0700 Subject: [PATCH 11/13] Drop self-defining 'intervals their names suggest' phrasing The previous wording told the reader the windows 'cover the intervals their names suggest' immediately before the table that defines those intervals -- a circular construction. The reader has no prior basis for what the names suggest until the table provides it. Rewording to point forward to the table directly: 'The three anchored windows below cover these intervals.' Co-authored-by: Cursor --- docs/proposals/anchored-composability-invariant.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/proposals/anchored-composability-invariant.md b/docs/proposals/anchored-composability-invariant.md index 0d95a88f02b..b90fdfe5bc2 100644 --- a/docs/proposals/anchored-composability-invariant.md +++ b/docs/proposals/anchored-composability-invariant.md @@ -17,7 +17,7 @@ PROM-52 ([`0052-extended-range-selectors-semantics`](https://github.com/promethe > - `r₁` = the length of `(T₀, T₁]`, subject to `r₁ ≤ lookback_delta` > - `r₂` = the length of `(T₁, T₂]` > -> Then the three anchored windows cover exactly the intervals their names suggest. (Recall the PromQL rule: `m[duration] anchored @ T` covers `(T − duration, T]` — the `@` instant is always the *right* edge, and the range extends backward from it.) +> The three anchored windows below cover these intervals. (Recall the PromQL rule: `m[duration] anchored @ T` covers `(T − duration, T]` — the `@` instant is always the *right* edge, and the range extends backward from it.) > > | Window | Covers | > |---|---| From 4b7facf61492450d569e7bfd9d74764dd508bc15 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Mon, 11 May 2026 10:52:34 -0700 Subject: [PATCH 12/13] Strengthen Invoca prior-art framing and link existing additivity tests MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three related edits, all on the upstream-facing draft: 1. Rename 'Regression tests' (Proposed additions #3) to 'Invariant tests'. 'Regression' connoted defensive backsliding-protection, which understates the role: these tests codify the contract being proposed. They are the contract; regression defense is the side effect. 2. Add a permalink in §3 to Invoca's already-landed additivity_* block on the invoca-2.55.1/align-yrate-to-3x-range-boundary branch. Pinned to the commit SHA so the L531-L593 range stays stable as the file grows. Notes that uniform / earlier-reset / later-reset are covered; off-cadence and partial-dataset still to add. 3. In Related prior art, expand the '~5 years in production' sentence to actually say what we learned: composability via additivity is the most valuable property of the family in practice (dashboards zoom, recording rules roll up, alerts fire without partition-boundary artifacts). The original wording named the duration but not the lesson. 4. Tighten 'Happy to contribute' since the porting claim is now redundant with §3's concrete link. Co-authored-by: Cursor --- docs/proposals/anchored-composability-invariant.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/proposals/anchored-composability-invariant.md b/docs/proposals/anchored-composability-invariant.md index b90fdfe5bc2..4d0d602a6ec 100644 --- a/docs/proposals/anchored-composability-invariant.md +++ b/docs/proposals/anchored-composability-invariant.md @@ -72,21 +72,23 @@ The proposal's partial-dataset example (lines 231–237) — *"The first window ## Related prior art -This property is the design goal of the Invoca `yrate` family (referenced in the PROM-52 "Other docs or links" as [Prometheus y-rate](https://docs.google.com/document/d/1CF5jhyxSD437c2aU2wHcvg88i8CjSPO3kMHsEaDRe2w/edit)). Invoca has run `yrate`-semantics in production for ~5 years with this invariant as a documented contract; `anchored + increase` converges on the same behavior via a cleaner modifier-based syntax that avoids function proliferation. +This property is the design goal of the Invoca `yrate` family (referenced in the PROM-52 "Other docs or links" as [Prometheus y-rate](https://docs.google.com/document/d/1CF5jhyxSD437c2aU2wHcvg88i8CjSPO3kMHsEaDRe2w/edit)). Invoca has run `yrate`-semantics in production for ~5 years with this invariant as a documented contract — long enough to find that composability via additivity is the most valuable property of the family in practice: dashboards zoom across granularities without numerical surprises, recording rules roll up cleanly, and alerts fire reliably on windowed counter increases without partition-boundary artifacts. `anchored + increase` converges on the same behavior via a cleaner modifier-based syntax that avoids function proliferation. ## Proposed additions 1. **User-facing docs** (`docs/feature_flags.md` and the `anchored` entry under `docs/querying/functions.md`): a short callout stating the invariant. 2. **Proposal amendment** (`prometheus/proposals#…`): one paragraph under "How" linking the invariant to the "composability" goal. -3. **Regression tests** (`promql/promqltest/testdata/…`): paired-window cases asserting the invariant across: +3. **Invariant tests** (`promql/promqltest/testdata/…`): paired-window cases asserting the invariant across: - Regular scrape cadence, boundary timestamps aligned with sample cadence - Same, but shifted off-cadence (to exercise the `last_in` / `anchor` coincidence) - Ranges containing counter resets on both sides of `T₁` - Partial datasets with missing scrapes straddling `T₁` + Invoca's public fork already has a working version of these — see the `additivity_*` block in [`promql/promqltest/testdata/functions.test#L531-L593`](https://github.com/Invoca/prometheus/blob/4bf7c401e55f2376a40382e2be5fb838f4b9f517/promql/promqltest/testdata/functions.test#L531-L593). The three scenarios there cover uniform counters, a reset in the earlier window, and a reset in the later window; the partial-dataset and off-cadence cases on the list above are straightforward to add on top. + ## Happy to contribute -I can split this into two PRs — docs first for quick review, then tests — and port test-data patterns from our internal `yrate` suite that have exercised this invariant for years. Please let me know if a proposal amendment is preferred before or after the docs/tests land. +I can split this into two PRs — docs first for quick review, then tests. The test patterns linked in §3 above are ready to port: they have been part of Invoca's `yrate` suite for years and were recently formalized as the `additivity_*` block on our public fork. Please let me know if a proposal amendment is preferred before or after the docs/tests land. --- From 20e6ea9eaf0e86813fc9c7ea0de0393747613fe9 Mon Sep 17 00:00:00 2001 From: Colin Kelley Date: Mon, 11 May 2026 10:55:42 -0700 Subject: [PATCH 13/13] Drop 'add on top' framing for invariant tests; claim full coverage MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Our existing additivity_* block already covers what §3 asks for: * Off-cadence boundary timestamps -- deliberate, called out in the block header. * Counter resets in the earlier window (Scenario 2) and the later window (Scenario 3). * Partial-dataset / missed-scrape semantics -- the last_in / anchor lookups treat off-cadence boundaries and missing samples through the same engine code paths, so the existing scenarios exercise that behavior without needing a separate 'gap' test. Rewording §3's link sentence to claim full coverage rather than 'three scenarios, more to add on top'. Reviewer can verify against the L531-L593 permalink. Co-authored-by: Cursor --- docs/proposals/anchored-composability-invariant.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/proposals/anchored-composability-invariant.md b/docs/proposals/anchored-composability-invariant.md index 4d0d602a6ec..6c44364b172 100644 --- a/docs/proposals/anchored-composability-invariant.md +++ b/docs/proposals/anchored-composability-invariant.md @@ -84,7 +84,7 @@ This property is the design goal of the Invoca `yrate` family (referenced in the - Ranges containing counter resets on both sides of `T₁` - Partial datasets with missing scrapes straddling `T₁` - Invoca's public fork already has a working version of these — see the `additivity_*` block in [`promql/promqltest/testdata/functions.test#L531-L593`](https://github.com/Invoca/prometheus/blob/4bf7c401e55f2376a40382e2be5fb838f4b9f517/promql/promqltest/testdata/functions.test#L531-L593). The three scenarios there cover uniform counters, a reset in the earlier window, and a reset in the later window; the partial-dataset and off-cadence cases on the list above are straightforward to add on top. + Invoca's public fork already has a working version of these — see the `additivity_*` block in [`promql/promqltest/testdata/functions.test#L531-L593`](https://github.com/Invoca/prometheus/blob/4bf7c401e55f2376a40382e2be5fb838f4b9f517/promql/promqltest/testdata/functions.test#L531-L593). All three scenarios use deliberately off-cadence boundary timestamps (so the `last_in`/`anchor` paths get exercised the same way they would under partial-dataset/missed-scrape conditions); two of the three include counter resets, one in the earlier window and one in the later window. ## Happy to contribute