[ivmat]

Resolves #4983. Part of #942 (RFC 0015, #4727). Follows #4941.

Description

RFC 0015 says an earlier --export-json file is replaced by an INCOMPLETE marker when verification
begins. Without it, a run that is killed during verification leaves the earlier COMPLETE document in
place, and that document looks current (see the
#4941 review).

• After the build and harness selection succeed, Kani builds the run context once and writes the
  marker with the same atomic write as the final document. After verification, the final document
  from the same context replaces it, so started_at and the other shared fields are equal in both.
• The marker has the fields of the RFC presence matrix and run_state: "INCOMPLETE", and no
  outcome, wall_time_s, summary or harnesses.
• A failed marker write stops the run before any harness is verified. A build error or a rejected
  harness selection (a filter that matches nothing) leaves an earlier file in place.
• wall_time_s now also covers the tool version probes and the marker write. The build is still not
  included.

This implements the marker that the RFC proposes. The RFC's open question "marker or delete-up-front"
is unchanged; the flag stays unstable. The docs and the RFC text are updated to match.

Readers of the export should treat a run_state other than COMPLETE as incomplete evidence. For example,
kani-mcp in #5059 deletes any earlier export before a run and reports a timeout only when no export exists.
With this change, a run that stops after the marker write leaves an INCOMPLETE export, so the existence of
the file alone does not show that verification finished.

Testing

• Unit tests: the marker's exact key set, and null metadata serialized as null; a marker and a final
  document from one context have equal shared fields.
• tests/json-handler/incomplete-marker runs the real driver with a fake cbmc that waits for a
  release file. Killing the driver leaves the marker; releasing it gives a final document with the
  marker's started_at; a bad export path and a rejected --harness filter stop the run before
  CBMC verification starts.
• Each of these mutations makes a test fail: the marker written after verification, the marker
  written before harness selection, a marker write error ignored, summary: null in the marker, and
  a recomputed started_at.
• Full regression, cargo clippy and cargo fmt --check pass at 1b6fefa.

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