[Codegen#52] Generated Rust license follows the consumer: user choice, then repo license, else none #52

Problem

The generator always stamps // SPDX-License-Identifier: MIT OR Apache-2.0 on emitted Rust (NFR-002). That code lands in someone else's codebase, so its license is theirs to decide, not ours.

Required behavior (owner decision 2026-09-15)

The SPDX identity of generated source is resolved in this order:

1. User's explicit choice: a generator option (e.g. license: <SPDX expression>) is stamped verbatim.
2. Repository license: if no option is given, use the consuming repository's declared license (e.g. the target crate's Cargo.toml license, or the workspace package.license).
3. Nothing: if neither is stated, emit no SPDX header. The file then falls under the repo's own terms, or is closed / all rights reserved if the repo has none. No license means private.

The generator must never stamp a license the user or repo didn't state. That includes our AGPL, and it includes a permissive default.

Scope

• Emitter SPDX sites: src/bound_strategy/generation.rs, src/bound_strategy/population.rs, src/harness.rs, src/kani.rs, src/oracle.rs, src/strategy.rs
• Schemas generated-rust-kani-v1, generated-rust-kani-v2, generated-rust-oracle-v1: the required ^// SPDX-License-Identifier: MIT OR Apache-2\\.0\\n pattern must allow any valid SPDX expression or no header. This is a schema change, so decide whether it needs a new schema version.
• The provenance/identity envelope should record which source the license came from (option, repo, or none).
• Spec: rewrite NFR-002 (the "dual-licence" requirement and AC-2), interface-001-codegen-api.md licensing line, and add TCs for each of the 3 resolution branches.
• Tests and examples: tests/oracle_generation.rs, examples/generation_conformance.rs (the 3 "dual-license" checks), the tests/fixtures/generated_boolean_oracle.golden golden, and assurance/change-assurance.json.
• README license note.
• quire-contract-ir spec/program/PGM-01-governance.md:83 ("Generated source defaults to MIT OR Apache-2.0") needs the matching policy change.

Acceptance

• An explicit option produces exactly that SPDX line.
• No option in a repo with a declared license produces that repo's license.
• No option and no repo license produces no SPDX line.
• An invalid SPDX expression in the option is rejected with a file:line-bearing error.

🤖 Generated with Claude Code

https://claude.ai/code/session_01SXCEodZi7YFYHt43Dm5PVw