docs(lstar): tidy docstring summaries in slot, checkpoint, state (#1145)

Reword the justification-candidate summary as a noun phrase per the
noun-phrase summary rule, collapse the checkpoint advance docstring to a
single accurate summary while keeping the forward-only invariant, and
drop the self-contradicting first-person phrasing in the justified-slot
range comment.

Docs-only, no behavior change. just check passes.

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: tcoratger

src/lean_spec/spec/forks/lstar/containers/checkpoint.py

@@ -22,11 +22,10 @@ class Checkpoint(Container):
 
     def advance_to(self, candidate: "Checkpoint") -> "Checkpoint":
         """
-        Return the later of two checkpoints, keeping this one on a slot tie.
-
-        Forward-only progression for justified and finalized checkpoints.
+        The later of two checkpoints, keeping this one on a slot tie.
 
         The candidate replaces this checkpoint only when its slot is strictly higher.
+        This enforces forward-only progression for justified and finalized checkpoints.
         """
         return candidate if candidate.slot > self.slot else self
 

src/lean_spec/spec/forks/lstar/containers/state.py

@@ -58,7 +58,7 @@ def is_slot_justified(self, finalized_slot: Slot, target_slot: Slot) -> Boolean:
 
         # Check the tracked bitfield for the slot's status.
         #
-        # We assume the slot is within the tracked range.
+        # The slot is expected within the tracked range.
         #
         # If the caller asks for a slot too far in the future, it indicates a logic error.
         # Surface it as a domain rejection so the uniform rejection funnel catches it,

src/lean_spec/spec/forks/lstar/slot.py

@@ -27,7 +27,7 @@ def justified_index_after(self, finalized_slot: "Slot") -> int | None:
 
     def is_justifiable_after(self, finalized_slot: "Slot") -> bool:
         """
-        Checks if this slot is a valid candidate for justification after a given finalized slot.
+        Whether this slot is a valid justification candidate after a given finalized slot.
 
         According to the 3SF-mini specification, a slot is justifiable if its
         distance (delta) from the last finalized slot is: