Witness data via trace; Python WitnessCreator #57

Replace stdout witness markers with witness data in the trace, and turn WitnessCreator into a Python package.

Current state: the executor prints base64 @@@ markers ([WITNESS], [WITNESS_TARGET]) to stdout, the driver scrapes the last round from the log and passes everything as one argv to the Java WitnessCreator.

Plan:

• WitnessCreator → Python package (stays its own repo; also used outside SWAT): typed model (NondetReturn, Violation, Location, Task), YAML 2.3 writer (+ GraphML while still needed), stdlib only. Standalone CLI reads a versioned JSON event file; legacy @@@ markers supported in the CLI only.
• Executor: InputDTO gets a location (class, source file, line, call index on the line); TraceDTO gets a violation entry (throwable, stack frames). [WITNESS]/[WITNESS_TARGET] stdout output is removed.
• Explorer (SV-COMP mode) imports the package and writes the witness from the trace of the violating round. No stdout parsing for witnesses.
• If abrupt JVM exits (e.g. System.exit, StackOverflow in the task) lose the trace in testing, send the trace in those cases too.
• Package is pinned in the explorer requirements and vendored into the SV-COMP archive (libs/python/, see Make SV-COMP archive run on Ubuntu 26.04 #52). The jar is no longer needed in the archive.

Also from the review of WitnessCreator#1, for this rewrite:

• Exactly one final (target) segment per violation witness, enforced by a test (WitnessLint does not check this)
• Target statement column: innermost statement/full expression, not the first token of the line
• Golden end-to-end tests on sv-benchmarks tasks + WitnessLint in CI
• Executor: SVCompMethodAdapter rewrites nondetObject to an invalid descriptor (see Support Verifier.nondetObject #53); any method named assume is redirected regardless of owner

Target: final resubmission (Nov 17).