feat(verifier): Add --keep-all-files option

[olivier-aws]

Add a --keep-all-files CLI option that forwards a directory to Strata so the intermediate Laurel and Core IR emitted after each pipeline phase is retained for debugging. The directory is resolved to an absolute path and used as a <dir> prefix when invoking the Strata backend.

Thread the new keepAllFilesDir field through VerifierOptions and update the test engine and EmitLaurelWorkflowTest call sites accordingly.

What was changed?

How has this been tested?

Manually tested.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.

[fabiomadge]

Approve — sound and correct. Debug-only flag; unset → command line byte-identical. /program prefix + toAbsolutePath() both right (process runs from StrataCLI). All three VerifierOptions sites updated. Verified locally on a rebuilt backend.

Two non-blocking points:

1. Silently ignored with --emit-laurel — emit-only mode returns before runVerifier. Worth a help-text note.
2. No test. Proposing this (passes locally): positive case asserts a verified method is counted; negative case (check(1 == 2)) proves the round-trip preserves the obligation; keep-all-files case asserts the dir is created and both Laurel and Core dumps land in it. Suffixes/prefix only, so it survives pipeline changes. Spawns the real Strata process, like the existing test.

@Test
public void emittedLaurelVerifiesAndCountsAVerifiedMethod() throws Exception {
    var result = emitThenVerify("""
            import static org.strata.jverify.JVerify.*;
            class Emit {
                static void trueCheck() { check(1 == 1); }
            }
            """);
    assertEquals(0, result.exitCode(), "true program should verify");
    assertNotNull(result.verificationResults());
    assertTrue(result.verificationResults().verificationPassedMethods() > 0,
            "the verified method must be counted, not vacuously skipped");
    assertEquals(0, result.verificationResults().verificationFailedAssertions());
}

@Test
public void emittedLaurelStillCatchesAFalseObligation() throws Exception {
    var result = emitThenVerify("""
            import static org.strata.jverify.JVerify.*;
            class Emit {
                static void falseCheck() { check(1 == 2); }
            }
            """);
    assertNotEquals(0, result.exitCode(), "false program must not verify clean");
    assertTrue(result.verificationResults().verificationFailedAssertions() > 0,
            "the false check must produce a failed assertion");
}

@Test
public void keepAllFilesWritesIntermediateIrIntoRequestedDir() throws Exception {
    var keepDir = Files.createTempDirectory("keep-all-files-test")
            .resolve("nested-not-yet-created");
    assertFalse(Files.exists(keepDir), "precondition: dir does not exist yet");

    var source = """
            import static org.strata.jverify.JVerify.*;
            class Emit { static void trivial() { check(1 == 1); } }
            """;
    var driver = Driver.getDriver(withKeepAllFiles(baseOptions(), keepDir));
    driver.verifyJavaFiles(new java.util.ArrayList<>(List.of(
            new SourceFile(Path.of("Emit.java"), source))));

    assertTrue(Files.isDirectory(keepDir),
            "--keep-all-files must create the requested directory");
    try (Stream<Path> files = Files.list(keepDir)) {
        var names = files.map(p -> p.getFileName().toString()).sorted().toList();
        assertFalse(names.isEmpty(), "intermediate IR files should have been written");
        assertTrue(names.stream().allMatch(n -> n.startsWith("program.")),
                "emitted files should use the 'program' prefix: " + names);
        // Both IR families kept (the feature claim), decoupled from phase names/counts.
        assertTrue(names.stream().anyMatch(n -> n.endsWith(".laurel.st")),
                "a Laurel-phase dump should be present: " + names);
        assertTrue(names.stream().anyMatch(n -> n.endsWith(".core.st")),
                "a Core-phase dump should be present: " + names);
    }
}

Helpers (emitThenVerify, withKeepAllFiles, baseOptions) omitted for brevity.