docs: update invariant references in documentation for accuracy (#10)

* docs: update invariant references in documentation for accuracy

* refactor: update invariants and descriptions for clarity and consistency across documentation

* refactor: update invariants and documentation for cache consistency and rebalance execution

---------

Co-authored-by: Mykyta Zotov <mykyta.zotov@ihsmarkit.com>

Author: blaze6950

AGENTS.md

@@ -224,7 +224,7 @@ catch (Exception ex)
 - **Strong consistency**: `GetDataAndWaitForIdleAsync` — always waits for idle regardless of `CacheInteraction`
 
 **Serialized Access Requirement for Hybrid/Strong Modes:**
-`GetDataAndWaitOnMissAsync` and `GetDataAndWaitForIdleAsync` provide their warm-cache guarantee only under **serialized (one-at-a-time) access**. Under parallel access, `WaitForIdleAsync`'s "was idle at some point" semantics (Invariant H.49) may return the old completed TCS, missing the rebalance triggered by the concurrent request. These methods remain safe (no crashes/hangs) but the guarantee degrades under parallelism.
+`GetDataAndWaitOnMissAsync` and `GetDataAndWaitForIdleAsync` provide their warm-cache guarantee only under **serialized (one-at-a-time) access**. Under parallel access, `WaitForIdleAsync`'s "was idle at some point" semantics (Invariant H.3) may return the old completed TCS, missing the rebalance triggered by the concurrent request. These methods remain safe (no crashes/hangs) but the guarantee degrades under parallelism.
 
 **Lock-Free Operations:**
 ```csharp

README.md

@@ -402,7 +402,7 @@ Canonical guide: `docs/diagnostics.md`.
 
 By default, `GetDataAsync` is **eventually consistent**: data is returned immediately while the cache window converges asynchronously in the background. Two opt-in extension methods provide stronger consistency guarantees. Both require a `using SlidingWindowCache.Public;` import.
 
-> **Serialized access requirement:** The hybrid and strong consistency modes provide their warm-cache guarantee only when requests are made one at a time (serialized). Under concurrent/parallel callers they remain safe (no crashes or hangs) but the guarantee degrades — due to `AsyncActivityCounter`'s "was idle at some point" semantics (Invariant H.49) and a brief gap between the counter increment and TCS publication in `IncrementActivity`, a concurrent waiter may observe a previously completed idle TCS and return without waiting for the new rebalance.
+> **Serialized access requirement:** The hybrid and strong consistency modes provide their warm-cache guarantee only when requests are made one at a time (serialized). Under concurrent/parallel callers they remain safe (no crashes or hangs) but the guarantee degrades — due to `AsyncActivityCounter`'s "was idle at some point" semantics (Invariant H.3) and a brief gap between the counter increment and TCS publication in `IncrementActivity`, a concurrent waiter may observe a previously completed idle TCS and return without waiting for the new rebalance.
 
 ### Eventual Consistency (Default)
 

docs/actors.md

@@ -35,19 +35,18 @@ Non-responsibilities
 - Does not compute `DesiredCacheRange` (belongs to Cache Geometry Policy).
 
 Invariant ownership
-- -1. User Path and Rebalance Execution never write to cache concurrently
-- 0. User Path has higher priority than rebalance execution
-- 0a. User Request MAY cancel any ongoing or pending Rebalance Execution ONLY when a new rebalance is validated as necessary
-- 1. User Path always serves user requests
-- 2. User Path never waits for rebalance execution
-- 3. User Path is the sole source of rebalance intent
-- 5. Performs only work necessary to return data
-- 6. May synchronously request from IDataSource
-- 7. May read cache and source, but does not mutate cache state
-- 8. MUST NOT mutate cache under any circumstance (read-only)
-- 10. Always returns exactly RequestedRange
-- 24e. Intent MUST contain delivered data (RangeData)
-- 24f. Delivered data represents what user actually received
+- A.1. User Path and Rebalance Execution never write to cache concurrently
+- A.2. User Path has higher priority than rebalance execution
+- A.2a. User Request MAY cancel any ongoing or pending Rebalance Execution ONLY when a new rebalance is validated as necessary
+- A.3. User Path always serves user requests
+- A.4. User Path never waits for rebalance execution
+- A.5. User Path is the sole source of rebalance intent
+- A.7. Performs only work necessary to return data
+- A.8. May synchronously request from IDataSource
+- A.11. May read cache and source, but does not mutate cache state
+- A.12. MUST NOT mutate cache under any circumstance (read-only)
+- C.8e. Intent MUST contain delivered data (RangeData)
+- C.8f. Delivered data represents what user actually received
 
 Components
 - `WindowCache<TRange, TData, TDomain>` (facade / composition root; also owns `RuntimeCacheOptionsHolder` and exposes `UpdateRuntimeOptions`)
@@ -69,12 +68,12 @@ Non-responsibilities
 - Does not perform I/O.
 
 Invariant ownership
-- 29. DesiredCacheRange computed from RequestedRange + config
-- 30. Independent of current cache contents
-- 31. Canonical target cache state
-- 32. Sliding window geometry defined by configuration
-- 33. NoRebalanceRange derived from current cache range + config
-- 35. Threshold sum constraint (leftThreshold + rightThreshold ≤ 1.0)
+- E.1. DesiredCacheRange computed from RequestedRange + config
+- E.2. Independent of current cache contents
+- E.3. Canonical target cache state
+- E.4. Sliding window geometry defined by configuration
+- E.5. NoRebalanceRange derived from current cache range + config
+- E.6. Threshold sum constraint (leftThreshold + rightThreshold ≤ 1.0)
 
 Components
 - `ProportionalRangePlanner<TRange, TDomain>` — computes `DesiredCacheRange`; reads configuration from `RuntimeCacheOptionsHolder` at invocation time
@@ -95,11 +94,11 @@ Non-responsibilities
 - Does not call `IDataSource`.
 
 Invariant ownership
-- 24. Decision Path is purely analytical (CPU-only, no I/O)
-- 25. Never mutates cache state
-- 26. No rebalance if inside NoRebalanceRange (Stage 1 validation)
-- 27. No rebalance if DesiredCacheRange == CurrentCacheRange (Stage 4 validation)
-- 28. Rebalance triggered only if ALL validation stages confirm necessity
+- D.1. Decision Path is purely analytical (CPU-only, no I/O)
+- D.2. Never mutates cache state
+- D.3. No rebalance if inside NoRebalanceRange (Stage 1 validation)
+- D.4. No rebalance if DesiredCacheRange == CurrentCacheRange (Stage 4 validation)
+- D.5. Rebalance triggered only if ALL validation stages confirm necessity
 
 Components
 - `RebalanceDecisionEngine<TRange, TDomain>`
@@ -121,14 +120,14 @@ Non-responsibilities
 - Does not determine rebalance necessity (delegates to Decision Engine).
 
 Invariant ownership
-- 17. At most one active rebalance intent
-- 18. Older intents may become logically superseded
-- 19. Executions can be cancelled based on validation results
-- 20. Obsolete intent must not start execution
-- 21. At most one rebalance execution active
-- 22. Execution reflects latest access pattern and validated necessity
-- 23. System eventually stabilizes under load through work avoidance
-- 24. Intent does not guarantee execution — execution is opportunistic and validation-driven
+- C.1. At most one active rebalance intent
+- C.2. Older intents may become logically superseded
+- C.3. Executions can be cancelled based on validation results
+- C.4. Obsolete intent must not start execution
+- C.5. At most one rebalance execution active
+- C.6. Execution reflects latest access pattern and validated necessity
+- C.7. System eventually stabilizes under load through work avoidance
+- C.8. Intent does not guarantee execution — execution is opportunistic and validation-driven
 
 Components
 - `IntentController<TRange, TData, TDomain>`
@@ -164,18 +163,18 @@ Non-responsibilities
 - Does not check if `DesiredCacheRange == CurrentCacheRange` (Stage 4 already passed).
 
 Invariant ownership
-- A.4. Rebalance is asynchronous relative to User Path
-- F.35. MUST support cancellation at all stages
-- F.35a. MUST yield to User Path requests immediately upon cancellation
-- F.35b. Partially executed or cancelled execution MUST NOT leave cache inconsistent
-- F.36. Only path responsible for cache normalization (single-writer architecture)
-- F.36a. Mutates cache ONLY for normalization using delivered data from intent
-- F.37. May replace / expand / shrink cache to achieve normalization
-- F.38. Requests data only for missing subranges (not covered by delivered data)
-- F.39. Does not overwrite intersecting data
-- F.40. Upon completion: CacheData corresponds to DesiredCacheRange
-- F.41. Upon completion: CurrentCacheRange == DesiredCacheRange
-- F.42. Upon completion: NoRebalanceRange recomputed
+- A.6. Rebalance is asynchronous relative to User Path
+- F.1. MUST support cancellation at all stages
+- F.1a. MUST yield to User Path requests immediately upon cancellation
+- F.1b. Partially executed or cancelled execution MUST NOT leave cache inconsistent
+- F.2. Only path responsible for cache normalization (single-writer architecture)
+- F.2a. Mutates cache ONLY for normalization using delivered data from intent
+- F.3. May replace / expand / shrink cache to achieve normalization
+- F.4. Requests data only for missing subranges (not covered by delivered data)
+- F.5. Does not overwrite intersecting data
+- F.6. Upon completion: CacheData corresponds to DesiredCacheRange
+- F.7. Upon completion: CurrentCacheRange == DesiredCacheRange
+- F.8. Upon completion: NoRebalanceRange recomputed
 
 Components
 - `RebalanceExecutor<TRange, TData, TDomain>`
@@ -190,12 +189,12 @@ Responsibilities
 - Coordinate single-writer access between User Path (reads) and Rebalance Execution (writes).
 
 Invariant ownership
-- 11. CacheData and CurrentCacheRange are consistent
-- 12. Changes applied atomically
-- 13. No permanent inconsistent state
-- 14. Temporary inefficiencies are acceptable
-- 15. Partial / cancelled execution cannot break consistency
-- 16. Only latest intent results may be applied
+- B.1. CacheData and CurrentCacheRange are consistent
+- B.2. Changes applied atomically
+- B.3. No permanent inconsistent state
+- B.4. Temporary inefficiencies are acceptable
+- B.5. Partial / cancelled execution cannot break consistency
+- B.6. Only latest intent results may be applied
 
 Components
 - `CacheState<TRange, TData, TDomain>`

docs/components/decision.md

@@ -75,6 +75,6 @@ The system prioritizes **decision correctness and work avoidance** over aggressi
 
 ## See Also
 
-- `docs/invariants.md` — formal Decision Path invariant specifications (D.24–D.29)
+- `docs/invariants.md` — formal Decision Path invariant specifications (D.1–D.5)
 - `docs/architecture.md` — Decision-Driven Execution section
 - `docs/components/overview.md` — Invariant Implementation Mapping (Decision subsection)

docs/components/execution.md

@@ -53,7 +53,7 @@ The execution subsystem performs debounced, cancellable background work and is t
 6. Update `CacheState.NoRebalanceRange` — new stability zone
 7. Set `CacheState.IsInitialized = true` (if first execution)
 
-**Cancellation checkpoints** (Invariant F.35):
+**Cancellation checkpoints** (Invariant F.1):
 - Before I/O: avoids unnecessary fetches
 - After I/O: discards fetched data if superseded
 - Before mutation: guarantees only latest validated execution applies changes
@@ -67,7 +67,7 @@ The execution subsystem performs debounced, cancellable background work and is t
 - Merges new data with preserved existing data (union operation)
 - Propagates `CancellationToken` to `IDataSource.FetchAsync`
 
-**Invariants**: F.38 (incremental fetching), F.39 (data preservation during expansion).
+**Invariants**: F.4 (incremental fetching), F.5 (data preservation during expansion).
 
 ## Responsibilities
 
@@ -100,21 +100,21 @@ In both cases, `OperationCanceledException` is reported via `ICacheDiagnostics.R
 
 | Invariant | Description                                                                                            |
 |-----------|--------------------------------------------------------------------------------------------------------|
-| A.7       | Only `RebalanceExecutor` writes to `CacheState` (single-writer)                                        |
-| A.8       | User path never blocks waiting for rebalance                                                           |
-| B.12      | Cache updates are atomic (all-or-nothing via `Rematerialize`)                                          |
-| B.13      | Consistency under cancellation: mutations discarded if cancelled                                       |
-| B.15      | Cache contiguity maintained after every `Rematerialize`                                                |
-| B.16      | Obsolete results never applied (cancellation token identity check)                                     |
-| C.21      | Serial execution: at most one active rebalance at a time                                               |
-| F.35      | Multiple cancellation checkpoints: before I/O, after I/O, before mutation                              |
-| F.35a     | Cancellation-before-mutation guarantee                                                                 |
-| F.37      | `Rematerialize` accepts arbitrary range and data (full replacement)                                    |
-| F.38      | Incremental fetching: only missing subranges fetched                                                   |
-| F.39      | Data preservation: existing cached data merged during expansion                                        |
-| G.45      | I/O isolation: `IDataSource` called by execution path only (not by user path during normal cache hits) |
-| H.47      | Activity counter incremented before channel write / task chain step                                    |
-| H.48      | Activity counter decremented in `finally` blocks                                                       |
+| A.12a/F.2 | Only `RebalanceExecutor` writes to `CacheState` (single-writer)                                        |
+| A.4       | User path never blocks waiting for rebalance                                                           |
+| B.2       | Cache updates are atomic (all-or-nothing via `Rematerialize`)                                          |
+| B.3       | Consistency under cancellation: mutations discarded if cancelled                                       |
+| B.5       | Cancelled rebalance cannot violate `CacheData ↔ CurrentCacheRange` consistency                        |
+| B.6       | Obsolete results never applied (cancellation token identity check)                                     |
+| C.5       | Serial execution: at most one active rebalance at a time                                               |
+| F.1       | Multiple cancellation checkpoints: before I/O, after I/O, before mutation                              |
+| F.1a      | Cancellation-before-mutation guarantee                                                                 |
+| F.3       | `Rematerialize` accepts arbitrary range and data (full replacement)                                    |
+| F.4       | Incremental fetching: only missing subranges fetched                                                   |
+| F.5       | Data preservation: existing cached data merged during expansion                                        |
+| G.3       | I/O isolation: User Path MAY call `IDataSource` for U1/U5 (cold start / full miss); Rebalance Execution calls it for background normalization only |
+| H.1       | Activity counter incremented before channel write / task chain step                                    |
+| H.2       | Activity counter decremented in `finally` blocks                                                       |
 
 See `docs/invariants.md` (Sections A, B, C, F, G, H) for full specification.
 

docs/components/intent-management.md

@@ -24,7 +24,7 @@ Intent management bridges the user path and background work. It receives access
 Called by `UserRequestHandler` after serving a request:
 
 1. Atomically replaces pending intent via `Interlocked.Exchange` (latest wins; previous intent superseded)
-2. Increments `AsyncActivityCounter` (before signalling — ordering required by Invariant H.47)
+2. Increments `AsyncActivityCounter` (before signalling — ordering required by Invariant H.1)
 3. Releases semaphore (wakes up `ProcessIntentsAsync` if sleeping)
 4. Records `RebalanceIntentPublished` diagnostic event
 5. Returns immediately (fire-and-forget)
@@ -80,15 +80,15 @@ User burst: intent₁ → intent₂ → intent₃
 
 | Invariant | Description                                                              |
 |-----------|--------------------------------------------------------------------------|
-| C.17      | At most one pending intent at any time (atomic replacement)              |
-| C.18      | Previous intents become obsolete when superseded                         |
-| C.19      | Cancellation is cooperative via `CancellationToken`                      |
-| C.20      | Cancellation checked after debounce before execution starts              |
-| C.21      | At most one active rebalance scheduled at a time                         |
-| C.24      | Intent does not guarantee execution                                      |
-| C.24e     | Intent carries `deliveredData` (the data the user actually received)     |
-| H.47      | Activity counter incremented before semaphore signal (ordering)          |
-| H.48      | Activity counter decremented in `finally` blocks (unconditional cleanup) |
+| C.1       | At most one pending intent at any time (atomic replacement)              |
+| C.2       | Previous intents become obsolete when superseded                         |
+| C.3       | Cancellation is cooperative via `CancellationToken`                      |
+| C.4       | Cancellation checked after debounce before execution starts              |
+| C.5       | At most one active rebalance scheduled at a time                         |
+| C.8       | Intent does not guarantee execution                                      |
+| C.8e      | Intent carries `deliveredData` (the data the user actually received)     |
+| H.1       | Activity counter incremented before semaphore signal (ordering)          |
+| H.2       | Activity counter decremented in `finally` blocks (unconditional cleanup) |
 
 See `docs/invariants.md` (Section C: Intent invariants, Section H: Activity counter invariants) for full specification.