fix(search,minimize): validate replay outcomes and allow deadlocked invariant minimization

src/main/java/dev/samhb/interleave/minimize/DeltaDebugger.java

@@ -77,26 +77,24 @@ public Trace minimize(Program program, Trace failingTrace, TraceOutcome expected
      * Checks whether replaying the given trace still produces the expected outcome.
      *
      * <p>Replays the trace from the initial state using {@link ExecutionDriver} and
-     * verifies the final configuration matches the expected outcome. For VIOLATION
-     * outcomes, the invariant is re-checked to ensure the trace genuinely reproduces
-     * the bug.
+     * verifies the final configuration matches the expected outcome. Only thread choices are
+     * replayed; recorded step outcomes and the trace's terminal verdict are ignored. Replay
+     * stops when the schedule is consumed or all threads terminate.
      *
-     * <p><b>The VIOLATION guard is not {@code isDeadlockCandidate()}, and must not be "simplified" into
-     * it.</b> The guard below expands to {@code !allTerminated() && !enabled.isEmpty()} — live threads
-     * <em>and</em> something still enabled — which is a different predicate from "not a deadlock". Using
-     * the canonical predicate here would accept deadlocked configurations that violate the invariant,
-     * and would let the minimiser shrink a trace into one that ends in a state the search would have
-     * classified differently. The cost of the current form is that a violation occurring in a deadlocked
-     * state is not recognised as still failing, so such a trace cannot be minimised. That is a real
-     * limitation, but fixing it changes which traces the minimiser accepts and needs its own
-     * specification and tests rather than a quiet edit here. Recorded in
-     * {@code docs/specs/active/13-deferred-debt/03-canonical-configuration-key.md}.
+     * <p>For {@code VIOLATION} outcomes with an invariant, the invariant predicate is evaluated
+     * directly regardless of thread termination or deadlock status, ensuring invariant violations
+     * occurring in deadlocked terminal configurations are recognized and minimizable. When no invariant
+     * is supplied, fallback checks require live threads and non-deadlocked configurations.
+     *
+     * <p>An {@link IllegalScheduleException} from replay or invariant evaluation produces
+     * {@code false}; other runtime exceptions propagate to the caller.
      *
      * @param program the program to replay
      * @param trace the trace to replay
      * @param expectedOutcome the expected outcome to verify
      * @param invariant the invariant to check for VIOLATION outcomes; may be null
-     * @return true if the replayed trace reproduces the expected outcome
+     * @return true if the final configuration satisfies the selected outcome check;
+     *         false for an illegal schedule or {@code INCOMPLETE}
      */
     private boolean isStillFailing(Program program, Trace trace, TraceOutcome expectedOutcome, Invariant invariant) {
         try {
@@ -108,7 +106,7 @@ private boolean isStillFailing(Program program, Trace trace, TraceOutcome expect
                 case COMPLETED -> config.allTerminated();
                 case DEADLOCK -> config.isDeadlockCandidate();
                 case VIOLATION -> invariant != null
-                    ? !config.allTerminated() && !config.isDeadlockCandidate() && !invariant.holds(config.state(), config)
+                    ? !invariant.holds(config.state(), config)
                     : !config.allTerminated() && !config.isDeadlockCandidate();
                 // INCOMPLETE describes the search, not a schedule: it means the preemption bound
                 // was reached. No replay of a prefix can reproduce that, so reporting true here

src/main/java/dev/samhb/interleave/search/CorruptedTraceException.java

@@ -0,0 +1,16 @@
+/** Signals a recorded trace outcome that diverges from actual step execution. */
+package dev.samhb.interleave.search;
+
+/**
+ * Signals that replaying a recorded step produced an execution outcome that disagrees
+ * with the outcome recorded in the trace.
+ */
+public class CorruptedTraceException extends RuntimeException {
+    /**
+     * Creates corrupted trace exception with diagnostic message.
+     * @param message diagnostic explaining the outcome mismatch
+     */
+    public CorruptedTraceException(String message) {
+        super(message);
+    }
+}

src/main/java/dev/samhb/interleave/search/TraceReplayer.java

@@ -9,19 +9,21 @@ public final class TraceReplayer {
     public TraceReplayer() {}
 
     /**
-     * Replays thread choices while trusting the step outcomes recorded in the trace.
+     * Replays thread choices while validating each step outcome against the trace.
      *
      * <p>The program supplies a fresh initial configuration. Each chosen step mutates that
-     * configuration’s state; the recorded outcome, rather than the returned execution outcome,
-     * controls counter advancement. This method does not validate trace consistency or verdicts.
-     * Callers must supply aligned thread/outcome lists and valid thread IDs and counters.
+     * configuration’s state and must produce the outcome recorded in the trace.
+     * An empty trace returns the initial configuration. Replay does not reject a chosen step
+     * solely because it is disabled, or validate the trace's terminal verdict. Exceptions from
+     * model callbacks propagate to the caller.
      *
      * <pre>{@code
      * Configuration end = new TraceReplayer().replay(program, trace);
      * }</pre>
      * @param program program whose initial state and steps are replayed
      * @param trace recorded thread choices and outcomes
      * @return configuration after the recorded prefix has been executed
+     * @throws CorruptedTraceException if an executed step outcome differs from the trace outcome
      * @throws IndexOutOfBoundsException if a recorded thread, counter, or outcome index is invalid
      */
     public Configuration replay(Program program, Trace trace) {
@@ -35,10 +37,17 @@ public Configuration replay(Program program, Trace trace) {
             int pc = config.programCounters().get(threadId);
             Step step = thread.steps().get(pc);
 
-            step.execute(config.state());
+            StepOutcome actualOutcome = step.execute(config.state());
+            if (actualOutcome != outcome) {
+                throw new CorruptedTraceException(
+                    "Trace outcome mismatch at step " + i + " (thread " + threadId + "): "
+                    + "recorded " + outcome + " but execution produced " + actualOutcome
+                );
+            }
             config = config.successor(threadId, outcome, program.threads(), config.state());
         }
 
         return config;
     }
 }
+

src/test/java/dev/samhb/interleave/minimize/DeltaDebuggerTest.java

@@ -92,4 +92,58 @@ void minimize_returnsSubsequence() {
         assertTrue(minimizedIndex == minimizedThreadIds.size(),
             "Minimized trace should be a subsequence of original");
     }
+
+    @Test
+    void minimize_invariantViolationInDeadlockedConfiguration_succeeds() {
+        // T0 writes counter=1 then blocks on a condition that never becomes true.
+        // T1 performs an irrelevant read then terminates.
+        // Invariant asserts counter != 1.
+        // The terminal configuration is deadlocked (T0 live and blocked; T1 terminated),
+        // yet violates the invariant. DeltaDebugger should accept and minimize this trace.
+        Program program = new Program(CounterState.of(0), List.of(
+            new ModelThread(0, List.of(
+                new WriteCounterStep(0),
+                new Step() {
+                    @Override
+                    public boolean enabled(SharedState state) {
+                        return false; // permanently blocked -> deadlock candidate
+                    }
+
+                    @Override
+                    public StepOutcome execute(SharedState state) {
+                        return StepOutcome.BLOCKED;
+                    }
+
+                    @Override
+                    public Set<MemoryLocation> reads() {
+                        return Set.of();
+                    }
+
+                    @Override
+                    public Set<MemoryLocation> writes() {
+                        return Set.of();
+                    }
+                }
+            )),
+            new ModelThread(1, List.of(new ReadCounterStep(1)))
+        ));
+
+        Invariant invariant = (state, config) -> ((CounterState) state).counter() != 1;
+        Trace failing = Trace.of(
+            List.of(1, 0),
+            List.of(StepOutcome.ADVANCED, StepOutcome.ADVANCED),
+            TraceOutcome.VIOLATION
+        );
+
+        Configuration end = new TraceReplayer().replay(program, failing);
+        assertTrue(end.isDeadlockCandidate(), "Replayed configuration must be a deadlock candidate");
+        assertFalse(invariant.holds(end.state(), end), "Invariant must fail");
+
+        DeltaDebugger debugger = new DeltaDebugger();
+        Trace minimized = debugger.minimize(program, failing, TraceOutcome.VIOLATION, invariant);
+
+        assertEquals(List.of(0), minimized.threadIds(), "Should shrink away T1's irrelevant read");
+        assertEquals(List.of(StepOutcome.ADVANCED), minimized.outcomes());
+    }
 }
+

src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java

@@ -0,0 +1,55 @@
+/** Verifies trace replay against actual step execution and detects corrupted outcomes. */
+package dev.samhb.interleave.search;
+
+import dev.samhb.interleave.bugs.ReadCounterStep;
+import dev.samhb.interleave.bugs.WriteCounterStep;
+import dev.samhb.interleave.core.*;
+import org.junit.jupiter.api.Test;
+
+import java.util.List;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+class TraceReplayerTest {
+
+    @Test
+    void replay_matchingTrace_succeeds() {
+        Program program = new Program(CounterState.of(0), List.of(
+            new ModelThread(0, List.of(new WriteCounterStep(0), new ReadCounterStep(0)))
+        ));
+
+        Trace trace = Trace.of(
+            List.of(0, 0),
+            List.of(StepOutcome.ADVANCED, StepOutcome.ADVANCED),
+            TraceOutcome.COMPLETED
+        );
+
+        TraceReplayer replayer = new TraceReplayer();
+        Configuration end = replayer.replay(program, trace);
+
+        assertEquals(1, ((CounterState) end.state()).counter());
+        assertTrue(end.allTerminated());
+    }
+
+    @Test
+    void replay_divergentOutcome_throwsCorruptedTraceException() {
+        Program program = new Program(CounterState.of(0), List.of(
+            new ModelThread(0, List.of(new WriteCounterStep(0)))
+        ));
+
+        // The step produces StepOutcome.ADVANCED, but the trace erroneously claims BLOCKED
+        Trace corruptedTrace = Trace.of(
+            List.of(0),
+            List.of(StepOutcome.BLOCKED),
+            TraceOutcome.VIOLATION
+        );
+
+        TraceReplayer replayer = new TraceReplayer();
+        CorruptedTraceException ex = assertThrows(
+            CorruptedTraceException.class,
+            () -> replayer.replay(program, corruptedTrace)
+        );
+
+        assertTrue(ex.getMessage().contains("recorded BLOCKED but execution produced ADVANCED"));
+    }
+}