Skip to content

docs: sync mumei-side live generated theorem path count to thirteen - #491

Merged
AkiraTamai merged 1 commit into
developfrom
devin/1785653053-docs-sync-live-paths
Aug 4, 2026
Merged

docs: sync mumei-side live generated theorem path count to thirteen#491
AkiraTamai merged 1 commit into
developfrom
devin/1785653053-docs-sync-live-paths

Conversation

@AkiraTamai

Copy link
Copy Markdown
Collaborator

Summary

docs-sync only. docs/CROSS_PROJECT_ROADMAP.md §SI-6 already lists 13 live generated Lean bridge paths (through predicate_guard_collapse), but three other places still carried stale counts:

  • docs/STDLIB.md: "eight live generated theorem paths" + 8-item list → thirteen, adding rtgs_transfer_conservation, ff_mul_commutative, ff_mul_associative, ff_mul_add_distributive, predicate_guard_collapse.
  • docs/ROADMAP.md: "(ten in total: …)" → thirteen with the same list.
  • docs/CROSS_PROJECT_ROADMAP.md V1 summary table/prose (10 live generated theorem paths13), noting that paths 12/13 have no bridge lemma template and are adopted by the deterministic 16-candidate tactic search (mumei_ff_mod / tauto), so bridge_lemma_hash is unchanged.

Source of truth is the mumei-lean implementation (tests/test_lean_bridge_e2e.py + the 13 live *.proof-cert.json fixtures); the matching mumei-lean docs sync is mumei-lang/mumei-lean#109. No vocabulary, verdict, or audit-key change: harness_contract, intent_fidelity, artifact_paths, budget_policy_fingerprint, lean_verified and the 8 fixed audit keys are untouched.

Regression commands

# mumei
python3 scripts/check_contract_vocabulary.py           # passed
python3 scripts/generate_stdlib_metrics.py --mumei-bin target/debug/mumei
#   → 59 modules (59 OK / 0 FAIL / 0 SKIP), 344 atoms (344 proven · 0 trusted), health 1.000
#     i.e. docs/STDLIB_METRICS.md already matches the implementation; no regeneration needed here.

# mumei-agent
uv run pytest tests/test_contract_vocabulary.py -q     # 7 passed

# mumei-lean
PYTHONPATH=scripts MUMEI_LEAN_SKIP_LIVE=1 python -m pytest -q   # 306 passed, 11 skipped

Link to Devin session: https://app.devin.ai/sessions/adfa18cdf78948c09b218b54aa5a83b0
Requested by: @AkiraTamai

Co-Authored-By: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
@AkiraTamai AkiraTamai self-assigned this Aug 2, 2026
@devin-ai-integration

Copy link
Copy Markdown
Contributor

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

  • Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
  • Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

  • Disable automatic comment, CI, and merge conflict monitoring

@AkiraTamai
AkiraTamai marked this pull request as ready for review August 2, 2026 06:50

@devin-ai-integration devin-ai-integration Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✅ Devin Review: No Issues Found

Devin Review analyzed this PR and found no bugs or issues to report.

Open in Devin Review

@AkiraTamai
AkiraTamai merged commit 9199a17 into develop Aug 4, 2026
2 checks passed
@AkiraTamai
AkiraTamai deleted the devin/1785653053-docs-sync-live-paths branch August 4, 2026 06:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant