autoharness_analyzer fails on metadata from current Kani #679

The analyzer cannot deserialize two skip reasons that Kani at main now writes to kani-metadata.json. Fed a file containing either, it exits with:

Error: invalid type: string "no candidate instantiation", expected unit
Error: unknown variant `RequiresBoundedArguments`, expected one of `GenericFn`, `KaniImpl`, `MissingArbitraryImpl`, `NoBody`, `UserFilter`

scripts/autoharness_analyzer/src/main.rs keeps its own copy of AutoHarnessSkipReason (lines 54 to 77) instead of depending on kani_metadata. Two changes to the real enum are missing from the copy: model-checking/kani#4679 made GenericFn carry a String, and model-checking/kani#4691 added RequiresBoundedArguments(Vec<(String, String)>). CI does not see this because run-kani.sh builds Kani at the pinned commit d4df833c, which predates both.

Reproduce

Minimal metadata/core-kani-metadata.json, one file per new shape:

{ "crate_name": "core", "autoharness_md": { "chosen": [],
  "skipped": { "f": { "GenericFn": "no candidate instantiation" } } } }

{ "crate_name": "core", "autoharness_md": { "chosen": [],
  "skipped": { "g": { "RequiresBoundedArguments": [["s", "&[u8]"]] } } } }

With a header-only scanner_results/core_scan_functions.csv:

cargo run -- metadata/ scanner_results/ --for-crate core

Each fails with the corresponding error above, from main.rs:130. The same layout with the old shapes ("GenericFn" as a bare string, no RequiresBoundedArguments) passes.

I can send a PR. It needs to keep reading the old GenericFn form alongside the new one, since CI will keep building the pinned Kani until tool_config/kani-version.toml moves. I would also give RequiresBoundedArguments its own table instead of folding it into the missing-implementation breakdown, since it needs a flag rather than an implementation.

I will open a separate issue on Kani about versioning kani-metadata.json, which kani list output already does.