feat(modes/manifest): per-repo A2ML manifest schema v2.0 (closes C12 estate blocker)

[hyperpolymath]

Summary

Closes the estate-onboarding blocker C12 surfaced in the recent "what stops echidna from running proof work across the estate" audit. The v1.0 directive at .machine_readable/bot_directives/echidnabot.a2ml only carried [bot] mode, so onboarding the ~325-repo estate required ad-hoc per-bot conventions and out-of-band agreement on which provers, file globs, timeouts, axiom rules, and merge gates applied per repo.

This adds src/modes/manifest.rs::RepoManifest with five new sections, additively over v1.0:

Section	Purpose
[provers]	whitelist / blacklist + per-prover overrides (flags, timeout, lake)
[proofs]	include / exclude globs (extension fallback when include is empty)
[axioms]	forbid tokens (Admitted/sorry/postulate/...) + info/warning/error
[merge_block]	Regulator-mode gates: min_confidence (1..5) + axiom_severity
[blocked_on]	upstream-blocker labels surfaced in PR comments / check summaries

Backwards compatibility

• v1.0 directives keep parsing — parse_a2ml_directive is unchanged.
• RepoManifest::effective_mode(default) mirrors the v1.0 resolver shape.
• Unknown fields are silently ignored so future schema versions don't break older echidnabot builds.
• Missing fields fall back to documented defaults.

Two estate-shaped fixtures

• tests/fixtures/manifest/ephapax.a2ml — Regulator + Coq-only + Admitted/sorry forbidden + Semantics.v excluded (mirrors the four-layer redesign in formal/PRESERVATION-DESIGN.md).
• tests/fixtures/manifest/valence-shell.a2ml — Advisor + Coq+Idris2 + sorry-only forbid (matches the Idris2 0.8.0 oracle maturity caveat).

Test plan

• 14 unit tests cover the v1.0 path, the full v2.0 path, unknown-field tolerance, prover whitelist/blacklist semantics, empty-manifest detection, axiom-severity ordering, disabled-bot, invalid-TOML, and both fixtures parse cleanly.
• cargo check --lib green (with local shared-context path override).
• cargo test --lib modes::manifest:: → 14 passed; 0 failed.

Notes

• Schema documentation lives in the module rustdoc (//! block at the head of src/modes/manifest.rs) and is exemplified by the two fixtures.
• The aspirational .echidnabot.toml block in docs/content/configuration.md is left unchanged — that file lacks an SPDX header and SPDX/licence edits are owner-only per estate policy. A follow-up doc PR (with owner sign-off on the SPDX header) is the natural home for the user-facing schema reference.
• Estate context: this PR is fix: complete ProverSlug migration + Tier-3 prover coverage #1 of 5 in the C12/C14/C15/B7/D18 critical-blocker pass coming out of the echidna estate-scale audit.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 152 issues detected

Severity	Count
🔴 Critical	11
🟠 High	12
🟡 Medium	129

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI task file -- delete or move to docs/",
    "type": "stale",
    "file": "SONNET-TASKS.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Action us cache\n        uses: actions/cache@8b402f58fbc84540c8b491a91e5 needs attention",
    "type": "unpinned_action",
    "file": "echidna-fuzz.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "echidnabot.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence