Build discovery

theoremc now uses a root-level build.rs script to discover theorem files under theorems/**/*.theorem.

The build-time contract is:

• theorem files are discovered recursively from the crate-root theorems/ directory,
• discovered theorem paths are normalized to forward-slash crate-relative form and sorted deterministically, and
• editing a discovered .theorem file causes Cargo to rerun the build script on the next build.

The repository does not need a pre-seeded theorems/ directory. On the supported toolchain, theoremc watches the root theorems path even when it is absent, so creating the directory and adding the first theorem later still causes the next build to rerun the build script.

Only files ending in .theorem are treated as theorem inputs. However, the root theorems/ directory is watched so Cargo can notice newly created theorem trees. As a result, changes elsewhere under that watched directory may still rerun the build script even though non-.theorem files are not parsed or fed into later theorem compilation steps.

After discovery, theoremc compiles each discovered theorem file through the public theorem_file! proc macro. Each invocation expands to a deterministic private per-file module, includes the theorem source via include_str!(concat!(env!("CARGO_MANIFEST_DIR"), "/", P)), and creates one stable Kani proof harness stub per theorem document in that file. Evidence.kani is required for every theorem compiled by theorem_file!; omitting it fails macro expansion with MissingKaniEvidence. The generated Kani module is compiled only when cfg(kani) is active, so ordinary cargo build does not require Kani to be installed or available as a dependency. Invalid theorem files therefore fail the Rust build during macro expansion, using the same schema diagnostics returned by load_theorem_docs_with_source or the macro-specific missing Kani evidence diagnostic.