fix(hotblocks): keep the finalized head when retention passes it

crates/hotblocks-harness/src/compare.rs

@@ -203,14 +203,15 @@ pub async fn assert_conforms(client: &Client, model: &Model, chain: &dyn Chain,
     if observed != expected {
         errs.push(format!("STATUS: expected {expected:?}, got {observed:?}"));
     }
-    // INV-5/30: first <= fin <= head, in one consistent view.
+    // INV-5/30: fin <= head, in one consistent view. `fin` may sit below the window —
+    // retention can pass finality, and the watermark survives as a claim about the chain.
     if let Some(data) = &status.data {
         if let Some(fin) = &data.finalized_head
-            && !(data.first_block <= fin.number && fin.number <= data.last_block)
+            && fin.number > data.last_block
         {
             errs.push(format!(
-                "INV-5: finalized head {} outside [{}, {}]",
-                fin.number, data.first_block, data.last_block
+                "INV-5: finalized head {} above the head {}",
+                fin.number, data.last_block
             ));
         }
         let head_ts = model

crates/hotblocks-harness/src/model.rs

@@ -131,18 +131,21 @@ impl Model {
             }
         }
         if let Some(fin) = &self.fin {
-            let first = self.first().expect("INV-5: finalized watermark without a window");
             let head = self.head().expect("INV-5: finalized watermark without a window").number;
             assert!(
-                first <= fin.number && fin.number <= head,
-                "INV-5: finalized watermark {} outside [{first}, {head}]",
+                fin.number <= head,
+                "INV-5: finalized watermark {} above the head {head}",
                 fin.number
             );
-            assert_eq!(
-                self.block_at(fin.number).map(|b| b.hash.as_str()),
-                Some(fin.hash.as_str()),
-                "INV-6: finalized watermark does not name the stored block"
-            );
+            // `fin` may sit below the window: a trim keeps it as a claim about the chain
+            // (finality does not move back), and no stored block backs it there.
+            if fin.number >= self.first().expect("INV-5: window without a first block") {
+                assert_eq!(
+                    self.block_at(fin.number).map(|b| b.hash.as_str()),
+                    Some(fin.hash.as_str()),
+                    "INV-6: finalized watermark does not name the stored block"
+                );
+            }
         }
     }
 
@@ -377,10 +380,11 @@ impl Model {
             }
             self.seg.drain(..drop);
             self.anchor = Anchor::new(new_anchor.number, Some(new_anchor.hash));
