From 5dc137d11ce140b382ec51fd85b6b052f5716dc4 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Wed, 12 Aug 2026 16:47:05 +0530
Subject: [PATCH] fix(ltl): serialize the resolved deadline of a bounded window

Two obligations spawned at different steps from one duration-bounded formula
differ only in the deadline the evaluator resolved for them, so they serialized
identically and the trace erased a distinction the evaluator makes. The authored
window stays in amount/unit; the resolved deadline rides alongside.

Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
---
 internal/ltl/formula.go      | 57 +++++++++++++++++++++++++-----------
 internal/ltl/formula_test.go | 29 ++++++++++++++++++
 2 files changed, 69 insertions(+), 17 deletions(-)

diff --git a/internal/ltl/formula.go b/internal/ltl/formula.go
index afb96c4..748a5ec 100644
--- a/internal/ltl/formula.go
+++ b/internal/ltl/formula.go
@@ -219,10 +219,43 @@ func (n NotFormula) describe() string { return "Not(" + n.Inner.describe() + ")"
 func Describe(formula Formula) string { return formula.describe() }
 
 // withinNode mirrors the optional `within` clause attached to bounded
-// Eventually nodes in the JSON AST.
+// Always/Eventually nodes in the JSON AST.
 type withinNode struct {
 	Amount int64  `json:"amount"`
 	Unit   string `json:"unit"`
+	// Deadline is the absolute instant the window closes, in unix
+	// milliseconds, present once the evaluator resolved a relative duration
+	// against an observation. Two obligations spawned at different steps from
+	// the same duration differ only here, so without it they serialize
+	// identically and the trace erases the distinction the evaluator makes.
+	Deadline int64 `json:"deadline,omitempty"`
+}
+
+// withinFor renders the bound clause of a bounded Always or Eventually. The
+// authored window (steps or duration) stays in amount/unit so readers keep
+// seeing what the spec asked for; the resolved deadline rides alongside.
+func withinFor(
+	hasStepBound bool,
+	stepBound int,
+	duration time.Duration,
+	hasDeadline bool,
+	deadline time.Time,
+) *withinNode {
+	var node *withinNode
+	switch {
+	case hasStepBound:
+		node = &withinNode{Amount: int64(stepBound), Unit: "steps"}
+	case duration > 0:
+		node = &withinNode{Amount: duration.Milliseconds(), Unit: "milliseconds"}
+	case hasDeadline:
+		return &withinNode{Amount: deadline.UnixMilli(), Unit: "deadline"}
+	default:
+		return nil
+	}
+	if hasDeadline {
+		node.Deadline = deadline.UnixMilli()
+	}
+	return node
 }
 
 func (a AlwaysFormula) MarshalJSON() ([]byte, error) {
@@ -231,14 +264,9 @@ func (a AlwaysFormula) MarshalJSON() ([]byte, error) {
 		Arg    Formula     `json:"arg"`
 		Within *withinNode `json:"within,omitempty"`
 	}{Op: "always", Arg: a.Inner}
-	switch {
-	case a.HasStepBound:
-		payload.Within = &withinNode{Amount: int64(a.StepBound), Unit: "steps"}
-	case a.Duration > 0:
-		payload.Within = &withinNode{Amount: a.Duration.Milliseconds(), Unit: "milliseconds"}
-	case a.HasDeadline:
-		payload.Within = &withinNode{Amount: a.Deadline.UnixMilli(), Unit: "deadline"}
-	}
+	payload.Within = withinFor(
+		a.HasStepBound, a.StepBound, a.Duration, a.HasDeadline, a.Deadline,
+	)
 	return json.Marshal(payload)
 }
 
@@ -269,14 +297,9 @@ func (e EventuallyFormula) MarshalJSON() ([]byte, error) {
 		Arg    Formula     `json:"arg"`
 		Within *withinNode `json:"within,omitempty"`
 	}{Op: "eventually", Arg: e.Inner}
-	switch {
-	case e.HasStepBound:
-		payload.Within = &withinNode{Amount: int64(e.StepBound), Unit: "steps"}
-	case e.Duration > 0:
-		payload.Within = &withinNode{Amount: e.Duration.Milliseconds(), Unit: "milliseconds"}
-	case e.HasDeadline:
-		payload.Within = &withinNode{Amount: e.Deadline.UnixMilli(), Unit: "deadline"}
-	}
+	payload.Within = withinFor(
+		e.HasStepBound, e.StepBound, e.Duration, e.HasDeadline, e.Deadline,
+	)
 	return json.Marshal(payload)
 }
 
diff --git a/internal/ltl/formula_test.go b/internal/ltl/formula_test.go
index ffb700e..455c208 100644
--- a/internal/ltl/formula_test.go
+++ b/internal/ltl/formula_test.go
@@ -288,3 +288,32 @@ func TestResidual_HoldsViolatedPending(t *testing.T) {
 		t.Errorf("pending residual:\n got: %s\nwant: %s", body, want)
 	}
 }
+
+// TestMarshalJSON_ResolvedDeadlineDistinguishesObligations: obligations spawned
+// at different steps from one duration-bounded eventually differ only in the
+// deadline the evaluator resolved for them, and collapse keeps them apart on
+// exactly that. The serialized AST has to keep them apart too, or the trace
+// shows N copies of one node where the evaluator has N different obligations.
+func TestMarshalJSON_ResolvedDeadlineDistinguishesObligations(t *testing.T) {
+	base := time.UnixMilli(1700000000000)
+	first := EventuallyFormula{
+		Inner:       PureFormula{Value: false},
+		Duration:    300 * time.Second,
+		Deadline:    base.Add(300 * time.Second),
+		HasDeadline: true,
+	}
+	second := first
+	second.Deadline = base.Add(301 * time.Second)
+
+	firstBody, _ := json.Marshal(first)
+	secondBody, _ := json.Marshal(second)
+	if string(firstBody) == string(secondBody) {
+		t.Errorf("obligations with different deadlines serialize identically: %s", firstBody)
+	}
+	if !strings.Contains(string(firstBody), `"unit":"milliseconds"`) {
+		t.Errorf("authored window lost: %s", firstBody)
+	}
+	if !strings.Contains(string(firstBody), `"deadline":1700000300000`) {
+		t.Errorf("resolved deadline missing: %s", firstBody)
+	}
+}