Add hash-bound Pilot C project lifecycle

[Mnehmos]

What

• Carry an optional, SHA-256-bound Lake project archive through formalization, verification, audit, publication, release, and MathCorpus export.
• Safely extract project tarballs and run the exact module from the bound project closure.
• Reuse the immutable verifier result during audit instead of rebuilding it.
• Add the Linux publication profile with a 12 GiB limit, Bubblewrap network isolation, and an exact Elan toolchain mount.
• Add protected Pilot C candidate/authority and fresh database-free release jobs while preserving the existing Pilot A path.
• Retain project.tar in both release replay material and the MathCorpus Lean project export.

Why

The standalone worker only materialized Final.lean. The BH proof imports project-local modules under the BH prefix, so the real project failed before elaboration even though the final module itself was valid. Pilot C needs the whole hash-bound project closure, not a copied terminal file.

Impact

• The exact BH project now completes local diagnostic verification and audit with its project, environment, module, declaration, logs, and axiom closure all hash-bound.
• Publication-mode workers require enforced memory and network controls.
• Release verification runs after SQLite is moved outside the state root, and the release/corpus artifacts preserve the project archive without database access.
• Pilot A behavior and its regular protected-main trigger remain unchanged.

Verification

• cargo fmt --all -- --check
• cargo clippy --locked --workspace --all-targets --all-features -- -D warnings
• cargo test --locked --workspace --quiet (213 library tests plus all workspace targets)
• python -m unittest discover -s tests -v (39 tests)
• shellcheck and bash -n for all changed shell scripts
• actionlint for publication.yml and ci.yml
• Exact local BH diagnostic:
  • verifier job 019f9c73-18d3-7d91-8e72-24073e3fae7c
  • report 50a436a723b4b79d22bdda0d99f079809b654c9af38b8f36c2c66ec3088bc36b
  • elaborated successfully with exactly Classical.choice, Quot.sound, and propext
• Exact local BH audit:
  • audit job 019f9d3d-1247-76b2-8675-a6217f9f29c4
  • report 6e8dfcc92b89ac547ea05d5d61c5bac8427580727862216a585a5eebe296886a
  • passed with complete dependency closure and identical retained verifier logs

Local evidence is intentionally non-authoritative. Protected publication authority and the database-free release are exercised only by the protected-main Pilot C workflow after merge.

Refs #74
Refs #25

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro Plus

Run ID: 92dcce25-b044-47ac-9afb-799f1105fe40

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch feat/pilot-c-vertical

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}