-            // RS-2: the finalized watermark cannot survive below the window.
-            if let Some(fin) = &self.fin
-                && fin.number < from
-            {
+            // `fin` survives below the window: finality does not move back, so the trim
+            // deletes the finalized blocks but keeps the watermark as a claim about the
+            // chain. A trim that empties the window is the exception — an empty window
+            // has no head to bound the watermark (INV-5), and the label clears with it.
+            if self.seg.is_empty() {
                 self.fin = None;
             }
             self.ver += 1;
@@ -437,9 +441,19 @@ impl Model {
             // be replaced (WP-6): the finalized block is common to both chains unless the
             // source contradicts finality — repeated rejection here is FM-SRC-5, never RESET.
             None => match &self.fin {
-                Some(fin) => ForkResolution::Resume {
-                    from: fin.number + 1,
-                    parent_hash: Some(fin.hash.clone())
+                Some(fin) => match self.first() {
+                    // WP-6: a trim may leave `fin` below the window (RS-2). Everything
+                    // stored then sits above the watermark, the finality floor is vacuous,
+                    // and the fallback is the window start with its anchor — `fin + 1`
+                    // would be a position INV-14 forbids `replace` from taking.
+                    Some(first) if fin.number + 1 < first => ForkResolution::Resume {
+                        from: first,
+                        parent_hash: self.anchor.hash.clone()
+                    },
+                    _ => ForkResolution::Resume {
+                        from: fin.number + 1,
+                        parent_hash: Some(fin.hash.clone())
+                    }
                 },
                 // Full-window replacement *probe*; repeated WP-2 rejection at `first(D)`
                 // escalates to RESET per WP-6b.
@@ -724,15 +738,19 @@ mod tests {
     }
 
     #[test]
-    fn retain_trims_moves_the_anchor_and_drops_stale_finality() {
+    fn retain_trims_moves_the_anchor_and_keeps_finality_below_the_window() {
         let (mut m, blocks) = model_at(100, 10);
         m.finalize(&BlockRef::new(101, block_hash(101, 0)));
 
         m.retain(105, None);
 
         assert_eq!(m.first(), Some(105));
         assert_eq!(m.anchor, Anchor::new(104, Some(blocks[4].hash.clone())), "INV-18");
-        assert_eq!(m.fin, None, "RS-2: finality below the window is dropped");
+        assert_eq!(
+            m.fin,
+            Some(BlockRef::new(101, block_hash(101, 0))),
+            "finality does not move back: the watermark survives below the window"
+        );
         assert_eq!(m.head().unwrap().number, 109);
         assert_eq!(
             m.finalize(&BlockRef::new(104, blocks[4].hash.clone())),
@@ -745,6 +763,29 @@ mod tests {
         assert_eq!(m.first(), Some(105));
     }
 
+    #[test]
+    fn retain_that_empties_the_window_clears_finality() {
+        let (mut m, blocks) = model_at(100, 10);
+        m.finalize(&BlockRef::new(101, block_hash(101, 0)));
+
+        // RETAIN at `next` keeps nothing: an empty window has no head to bound the
+        // watermark (INV-5), and the service clears the label with the data.
+        m.retain(110, None);
+
+        assert!(m.seg.is_empty());
+        assert_eq!(m.fin, None);
+        assert_eq!(m.anchor, Anchor::new(109, Some(blocks[9].hash.clone())), "INV-18");
+        assert_eq!(m.next(), 110);
+
+        // Re-trimming at the same floor changes nothing, and the window re-attaches
+        // at the anchor the trim left.
+        m.retain(110, None);
+        assert!(m.seg.is_empty());
+
+        m.extend(&run(110, 2, 0, &blocks[9].hash), None).unwrap();
+        assert_eq!(m.first(), Some(110));
+    }
+
     #[test]
     fn retain_below_the_window_is_a_destructive_reset() {
         let (mut m, _) = model_at(100, 10);
@@ -827,6 +868,32 @@ mod tests {
         );
     }
 
+    #[test]
+    fn resolve_fork_with_finality_below_the_window_falls_back_to_the_window_start() {
+        let (mut m, _) = model_at(100, 10);
+        m.finalize(&BlockRef::new(101, block_hash(101, 0)));
+        m.retain(105, None);
+
+        // The watermark (101) sits below the window (105..109): `fin + 1` names a
+        // position INV-14 forbids, so the fallback is the window start with its anchor.
+        let hints = vec![
+            BlockRef::new(107, block_hash(107, 9)),
+            BlockRef::new(108, block_hash(108, 9)),
+        ];
+        assert_eq!(
+            m.resolve_fork(&hints).unwrap(),
+            ForkResolution::Resume {
+                from: 105,
+                parent_hash: Some(block_hash(104, 0))
+            }
+        );
+
+        // The resume point is a position `replace` accepts.
+        let fork = run(105, 2, 9, &block_hash(104, 0));
+        m.replace(105, &fork, None).unwrap();
+        assert_eq!(m.head().unwrap().hash, block_hash(106, 9));
+    }
+
     #[test]
     fn resolve_fork_contradicting_the_anchor_resets() {
         let (m, _) = model_at(100, 5);

crates/hotblocks/spec/02-data-model.md

@@ -116,9 +116,11 @@ protocol anchors a client or a source to a position — the anchor (DEF-7),
 **not** "a block numbered `p` has hash `h`". The two readings coincide exactly on
 densely-numbered chains.
 
-**DEF-8 (Finalized watermark).** `fin`, when defined, designates a stored block
-(`first ≤ fin.number ≤ head.number`, hash matching the stored block — INV-5/6) that the
-sources have declared irreversible. Blocks at or below `fin.number` form the **finalized
+**DEF-8 (Finalized watermark).** `fin`, when defined, designates a block
+(`fin.number ≤ head.number` — INV-5) that the sources have declared irreversible. When
+`fin.number ≥ first(D)` it matches the stored block at that height (INV-6); a trim may
+leave it below the window, where it survives as a claim about the chain (RS-2) with no
+stored block behind it. Blocks at or below `fin.number` form the **finalized
 prefix**; blocks above it are the **volatile suffix**, subject to replacement by forks.
 
 **DEF-9 (Retention policy).** One of:

crates/hotblocks/spec/03-write-path.md

@@ -140,7 +140,9 @@ the stored chain (or the anchor). If no hint matches stored state, the fallback
 respect the finality floor:
 
 - `fin ≠ ⊥` → resume from `⟨fin.number + 1, fin.hash⟩`, or from any lower physical position
-  `≥ chunk_first(D)` whose replacement reproduces the finalized prefix (INV-14). The finalized
+  `≥ chunk_first(D)` whose replacement reproduces the finalized prefix (INV-14). When
+  `fin` sits below the window (kept by a trim, RS-2), everything stored is above it, the
+  finality floor is vacuous, and the fallback position is `chunk_first(D)`. The finalized
   block is common to both chains unless the source contradicts finality, so only the
   volatile suffix carries new data either way. An implementation whose REPLACE granularity
   is a storage chunk MUST take the lower position when `fin` falls inside a chunk: `fin + 1`
@@ -236,18 +238,20 @@ history cannot be re-acquired through RETAIN.
   destructive re-bootstrap, not a widening, and controllers MUST treat it as such
   (FM-OP-4). During boot validation of a `Pinned` policy whose `from` lies below the
   stored window, the service MUST refuse the dataset (INV-43) rather than destroy data —
-  symmetric with WP-9. *Finality note:* like every RESET (§2.6) and like upward trims
-  (RS-2), this discards the finalized prefix and clears `fin` — retention dominates
-  finality. It is **not** a rollback below `fin`: the fork floor (INV-13/14) is
+  symmetric with WP-9. *Finality note:* like every RESET (§2.6), this discards the
+  finalized prefix and clears `fin` — retention dominates finality (upward trims keep
+  `fin`, §2.5). It is **not** a rollback below `fin`: the fork floor (INV-13/14) is
   untouched — *sources* can never alter anything at or below `fin` — and this path is
   reachable only through an explicit retention instruction (operator-class actor,
   FM-OP-4), never through source input.
 - Case `first(D) < from ≤ next(D)`:
   - Post: `seg' = seg[from‥]`; `anchor' = ⟨from − 1, hash of from's preceding block in
     the pre-trim state⟩` (= `hash_at(from − 1)`, DEF-16). The hash MUST be carried over
     from previously stored data, never recomputed or dropped (INV-18);
-  - `fin' = fin` if `fin.number ≥ from`, else `fin' = ⊥` (retention dominates finality,
-    RS-2).
+  - `fin' = fin`: finality does not move back, so the watermark survives below the window
+    as a claim about the chain (RS-2) and keeps anchoring responses until finality climbs
+    back in. Exception: `from = next(D)` leaves `seg' = ∅`, and an empty window has no head
+    to bound the watermark (`seg = ∅ ⇒ fin = ⊥`, INV-5) — the label clears with the data.
 - Case `from > next(D)`: equivalent to `RESET(⟨from − 1, h?⟩)` — the whole window is
   discarded and the dataset awaits future blocks.
 - **WP-9 (Mismatch policy).** If `h?` is provided and disagrees with the stored chain's

crates/hotblocks/spec/06-invariants.md

@@ -43,13 +43,16 @@ enclosing block's number.
 *Check:* CT-1, CT-5 structural validators.
 
 **INV-5 — Watermark bounds.** [state]
-If `seg = ∅` then `fin = ⊥`. Otherwise, if `fin ≠ ⊥` then
-`first(D) ≤ fin.number ≤ head(D).number`.
-*Why:* a finalized pointer outside the window is meaningless and breaks fork-floor logic.
-*Check:* CT-1 (assert on every STATUS read).
+If `seg = ∅` then `fin = ⊥`. Otherwise, if `fin ≠ ⊥` then `fin.number ≤ head(D).number`;
+a trim may leave `fin.number < first(D)` (RS-2).
+*Why:* finality does not move back, so a watermark below the window stays a true claim
+about the chain and clients read the whole window as unfinalized; above the head it
+would be meaningless and break fork-floor logic.
+*Check:* CT-1 (assert on every STATUS read); retention passing finality (CT-10).
 
 **INV-6 — Finalized-on-chain.** [state]
-If `fin ≠ ⊥` then the stored block at height `fin.number` has hash `fin.hash`.
+If `fin ≠ ⊥` and `fin.number ≥ first(D)`, then the stored block at height `fin.number`
+has hash `fin.hash`. Below the window no stored block backs the watermark.
 *Why:* finality must describe the chain actually served, else finalized-only reads lie.
 *Check:* CT-1; CT-4 with equivocating-finality sources; write-controller finality
 resolver regressions.
@@ -77,7 +80,7 @@ previous head.
 
 **INV-12 — Finality monotonicity.** [transition]
 `fin.number` never decreases while defined, and at a fixed height the finalized hash never
-changes. `fin` may become `⊥` only via RETAIN (window passing above it), RESET, or DROP.
+changes. `fin` may become `⊥` only via a RETAIN that empties the window, RESET, or DROP.
 *Why:* clients treat finalized data as irreversible-while-retained.
 *Check:* CT-1 (monitor every FINALIZED-HEAD read); CT-4 stale/regressing finality sources.
 

crates/hotblocks/spec/09-retention-and-space.md

@@ -16,10 +16,14 @@ between them.
 | `Unbounded` | nothing trimmed | never |
 
 - **RS-2 (Retention dominates finality).** Trimming ignores `fin`: finalized blocks below
-  the retention bound are deleted, and `fin` becomes `⊥` when the window passes above it
-  (03 §2.5). Rationale: this is a bounded hot store, not an archive (NG1). Consequence
-  for clients: "finalized" means *irreversible while retained*, not *retained forever*
-  (INV-24 note).
+  the retention bound are deleted. The watermark itself survives below the window
+  (03 §2.5): finality does not move back, so `fin` stays a true claim about the chain,
+  responses keep reporting it, and clients read the whole window as unfinalized. Only a
+  RESET — or a trim that empties the window, where `seg = ∅` forces `fin = ⊥` (INV-5) —
+  clears it. Rationale: this is a bounded hot store, not an archive (NG1).
+  Consequence for clients: "finalized" means *irreversible*, not *retained forever*
+  (INV-24 note) — blocks at or below `fin.number` may be gone even while `fin` reports
+  them final.
 - **RS-3 (Availability floor).** For `Window(k)`: at every committed state,
   all blocks in `[next(D) − k, next(D) − 1] ∩ [window start after initial fill, ∞)` are
   present and queryable (an interval of *positions* — DEF-9; on a slot-numbered chain it

crates/hotblocks/spec/12-conformance-tdd.md

@@ -123,7 +123,10 @@ model Dataset:
         if h != ⊥ and h != hash_at(from_ - 1): return reset((from_ - 1, h))   # WP-9 self-heal
         new_anchor = (from_ - 1, hash_at(from_ - 1))                          # INV-18 (DEF-16)
         seg = [b in seg | b.number >= from_]; anchor = new_anchor
-        if fin != ⊥ and fin.number < from_: fin = ⊥                           # RS-2
+        if not seg: fin = ⊥                            # from_ = next() emptied the window:
+                                                         # no head bounds the watermark (INV-5)
+        # RS-2: `fin` survives below the window — finality does not move back, so the
+        # watermark stays a true claim about the chain and keeps anchoring responses.
         ver += 1; wf()
     else:
         reset((from_ - 1, h))                        # from_ > next()
@@ -141,7 +144,12 @@ model Dataset:
         return RESET((anchor.number, hint hash at that position))  # WP-6b: below-window divergence
     m = max({x in hints | stored_or_anchor(x)}, default=⊥)
     if m != ⊥: return (m.number + 1, m.hash)
-    if fin != ⊥: return (fin.number + 1, fin.hash)   # or any lower position reproducing the
+    if fin != ⊥:
+        if seg and fin.number + 1 < first(): return (first(), anchor.hash)
+                                                     # fin sits below the window (RS-2): the
+                                                     # finality floor is vacuous, so the fallback
+                                                     # is the window start (WP-6)
+        return (fin.number + 1, fin.hash)   # or any lower position reproducing the
                                                      # finalized prefix (INV-14) — a batch-granular
                                                      # implementation must, when fin sits inside a
                                                      # batch. Repeated rejection here = FM-SRC-5,

crates/hotblocks/src/dataset_controller/write_controller.rs

@@ -291,15 +291,11 @@ impl WriteController {
                                 .next()
                                 .expect("bottom chunk can't exist without head chunk")?;
 
-                            let finalized_head = tx
-                                .label()
-                                .finalized_head()
-                                .filter(|h| chunk.first_block() <= h.number)
-                                .cloned();
-
-                            if finalized_head.is_none() {
-                                tx.set_finalized_head(None)
-                            }
+                            // Finality does not move back, so the head stays true even when
+                            // the trim leaves it below the window. Dropping it would strip
+                            // finality information from every response until the chain's
+                            // finality climbs back into the window.
+                            let finalized_head = tx.label().finalized_head().cloned();
 
                             return Ok(Status::Range {
                                 first_chunk: chunk,
@@ -1668,6 +1664,61 @@ mod tests {
         Ok(())
     }
 
+    // Finality does not move back, so a trim that passes the finalized head keeps it as a
+    // claim about the chain: every block left in the window is then unfinalized, and
+    // responses keep reporting the head instead of losing finality information.
+    #[test]
+    fn a_trim_past_the_finalized_head_keeps_it() -> anyhow::Result<()> {
+        let mut f = fixture();
+        let (_, second) = seed_chain(&mut f)?;
+        let finalized = block(3, "old-3");
+        f.wc.finalize(&finalized)?;
+
+        assert!(f.wc.retain(6, None)?);
+
+        assert_eq!(stored_chunks(&f)?, vec![second]);
+        assert_eq!(f.wc.start_block(), 6);
+        assert_eq!(*f.fin_rx.borrow(), Some(finalized.clone()));
+        assert_eq!(
+            f.db.snapshot()
+                .get_label(f.dataset_id)?
+                .and_then(|label| label.finalized_head().cloned()),
+            Some(finalized)
+        );
+        Ok(())
+    }
+
+    // The kept head survives a writer restart, and while it sits below the window a report
+    // below the window changes nothing while one inside the window raises it.
+    #[test]
+    fn a_kept_head_below_the_window_survives_and_advances() -> anyhow::Result<()> {
+        let mut f = fixture();
+        seed_chain(&mut f)?;
+        f.wc.finalize(&block(3, "old-3"))?;
+        f.wc.retain(6, None)?;
+        drop(f.wc);
+
+        let (head_tx, _head_rx) = watch::channel(None);
+        let (fin_tx, fin_rx) = watch::channel(None);
+        let mut wc = WriteController::new(f.db.clone(), f.dataset_id, DatasetKind::Evm, head_tx, fin_tx)?;
+        assert_eq!(*fin_rx.borrow(), Some(block(3, "old-3")));
+
+        wc.finalize(&block(4, "old-4"))?;
+        assert_eq!(
+            *fin_rx.borrow(),
+            Some(block(3, "old-3")),
+            "a below-window report must not move the head"
+        );
+
+        wc.finalize(&block(7, "old-7"))?;
+        assert_eq!(
+            *fin_rx.borrow(),
+            Some(block(7, "old-7")),
+            "an in-window report must raise the head"
+        );
+        Ok(())
+    }
+
     // `fin` anchors the finalized-prefix guard and every later `compute_rollback`, so a report
     // naming a hash the chunk does not carry is an equivocation, not a detail.
     #[test]