[TRACK_F] FIX: Stop the fast-mode metrics fallback from carrying non-Coq claims

[ib823]

Summary

When reports/noncoq_mechanized_status.json was stale, scripts/generate-metrics.sh --fast fell back to the previous metrics.json. The pre-commit hook and deploy-website.sh both use this path. The fallback rebuilt each lane's *_COMPILED and *_MECHANIZED_READY from two sources: the previously published claimLevels, and smoke passes.

So a smoke pass became a published "compiled" claim. Every later fast run then read that claim back as evidence, so the overclaim kept itself alive. This is what put Alloy at "compiled" during the PR #89 deploy, until the public claim-integrity gate refused the sync.

Changes

• The fallback no longer carries claims. It keeps only descriptive fields:

  • pending reasons ("none" becomes the stale-report reason);
  • backlogs;
  • smoke results this run did not observe.

  Without a fresh report, every non-Coq lane is generated. That is the rule public-quality-gates.sh already enforces.

• A smoke result observed in this run beats a cached one. Each smoke check now records whether it actually ran, so a cached pass can no longer hide a smoke check that now fails.

• One freshness rule. report_head_matches_or_compatible in the generator now matches the public gate:

  • lane paths must be content-identical between the report's commit and HEAD;
  • .md files are ignored;
  • no ancestry is required;
  • a missing commit or a failing git diff counts as stale.

  Before, the generator could call a report stale that the gate accepted as fresh.

• Isabelle: a smoke pass no longer sets isabelleCompiled. This extends the HONESTY POLICY that already covered F*, TLA+ and Alloy. The flaw was hidden only because the Isabelle lane is retired.

• New test: scripts/test-generate-metrics-fallback.sh runs the generator in a throwaway clone (about 3 minutes) and covers three scenarios:

  1. A stale report plus inflated cached metrics: no claim survives, including across a second run.
  2. A smoke check observed failing beats a cached pass.
  3. The freshness rule agrees with the gate: a markdown-only lane change keeps the report fresh, and a code change makes it stale.

• RIINA_MASTER_PLAN.md Part 11 records the fix and closes the open item noted in the PR Audit remediation: proof integrity, new core theorems, compiler/runtime soundness, supply chain #89 deploy entry.

Type

• Bug fix
• New feature
• Documentation
• Example .rii file
• Formal proof
• Refactor

Testing

• cargo test --all passes: 3,528 tests in the pre-commit hook. No Rust code changed.
• cargo clippy -- -D warnings passes
• Coq build passes (make in 02_FORMAL/coq/) — not applicable, no proofs changed
• New tests added for new functionality: scripts/test-generate-metrics-fallback.sh fails 32 assertions against the generator on main (the original bug, reproduced) and passes against this branch.
• generate-metrics.sh --fast on this tree: published claims are unchanged (the current report is fresh). Only the timestamp, commit and branch fields moved.
• public-quality-gates.sh (claim integrity PASS), audit-docs.sh (all current) and update-proof-ledger.sh --check (up to date).
• Pre-push hook, including the strict security gates.

Checklist

• No external dependencies added
• No unsafe without justification
• No Admitted in Coq proofs
• Examples use Bahasa Melayu keywords — not applicable

🤖 Generated with Claude Code

https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

---

Generated by Claude Code