diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go index a24de88..bae320f 100644 --- a/internal/ltl/evaluator.go +++ b/internal/ltl/evaluator.go @@ -37,6 +37,11 @@ type Evaluator struct { violated bool steps int violation *Violation + // observations counts the states this evaluator actually reduced, which is + // what a `within(n, "steps")` window is measured in. It differs from steps + // whenever the caller's numbering skipped an observation, and the two are + // told apart in the serialized AST by expiresAtObservation. + observations int // oneShot marks a root that is armed once at the first observation rather // than re-asserted at every one; armed records that it has been. oneShot bool @@ -93,6 +98,7 @@ func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict { return VerdictViolated } e.steps = step + e.observations++ obligations := make([]obligation, 0, len(e.pending)+1) obligations = append(obligations, e.pending...) @@ -102,7 +108,7 @@ func (e *Evaluator) ObserveAtStep(now time.Time, step int) Verdict { e.pending = e.pending[:0] for _, entry := range obligations { - result := reduce(entry.formula, now) + result := reduce(entry.formula, now, e.observations) switch result.status { case statusHolds: // drop @@ -374,7 +380,11 @@ func pending(f Formula) reduceResult { return reduceResult{status: statusPending, formula: f} } -func reduce(formula Formula, now time.Time) reduceResult { +// reduce advances one obligation against the current state. `now` is the +// observation's wall clock and `observation` its index in the sequence of +// states this evaluator reduced; the two are the clocks a duration-bounded and +// a step-bounded window are resolved against. +func reduce(formula Formula, now time.Time, observation int) reduceResult { switch concrete := formula.(type) { case PureFormula: if concrete.Value { @@ -399,7 +409,7 @@ func reduce(formula Formula, now time.Time) reduceResult { return violatedWith(concrete, "predicate false") case NowFormula: - return reduce(concrete.Inner, now) + return reduce(concrete.Inner, now, observation) case NextFormula: // Next defers the inner obligation to the following step without @@ -414,23 +424,24 @@ func reduce(formula Formula, now time.Time) reduceResult { concrete.Deadline = now.Add(concrete.Duration) concrete.HasDeadline = true } - innerResult := reduce(concrete.Inner, now) + if concrete.HasStepBound && !concrete.HasExpiryObservation { + concrete.ExpiryObservation = observation + concrete.StepBound - 1 + concrete.HasExpiryObservation = true + } + innerResult := reduce(concrete.Inner, now, observation) if innerResult.status == statusHolds { return holds() } // The window is measured in observations at which the inner could have // discharged, so an inner that is merely pending has not discharged and // the window closing on it is a violation. - if concrete.HasStepBound && concrete.StepBound <= 1 { + if concrete.HasExpiryObservation && observation >= concrete.ExpiryObservation { return violatedFrom(innerResult, concrete, "eventually bound exhausted") } if concrete.HasDeadline && !now.Before(concrete.Deadline) { return violatedFrom(innerResult, concrete, "eventually deadline reached") } next := concrete - if concrete.HasStepBound { - next.StepBound = concrete.StepBound - 1 - } // F(inner) unrolls to inner or X F(inner). A pending inner is a // deferred way of satisfying the promise, so it is kept as a disjunct // rather than dropped; dropping it is what made an inner that only @@ -449,11 +460,11 @@ func reduce(formula Formula, now time.Time) reduceResult { return reduce(OrFormula{ Left: pushNot(concrete.Antecedent), Right: nnf(concrete.Consequent), - }, now) + }, now, observation) case OrFormula: - left := reduce(concrete.Left, now) - right := reduce(concrete.Right, now) + left := reduce(concrete.Left, now, observation) + right := reduce(concrete.Right, now, observation) if left.status == statusHolds || right.status == statusHolds { return holds() } @@ -469,8 +480,8 @@ func reduce(formula Formula, now time.Time) reduceResult { return pending(OrFormula{Left: left.formula, Right: right.formula}) case AndFormula: - left := reduce(concrete.Left, now) - right := reduce(concrete.Right, now) + left := reduce(concrete.Left, now, observation) + right := reduce(concrete.Right, now, observation) if left.status == statusViolated { return violatedFrom(left, concrete, "conjunct violated") } @@ -489,7 +500,7 @@ func reduce(formula Formula, now time.Time) reduceResult { return pending(AndFormula{Left: left.formula, Right: right.formula}) case NotFormula: - inner := reduce(concrete.Inner, now) + inner := reduce(concrete.Inner, now, observation) switch inner.status { case statusHolds: return violatedWith(concrete, "negated formula held") @@ -506,7 +517,11 @@ func reduce(formula Formula, now time.Time) reduceResult { concrete.Deadline = now.Add(concrete.Duration) concrete.HasDeadline = true } - innerResult := reduce(concrete.Inner, now) + if concrete.HasStepBound && !concrete.HasExpiryObservation { + concrete.ExpiryObservation = observation + concrete.StepBound - 1 + concrete.HasExpiryObservation = true + } + innerResult := reduce(concrete.Inner, now, observation) if innerResult.status == statusViolated { return violatedFrom(innerResult, concrete, "always inner violated") } @@ -517,16 +532,13 @@ func reduce(formula Formula, now time.Time) reduceResult { // hold". A pending inner has not been breached inside the window, so it // discharges vacuously here exactly as its negation violates on the // Eventually side. - if concrete.HasStepBound && concrete.StepBound <= 1 { + if concrete.HasExpiryObservation && observation >= concrete.ExpiryObservation { return holds() } if concrete.HasDeadline && !now.Before(concrete.Deadline) { return holds() } next := concrete - if concrete.HasStepBound { - next.StepBound = concrete.StepBound - 1 - } if innerResult.status == statusHolds { return pending(next) } diff --git a/internal/ltl/formula.go b/internal/ltl/formula.go index 748a5ec..759564d 100644 --- a/internal/ltl/formula.go +++ b/internal/ltl/formula.go @@ -39,12 +39,14 @@ func (e ErrorFormula) describe() string { // window and is vacuously satisfied once the window closes. An unbounded // Always carries no bound fields and is checked at every observed step. type AlwaysFormula struct { - Inner Formula - StepBound int - HasStepBound bool - Duration time.Duration - Deadline time.Time - HasDeadline bool + Inner Formula + StepBound int + HasStepBound bool + ExpiryObservation int + HasExpiryObservation bool + Duration time.Duration + Deadline time.Time + HasDeadline bool } type PureFormula struct { @@ -91,13 +93,20 @@ type NextFormula struct { // resolves the absolute deadline on first reduction using the observation // time. This matches the "within N seconds of obligation instantiation" // semantics used by nested Always(Eventually(...).within(...)) formulas. +// +// StepBound is the step-domain counterpart: the window counts observations the +// evaluator reduced, and ExpiryObservation is the absolute closing observation +// the evaluator resolves on first reduction, exactly as Deadline is for +// Duration. type EventuallyFormula struct { - Inner Formula - StepBound int - HasStepBound bool - Duration time.Duration - Deadline time.Time - HasDeadline bool + Inner Formula + StepBound int + HasStepBound bool + ExpiryObservation int + HasExpiryObservation bool + Duration time.Duration + Deadline time.Time + HasDeadline bool } type ImpliesFormula struct { @@ -179,6 +188,9 @@ func (a AlwaysFormula) describe() string { if a.HasStepBound { parts = append(parts, fmt.Sprintf("steps=%d", a.StepBound)) } + if a.HasExpiryObservation { + parts = append(parts, fmt.Sprintf("expiresAtObservation=%d", a.ExpiryObservation)) + } if a.HasDeadline { parts = append(parts, "deadline="+a.Deadline.Format(time.RFC3339Nano)) } else if a.Duration > 0 { @@ -197,6 +209,9 @@ func (e EventuallyFormula) describe() string { if e.HasStepBound { parts = append(parts, fmt.Sprintf("steps=%d", e.StepBound)) } + if e.HasExpiryObservation { + parts = append(parts, fmt.Sprintf("expiresAtObservation=%d", e.ExpiryObservation)) + } if e.HasDeadline { parts = append(parts, "deadline="+e.Deadline.Format(time.RFC3339Nano)) } else if e.Duration > 0 { @@ -229,33 +244,73 @@ type withinNode struct { // 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"` + // ExpiresAtObservation is the step-domain counterpart of Deadline: the + // index of the observation the window closes at. It names observations + // rather than runner steps because a step the verifier skipped never + // reached the evaluator and so cannot close a window; the pair of fields + // is what lets a reader tell the two numberings apart. + ExpiresAtObservation int `json:"expiresAtObservation,omitempty"` +} + +// boundWindow is the optional window shared by AlwaysFormula and +// EventuallyFormula: the window the spec authored plus the absolute close the +// evaluator resolved for this obligation. +type boundWindow struct { + hasStepBound bool + stepBound int + hasExpiryObservation bool + expiryObservation int + duration time.Duration + hasDeadline bool + deadline time.Time } // 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 +// seeing what the spec asked for; the resolved close rides alongside. +func withinFor(window boundWindow) *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"} + case window.hasStepBound: + node := &withinNode{Amount: int64(window.stepBound), Unit: "steps"} + if window.hasExpiryObservation { + node.ExpiresAtObservation = window.expiryObservation + } + return node + case window.duration > 0: + node := &withinNode{Amount: window.duration.Milliseconds(), Unit: "milliseconds"} + if window.hasDeadline { + node.Deadline = window.deadline.UnixMilli() + } + return node + case window.hasDeadline: + return &withinNode{Amount: window.deadline.UnixMilli(), Unit: "deadline"} default: return nil } - if hasDeadline { - node.Deadline = deadline.UnixMilli() +} + +func (a AlwaysFormula) boundWindow() boundWindow { + return boundWindow{ + hasStepBound: a.HasStepBound, + stepBound: a.StepBound, + hasExpiryObservation: a.HasExpiryObservation, + expiryObservation: a.ExpiryObservation, + duration: a.Duration, + hasDeadline: a.HasDeadline, + deadline: a.Deadline, + } +} + +func (e EventuallyFormula) boundWindow() boundWindow { + return boundWindow{ + hasStepBound: e.HasStepBound, + stepBound: e.StepBound, + hasExpiryObservation: e.HasExpiryObservation, + expiryObservation: e.ExpiryObservation, + duration: e.Duration, + hasDeadline: e.HasDeadline, + deadline: e.Deadline, } - return node } func (a AlwaysFormula) MarshalJSON() ([]byte, error) { @@ -264,9 +319,7 @@ func (a AlwaysFormula) MarshalJSON() ([]byte, error) { Arg Formula `json:"arg"` Within *withinNode `json:"within,omitempty"` }{Op: "always", Arg: a.Inner} - payload.Within = withinFor( - a.HasStepBound, a.StepBound, a.Duration, a.HasDeadline, a.Deadline, - ) + payload.Within = withinFor(a.boundWindow()) return json.Marshal(payload) } @@ -297,9 +350,7 @@ func (e EventuallyFormula) MarshalJSON() ([]byte, error) { Arg Formula `json:"arg"` Within *withinNode `json:"within,omitempty"` }{Op: "eventually", Arg: e.Inner} - payload.Within = withinFor( - e.HasStepBound, e.StepBound, e.Duration, e.HasDeadline, e.Deadline, - ) + payload.Within = withinFor(e.boundWindow()) return json.Marshal(payload) } diff --git a/internal/ltl/nnf.go b/internal/ltl/nnf.go index 51d07ca..9fa438e 100644 --- a/internal/ltl/nnf.go +++ b/internal/ltl/nnf.go @@ -65,21 +65,25 @@ func pushNot(formula Formula) Formula { return NextFormula{Inner: pushNot(concrete.Inner)} case AlwaysFormula: return EventuallyFormula{ - Inner: pushNot(concrete.Inner), - StepBound: concrete.StepBound, - HasStepBound: concrete.HasStepBound, - Duration: concrete.Duration, - Deadline: concrete.Deadline, - HasDeadline: concrete.HasDeadline, + Inner: pushNot(concrete.Inner), + StepBound: concrete.StepBound, + HasStepBound: concrete.HasStepBound, + ExpiryObservation: concrete.ExpiryObservation, + HasExpiryObservation: concrete.HasExpiryObservation, + Duration: concrete.Duration, + Deadline: concrete.Deadline, + HasDeadline: concrete.HasDeadline, } case EventuallyFormula: return AlwaysFormula{ - Inner: pushNot(concrete.Inner), - StepBound: concrete.StepBound, - HasStepBound: concrete.HasStepBound, - Duration: concrete.Duration, - Deadline: concrete.Deadline, - HasDeadline: concrete.HasDeadline, + Inner: pushNot(concrete.Inner), + StepBound: concrete.StepBound, + HasStepBound: concrete.HasStepBound, + ExpiryObservation: concrete.ExpiryObservation, + HasExpiryObservation: concrete.HasExpiryObservation, + Duration: concrete.Duration, + Deadline: concrete.Deadline, + HasDeadline: concrete.HasDeadline, } default: return NotFormula{Inner: formula} diff --git a/internal/ltl/step_bound_test.go b/internal/ltl/step_bound_test.go new file mode 100644 index 0000000..ffecdfd --- /dev/null +++ b/internal/ltl/step_bound_test.go @@ -0,0 +1,195 @@ +package ltl + +import ( + "encoding/json" + "strings" + "testing" + "time" +) + +func alwaysFalse() func() (bool, error) { + return func() (bool, error) { return false, nil } +} + +// A step-bounded window counts the observations the evaluator reduced, and the +// residual has to keep saying which window the spec authored rather than the +// part of it that is left. Bug class: the replay UI renders "within N steps" +// straight off the residual, so a shrinking N tells the reader the spec asked +// for a window it never asked for. +func TestStepBoundedEventually_ResidualKeepsAuthoredWindow(t *testing.T) { + evaluator := NewEvaluator(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 5)) + for index := range 3 { + if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending { + t.Fatalf("observation %d: got %v, want pending", index+1, got) + } + } + + body, err := json.Marshal(evaluator.Residual()) + if err != nil { + t.Fatal(err) + } + if !strings.Contains(string(body), `"unit":"steps"`) || !strings.Contains(string(body), `"amount":5`) { + t.Errorf("authored window lost after reduction: %s", body) + } + if !strings.Contains(string(body), `"expiresAtObservation":5`) { + t.Errorf("resolved expiry missing: %s", body) + } +} + +// Two obligations spawned at different observations from one `within(n, +// "steps")` window close at different observations, and the serialized AST has +// to keep them apart the way a resolved deadline keeps two duration-bounded +// ones apart. Bug class: the trace shows one node where the evaluator holds +// several distinct obligations. +func TestStepBoundedEventually_ObligationsSerializeApart(t *testing.T) { + evaluator := NewEvaluator(Always(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 3))) + for index := range 2 { + if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending { + t.Fatalf("observation %d: got %v, want pending", index+1, got) + } + } + + body, err := json.Marshal(evaluator.Residual()) + if err != nil { + t.Fatal(err) + } + text := string(body) + if strings.Count(text, `"amount":3`) != 2 { + t.Errorf("both obligations should report the authored window of 3: %s", text) + } + if !strings.Contains(text, `"expiresAtObservation":3`) || !strings.Contains(text, `"expiresAtObservation":4`) { + t.Errorf("obligations armed at different observations share a closing observation: %s", text) + } +} + +// A bounded Always is the dual of a bounded Eventually, so its window resolves +// and serializes the same way. +func TestStepBoundedAlways_ResidualKeepsAuthoredWindow(t *testing.T) { + formula := AlwaysFormula{ + Inner: ThunkNamed("p", func() (bool, error) { return true, nil }), + StepBound: 4, + HasStepBound: true, + } + evaluator := NewEvaluator(formula) + for index := range 2 { + if got := evaluator.ObserveAt(time.Unix(int64(index), 0)); got != VerdictPending { + t.Fatalf("observation %d: got %v, want pending", index+1, got) + } + } + + body, err := json.Marshal(evaluator.Residual()) + if err != nil { + t.Fatal(err) + } + if !strings.Contains(string(body), `"amount":4`) { + t.Errorf("authored window lost after reduction: %s", body) + } + if !strings.Contains(string(body), `"expiresAtObservation":4`) { + t.Errorf("resolved expiry missing: %s", body) + } +} + +// A step the verifier skipped (a transitional tree, an empty hierarchy) never +// reached the evaluator, so the property was given no chance to discharge +// there and the window must not charge for it. The runner's step numbering +// only labels the witness; it does not drive the window. +func TestStepBoundedEventually_SkippedRunnerStepsDoNotConsumeWindow(t *testing.T) { + observed := 0 + inner := ThunkNamed("p", func() (bool, error) { + observed++ + return observed == 3, nil + }) + evaluator := NewEvaluator(EventuallyWithinSteps(inner, 3)) + + var verdict Verdict + for _, runnerStep := range []int{1, 7, 19} { + verdict = evaluator.ObserveAtStep(time.Unix(int64(runnerStep), 0), runnerStep) + } + if verdict != VerdictHolds { + t.Errorf("three observations inside a three-observation window: got %v, want holds", verdict) + } +} + +// The witness still carries the runner's numbering, so a report names the step +// that armed the obligation even though the window counted observations. +func TestStepBoundedEventually_WitnessCarriesRunnerStep(t *testing.T) { + evaluator := NewEvaluator(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 2)) + for _, runnerStep := range []int{4, 11} { + evaluator.ObserveAtStep(time.Unix(int64(runnerStep), 0), runnerStep) + } + + witness := evaluator.Violation() + if witness == nil { + t.Fatal("no violation recorded") + } + if witness.Step != 4 { + t.Errorf("witness Step = %d, want the runner step that armed the obligation (4)", witness.Step) + } +} + +// An undischarged bounded eventually is a broken liveness promise at run end +// whatever unit bounded it. Bug class: choosing "steps" over "seconds" quietly +// turning an unmet obligation into a vacuous pass. +func TestFinalize_StepBoundedEventuallyMatchesWallClock(t *testing.T) { + byStep, stepEvaluator := runAndFinalize(EventuallyWithinSteps(ThunkNamed("p", alwaysFalse()), 50), 3) + byClock, clockEvaluator := runAndFinalize(EventuallyWithin(ThunkNamed("p", alwaysFalse()), time.Hour), 3) + + if byStep != VerdictViolated || byClock != VerdictViolated { + t.Fatalf("step bound = %v, wall clock = %v, want both violated", byStep, byClock) + } + stepWitness, clockWitness := stepEvaluator.Violation(), clockEvaluator.Violation() + if stepWitness == nil || clockWitness == nil { + t.Fatal("both undischarged obligations must carry a witness") + } + if stepWitness.Reason != clockWitness.Reason { + t.Errorf("reasons diverge: step %q, wall clock %q", stepWitness.Reason, clockWitness.Reason) + } + if stepWitness.Step != clockWitness.Step { + t.Errorf("origin steps diverge: step %d, wall clock %d", stepWitness.Step, clockWitness.Step) + } +} + +// The reason the unit exists. Two action-selection policies get the same +// 300-step budget and reach the same state at the same step, but the model +// policy takes 359 seconds where the seeded policy takes 47 because it makes a +// provider call per step. A wall-clock bound fails the slow policy on elapsed +// time alone; the same window written in steps decides both policies alike. +func TestStepBound_SlowPolicyDoesNotFailOnTimeAlone(t *testing.T) { + const budget = 300 + const satisfiedAtObservation = 260 + seededCadence := 47 * time.Second / budget + modelCadence := 359 * time.Second / budget + + run := func(cadence time.Duration, bound func(Formula) Formula) Verdict { + observed := 0 + inner := ThunkNamed("someTransactionExists", func() (bool, error) { + observed++ + return observed >= satisfiedAtObservation, nil + }) + evaluator := NewEvaluator(bound(inner)) + base := time.Unix(1780000000, 0) + for index := range budget { + verdict := evaluator.ObserveAtStep(base.Add(time.Duration(index)*cadence), index+1) + if verdict != VerdictPending { + return verdict + } + } + return evaluator.Finalize() + } + + byClock := func(inner Formula) Formula { return EventuallyWithin(inner, 300*time.Second) } + bySteps := func(inner Formula) Formula { return EventuallyWithinSteps(inner, 1915) } + + if got := run(seededCadence, byClock); got != VerdictHolds { + t.Errorf("wall-clock bound under the seeded policy: got %v, want holds", got) + } + if got := run(modelCadence, byClock); got != VerdictViolated { + t.Errorf("wall-clock bound under the model policy: got %v, want violated (the false positive this unit removes)", got) + } + if got := run(seededCadence, bySteps); got != VerdictHolds { + t.Errorf("step bound under the seeded policy: got %v, want holds", got) + } + if got := run(modelCadence, bySteps); got != VerdictHolds { + t.Errorf("step bound under the model policy: got %v, want holds", got) + } +}