diff --git a/README.md b/README.md index cef518e..925c3b2 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,22 @@ External **Lean 4** proof backend for the [mumei](https://github.com/mumei-lang/ For P9-G NLAE integration, mumei-lean is the Fidelity Checker: it confirms that reconstructed `.mm` obligations can become `lean_verified` certificates, including live generated theorem paths. +## Distributed proof bundle verification + +mumei release bundles expose per-module certificates and a bundle-level +`lean_provenance` index. Consumers use `artifact_paths` to locate each +certificate and source, confirm `z3_check_result: "lean_verified"` together +with the current `translator_version`, `bridge_lemma_hash`, and +`manual_lemma_reason`, and re-run: + +```bash +mumei verify-cert --strict +``` + +Use `--allow-lean-verified` explicitly on mumei acceptance paths that permit +Lean results. A translator or bridge-lemma mismatch is `stale_translator`, not +a successful proof. + ## Unknown obligation bridge contract The promoted path is: select Z3 `unknown` atoms, translate them with typed metadata, build generated Lean, export a certificate with `translator_version` and `bridge_lemma_hash`, and let mumei accept only matching `lean_verified` results. Eight live theorem paths are covered: `abs_saturating`, `bounded_mul_with_overflow_check`, `constant_time_eq_flag`, `ff_zero_eq_zero`, `verified_insertion_sort_ascending`, `poly_bound_monotone`, `exists_pivot_partition`, and `sum_nonneg_inductive`. See [`docs/LEAN_HARNESS_CONTRACT.md`](docs/LEAN_HARNESS_CONTRACT.md) for per-path details. diff --git a/docs/BRIDGE_HARNESS_SPEC.md b/docs/BRIDGE_HARNESS_SPEC.md index 857b9a9..7d16cb9 100644 --- a/docs/BRIDGE_HARNESS_SPEC.md +++ b/docs/BRIDGE_HARNESS_SPEC.md @@ -11,6 +11,18 @@ For the artifact-level contract covering `.proof-cert.json`, generated Lean, Vocabulary is inherited from the cross-project roadmap: `harness_contract`, `intent_fidelity`, `artifact_paths`, `budget_policy_fingerprint`, and `lean_verified` are the only canonical field names. +## Distributed bundle verification + +Consumers of a distributed `std-proof-bundle.json` should use its +`artifact_paths` to locate the packaged per-module certificate and source, then +check the corresponding `lean_provenance` entry. Promotion requires +`z3_check_result == "lean_verified"` plus matching `translator_version` and +`bridge_lemma_hash`; `manual_lemma_reason` must be inspected and must not hide an +unresolved manual obligation. Re-run the packaged certificate with +`mumei verify-cert --strict`. Where the mumei acceptance +path allows Lean results, add `--allow-lean-verified` explicitly. Any metadata +mismatch remains `stale_translator` and is not proven. + ## Unknown obligation bridge contract diff --git a/docs/LEAN_HARNESS_CONTRACT.md b/docs/LEAN_HARNESS_CONTRACT.md index ab86fc4..287d427 100644 --- a/docs/LEAN_HARNESS_CONTRACT.md +++ b/docs/LEAN_HARNESS_CONTRACT.md @@ -8,6 +8,23 @@ contract that callers can use to validate inputs, generated Lean, `lake build`, The cross-project roadmap is the sole upper roadmap. This contract uses the canonical field names `harness_contract`, `intent_fidelity`, `artifact_paths`, `budget_policy_fingerprint`, and `lean_verified` without aliases. The docs-sync and code-surface contract is pinned by `tests/test_contract_vocabulary.py` so `lean_verified`, `stale_translator`, `translator_version`, and `bridge_lemma_hash` do not drift. The test covers docs text, Python bridge code constants (`scripts/export_cert.py` `TRANSLATOR_VERSION` / `BRIDGE_LEMMA_HASH` ↔ document pinned values), and code-surface alias drift in docstrings, argparse help, and user-visible output strings across `scripts/export_cert.py`, `scripts/bridge.py`, `scripts/ingest_cert.py`, and `scripts/bridge_harness.py`. +## Distributed bundle consumer procedure + +When consuming a distributed proof bundle, use `artifact_paths` to locate the +per-module certificate and source, then select the module and atom from +`lean_provenance`. Confirm `z3_check_result == "lean_verified"` and verify the +entry's `translator_version`, `bridge_lemma_hash`, and `manual_lemma_reason`. +Re-run the packaged certificate with: + +```bash +mumei verify-cert --strict +``` + +If the mumei acceptance path is configured to accept Lean-proved atoms, pass +`--allow-lean-verified` explicitly as well. The certificate and provenance must +agree with the current translator contract; otherwise the result is +`stale_translator` and must remain unproven. + ## Unknown obligation bridge contract diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 217e8c7..b9088cd 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -6,6 +6,23 @@ Promotion to `lean_verified` requires a successful Lean build plus matching `translator_version` and `bridge_lemma_hash` in both the exported atom and `lean_result_metadata`; mismatches are `stale_translator`. PRs that update this roadmap should review the cross-project roadmap in the same diff and record relevant bridge regression commands from `tests/`. +### Priority 17 bridge surface + +The mumei `docs/CROSS_PROJECT_ROADMAP.md` is canonical for the cross-project +Priority 17 contract. This local checkpoint records only the Lean-relevant +surface: distributed proof bundles expose `lean_provenance` entries whose +`z3_check_result` is `"lean_verified"` together with `translator_version`, +`bridge_lemma_hash`, and `manual_lemma_reason`. Consumers must preserve +`stale_translator` as the signal for translator or bridge-lemma drift. + +For a distributed bundle, locate the referenced certificate using its +`artifact_paths`, inspect the matching `lean_provenance` entry, and confirm the +atom has `z3_check_result == "lean_verified"`, current `translator_version` and +`bridge_lemma_hash`, and an understood `manual_lemma_reason`. Re-run +`mumei verify-cert --strict`; on a mumei acceptance path +that permits Lean results, pass `--allow-lean-verified` explicitly. A mismatch +remains `stale_translator` and is not promoted. + Run the local contract vocabulary gate before opening a PR that touches `README.md`, `docs/LEAN_HARNESS_CONTRACT.md`, `docs/INTEGRATION.md`, or the bridge scripts: ```bash