Theorem harness naming

The theoremc::mangle module also provides deterministic theorem harness naming for Kani proof functions. Each theorem document maps to a harness identifier of the form:

theorem__{theorem_slug(T)}__h{hash12(P#T)}

Generated Kani proof harnesses live under the generated per-file module's kani submodule. That submodule is gated with #[cfg(kani)]; ordinary Rust builds still parse and validate theorem files, but they do not compile Kani attributes or require the Kani crate. Kani-targeted builds can discover these harnesses with their short harness identifiers or full module-qualified paths.

Each generated harness currently has an empty body and carries:

• #[kani::proof]
• #[kani::unwind(n)], where n comes from Evidence.kani.unwind

Final theorem step semantics, including symbolic inputs, assumptions, assertions, witnesses, and action calls, are implemented in later roadmap steps.

Where:

• P is the literal theorem file path string supplied by the caller.
• T is the theorem identifier from the Theorem field.
• theorem_key(P, T) is the exact string {P}#{T}.
• theorem_slug(T) preserves identifiers already matching ^[a-z_][a-z0-9_]*$ and otherwise converts CamelCase deterministically, including acronym and digit boundaries.

• theorem_key(path, theorem) — returns the exact theorem key {P}#{T}.
• theorem_slug(theorem) — returns the deterministic harness slug.
• mangle_theorem_harness(path, theorem) — returns a MangledHarness with theorem(), slug(), theorem_key(), hash(), and identifier() accessors.

use theoremc::mangle::{hash12, mangle_theorem_harness, theorem_key, theorem_slug};

assert_eq!(
    theorem_key(
        "theorems/bidirectional.theorem",
        "BidirectionalLinksCommitPath3Nodes",
    ),
    "theorems/bidirectional.theorem#BidirectionalLinksCommitPath3Nodes",
);
assert_eq!(
    theorem_slug("BidirectionalLinksCommitPath3Nodes"),
    "bidirectional_links_commit_path_3_nodes",
);

let harness = mangle_theorem_harness(
    "theorems/bidirectional.theorem",
    "BidirectionalLinksCommitPath3Nodes",
);
assert_eq!(
    harness.identifier(),
    format!(
        "theorem__bidirectional_links_commit_path_3_nodes__h{}",
        hash12(&theorem_key(
            "theorems/bidirectional.theorem",
            "BidirectionalLinksCommitPath3Nodes",
        )),
    ),
);

load_theorem_docs_with_source now rejects duplicate theorem keys before code generation. In the current loader boundary this means a multi-document .theorem source cannot declare the same Theorem identifier twice, because both documents would produce the same literal theorem key {source}#{Theorem}.

The loader returns SchemaError::DuplicateTheoremKey with:

• the exact colliding theorem key,
• structured collision diagnostics naming every duplicate theorem-key occurrence in deterministic order, and
• a structured diagnostic pointing at the duplicate theorem field.